3vec
A 3vec is a 4vec that has no Z bits.
In hardware modeling, Z bits (floating/undriven wires) are:
- relatively rare—for instance, an AND gate will never produce a Z
value.
- often indistinguishable from X—for instance, if we give an undriven
input to an OR gate, the hardware may interpret it as either a 0 or as a 1, so
we may as well supplied an X instead.
In most of our 4vec-operations, we account for the second property by
first ``unfloating'' our inputs, e.g., with 3vec-fix. But since Z
values are relatively rare in the first place, this unfloating is often
unnecessary. That is, in a circuit like:
(OR A (AND B C))
we can tell, statically, that we don't need to unfloat the result of the
(AND B C) when computing the OR, because the AND can never produce a Z
value anyway. This turns out to be a useful optimization during
bit-blasting.
Subtopics
- 3vec-fix
- Coerces an arbitrary 4vec to a 3vec by ``unfloating''
it, i.e., by turning any Zs into Xes.
- 3vec-equiv
- Equivalence up to 3vec-fix.
- 3vec-p!
- Recognizer for 3vec (without a 4vec-p guard).
- 3vec-p
- Recognizer for 3vecs (with a 4vec-p guard).
- 3vec-fix-fast
- Logically just 3vec-fix, but guarded with 3vec-p so
that in the execution this is just the identity.
