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.
CITATION STYLE
Kurshan, R. P., & Lamport, L. (1993). Verification of a multiplier: 64 Bits and beyond. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 697 LNCS, pp. 166–179). Springer Verlag. https://doi.org/10.1007/3-540-56922-7_14
Mendeley helps you to discover research relevant for your work.