EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations
作者: FNU Aditi
分类: cs.LG
发布日期: 2026-09-22
备注: EquivSVA is a 9-page paper by FNU Aditi introducing a formally verified dataset of 120 behavior families, 480 RTL implementations, 914 gold properties, and 360 mutants across 12 categories, featuring 2 figures, 5 tables, and a case study evaluating Qwen2.5-Coder-7B-Instruct
🔗 代码/项目: GITHUB
💡 一句话要点
提出EquivSVA以验证行为断言在等效RTL实现中的一致性
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 行为断言 RTL实现 数据集 形式验证 自动化测试 硬件设计
📋 核心要点
- 现有方法缺乏对生成断言是否捕捉外部可观察行为的系统性研究，容易受到特定RTL实现细节的影响。
- 论文提出EquivSVA数据集，通过行为家族组织，提供多种结构不同但行为一致的RTL实现，支持断言生成的验证。
- 实验结果显示，在293个生成的仅接口属性中，有93个是形式上有效的，验证了行为家族组织的有效性。
📝 摘要（中文）
随着大型语言模型在从自然语言规范和寄存器传输级设计生成SystemVerilog断言中的应用日益增加，现有的数据集和基准测试支持了大规模训练、正式评估、规范到断言生成和基于突变的测试等重要目标。本文提出的EquivSVA是一个正式验证的数据集，围绕行为家族组织，每个家族包含四个结构上不同但具有相同外部可观察行为的RTL实现、共享的接口级金属性质、三个受控突变体和正式验证证据。EquivSVA包含120个行为家族，480个参考RTL实现，914个金属性质和360个突变体。每个最终家族都通过了固定的17项验证套件，涵盖RTL等价性、金属性质证明、性质可达性、突变体可区分性和突变体上的金属性质检查。
🔬 方法详解
问题定义：本文旨在解决生成的SystemVerilog断言是否能够准确捕捉外部可观察行为的问题。现有方法往往依赖于特定RTL实现的细节，缺乏对等效实现的全面评估。
核心思路：论文的核心思路是构建EquivSVA数据集，围绕行为家族组织，确保每个家族包含多个结构不同但行为一致的RTL实现，以便进行系统性验证。
技术框架：EquivSVA数据集的整体架构包括行为家族的定义、RTL实现的生成、金属性质的提取、突变体的创建和验证套件的设计。每个家族都经过严格的验证流程，确保其一致性和有效性。
关键创新：最重要的技术创新在于通过行为家族的组织方式，提供了一个系统化的框架来研究断言生成的鲁棒性，避免了对功能意图的改变。与现有方法相比，EquivSVA提供了更为全面的验证机制。
关键设计：在设计中，采用了固定的17项验证套件，涵盖了RTL等价性、金属性质证明、性质可达性等关键指标，确保每个家族的最终验证结果的可靠性。
🖼️ 关键图片
📊 实验亮点
实验结果显示，在293个生成的仅接口属性中，有93个被正式验证为有效，且在24个测试家族中，有14个家族的有效属性数量在不同的等效实现中存在差异。这表明行为家族组织能够有效支持断言生成的鲁棒性研究。
🎯 应用场景
该研究的潜在应用领域包括硬件设计验证、自动化测试生成和断言生成工具的开发。EquivSVA数据集为研究人员和工程师提供了一个可靠的基准，能够提升RTL设计的验证效率和准确性，推动硬件设计领域的进步。
📄 摘要（原文）
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.