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.
An svtv-data stobj holds an SV design and several other pieces of data, such
as finite-state machine and symbolic pipeline objects, tied to that design.
These data objects are constrained by the abstract stobj invariant to have
certain relationships among each other and to the design. For example, one
invariant states that if the phase-fsm-validp field is true, then the
phase-fsm object is equivalent to the composition of the normalized signal
assignments from the flatten field, which in turn (if flatten-validp
is true) is a certain function of the original design. Similarly, the
cycle-fsm and pipeline fields are known to equivalent to certain
functions of the other fields. These relations are designed so that, for
example, a pipeline can be used to prove a lemma about a cycle FSM to aid in a
larger proof.
Beta Warning
This is relatively new and the structure/interface of the stobj may still
change in backward-incompatible ways. Howeer, at least the high-level tools
defsvtv$ and defcycle should retain their same interfaces.
Steps
The stobj contains data members that trace the following steps:
- The initial SV design is flattened, producing the flatten
field, a product of type flatten-res containing signal assignments, fixup
assignments, constraints, and a variable declaration map.
- The flattened design is normalized, producing the flatnorm
field, a product of type flatnorm-res containing finalized signal
assignments and constraints and a signal delay map.
- The flattened, normalized design is composed into a finite state machine
representation and stored in the phase-fsm field. This contains the
nextstate functions and the values for each signal in terms of previous states
and primary input.
- The user may attach names to certain signals, which are processed into a
namemap.
- The user may define a cycle as a composition of one or
more (usually two) phases of the phase FSM into a new FSM.
- The user may define a pipeline as a run of several cycles of the
cycle FSM in which certain inputs are given symbolic or concrete values at
particular times and certain outputs are read at particular times.
High-level tools
defsvtv$ provides a drop-in replacement for the old defsvtv and
defsvtv-phasewise utilities. However, it drops support for the
:state-machine, :keep-final-states, and :keep-all-states options
because these are geared toward using a pipeline-style SVTV as a cycle FSM,
which is now deprecated since we have such FSMs as separate structures. The
primary function for running concrete simulations of an SVTV and reasoning
about SVTVs is still svtv-run.
defcycle produces a cycle FSM from a design, given a name mapping and
phase specification. This is intended to replace the use of defsvtv with
the :state-machine option.
A nice thing about these two tools is that they don't need to repeat work
whose results have already been stored in the svtv-data stobj. For example, to
create two SVTV objects representing pipelines built on the same module with
the same clock cycle phases, only the pipeline composition needs to be
repeated, not the flattening, phase-FSM composition, or clock-cycle
composition.
Lower-level tools
The fields of the svtv-data stobj may be updated directly, but there
are stringent guard requirements to prevent the invariants from being broken.
Because these guard obligations can be somewhat baroque, we define several
helper utilities that are lower level than defsvtv$ and defcycle
but with easier guard requirements than the core updaters. To ease these guard
requirements, these functions invalidate any fields that might violate
invariants.
svtv-data-set-design initializes the design of the svtv-data
object to the given design. If this differs from the current design, it
invalidates the flatten and namemap fields.
svtv-data-maybe-compute-flatten computes the flatten field from
the current design, unless that field is already valid. It invalidates
all the other derived fields since they all depend on the flatten field.
svtv-data-maybe-compute-flatnorm computes the flatnorm field,
requiring that flatten is valid.
svtv-data-maybe-compute-namemap computes the namemap from the given
user namemap, requiring that flatten is valid and invalidating the
pipeline since it is derived from the namemap.
svtv-data-maybe-compute-phase-fsm computes the phase-fsm field,
requiring that flatnorm is valid. It invalidates the cycle-fsm.
svtv-data-maybe-compute-cycle-fsm computes the cycle-fsm field
given a list of phase specifications, requiring that the phase-fsm is
valid. It invalidates the pipeline.
svtv-data-maybe-compute-pipeline computes the pipeline given a
pipeline-setup object. It requires that the phase-fsm and
cycle-fsm fields are valid.
The following functions apply SVEX rewriting to various fields:
- svtv-data-rewrite-phase-fsm
- svtv-data-rewrite-cycle-fsm
- svtv-data-rewrite-pipeline
Export and Import
The svtv-data stobj is not saved by certify-book. If you want to create an
svtv-data object in one book and include it elsewhere, we provide the utility
def-svtv-data-export/import. This saves (almost all) the current contents
of the svtv-data stobj (or some congruent stobj) as a constant function, with
theorems stating that this function satisfies the svtv-data invariant. It also
produces a function which imports that object back into an svtv-data object,
recomputing the parts (the moddb and aliases sub-stobjs) that
couldn't be saved.
Debugging and VCD dumping
Various utilities are provided for dumping VCD files showing runs of the
design. There are three families of such utilities:
- Debug functions dump a VCD waveform file for a given concrete simulation
- Chase functions enter a read-eval-print loop with commands to navigate through the drivers of signals under a given concrete simulation in order to trace root causes of a signal's value
- Run functions run a concrete simulation and returns the values of certain signals at certain times.
We'll describe the functions of the debug family. The chase and
run families have basically analogous functions, which we list after that.
- svtv-debug$ takes an SVTV object created by defsvtv$, recreates
the svtv-data stobj for that SVTV to the extent necessary up to the phase-fsm
stage, and dumps a VCD showing the run of the pipeline given the assignments
for the pipeline variables.
- svtv-data-debug-defsvtv$ takes a defsvtv$ form and dumps a VCD
given the assignments for the pipeline variables. An advantage of this utility
is that you don't need to run the full defsvtv$ (in particular, compose
the pipeline) first, cutting down on a sometimes significant part of the debug
loop when fine-tuning the signals to set and extract.
- svtv-data-debug-pipeline operates on an existing svtv-data stobj,
dumping a VCD to a file given assignments for the pipeline variable.
- svtv-data-debug-cycle-fsm dumps a VCD showing a cycle FSM run, given
an initial state environment and a list of input environments for the cycles to
be run.
- svtv-data-debug-phase-fsm dumps a VCD showing a phase FSM run, given
an initial state environment and a list of input environments for the phases to
be run.
The corresponding functions for the chase family:
- svtv-chase$
- svtv-data-chase-defsvtv$
- svtv-data-chase-pipeline
- svtv-data-chase-cycle-fsm
- svtv-data-chase-phase-fsm
And the corresponding functions for the run family:
- svtv-run$ (though svtv-run is almost always a better choice)
- svtv-data-run-defsvtv$
- svtv-data-run-pipeline
- svtv-data-run-cycle-fsm
- svtv-data-run-phase-fsm
Note: These functions don't replace svtv-run for reasoning purposes;
svtv-run$ should always produce the same result as svtv-run but is in
program mode and is likely slower.
Subtopics
- Defsvtv$
- Create an SVTV structure for some simulation pattern of a hardware design.
- Defcycle
- Create a FSM from a design and a clock cycle specification, along with a signal name list.
- Def-pipeline-thm
- Prove that an SVTV pipeline is an unrolling of the FSM that it's based on
- Def-svtv-data-export
- Copy the contents of a svtv-data stobj into a constant.
- Def-svtv-data-import
- Define a function that imports a particular svtv data object (such as created by def-svtv-data-export) into a svtv-data stobj.
- Svtv-name-lhs-map
- Mapping from user-provided names (generally symbols) to normalized internal names.
- Def-cycle-thm
- Prove that an SVTV cycle FSM an unrolling of the phase FSM that it's based on
- Def-svtv-data-export/import
- Combines def-svtv-data-export and def-svtv-data-import.
- Defsvtv$-phasewise
- (Deprecated) Create an SVTV using the defsvtv-phasewise syntax, storing and
possibly using intermediate results from the svtv-data stobj.
