Proof by decomposing and re-composing a hardware model

Part of the sv-tutorial. Previous section: proofs-with-stvs.

Certain kinds of hardware models aren't amenable to direct verification by bit-blasting because the function computed is too hard for SAT solvers/BDD packages. Multipliers, most significantly, fall into this category -- expressing a multiplier function as BDDs always results in exponential memory usage, and they are notoriously difficult for SAT solvers to handle as well. A standard trick for verifying a multiplier is to split the design into two or more parts, specifying separately how each of the parts should behave; prove (by bit-blasting or automatic methods) that each of the parts matches its specification, and prove (by traditional theorem-proving methods) that the composition of the spec functions is equivalent to the spec for the whole module.

The file "boothpipe.lisp" where this documentation topic is defined contains an example to show how to do this with SVEX. In this topic we will discuss a few critical parts of the process, but for a more complete picture see that file and the comments in it.

In the boothpipe example, the intermediate signals to split the pipeline on
are the partial products

(defsvtv$ boothpipe-run :design *boothpipe* :cycle-phases (list (make-svtv-cyclephase :constants '(("clk" . 0)) :inputs-free t :outputs-captured t) (make-svtv-cyclephase :constants '(("clk" . 1)))) :phases ((:label c0 :inputs (("en" en :hold t) ("a" a) ("b" b))) (:label c1 :outputs (("minusb" minusb))) (:label c2 :overrides (("pp01_c2[35:18]" pp0 :cond pp0-ovr :output pp0) ("pp01_c2[17:0]" pp1 :cond pp1-ovr :output pp1) ("pp23_c2[35:18]" pp2 :cond pp2-ovr :output pp2) ("pp23_c2[17:0]" pp3 :cond pp3-ovr :output pp3) ("pp45_c2[35:18]" pp4 :cond pp4-ovr :output pp4) ("pp45_c2[17:0]" pp5 :cond pp5-ovr :output pp5) ("pp67_c2[35:18]" pp6 :cond pp6-ovr :output pp6) ("pp67_c2[17:0]" pp7 :cond pp7-ovr :output pp7))) (:label c3 :outputs (("o" o)))) :parents (decomposition-proofs))

Each entry in the

("pp01_c2[35:18]" pp0 :cond pp0-ovr :output pp0)says

The basic steps for completing the top-level proof we want are as follows:

- Prove that the partial products are correctly computed.
- Prove that summation of the partial products is correctly computed.
- Prove that the correct summation of the correctly-computed partial products produces a multiply.
- Put steps 1 through 3 together to prove that the output of the circuit is a multiply.

Steps 1 and 2 can be done via bit-blasting proofs as discussed in the previous section of the tutorial (proofs-with-stvs). However, since we are using conditional overrides there are a couple of extra steps involved in making it so they can be composed together, which we'll discuss next. Step 3 is simply an ACL2 arithmetic proof, and step 4 is also done with regular ACL2 rewriting.

In Step 2, proving that the summation of the parital products is correct, we
want to override the partial products of the SVTV with free variables and show
that the output computed is a function of those variables. However, ultimately
we want to know what happens in the SVTV when these signals are not
overridden. To do this, we'll use the facts that we prove via symbolic
simulation on the SVTV to prove similar facts about another object, the
*ideal* svtv-spec. The topic svex-fixpoint-decomposition-methodology has more details of what this object
is; generally speaking, we won't compute the ideal but we'll prove things about
it and we can sometimes execute a simulation of it (via a mbe trick).
First we define the ideal as a 0-ary function (though it will produce an error
if that function is run), and automatically prove some facts relating the SVTV
to the ideal. These facts show:

- Runs of the SVTV are conservative approximations of runs of the ideal, and
- The ideal has the property that if a signal is overridden with the value that signal would have anyway, it doesn't change the values of any other signals.

