We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Model checking answers the question of whether every execution of a given system satisfies a desired temporal logic specification. Unlike testing, model checking provides formal guarantees. Its application is expected standard in silicon design and the EDA industry has invested decades into the development of performant symbolic model checking algorithms. Our new approach combines machine learning and symbolic reasoning by using neural networks as formal proof certificates for linear temporal logic. We train our neural certificates from randomly generated executions of the system and we then symbolically check their validity using satisfiability solving which, upon the affirmative answer, establishes that the system provably satisfies the specification. We leverage the expressive power of neural networks to represent proof certificates as well as the fact that checking a certificate is much simpler than finding one. As a result, our machine learning procedure for model checking is entirely unsupervised, formally sound, and practically effective. We experimentally demonstrate that our method outperforms the state-of-the-art academic and commercial model checkers on a set of standard hardware designs written in SystemVerilog.

翻译：本文提出一种用于模型检验时序逻辑的机器学习方法，并应用于形式化硬件验证。模型检验旨在回答给定系统的所有执行是否均满足期望的时序逻辑规约。与测试不同，模型检验能提供形式化保证。其在芯片设计中的应用已成为行业标准，电子设计自动化产业已投入数十年研发高性能符号模型检验算法。我们的新方法通过使用神经网络作为线性时序逻辑的形式化证明证书，将机器学习与符号推理相结合。我们从系统随机生成的执行轨迹中训练神经证书，随后通过可满足性求解进行符号化验证——若验证通过，则可证明系统满足规约。我们利用神经网络的表达能力来表征证明证书，并基于“检验证书比寻找证书更简单”这一事实。因此，我们的模型检验机器学习流程完全无需监督、具有形式化可靠性且实际有效。实验结果表明，在基于SystemVerilog编写的一组标准硬件设计案例中，本方法优于当前最先进的学术与商业模型检验工具。