4vec-operations
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.
Subtopics
- 4vec-bit?
- Bitwise multiple if-then-elses of 4vecs; doesn't unfloat
then/else values.
- 4vec-part-install
- Part install operation: replace width bits of in starting at
lsb with the least-significant bits of val.
- 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-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-===*
- 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-bit-extract
- Like logbit for 4vecs; the bit position may be a 4vec.
- 4vec-rev-blocks
- Similar to a streaming concatenation operation in SystemVerilog.
- 4vec-lsh
- Left ``arithmetic'' shift of 4vecs.
- 4vec-resor
- Bitwise wired OR resolution of two 4vecs.
- 4vec-resand
- Bitwise wired AND resolution of two 4vecs.
- 4vec-parity
- Reduction logical XOR (i.e., parity) of a 4vec.
- 4vec-plus
- Integer addition of two 4vecs.
- 4vec-<
- Integer less-than for 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-bit-index
- Like logbit for 4vecs; the bit position must be a natp.
- 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-zero-ext
- Like loghead for 4vecs; the width is also a 4vec.
- 4vec-part-select
- Part select operation: select width bits of in starting at lsb.
- 4vec-===
- Unsafe, Verilog-style ``case equality'' of 4vecs.
- 4vec-remainder
- Integer remainder as in rem for 4vecs.
- 4vec-reduction-or
- Reduction logical OR of a 4vec.
- 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-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-bitxor
- Bitwise logical XOR of 4vecs.
- 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-times
- Integer multiplication of 4vecs.
- 4vec-bitmux
- 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-bitand
- Bitwise logical AND of 4vecs.
- 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-bitor
- Bitwise logical OR of 4vecs.
- 4vec-shift-core
- 4vec-pow
- Power operator (** in SystemVerilog).
- 4vec-onset
- Identity, except Z bits become 0.
- 4vec-offset
- Negation, 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
- Converts 4vec-p into string of 0,1,x,z's msb-first
- 4vec-onehot0
- Count of 1 bits in a 4vec (X-monotonic).
- 4vec-1mask
- 4vec-p-to-stringp-aux
- 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.
- Unsigned-4vec-p
