核心问题：当 RTL 与验证它的断言都由同一份中间规格生成时，形式化证明是在确认原始设计意图，还是只在确认两份产物彼此一致？

论文卡片

  • 原题： LLM-enabled Behavior Driven Development Workflow for Formally Verified Hardware Designs
  • 作者： Luca Müller、Qian Liu、Rolf Drechsler。
  • 机构： DFKI、University of Bremen。
  • 版本： 2026-09-14，arXiv v1；分类为 cs.AR、cs.SE；12 页。
  • 定位： 受控自然语言规格、LLM 辅助 RTL 生成与形式化属性验证的实证型工作流论文。
  • 阅读入口： alphaXiv · arXiv · 免费全文 · PDF
  • 实验材料： 作者公开的评测产物。

论文讲了什么

论文认为，普通自然语言规格便于阅读，却容易含有歧义；完全形式化的规格精确，但不易由人审阅。作者把软件工程中的 Gherkin 改造成 Formal Verification Gherkin Scenario（FV Gherkin Scenario），试图在两者之间建立一种受控自然语言。

FV Gherkin 不再依赖少量示例值描述行为，而要求后置条件用前置条件中的信号或常量作符号化表达，并取消测试样例表。工作流先由 Gherkin Agent 把原始需求改写成这类场景，再分别由 Verilog Agent 生成 RTL、SVA Agent 生成 SystemVerilog Assertions；生成的断言与设计交给形式化验证工具检查。

这里存在两类反馈。Gherkin 是否符合形式、是否覆盖原始需求，主要由 LLM judge 判断；RTL 与 SVA 的语法、仿真结果和形式化覆盖，则由 Xcelium、JasperGold 等工具提供确定性反馈。论文的关键主张不是“让 LLM 直接写更多代码”，而是让一个结构化的中间规格同时约束设计与验证产物。

主要结果

作者使用 Claude Sonnet 5，并以严格的 pass@1 运行两组分开的实验。

在 RTL 路径上，工作流在 VerilogEval v2 的 156 个设计中达到 98.7% 语法通过率和 89.1% 功能通过率；在 ChipBench 的 45 个设计中分别为 95.6% 和 31.1%。论文摘要中的“功能正确性提高 2.48 倍”，特指相对作者重跑的 CodeV 在 VerilogEval v2 上从 35.9% 到 89.1%；它并非相对所有基线，因为重新评分的 VerilogCoder 达到 90.4%，而 ChipBench 上该工作流与重跑的 MAGE 同为 31.1%。

在 SVA 路径上，作者用 AssertLLM 和 AssertLLM2 评测生成断言。对 AssertLLM2 的 23 个设计子集，工作流的断言证明率为 43.1%、COI 覆盖为 92.9%、形式化覆盖为 39.5%；Plain 基线重跑结果分别为 67.8%、99.9% 和 15.5%。因此论文所说的“形式化覆盖提高 2.54 倍”，对应 39.5% 与 15.5%，同时不能忽略该工作流在另外两个指标上更低。

证据边界

论文提出的是一条端到端流程，但实验分别评估两条支路：生成的 RTL 由基准测试台检查；生成的 SVA 则在 golden RTL 上评分。实验没有直接证明“同一次运行中生成的 RTL 与生成的 SVA 通过形式化检查”就忠实实现了最初的自然语言需求。

这一区别很重要。形式化工具能够证明给定属性在给定设计上成立，却不能自行判断属性是否完整表达了人的原始意图。如果 Gherkin Agent 对需求作出了同一个错误解释，RTL Agent 与 SVA Agent 可能共同继承该错误；两者彼此一致，仍不等于原始规格被正确理解。

此外，实验只采用一个基础模型；AssertLLM2 只评测了 23 个设计的子集；不同基线的可重跑程度并不一致。现有结果支持“FV Gherkin 是有希望的中间表示”，但还不足以把整条流程称为已经获得了端到端正确性保证。

重点读哪里

先读 §3.1，看 FV Gherkin 的三条定义如何把“示例行为”改写为“符号行为”；再读 §4.1.2，分辨摘要中的 2.48 倍比较了哪条基线；最后读 §4.2.2／表 7，同时比较证明率、COI 覆盖与形式化覆盖，而不要只看最大的提升倍数。

思考启发

以下是导读者由论文引出的理解角度，不是论文新增结论。

这篇论文把规格放在了一个特殊位置：它既是设计的来源，也是验证的来源。这样做可以减少设计与验证之间的表面偏差，却也可能让两者共享同一种误解。独立性与一致性在这里形成张力——越共享同一份表示，越容易保持一致；但如果源头错了，独立发现错误的机会也可能越少。

形式化证明的力量始终是相对于属性而言的。论文真正提醒人的，不只是“形式化工具可以给 Agent 反馈”，还有“谁来验证属性本身”。把自然语言改写为受控语言，并没有消灭解释，只是把解释集中到了一个更明确、也更值得审查的边界上。

三个思考问题

1. 同源生成的 RTL 与断言彼此吻合，能否增加我们对原始意图的信心？

如果二者继承了 Gherkin 中同一个误解，形式化证明还排除了哪些错误，又没有排除哪些错误？

展开思考线索

证明可以排除“设计违反当前断言”的情形，却不能排除“当前断言错误表达了需求”。共享中间规格提高了一致性，但一致性和忠实性是两种性质。判断信心是否增加，取决于中间规格是否获得了独立证据。

2. 受控自然语言是在消除歧义，还是在转移歧义？

FV Gherkin 限制了句式和取值表达，但原始需求到符号场景的转换仍由模型完成。歧义究竟消失在了哪里？

展开思考线索

结构化语法能消除一部分表达层面的含混，例如不再用有限示例暗示完整行为；语义选择却仍可能存在于信号对应、时序边界和遗漏条件中。更准确的说法也许不是“无歧义”，而是让歧义更集中、更可见。

3. 当证明率下降而形式化覆盖上升时，哪一组断言更好？

AssertLLM2 上，本文工作流的形式化覆盖更高，但证明率和 COI 覆盖低于 Plain 基线。这三个指标之间应如何排序？

展开思考线索

高证明率可能来自容易成立但约束较弱的属性；高覆盖也可能伴随错误或过强的属性。单个指标无法同时表达正确性、完整性和可证明性。这里的冲突说明“更好的断言集”本身就是一个多维概念，而不是一条单调刻度。