		Search-engine friendly clone of the ACL2 documentation.

Lex-numbers

Vl-correct-bitlist

Extend (or truncate) a bit-list to match the size specifier for an integer token.

Signature
(vl-correct-bitlist loc bits width etext warnings) → (mv warnings new-bits)
Arguments: loc — Context for any new warnings.
Guard (vl-location-p loc).; bits — The actual bits for this number. This list of bits may be shorter or longer than width, which is the size specified for this integer or is nil if no size was specified.
Guard (vl-bitlist-p bits).; width — The desired width specified for this number. For instance, this would be 3 for 3'bx. Note that we emulate a 32-bit Verilog implementation and treat unsized numbers as having width 32.
Guard (maybe-posp width).; etext — Actual text for this number, for better warnings.
Guard (vl-echarlist-p etext).; warnings — An ordinary warnings accumulator.
Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; new-bits — Type (vl-bitlist-p new-bits), given (force (vl-bitlist-p bits)).

Our goal is to produce a new list of bits that has exactly the desired width, by truncating or extending bits as necessary.

The rules for how to do this are given in Section 3.5.1 of the Verilog-2005 standard, or Section 5.7.1 of the SystemVerilog-2012 standard. Both standards agree about the details. Essentially:

If the actual list of bits is longer than width, we are to truncate it from the left, keeping the least significant width-many bits. We produce a truncation warning in this case.
If the actual list of bits is shorter than width, we are usually supposed to zero-extend it. However, when the most significant bit is X or Z, we are instead supposed to X-extend or Z-extend, respectively.

The specification notes that in the 1995 Verilog standard, an unsized constant whose leading bit is X or Z is only X/Z extended to 32 bits. We therefore detect and warn about this very unusual case.

Definitions and Theorems

Function: vl-correct-bitlist

(defun vl-correct-bitlist (loc bits width etext warnings)
 (declare (xargs :guard (and (vl-location-p loc)
                             (vl-bitlist-p bits)
                             (maybe-posp width)
                             (vl-echarlist-p etext)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-correct-bitlist))
  (declare (ignorable __function__))
  (b*
   ((actual-len (len bits))
    (desired-len (if width (lnfix width) 32))
    ((when (eql desired-len actual-len))
     (mv (ok) bits))
    ((when (eql actual-len 0))
     (raise "Programming error: expected at least one bit.")
     (mv (ok)
         (replicate desired-len :vl-0val)))
    ((when (< actual-len desired-len))
     (b*
      ((pad-bit (case (car bits)
                      (:vl-zval :vl-zval)
                      (:vl-xval :vl-xval)
                      (otherwise :vl-0val)))
       (warnings
        (if
         (and (not width)
              (or (eq pad-bit :vl-xval)
                  (eq pad-bit :vl-zval)))
         (warn
          :type :vl-warn-incompatible
          :msg
          "~l0: unsized numbers with leading X or Z bit ~
                              have a different interpretation in Verilog-1995 ~
                              than in Verilog-2001 and beyond.  You should ~
                              put an explicit size on this number: ~s1."
          :args (list loc (vl-echarlist->string etext)))
         (ok)))
       (pad (replicate (- desired-len actual-len)
                       pad-bit))
       (bits-prime (append pad bits)))
      (mv (ok) bits-prime)))
    (bits-prime (rest-n (- actual-len desired-len)
                        bits))
    (warnings
     (if (all-equalp :vl-xval bits)
         (ok)
      (warn
       :type :vl-warn-overflow
       :msg
       (cat
        "~l0: implicitly truncating ~s1 from ~x2 to ~x3 bits."
        (if
         (not width)
         " Note that we are emulating a 32-bit Verilog ~
                                implementation, but a 64-bit simulator would ~
                                get a different value here.  You should add ~
                                an explicit size specifier."
         ""))
       :args (list loc (vl-echarlist->string etext)
                   actual-len desired-len)))))
   (mv (ok) bits-prime))))

Theorem: vl-warninglist-p-of-vl-correct-bitlist.warnings

(defthm vl-warninglist-p-of-vl-correct-bitlist.warnings
  (b* (((mv ?warnings ?new-bits)
        (vl-correct-bitlist loc bits width etext warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-bitlist-p-of-vl-correct-bitlist.new-bits

(defthm vl-bitlist-p-of-vl-correct-bitlist.new-bits
 (implies (force (vl-bitlist-p bits))
          (b* (((mv ?warnings ?new-bits)
                (vl-correct-bitlist loc bits width etext warnings)))
            (vl-bitlist-p new-bits)))
 :rule-classes :rewrite)

Theorem: len-of-vl-correct-bitlist

(defthm len-of-vl-correct-bitlist
 (equal
   (len (mv-nth 1
                (vl-correct-bitlist loc bits width etext warnings)))
   (if width (nfix width) 32)))