Beyond Safety: Customized SAT-based Model Checking - Technical Paper from DAC 2005

NEC Laboratories America

Paper by Malay K Ganai, Aarti Gupta and Pranav Ashar.

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 fixedpoint 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.


Read the complete story ...


Review Article Be the first to review this article

Aldec Simulator Evaluate Now

Featured Video
Jobs
Principal PIC Hardware Controls Engineer for Infinera Corp at Sunnyvale, CA
ASIC Design Engineer for Infinera Corp at Sunnyvale, CA
Senior Formal FAE Location OPEN for EDA Careers at San Jose or Anywhere, CA
Senior PIC Test Development Engineer for Infinera Corp at Sunnyvale, CA
Senior DSP Firmware Engineer for Cirrus Logic, Inc. at Austin, TX
Design Verification Engineer for Cirrus Logic, Inc. at Austin, TX
Upcoming Events
IC Open Innovation Panel During REUSE 2017 at Santa Clara Convention Center 5001 Great America Parkway Santa Clara CA - Dec 14, 2017
Essentials of Electronic Technology: A Crash Course at Columbia MD - Jan 16 - 18, 2018
Essentials of Digital Technology at MD - Feb 13 - 14, 2018
CST: Webinar series



Internet Business Systems © 2017 Internet Business Systems, Inc.
25 North 14th Steet, Suite 710, San Jose, CA 95112
+1 (408) 882-6554 — Contact Us, or visit our other sites:
AECCafe - Architectural Design and Engineering TechJobsCafe - Technical Jobs and Resumes GISCafe - Geographical Information Services  MCADCafe - Mechanical Design and Engineering ShareCG - Share Computer Graphic (CG) Animation, 3D Art and 3D Models
  Privacy PolicyAdvertise