These facts allow us to generalize proofs about the SVTV to theorems about the ideal, which can easily be composed together. The steps for defining the ideal are as follows:

(def-svtv-data-export boothpipe-data)

(def-svtv-ideal boothpipe-ideal boothpipe-run boothpipe-data)

This last event (for which the previous one is a prerequisite) produces a
0-ary function

Now we can use the def-svtv-idealized-thm utility to prove our two
steps. First, we set some defaults that will be used for all

(progn (local (table svtv-idealized-thm-defaults :svtv 'boothpipe-run)) (local (table svtv-idealized-thm-defaults :ideal 'boothpipe-ideal)) (local (table svtv-idealized-thm-defaults :unsigned-byte-hyps t)) (local (table svtv-idealized-thm-defaults :input-var-bindings '((en 1)))))

We can start by proving the partial product computation correct:

(def-svtv-idealized-thm boothpipe-pp-correct :input-vars (a b) :output-vars (pp0 pp1 pp2 pp3 pp4 pp5 pp6 pp7) :concl (and (equal pp0 (boothpipe-pp-spec 16 0 a b)) (equal pp1 (boothpipe-pp-spec 16 1 a b)) (equal pp2 (boothpipe-pp-spec 16 2 a b)) (equal pp3 (boothpipe-pp-spec 16 3 a b)) (equal pp4 (boothpipe-pp-spec 16 4 a b)) (equal pp5 (boothpipe-pp-spec 16 5 a b)) (equal pp6 (boothpipe-pp-spec 16 6 a b)) (equal pp7 (boothpipe-pp-spec 16 7 a b))))

This form expands to an encapsulate that first proves the following lemma using FGL -- a typical bit-blasting proof similar to those in proofs-with-stvs:

(fgl::def-fgl-thm boothpipe-pp-correct-override-lemma (implies (and (unsigned-byte-p 16 a) (unsigned-byte-p 16 b) t) (b* ((run (svtv-run (boothpipe-run) (append (list (cons 'en 1)) (list (cons 'a a) (cons 'b b)) 'nil (list) (list)) :include '(pp0 pp1 pp2 pp3 pp4 pp5 pp6 pp7))) ((svassocs pp0 pp1 pp2 pp3 pp4 pp5 pp6 pp7) run)) (and (integerp pp0) (integerp pp1) (integerp pp2) (integerp pp3) (integerp pp4) (integerp pp5) (integerp pp6) (integerp pp7) (and (equal pp0 (boothpipe-pp-spec 16 0 a b)) (equal pp1 (boothpipe-pp-spec 16 1 a b)) (equal pp2 (boothpipe-pp-spec 16 2 a b)) (equal pp3 (boothpipe-pp-spec 16 3 a b)) (equal pp4 (boothpipe-pp-spec 16 4 a b)) (equal pp5 (boothpipe-pp-spec 16 5 a b)) (equal pp6 (boothpipe-pp-spec 16 6 a b)) (equal pp7 (boothpipe-pp-spec 16 7 a b)))))))

This lemma is used to prove a much more general result about the ideal:

(defthm boothpipe-pp-correct (b* (((svassocs a b en) env) (run (svtv-spec-run (boothpipe-ideal) env :base-ins base-ins :initst initst)) ((svassocs) run)) (implies (and (svtv-override-triplemaplist-envs-match (boothpipe-run-triplemaplist) env 'nil) (and (unsigned-byte-p 16 a) (unsigned-byte-p 16 b) t) (equal en 1) (svarlist-override-p (svex-envlist-all-keys base-ins) nil)) (b* (((svassocs pp0 pp1 pp2 pp3 pp4 pp5 pp6 pp7) run)) (and (equal pp0 (boothpipe-pp-spec 16 0 a b)) (equal pp1 (boothpipe-pp-spec 16 1 a b)) (equal pp2 (boothpipe-pp-spec 16 2 a b)) (equal pp3 (boothpipe-pp-spec 16 3 a b)) (equal pp4 (boothpipe-pp-spec 16 4 a b)) (equal pp5 (boothpipe-pp-spec 16 5 a b)) (equal pp6 (boothpipe-pp-spec 16 6 a b)) (equal pp7 (boothpipe-pp-spec 16 7 a b)))))) :hints (("Goal" :use ((:instance boothpipe-ideal-refines-boothpipe-run (spec-pipe-env env) (spec-base-ins base-ins) (spec-initst initst) (pipe-env (b* ((?run (svtv-spec-run (boothpipe-ideal) env :base-ins base-ins :initst initst)) ((svassocs) run) ((svassocs a b) env)) (append (list (cons 'en 1)) (list (cons 'a a) (cons 'b b)) 'nil (list) (list))))) (:instance boothpipe-pp-correct-override-lemma (a (svex-env-lookup 'a env)) (b (svex-env-lookup 'b env)))) :in-theory (e/d** ((:rewrite svarlist-p-of-boothpipe-run-input-vars) (:ruleset svtv-idealized-thm-rules))) :do-not '(generalize fertilize eliminate-destructors) :do-not-induct t)) :rule-classes :rewrite)

Notes: First,

(b* (((svassocs a b en) env) ...) ...)

expands to approximately

(let* ((a (svex-env-lookup 'a env)) (b (svex-env-lookup 'b env)) (en (svex-env-lookup 'en env)) ...) ...)

Second, there are two special hypotheses:

(SVTV-OVERRIDE-TRIPLEMAPLIST-ENVS-MATCH (BOOTHPIPE-RUN-TRIPLEMAPLIST) ENV 'NIL) (SVARLIST-OVERRIDE-P (SVEX-ENVLIST-ALL-KEYS BASE-INS) NIL)

The first says that in the environment, there are no conditional override test variables set to 1s -- i.e., no signals defined as conditional overrides are actually overridden. The second says that the base-ins, which can be used to set FSM input signals that aren't stimulated by the SVTV, doesn't set any overrides.

Third, note that

Next we can similarly prove the sum of partial products correct:

(def-svtv-idealized-thm boothpipe-sum-correct :override-vars (pp0 pp1 pp2 pp3 pp4 pp5 pp6 pp7) :output-vars (o) :concl (b* ((- (cw "o: ~s0~%" (hexify o))) (res (loghead 32 (+ (ash (logext 18 pp0) 0) (ash (logext 18 pp1) 2) (ash (logext 18 pp2) 4) (ash (logext 18 pp3) 6) (ash (logext 18 pp4) 8) (ash (logext 18 pp5) 10) (ash (logext 18 pp6) 12) (ash (logext 18 pp7) 14)))) (- (cw "res: ~s0~%" (hexify res)))) (equal o res)))

Here, the FGL lemma has an additional wrinkle in that it overrides the partial products:

(fgl::def-fgl-thm boothpipe-sum-correct-override-lemma (implies (and (unsigned-byte-p 18 pp0) (unsigned-byte-p 18 pp1) (unsigned-byte-p 18 pp2) (unsigned-byte-p 18 pp3) (unsigned-byte-p 18 pp4) (unsigned-byte-p 18 pp5) (unsigned-byte-p 18 pp6) (unsigned-byte-p 18 pp7) t) (b* ((run (svtv-run (boothpipe-run) (append (list (cons 'en 1)) (list) '((pp0-ovr . -1) (pp1-ovr . -1) (pp2-ovr . -1) (pp3-ovr . -1) (pp4-ovr . -1) (pp5-ovr . -1) (pp6-ovr . -1) (pp7-ovr . -1)) (list) (list (cons 'pp0 pp0) (cons 'pp1 pp1) (cons 'pp2 pp2) (cons 'pp3 pp3) (cons 'pp4 pp4) (cons 'pp5 pp5) (cons 'pp6 pp6) (cons 'pp7 pp7))) :include '(o))) ((svassocs o) run)) (and (integerp o) (b* ((- (cw "o: ~s0~%" (hexify o))) (res (loghead 32 (+ (ash (logext 18 pp0) 0) (ash (logext 18 pp1) 2) (ash (logext 18 pp2) 4) (ash (logext 18 pp3) 6) (ash (logext 18 pp4) 8) (ash (logext 18 pp5) 10) (ash (logext 18 pp6) 12) (ash (logext 18 pp7) 14)))) (- (cw "res: ~s0~%" (hexify res)))) (equal o res))))))

The final theorem proved by the

We now have two rewrite rules that will be useful in our final theorem: one
expresses the final output

(defthm booth-sum-of-products-correct (implies (and (natp a) (natp b) (< a (expt 2 16)) (< b (expt 2 16))) (let ((pp0 (boothpipe-pp-spec 16 0 a b)) (pp1 (boothpipe-pp-spec 16 1 a b)) (pp2 (boothpipe-pp-spec 16 2 a b)) (pp3 (boothpipe-pp-spec 16 3 a b)) (pp4 (boothpipe-pp-spec 16 4 a b)) (pp5 (boothpipe-pp-spec 16 5 a b)) (pp6 (boothpipe-pp-spec 16 6 a b)) (pp7 (boothpipe-pp-spec 16 7 a b))) (equal (+ (ash (logext 18 pp0) 0) (ash (logext 18 pp1) 2) (ash (logext 18 pp2) 4) (ash (logext 18 pp3) 6) (ash (logext 18 pp4) 8) (ash (logext 18 pp5) 10) (ash (logext 18 pp6) 12) (ash (logext 18 pp7) 14)) (* (logext 16 a) (logext 16 b))))) :hints (("goal" :use ((:instance booth-sum-impl-is-multiply (n 8) (sz 16))) :in-theory (e/d nil (booth-sum-impl-is-multiply ash logext logapp loghead signed-byte-p boothpipe-pp-spec)))))

This can now be used to prove our top-level theorem. We can do this with
another

(def-svtv-idealized-thm boothpipe-correct-gen :input-vars (a b) :output-vars (o) :concl (equal o (loghead 32 (* (logext 16 a) (logext 16 b)))) :no-lemmas t)

The theorem resulting from this form:

(defthm boothpipe-correct-gen (b* (((svassocs a b en) env) (run (svtv-spec-run (boothpipe-ideal) env :base-ins base-ins :initst initst)) ((svassocs) run)) (implies (and (svtv-override-triplemaplist-envs-match (boothpipe-run-triplemaplist) env 'nil) (and (unsigned-byte-p 16 a) (unsigned-byte-p 16 b) t) (equal en 1) (svarlist-override-p (svex-envlist-all-keys base-ins) nil)) (b* (((svassocs o) run)) (equal o (loghead 32 (* (logext 16 a) (logext 16 b))))))) :rule-classes :rewrite)

This is, again, a quite general theorem. However, as a matter of taste it
might be pleasant to see a more specific version of this theorem that avoids
these complicated hypotheses, which could lead to worries that the theorem is
vacuous (i.e. there is no

(defthm boothpipe-correct (implies (and (unsigned-byte-p 16 a) (unsigned-byte-p 16 b)) (b* ((in-alist (list (cons 'a a) (cons 'b b) '(en . 1))) (out-alist (svtv-spec-run (boothpipe-ideal) in-alist)) (o (svex-env-lookup 'o out-alist))) (equal o (loghead 32 (* (logext 16 a) (logext 16 b)))))) :hints (("Goal" :in-theory (e/d (svex-env-lookup-of-cons 4vec-p-when-integerp svex-env-lookup-use-exec svex-env-keys-no-1s-p-of-variable-free-term hons-intersection-force-execute svex-env-keys-no-1s-p-of-cons) ((svex-env-lookup))))))