AI 中文总结
本文提出Rtl2lean框架，自动将RTL设计转为Lean 4模型并构建分层定理库。通过四层定理框架和基于大语言模型的证明循环处理验证。实验表明该框架能构建机器检查的RTL证明库，检查开销低且引理重用性高。
AI 中文摘要
使用交互式定理证明器进行形式验证可为寄存器传输级设计提供强大的正确性保证，但将其应用于现有的SystemVerilog代码需要在语义建模和证明构建方面付出大量的人工。本文提出了Rtl2lean框架，它能自动将寄存器传输级（RTL）设计转换为可执行的Lean 4模型，并构建分层定理库以供后续验证。生成的模型将硬件执行表示为纯状态转换函数，同时四层定理框架捕获组合语义、顺序更新、单周期行为以及可达性和不变性。当现有定理库无法证明高层属性时，基于大语言模型的证明循环会根据当前证明上下文和Lean反馈提出中间引理。只有被Lean内核接受的引理才会被添加到可重用引理池中。对六个SystemVerilog设计进行的实验生成了403个定理，所有这些定理都被Lean成功验证。在358个基础引理中，287个可自动重用，可重用引理比率为80.2%。结果表明，Rtl2lean可以构建机器检查的RTL证明库，且检查开销低，跨属性引理重用性高。
英文摘要
Formal verification with interactive theorem provers can provide strong correctness guarantees for register transfer level designs, but applying it to existing SystemVerilog code requires substantial manual effort in semantic modeling and proof construction. This paper presents Rtl2lean, a framework that automatically translates RTL designs into executable Lean 4 models and builds a hierarchical theorem library for subsequent verification. The generated model represents hardware execution as a pure state transition function, while a four layer theorem framework captures combinational semantics, sequential updates, single cycle behavior, and reachability and invariants. When a high level property cannot be discharged by the existing theorem base, an LLM based proving loop proposes intermediate lemmas from the current proof context and Lean feedback. Only lemmas accepted by the Lean kernel are added to the reusable lemma pool. Experiments on six SystemVerilog designs generate 403 theorems, all of which are successfully checked by Lean. Among 358 foundational lemmas, 287 are available for automatic reuse, yielding a reusable lemma ratio of 80.2 percent. The results demonstrate that Rtl2lean can construct machine checked RTL proof libraries with low checking overhead and substantial cross property lemma reuse.
Comments6 pages, 2 figures
