NeuroPDR and DeepIC3

In recent years, machine learning has demonstrated its potential in many challenging problems. In NeuroPDR and DeepIC3, we extend its use to hardware formal property verification to take advantage of graph learning in the classic IC3/PDR algorithm. In both algorithms, graph neural networks are integrated to improve the result of local inductive generalization. This helps provide a global view of the state transition system and can potentially lead the algorithm out of local optima in the search of inductive invariants. NeuroPDR is our first attempt and is published in MLCAD 23. It is an online integration to predict relatively inductive clauses and implemented on a Python replica of the IC3/PDR algorithm. Though it demonstrates the potential of machine learning in accelerating hardware model checking algorithms, it bears the overhead of online inference. Therefore, we later propose DeepIC3 (an upgrade of NeuroPDR), featuring offline machine learning inference to further unleash the power of AI heuristics in model checking.

Our experiments demonstrate that DeepIC3 accelerates the vanilla algorithm in nontrivial test cases of hardware model checking competition benchmarks (HWMCC2020) with up to 10.8x speed-up. The proposed machine-learning integration preserves soundness and is universally applicable to various IC3/PDR implementations.