Using an induction prover for verifying arithmetic circuits

Deepak Kapur, Mahadevan Subramaniam

Research output: Contribution to journalArticle

16 Citations (Scopus)

Abstract

We show that existing theorem proving technology can be used effectively for mechanically verifying a family of arithmetic circuits. A theorem prover implementing: (i) a decision procedure for quantifier-free Presburger arithmetic with uninterpreted function symbols; (ii) conditional rewriting; and (iii) heuristics for carefully selecting induction schemes from terminating recursive function definitions; and (iv) well integrated with backtracking, can automatically verify number-theoretic properties of parameterized and generic adders, multipliers and division circuits. This is illustrated using our theorem prover Rewrite Rule Laboratory (RRL). To our knowledge, this is the first such demonstration of the capabilities of a theorem prover mechanizing induction. The above features of RRL are briefly discussed using illustrations from the verification of adder, multiplier and division circuits. Extensions to the prover likely to make it even more effective for hardware verification are discussed. Furthermore, it is believed that these results are scalable, and the proposed approach is likely to be effective for other arithmetic circuits as well.

Original languageEnglish (US)
Pages (from-to)32-65
Number of pages34
JournalInternational Journal on Software Tools for Technology Transfer
Volume3
Issue number1
DOIs
StatePublished - Dec 1 2000

Fingerprint

Networks (circuits)
Adders
Recursive functions
Theorem proving
Demonstrations
Hardware

Keywords

  • Arithmetic circuits
  • Automated reasoning
  • Decision procedures
  • Hardware verification
  • Induction
  • Rewriting

ASJC Scopus subject areas

  • Software
  • Information Systems

Cite this

Using an induction prover for verifying arithmetic circuits. / Kapur, Deepak; Subramaniam, Mahadevan.

In: International Journal on Software Tools for Technology Transfer, Vol. 3, No. 1, 01.12.2000, p. 32-65.

Research output: Contribution to journalArticle

@article{8576484140a04115a3b6c817bcb62263,
title = "Using an induction prover for verifying arithmetic circuits",
abstract = "We show that existing theorem proving technology can be used effectively for mechanically verifying a family of arithmetic circuits. A theorem prover implementing: (i) a decision procedure for quantifier-free Presburger arithmetic with uninterpreted function symbols; (ii) conditional rewriting; and (iii) heuristics for carefully selecting induction schemes from terminating recursive function definitions; and (iv) well integrated with backtracking, can automatically verify number-theoretic properties of parameterized and generic adders, multipliers and division circuits. This is illustrated using our theorem prover Rewrite Rule Laboratory (RRL). To our knowledge, this is the first such demonstration of the capabilities of a theorem prover mechanizing induction. The above features of RRL are briefly discussed using illustrations from the verification of adder, multiplier and division circuits. Extensions to the prover likely to make it even more effective for hardware verification are discussed. Furthermore, it is believed that these results are scalable, and the proposed approach is likely to be effective for other arithmetic circuits as well.",
keywords = "Arithmetic circuits, Automated reasoning, Decision procedures, Hardware verification, Induction, Rewriting",
author = "Deepak Kapur and Mahadevan Subramaniam",
year = "2000",
month = "12",
day = "1",
doi = "10.1007/PL00010808",
language = "English (US)",
volume = "3",
pages = "32--65",
journal = "International Journal on Software Tools for Technology Transfer",
issn = "1433-2779",
publisher = "Springer Verlag",
number = "1",

}

TY - JOUR

T1 - Using an induction prover for verifying arithmetic circuits

AU - Kapur, Deepak

AU - Subramaniam, Mahadevan

PY - 2000/12/1

Y1 - 2000/12/1

N2 - We show that existing theorem proving technology can be used effectively for mechanically verifying a family of arithmetic circuits. A theorem prover implementing: (i) a decision procedure for quantifier-free Presburger arithmetic with uninterpreted function symbols; (ii) conditional rewriting; and (iii) heuristics for carefully selecting induction schemes from terminating recursive function definitions; and (iv) well integrated with backtracking, can automatically verify number-theoretic properties of parameterized and generic adders, multipliers and division circuits. This is illustrated using our theorem prover Rewrite Rule Laboratory (RRL). To our knowledge, this is the first such demonstration of the capabilities of a theorem prover mechanizing induction. The above features of RRL are briefly discussed using illustrations from the verification of adder, multiplier and division circuits. Extensions to the prover likely to make it even more effective for hardware verification are discussed. Furthermore, it is believed that these results are scalable, and the proposed approach is likely to be effective for other arithmetic circuits as well.

AB - We show that existing theorem proving technology can be used effectively for mechanically verifying a family of arithmetic circuits. A theorem prover implementing: (i) a decision procedure for quantifier-free Presburger arithmetic with uninterpreted function symbols; (ii) conditional rewriting; and (iii) heuristics for carefully selecting induction schemes from terminating recursive function definitions; and (iv) well integrated with backtracking, can automatically verify number-theoretic properties of parameterized and generic adders, multipliers and division circuits. This is illustrated using our theorem prover Rewrite Rule Laboratory (RRL). To our knowledge, this is the first such demonstration of the capabilities of a theorem prover mechanizing induction. The above features of RRL are briefly discussed using illustrations from the verification of adder, multiplier and division circuits. Extensions to the prover likely to make it even more effective for hardware verification are discussed. Furthermore, it is believed that these results are scalable, and the proposed approach is likely to be effective for other arithmetic circuits as well.

KW - Arithmetic circuits

KW - Automated reasoning

KW - Decision procedures

KW - Hardware verification

KW - Induction

KW - Rewriting

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

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

U2 - 10.1007/PL00010808

DO - 10.1007/PL00010808

M3 - Article

VL - 3

SP - 32

EP - 65

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

SN - 1433-2779

IS - 1

ER -