Our expressions operate on four-valued bit vectors called 4vecs. There are also useful subsets of 4vecs, such as 3vecs (which have no Z bits) and 2vecs (which have no X or Z bits).
- The fundamental 4-valued vector representation used throughout SV
- Lattice relation (information order) on 4vec values.
- A 3vec is a 4vec that has no Z bits.
- A 2vec is a 4vec that has no X or Z bits.
- A 2vecx is a 4vec that is either a 2vec or is
- A 2vecnatx is a 4vec that is either a natural-valued
2vec or is all Xes.
- Infinite width vector, all Xes.
- Vector with a single X bit (lsb), upper bits all 0.
- Vector with a single Z bit (lsb), upper bits all 0.
- Infinite width vector, all Zs.