The Application Research And Implementation Of Boolean Satisfiability Algorithm In Formal Verification

Verification of digital hardware designs is becoming an increasingly complex task as the designs are incorporating more functionality, becoming more complex and growing larger in size. Traditionally, functional verification has been done using simulation-based approaches. As the designs become more complex, however, these techniques often fail to capture corner-case errors. As a consequence, formal methods for design verification have been sought after. In formal verification, the conformance of a design to a given set of specifications is proven mathematically, thereby leaving no room for unexplored search spaces. And they have shown promise in capturing subtle bugs, which were missed otherwise.In formal verification, the set of verification tasks can be converted into a set of Boolean Satisfiability problem. Traditionally, BDD-based approaches often encounter a bottleneck of memory explosion problem to solve these SAT problems. However, SAT-based approaches, which are checked for satisfiability using a SAT solver, can alleviate the state explosion problem. Since the first development of the basic search based algorithm proposed by Davis, Putnam, Logemann and Loveland (DPLL) about forty years ago, this area has seen active research effort with many interesting contributions that have culminated in state-of-the-art SAT solvers today being able to handle problem instances with thousands, and in same cases even millions of variabIes.As a result, the subject of designing and implementing practical SAT solvers has received considerable research attention, and numerous solver algorithms (GRASP[6], SATO[7], BERKMIN[8], ZCHAFF[9], etc..) have been proposed and implemented.In this dissertation, we focus on the application and implement of Boolean Satisfiability (SAT) algorithm in formal verification (such as Symbolic Simulation, Bounded Model Checking and Equivalence Checking). First of all, we introduce basic frame and the key techonology of DPLL-based SAT algorighm, Bounded Model Checking and Symbolic Simulation as well as the Equivalence Checking. We describle in detail how to design and implement our SAT solver (ChiveriSover), which bases on DPLL deep search algorithm through appending some new learning heuristic rules such as branch choosing and conflict clause adding,etc.. we describle a novle approach IncrCEC to solve the problem of combinational equivalence checking with incremental SAT based techniques. In this approach, based on an analysis of Combinational circuit by gate logic cone, we solve the problem that loses shared circuit structures information. Then, At last, we conducted two experiments on a variety of benchmark circuits, which one compared to zchaff show that ChiveriSolver is better than zchaff in some aspects. The other one shows that the IncrCEC approach is very efficient in some big combinational circuit with ChiveriSover.