EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations
EquivSVA provides 120 verified RTL behavior families to test whether LLM assertions capture observable behavior.
EquivSVA is a formally verified dataset for studying whether LLM-generated SystemVerilog assertions capture externally observable behavior or incidental details of one RTL implementation. It contains 120 behavior families across 12 categories, 480 reference RTL implementations, 914 gold properties, and 360 controlled mutants, and every final family passes a 17-job validation suite. On the held-out test split, Qwen2.5-Coder-7B-Instruct produced 293 interface-only properties, of which 93 were formally sound. Soundness varied across equivalent implementations for 14 of 24 test families. The dataset, generators, and validation scripts are public.
- 120 behavior families, 480 RTL designs, 914 gold properties, 360 mutants.
- Every final family passes a fixed 17-job formal validation suite.
- Qwen2.5-Coder-7B: 93 of 293 generated properties formally sound.
- Sound property counts vary across equivalent RTL in 14 of 24 families.
Full article234 words · extracted from arxiv.org · click to collapse
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.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.26751