{"ID":2835342,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2601.19903","arxiv_id":"2601.19903","title":"STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification","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.","short_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...","url_abs":"https://arxiv.org/abs/2601.19903","url_pdf":"https://arxiv.org/pdf/2601.19903v3","authors":"[\"Saeid Rajabi\",\"Chengmo Yang\",\"Satwik Patnaik\"]","published":"2025-11-28T05:31:07Z","proceeding":"cs.AR","tasks":"[\"cs.AR\",\"cs.AI\"]","methods":"[\"Large Language Model\"]","has_code":false}