Chinese Journal of Computers   Full Text
Title	A Novel Circuit SAT Solver in Unbounded Model Checking
Authors	ZHAO Yang1),2),3) LV Tao1),2),3) LI Hua-Wei1),2) LI Xiao-Wei1),2)
Address	1)(Key Laboratory of Computer System and Architecture, Chinese Academy of Sciences, Beijing 100190) 2)(Institute of Computing Technology, Chinese Academy of Sciences, Beijing 100190) 3)(Graduate University of Chinese Academy of Sciences, Beijing 100039)
Year	2009
Issue	No.6(1110—1118)
Abstract &   Background	Abstract For the circuit-oriented SAT problems, general purpose SAT solver will make some unnecessary decision and implication. The reason lies in that the circuit structure information is lost in the conversion to CNF. To overcome this drawback in SAT-based unbounded model checking, an improved SAT solver is proposed. First, the concept of define-value clauses is given to store the circuit structure in CNF. The improved solver avoids many redundant decisions which would be made by previous solvers. And then, A CNF-based assignment reduction algorithm is employed to speedup the convergence in search. The experimental result shows that the improved solver achieves obvious speedup over a previous method in preimage computation. The new method is capable of handling complex circuit property checking on which BDD-based methods would hardly work. Keywords design verification; unbounded model checking; Boolean satisfiability (SAT); register-transfer level (RTL) Background Binary Decision Diagram (BDD) makes model checking a practical method in real design verification. It has achieved wide acceptance in academia and also successful application in industry, like the verifying the correctness of IEEE Futurebus+standard (IEEE Standard 896.1-1991). The state-of-the-art BDD-based algorithm can handle up to 10120 states in design. But its weakness is the unacceptable memory consumption in constructing the structure and doing operation, especially when the circuit design becomes more and more complex. This problem is known as the “space explosion” in model checking. SAT is a classic problem in computer science. It is the first known NP-complete problem and has wide applications in artificial intelligence, programming and electrical design automation (EDA). In recent years, many new efficient schemes of SAT solving are proposed, including two-literal watch, conflict-driven learning and VSIDS decision heuristic. The SAT solver becomes a powerful tool in tackle Boolean reasoning. In this case, the application of SAT solver in model checking is extensively researched. One of the most important achievement in SAT-based circuit verification is the advance of circuit SAT solver, including C-SAT by UCSB, CirCUs by University of Colorado and so on. The main contributions of these works are the circuit-oriented schemes to accelerate the speed of the pure CNF SAT solver. Until now, it is still an open question that how to balance the structures of circuit and CNF to achieve the highest efficiency. SAT-based unbounded model checking (UMC) is a relatively new topic. This research starts around 2002. Its basic idea is to eliminate the quantification in image and preimage computation using all-SAT solver. The circuit structure is converted to a SAT problem and SAT solver is employed to enumerate all solutions. This paper proposes an approach to speed up the SAT solver in UMC. Generally speaking, it is a CNF-based solver but circuit aware. Because of the new concepts we introduce, our solver grasps some feature and structure of CNF derived from circuit design. So it is advantageous over plain CNF-solver in speed. This research is supported in part by National Natural Science Foundation of China under grant No.60633060, National Basic Research Program (973 Program) of China under grant No.2005CB321605, and in part by National High Technology Research and Development Program (863 Program) of China under grant Nos.2007AA01Z476, 2007AA01Z113.