		Search-engine friendly clone of the ACL2 documentation.

Sv-tutorial

Decomposition-proofs

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.

STV Setup for Decomposition

In the boothpipe example, the intermediate signals to split the pipeline on are the partial products pp0...pp7. We'll have one SVTV that says how to run the whole module, whether we're decomposing on the partial products or not. For each of the partial products, this SVTV will both conditionally override the signal and provide an output signal that produces the un-overridden value:

(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 :overrides listed in the c2 phase gives the override value variable, override condition variable, and output variable for one of the partial products. For example, the first entry:

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

says pp01_c2[35:18] is overriden with the value of input variable pp0 when corresponding bits of input variable pp0-ovr are set to 1. Additionally, output variable pp0 is assigned the un-overridden value of pp01_c2[35:18]. Since input variables and output variables of SVTVs are treated as separate namespaces, it is OK (and somewhat conventional) for the override value (input) variable and corresponding output variable for the same signal to be the same.

Composing the Proof

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.

Conditional Override Elimination

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 boothpipe-ideal which is the object that we'll prove our composable theorems about, even though we can't execute it. It also produces a function boothpipe-ideal-exec that (logically) extracts certain output signals from a run of boothpipe-ideal -- but since boothpipe-ideal isn't executable, it actually uses boothpipe-run to compute what must be the values of those varibles.

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 def-svtv-idealized-thm invocations in this book: these forms say which SVTV we're using, the name of the SVTV's corresponding ideal, to assume by default that all input and override variables used are appropriate-sized unsigned bytes, and to assume the enable signal is 1.

(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))
   (progn$
    (and
     (or
      (and (integerp pp0)
           (integerp pp1)
           (integerp pp2)
           (integerp pp3)
           (integerp pp4)
           (integerp pp5)
           (integerp pp6)
           (integerp pp7))
      (progn$
        (cw "*** Failed: Some output variables contained Xes/Zs:~%")
        (svtv-print-alist-readable
             (svex-env-extract-non-2vecs
                  '(pp0 pp1 pp2 pp3 pp4 pp5 pp6 pp7)
                  run))
        nil))
     (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, svassocs is a b* binder that binds the variables listed to svex-env-lookups of the bound object -- e.g.,

(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 boothpipe-pp-correct is much more generally applicable as a set of rewrite rules than boothipe-pp-correct-override-lemma or any usual bitblasting theorem of the form discussed in proofs-with-stvs. The second argument to svtv-run in this theorem is just a variable env with some hypotheses about it, whereas in a typical bitblasting theorem it would be expressed as an alist of a specific shape with some symbolic values bound to concrete keys. This is what allows this theorem to be composed with others much more easily. The lemmas proved in the def-svtv-override-thms form allow the FGL lemma to be idealized into this form.

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))
   (progn$
    (and
     (or
      (and (integerp o))
      (progn$
        (cw "*** Failed: Some output variables contained Xes/Zs:~%")
        (svtv-print-alist-readable
             (svex-env-extract-non-2vecs '(o) run))
        nil))
     (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 def-svtv-idealized-thm form, however, eliminates these overrides. It again has the svtv-override-triplemaplist-envs-match and svarlist-override-p hypotheses, but extracts the partial products from the outputs of the svtv-run instead of providing them as an override in the input environment. That is, instead of a theorem \"If you run the SVTV with PPs overridden, output o is related to the override values\" we instead have a theorem \"If you run the ideal with no overrides, output o is related to the values of the PPs.\" This again is much easier to compose, because we can easily describe an svtv-run which satisfies the hypotheses of both boothpipe-pp-correct and boothpipe-sum-correct simultaneously.

We now have two rewrite rules that will be useful in our final theorem: one expresses the final output o of the ideal as the sum of the pp outputs, and the other expresses the pp outputs of the ideal as the correct Booth partial products for the inputs a and b. We want to use these to show that o is the multiplication of a and b. So we first need a theorem showing that the sum of the Booth partial products is multiplication. Note that this has nothing to do with the hardware design; it's purely an ACL2 arithmetic theorem:

(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 form, this time with the :no-lemmas t argument, which directs it to prove the idealized theorem directly with ACL2 rather than first proving an FGL lemma:

(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 env satisfying the hypotheses). The following theorem essentially specifies a class of environment that does satisfy the hypotheses:

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

Subtopics

Boothpipe-run