PaperlayerView exact revision on arXiv

Source-linked AI summary

Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations

FNU Aditi

arXiv:2609.05658v1cs.LG

TL;DR

Point accuracy evaluates LLM-generated SVA on a single RTL representation, not whether correctness survives equivalent rewrites. This paper tests that stability across three transformations and finds correct-to-wrong failures across all six model–transformation conditions.

  • Problem

    Point correctness does not establish whether a correct SVA generation remains correct under a semantics-preserving RTL rewrite.

    Source: §1 · p. 1

  • Method

    The study evaluates two open code models on a stratified 40-program VERT subset using operand reordering, identifier renaming, and redundant parenthesization.

    Source: §8 · p. 9

  • Results

    9.7%–27.0% of baseline-correct assignment behaviors become incorrect across the six model–transformation conditions.

    Source: §1 · p. 2, §8 · p. 9

  • Takeaways & Limitations

    Point accuracy alone is insufficient to characterize SVA-generation reliability because aggregate gains can coexist with regressions in previously correct behaviors.

    Source: §8 · p. 9

    The 40-program sample exposes repeated failures but does not support precise population-level estimates over all 20,000 VERT records.

    Source: §6 · p. 8

Abstract

from arXiv · show

Large language models (LLMs) are increasingly being explored for automating SystemVerilog Assertion (SVA) generation, yet most evaluations report correctness on a single syntactic representation of an input. Such point accuracy does not reveal whether a model's correct output is stable when the same RTL behavior is written differently. This paper presents a controlled metamorphic evaluation of LLM-based SVA generation under semantics-preserving RTL transformations. Starting from the VERT dataset, we construct a quality-filtered conditional-control pool and a stratified 40-program evaluation set containing 295 assignment behaviors. We evaluate two open code models, Qwen2.5-Coder-7B and DeepSeek-Coder-V2-Lite, with an identical evaluation prompt and greedy decoding. Three transformations are studied: operand reordering, deterministic identifier renaming, and redundant parenthesization. Beyond baseline and transformed accuracy, we measure conditional robustness, invariance failure, and any-flip rate, with 10,000-sample clustered bootstrap intervals at the RTL-program level. Across all six model-transformation conditions, 9.7%-27.0% of behaviors that were correct on the original RTL become incorrect after a semantics-preserving transformation. Aggregate accuracy can therefore hide substantial instability: under identifier renaming, DeepSeek-Coder-V2-Lite improves from 53.9% to 63.7% accuracy while 19.5% of its originally correct behaviors fail. Manual review of 30 sampled correct-to-wrong transitions identifies dropped path predicates, branch-polarity errors, Boolean-structure corruption, and output-contract violations. The results show that point accuracy alone is insufficient for characterizing LLM reliability in assertion generation and motivate robustness-aware evaluation for AI-assisted hardware verification.

1 Introduction

Most SVA-generation evaluations judge correctness on one RTL representation, leaving stability under semantics-preserving rewrites unmeasured. This paper studies that gap with a controlled metamorphic evaluation.

1 Introduction

  • A useful assertion must encode the correct control-flow precondition, timing relation, and consequent, not merely be syntactically valid.The experiment uses two open code models, an identical prompt, deterministic decoding, three transformations, behavior-level scoring, and clustered bootstrap statistics.Source: §1 · pp. 1–2
  • Point correctness leaves unanswered whether a correct assertion remains correct after a semantics-preserving RTL rewrite.The paper studies operand reordering, identifier changes, and redundant parentheses.Source: §1 · p. 1
  • Representation stability matters because RTL is routinely reformatted, refactored, generated, renamed, or normalized.A verification assistant that succeeds only on one surface form can appear accurate on a benchmark yet remain brittle in deployment.Source: §1 · p. 1
  • 9.7%–27.0% of baseline-correct behaviors fail across six model–transformation conditions, including cases where aggregate accuracy improves.The study frames this as representation sensitivity on its controlled set, not evidence that models do not understand RTL semantics.Source: §1 · p. 2

2 Background and Related Work

SVA generation requires recovering the full execution path for each assignment, while prior work has developed generation systems and datasets. This study brings metamorphic robustness testing to that task.

2.1 SVA Generation

  • An assignment in an else-if branch may require the full path predicate !a && b, rather than b alone.Omitting an earlier branch's negation yields a logically weaker, incorrect assertion.Source: §2.1 · p. 2
  • Prior SVA-generation work includes hybrid rule-based and machine-learning techniques, a later validatable generation pipeline, security-focused assertion generation [3], full-specification processing [4], and RTL-aware methods [5] [9].VERT provides RTL/SVA pairs and explicit assertion references [6]. This paper uses it for robustness evaluation rather than proposing another generation architecture or fine-tuning method [6].Source: §2.1 · p. 2

