A SAT-Based Arithmetic Circuit Bug-Hunting Method

Several differences lie between arithmetic circuit formal verification and conventional hardware formal verification. In this paper a SAT-based word-level model checking method aimed at arithmetic circuit bug-hunting is introduced. E-CNF is hybrid of Boolean formula and arithmetic formula. The original problem whether specification holds in the arithmetic circuit is translated into the satisfiability of an E-CNF problem. E-SAT, the E-CNF solver is an extension of complete SAT solver, with optimization techniques including tag clause. Experiments show SAT based word-level model checking method is highly automatic and powerful in bug-hunting for arithmetic circuit