The fundamental 4-valued vector representation used throughout SV expressions.
In hardware description languages like Verilog and SystemVerilog, each bit can typically take one of four values, named 1, 0, X, or Z. For some background see for instance the 4v library and in particular ACL2::why-4v-logic.
A 4vec represents a ``infinite width'' vector of 4-valued bits, i.e., each bit of a 4vec can be either 1, 0, X, or Z. 4vecs are fundamental to the sv expression representation: the variables in each expression are 4vec-valued, and each expression produces a result that is a 4vec.
The concrete representation of a 4vec is either:
In the latter case, the value of each 4-valued bit is determined by the corresponding bits in the two integers:
|Representation||Meaning (LSB first)|
|6||0,1,1,0,0,0,...infinitely many 0s...|
|-13||1,1,0,0,1,1,...infinitely many 1s...|
|(6 . -13)||Z,1,X,0,Z,Z,...infinitely many Zs...|
A 4vec should generally be honsed if it is going to be used in an expression, but it is better to avoid the expense of honsing ephemeral 4vecs, e.g., those that arise during evaluation. Accordingly we provide both make-4vec and make-honsed-4vec.
We provide a
(b* (((4vec x))) == (list :lower (4vec->lower x) (list :lower x.lower :upper (4vec->upper x)) :upper x.upper))