Expressions
The Symbolic Vector Expression 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.
Subtopics
- 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 Symbolic Vector
Expression may be either a constant 4vec, a variable, 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).
