Combinational Circuit Equivalence Checking The Preprocessing Algorithm Research

With the advances in VLSI and System-On-Chip (SOC) technology, the complexity of hardware systems and scale of circuits have increased manifold. Today, 70% of the design cost is spent in verifying these intricate systems. While traditional simulation can not handle current requirements, formal verification become more important, And now the two most widely used formal methods equivalent check and model check for design verification are the research hot point.The research of this paper is focusing on SAT Problem of combinational circuito Here proposes a technique to improve SAT-based Combinational Equivalence Checking (CEC) , to perform a low-cost preprocessing that will statically induce global signal relationships into the original CNF formula of the circuit under verification and hence reduce the complexity of the SAT instance, build up the implication graph for the circuit under verification, yielding a large set of logic implications composed of direct, indirect and extended backward implications, adding into Miter CNF formula, by that reduce the CNF analysis time.The main values of this thesis are: (1) By adding global signal relationships into the original clauses , quickly builds up the implication graph for the circuit. Converting implications inot binary clauses. (2) adding many binary clauses to contrain the search space of the SAT solver and provide correlation among the different variables ,can enhance BCP and reduce the SAT instance complexity significantly.