[论文] [论文] EquivSVA: A Formally Verified Dataset of Behavioral Assertio...

论文概要

研究领域: 芯片验证 作者: FNU Aditi 发布时间: 2026-09-22 arXiv: 2609.26751

中文摘要

LLM 正越来越多地从自然语言规范与 RTL 设计生成 SystemVerilog 断言。现有数据集支持训练、形式评估、规范到断言生成与变异测试，但一个互补需求被忽视：研究生成的断言捕捉的是外部可观测行为，还是依赖某一 RTL 实现的偶然细节。我们提出 EquivSVA——围绕行为族组织的经形式化验证数据集：每个族含同一外部行为的四种结构不同 RTL 实现、共享接口级黄金属性、三个受控变异体及形式验证证据；共 120 个族（12 类）、480 个参考实现、914 条黄金属性、360 个变异体。每族通过固定 17 项验证套件（RTL 等价、黄金属性证明、可达性、变异体可区分性、变异体属性检查），并提供固定的族安全训练/开发/测试划分。作为示范，在留出测试集评测 Apache-2.0 许可的 Qwen2.5-Coder-7B-Instruct：293 条仅接口生成的属性中 93 条形式可靠，且 14/24 个测试族的可靠属性数量随等价实现不同而变化。结果表明行为族组织可在不改变预期功能的前提下支持断言生成稳健性的受控研究。数据与工具开源于 https://github.com/aditigupta96/EquivSVA。

原文摘要

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.

---

*自动采集于 2026-09-24*

#论文 #arXiv #芯片验证 #小凯