(Deprecated) Proving that a decomposition is equivalent to some whole.

Here is an example, from "svex/tutorial/boothpipe.lisp", showing
how to use

(defthm boothmul-decomp-is-boothmul (implies (boothmul-direct-autohyps) (b* ( ;; Run the first part of the circuit to get the partial products (in-alist1 (boothmul-step1-autoins)) (out-alist1 (sv::svtv-run (boothmul-step1) in-alist1)) ;; Get the results from the output and stick them into an ;; input alist for step2. Some control signals from the ;; original input alist also are needed. (in-alist2 (boothmul-step2-alist-autoins (append out-alist1 in-alist1))) ;; Run the second part of the circuit on the results from the ;; first part, summing the partial products. (out-alist2 (sv::svtv-run (boothmul-step2) in-alist2)) ;; Separately, run the original circuit. (orig-in-alist (boothmul-direct-autoins)) (orig-out-alist (sv::svtv-run (boothmul-direct) orig-in-alist))) (equal ;; The final answer from running the decomposed circuit the second ;; time, after feeding its partial products back into itself. (cdr (assoc 'o out-alist2)) ;; The answer from running the original circuit. (cdr (assoc 'o orig-out-alist))))) :hints((sv::svdecomp-hints :hyp (boothmul-direct-autohyps) :g-bindings (boothmul-direct-autobinds))))

The

Additional optional arguments:

:enable simply adds a list of rules to the theory used in the first step, before the meta rules are used. This is useful because the conclusion of the theorem must be in a particular form, described below, for the meta rules to work. If the statement of the theorem uses special-purpose functions to (say) construct alists or compare outputs, the theory may need to be augmented with rules to rewrite these functions away so that the meta rule can work.:rewrite-limit sets the limit on the number of passes of rewriting to do on the resulting svex expressions. In some cases it might be useful to set this to 0, to disable rewriting. Using this keyword argument actually sets the state global variablesv::svdecomp-rewrite-limit , which sets the limit for future calls as well.

The core algorithm of the meta rule operates on a call of

(equal (svex-eval (svex-compose x a) env) (svex-eval x (append (svex-alist-eval a env) env)))

The meta rule supposes that the top-level evaluation is equivalent to the
RHS of the above rule for some term

This re-composition is usually best done at the top level, so the meta rules trigger on any of the following:

(equal (svex-eval (quote sv1) env1) (svex-eval (quote sv2) env2))

(equal (svexlist-eval (quote sv1) env1) (svexlist-eval (quote sv2) env2))

(equal (svex-alist-eval (quote sv1) env1) (svex-alist-eval (quote sv2) env2))

The

(quote val)

(cons (cons (quote var) val) env1)

(cons (quote (var . val)) env1)

(binary-append env1 env2)

(svex-alist-eval (quote svalist) e)

- Decomp.lisp
- Svdecomp-hints
- (Deprecated) Hint used for svex hardware model recomposition proofs -- see svex-decomp.