Tuning the VSIDS Decision Heuristic for Bounded Model Checking

13 years 11 months ago
Tuning the VSIDS Decision Heuristic for Bounded Model Checking
Bounded Model Checking (BMC) techniques have been used for formal hardware verification, with the help of tools such as GRASP (Generic search Algorithm for Satisfiability Problem) and more recently zchaff. In order to cope with very large hardware designs, our work exploited the unique characteristics of bounded model checking to enhance the SAT algorithms used to solve our problems. In our work, we tuned the VSIDS (Variable State Independent Decaying Sum) decision heuristics embedded in zchaff [5], in order to improve the efficiency of the DPLL SAT algorithm, which is especially effective for BMC problems. We also checked whether the conclusions reached by Strichman [6] regarding the tuning of GRASP, are also appropriate and hold true for zchaff. Our experimental results on actual hardware designs prove, with a few exceptions. that there is no real improvement when the existing tuned algorithms are applied to zchaff. However, our further modifications to the tuning proved to sign...
Ohad Shacham, Emmanuel Zarpas
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where MTV
Authors Ohad Shacham, Emmanuel Zarpas
Comments (0)