cs.LGSep 4, 2026

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

Authors: FNU Aditi

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

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.

Figures & tables

Figure 1: Controlled metamorphic evaluation. VERT records are filtered to the supported conditional-control fragment before constructing the stratified 40-program evaluation set. Each applicable original/transformed pair is then processed with the same model, prompt, and generation settings. The transformation changes source representation while preserving the intended Boolean behavior.
StageCount
Raw VERT records20,000
Synchronous / asynchronous10,000 / 10,000
Conditional-control candidates10,400
Excluded by quality filtering1,243
Quality-filtered eligible pool9,157
Controlled RTL programs40
Table 1: Dataset construction and experimental scope.
IDTransformationOriginal exampleTransformed example
T1Operand reorderinga && b && cc && b && a
T2Identifier renamingvalid && readyid_000 && id_001
T3Redundant parenthesesa || b && c((a) || (b) && (c))
Table 2: Controlled RTL transformations. The examples are schematic; the implementation transforms the full RTL condition while preserving its intended Boolean meaning.
ModelTransformPairsBeh.Base.Trans.Δ\DeltaLostGainedCRIFFlip
Qwen2.5-Coder-7BT1 operand order3828070.0%67.1%−2.9-2.9191190.3%9.7%10.7%
Qwen2.5-Coder-7BT2 identifier rename4029569.8%68.8%−1.0-1.0211889.8%10.2%13.2%
Qwen2.5-Coder-7BT3 parentheses4029569.8%58.6%−11.2-11.2451278.2%21.8%19.3%
DeepSeek-Coder-V2-LiteT1 operand order3828053.2%58.2%+5.0+5.0243883.9%16.1%22.1%
DeepSeek-Coder-V2-LiteT2 identifier rename4029553.9%63.7%+9.8+9.8316080.5%19.5%30.8%
DeepSeek-Coder-V2-LiteT3 parentheses4029553.9%49.8%−4.1-4.1433173.0%27.0%25.1%
Table 3: Controlled evaluation results. “Lost” denotes baseline-correct behaviors that become wrong after transformation; “Gained” denotes the reverse. Δ\Delta is transformed minus baseline accuracy in percentage points. CR = conditional robustness; IF = invariance failure.
ModelTransformAccuracy Δ\DeltaInvariance failureAny-flip rate
Qwen2.5-Coder-7BT1−2.9-2.9 [ −10.4-10.4 , +2.9+2.9 ]9.7% [2.6, 19.3]10.7% [4.7, 18.4]
Qwen2.5-Coder-7BT2−1.0-1.0 [ −7.3-7.3 , +5.2+5.2 ]10.2% [4.7, 16.6]13.2% [8.3, 18.5]
Qwen2.5-Coder-7BT3−11.2-11.2 [ −21.3-21.3 , −2.2-2.2 ]21.8% [10.5, 34.1]19.3% [10.7, 28.9]
DeepSeek-Coder-V2-LiteT1+5.0+5.0 [ −5.2-5.2 , +15.6+15.6 ]16.1% [8.4, 24.5]22.1% [14.9, 30.3]
DeepSeek-Coder-V2-LiteT2+9.8+9.8 [ −2.5-2.5 , +21.6+21.6 ]19.5% [8.8, 30.6]30.8% [23.0, 38.9]
DeepSeek-Coder-V2-LiteT3−4.1-4.1 [ −13.7-13.7 , +6.1+6.1 ]27.0% [17.1, 36.9]25.1% [17.7, 32.8]
Table 4: Clustered bootstrap statistics (10,000 replicates; resampling unit = RTL pair). Values are point estimate [95% percentile CI]. Accuracy delta is in percentage points.
Figure 2: Invariance failure: fraction of baseline-correct assignment behaviors that become incorrect after a semantics-preserving transformation. Error bars are 95% clustered bootstrap percentile intervals.
Figure 3: Aggregate accuracy change and invariance failure measure different properties. In particular, DeepSeek T1 and T2 improve aggregate accuracy while still losing 16.1% and 19.5% of baseline-correct behaviors, respectively.
ModelTransformFailure modeObserved effect
QwenT1Dropped prior-branch guardAn else-if assignment loses the required negation of an earlier condition after operands are reordered.
QwenT2Wrong branch polarityA renamed else-if path is generated using the previous disjunctive branch positively rather than requiring that branch to be false.
QwenT3Boolean-structure corruptionA negated disjunction is rewritten as a disjunction of negations, or an original OR relationship becomes an AND.
DeepSeekT1Missing path predicateA reordered condition causes one of the earlier branch constraints to disappear from the assignment antecedent.
DeepSeekT2Output-contract violationMultiple assignment behaviors are merged into a single conjunctive consequent instead of one property per behavior.
DeepSeekT3Guard inversion / omissionRedundant parentheses trigger positive conditions to be negated, required guards to disappear, or prior-branch structure to be inverted.
Table 5: Representative failure modes observed in the 30 manually inspected correct-to-wrong transitions. Examples are summarized at the logical level rather than reproduced verbatim.
More in this topic

