EquivSVA：面向等价 RTL 实现的形式化验证断言数据集
EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations
研究 RTL 断言生成的可以看看，120 个行为族都做了形式化验证，还能测模型对等价实现的鲁棒性。
EquivSVA 是一个围绕行为族组织的 SystemVerilog 断言数据集，每个族包含 4 个结构不同但外部行为等价的 RTL 实现、接口级 gold 属性和 3 个受控 mutant。整个数据集包含 120 个行为族、480 个 RTL 实现、914 条 gold 属性和 360 个 mutant，每个族都通过 17 项任务的验证套件，覆盖 RTL 等价性、属性证明和可达性检查。作者用 Apache-2.0 许可的 Qwen2.5-Coder-7B-Instruct 在测试集上做了演示：293 条仅接口生成的属性中有 93 条形式化正确，且 24 个测试族中有 14 个族在等价实现之间的正确属性数量存在差异。数据集、生成器、验证脚本已在 GitHub 公开。
EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations
Large language models are increasingly used to generate SystemVerilog Assertions from natural-language specifica- tions and register-transfer-level designs. Existing datasets and benchmarks support important goals such as large- scale training, formal evaluation, specification-to-assertion generation, and mutation-based testing. A complemen- tary need is to study whether a generated assertion cap- tures externally observable behavior or depends on inci- dental details of one RTL implementation. We present EquivSVA, a formally verified dataset organized around behavior families. Each family contains four structurally distinct RTL implementations of the same externally ob- servable behavior, shared interface-level gold properties, three controlled mutants, and formal-validation evidence. EquivSVA contains 120 behavior families across 12 cat- egories, 480 reference RTL implementations, 914 gold properties, and 360 mutants. Every final family passes a fixed 17-job validation suite covering RTL equivalence, gold-property proofs, property reachability, mutant dis- tinguishability, and gold-property checks on mutants. We also provide fixed family-safe train, development, and test splits. As a small demonstration of the analyses en- abled by the dataset, we evaluate the publicly released, Apache-2.0-licensed Qwen2.5-Coder-7B-Instruct model on the held-out test split. Of 293 interface-only generated properties, 93 are formally sound, and the number of sound properties varies across equivalent implementations for 14 of 24 test families. These results illustrate how behavior-family organization can support controlled stud- ies of assertion-generation robustness without requiring changes in intended functionality. The dataset, generators, validation scripts, and case-study artifacts are publicly released at https://github.com/aditigupta96/EquivSVA.
