# 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