|
|
|---|
|
|
|
|---|
Overview of the basic flow for processing and running STVs.
Here is a high-level overview of how we compile, process, and evaluate STVs. A picture of the flow is:
User-Level STV ESIM Module
| |
| ,-----------------------+
| | |
v v v
Compiled STV Fully General Sexprs
| |
| ,-----------------------'
| |
v v
Processed STV Simulation Input Alist
| |
| ,---------------------'
| |
v v
stv-run/debug
| |
| +-------> Waveform (VCD Dump)
| |
v v
Simulation Output Alist
Here, the user provides:
As a first step, we preprocess and compile the STV; see stv-compile. This step involves basic sanity checking and the computation of mappings that record what inputs to provide to ESIM at each step of the simulation, what outputs to extract after each phase, and how to translate between Esim bits and the user-level input and output alists. This compilation should generally be quite fast (it's mostly involving the STV instead of the module), and it only needs to be done once per STV.
Separately, we do a fully general symbolic simulation of the esim module for as many phases as are necessary to evaluate this STV; see stv-fully-general-simulation-run. Symbolically simulating a module for many steps can be very expensive. On the other hand, this cost can be shared across all STVs that target the same module, and it can even be at least partly shared when the STV's require different numbers of phases.
Next, we create a Processed STV; see stv-process. This involves pulling out the fully-general expressions for the signals we actually care about (cheap) and specializing these expressions using the bindings from the compiled STV (slightly expensive; basically 4v-sexpr-restrict-with-rw for each signal in the user-outs).
We generally expect the Processed STV to be saved as a constant, via defconsts since our use of defattach in esim prevents the sound use of defconst. This will allow the same STV to be saved in a book and reused for all evaluations of the STV. In other words, we really expect to only have to pay the price of processing an STV once.
Once the STV has been processed, we can run it with concrete values for the input simulation variables; see stv-run. To do this, we basically need to (1) translate the input numbers into bit-level bindings, (2) use 4v-sexpr-eval to reduce the sexprs that are found in the Processed STV with the bindings for their inputs, and (3) translate back from the resulting output-bit bindings into numbers (or Xes) for the output alist. This is about as cheap as we know how to make it.
Of course, we may alternately want to run the STV and generate a waveform for debugging; see stv-debug. But now there's a slight problem. When we compute the fully general sexprs, we omit internal signals because it gives us a speed boost. So, the processed STV doesn't contain the information we would need to generate a waveform.
Well, basically we just do a new esim simulation that does include the internal variables, and then run through the rest of the process again. We memoize things so that even though your first call of stv-debug is expensive, subsequent calls will not need to redo the simulation or specialization steps.