Lazy abstraction and SAT-based reachability in hardware model checking

In this work we present a novel lazy abstraction-refinement technique for hardware model checking, integrated with the SAT-based algorithm IC3. In contrast to most SAT-based model checking algorithms, IC3 avoids unrolling of the transition relation. Instead, it applies local checks, while computing over-approximated sets of reachable states. We find IC3 most suitable for lazy abstraction, since each one of its local checks requires different information from the checked model. Similarly to IC3, our algorithm obtains a series of over-approximated sets of states. However, when constructing the series, different abstractions are used for different sets. If an abstract counterexample is obtained, we either find a corresponding concrete one, or apply refinement to eliminate all counterexamples of the same length. Refinement makes the abstractions more precise as needed, and where needed. After refinement, the computation resumes from the same step where it was interrupted. The result is an incremental abstraction-refinement algorithm where the abstraction is lazy. We implemented our algorithm, called L-IC3, and compared it with the original IC3 on large industrial hardware designs. We obtained significant speedups of up to two orders of magnitude.