Beyond safety: Customized SAT-based model checking

Malay K. Ganai, Aarti Gupta, Pranav Ashar

Research output: Contribution to journalConference article

6 Scopus citations

Abstract

Model checking of safety properties has taken a significant lead over non-safety properties in recent years. To bridge the gap, we propose dedicated SAT-based model checking algorithms for properties beyond safety. Previous bounded model checking (BMC) approaches have relied on either converting such properties to safety checking, or finding proofs by deriving termination criteria using loop-free path analysis. Instead, our approach uses a customized SAT-based formulation for bounded model checking of non-safety properties, and determines the completeness bounds for liveness using unbounded SAT-based analysis. Our main contributions are: 1) Customized property translations for LTL formulas for BMC, with novel features that utilize partitioning, learning, and incremental formulation. Customized translations not only improve the BMC performance significantly in comparison to standard monolithic LTL translations, but also allow efficient derivation and use of completeness bounds. Though we discuss the translation schemas for liveness, they can be easily extended to handle other LTL properties as well. 2) Customized formulations for determining completeness bounds for liveness using SAT-based unbounded model checking (UMC) rather than using loop-free path analysis. These formulations comprise greatest fixed-point and least fixed-point computations to efficiently handle nested properties using SAT-based quantification approaches. We show the effectiveness of our overall approach for checking liveness on public benchmarks and several industry designs.

Original languageEnglish (US)
Article number45.1
Pages (from-to)738-743
Number of pages6
JournalProceedings - Design Automation Conference
DOIs
StatePublished - 2005
Externally publishedYes
Event42nd Design Automation Conference, DAC 2005 - Anaheim, CA, United States
Duration: Jun 13 2005Jun 17 2005

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Control and Systems Engineering

Keywords

  • Bounded model checking
  • Circuit cofactoring
  • Formal verification
  • LTL
  • Liveness
  • SAT
  • Unbounded model checking

Fingerprint Dive into the research topics of 'Beyond safety: Customized SAT-based model checking'. Together they form a unique fingerprint.

  • Cite this