Tunneling and slicing: Towards scalable BMC

Bounded model checking (BMC) provides complete design coverage with respect to a correctness property up to a bounded depth. However, with successive unrolling of the design, each BMC instance at depth k becomes bigger in size and harder to solve. We propose a novel scalable approach to decompose disjunctively a BMC instance, into simpler and independent subproblems, based on tunnels i.e., a set of control paths. We simplify each subproblem using slicing, data path simplification and tunnel specific control flow constraints, and solve them independently. We implemented such a tunneling and slicing-based reduction (TSR) approach in satisfiability-modulo-theory (SMT)-based BMC framework. Such a TSR-based approach improves the overall performance of BMC when applied to verification of low- level embedded industry programs.