|
|
|---|
|
|
|
|---|
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
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.
There are two utilities for defining svex-based S(V)TVs: the original defsvtv, and the newer defsvtv$, which uses the svtv-data stobj framework to keep track of logical relationships between the results of different steps in the process and support better debugging tools. These utilities both begin with SV modules as produced by the vl-to-svex tools, go through the steps described in svex-compilation to produce a finite state machine representation of the design, and then compose the FSM phases together to create the output expressions in terms of the input variables according to the I/O specification. Both use a similar timing diagram syntax for describing the I/O specification, and both support a variant defsvtv-phasewise, defsvtv$-phasewise that tend to make it easier to edit these I/O specifications.
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. See svtv-data for versions of these utilities that can shorten the debug loop when using SVTVs defined with defsvtv$.
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):
ERROR: some bits assumed to be Boolean were not.
If you see such an error, you should set
The book "svex/decomp.lisp" contains a proof strategy for proving that the
composition of two or more STV runs is equivalent to some other STV run. It
provides a computed hint that provides a good theory for rewriting such rules,
then a meta rule that can reverse the decomposition, and an invocation of GL to
finish off any mismatches due to svex simplification. Here is an example
showing that the composition of STVs
(defthm a-and-b-compose-to-c (implies (stv-c-autohyps) (b* ((c-out (stv-run (stv-c) (stv-c-autoins))) (a-ins (stv-a-autoins)) (a-out (stv-run (stv-a) a-ins)) ;; may be various ways of making the input to the 2nd phase (b-ins (stv-b-alist-autoins (append a-ins a-out))) (b-out (stv-run (stv-b) b-ins))) (and ;; may be various forms for the final equivalence (equal (extract-keys *my-keys* b-out) (extract-keys *my-keys* c-out)) (equal (cdr (assoc 'out b-out)) (cdr (assoc 'out c-out))) (equal b-out c-out)))) :hints ((sv::svdecomp-hints :hyp (stv-c-autohyps) :g-bindings (stv-c-autobinds) :enable (extract-keys-of-cons))))
The
More information about the decomposition strategy is in svex-decomp, or will be someday.