Svex-stvs
SVEX Symbolic Test Vectors
Historically, Symbolic Test Vectors or STVs were
developed to aid checking of pipeline properties in the VL2014/ESIM hardware
verification framework -- see ACL2::symbolic-test-vectors. The VL/SV
framework replicates and extends that functionality, of which we give an
overview here. For the implementation in the SV framework, we usually refer to
them as SVTVs, with the extra V distinguishing them from ESIM
STVs.
The SV tutorial gives a step by step
overview of how to run tests and prove properties about hardware modules using
the VL/SV/SVTV framework. Here we mainly summarize what SVTVs are for and link
to further documentation.
Concept
A symbolic test vector is a description of a multiphase simulation of a
hardware design, usually to show some particular functionality like the results
of running one fixed-latency instruction on an ALU. Usually in such a
simulation we want to set some inputs (or override some internal signals) to
constant values or variables at certain times, and extract the values (given
those inputs/overrides) of some outputs or internal signals at certain times.
The result of defining a symbolic test vector is an expression (svex)
for each output in terms of the input variables.
Defining an SVTV
The recommended utility for defining svex-based S(V)TVs is defsvtv$.
Previous versions these, defsvtv and defsvtv-phasewise are deprecated
since defsvtv$ supports better debugging tools, has a more coherent
logical story, and support better methods for decomposition. This takes an SV
hierarchical design as produced by the vl-to-svex tools, goes through
the steps described in svex-compilation to produce a finite state
machine representation of the design, and then composes the FSM phases together
to create the output expressions in terms of the input variables according to
the I/O specification.
Testing, Proof, and Debugging
Once an SVTV is defined, the function svtv-run can be used to run
tests on it, and is also the usual target for proofs about it. There are also
some useful debugging utilities: svtv-debug$ for dumping waveforms and
svtv-chase$ for chasing down the root causes of signal values.
When working on defining an SVTV, sometimes one goes through many iterations
before all the signal settings are right. A few utilities support debugging
concrete runs of SVTVs without first performing all the computation necessary
to define them. See svtv-debug-defsvtv$, svtv-chase-defsvtv$, and svtv-run-defsvtv$.
Symbolic Simulation
Svex STVs support symbolic simulation via the GL or FGL packages. First, the
formulas are expressed as AIGs and then these AIGs are composed with the
symbolic representations of the inputs. This is implemented in the book
"svex/symbolic.lisp". Svtv-run has an optional keyword argument that
can have an impact on symbolic execution (but doesn't mean anything logically):
:boolvars is T by default, and in this case the symbolic execution assumes
that all your input vectors are syntactically obviously Boolean-valued. This
helps symbolic execution speed, but can cause an error like:
ERROR: some bits assumed to be Boolean were not.
If you see such an error, you should set :boolvars nil.
Decomposition Proofs
See svex-decomposition-methodology and in particular def-svtv-generalized-thm for the recommended method for doing proofs by
decomposition on SVTVs.
Subtopics
- Svtv-data
- A stobj encapsulating an SVTV and the steps used in creating it, from
the initial SV design to (potentially) a pipelined symbolic run.
- Defsvtv$
- Create an SVTV structure for some simulation pattern of a hardware design.
- Svtv-run
- Run an SVTV and get the outputs.
- Defsvtv-phasewise
- (Deprecated) Alternative format for creating an SVTV.
- Svtv-spec
- A data object representing a run of an FSM, similar to an SVTV but
without computing the unrolling of the FSM.
- Svtv
- A shorter name for svex-stvs, i.e. SVEX Symbolic Test Vectors.
- Defsvtv
- (Deprecated) Create an SVTV structure for some simulation pattern of a hardware design.
- Process.lisp
- Svtv-doc
- Automatic documentation support for svex symbolic test vectors.
- Svtv-chase$
- Diagnose hardware or stimulus bugs by studying an SVTV run in a special-purpose
read-eval-print loop.
- Svtv-versus-stv
- A note on naming conventions
- Svtv-debug-fsm
- Dump a VCD waveform showing the internal signals of an svex STV.
- Structure.lisp
- Svtv-debug
- (Deprecated) Dump a VCD waveform showing the internal signals of an svex STV.
- Def-pipeline-thm
- Prove that an SVTV pipeline is an unrolling of the FSM that it's based on
- Expand.lisp
- Def-cycle-thm
- Prove that an SVTV cycle FSM an unrolling of the phase FSM that it's based on
- Svtv-utilities
- Various utilities for interacting with SVTV structures.
- Svtv-debug$
- Dump a VCD waveform showing the internal signals of an SVTV.
- Defsvtv$-phasewise
- (Deprecated) Create an SVTV using the defsvtv-phasewise syntax, storing and
possibly using intermediate results from the svtv-data stobj.
