Tunneling and slicing: Towards scalable BMC

Malay Ganai, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Scopus citations

Abstract

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 lowlevel embedded industry programs.

Original languageEnglish (US)
Title of host publicationProceedings of the 45th Design Automation Conference, DAC
Pages137-142
Number of pages6
DOIs
StatePublished - Sep 17 2008
Externally publishedYes
Event45th Design Automation Conference, DAC - Anaheim, CA, United States
Duration: Jun 8 2008Jun 13 2008

Publication series

NameProceedings - Design Automation Conference
ISSN (Print)0738-100X

Other

Other45th Design Automation Conference, DAC
CountryUnited States
CityAnaheim, CA
Period6/8/086/13/08

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Control and Systems Engineering

Fingerprint Dive into the research topics of 'Tunneling and slicing: Towards scalable BMC'. Together they form a unique fingerprint.

  • Cite this

    Ganai, M., & Gupta, A. (2008). Tunneling and slicing: Towards scalable BMC. In Proceedings of the 45th Design Automation Conference, DAC (pp. 137-142). [4555797] (Proceedings - Design Automation Conference). https://doi.org/10.1109/DAC.2008.4555797