Mechanizing verification of arithmetic circuits: SRT division

Deepak Kapur, M. Subramaniam

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

9 Citations (Scopus)

Abstract

The use of a rewrite-based theorem prover for verifying properties of arithmetic circuits is discussed. A prover such as Rewrite Rule Laboratory (RRL) can be used effectively for establishing numbertheoretic properties of adders, multipliers and dividers. Since verification of adders and multipliers has been discussed elsewhere in earlier papers, the focus in this paper is on a divider circuit. An SRT division circuit similar to the one used in the Intel Pentium processor is mechanically verified using RRL. The number-theoretic correctness of the division circuit is established from its equational specification. The proof is generated automatically, and follows easily using the inference procedures for contextual rewriting and a decision procedure for the quantifier-free theory of numbers (Presburger arithmetic) already implemented in RRL. Additional enhancements to rewrite-based provers such as RRL that would further facilitate verifying properties of circuits with structure similar to that of the SRT division circuit are discussed.

Original languageEnglish (US)
Title of host publicationFoundations of Software Technology and Theoretical Computer Science - 17th Conference, 1997, Proceedings
EditorsS. Ramesh, G. Sivakumar
PublisherSpringer Verlag
Pages103-122
Number of pages20
ISBN (Print)3540638768, 9783540638766
StatePublished - Jan 1 1997
Event17th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 1997 - Kharagpur, India
Duration: Dec 18 1997Dec 20 1997

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1346
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other17th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 1997
CountryIndia
CityKharagpur
Period12/18/9712/20/97

Fingerprint

Arithmetic Circuits
Division
Networks (circuits)
Adders
Multiplier
Decision Procedures
Rewriting
Quantifiers
Correctness
Enhancement
Specification
Specifications
Theorem

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Kapur, D., & Subramaniam, M. (1997). Mechanizing verification of arithmetic circuits: SRT division. In S. Ramesh, & G. Sivakumar (Eds.), Foundations of Software Technology and Theoretical Computer Science - 17th Conference, 1997, Proceedings (pp. 103-122). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1346). Springer Verlag.

Mechanizing verification of arithmetic circuits : SRT division. / Kapur, Deepak; Subramaniam, M.

Foundations of Software Technology and Theoretical Computer Science - 17th Conference, 1997, Proceedings. ed. / S. Ramesh; G. Sivakumar. Springer Verlag, 1997. p. 103-122 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1346).

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

Kapur, D & Subramaniam, M 1997, Mechanizing verification of arithmetic circuits: SRT division. in S Ramesh & G Sivakumar (eds), Foundations of Software Technology and Theoretical Computer Science - 17th Conference, 1997, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1346, Springer Verlag, pp. 103-122, 17th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 1997, Kharagpur, India, 12/18/97.
Kapur D, Subramaniam M. Mechanizing verification of arithmetic circuits: SRT division. In Ramesh S, Sivakumar G, editors, Foundations of Software Technology and Theoretical Computer Science - 17th Conference, 1997, Proceedings. Springer Verlag. 1997. p. 103-122. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Kapur, Deepak ; Subramaniam, M. / Mechanizing verification of arithmetic circuits : SRT division. Foundations of Software Technology and Theoretical Computer Science - 17th Conference, 1997, Proceedings. editor / S. Ramesh ; G. Sivakumar. Springer Verlag, 1997. pp. 103-122 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{fefe46d1114e44a082425730ea0e7f46,
title = "Mechanizing verification of arithmetic circuits: SRT division",
abstract = "The use of a rewrite-based theorem prover for verifying properties of arithmetic circuits is discussed. A prover such as Rewrite Rule Laboratory (RRL) can be used effectively for establishing numbertheoretic properties of adders, multipliers and dividers. Since verification of adders and multipliers has been discussed elsewhere in earlier papers, the focus in this paper is on a divider circuit. An SRT division circuit similar to the one used in the Intel Pentium processor is mechanically verified using RRL. The number-theoretic correctness of the division circuit is established from its equational specification. The proof is generated automatically, and follows easily using the inference procedures for contextual rewriting and a decision procedure for the quantifier-free theory of numbers (Presburger arithmetic) already implemented in RRL. Additional enhancements to rewrite-based provers such as RRL that would further facilitate verifying properties of circuits with structure similar to that of the SRT division circuit are discussed.",
author = "Deepak Kapur and M. Subramaniam",
year = "1997",
month = "1",
day = "1",
language = "English (US)",
isbn = "3540638768",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "103--122",
editor = "S. Ramesh and G. Sivakumar",
booktitle = "Foundations of Software Technology and Theoretical Computer Science - 17th Conference, 1997, Proceedings",

}

TY - GEN

T1 - Mechanizing verification of arithmetic circuits

T2 - SRT division

AU - Kapur, Deepak

AU - Subramaniam, M.

PY - 1997/1/1

Y1 - 1997/1/1

N2 - The use of a rewrite-based theorem prover for verifying properties of arithmetic circuits is discussed. A prover such as Rewrite Rule Laboratory (RRL) can be used effectively for establishing numbertheoretic properties of adders, multipliers and dividers. Since verification of adders and multipliers has been discussed elsewhere in earlier papers, the focus in this paper is on a divider circuit. An SRT division circuit similar to the one used in the Intel Pentium processor is mechanically verified using RRL. The number-theoretic correctness of the division circuit is established from its equational specification. The proof is generated automatically, and follows easily using the inference procedures for contextual rewriting and a decision procedure for the quantifier-free theory of numbers (Presburger arithmetic) already implemented in RRL. Additional enhancements to rewrite-based provers such as RRL that would further facilitate verifying properties of circuits with structure similar to that of the SRT division circuit are discussed.

AB - The use of a rewrite-based theorem prover for verifying properties of arithmetic circuits is discussed. A prover such as Rewrite Rule Laboratory (RRL) can be used effectively for establishing numbertheoretic properties of adders, multipliers and dividers. Since verification of adders and multipliers has been discussed elsewhere in earlier papers, the focus in this paper is on a divider circuit. An SRT division circuit similar to the one used in the Intel Pentium processor is mechanically verified using RRL. The number-theoretic correctness of the division circuit is established from its equational specification. The proof is generated automatically, and follows easily using the inference procedures for contextual rewriting and a decision procedure for the quantifier-free theory of numbers (Presburger arithmetic) already implemented in RRL. Additional enhancements to rewrite-based provers such as RRL that would further facilitate verifying properties of circuits with structure similar to that of the SRT division circuit are discussed.

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

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

M3 - Conference contribution

AN - SCOPUS:84949219848

SN - 3540638768

SN - 9783540638766

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

SP - 103

EP - 122

BT - Foundations of Software Technology and Theoretical Computer Science - 17th Conference, 1997, Proceedings

A2 - Ramesh, S.

A2 - Sivakumar, G.

PB - Springer Verlag

ER -