|
|
|---|
|
|
|
|---|
High-level description of decomposition methodology for svtvs.
In hardware verification, it is important to be able to break down proofs into pieces. An important technique for this purpose is to assume that certain internal signals have particular values at particular times, and prove something about their fanout logic. For symbolic simulation, the best performance for this method is obtained by replacing the fanin logic of these signals with free symbolic values, which we call "overriding" those signals. In order to compose together multiple proofs using this technique, it is important to be able to use a theorem proved about a design's behavior with certain signals overridden to prove a theorem about the design without (some of) those overrides.
As a high-level example, suppose we prove that the partial product summation
of a multiplier is correct by overriding the partial product signals. Note:
the following uses a made-up syntax, for illustration purposes only. In our
real framework,
(defthm multiplier-pp-sum-correct-override (implies (unsigned-byte-p 128 partial-products-value) (let* ((run (run-design (multiplier) :inputs `((opcode . ,*multiply-opcode*)) :overrides `((partial-product-signal . ,partial-products-value))))) (equal (lookup 'multiplier-output run) (pp-sum-spec partial-products-value))))) }
Additionally, suppose that we've proved that the same multiplier computes a correct Booth encoding as its partial products signal:
(defthm multiplier-booth-encoding-correct (implies (and (unsigned-byte-p 16 a) (unsigned-byte-p 16 b)) (let* ((run (run-design (multiplier) :inputs `((opcode . ,*multiply-opcode*) (a-input . ,a) (b-input . ,b))))) (equal (lookup 'partial-product-signal run) (booth-enc-spec a b)))))
We'd like to be able to compose these two theorems and prove the multiplier correct from end to end. But the design here has been run with two different settings for the inputs and overrides, and these can't be reconciled as-is. At a high level, our decomposition methodology works by allowing theorems such as these -- which are convenient to prove using symbolic simulation -- to be generalized into theorems that can be straightforwardly composed. Using the same made-up syntax:
(defthm multiplier-pp-sum-correct-gen (let* ((opcode (lookup 'opcode input-env)) (run (run-design (multiplier) :inputs input-env)) (partial-products-value (lookup 'partial-product-signal run)) (result (lookup 'multiplier-output run))) (implies (and (equal opcode *multiply-opcode*) (unsigned-byte-p 128 partial-products-value)) (equal result (pp-sum-spec partial-products-value)))))
Notice this has been changed in two ways:
The booth encoding theorem can be changed similarly, although since it had no overrides only the first change applies here:
(defthm multiplier-booth-encoding-correct-gen (let* ((opcode (lookup 'opcode input-env)) (a (lookup 'a-input input-env)) (b (lookup 'b-input input-env)) (run (run-design (multiplier) :inputs input-env)) (partial-products-value (lookup 'partial-product-signal run))) (implies (and (equal opcode *multiply-opcode*) (unsigned-byte-p 16 a) (unsigned-byte-p 16 b)) (equal partial-products-value (booth-enc-spec a b)))))
Notice that these theorems now can be composed! In fact, given a lemma about
the bit width of
(defthm multiplier-computes-pp-sum-of-booth-enc (let* ((opcode (lookup 'opcode input-env)) (a (lookup 'a-input input-env)) (b (lookup 'b-input input-env)) (run (run-design (multiplier) :inputs input-env)) (result (lookup 'multiplier-output run))) (implies (and (equal opcode *multiply-opcode*) (unsigned-byte-p 16 a) (unsigned-byte-p 16 b)) (equal result (pp-sum-spec (booth-enc-spec a b))))))
This methodology's main user interface is def-svtv-idealized-thm. See that topic for usage. In the rest of this topic we'll discuss how this works and the solutions to certain complications.
To produce the generalized forms of the theorems above, we want a particular
property of the design: that if we override a signal with the value that it
would have had anyway, then the values of all signals are preserved. Stated in
terms of our imaginary
(defthm multiplier-partial-product-overrides-correct (let* ((base-run (run-design (multiplier) :inputs input-env)) (partial-products-value (lookup 'partial-product-signal base-run)) (override-run (run-design (multiplier) :inputs input-env :overrides `((partial-product-signal . ,partial-products-value))))) (all-lookups-equivalent override-run base-run)))
This theorem, along with a couple of other simpler facts that allow the
generalization of the input environment would be sufficient to let us
generalize
Generally we also want to allow for multiple override signals in different combinations. potentially overridden signals:
(defthm multiplier-partial-product-overrides-correct (let* ((base-run (run-design (multiplier) :inputs input-env)) (override-run (run-design (multiplier) :inputs input-env :overrides override-env))) (implies (override-signals-consistent-with-base-run override-env base-run) (all-lookups-equivalent override-run base-run))))
Here we imagine
This overrides-correct condition seems intuitively obvious and we would like to prove it for all designs. However, it is actually a fairly deep property of the design object, and as we'll see, depending how we compose the design together it may or may not be true.
The problematic cases have to do with designs where there are 0-delay combinational loops. These can occur due to latch-based logic or clock gating logic, often enough that it isn't workable to just disallow them.
The correct way to deal with 0-delay combinational loops is to compute a
fixpoint. That is, for a given setting of the circuit inputs and
stateholding elements, begin at a state setting these values for the
inputs/states and all internal signals set to X. Apply the internal signals'
update functions to obtain a new state. Repeat this until we reach a fixpoint.
It is a theorem that if all signals have finite bit widths and the update
functions respect X-monotonicity, then a fixpoint is reached by the time we
have repeated this
Because of the number of repetitions needed, it isn't always practical to actually compute the fixpoint. Instead we use an approximate composition method that is efficient, practially useful, and conservative with respect to the fixpoint: that is, if a signal's value in this approximate composition is non-X, then its fixpoint value must be the same.
The approximate composition does not always satisfy the overrides-correct condition above. For example, if we override a signal that is part of a 0-delay combinational loop and its fanin logic therefore appears more than once in different forms (composed with itself a different number of times), then overriding all occurrences of that fanin logic with the signal's final value isn't guaranteed to preserve the value of other signals.
However, the overrides-correct condition is true of the fixpoint. One
version of this is proved in "centaur/sv/svex/fixpoint-override" as
This leads us to the following methodology for composing hardware proofs with overrides: