Def-svtv-to-fsm-thm
Lower a theorem about a SVTV-SPEC to a statement about the underlying FSM.
This macro takes an existing theorem about an SVTV-SPEC and turns it into a
theorem about the cycle FSM underlying it. This can be useful in order to
compose together theorems about multiple SVTVs that are based on the same FSM,
and to prove non-fixed temporal properties that can't be stated at the SVTV
level.
Usage example (from svtv-to-fsm-test.lisp):
(def-svtv-to-fsm-thm counter-invar-fsm-thm
:svtv-spec-thmname counter-invar-svtv-thm
; optional arguments
:eliminate-override-vars (sum1)
:eliminate-override-signals ("sum1")
:rule-classes :rewrite ;; this is the default
:cycle-num-rewrite-strategy :by-cycle ;; this is the default
:primary-output-var (sum-out)
:base-cycle-var base-cycle ;; this is the default
:pkg-sym symbol-from-my-package)
Prerequisites. As with def-svtv-generalized-thm, we need to first
show that the override transparency property holds of our SVTV and its
underlying FSM, using def-svtv-refinement. For following
def-svtv-to-fsm-thm events to work, def-svtv-refinement must be
invoked with the :svtv-spec and :fsm-name options. Unless the FSM is
already defined, the :define-fsm option should be set as well. For
example (from svtv-to-fsm-test.lisp):
(def-svtv-refinement counter-invar-run counter-invar-run-data
:svtv-spec counter-invar-spec
:inclusive-overridekeys t
:fsm counter-fsm
:define-fsm t)
In addition, the theorem to be lowered to the FSM level should be one resulting from an invocation of def-svtv-generalized-thm with the :svtv-spec option -- e.g.:
(def-svtv-generalized-thm counter-invar-svtv-thm
:svtv counter-invar-run
:svtv-spec counter-invar-spec
:input-vars :all
:output-vars (sum-out sum1-out)
:override-vars (sum)
:spec-override-vars (sum1)
:unsigned-byte-hyps t
:hyp (and (<= sum 11)
(<= sum1 10))
:concl (and (<= sum-out 11)
(<= sum1-out 10)))
Note: At the moment, the ideal FSM-based methodology isn't yet supported; it
should work, but we haven't gotten to it yet.
Given these two previous events, we have:
- an FSM, counter-fsm
- an svtv-spec object specifying a run of that FSM on a symbolic but temporally fixed sequence of inputs and a set of outputs to sample at fixed times in that sequence
- an svtv containing combinational svex expressions representing the outputs of the above svtv-spec in terms of their symbolic inputs, assuming initial states and all other inputs are X
- a theorem about the svtv-spec (likely proved by symbolic execution of the svtv).
We now want to lower the theorem about the svtv-spec to a theorem about the FSM. The following form
proves one:
(def-svtv-to-fsm-thm counter-invar-fsm-thm
:svtv-spec-thmname counter-invar-svtv-thm
:fsm counter-fsm)
Arguments
The first argument to the macro gives the name of the theorem to be
generated. The rest are keyword arguments:
- :svtv-spec-thmname (required): The name of the theorem, generated by
def-svtv-generalized-thm, that the new theorem is to be derived
from.
- :eliminate-override-vars: Either :all or a list of SVTV variables
that were left overridden in the svtv-spec-thm that we want to instead sample
as outputs in this theorem. Typically these were ones listed as
:spec-override-vars in the svtv-spec theorem, although they may in some
cases be listed as :input-vars. If :all, then all signals overridden
in the theorem will be eliminated and sampled as outputs, even ones that were
hard-coded overrides in the SVTV.
- :eliminate-override-signals: Either :all or a list of signal
names -- strings, like the signal names used in defsvtv$ -- that are
overridden unconditionally in the SVTV that we instead want to sample as
outputs in this theorem. Setting this to :all has the same effect as
setting :eliminate-override-vars to :all.
- :rule-classes: the rule-classes argument for the final
theorem. Defaults to :rewrite. Note that the final theorem may not be in
a very good form for a non-rewrite rule.
- :cycle-num-rewrite-strategy: one of :all-free,
:by-cycle (the default), or :single-var. This affects the form of
the rewrite rule and how aggressively it tries to match the possible forms of
the cycle numbers at which signals are sampled. In all three cases, every SVTV
variable mentiond in the theorem is bound to (lhs-eval-zx LHS (nth CYCLE
envs/outs)) where envs/outs is either the list of input environments or
outputs of the FSM simulation, LHS is canonical form of the concatenation of
variable selects comprising that SVTV variable, and CYCLE is some expression
giving the cycle number at which the variable is sampled or provided as input.
The form of CYCLE affects how the rule applies as a rewrite rule. Ultimately,
all such cycles are relative to some base cycle, the first cycle at which any
variables are sampled from the envs/outs. But if we express all cycles as
offsets relative to that base cycle, then it will be difficult to apply this
theorem as a rewrite rule: the left-hand side will contain expressions such as
(+ N base-cycle) for various constant values of N, and these may not match
the way these cycle numbers are expressed in the target term. This is still a
good option if we don't intend to use this as a rewrite rule or if the SVTV is
purely combinational so that everything happens in a single cycle; this is what
we do under the :single-var setting. Otherwise, we can use free variables
that are constrained to their proper values by hypotheses so as to make the
rewrite rule easier to apply. Under the setting :all-free, every SVTV
variable has a corresponding cycle-number variable that are all
independent (until restricted by the hypotheses). Under the setting
:by-cycle, there is one cycle-number variable for each cycle in which a
variable is sampled.
- :primary-output-var: This is irrelevant if the
:cycle-num-rewrite-strategy is set to :single-var. Otherwise, this
should be set to the name of an output that is sampled in the
svtv-spec-thm (i.e., listed in the :output-vars of the def-svtv-generalized-thm form). For best behavior as a rewrite rule, this
variable should occur in the LHS of the conclusion. When applied as a rewrite
rule, this variable will essentially match an expression such as
(lhs-eval-zx "signal" (nth (+ 3 k) outs)) where outs is an evaluation
of the FSM. This will determine the time offset (here (+ 3 k) minus the
time offset of this output variable in the SVTV) for this application of the
theorem. If not specified, we pick an arbitrary variable from the SVTV
theorem's output-vars.
- :base-cycle-var: A variable name to be used in the final theorem;
it's only important that it doesn't conflict with other variable names. The
default is sv::base-cycle.
- :pkg-sym: symbol that determines the package in which to put newly
generated names. Defaults to the theorem name.