Proc. of

Deepak Kapur and Mahadavan Subramaniam

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 number-theoretic 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.