Formal that "Floats" High: Formal Verification of Floating Point Arithmetic

本文提出了一种结合分治策略、反例引导精化及人机协同 AI 辅助的扩展方法论，通过直接 RTL 到 RTL 的模型检查实现了对浮点运算的高效形式化验证，显著提升了覆盖率并减少了断言数量。

要点

这篇论文讲述了一个关于如何确保计算机“浮点数”（小数）计算绝对正确的故事。

想象一下，计算机里的数字世界分为两类：一类是像“整数”（1, 2, 3）这样简单的数字，另一类是像“浮点数”（3.14159, 0.0001）这样复杂的小数。处理小数的电路（我们叫它“浮点运算单元”）非常精密，就像一台极其复杂的瑞士手表，里面充满了齿轮、发条和微小的弹簧。如果其中一个小齿轮歪了，手表可能看起来还在走，但时间早就错了。在航空航天或医疗设备的芯片里，这种错误可能是灾难性的。

这篇论文提出了一套全新的“质检”方法，并引入了AI 助手来帮忙，让这个过程变得更快、更准。

以下是用通俗语言和大白话对这篇论文的解读：

1. 以前的难题：翻译带来的“失真”

以前，工程师想检查这些精密电路对不对，通常的做法是：

• 写一个高级的“说明书”（用 C 语言写一个理想模型）。
• 把电路设计“翻译”成这个说明书，然后让电脑去比对。

这就像什么？
就像你要检查一个由乐高积木搭成的复杂城堡（硬件电路）是否完美。以前的方法是：先让人用文字描述这个城堡（C 语言模型），然后让电脑把乐高城堡“翻译”成文字描述，再对比两篇文字。
问题在于： 翻译过程很容易出错，或者为了简化，把一些关键的细节（比如某个积木的微小缝隙）给漏掉了。这就叫“抽象差距”。如果翻译错了，你根本不知道是城堡搭错了，还是翻译官水平不行。

2. 新方案：直接“实物对实物”

这篇论文提出的新方法非常直接：扔掉翻译官，直接拿“实物”比“实物”。

• 黄金标准（Golden Reference）： 工程师先造一个“完美版”的电路（虽然它可能运行得慢，像一辆笨重的老爷车，但它绝对正确，符合数学规则）。
• 待测版（Implementation）： 这是工程师实际要用的电路（像一辆经过改装的赛车，追求速度，但可能有瑕疵）。
• 直接比对： 让这两辆车同时跑，输入完全一样的指令，看它们输出的结果是否分毫不差。

比喻：
这就好比你要检查一把新做的尺子准不准。以前的方法是把尺子画成图纸，再拿图纸去量；现在的方法是，直接拿这把新尺子和一把国家标准的原子钟尺子（黄金标准）放在一起，量同一个东西。如果两者量出来的结果一样，那就绝对没问题。

3. 核心策略：化整为零（分而治之）

浮点运算太复杂了，一次性比对整个大电路，电脑会“死机”（算不过来）。
新方法怎么做？
就像你要检查一座大桥是否结实，你不会试图一次性检查整座桥。你会把桥拆成几个部分：

1. 对齐阶段： 先把两根不同长度的绳子（小数）对齐。
2. 计算阶段： 把对齐后的绳子接起来，再修剪整齐。

论文把电路也拆成这两个“小房间”（模块），分别检查。如果第一个房间没问题，再检查第二个。这样，电脑处理起来就轻松多了，就像玩拼图一样，一块一块地拼，最后拼成完美的整体。

4. 引入 AI 助手：从“人工写题”到"AI 出题”

这是论文最酷的部分。以前，工程师需要 manually（手动）写很多“检查规则”（就像老师出题考学生），告诉电脑：“如果输入是 A，输出必须是 B"。这需要极高的专业知识和大量时间。

现在的做法：

• AI 代理（Agentic AI）： 作者训练了一群 AI 助手（像 GPT-5 这样的模型）。
• 工作流程：
  1. 策划员 AI： 阅读设计图纸，制定检查计划。
  2. 出题员 AI： 根据计划，自动生成那些“检查规则”（代码）。
  3. 挑刺员 AI： 检查这些规则有没有逻辑漏洞。
  4. 纠错员 AI： 如果规则写错了，自动修改。
  5. 人类专家（HITL）： 如果 AI 卡住了，人类专家介入，像导师一样点拨一下：“嘿，这里要注意小数点的进位规则。”

比喻：
以前是老师（工程师）一个人熬夜出题、改卷。现在是一个AI 助教团队在帮忙出题，老师只需要最后把关，指出哪里出错了。结果发现，AI 出的题虽然一开始有点啰嗦（重复），但经过老师点拨后，效率极高，甚至能发现人类容易忽略的死角。

5. 实验结果：AI 真的行吗？

作者做了两个实验：

1. 有“标准答案”（黄金模型）时： AI 生成的检查规则非常有效，甚至比人类写的更精简，覆盖率高达 98% 以上。这意味着只要有人类专家稍微指导一下，AI 就能完美工作。
2. 没有“标准答案”时： 如果只给 AI 看待测电路，没有那个“完美版”做对比，AI 就会有点“晕”，生成的规则很多都跑不通，覆盖率下降。这说明 AI 目前还不太懂那些深奥的“微架构”细节，需要人类专家更多的指导。

总结：这篇论文到底说了什么？

这篇论文告诉我们：

1. 别搞翻译了： 检查芯片里的浮点运算，直接用“电路对电路”比对着最准，别通过 C 语言翻译。
2. 拆解是王道： 把大难题拆成小模块，逐个击破。
3. AI 是神助攻： 用 AI 自动生成检查规则，配合人类专家的“点睛之笔”，可以大幅提高效率，发现更多隐藏的错误。

一句话概括：
这就好比给精密仪器做质检，以前靠人工翻译图纸比对，现在直接拿“完美原型”和“成品”硬碰硬，再请一群 AI 助手帮忙写检查清单，人类专家只需最后拍板，既快又准，还能防住那些最狡猾的 Bug。

技术摘要

这是一份关于论文《Formal Verification of Floating Point Arithmetic》（浮点运算的形式化验证）的详细技术总结，该论文拟发表于 2025 年第 37 届 IEEE 微电子国际会议（ICM）。

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

• 核心挑战：浮点运算单元（FPU）的形式化验证极具挑战性。主要原因包括非线性的算术行为、控制逻辑与数据通路逻辑的紧密耦合，以及严格的 IEEE-754 合规性要求（如溢出、下溢、非规格化数、舍入等边缘情况）。
• 现有方法的局限性：
  • 现有的验证方法通常依赖高级 C 模型与寄存器传输级（RTL）设计进行等价性检查。
  • 这种方法引入了抽象间隙（Abstraction Gaps）和翻译开销，导致 C 模型语义与硬件执行不匹配。
  • 对于数据密集型（datapath-intensive）的 RTL 设计，基于 C 的转换流程在可扩展性（Scalability）和模型维护方面存在瓶颈。
  • 缺乏直接针对 RTL 层面的精确验证手段。

2. 方法论 (Methodology)

本文提出了一种可扩展的直接 RTL 到 RTL（RTL-to-RTL）模型检查方法，用于验证浮点加法器。该方法不依赖高级 C 模型，而是直接对比 RTL 实现与黄金参考模型（Golden Reference Model）。

• 分治策略（Divide-and-Conquer）：
  • 将浮点加法器在层次上分解为两个模块化阶段：尾数对齐阶段（Mantissa Alignment Stage）和加法 - 舍入阶段（Add-Round Stage）。
  • 通过辅助断言（Helper Assertions）和引理（Lemmas）来证明主正确性定理，从而降低证明复杂度并提高收敛性。
• 反例引导的细化（CEX-guided Refinement）：
  • 利用形式化工具生成的反例（Counterexamples, CEX）来迭代定位实现缺陷。
  • 通过细化断言和修复实现逻辑，逐步消除不匹配，直至证明功能等价。
• 故障注入（Fault Injection）：
  • 在 RTL 实现中系统性地注入受控故障（如粘滞位失真、操作数选择错误、舍入规则违反等），以评估验证流程的鲁棒性和断言检测精度关键缺陷的能力。
• 基于代理 AI 的属性生成（Agentic AI-based Property Generation）：
  • 引入多智能体系统（Multi-Agent System, MAS），结合大语言模型（LLM，如 GPT-5, Llama3.3）与**人在回路（Human-in-the-Loop, HITL）**机制。
  • 工作流：
    1. 规划：Lead Agent 解析设计意图，生成结构化验证计划（vPlan）。
    2. 生成：Property Generation Agent 将 vPlan 转化为 SystemVerilog 断言（SVA）。
    3. 审查与修正：Critic Agent 评估逻辑正确性，Error Correction Agent 修复语法/语义错误。
    4. 执行与反馈：Executor Agent 运行形式化工具，分析覆盖率，若未收敛则引入 HITL 指导进行细化。

3. 关键贡献 (Key Contributions)

1. 直接 RTL-to-RTL 模型检查：提出了一种无需依赖高级 C 模型或 HLS 转换流的验证方法，直接对比 RTL 实现与黄金参考模型，消除了语义翻译开销。
2. 基于属性的分层验证：通过分治策略将复杂设计分解为模块化阶段，利用引理和断言确保正确性，显著提升了证明的可扩展性。
3. 缺陷检测与形式化证明：成功识别并修复了实现中的具体缺陷（如操作数选择逻辑错误、指数行为未约束等），并完成了对黄金模型的等价性证明。
4. AI 辅助属性生成的评估：系统评估了 LLM 生成断言在手写断言对比下的表现，特别是在有参考模型和无参考模型两种场景下的覆盖率和效率。
5. 鲁棒性验证：通过故障注入实验，验证了该方法能有效检测数据通路中的精度关键错误。

4. 实验结果 (Results)

实验在 Cadence Jasper 平台上进行，针对单精度浮点加法器设计：

• 故障检测：
  • 在尾数对齐和加法 - 舍入阶段注入的多种故障（如粘滞位错误、移位错误、舍入规则违反）均被形式化属性成功检测。
• 覆盖率与效率对比（RTL-to-RTL 模式）：
  • 手写断言：仅需 2 个 断言，证明时间 0.073 秒，形式化覆盖率达到 98.42%。
  • LLM 生成（无 HITL）：初始生成的断言数量较多（7-15 个），存在冗余，且证明时间较长（1.7s - 12.8s），覆盖率未显著提升。
  • LLM 生成（有 HITL）：经过人工细化后，断言数量减少至 3-6 个，消除了冗余和 CEX。例如，GPT-5 仅需 3 个 断言，证明时间 1.318 秒，即达到了与手写断言相当的覆盖率。
• 独立 RTL 验证（无参考模型）：
  • 在没有黄金参考模型的情况下，LLM 生成的属性覆盖率显著下降（约 62%-90%），且存在大量不可达（Unreachable）项。
  • 这表明在没有微架构指导的情况下，LLM 难以准确约束有效的设计行为空间，需要大量 HITL 干预来添加特定的微架构检查（如粘滞位传播、归一化深度等）。

5. 意义与结论 (Significance & Conclusion)

• 方法论创新：该研究证明了直接 RTL-to-RTL 模型检查在浮点运算验证中的可行性和高效性，避免了传统 C 模型方法的抽象间隙问题。
• AI 在形式化验证中的角色：
  • 在有参考模型的场景下，AI 生成的属性经过 HITL 细化后，可以达到与专家手写属性相当的效果，但初始生成往往存在冗余。
  • 在无参考模型场景下，当前 LLM 仍难以独立捕捉完整的可达状态空间，HITL 指导对于约束微架构行为至关重要。
• 未来展望：该方法为可扩展的 AI 辅助形式化验证奠定了基础。未来的工作将探索如何更有效地从微架构意图中提取信息，以指导 LLM 进行属性合成，从而进一步减少人工细化工作量，并扩展至更复杂的 FPU（如乘法器、除法器）。

总结：本文提出了一种结合分层分解、直接 RTL 比对和 AI 辅助属性生成的新型浮点运算验证流程。实验表明，该流程不仅高效且鲁棒，特别是在引入人在回路（HITL）机制后，AI 生成的属性能够显著提升验证效率，为复杂算术数据通路的自动化验证提供了新的范式。