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.
Chapter PDF
References
Martin Abadi and Leslie Lamport. Open systems. To appear in 1993 as a SRC Research Report.
Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions On Computers, C-35(8):677–691, August 1986.
Shiu-Kai Chin. Verified functions for generating signed-binary arithmetic hardware. IEEE Transactions on Computer-Aided Design, 11(12):1529–1558, December 1992.
Urban Engberg, Peter Grønning, and Leslie Lamport. Mechanical verification of concurrent systems with TLA. In Computer-Aided Verification, Lecture Notes in Computer Science, Berlin, Heidelberg, New York, June 1992. Springer-Verlag. Proceedings of the Fourth International Conference, CAV'92.
Z. Har'El and R. P. Kurshan. Software for analytical development of communication protocols. AT&T Technical Journal, 69(1):44–59, 1990.
J. Katzenelson and R. P. Kurshan. S/R: A language for specifying protocols and other coordinating processes. In Proceedings of the 5th Annual International Phoenix Conference on Computer Communications, pages 286–292, Scottsdale, Arizona, 1986. IEEE Computer Society.
Israel Koren. Computer Arithmetic Algorithms. Prentice Hall, Englewood Cliffs, New Jersey, 1993.
R. P. Kurshan. Reducibility in analysis of coordination. In P. Varaiya and A.B. Kurzhanski, editors, Discrete Event Systems: Models and Applications, volume 103 of Lecture Notes in Control and Information Sciences, pages 19–39, Berlin, 1987. Springer-Verlag.
R. P. Kurshan. Analysis of discrete event coordination. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science, pages 414–453. Springer-Verlag, May/June 1989.
R. P. Kurshan and K. McMillan. A structural induction theorem for processes. In Proceedings of the 8th annual ACM Symposium on Principles of Distributed Computing, pages 239–247. ACM Press, 1989.
Leslie Lamport. What good is temporal logic? In R. E. A. Mason, editor, Information Processing 83: Proceedings of the IFIP 9th World Congress, pages 657–668, Paris, September 1983. IFIP, North-Holland.
Leslie Lamport. The temporal logic of actions. Research Report 79, Digital Equipment Corporation, Systems Research Center, December 1991.
Leslie Lamport. Hybrid systems in TLA+. In Hans Rischel and Anders P. Ravn, editors, Hybrid Systems, Lecture Notes in Computer Science, Berlin, 1993. Springer-Verlag. Proceedings of a Workshop on Hybrid Systems, to appear.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kurshan, R.P., Lamport, L. (1993). Verification of a multiplier: 64 bits and beyond. In: Courcoubetis, C. (eds) Computer Aided Verification. CAV 1993. Lecture Notes in Computer Science, vol 697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56922-7_14
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56922-0
Online ISBN: 978-3-540-47787-7
eBook Packages: Springer Book Archive