Def-svtv-generalized-thm
Prove a theorem about an idealized SVTV via a symbolic simulation lemma about the SVTV itself.
See svex-decomposition-methodology for background on the methodology that this supports.
Usage:
(def-svtv-generalized-thm theorem-name
:svtv svtv-name
:ideal ideal-name
:svtv-spec svtv-spec-name
:input-vars input-variable-list
:input-var-bindings input-variable-binding-list
:override-vars override-variable-list
:override-var-masks override-var-mask-alist
:x-override-vars x-override-variable-list
:override-var-bindings override-variable-binding-list
:spec-override-vars override-variable-list
:spec-override-var-bindings override-variable-binding-list
:output-vars output-variable-list
:output-parts output-part-list
:hyp hypothesis-term
:concl conclusion-term
:final-hyp hyp-term
:enable rules-list
:unsigned-byte-hyps nil
:no-lemmas nil
:no-integerp nil
:lemma-nonlocal nil
:lemma-defthm nil
:lemma-args nil
:lemma-use-ideal nil
:hints hints
:rule-classes rule-classes
:pkg-sym sym)
For each of the keyword arguments, if absent a default will be looked up in
the table svtv-generalized-thm-defaults, which may be (locally)
modified by users in order to avoid (for example) the need to repeatedly
specify the same SVTV and ideal in every form.
Prerequisite: See def-svtv-refinement and def-svtv-ideal
for the possible ways of
showing that the override transparency property holds of your design, which is
required for the use of this utility.
The generalized theorem produced by this utility may be about either a run
of the given SVTV, of an idealized SVTV-spec as produced by def-svtv-ideal, or of an SVTV-spec object equivalent to the SVTV.
- If the :ideal argument is given, it must be the name of the idealized
svtv-spec function as defined by def-svtv-ideal. This allows the use of
the fixpoint-based methodology disucssed in svex-decomposition-methodology, which avoids the syntactic check on the FSM
that is otherwise needed. The generalized theorem will be about the
svtv-spec-run of this idealized svtv-spec object. This argument should
be mutually exclusive with the :svtv-spec argument.
- If the :svtv-spec argument is given, it must be the name of the
svtv-spec function produced by def-svtv-refinement with the optional
:svtv-spec argument, and that event will do the syntactic check necessary
to ensure override transparency. The generalized theorem will be about the
svtv-spec-run of this object. The svtv-spec-run takes extra
inputs base-ins and initst that makes this more general than the run
of the SVTV (which always has Xes for the initial state and any inputs not
bound in the SVTV stimulus pattern).
- If neither the :svtv-spec nor the :ideal argument is given, then
the generalized theorem will be about the svtv-run of the SVTV itself.
The def-svtv-refinement event must have done the syntactic check
necessary to ensure override transparency.
We briefly describe the arguments of the macro and then we'll describe the
theorem proved in FGL and the generalized corollary this macro generates.
Arguments
Several arguments come in pairs with the naming convention
:<arg>, :more-<arg>. This allows one of these (typically the :more
version) to be set by the defaults table while the other still be set in
individual theorems. We note below which arguments support this and how the
two arguments are combined.
- :svtv is the name of the SVTV. This argument must always be provided
either explicitly or via the defaults table.
- :ideal and :svtv-spec affect the form of the generalized theorem; see above.
- :input-vars are the names of any input variables of the SVTV that will
appear in the hypothesis or conclusion, except those that are bound in
:input-var-bindings. Instead of a list of signals, users may pass ":all"
parameter to get all the input variables that are not bound. If not :all,
additional input variables can be specified in :more-input-vars; the two
sets of input variables are appended.
- :input-var-bindings (appended with :more-input-var-bindings is a
list of let-like bindings of input variables to expressions.
- :override-vars (appended with :more-override-vars)
is a list of override-value variables of the SVTV to be
overridden in the FGL lemma but not overridden in the generalized theorem.
Each such variable must have a corresponding output sampling the same signal at
the same time so as to support eliminating the override.
- :override-var-masks
is an alist of override-value variables bind to a mask value, which will be
used to override only a portion of the designated variable. Example call:
:override-var-masks ((mul-sum . (logmask 16))
(mul-carry . (logmask 16)))
- :override-var-bindings (appended with :more-override-var-bindings)
is a list of let-like bindings of override
value variables to expressions, to be overridden in the lemma but not
overridden in the generalized theorem. Each such variable must have a
corresponding output sampling the same signal at the same time so as to support
eliminating the override.
- :x-override-vars (appended with :more-x-override-vars) is a list
of override-value variables that will be overriden to X in the lemma, and not
mentioned in the final theorem; effectively, this asserts that these signals
are not relevant to the current computation and prunes them out of the fanin
cone by forcing them to X.
- :spec-override-vars (appended with :more-spec-override-vars)
is a list of override-value variables of the SVTV
to be overridden in both the FGL theorem and the resulting generalized theorem.
The difference between :override-vars and :spec-override-vars is that
the :override-vars will not be overridden in the generalized theorem, but
the :spec-override-vars still will.
- :spec-override-var-bindings (appended with :more-spec-override-var-bindings)
is a list of let-like bindings of
override value variables to expressions, which will be overridden in both the
FGL theorem and generalized theorem.
- :output-vars (appended with :more-output-vars)
is a list of output variables of the SVTV that are used in the conclusion.
- :output-parts is a list of 4vec expressions -- part selects, zero
extends, shifts, concatenations -- of the output variables. The given parts of
the outputs will be proved to be integerp in order to use a monotonicity
argument. Variables that are not mentioned in output-parts will be proved
integerp as a whole.
- :hyp (conjoined with :more-hyp is a term (default T), which may
reference variables listed in input-vars and override-vars as well as variables
used in the expressions of input-bindings.
- :concl is a term which may reference the same variables available to
:hyp as well as the output-vars.
- :final-hyp is a term (default T) with is conjoined at the beginning of
the hypotheses only of the final theorem. This is sometimes convenient for
adding syntaxp or bind-free directives.
- :enable is a list of rules to be included in the theory for the final
generalized theorm, mainly useful when specifying :output-parts.
- :no-lemmas says to skip the initial override theorem and monotonicity
lemma and tries to prove the final (generalized) theorem directly, with the
hints given by the user.
- :hints are hints for the final theorem, used by themselves if :no-lemmas
is set and in addition to the automatically provided hints if not.
- :lemma-defthm defaults to fgl::def-fgl-thm but can be set
to (e.g.) defthm or fgl::def-fgl-param-thm to change how the initial
lemma is proved.
- :lemma-args gives additional arguments to be passed to the form
proving the initial lemma, which could be hints for a defthm form or FGL
keyword args for fgl::def-fgl-thm or fgl::def-fgl-param-thm.
- :lemma-use-ideal phrases the lemma in terms of a run of the ideal
svtv-spec, rather than the SVTV.
- :lemma-use-svtv-spec phrases the lemma in terms of a run of
the (non-ideal) svtv-spec, rather than the SVTV.
- :lemma-nonlocal makes the lemma not be local.
- :lemma-custom-concl gives a custom conclusion for the lemma, different
from the one to be used in the final theorem. Can be convenient if it is
easier to prove the lemma in a different form which still implies the form of
the conclusion in the final theorem.
- :lemma-no-run makes the lemma not bind the output variables, skipping
the svtv-run (in the common case, or the svtv-spec-run in others); may be
useful with :lemma-custom-concl.
- :no-integerp says to skip proving integerp of each output in the
initial override theorem. The :enable option typically must be used to
provide additional rules for the final theorem to show that the lemma implies
the outputs are integers.
- :integerp-separate says to prove integerp of each output in a second
lemma, not the initial override theorem.
- :integerp-defthm defaults to defthm but can be set to (e.g.)
fgl::def-fgl-thm to choose a different method of proving the integerp
lemma, when :integerp-separate is set.
- :integerp-args gives a list of arguments for the event proving the
integerp lemma, when :integerp-separate is set). If none are given, the
default is to provide a hint using an instance of the override lemma and
disabling it, since commonly the override lemma itself implies all the outputs
are integers.
- :final-defthm defaults to defthm but can be set to a different
macro to change how the final generalized theorem is proved
- :final-defthm-args gives additional arguments to the form proving the
final generalized theorem.
- :rule-classes gives the rule classes of the theorem proved.
- :unsigned-byte-hyps says to automatically add unsigned-byte-p
hypotheses for each input and override variable.
- :run-before-concl gives a term that is placed in the override lemma
within (progn$ run-before-concl concl), perhaps to do some extra printing
in case of a counterexample.
- :integerp-run-before-concl gives a term to add to the integerp lemma
when :integerp-separate is set, similar to :run-before-concl.
- :pkg-sym defaults to the theorem name, and picks the package that
various symbols are generated in.
Initial override lemma
The initial override theorem is typically proved with FGL, but can be done
otherwise using the :lemma-defthm argument. It says that under the given
hypotheses, a run of the SVTV on a particular, explicitly constructed
environment produces outputs satisfying the conclusion. In addition, it proves
that those outputs are integers (whereas they could otherwise be arbitrary
4vecs including X and Z bits). The environment is constructed as
follows:
- Input variables bound in :input-var-bindings are bound to their respective values
- Input variables listed in :input-vars are bound to variables of the same name
- Override value variables listed in :override-vars and
:spec-override-vars are bound to variables of the same name
- Override value variables bound in :override-var-bindings and
:spec-override-var-bindings are bound to their respective values
- Override test variables corresponding to the override value variables
listed in :override-vars, :override-var-bindings,
:spec-override-vars, and :spec-override-var-bindings are all bound to
-1.
For example, the following form:
(def-svtv-generalized-thm partial-prods-to-product
:svtv multiplier-svtv
:ideal multiplier-svtv-ideal
:input-var-bindings ((opcode *mul-opcode*))
:spec-override-var-bindings ((clkgates 0))
:override-vars (partial-products)
:output-vars (product)
:hyp (unsigned-byte-p 128 partial-products)
:concl (equal product (sum-partial-products partial-products)))
produces approximately the following initial lemma:
(fgl::def-fgl-thm partial-prods-to-product-override-lemma
(implies (unsigned-byte-p 128 partial-products)
(b* ((run (svtv-run (multiplier-svtv)
`((opcode . ,*mul-opcode*)
(partial-products . ,partial-products)
(clkgates . 0)
(override-partial-products . -1)
(override-clkgates . -1))
:include '(product)))
(product (svex-env-lookup 'product run)))
(and (integerp product)
(equal product (sum-partial-products partial-products))))))
The :lemma-use-ideal option would replace the svtv-run form with the
following form:
(svex-env-reduce '(product)
(svtv-spec-run (multiplier-svtv-ideal)
`((opcode . ,*mul-opcode*)
(partial-products . ,partial-products)
...)))
Generalized theorem
The generalized theorem refers to a single free variable env rather
than a free variable for each input and override value. It binds run to
the run of the ideal on that env. Input variables -- both those listed in
:input-vars and the keys of :input-var-bindings -- are bound to their
lookups in env, and hypotheses are added stating that the keys of
:input-var-bindings are bound to their respective values. Outputs are
bound (as usual) to their lookups in run, and override variables from
:override-vars and :override-var-bindings are additionally bound to
the lookups of their respective reference variables in run. Override
variables listed in :spec-override-vars and
:spec-override-var-bindings are still overridden, i.e. the value variables
are looked up in env similar to inputs. An additional hypothesis states
that the only override test variables that are set in the env are those
corresponding to the value variables listed in :spec-override-vars and
:spec-override-var-bindings: this is the
svtv-override-triplemaplist-envs-match hypothesis in the theorem below.
Finally, when the :ideal or :svtv-spec options are used, the generalized
theorem refers to svtv-spec-run instead of svtv-run which allows an
additional setting of input and initial
state variables not set by the SVTV itself; these are given respectively by
base-ins and initst in the theorem. Base-ins, however, must be
assumed not to set any additional override test variables. The
svarlist-nonoverride-p hypothesis of the theorem below ensures this.
For example, the form above produces approximately the following generalized
theorem, which we have annotated to say where each binding and hypothesis comes
from:
(defthm partial-prods-to-product
(b* (;; Input variables bound to their lookups in env
(opcode (svex-env-lookup 'opcode env))
;; Spec-override variables bound to their lookups in env
(clkgates (svex-env-lookup 'clkgates env))
;; Run the idealized SVTV
(run (svtv-spec-run (multiplier-svtv-ideal) env :base-ins base-ins :initst initst))
;; Override variables bound to their lookups in run
(partial-products (svex-env-lookup 'partial-products run))
;; Output variables bound to their lookups in run
(product (svex-env-lookup 'product run)))
(implies (and ;; Hyp given by the user
(unsigned-byte-p 128 partial-products)
;; Implicit hyp from input-var-bindings
(equal opcode *mul-opcode*)
;; Implicit hyp from spec-override-var-bindings
(equal clkgates 0)
;; Env only overrides those variables mentioned in spec-override-vars/bindings
(svtv-override-triplelist-envs-match
(multiplier-svtv-triplemaplist)
env
'((override-clkgates . -1)))
;; Base-ins doesn't add any override test settings
(svarlist-nonoverride-p (svex-envlist-all-keys base-ins) :test))
;; Conclusion given by the user
(equal product (sum-partial-products partial-products)))))
Subtopics
- Svtv-override-triplemaplist-envs-match
- Checks that the given environment env has values matching
spec for the override test and value variables of the given triplemaplist
triplemaps.
