Lazy constraints and SAT heuristics for proof-based abstraction

Aarti Gupta, Malay Ganai, Pranav Ashar

Research output: Contribution to journalConference articlepeer-review

6 Scopus citations

Abstract

SAT proof analysis techniques have been used recently with BMC in order to generate proof-based abstractions that preserve the correctness of the property up to a certain depth. In this paper, we propose various techniques for handling BMC constraints that are targeted at reducing the size of the abstract model while preserving bounded correctness. We propose lazy constraints, where the idea is to delay propagation of certain implied values without modifying a standard SAT solver. We propose different methods for automatic use of lazy constraints in SAT-based BMC. Their use can be regarded as a heuristic, which typically leads to significant reduction in the size of the abstract model, frequently accompanied by an overall performance improvement. We also use SAT proof analysis to loosen the user-specified environmental constraints, in order to generate smaller abstract models for conservative verification. We briefly describe other SAT-based heuristics for reducing the size of the abstract model. We have implemented our techniques in a prototype verification platform, and demonstrate their effectiveness on several large industry designs.

Original languageEnglish (US)
Pages (from-to)183-188
Number of pages6
JournalProceedings of the IEEE International Conference on VLSI Design
StatePublished - Dec 1 2005
Externally publishedYes
Event18th International Conference on VLSI Design: Power Aware Design of VLSI Systems - Kolkata, India
Duration: Jan 3 2005Jan 7 2005

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Lazy constraints and SAT heuristics for proof-based abstraction'. Together they form a unique fingerprint.

Cite this