网易首页 > 网易号 > 正文 申请入驻

GateTruth 审计 Testbench:模型通过了,真能算正确吗?

0
分享至

一段 RTL 只要通过 benchmark 的 testbench,就算“功能正确”。大量 RTL 生成评测都建立在这条规则上,pass@1、pass@k 也由此产生。

麻烦就在这里:testbench 也可能漏判。

如果 testbench 没有激励到关键路径,没有检查某个输出,或者 oracle 本身写错,一段带 bug 的 RTL 仍然可以拿到通过。此时 leaderboard 排出的模型能力和 testbench 盲区一起进入了排名。2026 年 8 月 12 日提交到 arXiv 的 GateTruth,把这个长期被当作默认前提的问题摆到了台面上:先故意改坏 reference RTL,再看 testbench 能抓住多少。

作者报告,在其自建的 60 个静态 RTL 生成任务中,46 个 testbench 能杀死至少 95% 的注入变异体。把同一套引擎用于 RTLLM v2.0 后,46 个可审计设计里有 33 个低于这一门槛,3 个设计的 kill rate 为 0%。

这些数字足够醒目。更值得关注的是,RTL benchmark 的证据链终于多了一道可测的关卡。GateTruth 同时也暴露了这道关卡本身会怎样失真:门槛可被调参,等价变异体会污染分母,编译失败和超时的计数规则会改变结果,高 kill rate 也不等于 oracle 正确。


一个通过结果,到底证明了什么

传统 RTL 生成 benchmark 的逻辑很直观。给模型一段自然语言 specification,模型输出 Verilog 或 SystemVerilog,编译并运行 testbench;通过就记为成功。RTLLM 原论文进一步加入综合后的 timing、power、area 等设计质量指标,但功能正确性仍由 testbench 先做判定。

这套流程暗含了一个强假设:testbench 足够敏感,能够拒绝模型可能写出的关键错误。

代码覆盖率可以告诉工程师哪些语句、分支或条件被走到,functional coverage 可以检查预先定义的功能场景是否被命中,assertion 和 formal 能覆盖另一部分性质。但这些指标都不直接回答一个朴素问题:如果设计真的在某处坏了,当前 testbench 会不会报警?

mutation testing 的思路正是主动制造故障。GateTruth 在 reference RTL 上注入比较边界翻转、逻辑或位运算反转、移位方向反转、reset/enable 极性翻转、赋值删除、寄存器保持和输出反转等变异,再逐个运行 testbench。被 testbench 发现的变异体算 killed,漏掉的算 survived。

于是,“testbench 跑过了”之外又多了一条证据:它至少对一组明确注入的错误有反应。

不过,这里需要拆开三道门。

第一道门是 baseline/oracle 有效。未修改的 reference RTL 必须先通过 testbench,否则连“正确答案”都站不住。第二道门是故障敏感性,即 testbench 能杀死多少注入变异体。第三道门是代表性与公平性:变异算子是否覆盖真实错误,分母怎样计算,testbench 是否针对指标调过,合法的不同实现会不会被误杀。

GateTruth 的 95% floor 只对应第二道门的一部分。它是作者采用的工程门槛,不是行业标准,更不是 sign-off 证明。

46、33 和 775,三组数字要分开看

GateTruth 自建套件包含 60 个 specification-to-RTL(从规格生成 RTL)任务和 8 个智能体修复任务。论文最终报告,60 个 Track A testbench 中有 46 个达到至少 95% 的 mutation kill floor,14 个没有达到;Track B 的 8 个 testbench 尚未按同一协议完成认证。

对 RTLLM v2.0 的外部审计则从 50 个公开设计开始。作者先运行未修改的 golden/reference RTL,46 个通过 baseline 后进入变异测试,4 个标为 unsupported。这里的 unsupported 不能算 0%。工具没有完成审计,与 testbench 一个故障都抓不到,代表两种完全不同的状态。

在 46 个可审计设计中,33 个低于 95% floor,占 72%;13 个恰好为 100%。设计级 kill rate 的中位数是 74.0%。

