Create an SVTV structure for some simulation pattern of a hardware design.
See the sv-tutorial and the parent topic svex-stvs for
higher-level discussion; here, we provide a reference for the arguments.
- :design or :mod provides the SVEX design object containing
the hierarchical hardware model. One or the other of :design or :mod
should be given, but not both; they mean exactly the same thing.
- :phases describes what happens at each phase, or each clock cycle if
the :cycle-phases argument (below) is used: what inputs and overrides are
set and what outputs are sampled. Additionally, each phase may be given a
label for documentation purposes. As an alternative to :phases, arguments
:inputs, :overrides, and :outputs may be provided at the top
level with a timing diagram format, described below; this is the same format as
was used in the previous version defsvtv and ESIM's defstv, but using
:phases is recommended since it tends to be easier to edit. The format of
the :phases argument is described in its own section below.
- :cycle-phases optionally describes a clock cycle. Its value must be a
list of svtv-cyclephase objects. A typical clock cycle has two phases
where the clock is low in one and high in the other, and input signals are
provided and outputs read in the clock-low phase (this is appropriate for
typical positive-edge-triggered flip-flops):
(list (make-svtv-cyclephase :constants '(("clock" . 0))
(make-svtv-cyclephase :constants '(("clock" . 1))))
In this case, the phases of the provided timing diagram refer to the clock
cycles of the design rather than individual clock phases.
The default, when the :cycle-phases argument is not provided, is for
all clock phases to be explicitly represented in the timing diagram; this
corresponds to the following cycle-phases value:
(list (make-svtv-cyclephase :constants nil
- :parents, :short, :long, and :labels pertain to
documentation; if any of :parents, :short, or :long are given
then additional xdoc will also be generated to show a timing diagram.
:labels may only be used without :phases (alongside :inputs,
:outputs and :overrides), which has its own syntax for providing
phase labels; if provided, these label the phases in that timing diagram.
- :monotonify is T by default; it says whether to rewrite certain SVEX
constructs that are not bitwise monotonic with respect to Xes into monotonic
ones. Generally this is desirable; this monotonicity is used when generalizing
SVTV theorems for use in proof decomposition; see decomposition-proofs.
- :simplify is T by default; it can be set to NIL to avoid rewriting the
output svex expressions after composing the pipeline.
- :pre-simplify is T by default, and controls rewriting the svex
expressions at earlier stages -- after flattening, phase FSM composition, and
cycle FSM composition.
- :pipe-simp is NIL by default and must be a svex-simpconfig-p
object. It determines the level of SVEX simplification used on-the-fly when
composing cycle formulas together to compute the pipeline formulas.
- :cycle-simp is NIL by default and must be a svex-simpconfig-p
object. It determines the level of SVEX simplification used on-the-fly when
composing phase formulas together to compute the clock cycle formula, when
using the :cycle-phases feature.
- :define-macros is T by default; it controls whether macros
<svtv>-autoins, <svtv>-autohyps, etc. are created
- :define-mod is NIL by default; it controls whether a 0-ary function
<svtv>-mod is defined, returning the SV design for the SVTV. This is used
by some legacy utilities such as svtv-debug and svtv-chase, but
these are deprecated in favor of svtv-debug$ and svtv-chase$.
- :phase-config is the config object for the phase FSM
computation. Currently it is mainly an advanced feature useful for tweaking
which signals are conditionally overridden in the phase and cycle FSMs. By
default all internally driven signals are conditionally overridden; this makes
it so that it is fast to recompute the pipeline when changing the phases, even
if overrides are modified. But there may be some cases where it is better to
allow either only a few specific signals to be overridden, or else disallow a
few particular signals from being overridden.
- :clocks may be set to a list of clock input variable names. If this is
provided, then an analysis will be done before computing the phase FSM to
determine what other signals are derived clocks, and avoid providing
conditional overrides on these derived clock signals. It may be important to
avoid building conditional overrides on such signals because they can prevent
important simplifications that reduce the size of the expressions
- :phase-scc-limit affects the phase FSM constructed in cases where
there is an apparent combinational loop at the bit level. An apparent
combinational loop is equivalent to a strongly connected component in the
signal dependency graph; when such an SCC exists, self-composing those signals'
assignments N times where N is the size of the SCC is guaranteed to reach a
fixed point if all expressions are X-monotonic. However, in practice this can
result in very large expressions, and in practice a few such self-composition
iterations is all that is necessary. Setting the phase-scc-limit to a natural
number (instead of the default, NIL, meaning no limit) restricts the number of
self-composition steps to that limit. Warning: If you build an SVTV with a
current phase-scc-limit, then change the phase-scc-limit and try to build it
again, that won't be sufficient to force the phase FSM to be recomputed. You
can force this with
(update-svtv-data->phase-fsm-validp nil svtv-data).
:phases argument format
The following example shows the main features of the :phases argument
(;; Phase 0:
:inputs (("clk" 0 :toggle 1) ;; will toggle each phase until end or until reassigned
;; Phase 4:
(:delay 4 ;; number of phases since last one listed
:inputs (("cntl" cntl4 :hold t)) ;; will hold this value until end or until reassigned
:overrides (("inst.subinst.internalsig" internal4)
;; syntax for combined conditional override/output
("inst.subinst.decompsig" decompsig :cond decompsig-ovr :output decompsig)
;; old syntax for conditional override
("inst.subinst.decompsig" (testsig testsig-ovr))))
;; Phase 6:
:inputs (("late" late6))
:outputs (("early" early6)))
;; Phase 8:
:inputs (("cntl" _)) ;; release previous held value
:outputs (("inst.subinst.interesting" interesting8))))
The format of this argument is a list of individual phases, which are
keyword-value lists with the following keywords recognized:
- :delay: Number of phases since the previous one in the list,
defaulting to 1. Must be positive. (Note: If the first phase in the list has
a delay of 1, its assignments occur on the first phase that is to be simulated.
Phase 0 is skipped, in some sense.)
- :label: Optional name of the phase, for documentation purposes.
- :inputs: Input signals to be assigned a value at that phase. Entries are described below.
- :overrides: Internal signals to be overridden to some value at that phase. Entries are described below.
- :outputs: Signals to be read and their values stored in variables at that phase.
The format for :outputs is simply a list of entries of the form
where signal-name is a string giving the real hierarchical name in the
design and variable-name is a symbol.
The format for :inputs is a list of entries of the form:
(signal-name setting [ :hold t-or-nil | :toggle nphases ])
Setting can be one of:
- a 4vec constant, that is, an integer or a pair (upper . lower), both integers
- a don't-care indicator, which is a symbol whose name is "_", "-", or "&" in any package
- a variable, i.e. any other non-Boolean, non-keyword symbol.
The :hold keyword, if set to t, indicates that this assignment is
valid for all subsequent phases until the same signal is set again.
The :toggle keyword, if set to t or a positive integer nphases,
indicates that the signal will be held and toggled every nphases phases,
where t is the same as 1. It is only valid (for now) if the setting is a
Note: Don't use the special symbol ~, which is what you'd use for
:toggle in the original defsvtv.
The format for :overrides is similar to that of inputs, but adds two
additional keyword variables:
- :cond, if specified, gives an override condition value (a variable or
4vec constant), making this a conditional override. This means bits of the
signal corresponding to 1-bits of the override condition are overridden and
take the value of the corresponding bits of the override value (setting
- :output, if specified, gives an output variable for the same signal.
This output will be assigned the non-overridden value of the signal.
The setting field can also take one additional form (value test),
which is another way of specifying a conditional override (this may not be used
along with the :cond keyword). Here test is the override condition
and value is the override value.
The :toggle and :hold keywords still apply to overrides and
conditional overrides: :hold means that test and value both apply to
subsequent phases, and :toggle means that test applies to subsequent
phases and value is toggled.
Legacy stimulus/sampling specification format
Previous versions of this utility -- defsvtv and ESIM's
acl2::defstv -- used another format for specifying stimulus and output
sampling. Instead of a :phases argument, these utilities took
:inputs, :outputs, :overrides, and :labels. The format of
the first three is described in svtv-stimulus-format. The :labels
argument is a list of symbols giving names to each phase for documentation
purposes. Note that when using the :cycle-phases argument, each phase
listed in :labels or in an :inputs, :outputs, or :overrides
entry actually refers to a clock cycle.