Accelerating CAR-Based Model-Checking with Multiple Unsatisfiable Cores

Model checking is a framework for automated formal verification of transition systems, like hardware designs. Two leading model-checking techniques, PDR and CAR, are based on multiple calls to a SAT solver, for the purpose of finding a path to a bug or proving its absence. They build sequences of formulas, called frames, that represent approximated sets of states, e.g., a frame can contain an over-approximation of the states that can reach the negated property within a given number of steps. Part of the process is to make these sets more precise, i.e., less approximating, and this is done by strengthening the frames with negation of states that were proven to be spurious. A key component for performance is the ability of these engines to generalize those states and thus accelerate the process of making the frames more precise. This is done by strengthening them with the unsatisfiable cores that the SAT solver returns. In this work, we suggest several performance improvements to this process, most notably a technique for generating multiple such cores in linear time and adding them simultaneously to the frames. Our results show that our implementation of these techniques, on top of SimpleCAR, not only improves its performance, but also solves more (unsafe) cases than any other model-checker in the public domain, and solves instances from the HWMCC that no other model checker can solve, hence it contributes to the state-of-the-art.