Learning lemma support graphs in Quip and IC3

Formal verification is one of the fastest growing fields in verification. The Boolean satisfiability-based unbounded model checking algorithm of IC3 has become widely applied in industry and is frequently used as a subroutine in other formal verification algorithms, such as FAIR and IICTL. Any improvement to IC3 can therefore yield substantial benefits in many areas of formal verification. Towards that end, this paper introduces the notion of a support graph, which is applied in IC3. Techniques are presented to compute the support graph by modifying the satisfiability queries used in IC3 at the cost of a modest increase in runtime. It is used to increase the re-use of information across runs of the model checker, thereby improving runtime performance in incremental model checking. It can also be applied within a single run of the model checker to avoid unnecessary queries to the satisfiability solver and accelerate the discovery of a proof. Experiments are presented on HWMCC'15 circuits demonstrating the benefits of the presented approaches.

I. Introduction

Verification is the primary bottleneck in hardware design, consuming an average of 57% of the total project time [1]. Formal verification is one of the fastest growing segments in the field [1]. Of particular importance in formal verification is the problem of unbounded model checking, which asks if particular states are reachable in a circuit. IC3 [2] (also known as Property-Directed Reachability (PDR) [3]), has established itself as one of the state-of-the-art model checking techniques, and is now widely applied in industry [4], [5]. IC3 has been generalized to other domains such as software model checking [6], [7] and is frequently used as a subroutine in other algorithms [8], [9]. Any improvements to IC3 can therefore have wide-reaching impact in many areas of formal verification.