Benefits of bounded model checking at an industrial setting

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 that are specially tuned for the BMC problem domain. 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 adapting BDD-based model checking for BMC. We have conducted comparison of 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.