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

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 12 references that are in the map.
- First posted on arXiv 4 Sep 2026.

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

- [Qwen2.5-Coder Technical Report](https://mlsanity.com/paper/2409.12186/) (2024)
- [DeepSeek-Coder-V2: Breaking the Barrier of Closed-Source Models in Code Intelligence](https://mlsanity.com/paper/2406.11931/) (2024)
- [(Security) Assertions by Large Language Models](https://mlsanity.com/paper/2306.14027/) (2023)
- [AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2411.14436/) (2024)
- [AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL](https://mlsanity.com/paper/2503.19174/) (2025)
- [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)
- [Metamorphic Testing of Deep Code Models: A Systematic Literature Review](https://mlsanity.com/paper/2507.22610/) (2025)

## Built on by (most cited first, 1 of 1)

- [EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations](https://mlsanity.com/paper/2609.26751/) (2026)

## Abstract (arXiv)

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.