Mechanically verifying a family of multiplier circuits

Deepak Kapur, Mahadevan Subramaniam

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

15 Citations (Scopus)

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 publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Pages135-146
Number of pages12
Volume1102
ISBN (Print)3540614745, 9783540614746
DOIs
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)
Volume1102
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Multiplier
Networks (circuits)
Correctness
Specifications
Hardware
Specification
Linear Array
Hardware Design
Rewriting
Design Process
Reuse
Lemma
Proof by induction
Multiplication
Family
Methodology
Theorem

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Kapur, D., & Subramaniam, M. (1996). Mechanically verifying a family of multiplier circuits. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1102, 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

Mechanically verifying a family of multiplier circuits. / Kapur, Deepak; Subramaniam, Mahadevan.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 1102 Springer Verlag, 1996. p. 135-146 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1102).

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

Kapur, D & Subramaniam, M 1996, Mechanically verifying a family of multiplier circuits. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 1102, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1102, Springer Verlag, pp. 135-146, 8th International Conference on Computer Aided Verification, CAV 1996, New Brunswick, United States, 7/31/96. https://doi.org/10.1007/3-540-61474-5_64
Kapur D, Subramaniam M. Mechanically verifying a family of multiplier circuits. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 1102. Springer Verlag. 1996. p. 135-146. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-61474-5_64
Kapur, Deepak ; Subramaniam, Mahadevan. / Mechanically verifying a family of multiplier circuits. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 1102 Springer Verlag, 1996. pp. 135-146 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{0e7afe865faa49dab3041bb5dcafc140,
title = "Mechanically verifying a family of multiplier circuits",
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.",
author = "Deepak Kapur and Mahadevan Subramaniam",
year = "1996",
doi = "10.1007/3-540-61474-5_64",
language = "English (US)",
isbn = "3540614745",
volume = "1102",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "135--146",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Mechanically verifying a family of multiplier circuits

AU - Kapur, Deepak

AU - Subramaniam, Mahadevan

PY - 1996

Y1 - 1996

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

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

UR - http://www.scopus.com/inward/record.url?scp=84957366809&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84957366809&partnerID=8YFLogxK

U2 - 10.1007/3-540-61474-5_64

DO - 10.1007/3-540-61474-5_64

M3 - Conference contribution

SN - 3540614745

SN - 9783540614746

VL - 1102

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 135

EP - 146

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer Verlag

ER -