# LAAG-RV: LLM Assisted Assertion Generation for RTL Design Verification

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Aug 2024.

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

- [AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL](https://mlsanity.com/paper/2503.19174/) (2025)
- [Towards LLM-based Root Cause Analysis of Hardware Design Failures](https://mlsanity.com/paper/2507.06512/) (2025)
- [Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification](https://mlsanity.com/paper/2605.06434/) (2026)
- [SafeTune: Mitigating Data Poisoning in LLM Fine-Tuning for RTL Code Generation](https://mlsanity.com/paper/2604.27238/) (2026)
- [STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification](https://mlsanity.com/paper/2601.19903/) (2025)
- [DUET: Agentic Design Understanding via Experimentation and Testing](https://mlsanity.com/paper/2512.06247/) (2025)
- [Agentic Electronic Design Automation: A Handoff Perspective](https://mlsanity.com/paper/2606.19795/) (2026)

## Abstract (arXiv)

Writing SystemVerilog Assertions (SVA) is an important but complex step in verifying Register Transfer Level (RTL) designs. Conventionally, experts need to understand the design specifications and write the SVA assertions, which is time-consuming and error-prone. However, with the recent advancement of transformer models, the Large Language Models (LLMs) assisted assertion generation for design verification is gaining interest in recent times. Motivated by this, we proposed a novel LLM-based framework, LAAG-RV, to generate SVA from the natural language specifications of the design. Our framework provides a one-time Verilog loop for signal synchronization in the generated SVA to improve the generated assertion quality. For our experiments, we created a custom LLM based on OpenAI GPT-4. Furthermore, we developed test cases to validate the LLM-generated assertions. Initial observations show that some generated assertions contain issues and did not pass all the test cases. However, by iteratively prompting the LLMs using carefully crafted manual prompts derived from test case failures in a simulator, the framework can generate correct SVAs. Our results on OpenTitan designs demonstrate that LLMs significantly simplify the process of generating assertions, making it efficient and less error-prone.