用硬件结构引导大模型生成更准确的断言，提升芯片验证效率。
STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification
- 通过抽象语法树提取电路模块结构指纹，匹配相似设计与断言对。
- 在三个真实项目中，语法正确率提升至92.3%，功能正确性提高41%。
- 适合芯片验证工程师和自动化验证工具开发者使用。
形式化验证依赖高质量的SystemVerilog断言（SVAs），但手动编写过程缓慢且易出错。现有基于大模型的方法或从零生成断言，或忽视硬件设计与专家断言中的结构模式。本文提出STELLAR，首个利用结构相似性引导大模型生成SVAs的框架。STELLAR将RTL模块表示为抽象语法树（AST）结构指纹，从知识库中检索结构相关的（RTL, SVA）配对，并融入结构引导提示中。实验表明，STELLAR在语法正确性、风格一致性及功能正确性上均优于基线方法，凸显结构感知检索在工业级形式化验证中的潜力。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。