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 Satisfiabil-ity 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] regard-ing the tuning of GRASP, are also appropriate and hold true for zchaff. Our experimental results on actual hardware de-signs prove, with a few exceptions. that there is no real im-provement when the existing tuned algorithms are applied to zchaff. However, our further modifications to the tun-ing proved to significantly increase SAT efficiency for BMC problems. 1