STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification
This addresses the problem of improving efficiency and accuracy in formal verification for hardware design engineers, representing an incremental advancement by integrating structural patterns into existing LLM approaches.
The paper tackles the slow and error-prone manual writing of SystemVerilog Assertions for formal verification by introducing STELLAR, a framework that uses structural similarity to guide LLM-based generation, achieving superior syntax correctness, stylistic alignment, and functional correctness.
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.