Defsvtv$
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.
- :stages (or equivalently, but perhaps deprecated, :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 :stages, 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
:stages is recommended since it tends to be easier to edit. The format of
the :stages 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):
:cycle-phases
(list (make-svtv-cyclephase :constants '(("clock" . 0))
:inputs-free t
:outputs-captured t)
(make-svtv-cyclephase :constants '(("clock" . 1))))
In this case, the entries in the :stages argument or the columns in the
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 stages or timing diagram; this
corresponds to the following cycle-phases value:
:cycle-phases
(list (make-svtv-cyclephase :constants nil
:inputs-free t
:outputs-captured t))
- :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 :stages (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 (often just
a singleton). 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 produced. Additionally, if these clock signals are set in the
:stages argument and not in the :cycle-phases, their assignments in
each phase will initially be used to simplify the nextstate before composing
the pipeline.
- :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).
:stages argument format
The :stages (or :phases) argument may either be evaluated or not.
The decision to evaluate or not is done by checking the caar of the
argument: if it is a keyword symbol, then this is consistent with the format of
a literal stages list but not consistent with any untranslated term, so then it
will not be evaluated; otherwise it will. The following description of the
argument format pertains to the result of evaluating the argument, or the
literal form if not evaluated.
The following example shows the main features of the :stages argument
format:
:stages
(;; Phase 0:
(:label p
:inputs (("clk" 0 :toggle 1) ;; will toggle each phase until end or until reassigned
("start" 1)))
;; Phase 4:
(:delay 4 ;; number of stages since last one listed
:label q
: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:
(:delay 2
:label r
:inputs (("late" late6))
:outputs (("early" early6)))
;; Phase 8:
(:delay 2
:label s
:inputs (("cntl" _)) ;; release previous held value
:outputs (("inst.subinst.interesting" interesting8))))
The format of this argument is a list of individual stages, 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
(signal-name variable-name)
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 boolean-or-posp | :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. Alternatively,
it may be set to a positive integer in which case the given value is repeated
for that many stages (unless superseded by a subsequent setting) -- the default
value is 1, meaning the assignment is only for the current stage.
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
constant.
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 optional keywords:
- :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
field).
- :output, if specified, adds an output variable for the same signal.
This output will be assigned the non-overridden value of the signal.
The methodology for decomposition proofs (see svex-decomposition-methodology) makes use of conditional overrides with
corresponding output signals. A convention for these signals is to give the
same name to the override value and output variables, and name the override
condition with an "-ovr" suffix. For example:
:overrides (("foo" foo :cond foo-ovr :output foo))
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 :stages 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.
