摘要：We propose a novel technique to improve SAT-based Combinational Equivalence Checking (CEC). The idea is to perform a low-cost preprocessing that will statically induce global signal relationships into the original CNF formula of the miter circuit under verification, and hence reduce the complexity of the SAT instance. This efficient and effective preprocessing quickly builds up the implication graph for the miter circuit under verification, yielding a large set of direct, indirect and extended backward implications. These two-node implications spanning the entire circuit are converted into binary clauses, and they are added to the miter CNF formula. The added clauses constrain the search space of the SAT solver and provide correlation among the different variables, which enhances the Boolean Constraint Propagation (BCP). Experimental results on large and difficult ISCAS'85, ISC AS'89 (full scan) and ITC'99 (full scan) CEC instances show that our approach is independent of the state-of-the-art SAT solver used, and that the added clauses help to achieve not eworthy speedup for each of the cases. Also, comparison with Hyper-Resolution (Hypre), Non-Increasing Variable Elimination Resolution (NIVER) and the propositional formula checker HeerHugo, suggests that our technique is more powerful, yielding non-trivial clauses that significantly simplify the SAT instance complexity.
Loading...
