Stvs-and-testing
Defining a simulation pattern (STV) and using it to run tests.
Part of the sv-tutorial. Previous section: translating-verilog-to-svex.
Defining a simulation pattern
To run a test of our SVEX design,
we'll first write a form that describes how to stimulate the module and grab
its output. Looking at the ALU design, we have inputs coming into flip-flops.
The outputs of these flops are combined with the opcode input and used to
compute ans. This goes to another flop, the result of which is output.
So we need to provide the a and b inputs one cycle, opcode the
next, and read the output the cycle after that. The following form defines a
symbolic-test-vector that describes this simulation pattern:
(defsvtv$ alu-test-vector
:mod *alu-svex-design*
:parents (stvs-and-testing)
:short "A simple test of the alu16 module."
:phases ((:label dat
:inputs (("clk" 0 :toggle t)
("abus" a)
("bbus" b)))
(:label op
:delay 2
:inputs (("opcode" op)))
(:label out
:delay 2
:outputs (("out" res)))))
The most important field here is :phases, which says what inputs to
provide when and what outputs to read when. Arguments :parents,
:short, and :long (not provided here) are just for documentation.
You can see the documentation generated for this SVTV here.
Each entry in :phases says what should happen in a particular
time (phase) in the simulation. The first entry says that the "clk"
signal will initially be set to 0, but will toggle every time step.
It also says that the "abus" and "bbus" inputs should be set to
symbolic variables a and b at that time. That phase is also
labeled dat for documentation purposes.
The next entry in the phases is labeled op. It has a
:delay argument, which says how many time steps after the
previous entry the current entry should happen; the default delay is 1
and the delay must be positive. In this design everything of
importance happens on the clock-low phase of a clock cycle, which is
standard for designs that use positive edge-triggered flip-flops. So
the delay on each phase after the first is 2 because on the skipped
phases the clock is high and nothing much happens. In this phase
another input signal, "opcode", is set to another symbolic variable,
op.
Finally, in the third entry, labelled out, we read an output
signal "out" into a symbolic variable called res. Again, this
happens 2 phases after the last one, so on the next clock-low
phase.
The main effect of this defsvtv$ form is to create a
constant (accessed via a 0-ary function, (alu-test-vector) that
encapsulates the given simulation pattern in a set of svex
expressions, one for each output variable, expressed in terms of the
input variables. So the resulting (alu-test-vector) from the
defsvtv$ above contains an svex expression for res as a
combinational function in terms of a, b, and op. You
can examine this function by looking at the outexprs field of the
SVTV structure:
(svtv->outexprs (alu-test-vector))
Warning: This prints a lot of output -- around 11,000 lines. We
get a somewhat nicer result if we apply some rewriting before
displaying it:
(svex-alist-rewrite-fixpoint (svtv->outexprs (alu-test-vector)))
This is small enough to fit on two screens, and its meaning can be teased
out with some patience and reference to the svex functions.
Running tests using the simulation pattern
The basic way to run tests using the simulation pattern we've defined is
with svtv-run:
(svtv-run (alu-test-vector)
(cons (cons 'op *op-plus*)
'((a . 5) (b . 3))))
This takes as input an alist binding the STV input variables to integers.
Note that we don't have to do anything for the clock; its behavior was defined
by the defsvtv$ form, and it has no input variable. The output from
svtv-run is just another alist binding the output variable(s) to their
values -- here, our ALU has added 3 and 5 and returned 8.
Sometimes you may need to drive a wire to X, Z, or some combination of X/Z
with good Boolean values. The biggest difference in usage between svex's STV
functions and esim's is the notation used for this. Svex constants, including
those in defsvtv$ forms and in the inputs and outputs of svtv-run, are
always expressed as 4vec objects. Essentially, if your input or output
value is an all-Boolean vector, then you can just represent it as a single
integer. If not, it is then a pair of integers; see 4vec for more
details. Examples:
(svtv-run (alu-test-vector)
(cons (cons 'op *op-plus*)
(cons (cons 'a (4vec-x)) '((b . 3)))))
(svtv-run (alu-test-vector)
(cons (cons 'op *op-bitand*)
(cons (cons 'a (4vec 64672 3322))
(cons (cons 'b 65535) 'nil))))
When we do an svtv-run, we are essentially applying svex-eval to
interpret the output expressions examined above.
Viewing Simulation Waveforms
To debug these simulations in more depth, we can use svtv-debug$, which
produces a VCD waveform that can be examined in a waveform viewer such as
gtkwave:
(svtv-debug$ (alu-test-vector)
(cons (cons 'op *op-mult*)
'((a . 5) (b . 3)))
:filename "alu-min-debug.vcd")
To continue, next see proofs-with-stvs.
Subtopics
- Alu-test-vector
- A simple test of the alu16 module.
