		Search-engine friendly clone of the ACL2 documentation.

Values

4vec

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:

an integer (for special cases where there are no X/Z bits), or
a pair of integers, say (upper . lower).

In the latter case, the value of each 4-valued bit is determined by the corresponding bits in the two integers:

If the corresponding bits are equal, the resulting bit is the shared value (1 or 0).
Otherwise, if the upper bit is 1 and the lower 0, then the resulting value is X.
Otherwise, the upper bit is 0 and the lower 1, then the resulting value is Z.

Examples:

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 4vec b* binder that allows you to access, e.g.,

(b* (((4vec x)))          ==   (list :lower (4vec->lower x)
  (list :lower x.lower               :upper (4vec->upper x))
        :upper x.upper))

Subtopics

4vec-operations: Core operations on 4vecs.
4vec-p: Recognizer for 4vecs.
S4vecs: Representation of 4vecs using sparseint rather than bignum elements.
4vec-examples: 4vec examples
Maybe-4vec: Option type; 4vec or nil.
4vec-equiv: Equivalence relation for 4vecs.
Make-4vec: Raw constructor for 4vecs, using cons.
4vec->upper: Raw accessor for the upper integer from a 4vec.
4vec->lower: Raw accessor for the lower integer from a 4vec.
4veclist: A list of 4vec-p objects.
4vec-fix: Fix an arbitrary object to a 4vec.
Make-honsed-4vec: Raw constructor for 4vecs, using hons.
4vec-index-p