Benefits of Bounded Model Checking at an Industrial Setting
Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, Moshe Y. Vardi
To appear at
13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001
Abstract
Abstract. The usefulness of Bounded Model Checking (BMC) based on propositional satisfiability (SAT) methods for bug hunting has already been proven in several recent work. In this paper, we present two industrial strength systems performing BMC for both verification and falsification. The first is Thunder, which performs BMC on top of a new satisfiability solver, SIMO. The second is Forecast, which performs BMC on top of a BDD package. SIMO is based on the Davis Logemann Loveland procedure (DLL) and features the most recent search methods. It enjoys static and dynamic branching heuristics, advanced back-jumping and learning techniques. SIMO also includes new heuristics which are specially tuned for best BMC results. With Thunder we have achieved impressive capacity and productivity for BMC. Real designs, taken from Intel’s Pentium©4, with over 1000 model variables were validated using the default tool settings and without manual tuning. In Forecast, we present several alternatives for performing BMC on BDD, while trying to optimize our BDD-based unbounded model checker for Bounded search. We have conducted comparison between Thunder and Forecast on a large set of real and complex designs and on almost all of them Thunder has demonstrated clear win over Forecast in two important aspects: Capacity and Productivity.
Server
START
Conference Manager
Update Time
28 Mar 2001 at 08:36:01
Maintainer
www-cav01@lsv.ens-cachan.fr.
Conference Systems
