Verification of a multiplier: 64 bits and beyond

This work shows how to verify a 64-bit multiplier by applying COSPAN, a model-checking algorithm, to verify local properties of the complex low-level circuit, and using TLP, a theorem prover based on the Temporal Logic of Actions, to prove that these properties imply the correctness of the multiplier.

Abstract

Verifying a 64-bit multiplier has a computational complexity that puts it beyond the grasp of current finite-state algorithms, including those based upon homomorphic reduction, the induction principle, and bdd fixed-point algorithms. Theorem proving, while not bound by the same computational constraints, may not be feasible for routinely coping with the complex, low-level details of a real multiplier. We show how to verify such a multiplier by applying COSPAN, a model-checking algorithm, to verify local properties of the complex low-level circuit, and using TLP, a theorem prover based on the Temporal Logic of Actions, to prove that these properties imply the correctness of the multiplier. Both verification steps are automated, and we plan to mechanize the translation between the languages of TLP and COSPAN.