		Search-engine friendly clone of the ACL2 documentation.

Lex-numbers

Vl-lex-integer

Match any integral_number.

Signature
(vl-lex-integer echars breakp warnings) → (mv token? remainder warnings)
Arguments: echars — Guard (vl-echarlist-p echars).; breakp — Guard (booleanp breakp).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

We assume here that we have already checked echars for real_number and time_literal numbers and haven't found any. So, e.g., if we encounter a plain unsigned_number here, we don't have to worry that it might be part of a real number.

The integral_number production is new in SystemVerilog-2012 and isn't part of Verilog-2005. However, except for real_number, it's directly compatible with Verilog-2005's number production, so this is basically completely compatible between both standards. A slightly tweaked view of the grammar is:

integral_number ::= decimal_number
                  | octal_number
                  | binary_number
                  | hex_number

hex_number     ::= [size] hex_base    hex_value
octal_number   ::= [size] octal_base  octal_value
binary_number  ::= [size] binary_base binary_value

decimal_number ::= unsigned_number
                 | [size] decimal_base decimal_value

size ::= non_zero_unsigned_number

Definitions and Theorems

Function: vl-lex-integer

(defun vl-lex-integer (echars breakp warnings)
 (declare (xargs :guard (and (vl-echarlist-p echars)
                             (booleanp breakp)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-lex-integer))
  (declare (ignorable __function__))
  (b*
   ((warnings (vl-warninglist-fix warnings))
    (breakp (and breakp t))
    ((mv number remainder1)
     (vl-read-unsigned-number echars))
    (normalized-number (vl-echarlist-kill-underscores number))
    (value-of-number
         (vl-echarlist-unsigned-value normalized-number 10))
    ((mv ws remainder2)
     (vl-read-while-whitespace remainder1))
    ((mv base remainder2)
     (vl-read-any-base remainder2))
    ((when (and (not number) (not base)))
     (mv nil echars warnings))
    (firstchar (if number (car number) (car base)))
    ((when (and number (not value-of-number)))
     (mv
      (raise
       "Lexer error (~s0): thought this was impossible; cannot ~
                    interpret ~s1 as a number."
       (vl-location-string (vl-echar->loc firstchar))
       (vl-echarlist->string number))
      echars warnings))
    ((unless base)
     (b*
      ((val-fix (mod value-of-number (expt 2 32)))
       (warnings
        (cond
         ((< value-of-number (expt 2 31))
          warnings)
         ((< value-of-number (expt 2 32))
          (warn
           :type :vl-warn-overflow
           :msg
           "~l0: the plain number ~s1 is in [2^31, ~
                                 2^32); it will be considered a negative ~
                                 number by 32-bit Verilog implementations, ~
                                 but will be positive on 64-bit systems, so ~
                                 you should add an explicit size."
           :args (list (vl-echar->loc firstchar)
                       (vl-echarlist->string number))))
         (t
          (warn
           :type :vl-warn-overflow
           :msg
           "~l0: the plain number ~s1 is over 2^32; we ~
                                 truncate it to ~x2 like a 32-bit Verilog ~
                                 implementation.  But this number will have a ~
                                 different value on 64-bit systems and ~
                                 beyond, so you should add an explicit size."
           :args (list (vl-echar->loc firstchar)
                       (vl-echarlist->string number)
                       val-fix)))))
       (token (make-vl-inttoken :etext number
                                :width 32
                                :signedp t
                                :value val-fix
                                :bits nil
                                :wasunsized t
                                :breakp breakp)))
      (mv token remainder1 warnings)))
    (width-was-0 (eql 0 value-of-number))
    (unsizedp (or (not number) width-was-0))
    (width (if unsizedp 32 value-of-number))
    (chars-of-base (vl-echarlist->chars base))
    (signedp (vl-signed-basep chars-of-base))
    (radix (vl-base-to-radix chars-of-base))
    ((mv ws2 remainder2)
     (vl-read-while-whitespace remainder2))
    ((mv edigits remainder2)
     (case radix
           (16 (vl-read-hex-value remainder2))
           (10 (vl-read-decimal-value remainder2))
           (8 (vl-read-octal-value remainder2))
           (otherwise (vl-read-binary-value remainder2))))
    (etext (append number ws base ws2 edigits))
    (normalized-edigits (vl-echarlist-kill-underscores edigits))
    (value (vl-echarlist-unsigned-value normalized-edigits radix))
    ((when value)
     (b*
      ((val-fix (mod value (expt 2 width)))
       (token (make-vl-inttoken :etext etext
                                :width width
                                :signedp signedp
                                :value val-fix
                                :bits nil
                                :wasunsized unsizedp
                                :breakp breakp))
       (warnings
        (if width-was-0
         (warn
          :type :vl-0-width-number-literal
          :msg
          "~l0: Number ~s1 has explicit width 0, which ~
                                is not allowed by the SystemVerilog standard. ~
                                Implementations usually interpret these as ~
                                unsized (that is, actually 32 bits wide)."
          :args (list (vl-echar->loc firstchar)
                      (vl-echarlist->string etext)))
         warnings))
       (warnings
        (cond
         ((not unsizedp)
          (if (eql value val-fix)
              warnings
           (warn
            :type :vl-warn-overflow
            :msg
            "~l0: the number ~s1 is not within the ~
                                     range [0, 2^~x2) indicated by its size, ~
                                     and is being truncated to ~x2 bits, ~
                                     yielding ~x2'd~x3 (hex: ~x2'h~s4)."
            :args (list (vl-echar->loc firstchar)
                        (vl-echarlist->string etext)
                        width val-fix
                        (str::nat-to-hex-string val-fix)))))
         ((< value (expt 2 31)) warnings)
         ((and signedp (< value (expt 2 32)))
          (warn
           :type :vl-warn-overflow
           :msg
           "~l0: the unsized, signed number ~s1 is in ~
                                   [2^31, 2^32).  It will be considered a ~
                                   negative number by 32-bit Verilog ~
                                   implementations, but positive by 64-bit ~
                                   tools.  You should add an explicit size."
           :args (list (vl-echar->loc firstchar)
                       (vl-echarlist->string number))))
         ((< value (expt 2 32)) warnings)
         (t
          (warn
           :type :vl-warn-overflow
           :msg
           "~l0: the unsized number ~s1 is over 2^32; ~
                                   we truncate it to 32'd~x2 (hex: 32'h~s3) ~
                                   to emulate a 32-bit Verilog ~
                                   implementation, but it will have a ~
                                   different value on 64-bit tools.  You ~
                                   should add an explicit size."
           :args (list (vl-echar->loc firstchar)
                       (vl-echarlist->string number)
                       val-fix
                       (str::nat-to-hex-string val-fix)))))))
      (mv token remainder2 warnings)))
    (digits (vl-echarlist->chars normalized-edigits))
    (bits (case radix
                (16 (vl-hex-digits-to-bitlist digits))
                (10 (vl-decimal-digits-to-bitlist digits))
                (8 (vl-octal-digits-to-bitlist digits))
                (otherwise (vl-binary-digits-to-bitlist digits))))
    ((unless bits)
     (mv (cw "Lexer error (~s0): invalid number: ~s1.~%"
             (vl-location-string (vl-echar->loc firstchar))
             (vl-echarlist->string etext))
         echars warnings))
    ((mv warnings bits)
     (vl-correct-bitlist (vl-echar->loc firstchar)
                         bits
                         (and (not width-was-0) value-of-number)
                         etext warnings))
    (token (make-vl-inttoken :etext etext
                             :width width
                             :signedp signedp
                             :value value
                             :bits bits
                             :wasunsized unsizedp
                             :breakp breakp)))
   (mv token remainder2 warnings))))

