Def-svtv-idealized-thm
Prove a theorem about an idealized SVTV via a symbolic simulation lemma about the SVTV itself.
See svex-fixpoint-decomposition-methodology for background on the methodology that this supports.
Usage:
(def-svtv-idealized-thm theorem-name
:svtv svtv-name
:ideal ideal-name
:input-vars input-variable-list
:input-var-bindings input-variable-binding-list
:override-vars 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
: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: What we are calling the "ideal" here must be a svtv-spec object created for the given SVTV, which can be done using def-svtv-ideal.
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
- :svtv is the name of the SVTV
- :ideal must be the name of the "ideal" function produced by def-svtv-ideal, a 0-ary function that produces a svtv-spec object
reflecting the same run as the SVTV, but based on a full fixpoint of the
hardware module.
- :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.
- :input-var-bindings is a list of let-like bindings of input
variables to expressions.
- :override-vars is a list of override-value variables of the SVTV to be
overridden in the FGL theorem.
- :override-var-bindings is a list of let-like bindings of override
value variables to expressions.
- :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 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 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 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.
- :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.
- :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.
- :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.
- :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.
- :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.
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-idealized-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, the svtv-spec-run 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.
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-override-p (svex-envlist-all-keys base-ins) nil))
;; Conclusion given by the user
(equal product (sum-partial-products partial-products)))))
