Learning from BDDs in SAT-based bounded model checking

Aarti Gupta, Malay Ganai, Chao Wang, Zijiang Yang, Pranav Ashar

Research output: Contribution to journalConference article

38 Scopus citations

Abstract

Bounded Model Checking (BMC) based on Boolean Satisfiability (SAT) procedures has recently gained popularity as an alternative to BDD-based model checking techniques for finding bugs in large designs. In this paper, we explore the use of learning from BDDs, where learned clauses generated by BDD-based analysis are added to the SAT solver, to supplement its other learning mechanisms. We propose several heuristics for guiding this process, aimed at increasing the usefulness of the learned clauses, while reducing the overheads. We demonstrate the effectiveness of our approach on several industrial designs, where BMC performance is improved and the design can be searched up to a greater depth by use of BDD-based learning.

Original languageEnglish (US)
Pages (from-to)824-829
Number of pages6
JournalProceedings - Design Automation Conference
DOIs
StatePublished - Jan 1 2003
Externally publishedYes
EventProceedings of the 40th Design Automation Conference - Anaheim, CA, United States
Duration: Jun 2 2003Jun 6 2003

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Control and Systems Engineering

Keywords

  • BDD learning
  • BDDs
  • Boolean Satisfiability
  • Bounded model checking
  • Learning
  • Property checking
  • SAT
  • SAT solvers

Fingerprint Dive into the research topics of 'Learning from BDDs in SAT-based bounded model checking'. Together they form a unique fingerprint.

  • Cite this