如果把所有变异体放在一起,口径又变了。46 个设计一共生成 775 个变异体,其中 440 killed、320 survived、15 indeterminate,pooled kill rate 为 56.8%。每个设计的变异体数量从 1 到 115 不等,中位数只有 10.5,因此“设计级中位数”和“按变异体加权的总体比例”回答的是不同问题。

三个 0% 设计也得逐个拆开。adder_8bit只有 1 个变异体,square_wave有 6 个,作者检查到其中包括输出反转仍未被发现;这至少说明相关输出没有被有效检查。edge_detect的 10 个变异体全部属于 assignment_hold,它的 0% 只能证明 testbench 没抓住这类寄存器保持故障,不能外推为“什么错误都抓不住”。

因此,读 benchmark 审计不能只盯一个百分比。至少要同时看设计数、逐设计分布、变异体数量、算子分布和原始 survivor。

最有价值的部分,是作者把自己的失误也写了出来

GateTruth 最值得同行讨论的部分,是作者公开了两次自我纠正。

作者最初曾得到 60/60 全部过线的结论,后来修正为 49/60,再把 kill 的定义收紧为只统计行为仿真失败,最终变为 46/60。问题包括不可靠的“等价变异体”排除机制,以及把编译失败或 formal 抓到的故障混入原本声称衡量 simulation testbench 的指标。

更尖锐的是 Goodhart 效应。10 个 testbench 曾经为了跨过 95% 门槛而修改;按当前引擎回看,它们修改前的中位 kill rate 为 77.5%,修改后真正仍能过线的只有 3 个。其余修改部分依赖了有问题的等价变异体排除,test vector 并没有因此真正增强。

一旦指标变成准入门槛,团队就会围着它优化。mutation score 也不例外。工程上真正需要的是让 testbench 对真实 bug 更敏感,报表上的漂亮分母解决不了这个问题。

外部审计里也有一处口径不一致。RTLLM 的 440 个 killed 变异体中,13 个来自编译失败;论文同时承认,编译失败本身不能证明 testbench 发现了功能错误。若把这 13 个从分子和分母同时排除,pooled kill rate 会从 56.8% 降到 56.0%。差异不大,却说明审计工具也必须接受审计。

高 kill rate 仍然可能错

mutation score 测的是 sensitivity,也就是故障敏感性:在固定算子集制造的这些故障里,testbench 能发现多少。它没有证明 golden reference 正确,也没有证明 specification 完整,更没有证明 testbench 会接受所有合法实现。

RTLLM 的radix2_div提供了一个直接例子。按照 GateTruth 作者在 Icarus Verilog 下的单模拟器复现,这个任务的公开 golden reference 没通过自带 testbench,因此在 mutation testing 开始前就被标成 unsupported。这里暴露的是 oracle/baseline 问题,而不是 kill rate 问题。

算子分布也会塑造结果。RTLLM 的 775 个变异体中,assignment_hold 占 47%;不同算子的变异体存活率差异明显。一个 benchmark 对这组算子表现很好,仍可能对未注入的协议时序错误、跨时钟域问题、长序列状态错误或系统级交互缺乏辨识力。

等价变异体则从另一个方向影响分数。某些语法变化不会改变可观察行为,它们理论上无法被任何 testbench 杀死。如果不识别,kill rate 会被压低;如果排除规则不可靠,又会把真正可发现的故障删掉,虚高结果。

所以,mutation testing 更适合当作准入验证工具,不宜再被做成一张唯一榜单。它能暴露薄弱 testbench,却不能替代 functional coverage、code coverage、assertion、formal verification、真实 bug 回放和多模拟器回归。

RTL benchmark 应该补上一张“testbench 体检表”

对研究团队来说,GateTruth 给出的直接启示是:发布 pass@k 时,同时发布 testbench 的质量证据。最低限度应回答六个问题。

第一,未修改的 golden/reference 是否在声明的模拟器、版本和编译参数下通过?

第二,变异算子覆盖哪些故障类,每个任务生成多少变异体?

第三,编译失败、timeout、unsupported 和等价变异体如何进入分子分母?

第四,报告的是逐设计中位数、pooled rate,还是两者都报告?

