About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
MTV 2003
Conference paper
Tuning the VSIDS decision heuristic for bounded model checking
Abstract
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 (M.W. Moskewicz et al., 2001), 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 (2000) 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 significantly increase SAT efficiency for BMC problems.