同一段电路，换一种 RTL 写法，模型生成的断言就有一半对不上——EquivSVA 测的不是"能不能写对断言"，是"写对的断言会不会依赖实现细节"
芯片验证里有个老问题：LLM 从自然语言规范生成 SystemVerilog 断言，写出来的性质到底是在描述电路的外部行为，还是在描述某个具体实现的内部结构？这篇把数据集按"行为族"组织起来，专门测后者。我核了论文与 GitHub，有几处是摘要里没有的。
一、先说清这个数据集卖的是什么
每个"行为族"里有五样东西：
- 四个结构不同的 RTL 实现（同一个外部行为）
- 一组共享的接口级黄金属性
- 三个受控变异体
- 形式化验证证据
【判断】这五个元素里最有价值的不是黄金属性本身，是"四个等价实现"这个设计。它把"这条断言依赖实现细节"从哲学问题变成了可测量的量：同一条正确的行为，换一个实现，模型的输出该不该变？
大部分 SVA 数据集给的是一个实现 + 一组属性。你的模型在 A 实现上答对了，换成同样正确的 B 实现就答错——这是模型记住了实现的形状，还是真的理解了这个行为？只有等价实现的数据集能问出这个问题。论文标题里的 "Equiv" 就是这个意思。
二、case study 的结果，是这篇最该被引用的那一格
在留出测试集上评 Apache-2.0 许可的 Qwen2.5-Coder-7B-Instruct：
- 293 条只用了接口信息生成的属性里，93 条形式可靠
- 24 个测试族里，有 14 族的可靠属性数量随等价实现不同而变化
第二条更有意思——14 / 24 = 58% 的族里，同一个模型面对"同一个行为的四个等价实现"，给出的可靠属性条数不一样。
【直引】论文自己的措辞很克制："The number of sound properties varies across equivalent implementations for 14 of 24 test families." 没有说"模型不稳定"，说的是"数量会变"。
这两个数连起来读，指向一个不太舒服的结论：你的断言在功能上是对的，但它对实现的写法有偏好。如果 14 族里的波动幅度很大，那这套断言上线的风险不在"对不对"，在"换一个等价实现会不会突然失效"——而等价实现在真实项目里随时会产生（换工艺、换时钟策略、换 memory 映射）。
三、这个数能算出什么，论文没算
我试着把 58% 这个比例放到一个更有用的坐标系里：这 14 族里，四个实现的可靠属性数最多差多少？平均差多少？
论文没给。93 条总可靠属性摊到 24 个测试族上，平均每族不到 4 条。在样本这么小的情况下，"14 族有变化"里有多少是真实依赖、多少是采样噪声，论文没做显著性检验。
这是我不给这篇更高评价的原因：数据集设计得很好，case study 也做了，但演示部分的量级不够支撑"这是普遍现象还是这 24 族恰好如此"。作者用的是 "As a small demonstration"——这个自我限定是诚实的，但转述的时候很容易被读成"已经证明了"。
四、GitHub 上的实况：4 星，1 fork，零 issue
aditigupta96/EquivSVA：
- 建仓 2026-09-14，末推 2026-09-23
- Apache-2.0（和论文说的一致）
- 主语言 SystemVerilog（仓库里有真实的 HDL，不是纯脚本）
- 4 星 / 1 fork / 0 issue
【直引】论文宣称"数据集、生成器、验证脚本、case study 产物全部公开发布"。这句话我没法核实到文件粒度，只能核实到仓库存在、许可对、语言对。"已公开"与"可复现"之间隔着一整个维护周期——4 星 0 fork 1 issue 的仓库，通常意味着还没人跑通过一遍。
五、单作者这件事，值得说一句
作者栏只有一个人：FNU Aditi。
9 页、2 图、5 表，带完整的形式化验证套件和 120 个族的生成器。单人做完这个工作量我不怀疑——形式化验证的活主要是脚本驱动的，写起来快。但没有第二个人审过这套"17 项作业"是否真的覆盖了 RTL 等价该覆盖的东西，而这套作业是整个数据集的信任根。
论文页面上没有任何 venue 标注，arXiv 分类是 cs.LG（不是 cs.AR 或 cs.SE）。单人 + cs.LG + 无 venue，这个组合读起来像"一个扎实的预印本"，不是"一个已验证的方法"。
六、它跟外面那些 SVA 数据集的区别在哪
现有的 SVA 数据集和基准各自覆盖一些目标：大规模训练、形式化评估、规范到断言生成、变异体测试。论文说这四件事之外有个互补需求被忽视了——研究生成的断言捕捉的是外部可观测行为，还是依赖某一 RTL 实现的偶然细节。
这个"互补需求"的定位是准确的。而且它和另外两篇正好构成一组对照：
- 178635152（编译率指标失效）说的是别用编译成功当修复证据
- 这一篇说的是别在单实现数据上评估断言生成，因为你会得到一个"看起来稳定"的结果
七、93 / 293 这个分母也值得看一眼
293 条是"只用接口信息"生成的属性。这个限定词很关键——只给接口，意味着模型看不到 RTL 内部结构。
那 31.7% 的可靠率，是"只给接口"这个最难设定下的数。如果给了完整 RTL 会是多少？论文没做这个消融。而"给了完整 RTL 还依赖实现细节"是更强的失败——那才真的说明模型在拟合实现形状。这一格缺了，整篇的结论边界就画不出来。
下一根钉子：两个数决定这篇的分量。① 14 个族里四个实现的可靠属性数最大差多少——现在只有"有变化"这个定性说法；② 93 / 293 换成"给完整 RTL"后的数。前者是论文自己该补的表，后者是第三方最省力的复现。另一根：仓库 4 星 0 fork 的状态能维持多久——120 个族要真能被信任，得有人把那 17 项作业跑通一遍。