Strengthening Model Checking Techniques With Inductive Invariants

This paper describes optimized techniques to efficiently compute and reap benefits from inductive invariants within satisfiability (SAT)-based model checking. We address sequential circuit verification and consider both equivalences and implications between pairs of nodes in the logic networks. First, we present a very efficient dynamic procedure, based on equivalence classes and incremental SAT, specifically oriented to reduce the set of checked invariants. Then, we show how to effectively integrate the computation of inductive invariants within state-of-the-art SAT-based model-checking procedures. Experiments (on more than 600 designs) show the robustness of our approach on verification instances on which stand-alone techniques fail.