Svtv-stimulus-format
(Deprecated) Syntax for inputs/outputs/overrides/internals entries of defsvtv forms
This stimulus format can still be used in defsvtv$ and
the (deprecated) defsvtv, but the :phases format is recommended
instead.
An SVTV is a timing diagram-like format similar to esim ACL2::symbolic-test-vectors. Each of the fields :inputs, :outputs,
:overrides, and :internals may have a table (list of lists) where the
rows each pertain to a particular (vector) signal and the columns each pertain
to a particular time step. The :inputs and :overrides entries
provide inputs to the simulation and the :outputs and :internals
entries extract outputs.
Example
Here is an example input/override table:
'(("clk" 1 ~) ;; toggles until the end
("enable" _ en) ;; keeps assigned value until the end
("dataport" _ #x20 _)
("data_busa" _ _ _ a _)
("data_busb" _ _ _ b _)
("opcode" _ op _ _ _)
("clkgates" _ -1 _ -1 _))
And an example output/internal table:
'(("output_signal1" _ _ _ out1 _ _ _)
("output_signal2" _ _ _ _ _ out2 _))
In both cases, each table is a list of lists. Each interior list
contains a signal name followed by a list of entries, each of which corresponds
to a phase of simulation. The number of simulation phases of an SVTV is the
maximum length of any such entry list among the :inputs, :outputs,
:overrides, and :internals. Input/override entries that are shorter
than the simulation are extended to the simulation length by repeating their
last entry, whereas output/internal entries that are shorter than the
simulation are extended with _ entries.
Output Specifications
There are only two kinds of valid entry for :outputs/:internals
tables:
- _ or -, meaning the signal is ignored at the phase
- A variable name, meaning that the signal's value at that phase is assigned
to that output variable.
So in the above example, at simulation time frame 4, the value of
"output_signal1" will be extracted and at time frame 6, the value of
"output_signal2" will be extracted; and these values will be assigned,
respectively, to output variables out1 and out2.
Input Specifications
There are several types of valid entries for :inputs/:overrides
tables:
- _ or - (actually, any symbol whose name is "_" or "-") makes
the signal undriven at that phase. Actually, this means slightly different
things for inputs versus overrides: for an input, the wire simply doesn't get
assigned a value, whereas for an override, it isn't overridden at that
phase.
- An integer or 4vec: the signal is assigned that value at that
time. (An integer is a 4vec, just to be clear.)
- (Deprecated): the symbol acl2::x means the same thing as the constant
value (4vec-x) or (-1 . 0), namely, assign all bits of the signal the
value X at the given phase.
- (Deprecated): the symbol :ones means the same thing as -1, namely,
assign all bits of the signal the value 1 at the given phase.
- The symbol ~ (actually, any symbol whose name is "~"), which must be
preceded by a constant (4vec) or another ~, means the signal is assigned
the bitwise negation of its value from the previous phase. Thus the "clk"
signal in the above example is assigned 1, then 0, then 1, etc., because the
final ~ is replicated out to the end of the simulation.
- Any other symbol becomes an input variable assigned to that signal at that
phase.
