SpecAlign：面向SystemVerilog断言生成的语义对齐框架

现有基于大语言模型（LLM）的SystemVerilog断言（SVA）生成方法主要关注语法有效性和形式验证结果，而生成断言与自然语言规约之间的语义对齐仍难以量化。因此，在缺少黄金RTL（golden RTL）的情况下，幻觉或错位的SVA会降低置信度并增加调试工作量。本文提出SpecAlign，一个用于对LLM生成的SVA进行语义评估与精化的框架。SpecAlign引入两个迭代对齐循环，使用基于蕴含的分类，将自然语言属性和SVA分别与设计规约进行对照评估。我们通过思维链（chain-of-thought）提示生成多条推理路径，并通过自一致性投票机制加以聚合，从而改进对齐判定。对未对齐的断言进行分析，生成可操作的反馈以供精化。我们进一步定义了一个量化对齐分数，用于衡量跨迭代的语义一致性。实验结果表明，SpecAlign能够在不依赖黄金RTL的情况下有效检测语义不一致并改善断言对齐，为传统形式验证评估指标提供了可扩展的补充。