Core operations on 4vecs.

We now introduce many operations on 4vecs. These operations are generally intended to support the modeling of Verilog and SystemVerilog expressions. For instance, our 4vec-plus operation agrees with the Verilog notion of plus: if there are any X or Z bits in either input, it ``conservatively'' returns all Xes. Most of these operations have corresponding svex functions and can hence be used in expressions.

Many of these operations have similarities with the ACL2::4v-operations which were used in esim. But SV expressions are vectors instead of single bits, so there are many 4vec operations with no 4v equivalents (e.g., plus, times, etc.). Historically these operations were bit-blasted using the vl2014::occform transformation, but in svex they are primitives with well-defined semantics.

__Boolean Convention__. Most 4vec operations take and return 4vec
objects—even comparisons, reductions, etc., which you might instead
expect to produce a Boolean result. In these cases, we typically arrange so
that ``true'' is indicated by the all-1s vector (i.e., -1), ``false'' is
indicated by the all-0s vector (i.e., 0), and undetermined values are indicated
by the all-Xes vector. This is sometimes convenient in that it avoids needing
to explicitly replicate/extend comparison results.

It is critical that these functions support efficient symbolic simulation with gl. However, the logical definitions of these functions are typically not relevant to this, because we use a custom translation from expressions into ACL2::aigs; see bit-blasting for details.

- 4vec-bit?
- Bitwise multiple if-then-elses of 4vecs; doesn't unfloat then/else values.
- 4vec-part-install
- Part install operation: replace
width bits ofin starting atlsb with the least-significant bits ofval . - 4vec-bit?!
- Bitwise multiple if-then-elses of 4vecs; doesn't unfloat then/else values; uses else branch bits for any test bits not equal to 1 (non-monotonic semantics in this respect).
- 4vec-concat
- Like logapp for 4vecs; the width is also a 4vec.
- 4vec-?
- Atomic if-then-else of 4vecs; doesn't unfloat then/else values.
- 4vec-rsh
- Right ``arithmetic'' shift of 4vecs.
- 4vec-===*
- Approximation of Verilog-style ``case equality'' of 4vecs that is X-monotonic when one argument is constant
- 4vec-reduction-and
- Reduction logical AND of a 4vec.
- 4vec-rev-blocks
- Similar to a streaming concatenation operation in SystemVerilog.
- 4vec-bit-extract
- Like logbit for 4vecs; the bit position may be a 4vec.
- 4vec-resand
- Bitwise wired AND resolution of two 4vecs.
- 4vec-lsh
- Left ``arithmetic'' shift of 4vecs.
- 4vec-resor
- Bitwise wired OR resolution of two 4vecs.
- 4vec-parity
- Reduction logical XOR (i.e., parity) of a 4vec.
- 4vec-<
- Integer less-than for 4vecs.
- 4vec-plus
- Integer addition of two 4vecs.
- 4vec-minus
- Integer subtraction of two 4vecs.
- 4vec-res
- Bitwise wire resolution of two 4vecs.
- 4vec-override
- Resolution for when one signal is stronger than the other.
- 4vec-?!
- If-then-elses of 4vecs following the SystemVerilog semantics for procedural conditional branches, i.e. if the test has any bit that is exactly 1 (not 0, Z, or X), we choose the then branch, else the else branch. (Non-monotonic semantics).
- 4vec-bit-index
- Like logbit for 4vecs; the bit position must be a natp.
- 4vec-zero-ext
- Like loghead for 4vecs; the width is also a 4vec.
- 4vec-part-select
- Part select operation: select
width bits ofin starting atlsb . - 4vec-===
- Unsafe, Verilog-style ``case equality'' of 4vecs.
- 4vec-idx->4v
- Like logbit for 4vecs, for fixed indices, producing an 4v-style ACL2::4vp.
- 4vec-==
- Bitwise equality of 4vecs.
- 4vec-sign-ext
- Like logext for 4vecs; the width is also a 4vec.
- 4vec-remainder
- Integer remainder as in rem for 4vecs.
- 4vec-reduction-or
- Reduction logical OR of a 4vec.
- 4vec-quotient
- Integer division as in truncate for 4vecs.
- 4vec-?*
- Atomic if-then-else of 4vecs. Has the property that when branches are equal, the result is equal to the branch, regardless of the test.
- 4vec-wildeq
- True if for every pair of corresponding bits of a and b, either they are equal or the bit from b is X or Z.
- 4vec-bitxor
- Bitwise logical XOR of 4vecs.
- 4vec-times
- Integer multiplication of 4vecs.
- 4vec-symwildeq
- Symmetric wildcard equality: true if for every pair of corresponding bits of a and b, either they are equal or the bit from either a or b is Z.
- 4vec-wildeq-safe
- True if for every pair of corresponding bits of a and b, either they are equal or the bit from b is Z.
- 4vec-bitand
- Bitwise logical AND of 4vecs.
- 4vec-shift-core
- 4vec-pow
- Power operator (** in SystemVerilog).
- 4vec-bitor
- Bitwise logical OR of 4vecs.
- 4vec-offset
- Negation, except Z bits become 0.
- 4vec-onset
- Identity, except Z bits become 0.
- 4vec-xdet
- Identity function for 2vecs, or all Xes when there are any X or Z bits.
- 4vec-uminus
- Integer negation of a 4vec.
- 4vec-clog2
- Ceiling of the log2 of a, or X if any non-2-valued bits. Must be truncated to its width (nonnegative).
- 4vec-bitnot
- Bitwise logical NOT of a 4vec.
- 4vec-onehot
- Count of 1 bits in a 4vec (X-monotonic).
- 4vec-countones
- Count of 1 bits in a 4vec (X-monotonic).
- 4veclist-p-to-stringp
- Converts 4veclist-p into list of strings of 0,1,x,z's msb-first
- 4vec-p-to-stringp-aux
- 4vec-p-to-stringp
- Converts 4vec-p into string of 0,1,x,z's msb-first
- 4vec-onehot0
- Count of 1 bits in a 4vec (X-monotonic).
- 4v->4vec-bit
- Convert a 4v-style ACL2::4vp into an infinite width 4vec of that bit.
- 4v-to-characterp
- Bool->vec
- Convert an ACL2 booleanp into a 4vec according to the boolean-convention.