AutoTrans：68组断言，53组自动通过

写安全断言，最费时间的部分往往不是敲下那几行 SystemVerilog，而是先弄清楚目标 RTL 到底有什么信号、状态和时序关系。换一颗 RISC-V 处理器，指令集可能相同，微架构却会改变端口名字、位宽、地址范围、状态机和 clocking convention。原来验证过的一组安全属性，很快就变成一批需要重新理解、重新绑定、重新调试的工程任务。

9 月 9 日提交到 arXiv 的论文提出了 AutoTrans，试图把这件事交给一条由大模型和 EDA 工具共同组成的流水线。它把 NS31A 参考处理器上的安全断言迁移到 lowRISC Ibex，再用 QuestaSim 和 JasperGold 做两道硬门槛。论文报告的结果是：68 个 assertion groups 中，自动流程通过 53 个，Auto TAR 为 78%；加入针对目标微架构的人工修复后，Final TAR 达到 100%。

这组数字有吸引力，但需要先把三个概念分开。100% translation coverage 只表示每组源属性都生成了输出；78% Auto TAR 才表示无人干预时有多少组通过了形式验证和 non-vacuous 检查；100% Final TAR 则包含了人工处理目标 RTL 结构约束的结果。论文证明的是“生成、编译、形式验证和人工接管可以被串成一条链”，还没有证明安全断言迁移已经成为完全无人值守的生产能力。

大模型最先撞上的墙，是目标 RTL

安全属性写的是意图，SVA 写的是目标设计中的可观测行为。比如“禁止特权级越权访问”可以作为跨处理器复用的安全目标，但具体要引用哪个状态位、哪条地址比较结果、哪个异常信号，以及断言应该在当前周期还是下一个周期观察，都由目标 RTL 决定。

这正是跨架构迁移比代码补全更难的地方。模型如果只看到源断言和一段自然语言描述，很容易生成一个看似合理的属性，却引用目标设计中根本不存在的信号。论文在 PMP 模块上做了 grounding 消融：没有目标信号清单时，模型生成了 15 个不存在的信号名，输出还包在 Markdown fence 里，QuestaSim 在第一行就编译失败；加入信号 grounding 后，8 个信号全部有效，编译通过，PMP 的 TAR 达到 100%。

这里的关键动作很朴素：AutoTrans 先读 RTL，再让模型写断言。Step 1A 使用 Python 正则表达式提取端口、内部信号、参数、枚举和 packed struct 类型，并把结果写入signals.json。对时序模块，它还按命名规则识别clk_i和rst_ni。多个 RTL 文件会合并去重，和模块相关的 package 类型会被筛选出来。

这套提取器没有试图成为完整的 SystemVerilog 编译器。它的目标更窄：给 prompt 提供一份可追踪的目标接口清单。对 AutoTrans 来说，模型的自由度首先被限制在“目标 RTL 确实出现过的名字”之内，后面的语义判断才有机会落到真实设计上。

Prompt 固定下来，复现才有抓手

AutoTrans 的第二个设计选择，是把 prompt 组装变成可审计的中间产物。流程把signals.json、NS31A 的 CSV 属性、按模块类型选择的 SVA 模板和固定的 LLM prompt 模板放在一起，一次性填充占位符，生成prompts/final/ _final_prompt.txt 。

组合逻辑模块和时序逻辑模块使用不同模板。PMP 不允许引入 clocking、#或$past()；时序模块则要求使用@(posedge clk_i) disable iff (!rst_ni)，并根据需要处理延迟和过去值。DO、ETI、CF、MT 虽然共享ibex_controller.sv，流程仍为它们添加不同的逻辑后缀，避免 bind target 混淆。

论文把这种设计称为 byte-identical prompt assembly。相同 RTL 和相同输入重新运行时，signals.json与最终 prompt 的git diff应为空。模型输出则用temperature=0.0和seed=42尽量压低采样波动，初次翻译使用 V4-Flash，失败重试才升级到 V4-Pro。

这解决的是过程可复现问题，不能把它扩大解释成模型永远稳定。云端模型仍可能更新权重，固定 seed 也不等于跨版本输出必然一致。AutoTrans 的处理方式，是让编译和 FPV 继续承担最后的筛选：输出有变化并不直接进入结果集，只有通过形式验证且非 vacuous 的断言才算被接受。

形式验证把“像是对的”变成可拒绝的结果

Stage 2 分成两步。Step 2A 用 QuestaSim 把生成的 bind file 和 Ibex RTL 一起编译，筛掉语法错误、端口作用域错误和不符合 SystemVerilog 语法的输出。Step 2B 用 JasperGold FPV 执行analyze、elaborate、clock/reset setup、prove -all和report -vacuity，检查断言是否被证明，以及它的 antecedent 是否真的可达。

这两道门对应两种不同的失败。QuestaSim 报错，通常意味着输出还没有成为可编译的工程文件；JasperGold 出现 counterexample，则说明属性逻辑与目标 RTL 行为不一致；出现 vacuous，则可能是前件永远不成立，断言虽然“证明成功”，却没有检查到有效场景。AutoTrans 把这些日志重新送回 V4-Pro，让重试指令区分“只修语法”“修正逻辑”与“重写 antecedent”。

