Word-Level Augmentation of Formal Proof by Learning from Simulation Traces

Abstract

Formal verification has been widely adopted to check logic correctness. One of the challenges in formal verification is how to quickly reach a formal proof for a user-specified property. This is especially difficult when the property involves word-level reasoning. In this work, we propose to augment the target property with additional conjectures automatically learned from simulation traces. The conjectures are generated by a reinforcement learning model, which dynamically expands production rules according to observations from simulation. Experiments show that our property strengthening method achieves notable speed-up on multiple verification tasks, including sequential equivalence checking and word-level property checking.

Zhiyuan Yan

Ph.D. student in Microelectronics Thrust

My research interests include hardware formal verification, AI for EDA and Boolean Satisfiability Problem.