EquivSVA：跨等效 RTL 实现的行为断言的正式验证数据集

大型语言模型越来越多地用于根据自然语言规范和寄存器传输级设计生成 SystemVerilog 断言。现有的数据集和基准支持重要的目标，例如大规模训练、正式评估、规范到断言生成和基于突变的测试。一个补充需求是研究生成的断言是否捕获外部可观察的行为或依赖于一个 RTL 实现的附带细节。我们提出了 EquivSVA，这是一个围绕行为家族组织的经过正式验证的数据集。每个家族都包含四个结构不同的 RTL 实现，它们具有相同的外部可观察行为、共享的接口级黄金属性、三个受控突变体和形式验证证据。 EquivSVA 包含 12 个类别的 120 个行为家族、480 个参考 RTL 实现、914 个黄金属性和 360 个突变体。每个最终家族都会通过固定的 17 个作业验证套件，涵盖 RTL 等效性、黄金属性证明、属性可达性、突变体可区分性以及突变体的黄金属性检查。我们还提供固定的家庭安全训练、开发和测试拆分。作为数据集支持的分析的小型演示，我们在保留的测试拆分上评估了公开发布的 Apache-2.0 许可的 Qwen2.5-Coder-7B-Instruct 模型。在 293 个仅接口生成的属性中，有 93 个在形式上是健全的，并且健全属性的数量因 24 个测试系列中的 14 个的等效实现而异。这些结果说明了行为族组织如何支持断言生成稳健性的受控研究，而无需更改预期功能。数据集、生成器、验证脚本和案例研究工件在此 https URL 公开发布。