2.2 Metamorphic Testing and Code-Model Robustness

  • Metamorphic testing checks necessary relations across related executions, and code-model studies have used renaming and other semantics-preserving transformations [8].Here the generated artifact is a formal property with an antecedent tied to RTL control flow, and scoring distinguishes aggregate gains from losses of previously correct behaviors.Source: §2.2 · p. 2

3 Study Design

The study asks how transformations affect aggregate accuracy, retained correctness, and failure modes. It builds a controlled conditional-control sample from VERT and treats RTL program pairs as the resampling unit.

3.1 Research Questions

  • The study asks how semantics-preserving transformations change behavior-level accuracy, how often baseline-correct behaviors remain correct, and what errors appear in sampled regressions.These are the three research questions: aggregate accuracy, invariance, and qualitative failure modes.Source: §3.1 · pp. 2–3

3.2 Dataset Preprocessing and Quality Filtering

  • The controlled pool covers nested conditionals and multi-branch if/else trees, then excludes records with duplicate property names or unexpected property counts.The filter leaves 9,157 eligible examples, or 88.05% of the conditional-control candidate pool; the fragment is for consistent evaluation, not a judgment that excluded records are unsuitable for SVA generation.Source: §3.2 · p. 3

3.3 Controlled Evaluation Set

  • The evaluation set contains 40 stratified programs and 295 assignment behaviors, with 10 programs in each of four synchronous/asynchronous and control-structure groups.T1 applies to 38 programs and 280 behaviors, whereas T2 and T3 apply to all 40 programs and 295 behaviors; bootstrap resampling uses the RTL program/pair as the unit.Source: §3.3 · p. 3

3.4 Semantics-Preserving Transformations

The study applies three controlled RTL rewrites, evaluates original and transformed inputs under matched model settings, and scores each assignment behavior against its path condition and output contract.

3.4 Semantics-Preserving Transformations

  • T1 reverses safe homogeneous conjunction or disjunction operands, T2 consistently renames identifiers and inverse-maps outputs, and T3 adds redundant parentheses.Each transformation changes source representation while preserving the intended Boolean behavior; T1 avoids operator changes and distributive rewrites.Source: §3.4 · p. 3, Figure 1 · p. 4

3.5 Models and Evaluation Prompt

  • Both open code models receive the same evaluation prompt and deterministic generation settings for every original and transformed input.The prompt requires one property per assignment behavior and a concrete antecedent derived from the complete RTL control-flow path.Source: §3.5 · p. 4, §3.6 · p. 4

3.6 Behavior-Level Semantic Scoring

  • A behavior is correct only when the property meets the timing and output contract and its antecedent matches the reference path condition under the Boolean abstraction.The scorer parses a restricted Boolean grammar and checks propositional equivalence by exhaustive truth-table evaluation for expressions with at most 16 Boolean atoms; it does not model full four-state SystemVerilog semantics.Source: §3.6 · p. 4

3.7 Metrics

The metrics separate aggregate accuracy from retention of originally correct behaviors and from all correctness-state changes. Uncertainty is estimated by resampling RTL pairs, with percentile intervals interpreted descriptively.

3.7 Metrics

  • Accuracy delta is transformed accuracy minus baseline accuracy, so aggregate gains can coexist with substantial losses among originally correct behaviors.The distinction between ΔA and invariance failure is central to interpreting the metrics.Source: §3.7 · p. 5
  • Conditional robustness measures stability among behaviors correct on the original RTL, while any-flip rate counts all correctness-state changes.Baseline and transformed correct counts are B and T; R behaviors remain correct, L change from correct to wrong, and G from wrong to correct.Source: §3.7 · p. 5

3.8 Statistical Analysis

  • 95% percentile intervals for accuracy delta, invariance failure, and any-flip rate use 10,000 RTL-pair bootstrap replicates and are descriptive, not formal significance tests.The resampling unit is the RTL pair because assignment behaviors within a program are correlated.Source: §3.8 · p. 5

4 Results

Across the controlled results, transformations changed aggregate accuracy and caused some originally correct behaviors to fail in every model–transformation condition. Manual review found substantive generation errors, including lost path predicates, branch-polarity errors, Boolean-structure corruption, and output-contract violations.

