A Formally Verified Dataset for Testing Whether LLMs Understand Hardware Behavior
Large language models are increasingly being used to generate SystemVerilog Assertions from natural-language specifications and register-transfer-level designs. These assertions are the backbone of hardware verification, expressing safety and temporal properties that check whether a digital circuit behaves as intended. The problem is that RTL admits many implementations of the same external behavior: state encodings, conditional structures, helper expressions, and update styles can all change while the observable behavior remains identical. An assertion that is correct for one implementation may fail or behave differently for another semantically equivalent implementation.
FNU Aditi introduces EquivSVA, a formally verified dataset designed to study this specific problem. The paper's core insight is that existing datasets and benchmarks organize examples around isolated RTL files or tasks, but that a complementary need exists: testing whether a generated assertion captures externally observable behavior or depends on incidental details of one particular RTL implementation.
What Existing Resources Cover and What They Miss
Several prior resources address different aspects of the assertion-generation pipeline. VERT provides large-scale RTL-to-SVA training data for fine-tuning language models. FVEval benchmarks LLM capabilities across formal-verification subtasks including natural-language-to-SVA generation. AssertionBench offers curated Verilog designs with formally verified assertions for quantitative comparison. CodeV-SVA develops RTL-grounded data synthesis for specialized models. Veri2 provides formally filtered RTL-SVA pairs organized into quality tiers. AssertLLM2 supplies real-world designs with specifications, golden RTL, and systematically mutated buggy RTL.
What none of these resources provide is a controlled equivalence dimension. EquivSVA adds a new axis: behavior families, where multiple structurally distinct but formally equivalent RTL implementations are stored together with shared gold properties and controlled mutants. The goal is complementary rather than competitive: different resources serve different needs, and EquivSVA's contribution is a reusable representation for studying whether assertion-generation systems capture behavioral intent rather than implementation-specific structure.
The Dataset Design: Behavior Families as the Core Unit
EquivSVA's basic unit is the behavior family, represented as ℱ = (B, {Ri}⁴ᵢ₌₁, P, M, E). Here B is a machine-readable behavior specification, Ri are four reference RTL implementations, P is the shared set of gold behavioral properties, M is a set of three controlled mutants, and E is formal-validation evidence.
The four reference implementations are intentionally different in structure. Depending on the family type, variation spans state encoding, case versus nested conditional control, factored flag logic, sequential versus ternary updates, and function-based update expressions. The intended external behavior is held constant. Gold properties are defined over module-interface signals rather than implementation-specific internal state, so the same behavioral specification applies across variants.
The dataset contains 120 behavior families across 12 categories: arbiter, counter, FIFO control, handshake, interrupt control, mode controller, protocol controller, pulse/event, rate limiter, saturating arithmetic, sequence detector, and timer/watchdog. Each category contains exactly 10 families. The final corpus includes 80 finite-state-machine families, 27 register-rule families, and 13 multi-register-rule families. This balance is deliberate: it makes category-level comparisons straightforward and prevents overall metrics from being dominated by one frequently generated behavior class.
The 914 gold properties consist of 131 invariants and 783 next-cycle implications. Family-level property counts range from 5 to 13, with a mean of 7.62. Properties are written to describe externally observable functionality and avoid implementation-specific internal state names, which is central to the family abstraction.
Construction, Mutants, and Formal Validation
Families are generated from explicit machine-readable specifications rather than by independently sampling unrelated RTL files. Three generator paths produce finite-state machines, single-register rule systems, and multi-register rule systems. Each generator emits multiple implementation styles from the same behavior description, so variants share intended semantics but differ in control structure and coding form.
Each family contains three controlled mutants designed to change behavior in a controlled way. Mutation operators include dropped transitions, forced exits, ignored control conditions, missing updates, altered clear or enable behavior, and incorrect saturation. These mutants are not intended to model the full distribution of industrial hardware bugs; they provide known behavior-changing alternatives against which assertions can be tested.
Every final family passes a fixed 17-job validation suite using Yosys and SymbiYosys-based infrastructure with SMT backends including Bitwuzla. Three jobs compare alternate reference implementations against the canonical implementation. Four proof jobs exercise the family gold-property set across all four reference implementations. Four cover jobs check associated reachability witnesses. Three jobs establish that each controlled mutant is distinguishable from the reference behavior. The final three jobs run the family gold-property harness against each mutant in bounded model-checking mode and require an expected assertion failure.
The validation results are comprehensive: 2,040 total job records, all passing. This includes 360/360 RTL equivalence checks, 480/480 gold-property proofs, 480/480 reachability checks, 360/360 mutant distinguishability checks, and 360/360 gold-property checks on mutants.
Case Study: What Qwen2.5-Coder-7B Gets Wrong
The paper includes a held-out case study evaluating Qwen2.5-Coder-7B-Instruct on the untouched test split of 24 families and 96 RTL inputs. Decoding uses a public 4-bit MLX checkpoint with greedy decoding. The prompt requests interface-only behavioral SVAs and prohibits implementation-specific internal signals.
The results are instructive. Of 293 interface-only generated properties, 93 (31.7%) are formally sound. Forty-five of 96 RTL tasks produce at least one sound property. At the family level, eight of 24 families produce at least one sound property for all four equivalent implementations, while eight families produce none for any implementation.
Most revealing is the variant sensitivity: the number of sound properties changes across equivalent implementations for 14 of 24 families (58.3%). This does not by itself identify the cause of the difference, nor does it imply that one coding style is globally more difficult. But it demonstrates the type of controlled analysis that the family structure enables: assertion quality varies even when intended behavior is unchanged.
Mutation testing provides an additional perspective. Across 279 checks pairing a sound generated property with a family mutant, 16 checks detect the behavioral change, covering 11 of the 72 unique mutants in the test families. This is treated as a demonstration metric rather than a complete measure of assertion quality.
Splits and Release
The v2.0 release provides fixed family-safe, category-stratified train, development, and test splits. All four RTL variants of a family remain in the same split, preventing a model from seeing one implementation during training and another during evaluation. The splits were generated deterministically: 72 families for training, 24 for development, and 24 for testing.
The public release contains the dataset manifest, split file, generators, construction and validation scripts, task-export code, baseline inference code, syntax, formal, and mutant evaluators, and the case-study result files. The repository is licensed with Apache-2.0 for source code and CC BY 4.0 for the dataset artifacts.
Limitations
EquivSVA is intentionally controlled and therefore has several limitations. The families are programmatically generated rather than mined from industrial code bases, which provides precise semantics and repeatable formal validation but may not capture the full structural complexity, naming conventions, or specification ambiguity present in production RTL. The 12 categories emphasize control logic, small state machines, counters, handshakes, and related behaviors, and do not attempt comprehensive coverage of large datapaths, caches, or deeply pipelined arithmetic units. The gold-property distribution is dominated by next-cycle implications and invariants, with longer-horizon liveness properties remaining an open direction. The equivalent variants share stylistic regularities from common generator families, so formal equivalence does not guarantee the variants are indistinguishable from independently authored RTL. Finally, the Qwen2.5-Coder-7B experiment is a single-model case study intended to demonstrate dataset usage, not to establish a model leaderboard.
What This Means in Practice
For researchers working on LLM-based hardware verification, EquivSVA provides a reusable foundation for controlled experiments that were previously difficult to conduct. The family structure enables questions that conventional RTL-to-SVA examples cannot support: whether a model produces sound properties for all variants, whether property quality changes by implementation style, whether generated assertions transfer across family members, and whether mutation sensitivity is stable across implementations.
The dataset also demonstrates that the gap between syntactic correctness and behavioral correctness is real in the assertion-generation domain. A model can generate syntactically valid SystemVerilog that passes type and format checks yet fail to capture the intended behavioral specification. By making equivalent implementations a first-class dataset element, EquivSVA provides a basis for studying this gap systematically and for developing training objectives that encourage representation invariance or contrastive reasoning across equivalent designs.
The paper is a 9-page contribution with two figures and five tables. It does not present a new model architecture or a dramatic performance improvement; it presents a carefully constructed evaluation resource. Its value will be realized over time as other researchers adopt it for controlled studies of assertion-generation robustness, and its open release at https://github.com/aditigupta96/EquivSVA makes it immediately available for that purpose.