Accelerating high-level bounded model checking

Malay K. Ganai, Aarti Gupta

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

58 Scopus citations

Abstract

SAT-based Bounded Model Checking (BMC) has been found promising in finding deep bugs in industry designs and scaling well with design sizes. However, it has limitations due to requirement of finite data paths, inefficient translations and loss of high-level design information during the BMC problem formulation. These shortcomings inherent in Boolean-level BMC can be avoided by using high-level BMC. We propose a novel framework for high-level BMC, which includes several techniques that extract high-level design information from EFSM models to make the verification model "BMC friendly", and use it on-the-fly to simplify the BMC problem instances. Such techniques overcome the inherent limitations of Boolean-level BMC, while allowing integration of state-of-the-art techniques for BMC. In our controlled experiments we found signficant performance improvements achievable by the proposed techniques.

Original languageEnglish (US)
Title of host publicationProceedings of the 2006 International Conference on Computer-Aided Design, ICCAD
Pages794-801
Number of pages8
DOIs
StatePublished - 2006
Event2006 International Conference on Computer-Aided Design, ICCAD - San Jose, CA, United States
Duration: Nov 5 2006Nov 9 2006

Publication series

NameIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
ISSN (Print)1092-3152

Other

Other2006 International Conference on Computer-Aided Design, ICCAD
Country/TerritoryUnited States
CitySan Jose, CA
Period11/5/0611/9/06

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design

Fingerprint

Dive into the research topics of 'Accelerating high-level bounded model checking'. Together they form a unique fingerprint.

Cite this