第五,testbench 是否曾针对 mutation score 修改,是否保留修改前结果?

第六,有没有第二模拟器、独立复现、历史真实 bug 或形式性质作为交叉证据?

对模型厂商和企业采购者,这套问题同样适用。一个“RTL pass rate 提升”的数字,如果没有 testbench 质量、任务难度、采样条件和失败分类,很难转成工程判断。模型生成得更快,并不自动意味着验证成本下降;弱 testbench 甚至会把错误更快送进后续流程。

这也是中科麒芯在 AI+EDA 落地中持续强调的一点:模型输出、testbench、回归记录和人工 review 需要进入同一条可追溯流程。单次演示可以说明模型会写代码,工程证据才能说明它适合被接入研发链路。

GateTruth 没有给 RTL 生成 benchmark 盖下最终印章。它做了一件更基础、也更必要的事:把“谁来测试 testbench”从一句质疑变成了一套可运行的审计方法。

论文报告的 46/60、33/46 和 56.8%,都应留在作者预印本、固定仓库版本、固定模拟器和固定算子集的条件里。它们不代表第三方认证,不代表大型 SoC 验证效果,也不代表流片、量产或 sign-off。

真正可迁移的结论,是今后看到任何 RTL 生成榜单,都应顺着证据链继续追问:golden 先过了吗,testbench 真能杀死故障吗,变异算子覆盖了什么,分母怎样算,指标有没有被调过,最后还有哪些工程证据没有出现?

当 benchmark 自己也要先过测试,排行榜上的“正确率”才开始接近它声称衡量的东西。

作者:麒芯

声明:本文基于公开论文与开源仓库整理分析。文中实验数字均为作者 benchmark 结果,不代表第三方验证、客户部署、流片、量产或 sign-off,也不构成投资建议。

参考资料:

1. arXiv:《GateTruth: Auditing the Rigor of RTL Design Benchmarks via Mutation Testing》

2. GateTruth:公开代码仓库与 External Mutation Audit Summary

3. RTLLM / OpenLLM-RTL:论文与公开代码仓库

4. YosysHQ:《Mutation Cover with Yosys》

特别声明:以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布,本平台仅提供信息存储服务。

Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.

相关推荐
热点推荐
黄晓明澄清离婚脏水,37岁杨颖近况曝光,原来她早给自己留好退路

黄晓明澄清离婚脏水,37岁杨颖近况曝光,原来她早给自己留好退路

北海史记
2026-10-12 18:22:09
日媒:久保建英连续5场比赛无缘首发,处境十分艰难

日媒:久保建英连续5场比赛无缘首发,处境十分艰难

懂球帝
2026-10-12 16:33:12
不扒不知道,一扒吓一跳!被判死刑的明珍珍,私下生活能有多壕

不扒不知道,一扒吓一跳!被判死刑的明珍珍,私下生活能有多壕

哄动一时啊
2026-10-10 11:38:30
郑智与李玮锋从密友到路人:皆源于他俩均对于足球本身的心无旁骛

郑智与李玮锋从密友到路人:皆源于他俩均对于足球本身的心无旁骛

K唐伯虎
2026-10-10 08:00:17
北京,清华教授在一场公开论坛上罕见拍桌子:坚决反对养老政策无限拖延

北京,清华教授在一场公开论坛上罕见拍桌子:坚决反对养老政策无限拖延

回京历史梦
2026-10-12 09:10:52
退休 25 年晚节不保,79 岁陈元虎涉嫌违纪被查

退休 25 年晚节不保,79 岁陈元虎涉嫌违纪被查

小影的娱乐
2026-10-09 11:25:58
A股重要消息来了,不用等今天行情了,周二走势提前分析

A股重要消息来了,不用等今天行情了,周二走势提前分析

明心
2026-10-13 00:30:04
研究发现:复方丹参滴丸不只保护心脏,身体这4个变化很多人忽视

研究发现:复方丹参滴丸不只保护心脏,身体这4个变化很多人忽视

健康之光
2026-10-07 05:25:07
不查不知道,坐拥北京山庄,有4个孙子孙女的陈佩斯,私下有多壕

