知识卡片：EquivSVA：跨等价 RTL 实现的行为断言形式化验证数据集

一句话结论

EquivSVA 是一个围绕“行为族”组织的、经形式化验证的 SystemVerilog Assertions 数据集，用于受控研究 LLM 生成的断言是否捕捉同一外部可观察行为，而非依赖某一 RTL 实现的偶然细节；材料同时给出规模统计和 Qwen2.5-Coder-7B-Instruct 的小型演示结果。

事件概述或研究问题

大型语言模型正越来越多地被用于从自然语言规格和寄存器传输级设计生成 SystemVerilog Assertions。现有数据集和基准支持大规模训练、形式评估、规格到断言生成、基于变异的测试等重要目标。该论文关注一个补充性问题：生成的断言究竟捕捉了外部可观察行为，还是依赖某一个 RTL 实现的偶然细节。

方法/产品要点

• 数据集围绕“行为族”组织；每个行为族包含四个结构不同、但外部可观察行为相同的 RTL 实现。
• 每个行为族还包含共享的接口级 gold properties、三个受控 mutants，以及形式验证证据。
• 规模：120 个行为族，覆盖 12 个类别；480 个参考 RTL 实现；914 条 gold properties；360 个 mutants。
• 验证流程：每个最终行为族通过固定的 17-job 验证套件，覆盖 RTL 等价、gold-property 证明、属性可达性、mutant 可区分性，以及 gold properties 在 mutants 上的检查。
• 数据划分：提供固定的 family-safe 训练、开发、测试划分。
• 公开材料：数据集、生成器、验证脚本和案例研究工件发布在 https://github.com/aditigupta96/EquivSVA。
• 演示模型：在留出测试集上评估公开的、Apache-2.0 许可的 Qwen2.5-Coder-7B-Instruct 模型。

主要结果或产业意义

• 在留出测试集上，模型生成 293 条 interface-only 属性，其中 93 条被判定为形式可靠。
• 在 24 个测试行为族中，有 14 个族在不同等价实现之间的可靠属性数量发生变化。
• 材料认为，这些结果说明按行为族组织数据可以在不改变预期功能的情况下，支持对断言生成鲁棒性的受控研究。
• 产业意义：材料未直接给出产业部署结论；可能的相关方向是评估 LLM 生成断言是否跨等价 RTL 实现稳定，但具体产业影响待核实。

为什么重要

如果 LLM 生成的断言只能匹配某一个 RTL 实现，它可能把实现细节误当成规格，从而在等价实现或后续设计中失效。EquivSVA 通过“同一外部行为、多个结构不同实现、共享 gold properties、受控 mutants、固定验证套件、family-safe 划分”的设计，为研究断言生成的可迁移性和鲁棒性提供了受控设置。与已有相关卡片无直接主题重叠；本条增量在于提供硬件形式验证与 LLM 断言生成交汇处的数据集与评估视角。

局限与不确定性

• 材料仅提供摘要与元数据，论文正文、附录、具体验证工具、17-job 验证套件的逐项细节、统计方法、12 个类别的具体列表均待核实。
• 数据集本身的许可证、GitHub 仓库的实际可获取性与可复现性待核实。
• 演示仅使用一个 7B 模型 Qwen2.5-Coder-7B-Instruct，属于材料所称的“small demonstration”，不能推广到所有 LLM 或所有断言生成设置。
• 93/293 条形式可靠的判定标准、生成条件、提示方式、采样次数等细节待核实。
• 14/24 个测试族出现可靠属性数量变化，但变化方向、幅度、统计显著性和原因待核实。
• Qwen2.5-Coder-7B-Instruct 的 Apache-2.0 许可是模型许可信息；这不等于数据集或项目代码的许可证，后者待核实。

可用于图书/PPT/简报的角度

• 用“行为族”解释如何避免断言绑定到单一 RTL 实现。
• 用“同一外部行为、多个等价实现”说明断言生成的可迁移性评估。
• 用“17-job 验证套件”介绍形式验证作为数据质量门的设计思路。
• 用“family-safe train/dev/test splits”讨论数据泄漏与基准划分。
• 用 Qwen2.5-Coder-7B-Instruct 的初步结果说明 LLM 断言生成鲁棒性可作为独立研究问题。

原始材料

• 英文标题：EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations
• 英文关键词（摘要未单列关键词，依据摘要内容整理；待核实）：SystemVerilog Assertions; RTL; formal verification; dataset; behavior families; large language models; mutation-based testing; specification-to-assertion generation
• 作者：FNU Aditi
• arXiv ID：2609.26751v1
• 发布/更新：2026-09-22T17:33:09Z
• 主分类：cs.LG；分类：cs.LG
• 摘要 URL：https://arxiv.org/abs/2609.26751v1
• PDF URL：https://arxiv.org/pdf/2609.26751v1
• 项目/代码：https://github.com/aditigupta96/EquivSVA