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.

翻译：形式化验证依赖于高质量的系统验证语言断言，但人工编写过程缓慢且易出错。现有基于大语言模型的方法要么从零生成断言，要么忽略了硬件设计中的结构模式与专家编写的断言。本文提出STELLAR，首个通过结构相似性引导基于大语言模型的SVA生成的框架。STELLAR将RTL模块表示为抽象语法树结构指纹，从知识库中检索结构相关的(RTL, SVA)对，并将其整合到结构引导的提示中。实验表明，STELLAR在语法正确性、风格对齐性和功能正确性方面均表现优异，证明了结构感知检索在工业级形式化验证中的广阔前景。