An Improved Hybrid SAT Solver for Bounded Model Checking in Circuit Design

Model checking is one of main formal verification methods that are used in the process of circuit design and verification. However, there is a problem of state memory explosion in traditional model checking methods. Bounded model checking (BMC), in which the Davis-Putnam-Logemann-Loveland (DPLL) algorithm based Satisfiability (SAT) solver is used to verify the circuits, can avoid this problem, whereas, its efficiency depends on the performance of the solver. Hybrid SAT solver combines the advantages of the completeness of DPLL and the fast solving property of stochastic local search algorithm, e.g. WalkSAT, and is proved to be an efficient improving way. However, it is noted that the noise parameter in WalkSAT could affect the solver's overall performance. In this paper, an adaptive noise mechanism is proposed to integrate with the hybrid algorithm framework to further improve the solver's performance. Our experimental results have shown that the designed hybrid solver with adaptive noise performs well in BMC instances and some other circuits.Computer Science, Artificial IntelligenceComputer Science, Hardware & ArchitectureCPCI-S(ISTP)