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.
翻译:我们提出了一个算术RTL设计的正式核查方法,将逻辑等同测算与互动理论验证相结合。Verilog模块的中间模型在限制算法 C (RAC)中手工编码,这是C的原始子集,由C的整数和固定点登记册级模板加以补充。该模型的设计尽量抽象,但充分忠实于RTL,以便能够与商业工具进行有效的等同检查。然后,该模型被自动翻译成ACL2的逻辑,从而能够机械地核查正式建筑规格的正确性。我们在本文中描述了RAC语言、翻译过程以及一些有助于对由此产生的ACL2代码进行正式分析的技术。