Extend (or truncate) a bit-list to match the size specifier for an integer token.
(vl-correct-bitlist loc bits width etext warnings) → (mv warnings new-bits)
Our goal is to produce a new list of bits that has exactly the
desired width, by truncating or extending
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:
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.
Function:
(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:
(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:
(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:
(defthm len-of-vl-correct-bitlist (equal (len (mv-nth 1 (vl-correct-bitlist loc bits width etext warnings))) (if width (nfix width) 32)))