SystemVerilog Assertion Generation

See all 11 papers

Explore similar work

CardsList
May 24, 2026

SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation

Existing Large Language Model (LLM) approaches to SystemVerilog Assertion (SVA) generation primarily focus on syntactic validity and formal verification outcomes, while semantic alignment between generated assertions and natural language specifications remains difficult to quantify. As a result, hallucinated or misaligned SVAs can reduce confidence and increase debugging efforts in the absence of golden RTL. This paper presents SpecAlign, a framework for semantic evaluation and refinement of LLM-generated SVAs. SpecAlign introduces two iterative alignment loops that assess both natural language properties and SVAs against the design specification using entailment-based classification. We improve alignment decisions by generating multiple reasoning paths using chain-of-thought prompting and aggregating them via a self-consistency voting mechanism. Misaligned assertions are analyzed to generate actionable feedback for refinement. We further define a quantitative alignment score to measure semantic consistency across iterations. Experimental results demonstrate that SpecAlign effectively detects semantic inconsistencies and improves assertion alignment without relying on golden RTL, providing a scalable complement to traditional formal verification evaluation metrics.

Jaime Rafael Imperial, Hao Zheng

Bellini College of Cybersecurity, AI, and Computing University of South Florida Tampa, USA

Formal Hardware VerificationSystemVerilog Assertion GenerationLLM-Based Program SynthesisSemantic Alignment
AskPDF
Mar 15, 2026

QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis

SystemVerilog Assertions (SVAs) are crucial for hardware verification. Recent studies leverage general-purpose LLMs to translate natural language properties to SVAs (NL2SVA), but they perform poorly due to limited data. We propose a data synthesis framework to tackle two challenges: the scarcity of high-quality real-world SVA corpora and the lack of reliable methods to determine NL-SVA semantic equivalence. For the former, large-scale open-source RTLs are used to guide LLMs to generate real-world SVAs; for the latter, bidirectional translation serves as a data selection method. With the synthesized data, we train CodeV-SVA, a series of SVA generation models. Notably, CodeV-SVA-14B achieves 75.8% on NL2SVA-Human and 84.0% on NL2SVA-Machine in Func.@1, matching or exceeding advanced LLMs like GPT-5 and DeepSeek-R1.

Yutong Wu, Chenrui Cao, Pengwei Jin +6

SKL of Processors, Institute of Computing Technology, CAS Beijing, China · University of Chinese Academy of Sciences Beijing, China · University of Science and Technology of China Hefei, Anhui, China +1

SystemVerilog Assertion GenerationFormal Hardware VerificationLLM Code GenerationSynthetic Data Generation for Language Models
AskPDF
May 26, 2026

AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications

Assertion-based verification (ABV) is a cornerstone of modern hardware design, yet manually translating design intent into formal SystemVerilog Assertions (SVAs) remains labor-intensive and error-prone. While Large Language Models (LLMs) show promise for automating this process, existing benchmarks remain limited by unrealistic task formulations, weak specification inputs, and oversimplified evaluation. To address these limitations, we introduce AssertLLM2, an open-source benchmark for realistic assertion generation in hardware verification. AssertLLM2 contains 83 real-world designs across 13 functional categories. For each design, the benchmark provides a structured design specification, a verified dependency-complete golden RTL, and systematically mutated buggy RTL variants. These support two practical settings: bug-prevention, where assertions are generated from specifications to guard against design errors, and bug-hunting, where assertions are generated to expose discrepancies between intended behavior and faulty implementations. To the best of our knowledge, AssertLLM2 is the first benchmark to explicitly use buggy RTL as input to evaluate bug-detection capability. AssertLLM2 further adopts a more rigorous evaluation framework spanning syntactic validity, formal provability, coverage, and mutation-based bug detection. Our benchmark enables a more realistic and extensive assessment of assertion generation and establishes rigorous baselines for state-of-the-art LLMs in practical hardware verification.

Yuchao Wu, Wenji Fang, Jing Wang +3

Hong Kong University of Science and Technology (HKUST)

Formal Hardware VerificationLLM EvaluationSystemVerilog Assertion GenerationBenchmark Design
AskPDF