论文标题
算术RTL的形式验证：将Verilog转换为C ++为ACL2
Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2
论文作者
论文摘要
我们提出了一种对算术RTL设计形式验证的方法，该方法结合了顺序逻辑等效性检查与交互式定理证明。 Verilog模块的中间模型用受限的算法C（RAC）手工编码，RAC（RAC）是由整数和固定点寄存器寄存器类增强子集的原始子集，该模型的设计旨在尽可能抽象，紧凑，尽可能地忠实于RTL，以允许与RTL相等，以允许有效的等效工具。然后将其自动转换为ACL2的逻辑，从而使经过机械检查的正式体系结构规范的正确性证明。在本文中，我们描述了RAC语言，翻译过程以及一些有助于对所得ACL2代码进行正式分析的技术。
We present a methodology for formal verification of arithmetic RTL designs that combines sequential logic equivalence checking with interactive theorem proving. An intermediate model of a Verilog module is hand-coded in Restricted Algorithmic C (RAC), a primitive subset of C augmented by the integer and fixed-point register class templates of Algorithmic C. The model is designed to be as abstract and compact as possible, but sufficiently faithful to the RTL to allow efficient equivalence checking with a commercial tool. It is then automatically translated to the logic of ACL2, enabling a mechanically checked proof of correctness with respect to a formal architectural specification. In this paper, we describe the RAC language, the translation process, and some techniques that facilitate formal analysis of the resulting ACL2 code.
