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.