不查不知道,坐拥北京山庄,有4个孙子孙女的陈佩斯,私下有多壕

仙味少女心
2026-10-13 01:54:48
尊界踩断刹车 余承东为什么不发声了

尊界踩断刹车 余承东为什么不发声了

好猫财经
2026-10-12 10:33:54
苏州一对情侣,谈了7年,女子提了18次分手,分手后在街头痛哭!

苏州一对情侣,谈了7年,女子提了18次分手,分手后在街头痛哭!

川渝视觉
2026-04-17 22:13:14
毛主席虽活了83岁,保健医生却说:其实毛主席不具备长寿条件

毛主席虽活了83岁,保健医生却说:其实毛主席不具备长寿条件

华庭讲美食
2026-08-17 15:23:42
郑钦文的收入结构:2260万美元里,只有60万是打比赛挣的

郑钦文的收入结构:2260万美元里,只有60万是打比赛挣的

陈意小可爱
2026-10-13 02:31:36
追随拿破仑至孤岛的贴身侍卫,临终前揭秘:拿破仑的遗言另有其他

追随拿破仑至孤岛的贴身侍卫,临终前揭秘:拿破仑的遗言另有其他

白云故事
2025-11-14 14:05:08
美媒爆美军狼狈内幕:基地遭伊朗猛轰,连夜逃进沙漠还遭雷劈

美媒爆美军狼狈内幕:基地遭伊朗猛轰,连夜逃进沙漠还遭雷劈

张斌说
2026-10-12 10:43:14
气象站:一文了解什么是森林防火气象站

气象站:一文了解什么是森林防火气象站

测控技术有限公司
2026-10-08 09:44:05
特斯拉终于听劝了,2027款Model Y来了,真能让家庭用户满意?

特斯拉终于听劝了,2027款Model Y来了,真能让家庭用户满意?

阿芒娱乐说
2026-10-12 11:28:49
中天科技营收超309亿、净利23.87亿,股价为何仍在30元附近偏弱?

中天科技营收超309亿、净利23.87亿,股价为何仍在30元附近偏弱?

爱看剧的阿峰
2026-10-12 18:48:47
1949年李讷在课堂上指出老师错误,老师恼羞成怒:把你爸爸叫来

1949年李讷在课堂上指出老师错误,老师恼羞成怒:把你爸爸叫来

萧竹轻语
2025-08-04 11:45:40
10月份,苹果香蕉先靠边,这5种“黄金果”正当时,香甜多汁,润燥又养人,别不舍得吃!

10月份,苹果香蕉先靠边,这5种“黄金果”正当时,香甜多汁,润燥又养人,别不舍得吃!

秀厨娘
2026-10-12 15:27:30
2026-10-13 05:31:00
麒芯说AI
麒芯说AI
分享AI与芯片设计领域的行业新闻、时事热点、、技术干货与行业同仁共探智能算力时代的芯片研发赋能。
120文章数 0关注度
往期回顾 全部

科技要闻

尊界:10月底确认制动踏板支架升级方案

头条要闻

男子借5000万 已归还3325万后仍被要求还4980万

头条要闻

男子借5000万 已归还3325万后仍被要求还4980万

体育要闻

一周吃6顿披萨的胖子,也能单防姆巴佩?

娱乐要闻

张艺谋身体状况曝光 陈婷不再顾及体面

财经要闻

尊界,是江淮的救命车还是失血引擎?

汽车要闻

小鹏G9L巴黎车展全球上市 法国市场售价74990欧元起

态度原创

房产
亲子
教育
家居
公开课

房产要闻

等了半年!今年海口最值得期待的新盘,即将亮相!

亲子要闻

婚姻真相:为什么产后一年,是夫妻最难熬的一年

教育要闻

学校家委会让家长轮流到校看午休,爆上热搜,教育局回应:不存在家长代替教师管理午托,你信吗?

家居要闻

2026建博会(广州) 公装联探展交流活动

公开课

李玫瑾:为什么性格比能力更重要?

无障碍浏览 进入关怀版