Mechanically verifying a family of multiplier circuits

Deepak Kapur, M. Subramaniam

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

15 Scopus citations

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 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
Pages135-146
Number of pages12
ISBN (Print)3540614745, 9783540614746
DOIs
Publication statusPublished - Jan 1 1996
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)
Volume1102
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th International Conference on Computer Aided Verification, CAV 1996
CountryUnited States
CityNew Brunswick
Period7/31/968/3/96

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Kapur, D., & Subramaniam, M. (1996). Mechanically verifying a family of multiplier circuits. In T. A. Henzinger, & R. Alur (Eds.), Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings (pp. 135-146). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1102). Springer Verlag. https://doi.org/10.1007/3-540-61474-5_64