Mechanical verification of adder circuits using rewrite rule laboratory

Deepak Kapur, Mahadevan Subramaniam

Research output: Contribution to journalArticle

22 Citations (Scopus)

Abstract

A methodology for mechanically verifying generic adder circuits is proposed using the rewrite-rule based theorem prover Rewrite Rule Laboratory (RRL). Proofs of properties of adder circuit descriptions are done by rewriting and induction. Carry lookahead adder circuit is described using powerlists, a data structure introduced by Misra to support divide-and-conquer strategy used for designing data-parallel algorithms. This description uses an algorithm for parallel prefix computation on powerlists due to Adams. Reasoning about properties of this algorithm can be of independent interest since parallel prefix operator has been found useful in many data-parallel algorithms. The correctness of the carry-lookahead adder (i.e., the adder indeed implements addition on numbers) is established by showing its equivalence to a recursive description of the ripple-carry adder, which is shown to correctly implement addition on natural numbers. The ripple carry adder circuit is described in two different but equivalent ways: using powerlists employing the divide-and-conquer strategy, as well as using linear lists employing the linear decomposition strategy. The description of the ripple carry adder using powerlists is useful for showing equivalence of its input-output behavior to that of carry lookahead adder, whereas the description using linear lists is useful for showing its correctness with respect to addition on natural numbers. Descriptions of adder circuits using powerlists are based on Adams' work who also gave a hand proof of their correctness using the powerlist algebra. The emphasis in this paper is to generate proofs mechanically by a theorem prover. RRL exploits the algebraic laws of the powerlist algebra as rewrite rules, and uses heuristics for mechanizing proofs by induction using the cover set method to generate such proofs. The regularity in hardware circuits gets reflected in compact descriptions generated using the divide-and-conquer strategy as well as in mechanically generated proofs by induction. Mechanical proofs generated by RRL closely follow the well-crafted hand-proofs which is quite encouraging. A comparison with Adams' hand generated proof is also made. There is strong evidence that the proposed methodology for generating proofs should scale up for large circuits exhibiting regularity that can be described using divide-and-conquer strategy in terms of powerlists.

Original languageEnglish (US)
Pages (from-to)127-158
Number of pages32
JournalFormal Methods in System Design
Volume13
Issue number2
DOIs
StatePublished - Sep 1 1998

Fingerprint

Adders
Divide and conquer
Networks (circuits)
Look-ahead
Ripple
Proof by induction
Prefix
Natural number
Parallel Algorithms
Correctness
Regularity
Equivalence
Parallel algorithms
Algebra
Proof of correctness
Set Cover
Scale-up
Methodology
Rewriting
Theorem

Keywords

  • Automatic verification
  • Carry lookahead adder
  • Divide and conquer
  • Formal verification
  • Generic adders
  • Parallel prefix
  • Powerlists
  • Proof by induction
  • Ripple carry adder

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture

Cite this

Mechanical verification of adder circuits using rewrite rule laboratory. / Kapur, Deepak; Subramaniam, Mahadevan.

In: Formal Methods in System Design, Vol. 13, No. 2, 01.09.1998, p. 127-158.

Research output: Contribution to journalArticle

@article{cccd47021d9c4cca83ac6a4c7d15265c,
title = "Mechanical verification of adder circuits using rewrite rule laboratory",
abstract = "A methodology for mechanically verifying generic adder circuits is proposed using the rewrite-rule based theorem prover Rewrite Rule Laboratory (RRL). Proofs of properties of adder circuit descriptions are done by rewriting and induction. Carry lookahead adder circuit is described using powerlists, a data structure introduced by Misra to support divide-and-conquer strategy used for designing data-parallel algorithms. This description uses an algorithm for parallel prefix computation on powerlists due to Adams. Reasoning about properties of this algorithm can be of independent interest since parallel prefix operator has been found useful in many data-parallel algorithms. The correctness of the carry-lookahead adder (i.e., the adder indeed implements addition on numbers) is established by showing its equivalence to a recursive description of the ripple-carry adder, which is shown to correctly implement addition on natural numbers. The ripple carry adder circuit is described in two different but equivalent ways: using powerlists employing the divide-and-conquer strategy, as well as using linear lists employing the linear decomposition strategy. The description of the ripple carry adder using powerlists is useful for showing equivalence of its input-output behavior to that of carry lookahead adder, whereas the description using linear lists is useful for showing its correctness with respect to addition on natural numbers. Descriptions of adder circuits using powerlists are based on Adams' work who also gave a hand proof of their correctness using the powerlist algebra. The emphasis in this paper is to generate proofs mechanically by a theorem prover. RRL exploits the algebraic laws of the powerlist algebra as rewrite rules, and uses heuristics for mechanizing proofs by induction using the cover set method to generate such proofs. The regularity in hardware circuits gets reflected in compact descriptions generated using the divide-and-conquer strategy as well as in mechanically generated proofs by induction. Mechanical proofs generated by RRL closely follow the well-crafted hand-proofs which is quite encouraging. A comparison with Adams' hand generated proof is also made. There is strong evidence that the proposed methodology for generating proofs should scale up for large circuits exhibiting regularity that can be described using divide-and-conquer strategy in terms of powerlists.",
keywords = "Automatic verification, Carry lookahead adder, Divide and conquer, Formal verification, Generic adders, Parallel prefix, Powerlists, Proof by induction, Ripple carry adder",
author = "Deepak Kapur and Mahadevan Subramaniam",
year = "1998",
month = "9",
day = "1",
doi = "10.1023/A:1008610818519",
language = "English (US)",
volume = "13",
pages = "127--158",
journal = "Formal Methods in System Design",
issn = "0925-9856",
publisher = "Springer Netherlands",
number = "2",

}

