The **S**ymbolic **V**ector **Ex**pression language (SVEX)
forms the core of SV. It includes an S-expression language for certain
pre-defined hardware functions, an interpreter for evaluating these expressions
on four-valued integers, and related tools.

- Rewriting
- We implement a lightweight, mostly unconditional rewriter for simplifying svex expressions in provably sound ways. This is typically used to reduce expressions before processing them with bit-blasting or other reasoning tools.
- Svex
- Our core expression data type. A
**S**ymbolic**V**ector**Ex**pression may be either a constant 4vec, avariable, or a function applied to subexpressions. - Bit-blasting
- We implement an efficient translation from svex expressions into ACL2::aigs, to support symbolic simulation with gl.
- Functions
- Our expressions may involve the application of a fixed set of known functions. There are functions available for modeling many bit-vector operations like bitwise and, plus, less-than, and other kinds of hardware operations like resolving multiple drivers, etc.
- 4vmask
- Bitmasks indicating the relevant bits of SVEX expressions.
- Why-infinite-width
- Notes about our use of infinite-width vectors as the basis for our expression language.
- Svex-vars
- Collect all of the variables from an svex.
- Evaluation
- The formal semantics of our expressions are defined by svex-eval, a simple McCarthy-style evaluator for interpreting an svex
under an
environment that gives values to its variables. - Values
- 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).