Beyond safety: customized SAT-based model checking

Model checking of safety properties has taken a significant lead over nonsafety 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 nonsafety 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.