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. 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
Start Conference Manager
Conference Systems