TY - JOUR

T1 - Mechanical verification of adder circuits using rewrite rule laboratory

AU - Kapur, Deepak

AU - Subramaniam, Mahadevan

PY - 1998/9/1

Y1 - 1998/9/1

N2 - A methodology for mechanically verifying generic adder circuits is proposed using the rewrite-rule based theorem prover Rewrite Rule Laboratory (RRL). Proofs of properties of adder circuit descriptions are done by rewriting and induction. Carry lookahead adder circuit is described using powerlists, a data structure introduced by Misra to support divide-and-conquer strategy used for designing data-parallel algorithms. This description uses an algorithm for parallel prefix computation on powerlists due to Adams. Reasoning about properties of this algorithm can be of independent interest since parallel prefix operator has been found useful in many data-parallel algorithms. The correctness of the carry-lookahead adder (i.e., the adder indeed implements addition on numbers) is established by showing its equivalence to a recursive description of the ripple-carry adder, which is shown to correctly implement addition on natural numbers. The ripple carry adder circuit is described in two different but equivalent ways: using powerlists employing the divide-and-conquer strategy, as well as using linear lists employing the linear decomposition strategy. The description of the ripple carry adder using powerlists is useful for showing equivalence of its input-output behavior to that of carry lookahead adder, whereas the description using linear lists is useful for showing its correctness with respect to addition on natural numbers. Descriptions of adder circuits using powerlists are based on Adams' work who also gave a hand proof of their correctness using the powerlist algebra. The emphasis in this paper is to generate proofs mechanically by a theorem prover. RRL exploits the algebraic laws of the powerlist algebra as rewrite rules, and uses heuristics for mechanizing proofs by induction using the cover set method to generate such proofs. The regularity in hardware circuits gets reflected in compact descriptions generated using the divide-and-conquer strategy as well as in mechanically generated proofs by induction. Mechanical proofs generated by RRL closely follow the well-crafted hand-proofs which is quite encouraging. A comparison with Adams' hand generated proof is also made. There is strong evidence that the proposed methodology for generating proofs should scale up for large circuits exhibiting regularity that can be described using divide-and-conquer strategy in terms of powerlists.

AB - A methodology for mechanically verifying generic adder circuits is proposed using the rewrite-rule based theorem prover Rewrite Rule Laboratory (RRL). Proofs of properties of adder circuit descriptions are done by rewriting and induction. Carry lookahead adder circuit is described using powerlists, a data structure introduced by Misra to support divide-and-conquer strategy used for designing data-parallel algorithms. This description uses an algorithm for parallel prefix computation on powerlists due to Adams. Reasoning about properties of this algorithm can be of independent interest since parallel prefix operator has been found useful in many data-parallel algorithms. The correctness of the carry-lookahead adder (i.e., the adder indeed implements addition on numbers) is established by showing its equivalence to a recursive description of the ripple-carry adder, which is shown to correctly implement addition on natural numbers. The ripple carry adder circuit is described in two different but equivalent ways: using powerlists employing the divide-and-conquer strategy, as well as using linear lists employing the linear decomposition strategy. The description of the ripple carry adder using powerlists is useful for showing equivalence of its input-output behavior to that of carry lookahead adder, whereas the description using linear lists is useful for showing its correctness with respect to addition on natural numbers. Descriptions of adder circuits using powerlists are based on Adams' work who also gave a hand proof of their correctness using the powerlist algebra. The emphasis in this paper is to generate proofs mechanically by a theorem prover. RRL exploits the algebraic laws of the powerlist algebra as rewrite rules, and uses heuristics for mechanizing proofs by induction using the cover set method to generate such proofs. The regularity in hardware circuits gets reflected in compact descriptions generated using the divide-and-conquer strategy as well as in mechanically generated proofs by induction. Mechanical proofs generated by RRL closely follow the well-crafted hand-proofs which is quite encouraging. A comparison with Adams' hand generated proof is also made. There is strong evidence that the proposed methodology for generating proofs should scale up for large circuits exhibiting regularity that can be described using divide-and-conquer strategy in terms of powerlists.

KW - Automatic verification

KW - Carry lookahead adder

KW - Divide and conquer

KW - Formal verification

KW - Generic adders

KW - Parallel prefix

KW - Powerlists

KW - Proof by induction

KW - Ripple carry adder

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

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

U2 - 10.1023/A:1008610818519

DO - 10.1023/A:1008610818519

M3 - Article

VL - 13

SP - 127

EP - 158

JO - Formal Methods in System Design

JF - Formal Methods in System Design

SN - 0925-9856

IS - 2

ER -