# EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations

arXiv: https://arxiv.org/abs/2609.26751 · HTML: https://mlsanity.com/paper/2609.26751/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 15 references that are in the map.
- First posted on arXiv 22 Sep 2026.

## Builds on (most cited first, 6 of 6)

- [AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation](https://mlsanity.com/paper/2406.18627/) (2024)
- [Enhancing Large Language Models for Hardware Verification: A Novel SystemVerilog Assertion Dataset](https://mlsanity.com/paper/2503.08923/) (2025)
- [Spec2Assertion: Automatic Pre-RTL Assertion Generation using Large Language Models with Progressive Regularization](https://mlsanity.com/paper/2505.07995/) (2025)
- [AssertGen: Enhancement of LLM-aided Assertion Generation through Cross-Layer Signal Bridging](https://mlsanity.com/paper/2509.23674/) (2025)
- [AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications](https://mlsanity.com/paper/2605.27472/) (2026)
- [Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations](https://mlsanity.com/paper/2609.05658/) (2026)

## Abstract (arXiv)

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.