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.

翻译：形式化验证（FV）依赖高质量SystemVerilog断言（SVA），但手动编写过程缓慢且易出错。现有基于大语言模型（LLM）的方法要么从零开始生成断言，要么忽略硬件设计中的结构模式及专家编写的断言。本文提出STELLAR，首个利用结构相似性引导LLM生成SVA的框架。STELLAR将RTL模块表示为AST结构指纹，从知识库中检索结构相关的（RTL, SVA）配对，并将其整合为结构引导提示。实验表明，STELLAR在语法正确性、风格一致性和功能正确性方面均表现优越，凸显了结构感知检索作为工业级FV领域的可行方向。