Symbolic-test-vectors
A concise way to describe, evaluate, and debug symbolic simulations
of E modules.
A symbolic test vector is a description of a multi-phase esim simulation. It lets you say how the state bits should be initialized,
how the inputs should be set as the simulation proceeds, and when you would
like the outputs and internal signals to be sampled.
As a user, the main steps for using symbolic test vectors are:
- Use defstv to introduce the STV you want to run. You basically
explain when you want to send into the module, and which outputs you want to
extract at what times.
- Use stv-run to run the STV on some particular inputs. This is
intended to be compatible with gl proofs, and can also be used in a
stand-alone way to get the outputs of the circuit.
- Alternately, use stv-debug to run the STV on particular inputs and
also produce a waveform that can be inspected in a waveform viewer. This is
intended for debugging only and cannot be embedded in proofs due to subtle
memoization issues.
This interface is hopefully sufficient for most users. But if you want to
understand more about how we process STVs, you can see stv-implementation-details.
Subtopics
- Defstv
- Introduce a symbolic test vector as a constant.
- Stv-compile
- Syntactically transform a symbolic test vector, readying it for
evaluation, debugging, etc.
- Symbolic-test-vector-format
- How to write a symbolic test vector.
- Stv-implementation-details
- Overview of the basic flow for processing and running STVs.
- Compiled-stv-p
- Compiled form of symbolic-test-vectors.
- Stv-run-for-all-dontcares
- Test that a given setting of the don't-care bits of an STV are indeed
don't-cares under the given input alist.
- Stv-run
- Evaluate a symbolic test vector at particular, concrete inputs.
- Stv-process
- Process a symbolic test vector and prepare it to be run.
- Stv-run-check-dontcares
- Test that a given setting of the don't-care bits of an STV are indeed
don't-cares under the given input alist.
- Symbolic-test-vector-composition
- Strategy for performing compositional proofs involving stv's
- Stv-expand
- Expand Verilog-style names throughout an STV into LSB-ordered ESIM
style paths.
- Stv-easy-bindings
- Generating G-bindings from an STV in a particular way.
- Stv-debug
- Evaluate a symbolic test vector at particular, concrete inputs, and
generate a waveform.
- Stv-run-squash-dontcares
- Evaluate a symbolic test vector at particular, concrete inputs, and set all inputs and initial states that aren't bound to false.
- Stvdata-p
- Temporary internal representation of STV lines during compilation.
- Stv-doc
- Automatic documentation support for symbolic test vectors.
- Stv2c
- Naive compiler from symbolic test vectors into C++ code.
- Stv-widen
- Widen the input/output/internals lines so that they all agree on how
many phases there are.
- Stv-out->width
- Get the bit-length for a particular output simulation variable.
- Stv-in->width
- Get the bit-length for a particular input simulation variable.
- Stv-number-of-phases
- Maximum length of any line of an STV (i.e., how many phases we are
going to simulate.
- Stv->outs
- Get a list of an STV's output simulation variables.
- Stv->ins
- Get a list of an STV's input simulation variables.
- Stv-suffix-signals
- Convert a list of atoms into a list of symbols with some suffix.
- Stv->vars
- Get a list of an STV's simulation variables (both inputs and
outputs).
