用大模型自动生成高质量Verilog断言，减少人工错误。
Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting
- 分任务微调+迭代提示，提升断言正确性。
- 功能正确断言数量提升7.3倍，语法错误减少26%。
- 适合芯片设计验证人员快速生成可靠断言。
形式化属性验证（FPV）通过SystemVerilog断言（SVA）确保设计与规范的一致性。但编写SVA耗时且学习曲线陡峭。本文提出基于大语言模型（LLM）的自动化SVA生成流程，名为\ToolName。引入新型分任务聚焦微调方法，有效解决基线LLM生成的功能性错误断言问题，使功能正确断言数量提升7.3倍。针对语法与语义错误频发的问题，设计了迭代式优化方法，通过系统重提示修正错误，并结合自定义编译器生成有意义错误提示，引导模型持续改进。实验表明，该方法使无语法错误断言数量增加26%，显著提升验证效率，具备推动FPV流程自动化的潜力。
原文摘要 · Abstract (English)
Formal Property Verification (FPV), using SystemVerilog Assertions (SVA), is crucial for ensuring the completeness of design with respect to the specification. However, writing SVA is a laborious task and has a steep learning curve. In this work, we present a large language model (LLM) -based flow to automatically generate high-quality SVA from the design specification documents, named \ToolName. We introduce a novel sub-task-focused fine-tuning approach that effectively addresses functionally incorrect assertions produced by baseline LLMs, leading to a remarkable 7.3-fold increase in the number of functionally correct assertions. Recognizing the prevalence of syntax and semantic errors, we also developed an iterative refinement method that enhances the LLM's initial outputs by systematically re-prompting it to correct identified issues. This process is further strengthened by a custom compiler that generates meaningful error messages, guiding the LLM towards improved accuracy. The experiments demonstrate a 26\% increase in the number of assertions free from syntax errors using this approach, showcasing its potential to streamline the FPV process.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。