Theorem: vl-warninglist-p-of-vl-lex-integer.warnings

(defthm vl-warninglist-p-of-vl-lex-integer.warnings
  (b* (((mv ?token? ?remainder ?warnings)
        (vl-lex-integer echars breakp warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-token-p-of-vl-lex-integer

(defthm vl-token-p-of-vl-lex-integer
 (implies
  (and (force (vl-echarlist-p echars)) t)
  (equal
       (vl-token-p (mv-nth 0
                           (vl-lex-integer echars breakp warnings)))
       (if (mv-nth 0
                   (vl-lex-integer echars breakp warnings))
           t
         nil))))

Theorem: true-listp-of-vl-lex-integer

(defthm true-listp-of-vl-lex-integer
 (equal
      (true-listp (mv-nth 1
                          (vl-lex-integer echars breakp warnings)))
      (true-listp echars))
 :rule-classes
 ((:rewrite)
  (:type-prescription
     :corollary
     (implies
          (true-listp echars)
          (true-listp
               (mv-nth 1
                       (vl-lex-integer echars breakp warnings)))))))

Theorem: vl-echarlist-p-of-vl-lex-integer

(defthm vl-echarlist-p-of-vl-lex-integer
 (implies
  (force (vl-echarlist-p echars))
  (equal
   (vl-echarlist-p (mv-nth 1
                           (vl-lex-integer echars breakp warnings)))
   t)))

Theorem: append-of-vl-lex-integer

(defthm append-of-vl-lex-integer
 (implies
  (and (mv-nth 0
               (vl-lex-integer echars breakp warnings))
       (force (vl-echarlist-p echars))
       t)
  (equal
      (append (vl-token->etext
                   (mv-nth 0
                           (vl-lex-integer echars breakp warnings)))
              (mv-nth 1
                      (vl-lex-integer echars breakp warnings)))
      echars)))

Theorem: no-change-loser-of-vl-lex-integer

(defthm no-change-loser-of-vl-lex-integer
  (implies (not (mv-nth 0
                        (vl-lex-integer echars breakp warnings)))
           (equal (mv-nth 1
                          (vl-lex-integer echars breakp warnings))
                  echars)))

Theorem: acl2-count-of-vl-lex-integer-weak

(defthm acl2-count-of-vl-lex-integer-weak
  (<= (acl2-count (mv-nth 1
                          (vl-lex-integer echars breakp warnings)))
      (acl2-count echars))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-lex-integer-strong

(defthm acl2-count-of-vl-lex-integer-strong
 (implies
    (and (mv-nth 0
                 (vl-lex-integer echars breakp warnings))
         t)
    (< (acl2-count (mv-nth 1
                           (vl-lex-integer echars breakp warnings)))
       (acl2-count echars)))
 :rule-classes ((:rewrite) (:linear)))

Subtopics

Vl-lex-integer-token/remainder-thms: Token and remainder theorems for vl-lex-integer, automatically generated by def-token/remainder-thms.