# AssertGen: Enhancement of LLM-aided Assertion Generation through Cross-Layer Signal Bridging

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Sep 2025.

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

- [AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications](https://mlsanity.com/paper/2605.27472/) (2026)
- [QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis](https://mlsanity.com/paper/2603.14239/) (2026)
- [SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation](https://mlsanity.com/paper/2605.25181/) (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)

Assertion-based verification (ABV) serves as a crucial technique for ensuring that register-transfer level (RTL) designs adhere to their specifications. While Large Language Model (LLM) aided assertion generation approaches have recently achieved remarkable progress, existing methods are still unable to effectively identify the relationship between design specifications and RTL designs, which leads to the insufficiency of the generated assertions. To address this issue, we propose AssertGen, an assertion generation framework that automatically generates SystemVerilog assertions (SVA). AssertGen first extracts verification objectives from specifications using a chain-of-thought (CoT) reasoning strategy, then bridges corresponding signals between these objectives and the RTL code to construct a cross-layer signal chain, and finally generates SVAs based on the LLM. Experimental results demonstrate that AssertGen outperforms the existing state-of-the-art methods across several key metrics, such as pass rate of formal property verification (FPV), cone of influence (COI), proof core and mutation testing coverage.
