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

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 inputsbase-ins andinitst 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 thesvtv-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.

Several arguments come in pairs with the naming convention

: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 oflet -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 oflet -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 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.: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 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.:integerp-separate says to proveintegerp of each output in a second lemma, not the initial override theorem.:integerp-defthm defaults todefthm 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 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.: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.

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

(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-nonoverride-p (svex-envlist-all-keys base-ins) :test)) ;; Conclusion given by the user (equal product (sum-partial-products partial-products)))))

- Svtv-override-triplemaplist-envs-match
- Checks that the given environment
env has values matchingspec for the override test and value variables of the given triplemaplisttriplemaps .