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
Featured Video
Jobs
ASIC FPGA Verification Engineer for General Dynamics Mission Systems at Bloomington, MN
Principal Engineer FPGA Design for Intevac at Santa Clara, CA
SOC Logic Design Engineer for Global Foundaries at Santa Clara, CA
Development Engineer-WEB SKILLS +++ for EDA Careers at North Valley, CA
Technical Support Engineer for EDA Careers at Freemont, CA
Technical Marketing Manager Valley for EDA Careers at San Jose, CA
Upcoming Events
DVCon 2017 Conference at DoubleTree Hotel San Jose CA - Feb 27 - 2, 2017
IoT Summit 2017 at Great America ballroom, Santa Clara Convention Center Santa Clara CA - Mar 16 - 17, 2017
SNUG Silicon Valley 2017 at Santa Clara Convention Center Santa Clara CA - Mar 22 - 23, 2017
CDNLive Silicon Valley 2017 at Santa Clara Convention Center Santa Clara CA - Apr 11 - 12, 2017



Internet Business Systems © 2017 Internet Business Systems, Inc.
595 Millich Dr., Suite 216, Campbell, CA 95008
+1 (408)-337-6870 — 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 Policy