# Spec2Assertion: Automatic Pre-RTL Assertion Generation using Large Language Models with Progressive Regularization

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 May 2025.

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

- [Hybrid-NL2SVA: Integrating RAG and Finetuning for LLM-based NL2SVA](https://mlsanity.com/paper/2506.21569/) (2025)
- [SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation](https://mlsanity.com/paper/2605.25181/) (2026)
- [GoGoTB: Agentic RTL Verification with Specification-Grounded Coverage Closure](https://mlsanity.com/paper/2607.26181/) (2026)
- [Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations](https://mlsanity.com/paper/2609.05658/) (2026)
- [Arcane: An Assertion Reduction Framework through Semantic Clustering and MCTS-Guided Rule Exploring](https://mlsanity.com/paper/2605.10107/) (2026)
- [HierSVA: A Data Synthesis Pipeline, Dataset, and Benchmark for LLM-Driven Hierarchical Hardware Formal Verification](https://mlsanity.com/paper/2606.13706/) (2026)
- [EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations](https://mlsanity.com/paper/2609.26751/) (2026)
- [A Survey on LLM-Integrated Hardware Design Verification](https://mlsanity.com/paper/2610.10580/) (2026)

## Abstract (arXiv)

SystemVerilog Assertions (SVAs) play a critical role in detecting and debugging functional bugs in digital chip design. However, generating SVAs has traditionally been a manual, labor-intensive, and error-prone process. Recent advances in automatic assertion generation, particularly those using machine learning and large language models (LLMs), have shown promising potential, though most approaches remain in the early stages of development. In this work, we introduce Spec2Assertion, a new technique for automatically generating assertions from design specifications prior to RTL implementation. It leverages LLMs with progressive regularization and incorporates Chain-of-Thought (CoT) prompting to guide assertion synthesis. Additionally, we propose a new evaluation methodology that assesses assertion quality across a broad range of scenarios. Experiments on multiple benchmark designs show that Spec2Assertion generates 70% more syntax-correct assertions with 2X quality improvement on average compared to a recent state-of-the-art approach.