Search papers, labs, and topics across Lattice.
This paper introduces A-IC3, a novel framework that uses a multi-armed bandit (MAB) algorithm to dynamically select inductive generalization strategies within the IC3 hardware model checking algorithm. By adaptively choosing strategies based on real-time feedback from the verification process, A-IC3 overcomes the limitations of fixed generalization strategies. Experiments on 914 hardware model checking instances show that A-IC3, when integrated with rIC3, solves 26-50 more cases and significantly improves the PAR-2 score compared to baselines.
Stop guessing which inductive generalization strategy works best for IC3 – this adaptive, learning-guided approach solves significantly more hardware model checking problems.
The IC3 algorithm represents the state-of-the-art (SOTA) hardware model checking technique, owing to its robust performance and scalability. A significant body of research has focused on enhancing the solving efficiency of the IC3 algorithm, with particular attention to the inductive generalization process: a critical phase wherein the algorithm seeks to generalize a counterexample to inductiveness (CTI), which typically is a state leading to a bad state, into a broader set of states. This inductive generalization is a primary source of clauses in IC3 and thus plays a pivotal role in determining the overall effectiveness of the algorithm. Despite its importance, existing approaches often rely on fixed inductive generalization strategies, overlooking the dynamic and context-sensitive nature of the verification environment in which spurious counterexamples arise. This rigidity can limit the quality of generated clauses and, consequently, the performance of IC3. To address this limitation, we propose a lightweight machine-learning-based framework that dynamically selects appropriate inductive generalization strategies in response to the evolving verification context. Specifically, we employ a multi-armed bandit (MAB) algorithm to adaptively choose inductive generalization strategies based on real-time feedback from the verification process. The agent is updated by evaluating the quality of generalization outcomes, thereby refining its strategy selection over time. Empirical evaluation on a benchmark suite comprising 914 instances, primarily drawn from the latest HWMCC collection, demonstrates the efficacy of our approach. When implemented on the state-of-the-art model checker rIC3, our method solves 26 to 50 more cases than the baselines and improves the PAR-2 score by 194.72 to 389.29.
