Mechanizing Verification of Arithmetic Circuits: SRT Division

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