Mechanical verification of adder circuits using rewrite rule laboratory

Deepak Kapur, M. Subramaniam

Research output: Contribution to journalArticlepeer-review

25 Scopus citations


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
Issue number2
StatePublished - Sep 1998
Externally publishedYes


  • 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


Dive into the research topics of 'Mechanical verification of adder circuits using rewrite rule laboratory'. Together they form a unique fingerprint.

Cite this