Abstract
Serial data-path circuits are often more difficult to analyze than their parallel counterparts. The major reason is data and operations are spread over time. Here the strength of formal verification is demonstrated with verification of classical serial pipeline multipliers. The designer's informal notions of how to interpret the design are formally captured in well-defined functions and standard mathematical notation. A linear-time temporal logic is found to be useful for analyzing such circuits; temporal operators are succinct in expressing certain operating conditions that are otherwise verbose, and temporal laws and operators enable us to work more efficiently in a higher level of reasoning.
This work was supported by the NY State Center for Advanced Technology in Computer Applications and Software Engineering (CASE) at Syracuse University. The authors are grateful to Anand Chavan for his help with the GDT tools for getting layouts and simulations for this work.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Henry S. McDonald, Leland B. Jackson, James F. Kaiser, “An approach to the implementation of digital filters,” IEEE Trans. on Audio and Electroacoustics, AU-16(3):413–421, Sept 1968.
R. F. Lyon, “Two's complement pipeline multipliers,” IEEE Transactions on Communications, pages 418–425, April 1976.
Shiu-Kai Chin, Juin-Yeu Lu, “The mechanical verification and synthesis of parameterized serial/parallel multiplier,” Technical Report 9140, CASE Center, Syracuse University, 1991.
Shiu-Kai Chin, “Verified Functions for Generating Signed-Binary Arithmetic Hardware,” IEEE Trans. Computer-Aided Design, pages 1529–1558, December 1992.
Amir Pnueli, Zohar Manna, The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag, 1992.
Michael J.C. Gordon, “Why higher-order logic is a good formalism for specifying and verifying hardware,” In G. J. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design, pages 153–177. Elsevier Scientific Publishers, 1986.
Wai Wong, “Modelling bit vectors in HOL: the word library,” Proc. of 6th Intl. HOL Users Group Workshop 1993, Vancouver, B.C, Canada, August 1993, Springer-Verlag, New York, 1994.
J. Y. Lu, S. K. Chin, “Linking HOL to a VLSI CAD system,” Higher Order Logic Theorem Proving and Its Applications, Lecture Notes in Computer Science 780, Springer-Verlag, Berlin Heidelberg 1994.
Mentor Graphics Inc., GDT Led, Lx Standard Cell, Explorer Lsim V.5.3 users manuals, San Jose, CA, 1990.
Mentor Graphics Inc., Explorer AutoCells Users Guide, San Jose, CA, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kim, J.D., Chin, SK. (1995). Formal verification of serial pipeline multipliers. In: Thomas Schubert, E., Windley, P.J., Alves-Foss, J. (eds) Higher Order Logic Theorem Proving and Its Applications. TPHOLs 1995. Lecture Notes in Computer Science, vol 971. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60275-5_68
Download citation
DOI: https://doi.org/10.1007/3-540-60275-5_68
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60275-0
Online ISBN: 978-3-540-44784-9
eBook Packages: Springer Book Archive