Safety property verification using sequential SAT and bounded model checking |
| |
Authors: | Parthasarathy G Iyer MK Cheng K-T Wang L-C |
| |
Affiliation: | California Univ., Santa Barbara, CA, USA; |
| |
Abstract: | Model checkers verify properties of safety- or business-critical systems. The main idea behind model checking is to convert a design's verification into a problem of checking key design properties expressed as a set of temporal logic formulas. The graph representing the design's state space then becomes the basis for testing these formulas' satisfiability (SAT). This divide-and-conquer approach provides an overall test for design correctness. We describe a method for checking safety properties using sequential SAT. SSAT can efficiently prove true properties by harnessing the power of bounded model checking (BMC) using SAT, but without the need for a pre-computed correctness threshold. Using a standard set of benchmarks, we conducted experiments to compare the runtime behavior of SSAT with BMC and binary decision diagrams (BDDs). |
| |
Keywords: | |
|
|