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

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.

: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 oflet -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 oflet -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 oflet -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 tofgl::def-fgl-thm but can be set to (e.g.)defthm orfgl::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 adefthm form or FGL keyword args forfgl::def-fgl-thm orfgl::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 provingintegerp 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 todefthm 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 addunsigned-byte-p hypotheses for each input and override variable.

The initial override theorem is typically proved with FGL, but can be done
otherwise using the

- 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

(svex-env-reduce '(product) (svtv-spec-run (multiplier-svtv-ideal) `((opcode . ,*mul-opcode*) (partial-products . ,partial-products) ...)))

The generalized theorem refers to a single free variable

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)))))