Defsvtv-phasewise
(Deprecated) Alternative format for creating an SVTV.
This is deprecated in favor of defsvtv$.
A longstanding frustration with the SVTV user interface is that you
need to insert the right number of underscores on each line before a cycle in
which something happens. When the sequencing changes, you need to then insert
or delete the right number of underscores on multiple lines.
This alternative interface for defsvtv works around this problem by
generating an old-style SVTV from a new input format that is easier to get
right and easier to maintain.
The input format looks like this:
(defsvtv$-phasewise my-svtv
:design *my-design*
:parents ... :short ... :long ...
:simplify t ;; default
:phases
(;; 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 phases 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 keyword options are the same as for defsvtv$, except that
:phases replaces :inputs, :overrides, :outputs,
:internals, and :labels.
For now, defsvtv$-phasewise is implemented by simply preprocessing it into a defsvtv$ form. Perhaps later both forms will instead be different interfaces
to a shared backend.
The format of the :phases input 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
(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 t-or-nphases | :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. If it is set to a
number, it is held for that number of additional phases or until it is set
again. I.e., :hold 0 would be the same as :hold nil (but isn't
allowed), :hold 1 means hold for a total of two phases -- the current
one (which this entry would affect without the hold) and one additional.
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 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
field).
- :output, if specified, gives an output variable for the same signal at
the given time. This output will be assigned the non-overridden value of the
signal. This syntactic convenience supports the recommended method for
decomposition proofs; see def-svtv-generalized-thm. The :hold and
:toggle options don't apply to the output, in that it is only sampled at
the phase in which it is declared.
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.
