Safety Model Checking with Complementary Approximations

TL;DR

This paper introduces Complementary Approximate Reachability (CAR), a novel SAT-based safety model checking framework that maintains over- and under-approximations simultaneously, improving the ability to verify hardware safety properties.

Contribution

CAR is a new framework that combines over- and under-approximations in safety model checking, demonstrating improved performance over existing methods like IC3/PDR.

Findings

CAR solved 42 instances unsolvable by IC3/PDR.

CAR solved 21 instances other approaches could not.

CAR outperforms some existing safety model checking techniques.

Abstract

Formal verification techniques such as model checking, are becoming popular in hardware design. SAT-based model checking techniques such as IC3/PDR, have gained a significant success in hardware industry. In this paper, we present a new framework for SAT-based safety model checking, named Complementary Approximate Reachability (CAR). CAR is based on standard reachability analysis, but instead of maintaining a single sequence of reachable- state sets, CAR maintains two sequences of over- and under- approximate reachable-state sets, checking safety and unsafety at the same time. To construct the two sequences, CAR uses standard Boolean-reasoning algorithms, based on satisfiability solving, one to find a satisfying cube of a satisfiable Boolean formula, and one to provide a minimal unsatisfiable core of an unsatisfiable Boolean formula. We applied CAR to 548 hardware model-checking instances, and compared its performance with IC3/PDR. Our results show that CAR is able to solve 42 instances that cannot be solved by IC3/PDR. When evaluated against a portfolio that includes IC3/PDR and other approaches, CAR is able to solve 21 instances that the other approaches cannot solve. We conclude that CAR should be considered as a valuable member of any algorithmic portfolio for safety model checking.