4.1 RQ1: Aggregate Accuracy

  • 70.0% to 58.6% (−11.2 points) under T3 was Qwen2.5-Coder-7B’s largest accuracy reduction; DeepSeek accuracy rose under T1 and T2 but fell under T3.For DeepSeek-Coder-V2-Lite, T1 increased accuracy by 5.0 points, T2 by 9.8 points, and T3 decreased it by 4.1 points; only Qwen under T3 had an accuracy-delta interval excluding zero.Source: §4.1 · p. 5, Table 3 · p. 6

4.2 RQ2: Correctness Is Not Invariant

  • 9.7%–27.0% of originally correct behaviors failed after transformation across the six model–transformation conditions.Figure 2 shows invariance-failure estimates with clustered bootstrap intervals; every condition exhibits a nontrivial loss of previously correct behavior.Source: §4.2 · p. 5
  • 53.9% to 63.7% accuracy for DeepSeek-Coder-V2-Lite under T2 accompanied 31 correct-to-wrong losses and 60 wrong-to-correct gains; 19.5% of originally correct behaviors failed.The positive aggregate change therefore did not imply representation invariance.Source: §4.2 · p. 5
  • Figure 3 shows that conditions with positive accuracy change can still have high invariance failure, so positive ΔA is not evidence of representation invariance.Conditions to the right of the zero line improve aggregate accuracy.Source: §4.2 · p. 5

4.3 RQ3: Failure Analysis

  • All 15 sampled Qwen losses were genuine generation failures; 13 of 15 sampled DeepSeek losses were semantic or path-condition failures, and two violated the output contract.The 30 inspected losses included no scorer false positives in the final audit.Source: §4.3 · pp. 5–6
  • Reviewed failures included missing guards after operand reordering, errors composing nested control flow, and regressions despite parenthesization making Boolean grouping more explicit.The observed patterns motivate evaluating full nested control context rather than isolated Boolean expressions.Source: §4.3 · p. 6

5 Analysis and Implications

Aggregate accuracy and robustness measure different properties: models can gain overall accuracy while losing behaviors they previously handled correctly. The analysis compares transformation-specific instability and recommends adding robustness measures alongside conventional benchmark metrics.

5.2 Transformation-Specific Sensitivity

  • T3 has the largest invariance failure for both models: 21.8% for Qwen2.5-Coder-7B and 27.0% for DeepSeek-Coder-V2-Lite.T3 only adds grouping syntax, yet both models show their highest failure rates under this transformation; the experiment does not identify the cause.Source: §5.2 · p. 6, Figure 2 · p. 7

5.1 Point Accuracy and Robustness Measure Different Properties

  • DeepSeek T1 and T2 improve aggregate accuracy while losing 16.1% and 19.5% of baseline-correct behaviors, respectively.This illustrates why net accuracy change does not establish behavioral stability.Source: §5.1 · p. 6, Figure 3 · p. 7

5.2 Transformation-Specific Sensitivity

  • Under T2 identifier renaming, Qwen2.5-Coder-7B changes by −1.0 point and DeepSeek-Coder-V2-Lite by +9.8 points, while invariance failure is 10.2% and 19.5%, respectively.Thus, aggregate effects can differ across models while previously correct behaviors still regress.Source: §5.2 · p. 7, Figure 3 · p. 7
  • T1 shows that reordering commutative operands can disrupt reconstruction of the complete path condition, including enclosing and preceding branch predicates.The target assertion must integrate the edited expression with those other predicates, not merely translate the subexpression.Source: §5.2 · p. 7

5.3 Implications for Hardware-Verification Benchmarks

  • Benchmarks should add a robustness layer rather than replace existing metrics, reporting canonical-input accuracy, conditional robustness, and total flip rate.These quantities distinguish stable improvement from reshuffling which behaviors are correct.Source: §5.3 · p. 7
  • For synthetic or templated code, controlled rewrites provide a relatively inexpensive probe of dependence on naming, formatting, or expression-style cues.Such cues may not be part of the verification problem itself.Source: §5.3 · p. 7

6 Threats to Validity and Limitations

The study is a controlled robustness evaluation, not a population-level model ranking. Its scope is bounded by the sample, dataset fragment, two-model setup, Boolean scorer, and transformation assumptions.

Controlled sample size

  • The 40-program sample exposes repeated representation-sensitive failures but cannot support precise population-level estimates over all 20,000 VERT records.Accordingly, the work is framed as a controlled study rather than a definitive ranking of models or transformations.Source: §6 · p. 8

