Application of Term Rewriting Techniques to Hardware Design Verification

Term rewriting systems have been used in automatic theorem proving. A canonical term rewriting system for boolean algebra recently discovered, and a refutation technique using Knuth-Bendix completion procedure can be used to prove boolean formulas arising in logic verification. In this paper a design verification system based on term rewriting techniques is presented. It can prove total correctness of combinational circuits without exhaustive simulation. A prototype system implemented on a Motorola 68010 based workstation shows that the system performs favorably compared to a simulator.