# STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 29 references that are in the map.
- First posted on arXiv 28 Nov 2025.

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

- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [DeepGate: Learning Neural Representations of Logic Gates](https://mlsanity.com/paper/2111.14616/) (2021)
- [AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2411.14436/) (2024)
- [HW2VEC: A Graph Learning Tool for Automating Hardware Security](https://mlsanity.com/paper/2107.12328/) (2021)
- [AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL](https://mlsanity.com/paper/2503.19174/) (2025)
- [AutoSVA: Democratizing Formal Verification of RTL Module Interactions](https://mlsanity.com/paper/2104.04003/) (2021)
- [FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware](https://mlsanity.com/paper/2410.23299/) (2024)
- [Enhancing Large Language Models for Hardware Verification: A Novel SystemVerilog Assertion Dataset](https://mlsanity.com/paper/2503.08923/) (2025)
- [LAAG-RV: LLM Assisted Assertion Generation for RTL Design Verification](https://mlsanity.com/paper/2409.15281/) (2024)
- [Are LLMs Ready for Practical Adoption for Assertion Generation?](https://mlsanity.com/paper/2502.20633/) (2025)

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

- [Agentic Electronic Design Automation: A Handoff Perspective](https://mlsanity.com/paper/2606.19795/) (2026)

## Abstract (arXiv)

Formal Verification (FV) relies on high-quality SystemVerilog Assertions (SVAs), but the manual writing process is slow and error-prone. Existing LLM-based approaches either generate assertions from scratch or ignore structural patterns in hardware designs and expert-crafted assertions. This paper presents STELLAR, the first framework that guides LLM-based SVA generation with structural similarity. STELLAR represents RTL blocks as AST structural fingerprints, retrieves structurally relevant (RTL, SVA) pairs from a knowledge base, and integrates them into structure-guided prompts. Experiments show that STELLAR achieves superior syntax correctness, stylistic alignment, and functional correctness, highlighting structure-aware retrieval as a promising direction for industrial FV.