Using an induction prover for verifying arithmetic circuits

Deepak Kapur, Mahadevan Subramaniam

Research output: Contribution to journalArticle

16 Scopus citations

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

Keywords

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

ASJC Scopus subject areas

  • Software
  • Information Systems

Cite this