算术 RTL 的形式验证：将 Verilog 翻译为 C++ 再到 ACL2
计算机科学中的逻辑
2020-09-30 v1 符号计算
摘要
我们提出了一种算术 RTL 设计形式验证的方法论，它将对序逻辑等价性检查与交互式定理证明相结合。Verilog 模块的中间模型以受限算法化 C（RAC）手工编码，RAC 是 C 的一个原始子集，由算法化 C 的整型和定点寄存器类模板增强。该模型被设计得尽可能抽象和紧凑，但对 RTL 足够忠实，以允许使用商业工具进行高效的等价性检查。随后它会被自动翻译到 ACL2 的逻辑中，从而能够针对形式化体系结构规范进行机械检查的正确性证明。在本文中，我们描述了 RAC 语言、翻译过程，以及有助于对所生成 ACL2 代码进行形式分析的一些技术。
引用
@article{arxiv.2009.13761,
title = {Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2},
author = {David M. Russinoff},
journal= {arXiv preprint arXiv:2009.13761},
year = {2020}
}
备注
In Proceedings ACL2 2020, arXiv:2009.12521