Design, Automation and Test in Europe Conference and Exhibition (DATE'03) Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals Munich, Germany March 03-March 07 ISBN: 0-7695-1870-2
Binary Decision Diagrams (BDDs) have been widely used for hardware verification since the beginning of the ?90s, whereas Boolean Satisfiability (SAT) has been gaining ground more recently, with the introduction of Bounded Model Cheking (BMC). In this paper we dovetail BDD and SAT based methods to improve the efficiency of BMC. More specifically, we first exploit inexpensive symbolic approximate reachability analysis to gather information on the state space. We then use the above information to restrict and focus the overall search space of SAT based BMC. In the experimental results section we show how the information coming from a BDD tool can improve the efficiency of a SAT engine by drastically reducing the number of "variable assignments" and "variable conflicts". This results in a significant overall performance gain associated with a general, robust, and easy-to-apply methodology.
Citation:
Gianpiero Cabodi, Sergio Nocco, Stefano Quer, "Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals," date, vol. 1, pp.10898, Design, Automation and Test in Europe Conference and Exhibition (DATE'03), 2003 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb