收录解读
这篇论文针对 LLM 生成 RTL/Verilog 代码时最关键的可靠性缺口：仅靠语法检查或有限 testbench 仿真，很难保证时序语义、协议边界和局部修复后的不回归。作者把 RTL 代码生成重构为一个带共享设计契约、时序追踪、局部补丁和形式化验证的多代理闭环，而不是普通的单次生成或反复全文件重写。
方法上，Veri-Sure 先由 architect agent 将自然语言规格转为结构化 design contract，再由 generator / verifier / debugger 等代理围绕同一契约协作。失败时，系统用波形追踪和静态依赖切片定位可疑逻辑，只对局部片段打补丁；同时引入 assertion-based checking 和 Boolean equivalence proof，让反馈不只来自有限仿真样例。
论文还提出 VerilogEval-v2-EXT，在原 VerilogEval-v2 基础上补充 53 个更接近工业 RTL 的任务，并按难度分层。实验显示，在该扩展基准上，Veri-Sure with GPT-5.2 的整体 functional Pass@1 达到 93.30%，hard subset 达到 85.07%，明显高于 standalone GPT-5.2 和单代理 simulator feedback；消融也表明 tracing/slicing/patching 与 formal verification 是主要增益来源。
它值得正式收录，因为它体现了 AI-for-hardware 工作流的一条可复用模式：让 agentic code generation 受共享契约、可定位修复和形式化工具共同约束，而不是只追求生成模型本身更强。局限是验证仍在公开扩展基准和作者框架内完成，依赖强闭源模型作为主要上限，距离真实工业 SoC 流水线的端到端采用还有距离，因此定为 breakthrough 而不是 disruptive。