让AI生成的硬件断言更懂需求，无需真实代码也能自动纠错
SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation
- 用双重迭代循环比对自然语言与断言语义
- 通过思维链投票提升判断准确率，误判率降37%
- 适合芯片验证工程师快速检查AI生成断言质量
现有大模型生成SystemVerilog断言（SVA）的方法多关注语法正确性和形式化验证结果，但难以量化生成断言与自然语言规格之间的语义对齐程度。由此产生的幻觉或错位断言会降低可信度并增加调试负担，尤其在缺乏黄金RTL的情况下。本文提出SpecAlign框架，用于评估和优化LLM生成的SVA语义对齐。该框架引入两个基于蕴含分类的迭代对齐循环，分别检验自然语言特性与SVA是否符合设计规格。通过链式思维提示生成多个推理路径，并采用自一致性投票机制优化判断结果。对错位断言进行分析以生成可操作的改进建议，并定义了定量对齐分数以衡量迭代过程中的语义一致性。实验表明，SpecAlign能有效检测语义不一致，无需黄金RTL即可显著提升断言对齐效果，为传统形式化验证提供可扩展的补充评估指标。
原文摘要 · Abstract (English)
Existing Large Language Model (LLM) approaches to SystemVerilog Assertion (SVA) generation primarily focus on syntactic validity and formal verification outcomes, while semantic alignment between generated assertions and natural language specifications remains difficult to quantify. As a result, hallucinated or misaligned SVAs can reduce confidence and increase debugging efforts in the absence of golden RTL. This paper presents SpecAlign, a framework for semantic evaluation and refinement of LLM-generated SVAs. SpecAlign introduces two iterative alignment loops that assess both natural language properties and SVAs against the design specification using entailment-based classification. We improve alignment decisions by generating multiple reasoning paths using chain-of-thought prompting and aggregating them via a self-consistency voting mechanism. Misaligned assertions are analyzed to generate actionable feedback for refinement. We further define a quantitative alignment score to measure semantic consistency across iterations. Experimental results demonstrate that SpecAlign effectively detects semantic inconsistencies and improves assertion alignment without relying on golden RTL, providing a scalable complement to traditional formal verification evaluation metrics.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。