Verification of a Multiplier: 64 Bits and Beyond

As I observed in [124], verifying a system by first decomposing it into separate subsystems can’t reduce the size of a proof and usually increases it. However, such a decomposition can reduce the amount of effort if it allows much of the resulting proof to be done automatically by a model checker. This paper shows how the decomposition theorem of [112] can be used to decompose a hardware component (in this case, a multiplier) that is too large to be verified by model checking alone. Here is Kurshan’s recollection of how this paper came to be. My CAV’92 talk was mostly about [101], and the “Larch support” refers to [96]

I cornered you after your invited address at CAV92. At CAV, you talked about indenting (and TLA, and its Larch support). I challenged you with a matter I had been thinking about since at least 1990, the year of the first CAV. In the preface to the CAV90 proceedings, I stated as a paramount challenge to the CAV community, to create a beneficial interface between automated theorem proving, and model checking.

I asked you if you thought that linking TLA/Larch with S/R (which should be simple to do on account of their very close syntax and semantics for finite-state models), could be useful. I suggested the (artificial) problem of verifying a multiplier constructed from iterated stages of a very complex 8×8 multiplier. The 8×8 multiplier would be too complex to verify handily with a theorem prover. A (say) 64×64 multiplier could be built from the 8×8 one. We’d use the model checker (cospan) to verify the 8×8, and Larch/TLA to verify the induction step. You liked the idea, and we did it, you working with Urban and I working with Mark [Foissoitte].

Sadly, with the interface in place, I was unable to come up with a non-artificial feasible application. To this day, although there have been a succession of such interfaces built (I believe ours was the first), none has really demonstrated a benefit on a real application. The (revised) challenge is to find an application in which the combination finds a bug faster than either one could by itself.