核心问题：如果“功能正确”只表示生成的断言能在当前 RTL 上被形式证明且不空洞，那么 82% 的分数证明了 Agent 抓住了重要设计意图，还是只证明它找到了当前实现中成立的性质？
论文卡片
- 原题： From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation
- 作者： Nowfel Mashnoor、Hadi Kamali、Kimia Azar。
- 机构： University of Central Florida。
- 版本： 2026-04-25，arXiv v1；cs.CR；IEEE VLSI Test Symposium 2026 Special Session 论文。
- 定位： 以 AST 检索、形式工具结构查询和 solver-in-the-loop 反馈辅助 LLM 生成 SystemVerilog Assertions（SVA）。
- 阅读入口： alphaXiv · arXiv · HTML 全文 · PDF
论文讲了什么
直接把 RTL 交给 LLM 生成 SVA，常见错误不只来自 SVA 语法。模型还可能引用不存在的信号、误判时钟与复位方式，或者没有追踪跨模块的扇入扇出关系。ProofLoop 的主张是：这些信息已经存在于编译器和形式工具中，Agent 不必仅靠上下文窗口猜测。
系统分成两个阶段。预处理先把 RTL 解析为 AST，再按模块接口、always 块、实例和连续赋值四类切片，嵌入向量数据库。Phase A 允许 ReAct Agent 最多进行六轮工具调用：它既能按语义检索 AST 片段、查询层次结构与参数，也能调用 JasperGold 获取信号扇入扇出、触发器的时钟、复位值和数据输入。
Phase B 根据收集的上下文生成 SVA，并最多进行三轮 JasperGold 验证。若出现编译错误或反例，错误消息与 counterexample trace 会回到 Agent，后者局部修改信号引用、时序算子或前件/后件。对于 proven 或 undetermined 的性质，流程还调用 vacuity analysis，试图区分真实约束与因前件不可达而自动成立的断言。
这不是让 LLM 替代形式工具，而是让形式工具同时承担三种角色：提供结构化设计知识、给出候选性质的证明状态、为下一轮生成提供机器可读的纠错证据。
主要结果
论文使用 FVEval 的 96 个流水线设计和 96 个 FSM 设计。主要模型为 Qwen3.5-35B，另以 Mistral-Small-3.1-24B 检验跨模型趋势；直接向同一模型提供原始 RTL、不给检索、结构工具和验证反馈，作为 direct-prompt baseline。
| 模型 | 方法 | 语法正确率 | 论文定义的功能正确率 |
|---|---|---|---|
| Qwen3.5-35B | Direct prompt | 78.3% | 43.2% |
| Qwen3.5-35B | ProofLoop | 93.7% | 82.0% |
| Mistral-Small-24B | Direct prompt | 65.8% | 31.1% |
| Mistral-Small-24B | ProofLoop | 85.5% | 53.3% |
这里的“功能正确率”定义为已证明断言数占全部生成断言数的比例，并非与一条人工金标准性质做逻辑等价。Design2SVA 的输入主要是 RTL 与 testbench 接口，问题要求模型生成“最重要”的断言；由于可能存在许多不同但都成立的性质，评测把形式工具能证明的候选视为功能通过。
36 个设计上的消融报告：完整流程为 82.0%，去掉 RAG 后为 70.9%，去掉验证循环后为 64.7%，去掉结构分析工具后为 58.4%，去掉全部工具后为 36.1%。这支持三类工具信息都与成绩有关；但消融不是全因子实验，不能由此证明组件彼此“正交”或把差值解释成可相加的独立贡献。
与原始 FVEval 模型结果比较时，ProofLoop 的 Qwen3.5-35B 在流水线设计上达到 Func@1 0.412、Func@5 0.896，在 FSM 上达到 0.860 和 0.958。这里每个设计运行五次、采用 nucleus sampling；Func@5 表示五次中至少一次生成了可证明断言，不等于单次稳定成功率。由于外部基线使用不同模型且没有 ProofLoop 的工具与三轮反馈，这张表比较的是完整系统，而不是单独的 backbone 能力。
证据边界
形式证明回答的是“这条 SVA 是否对当前 RTL 的所有被建模行为成立”。它不会自动回答“这条 SVA 是否表达了设计者原本想要的性质”。若 RTL 本身带有系统性错误，Agent 也可能抽取并证明错误实现中的规律；若断言只是重述局部赋值关系，它可以正确、非空洞，却未必覆盖最危险的行为。
Vacuity analysis 排除了部分“前件永远不触发”的假成功，但空洞性与价值不是同一个概念。一条频繁触发、永远成立的弱性质仍可能缺乏区分力。论文没有使用 mutation score、人工重要性标注或独立规格等证据，去检验生成断言能否杀死错误实现、发现已知 bug，或者覆盖设计意图中的关键风险。
论文对 vacuity 结果的处置也交代得不够完整。算法在证明状态为 proven 或 undetermined 时执行 vacuity check 后直接退出循环，没有写明检测为空洞后是否拒绝、重写或如何计入指标；正文称功能分数统计 proven assertions，但没有单列空洞、undetermined 与超时数量。因而 82.0% 的精确统计口径无法仅凭论文完整复核。
验证循环更擅长修复可定位的结构错误。论文报告 59.3% 的初始语法失败可由反馈修正；而 101 个初始被反例推翻的规格中，只有 20 个最终完全恢复。这一差异支持“工具反馈有帮助”，也说明从明确报错修语法与根据反例重建正确时序语义，仍是不同难度的推理问题。
重点读哪里
先读 §3.B–3.D 与算法 1，看 AST 知识库、结构查询和三轮证明反馈如何连接；再读 §4.A–4.C 与表 2、表 3，核对“功能正确率”的定义和消融范围。随后读 §4.E–4.F 与表 4，区分 Func@1、Func@5、语法恢复和反例恢复；最后对照 FVEval 的 Design2SVA §3.4，理解为什么“断言可证明”被用作开放式性质生成的评分代理。
思想启发
以下是导读者由论文引出的理解角度，不是作者额外验证过的结论。
ProofLoop 最有力的证据并不是“Agent 已理解设计意图”，而是结构化工具能够改变生成分布。直接 prompt 容易因跨模块上下文、时钟和复位信息缺失而失败；让 Agent 主动查询权威结构信息，再用反例进行局部修正，明显增加了可编译、可证明的候选。这说明可靠反馈的粒度比简单的成功/失败标签更重要。
论文同时揭示了验证 Agent 的双重 oracle 问题。形式工具可以严格判断“性质是否对实现成立”，却不能独自判断“性质是否值得证明”；后一个判断需要来自规格、威胁模型、验证计划或故障模型的独立语义来源。若生成与验收都只围绕同一份 RTL，闭环可能越来越擅长描述实现，却没有越来越接近设计意图。
三个思考问题
1. 可证明、非空洞与有价值之间还差什么？
ProofLoop 已加入 vacuity analysis；为什么这仍不足以说明生成的断言是“最重要”的性质？
展开思考线索
可证明说明当前 RTL 没有违反性质；非空洞说明它不是仅因触发条件永远不出现而成立。有价值还要求性质能约束关键行为：例如排除某类错误实现、覆盖重要状态转移或对应规格中的风险。out == a + b 与某个内部辅助信号始终等于自身都可能非空洞地成立，但前者更可能发现功能错误。没有独立规格、mutation testing 或人工验证计划，就难以量化这层差异。
2. Solver 反馈会把断言修正确，还是修得更容易被证明？
一个候选被反例推翻后，Agent 可以修正时序，也可以弱化前件或后件；现有奖励如何区分这两条路径？
展开思考线索
反例精确指出当前性质与 RTL 的冲突，却不告诉 Agent 哪一方偏离了意图。若目标只是从 falsified 变为 proven，缩小触发范围、放宽后件或改写为实现已经保证的局部事实，都可能提高分数。Vacuity check 能拦住极端的永不触发，但未必拦住“很弱却经常触发”的性质。要区分语义修复与证明规避，还需要与外部规格等价、性质强度或变异杀伤能力等证据。
3. 五次至少成功一次，说明系统可靠到什么程度？
流水线设计的 Func@5 从 0.896 看起来很高，但 Func@1 只有 0.412；这两个数字分别支持怎样的结论？
展开思考线索
Func@5 说明给定五次采样预算，系统大多能找到至少一个可证明候选，适合衡量搜索空间中是否存在容易到达的成功解。Func@1 更接近一次运行的命中率。两者差距很大时，结果依赖候选并行生成和后续选择；若没有可靠机制在多个候选中识别更重要、更强的性质，“至少一个被证明”仍不能自动转化为稳定的验证产出。