Extended CTG Generalization and Dynamic Adjustment of Generalization Strategies in IC3

TL;DR

This paper tackles scalability bottlenecks in IC3 generalization by introducing Extended CTG Generalization (EXCTG) and DynAMic dynamic strategy adjustment. EXCTG recursively blocks the CTG predecessors to achieve finer generalization, while DynAMic adapts the generalization strategy based on blocking difficulty, using thresholds to switch among Standard, CTG, and EXCTG. On HWMCC'19/20 benchmarks, EXCTG solves $8$ more cases than CTG, and DynAMic solves $25$ more cases than CTG and $17$ more than EXCTG, highlighting the tradeoff between generalization quality and overhead. Overall, these methods offer a practical approach to balance generalization effectiveness and computational cost, improving IC3-based hardware verification scalability.

Abstract

The IC3 algorithm is widely used in hardware formal verification, with generalization as a crucial step. Standard generalization expands a cube by dropping literals to include more unreachable states. The CTG approach enhances this by blocking counterexamples to generalization (CTG) when dropping literals fails. In this paper, we extend the CTG method (EXCTG) to put more effort into generalization. If blocking the CTG fails, EXCTG attempts to block its predecessors, aiming for better generalization. While CTG and EXCTG offer better generalization results, they also come with increased computational overhead. Finding an appropriate balance between generalization quality and computational overhead is challenging with a static strategy. We propose DynAMic, a method that dynamically adjusts generalization strategies according to the difficulty of blocking states, thereby improving scalability without compromising efficiency. A comprehensive evaluation demonstrates that EXCTG and DynAMic achieve significant scalability improvements, solving 8 and 25 more cases, respectively, compared to CTG generalization.

Figures (5)

• Figure 1: $p_0$, $p_1$, and $cand$ are cubes representing states, where $p_0$ is the predecessor of $p_1$, and $p_1$ is the predecessor of $cand$. $I$ represents the initial states. The cubes in shaded areas represent a set of states attempting to block. These diagrams illustrate the process of the different generalization strategies.
• Figure 2: The relationships between Standard, CTG, and EXCTG.
• Figure 3: $c_0$ and $c_1$ represent bad states, and $p_i$ denote their predecessors. The dashed circle illustrates the state space generalized from $p_0$ or $p_4$ using different strategies.
• Figure 4: The number of cases solved by different configurations over time.
• Figure 5: This plot compares the solving times (in seconds) between different configurations.