FormalRTL: Verified RTL Synthesis at Scale

本文提出了 FormalRTL，一种通过集成软件参考模型作为形式化规范来指导生成与验证、从而解决工业级数据路径设计挑战的可扩展多智能体框架。

要点

这篇论文介绍了一个名为 FormalRTL 的新系统，它的核心目标是解决一个让芯片工程师头疼的大问题：如何用人工智能（AI）自动写出既复杂又绝对正确的硬件代码？

为了让你轻松理解，我们可以把设计芯片比作建造一座摩天大楼。

1. 背景：为什么现在的 AI 造不出“摩天大楼”？

过去，AI（大语言模型）在写简单的代码（比如盖个狗窝或小亭子）上表现不错。但在芯片设计领域，尤其是那些处理海量数据的“数据通路”（Datapath）设计，AI 经常“翻车”。

• 问题一：图纸太模糊。 如果只给 AI 一句自然语言指令（比如“造个能算浮点数的单元”），就像只给建筑师一句“我要个漂亮的房子”。AI 可能会盖出个外观不错但内部结构混乱的房子，甚至地基都打歪了。
• 问题二：测试不够严谨。 传统的测试方法就像“试错法”：盖好一部分，试着用用，看坏没坏。但对于复杂的芯片，这种测试很难覆盖所有极端情况（比如暴雨天、地震时房子会不会塌）。一旦芯片流片（正式生产）后发现有个小 bug，损失就是几百万美元。

2. 核心创新：FormalRTL 的“三驾马车”

FormalRTL 并没有让 AI 直接“拍脑袋”写代码，而是引入了一套**“有参照、有监督、有纠错”的自动化流程。我们可以把它想象成一个超级建筑监理团队**，由三个智能角色组成：

🏗️ 角色一：规划师 (Planning Agent) —— “拿着图纸拆任务”

• 传统做法： 让 AI 直接盖整栋楼，容易晕头转向。
• FormalRTL 做法： 系统里有一份**“软件参考模型”（通常是用 C/C++ 写的，逻辑非常清晰，相当于大楼的完美设计蓝图**）。
  • 规划师先拿着这份蓝图，用静态分析工具把大楼拆解成一个个小房间（子模块）。
  • 它确保每个小房间的任务都清晰明确，并且按照依赖关系（先打地基，再砌墙，最后封顶）安排施工顺序。
  • 比喻： 就像把盖摩天大楼的任务，拆解成“先盖 A 区地基”、“再盖 B 区墙体”，每个小任务都有明确的图纸，不让 AI 一次性面对几千行代码的混乱。

🧱 角色二：施工队 (Initializing Agent) —— “边盖边对照”

• 任务： 根据规划师分派的小任务，生成硬件代码（RTL）。
• 关键创新： 施工队不仅仅是写代码，它还会同时生成一个“测试环境”。
  • 这个环境会拿着 AI 盖好的“硬件房间”和之前的“软件蓝图”（C 代码）进行实时比对。
  • 比喻： 就像每砌好一面墙，立刻拿尺子量一下，看看是不是和蓝图完全一致。如果不一致，马上知道哪里错了，而不是等楼盖完了再发现。

🔍 角色三：纠错员 (Debugging Agent) —— “拿着错题本改错”

• 任务： 当比对发现错误时，谁来修？
• 传统做法： 告诉 AI“这里错了”，AI 可能猜半天。
• FormalRTL 做法： 使用**形式化等价检查（Formal EC）**工具。
  • 这个工具不仅能说“错了”，还能给出**“反例”（Counterexample）**。它会具体指出：“在第 134 个状态，输入是 A，你的输出是 B，但蓝图要求是 C。”
  • 纠错员把这些具体的“错题”整理好，喂给 AI，让它精准修改。
  • 比喻： 就像老师批改作业，不是只打个红叉，而是圈出具体哪一步算错了，并告诉你正确答案应该是多少。AI 看着这个“错题本”，就能迅速修正，而不是盲目重试。

