Abstract
A methodology for mechanically verifying a family of parameterized multiplier circuits, including many well-known multiplier circuits such as the linear array, the Wallace tree and the 7-3 multiplier is proposed. A top level specification for these multipliers is obtained by abstracting the commonality in their behavior. The behavioral correctness of any multiplier in the family can be mechanically verified by a uniform proof strategy. Proofs of properties are done by rewriting and induction using an automated theorem prover RRL (Rewrite Rule Laboratory). The behavioral correctness of the circuits is established with respect to addition and multiplication on numbers. The automated proofs involve minimal user intervention in terms of intermediate lemmas required. Generic hardware components are used to segregate the specification and the implementation aspects, enabling verification of circuits in terms of behavioral constraints that can be realized in different ways. The use of generic components aids reuse of proofs and helps modularize the correctness proofs, allowing verification to go hand in hand with the hardware design process in a hierarchical fashion.
Partially supported by the National Science Foundation Grant no. CCR-9308016.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R.S. Boyer and J. Moore, A Computational Logic Handbook. New York: Academic Press, 1988.
R.S. Boyer, J. Moore and M. Kaufmann “Functional Instantiation in Nqthm”, CLI Inc. Tech. Report.
Bryant R.E., “Graph-based Algorithms for boolean function manipulation”, IEEE trans. on Computers, C-35(8), 1986.
R. E. Bryant, and Y.-A. Chen, ”Verification of Arithmetic Functions with Binary Moment Diagrams”, Tech. Rep. CMU-CS-94-160, June 1994.
J. R. Burch, E.M. Clarke, K. L. Mcmillan and D.L. Dill, “Sequential Circuit Verification using symbolic model checking”, in proceedings of Twenty seventh ACM/IEEE Design Automation Conference, 1990.
A.J. Camilleri, M.J.C. Gordon and T.F. Melham, “Hardware verification using higher-order logic””, HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione (editor) pp. 43–67, N.Holland, Amsterdam 1987.
L. Dadda “Some Schemes for parallel multipliers,” in Computer Arithmetic Vol. I, E.E. Swartzlander Jr. (editor), IEEE Computer Society Press, 1990.
W.A. Hunt., “FM8501: A verified Microprocessor”, Ph.D thesis, UT Austin, 1985.
R.K.Montoye, E. Hokenek and S.L.Runyon, “Design of the IBM RISC System/6000 floating-point execution unit,” IBM Journal, Vol. 34, No. 1, 1990.
”Theorem Provers in circuit design”, IFIP Transactions, V. Stavridou, T.F. Melham, R.T.Boute (eds.) N.Holland 1992.
J. Joyce, G. Birtwistle and M. Gordon, “Proving a computer correct in HOL”, Tech. Report 100, Computer Lab. University of Cambridge 1986.
D. Kapur and M. Subramaniam, “Mechanical Verification of Adder Circuits Using Powerlists,” CS.Tech. Report, Dept. of CS Suny Albany, November 1995.
R.P. Kurhshan, L. Lamport, “Verification of a Multiplier: 64 Bits and Beyond,” Fifth Intl. Conf. on CAV, C. Courcoubetis (editor), LNCS 697, July 1993.
L. Pierre, “VHDL Description and Formal Verification of Systolic Multipliers,” in Proc. of CHDL, D. Agnew and L. Claesea (eds.) N. Holland 1993.
D. Kapur, and H. Zhang, “An overview of Rewrite Rule Laboratory (RRL),” J. of Computer and Mathematics with Applications, 29, 2, 1995, 91–114.
D. Cyrluk and S. Rajan and N. Shankar and M. K. Srivas, “Effective Theorem Proving for Hardware Verification”, Proc, 2nd conference on theorem provers in circuit design, R. Kumar and T. Kropf (eds.), Sept. 1994.
M. Srivas and M. Bickford, “Formal Verification of a pipelined microprocessor.”, IEEE Software, Sept. 1990.
Shui-Kai Chin, “Verified Functions for Generating Signed-Binary Arithmetic Hardware”, IEEE trans. on Computer Aided Design, Vol. 11, No. 12, Dec. 1992.
D. Verkest, L. Claesen, and H. De Man, “Correctness Proofs of Parameterized Hardware Modules in the Cathedral-II Synthesis Environment”, EDAC '90, Glasgow, Scotland, March 1990.
C.S. Wallace, “A Suggestion for a fast multiplier,” in IEEE Trans. Electron. Comput., EC-13. 14–17, 1964.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kapur, D., Subramaniam, M. (1996). Mechanically verifying a family of multiplier circuits. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_64
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_64
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive