• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
          • Svtv-data
          • Svtv-run
          • Defsvtv-phasewise
          • Defsvtv
          • Process.lisp
          • Svtv-doc
          • Defsvtv$
          • Svtv-debug-fsm
          • Svtv-versus-stv
          • Structure.lisp
          • Def-pipeline-thm
          • Svtv-debug
          • Expand.lisp
          • Def-cycle-thm
          • Defsvtv$-phasewise
          • Svtv-utilities
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • Moddb
        • Svex-compilation
        • Svmods
        • Svstmt
        • Sv-tutorial
        • Expressions
        • Symbolic-test-vector
        • Vl-to-svex
      • Fgl
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Testing-utilities
    • Math
  • Sv

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

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.

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. See svtv-data for versions of these utilities that can shorten the debug loop when using SVTVs defined with 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

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 stv-a and stv-b is equivalent to stv-c:

(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 :hyp and :g-bindings arguments to svdecomp-hints are for the GL phase. Usually some autohyps and autobindings from your STV are appropriate. :enable allows you to add rules to use in the initial rewriting phase before the meta rule is used. This can help on occasion when you want to use some particular function to (e.g.) construct the alist for some subsequent step or to extract values to compare.

More information about the decomposition strategy is in svex-decomp, or will be someday.

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.
Svtv-run
Run an SVTV and get the outputs.
Defsvtv-phasewise
Alternative format for creating an SVTV.
Defsvtv
Create an SVTV structure for some simulation pattern of a hardware design.
Process.lisp
Svtv-doc
Automatic documentation support for svex symbolic test vectors.
Defsvtv$
Create an SVTV, storing and possibly using intermediate results from the svtv-data stobj.
Svtv-debug-fsm
Dump a VCD waveform showing the internal signals of an svex STV.
Svtv-versus-stv
A note on naming conventions
Structure.lisp
Def-pipeline-thm
Prove that an SVTV pipeline is an unrolling of the FSM that it's based on
Svtv-debug
Dump a VCD waveform showing the internal signals of an svex STV.
Expand.lisp
Def-cycle-thm
Prove that an SVTV cycle FSM an unrolling of the phase FSM that it's based on
Defsvtv$-phasewise
Create an SVTV using the defsvtv-phasewise syntax, storing and possibly using intermediate results from the svtv-data stobj.
Svtv-utilities
Various utilities for interacting with SVTV structures.