3. 为什么这个系统很厉害？

论文通过一系列工业级的测试（比如处理复杂的浮点运算、AI 芯片常用的数据类型）证明了：

1. 规模大： 以前 AI 只能写几百行代码，现在能搞定上千行甚至更复杂的工业级模块。
2. 准确率高： 通过“蓝图比对”和“错题本纠错”，最终生成的代码几乎 100% 能通过验证。
3. 效率高： 它把原本需要人类工程师几个月的工作，变成了自动化的流水线。

4. 总结与比喻

如果把芯片设计比作做一道极其复杂的满汉全席：

• 以前的 AI： 厨师（AI）看着菜单（自然语言描述），凭感觉炒菜。偶尔能做出好吃的，但经常盐放多了，或者把糖当成盐，而且很难保证每一道菜都完美。
• FormalRTL：
  • 规划师先把菜单拆解成“切菜”、“炒菜”、“摆盘”等具体步骤，并对照标准食谱（C 代码参考模型）。
  • 施工队每做一步，就对照食谱检查味道。
  • 纠错员如果尝出咸了，会直接告诉厨师：“第 3 步盐放多了 2 克，请减掉”，而不是只说“不好吃”。

最终结果： FormalRTL 让 AI 从“凭感觉的野厨师”变成了“拿着标准食谱和精密仪器的专业大厨”，能够大规模、高可靠地制造出复杂的芯片逻辑。

这篇论文最大的贡献就是开源了这套系统和一套工业级的测试题库，让未来的研究者也能在这个基础上，继续把 AI 造芯片的能力推向新的高度。

技术摘要

1. 研究背景与问题 (Problem)

随着 AI 工作负载的扩展，GPU、NPU 等计算密集型芯片的设计已成为工程瓶颈。虽然 LLM 在代码生成方面表现出色，但在工业级、数据路径（datapath）密集的硬件 RTL 合成中仍面临两大核心挑战：

1. 大规模设计复杂性：工业级 IP 核心通常需要数千行 RTL 代码。现有的基于规划的方法往往依赖模糊的自然语言规范，导致 LLM 难以做出正确的架构决策，且难以处理复杂的依赖关系。
2. 复杂的算术与逻辑结构：工业 IP 常包含深层嵌套的数据路径和自定义数据类型（如 bfloat16, hifloat8）。传统的基于仿真的验证方法难以覆盖所有边界情况（Corner Cases），无法提供形式化的正确性保证。

核心痛点：现有的 LLM 驱动方法直接从自然语言生成 RTL，缺乏形式化验证，导致生成的代码在工业场景中不可靠。工业界通常依赖 C/C++ 参考模型作为“黄金规范”进行等价性检查（Equivalence Checking, EC），但这一宝贵资源在现有的 LLM 合成流程中被忽视了。

2. 方法论 (Methodology)

FormalRTL 是一个新颖的端到端多智能体框架，其核心创新在于将软件参考模型（C/C++）作为形式化、可执行的规范，引导整个 RTL 生成和验证过程。

核心流程与智能体架构：

1. 规划智能体 (Planning Agent)：

   • 输入：C 参考模型和自然语言规范。
   • 机制：利用 C 编译器（Clang）进行静态分析（解析抽象语法树 AST），分析函数依赖关系。
   • 策略：将复杂设计分解为模块化的子任务，并严格按照依赖关系的拓扑顺序（Topological Order）生成。这比单纯依赖自然语言规划更可靠，且限制了等价性检查的规模。

2. 初始化智能体 (Initializing Agent)：

   • 任务：针对每个子模块，生成初始 RTL 代码和对应的验证 Harness。
   • Harness 构建：建立 C 代码与 RTL 代码的验证环境，假设输入相同并断言输出等价。
   • 时序控制：根据规范确定时序逻辑的时间范围（时钟周期数），以支持事务级等价性检查（Transactional EC）。

3. 调试智能体 (Debugging Agent)：

   • 反馈机制：利用形式化等价性检查工具（hw-cbmc）提供的反馈。
   • 错误处理：
     • 语法错误：使用 Bug Locator 定位错误行并提取上下文代码。
     • 反例 (Counterexamples)：使用 CE Simplifier 简化报告，仅展示问题函数和信号不匹配的具体值。
   • 闭环修正：LLM 根据上述结构化反馈生成补丁（Patch），迭代修正代码，直到通过等价性检查。

技术栈：

• LLM 选择：规划使用 GPT-4.1，生成和复杂调试使用 GPT-5。
• 验证工具：hw-cbmc（用于 C-RTL 形式化等价性检查）。
• 基准测试：构建了包含学术（Softfloat FP16）和工业（Ascend AI 芯片的 Hifloat8）场景的新基准套件。

3. 主要贡献 (Key Contributions)

1. 首创软件参考模型驱动的方法论：提出了一种利用 C 参考模型进行静态分析规划和等价性检查的新范式，确保了硬件生成的可扩展性和正确性。
2. 端到端多智能体引擎：开发了从规划、合成、调试到形式化验证的全自动工作流，实现了“生成即验证”。
3. 工业级基准套件：构建并开源了一套包含复杂数据路径模块（如 FP16 和 Hifloat8 运算器）的基准测试，提供了规格说明和对应的软件参考模型，填补了该领域缺乏工业级基准的空白。

4. 实验结果 (Results)

在包含 1000+ 行代码的复杂模块上进行了广泛评估：

• 最终成功率 (FSR)：在迭代限制内，所有子模块均达到了较高的最终成功率（大部分模块达到 95%-100%）。即使是复杂的顺序逻辑电路，FSR 也保持在 70%-80%。
• 初始成功率 (ISR)：许多模块的初始生成成功率较低（如 Hifloat8 乘法器仅为 15%），这突显了当前 LLM 直接生成的局限性，但也证明了调试智能体的必要性。
• 规划方法对比 (Ablation Study)：
  • 与仅依赖自然语言规范的基线方法相比，FormalRTL 在处理大规模设计（如 1000+ 行代码）时表现显著更优。
  • 基线方法在复杂设计上的成功率降至 0%，而 FormalRTL 保持了高稳定性。
  • 自底向上的验证策略（先验证依赖模块）显著降低了顶层模块的调试负担。
• 调试工具有效性：
  • 移除“反例引导调试”会导致成功率大幅下降（从 95% 降至 55%），证明形式化反例比单纯的 Pass/Fail 反馈更有效。
  • Bug Locator 和 CE Simplifier 显著减少了修复所需的迭代次数。
• 质量 (QoR)：虽然 LLM 生成的 RTL 在面积和延迟上略逊于人工优化的设计（这是为了优先保证功能正确性），但它为工程师提供了一个可执行、经过验证的基线，极大地加速了后续的 PPA（性能、功耗、面积）优化迭代。

5. 意义与展望 (Significance & Future Work)

• 缩小学术与工业的差距：FormalRTL 证明了利用形式化验证和软件参考模型，LLM 可以生成工业级复杂度的硬件代码，解决了当前原型系统无法落地的关键问题。
• 提升开发效率：通过自动化生成和验证，减少了人工编写测试用例和调试的时间，使硬件开发更加敏捷。
• 未来方向：
  • 进一步扩展至更大规模的工业 RTL 设计。
  • 训练专门针对反例修复的小型专用模型，降低对昂贵商业 LLM 的依赖。
  • 推动开源 C-RTL 等价性检查工具的发展，以支持更现代的 RTL 语法。

总结：FormalRTL 通过引入“软件参考模型”作为核心锚点，结合静态分析和形式化验证，成功构建了一个可靠、可扩展的硬件合成框架，为 LLM 在工业级芯片设计中的实际应用提供了重要的技术路径。