Symbolic-test-vector-format
How to write a symbolic test vector.
Example Test Vector
(
;; phases: 0 1 2 3 4 5 6 ...
;; ---------------------------------------------------------------------------
(:inputs ;; for supplying values to input wires
("clock" 0 ~)
("ibus[13:10]" #b101 #b101 _)
("ibus[9:0]" op op _)
("fwd" 16 16 _)
("a_bus" _ _ a1 a1 a2 a2 _)
("b_bus" _ _ b b b b _)
("reset" 0)
("fuse[0]" X))
(:outputs ;; for extracting values on output wires
("result_bus" _ _ _ _ _ res1 res2)
("result_bus[63:32]" _ _ _ _ _ res-hi1 res-hi2)
("result_bus[31:0]" _ _ _ _ _ res-lo1 res-lo2)
)
(:internals ;; for extracting values on internal wires
("queue0.mgr.fail" _ _ qf1 qf2 _))
;; advanced features:
(:overrides ;; for forcibly overriding values on wires
;; abstract away product wire, replacing it with variables
("foo.prod" _ _ prod _ _ _ _ )
;; force fast mode to true after phase 1, no matter what its real value is
("foo.fastmode" _ _ 1 1 1 1 1 ))
)
High-Level Overview
The :inputs section controls how the module's inputs will be set over
the course of the simulation. For the above vector,
- clock starts low and then toggles throughout the simulation,
- ibus[13:10] is held to 5 (#b101) during the first full cycle, but is
not constrained afterward,
- ibus[9:0] is held to a certain value (call it op) during the
first full cycle, and is not constrained afterward,
- fwd is held constant at 16 during the first full cycle, but is
unconstrained afterward,
- a_bus is held at some particular value during the second full
cycle (call it a1), and at a (possibly different) value, a2 during
the third cycle, but is unconstrained otherwise
- b_bus is held at the same value, call it b, for the full second
and third cycle, but is unconstrained otherwise,
- reset is kept off for the entire simulation,
- fuse[0] is explicitly set to X for the whole simulation. This is
similar to setting it to _, but is likely (1) more efficient and (2) more
likely to lead to false Xes in the outputs.
- Any inputs to the module besides those specified above are implicitly
unconstrained (i.e., they are implicitly _) for the whole simulation.
The :outputs section controls when the outputs should be sampled. For
this simulation:
- The full result_bus will be sampled twice. Its results from phases 5
and 6 will be called res1 and res2, respectively.
- The high and low parts of the result_bus will also be sampled during
these cycles. This might seem redundant, but it can be useful in cases where
there is an X in only one side of the result bus.
The :internals section is similar to the outputs section, but it allows
you to pull out the values of internal signals in the module.
The :overrides section is similar to the inputs section, but it allows
you to forcibly install new values onto wires, regardless of how they are
actually driven by the circuit.
Input Line Format
Each line in the :inputs section explains how a certain input should be
driven over time. Each line has the form:
(input-name value1 value2 ... valueN)
The valid input names are:
- A string that names a particular input bus,
- A string that is a Veriog-style bit- or part-select from a particular input
bus,
- (Advanced) an explicit list of E input bits, in LSB-first order. We don't
show this above, and it's not something you probably want to use. But it may
be useful to know about this; generally all of the Verilog-level stuff is just
layered on top of lists of E bits, using a preprocessor, and the STV compiler
only ever sees with these bit lists.
The values explain how to set the bits of this input during the phases of
the simulation. As a convenience, the last value on an input line is
implicitly repeated for the rest of the simulation. What are the legal
values?
- A natural number can be used to set the input to a fixed value during this
particular phase. The number supplied must be within [0, 2^n), where
n is the size of the input, or an error will be caused.
- The special ~ value is intended to support clock inputs, and basically
means invert the previous value of this signal. This is only legal for
one-bit inputs whose previous value expanded to 0 or 1. In practice,
this means the only things that can occur before a ~ are 0, 1,
or another ~.
- The special _ value represents an unconstrained, four-valued variable.
As a rule, use _ during any phase where you don't care about the value on
this input. There is no relationship between separate underscores, e.g., in
the example above, separate variables are used for a_bus during the first
and second phases.
- The special :ONES value sets an input bus to all 1's, no matter what
its size.
- Besides x, any other non-keyword symbols (like op, a1,
a2, and b above) are called simulation variables. A
simulation variable lets you supply a particular value for the input at this
phase when you evaluate the symbolic test vector.
- (Advanced) the special X value allows you to say that an input should
be explicitly set to X values. It is similar to using _, but supplies an
explicit X value instead of fresh variables. The advantage of this is that it
can be very efficient: X values often remain as X as they propagate through
gates, whereas free variables generally become larger expressions. So, using
explicit Xes may lead to more efficient simulations by avoiding the
construction of lots of irrelevant expressions. However, using explicit X
values can also lead to false Xes, e.g., whereas (AND A (NOT A)) is
obviously 0, (AND X (NOT X)) is X. So, using Xes can lead to overly
conservative results.
Output Line Format
Each line in the :outputs section controls when to sample certain
output signals. The format is:
(output-name value1 value2 ... valueN)
As with input-names, the output-names can be either (1) a string that names
a particular output bus, (2) a Verilog-style bit- or part-select, or (3) a list
of E output bits in LSB-first order.
But here the only legal values are:
- _, which means don't sample the output at this time, or
- a symbol, like res1 or res2 above, which gives a name to the
output at this time. These names have to be unique, since outputs can vary
over time.
To avoid any confusion between input and output lines, we don't allow you to
use ~, X, or keyword symbols in output lines.
Internals Line Format
Except for their names, the lines in the :internals section are
essentially the same as lines in the :outputs section. Generally speaking
we try to make the differences between outputs and internal signals as
invisible as possible. For instance, it doesn't matter during stv-run
whether a signal is an internal or output signal.
The names on internal lines may be strings that are Verilog-style plain or
hierarchical identifiers using periods as separators, which may optionally
include a Verilog-style bit- or part-select at the end. It is also possible to
use explicit lsb-first ordered lists of ESIM paths.
Override Line Format
Each line in the :override section explains how to override some
internal wire.
The names in override lines may be strings that are Verilog-style plain or
hierarchical identifiers using periods as separators, which may optionally
include a Verilog-style bit- or part-select at the end. It is also possible to
use explicit lsb-first ordered lists of ESIM paths.
The values here are similar to those of input lines, except that:
- ~ is not allowed, because it would be somewhat confusing.
- _ means "don't override the wire during this phase".
Every variable used in an override line becomes both an input and an output
variable of the STV. For instance, in the example above, we had the following
override line:
("foo.prod" _ _ prod _ _ _ _ )
Here, as an input to the STV, prod allows us to forcibly set the value
of the wire foo.prod. As an output, prod gives us the original,
un-overridden expression for prod. (Well, that's probably mostly
true. If prod depends on other overridden values, or is involved in some
combinational loop so that it affects itself, then this may not be quite
right.)