Dataset scope

  • The study covers nested conditionals and multi-branch if/else structures, so results may not generalize to temporal, arithmetic-heavy, protocol-level, or large industrial RTL.VERT also includes synthetic augmentation and differs from handwritten production RTL [6].Source: §6 · p. 8

Two models

  • Two models—one dense 7B code model and one MoE code model—are insufficient to support conclusions about architecture families, parameter count, or quantization.Both use local 4-bit MLX checkpoints.Source: §6 · p. 8

Boolean semantic abstraction

  • The scorer uses a restricted Boolean grammar and canonicalized equality/inequality expressions, not a full SystemVerilog simulator or formal engine.It does not model four-state X/Z semantics, arbitrary bit-vector arithmetic, or all temporal SVA constructs; the authors recommend future validation with a full compiler/formal/simulation stack.Source: §6 · p. 8

Transformation validity

  • T1 is restricted to safe homogeneous operator groups, T2 uses consistent alpha-renaming with inverse mapping, and T3 changes only parenthesization.The authors note that transformation-framework implementation bugs remain possible and emphasize releasing exact inputs and scripts for reproducibility.Source: §6 · p. 8

Behavior-level dependence

  • Assignment behaviors within a program are dependent, so the study resamples at the RTL-pair level rather than treating raw behavior counts as independent.The behavior counts in Table 3 should not be read as 280–295 independent experimental samples.Source: §6 · p. 8

No causal claim

  • Observed sensitivity establishes invariance failure under controlled rewrites, but does not establish its cause.The study does not attribute failures to memorization, contamination, tokenization, architecture, or lack of semantic understanding.Source: §6 · p. 8

7 Reproducibility

The reproducibility protocol specifies controlled generation and analysis settings, and the accompanying artifact is intended to expose implementation-level materials for independent reproduction.

Reproducibility

  • Both models use the same dataset, transformations, prompt, and deterministic generation configuration, with greedy decoding, temperature 0, and a 1,536-token maximum.Uncertainty intervals use 10,000 clustered bootstrap resamples at the RTL-program level; manual analysis samples five correct-to-wrong transitions per model–transformation condition.Source: §7 · pp. 8–9
  • The planned artifact includes preprocessing and transformation scripts, evaluation data and prompt, raw generations, paired records, scoring outputs, bootstrap analysis, and sampled failures.These materials supply implementation details omitted from the manuscript for readability.Source: §7 · p. 9

8 Conclusion

The paper evaluates whether SVA correctness survives semantics-preserving RTL changes and finds correct-to-wrong failures across the tested models and transformations. It concludes that net accuracy can conceal instability, while noting the study’s limited scale and controlled scope.

Conclusion

  • Across the tested model–transformation conditions, 9.7%–27.0% of baseline-correct assignment behaviors become incorrect after semantics-preserving RTL changes.The evaluation uses a stratified 40-program conditional-control subset of VERT and two open code models.Source: §8 · p. 9
  • DeepSeek-Coder-V2-Lite gains 9.8 percentage points under identifier renaming while losing 19.5% of behaviors it originally answered correctly.Robustness therefore needs direct measurement rather than inference from net accuracy change.Source: §8 · p. 9
  • The controlled, limited-scale study motivates future evaluation on broader RTL corpora, more model families, richer temporal SVA constructs, and full formal or simulation validation.The paper presents metamorphic testing as a way to examine whether correctness remains stable when irrelevant surface details change.Source: §8 · p. 9

A Evaluation Prompt Specification

The evaluation applies one prompt specification to both models and all original and transformed RTL inputs. It requires concrete properties that preserve the RTL’s control-flow and assignment semantics while following strict output-format rules.

A Evaluation Prompt Specification

  • The same prompt specification governs both models and every original or transformed RTL input, and its exact experimental wording is retained with the artifact.Source: A Evaluation Prompt Specification · p. 9
  • The prompt requires one property per assignment behavior, with a concrete Boolean antecedent derived from the complete control-flow path.Antecedents must include enclosing branches and negate earlier mutually exclusive branches for else-if paths.Source: A Evaluation Prompt Specification · p. 9
  • Properties must preserve Boolean operator precedence, negate compound expressions as a whole, use one implication, and match the assignment in the equality consequent.Source: A Evaluation Prompt Specification · p. 9
  • Synchronous records use the supplied clock event and |->, whereas asynchronous records omit event control and use |=>.Source: A Evaluation Prompt Specification · p. 9
  • Outputs must contain property declarations only, without procedural assertions, control-flow syntax, explanatory prose, or Markdown.Source: A Evaluation Prompt Specification · p. 9
Loading 2609.05658v1…