To Meet The Problem Algorithm And Sequential Equivalence Checking

The development of modern VLSI design challenges the verification process. As the complement to traditional simulation-based verification process, Formal Verification methods gain more momentum recently. Improving the scalability and speed of Formal Methods becomes hot spot in worldwide research. By following this trend, this thesis can be divided into two parts:I. The research of Satisfiability problem (SAT). As a fundamental problem of formal verification, SAT algorithms are our startup research. The mainstream algorithm - DPLL based algorithm is selected as our research object. After analyzing the basic heuristics used in DPLL and its advanced reasoning techniques, we presented a modified FLD procedure with our Dynamic Filtering heuristic. The main contributions are: 1) The presented Dynamic Filtering heuristic reduced the computational overhead of FLD and the space searched by DPLL procedure while improving the running speed of DPLL algorithm; 2) Since DPLL-based algorithms dominate this area, any heuristics used must be suitable to be integrated into this kind of algorithm. Compared with other advanced reasoning techniques, our modified FLD procedure is more suitable to be integrated into DPLL algorithm.II. The research of sequential equivalence checking problem. Based on the research of SAT algorithms, we pay more effort on using SAT algorithm as engine into the sequential equivalence checking. The traditional state-space traversal based algorithm is analyzed and two main engines - BDD and SAT are compared. Then, by exploiting the induction based algorithms of Model checking, a frame expansion based algorithm is presented that uses SAT as the only engine. The main characteristics are: 1) Our verification algorithm uses SAT algorithm as the only engine. In contrast to BDD-based algorithm, not only there is no memory explosion problem, but also it improves the iteration efficiency of the engine. 2) By integrated unsatisfiable core extraction, induction based verification and structural fixed-point calculation, our algorithm is more suitable for verifying circuits with long sequential depth. Using our modification techniques, the presented algorithm is superior to the induction-based algorithm.