Sat Algorithm Used In Ic Formal Verification

The design verification is the critical part of the Integrated circuit designs. The function of system is becoming more and more complex With the scale of Integrated circuit increasing. Extensive simulation, the traditional approach is no longer adequate the design required so formal verification has attracted dramatically the interests of both academic and industrial fields.Equivalence checking is an important method of formal verification, the chief function is verify the equivalence of circuits. Almost all the equivalence checking problems can be changed into Satisfiability problems, consequently the research of SAT solver is the critical point of formal verification. Many universities, institutes and corporations (such as Intel, IBM) all aim at SAT solver take a deep research, and gained remarkable fruits. Many of them had been applied into industry and manufacturing, such as microprocessors, floating-point assemblies and correspondence hardware.This paper summarize the fruit of the formal verification comprehensively. The new SAT solver(ArtSat) combined the Symmetric Extended Unit Propagation (SEUP) with Dynamic filtration algorithm and add VSIDS tactic. It proved that the result of relativity testing was anticipanted.The main content of this thesis is advanced forward reasoning based on DPLL. The normal DPLL arithmetic consist four parts:Decision Process, BCP Process, Learning Process; Retrospect Process. Improving the efficiency of the four processes or others of the DPLL is so important. Through research on the BCP Process carefully and integrate the complicacy of calculation and time of arithmetic, This paper proposes a new Propositional SAT solver which combined the Failed Literal Detection(FLD) one of the advanced forward reasoning technologies and DPLL,The ArtSat solver had a excellent performance through the comparison with other results of SAT solver.