Extended CTG Generalization and Dynamic Adjustment of Generalization Strategies in IC3

TL;DR

This paper enhances the IC3 verification algorithm by extending the CTG generalization method and introducing a dynamic strategy to balance generalization quality and computational efficiency, leading to improved scalability.

Contribution

It proposes an extended CTG method (EXCTG) for better generalization and a dynamic adjustment approach (DynAMic) to optimize performance versus overhead in IC3.

Findings

EXCTG improves generalization results over CTG.

DynAMic dynamically balances generalization quality and efficiency.

Both methods significantly increase the number of solvable cases.

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.