Mechanically verifying a family of multiplier circuits

Deepak Kapur, M. Subramaniam

Research output: Chapter in Book/Report/Conference proceedingConference contribution

17 Scopus citations


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 axe 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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 8th International Conference, CAV 1996, Proceedings
EditorsThomas A. Henzinger, Rajeev Alur
PublisherSpringer Verlag
Number of pages12
ISBN (Print)3540614745, 9783540614746
StatePublished - 1996
Externally publishedYes
Event8th International Conference on Computer Aided Verification, CAV 1996 - New Brunswick, United States
Duration: Jul 31 1996Aug 3 1996

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other8th International Conference on Computer Aided Verification, CAV 1996
Country/TerritoryUnited States
CityNew Brunswick

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Mechanically verifying a family of multiplier circuits'. Together they form a unique fingerprint.

Cite this