		Search-engine friendly clone of the ACL2 documentation.

Lex-numbers

Vl-lex-time-or-real-number

Match real_number or time_literal.

Signature
(vl-lex-time-or-real-number echars st) → (mv token? remainder)
Arguments: echars — Characters we're lexing.
Guard (vl-echarlist-p echars).; st — Governs whether time_literals are valid.
Guard (vl-lexstate-p st).

Verilog-2005 has no time_literals and the syntax for real numbers is just:

sign ::= + | -
exp ::= e | E
real_number ::=                        // no embedded spaces
   unsigned_number . unsigned_number
 | unsigned_number [ . unsigned_number ] exp [ sign ] unsigned_number

SystemVerilog-2012 slightly tweaks real_number, but it is exactly equivalent to the above:

real_number ::=                       // no embedded spaces
   fixed_point_number
 | unsigned_number [ . unsigned_number ] exp [ sign ] unsigned_number

fixed_point_number ::= unsigned_number . unsigned_number

However, this new fixed_point_number is also used in time_literals:

time_literal ::=                      // no embedded spaces
     unsigned_number time_unit
   | fixed_point_number time_unit

time_unit ::= s | ms | us | ns | ps | fs

And lexing these is slightly subtle because we now need to check for these extra possibilities, e.g., 37.45us is a time literal whereas 37.45 followed by something else is a real number.

Definitions and Theorems

Function: vl-lex-time-or-real-number

(defun vl-lex-time-or-real-number (echars st)
 (declare (xargs :guard (and (vl-echarlist-p echars)
                             (vl-lexstate-p st))))
 (let ((__function__ 'vl-lex-time-or-real-number))
  (declare (ignorable __function__))
  (b*
   (((mv ipart ipart-rest)
     (vl-read-unsigned-number echars))
    ((unless ipart) (mv nil echars))
    ((mv tail tail-rest)
     (vl-read-real-tail ipart-rest))
    ((when tail)
     (mv (make-vl-realtoken :etext (append ipart tail))
         tail-rest))
    ((vl-lexstate st) st)
    ((mv units units-rest)
     (if st.timelitsp (vl-read-time-unit ipart-rest)
       (mv nil ipart-rest)))
    ((when units)
     (mv
      (make-vl-timetoken
           :etext (append ipart units)
           :quantity (vl-echarlist->string ipart)
           :units (vl-timeunit-lookup (vl-echarlist->string units)))
      units-rest))
    ((mv dot dot-rest)
     (vl-read-literal "." ipart-rest))
    ((unless dot) (mv nil echars))
    ((mv fpart fpart-rest)
     (vl-read-unsigned-number dot-rest))
    ((unless fpart) (mv nil echars))
    ((mv tail tail-rest)
     (vl-read-real-tail fpart-rest))
    ((when tail)
     (mv (make-vl-realtoken :etext (append ipart dot fpart tail))
         tail-rest))
    ((mv units units-rest)
     (if st.timelitsp (vl-read-time-unit fpart-rest)
       (mv nil fpart-rest)))
    ((when units)
     (mv
      (make-vl-timetoken
           :etext (append ipart dot fpart units)
           :quantity (vl-echarlist->string (append ipart dot fpart))
           :units (vl-timeunit-lookup (vl-echarlist->string units)))
      units-rest)))
   (mv (make-vl-realtoken :etext (append ipart dot fpart))
       fpart-rest))))

Theorem: vl-token-p-of-vl-lex-time-or-real-number

(defthm vl-token-p-of-vl-lex-time-or-real-number
 (implies
   (and (force (vl-echarlist-p echars)) t)
   (equal
        (vl-token-p (mv-nth 0
                            (vl-lex-time-or-real-number echars st)))
        (if (mv-nth 0
                    (vl-lex-time-or-real-number echars st))
            t
          nil))))

Theorem: true-listp-of-vl-lex-time-or-real-number

(defthm true-listp-of-vl-lex-time-or-real-number
 (equal (true-listp (mv-nth 1
                            (vl-lex-time-or-real-number echars st)))
        (true-listp echars))
 :rule-classes
 ((:rewrite)
  (:type-prescription
   :corollary
   (implies
    (true-listp echars)
    (true-listp (mv-nth 1
                        (vl-lex-time-or-real-number echars st)))))))

Theorem: vl-echarlist-p-of-vl-lex-time-or-real-number

(defthm vl-echarlist-p-of-vl-lex-time-or-real-number
 (implies
  (force (vl-echarlist-p echars))
  (equal
    (vl-echarlist-p (mv-nth 1
                            (vl-lex-time-or-real-number echars st)))
    t)))

Theorem: append-of-vl-lex-time-or-real-number

(defthm append-of-vl-lex-time-or-real-number
 (implies
  (and (mv-nth 0
               (vl-lex-time-or-real-number echars st))
       (force (vl-echarlist-p echars))
       t)
  (equal
       (append (vl-token->etext
                    (mv-nth 0
                            (vl-lex-time-or-real-number echars st)))
               (mv-nth 1
                       (vl-lex-time-or-real-number echars st)))
       echars)))

Theorem: no-change-loser-of-vl-lex-time-or-real-number

(defthm no-change-loser-of-vl-lex-time-or-real-number
  (implies (not (mv-nth 0
                        (vl-lex-time-or-real-number echars st)))
           (equal (mv-nth 1
                          (vl-lex-time-or-real-number echars st))
                  echars)))

Theorem: acl2-count-of-vl-lex-time-or-real-number-weak

(defthm acl2-count-of-vl-lex-time-or-real-number-weak
  (<= (acl2-count (mv-nth 1
                          (vl-lex-time-or-real-number echars st)))
      (acl2-count echars))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-lex-time-or-real-number-strong

(defthm acl2-count-of-vl-lex-time-or-real-number-strong
 (implies
     (and (mv-nth 0
                  (vl-lex-time-or-real-number echars st))
          t)
     (< (acl2-count (mv-nth 1
                            (vl-lex-time-or-real-number echars st)))
        (acl2-count echars)))
 :rule-classes ((:rewrite) (:linear)))

Subtopics

Vl-lex-time-or-real-number-token/remainder-thms: Token and remainder theorems for vl-lex-time-or-real-number, automatically generated by def-token/remainder-thms.