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

Saeid Rajabi, Chengmo Yang, Satwik Patnaik

63rd Design Automation Conference (DAC 2026)

Abstract

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.

BibTeX

@article{rajabi2025stellar,
  title={STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification},
  author={Rajabi, Saeid and Yang, Chengmo and Patnaik, Satwik},
  journal={arXiv preprint arXiv:2601.19903},
  year={2025}
}