FuseIC3

An Algorithm for Checking Large Design Spaces

Rohit Dureja and Kristin Yvonne Rozier

This webpage contains further details and artifacts for reproducibility of the experiments in "FuseIC3: An Algorithm for Checking Large Design Spaces" by R. Dureja and K.Y. Rozier.

=> Proofs of theorems appearing in the paper can be found here <=

Abstract

The design of safety-critical systems often requires design space exploration: comparing several system models that differ in terms of design choices, capabilities, and implementations. Model checking can compare different models in such a set, however, it is continuously challenged by the state space explosion problem. Therefore, learning and reusing information from solving related models becomes very important for future checking efforts. For example, reusing variable ordering in BDD-based model checking leads to substantial performance improvement. In this paper, we present a SAT-based algorithm for checking a set of models. Our algorithm, FuseIC3, extends IC3 to minimize time spent in exploring the common state space between related models. Specifically, FuseIC3 accumulates artifacts from the sequence of over-approximated reachable states, called frames, from earlier runs when checking new models, albeit, after careful repair. It uses bidirectional reachability; forward reachability to repair frames, and IC3-type backward reachability to block predecessors to bad states. We extensively evaluate FuseIC3 over a large collection of challenging benchmarks. FuseIC3 is 1.75× faster than checking each model individually, and 1.72× faster than the state-of-the-art incremental IC3 algorithm.

Algorithm

FuseIC3 automatically reuses information from earlier model-checking runs to minimize the time spent in exploring the state space in common between related models. Given a set of models and a safety property, FuseIC3 sequentially checks each model by reusing information: reachable state approximations, counterexamples (cex), and invariants, learned in earlier runs to reduce the set’s total checking time. When the difference in two subsequent models is small or beyond the cone-of-influence of the property, the invariant or counterexample from earlier models may be directly used to verify the current model. Otherwise, FuseIC3 uses reachable state approximations as input to IC3 to only explore undiscovered reachable states in the current model. In the former, verification completes almost instantly, while in the latter, significant time is saved. When the stored information cannot be used directly, FuseIC3 repairs and patches it using an efficient SAT-based algorithm. The repair algorithm is the main strength of FuseIC3, and uses features present in modern SAT solvers. It adds “just enough” extra information to the saved reachable states to enable reuse.