论文因此引入 TAR：每个模块的 TAR 等于在 clean RTL 上同时满足 Proven 和 non-vacuous 的 assertion groups，除以该模块的 source groups。这个指标比 BLEU、文本相似度或单纯 coverage 更接近验证工程真正关心的结果，但它也只衡量这组实验中被选中的属性、目标模块和验证环境。

78% 自动通过，剩下的 16 组说明了什么

AutoTrans 覆盖 Ibex 的 9 个安全模块、68 个 groups。PMP 和 CSR 共 20 个 groups 由 V4-Flash 直接通过；DO、ETI、CF、MT、MA、IE 使用过 V4-Pro retry。合计 53/68 个 groups 在没有人工介入的情况下通过，Auto TAR 为 78%。

剩下 16 个 groups 并非简单的“模型不会写 SVA”。作者根据 QuestaSim 和 JasperGold 的错误输出来定位 Ibex 特有的结构问题，再进行人工修复。修复集中在三类：

•时序表达：PC_JUMP、$past、Debug FSM 等行为在目标设计中的观察周期不同；

•前件范围和可达性：MRET/DRETguard、tbranch、lsu_typefree-variable 等条件需要重新限定；

•绑定与信号对应：包括csr_save_wb_o、FENCE.I、端口作用域和精确 RTL mux equation。

这 16 组最能说明自动化边界。模型可以根据目标信号列表和源属性生成候选断言，验证工具可以给出 counterexample、vacuity 或 elaboration 反馈，但判断一个属性怎样对应 Ibex 的具体状态机和数据通路，仍然需要目标 RTL 知识。论文说人工修复改变的是 property 的表达方式，没有改变它要检查的 security intent；从工程角度看，这仍然是需要责任人签字的安全验证动作。

更值得关注的是，AutoTrans 把人工工作从“从头写一套断言”压缩成“根据工具反馈处理局部结构约束”。论文将这部分描述为从每个模块需要数天的 RTL 专家工作，转成由错误日志引导的 targeted fixes。这个时间判断属于作者对工程成本的估计，不能当作独立测量；但流程变化本身很清楚：人工不再面对一张空白编辑器，而是面对一组已经过编译和形式验证分诊的失败项。

对验证团队，真正的收益怎么验收

这篇论文对验证工程师、CAD/流程负责人和研发管理者的意义并不相同。

一线工程师关心的是失败项是否可定位。AutoTrans 保存signals.json、最终 prompt、bind file、QuestaSim 日志、FPV baseline 和 vacuity 报告，能够把一次生成拆成输入、模型输出、工具反馈和修复结果。只给一个“78%”没有用，能否回放一个失败断言、看到它引用了什么信号、知道它卡在编译还是语义验证，才决定它能不能进入日常流程。

流程负责人关心的是工具边界。Stage 1 可以在笔记本上完成 RTL 解析、prompt 组装和模型调用，Stage 2 仍需要商业 EDA license 和服务器。也就是说，成本并没有消失，而是从人工翻译时间转移到 EDA 运行、日志归档、模型版本管理和人工 review。若没有稳定的 EDA 执行环境，所谓“接入闭环”只能停留在生成文件层面。

研发管理者更应该追问三个验收问题：自动通过率按 assertion group、单条 assertion 还是模块计算；FPV 是否包含 non-vacuous 检查；人工修复后有没有独立 review、回归和责任记录。AutoTrans 的 TAR 定义回答了前两个问题，但论文仍没有给出跨版本、跨处理器、跨团队的独立复现结果。

真正可落地的 AI+EDA，不会停留在个人问答助手，而是要把模型能力、企业知识、设计流程和治理边界放进同一条研发链路。对高保密研发环境来说，本地化、私有化、隔离式部署、权限审计和过程留痕，也会比单点模型能力更早成为落地门槛。

下一步看什么

AutoTrans 的价值，落在把大模型放进一个可以拒绝错误结果的工程流程里。信号提取解决“模型看见什么”，固定模板解决“流程如何回放”，QuestaSim 和 JasperGold 解决“错误怎样被挡住”。三者缺一，模型输出都可能停留在演示层。

这条路线也给 AI+EDA 的落地提供了一个更实用的判断标准：先看输入是否被目标设计约束，再看输出是否经过真正的工程工具验证，最后看失败结果能否被人接管、重跑和审计。模型名称和 prompt 长度反而排在后面。

AutoTrans 目前给出的，是一个有清晰边界的研究样本：在指定的 NS31A 到 Ibex 迁移任务上，模型生成可以被编译和 FPV 反复筛选，53/68 个 groups 实现自动通过，剩余 16 个由人工处理后全部通过。它离“安全验证自动化”还有距离，却已经把问题从“模型能不能写断言”推进到“哪些断言能被工程流程接受、哪些必须交给人”。对于接下来评估同类 AI 验证工具的团队，这个问题比单独看一个漂亮的百分比更值得追踪。

作者：麒芯

声明：本文基于公开论文与代码仓库整理。AutoTrans 的数字为作者实验结果，不能等同于独立复现、sign-off 或量产证据。

参考资料：

1. arXiv：《AutoTrans: AI-Assisted Automatic Translation of Security Assertions for RISC-V Processors》

2. AutoTrans 官方 GitHub 仓库：《AI-assisted automatic translation of RISC-V security assertions》

3. lowRISC 官方 GitHub 仓库：《Ibex RISC-V Core》