### 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 language | English (US) |
---|---|

Title of host publication | Foundations of Software Technology and Theoretical Computer Science - 17th Conference, 1997, Proceedings |

Editors | S. Ramesh, G. Sivakumar |

Publisher | Springer Verlag |

Pages | 103-122 |

Number of pages | 20 |

ISBN (Print) | 3540638768, 9783540638766 |

DOIs | |

State | Published - 1997 |

Event | 17th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 1997 - Kharagpur, India Duration: Dec 18 1997 → Dec 20 1997 |

### Publication series

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

Volume | 1346 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 17th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 1997 |
---|---|

Country | India |

City | Kharagpur |

Period | 12/18/97 → 12/20/97 |

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

## Fingerprint Dive into the research topics of 'Mechanizing verification of arithmetic circuits: SRT division'. Together they form a unique fingerprint.

## Cite this

*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. https://doi.org/10.1007/bfb0058026