🤖 AI

SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation

本文提出了 SpecAlign，这是一个通过基于迭代蕴含的评估、思维链推理和自一致性投票来增强大语言模型生成的 SystemVerilog 断言与自然语言规范之间语义对齐的框架，从而在不依赖黄金 RTL 的情况下提高了断言的准确性。

原作者： Jaime Rafael Imperial, Hao Zheng

发布于 2026-05-26

📖 1 分钟阅读☕ 轻松阅读

原作者： Jaime Rafael Imperial, Hao Zheng

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象你是一位总建筑师（即设计规范），已经为新建的一栋复杂房屋绘制了详细的蓝图。你想聘请一位速度极快、极具创造力但偶尔有些天马行空的施工工头（即大型语言模型，或 LLM），让他为这栋房屋编写一份安全规则清单。这些规则需要用一种严格的、技术性的代码语言**SystemVerilog 断言（SVA）**来书写。

问题在于？这位工头非常擅长写出看起来像安全规则且能通过语法检查的句子，但他有时写出的规则实际上毫无意义，或者与你的原始蓝图相矛盾。

例如，你的蓝图规定：“当警报开启时，前门必须上锁。”工头可能会写出一条规则：“当前门开启时，前门必须上锁。”这句话听起来像是一条规则，计算机甚至可能会说：“是的，这是一个有效的句子。”但在现实世界中，这毫无意义。

问题所在：“有效”但错误

传统上，为了检查这些规则是否良好，工程师们会构建房屋的物理模型（称为黄金 RTL），并将规则与该模型进行运行测试。如果规则没有破坏模型，他们便假设该规则是良好的。

但本文认为，这就像仅仅通过观察规则是否适用于某个特定模型来检查其有效性。如果模型是完美的，那当然很好。但如果你还没有模型呢？或者，如果该规则在技术上对那个特定模型是“真”的，却完全偏离了你原本的要求呢？工头可能会幻觉出一些听起来很聪明但实际上毫无用处的规则。

解决方案：SpecAlign

作者们引入了SpecAlign，这是一种全新的“质量控制”框架。SpecAlign 不再通过构建物理模型来测试规则，而是充当一位超级聪明的翻译员和事实核查员，直接将工头编写的规则与你的原始蓝图（自然语言规范）进行比对。

以下是 SpecAlign 的工作原理，使用一个简单的类比：

1. 翻译步骤（规范化）

工头用严格的代码（SVA）编写规则。SpecAlign 首先将这些规则翻译回纯英文。

类比： 想象工头用“建筑代码”书写。SpecAlign 将其翻译回“英语”，以便能直接与你的英文蓝图进行比对。

2. 两步事实核查（对齐循环）

SpecAlign 运行两轮检查：

第一轮（属性检查）： 它检查工头从你的蓝图中提取的想法。这些想法是否与你写的内容相符？
第二轮（规则检查）： 它检查实际翻译后的规则。它们是否与这些想法以及你的蓝图相符？

3. “三盒”裁决

SpecAlign 不再仅仅给出“通过”或“失败”的结论，而是将每条规则归入三个盒子之一：

🟢 蕴含（绿色）： 规则与你的蓝图完美匹配。“是的，这正是你所要求的。”
🔴 矛盾（红色）： 规则直接与你的蓝图冲突。“不，你说警报开启时门应上锁，但这条规则却说应解锁。”
⚪ 未知（灰色）： 规则提到了你的蓝图中从未涉及的内容。“你提到了‘智能锁’，但你的蓝图只说了‘门’。我不知道这个额外功能是否可以接受。”

4. “自我修正”循环

如果一条规则落入**红色（矛盾）**盒子，SpecAlign 不会直接将其丢弃。它会像一位严格的编辑那样行动：

它明确告知工头规则具体错在哪里。
它要求工头根据蓝图重写该规则。
它再次检查新规则。
它重复此过程，直到规则变为绿色，或者至少明确为灰色。

为了确保这位“编辑”不会犯错，SpecAlign 会让 AI 通过三种不同的方式思考该问题（就像咨询三位不同的专家），然后对最终答案进行投票。这被称为自洽性（Self-Consistency）。

结果：清理混乱

作者在两个现实世界的设计上测试了该方法（例如芯片的通信协议，类似于 USB 或网卡如何与计算机通信）。

在 SpecAlign 之前： 一种竞争方法生成了数百条规则。其中大多数要么是红色（与蓝图矛盾），要么是灰色（编造细节）。只有极小部分是绿色（真正符合蓝图）。
在 SpecAlign 之后：
- 红色（矛盾）规则的数量急剧下降。对于其中一个设计，坏规则从 148 条减少到了仅 6 条。
- 绿色（对齐）规则的数量显著增加。
- 灰色（未知）规则的数量增加了。为什么？ 因为 SpecAlign 不再假装那些编造细节的规则是“好的”。它正确地识别出它们为“我们没有足够信息来判断这是否良好”。

核心结论

本文的结论是：仅仅因为一条规则在语法上是正确的，或者通过了计算机测试，并不意味着它的意思就是你以为的那个意思。

SpecAlign 提供了一种方法，可以在无需先构建物理模型的情况下，检查 AI 是否真正听从了你的指令。它将一堆“技术上有效但无用”的规则，转化为一套更小、更干净、你真正可以信赖的规则集，同时清晰地标记出那些因过于模糊而无法确定的规则。

技术摘要：SpecAlign – 用于 SystemVerilog 断言生成的语义对齐框架

1. 问题陈述

现代硬件设计复杂性的日益增加推动了大型语言模型（LLM）在生成 SystemVerilog 断言（SVA）以支持基于断言的验证（ABV）方面的应用。然而，现有的 LLM 方法主要关注语法有效性和形式验证（FV）结果（例如，断言在给定 RTL 上是否被证明或产生反例）。这些指标未能解决语义对齐问题：即生成的断言是否准确反映了自然语言规范中描述的行为意图。

LLM 可能会生成语法正确且在特定 RTL 实现上形式可证明的断言，但在语义上无效或属于幻觉。例如，一个断言可能在触发属性的同一边沿对时钟进行采样，导致其在通过 FV 的同时却是空洞的（vacuous）。在缺乏用于比较的“黄金”RTL 模型的情况下，人工检查此类断言既耗时又降低了可信度。此外，FV 引擎在评估复杂设计的大量生成断言时，面临可扩展性问题（状态空间爆炸）。因此，迫切需要一种能够独立于 RTL 实现细节、直接针对规范本身评估语义一致性的框架。

2. 方法论：SpecAlign 框架

SpecAlign 是一个以规范为中心的框架，旨在无需依赖黄金 RTL 的情况下评估并迭代优化 LLM 生成的 SVA。它通过两个主要的迭代循环运行：属性对齐循环和SVA 对齐循环。这两个循环均利用三个核心阶段：对齐检查、不一致性分析和证据提取。

A. 架构概述

该框架规范化了不同设计意图表示之间的比较。虽然输入包含自然语言属性（ $P$ ）和生成的 SVA（ $A$ ），但框架通过特定的提取过程将每个 SVA 转换为自然语言摘要（ $N$ ）。这种规范化使得属性和断言能够在同一语义层面上，针对设计规范（ $S$ ）进行评估。

B. 核心组件

对齐检查：
- 分类： 框架根据自然语言描述（ $X_i$ $X_{i}$ ）与规范的关系，将其分为三类：
  - 蕴含（Entails）： 所有元素均得到规范的支持。
  - 矛盾（Contradicts）： 至少有一个元素与规范相矛盾。
  - 未知（Unknown）： 元素既未得到支持也未构成矛盾（通常是由于规范中不存在实现特定的假设）。
- 自洽性投票： 为提高可靠性，系统采用思维链（CoT）提示策略。它为给定输入生成 $k$ 条推理路径，并使用多数投票聚合子判决。若出现平局，则应用保守优先级：矛盾 > 未知 > 蕴含。
- 参考选择： 属性循环使用设计规范（ $S$ ）作为参考。SVA 循环使用“对齐属性库”（如果可用）以减少来自分散规范文档的噪声；否则，回退至 $S$ 。
不一致性分析与优化：
- 当判决为矛盾时，系统执行不一致性分析。它识别描述中具体的冲突元素，参考规范中的正确行为，并生成结构化、可操作的反馈（ $F_i$ ）。
- 该反馈指导 LLM 重新生成属性或断言（ $P'_i$ 或 $A'_i$ ），明确定义触发条件，并避免引入规范中不存在的新信号或行为。
- 优化后的输出在对齐循环中重新评估，直到达到固定迭代次数或输出已对齐。
证据提取：
- 对于蕴含案例，系统从规范中提取支持性证据（引用和位置），以促进人工审查并增强信心。
- 对于未知案例，系统分类哪些元素是模糊或未定义的，从而区分真正的矛盾与未明确定义的行为。
量化指标：
- 该框架定义了一个对齐分数（ $a_t$ ），计算为给定迭代中蕴含断言（ $E$ ）与断言总数（ $n$ ）的比率（ $a_t = E/n$ ）。优化过程的目标是最大化该分数。

C. 自然语言摘要提取

一个关键的预处理步骤是将形式化的 SVA 转换为结构化的自然语言摘要。提示 LLM 识别特定的 SVA 组件（触发器、前件、蕴含运算符、后件和禁用条件），并将它们映射为等效的自然语言短语。这确保了形式代码的语义意图在比较过程中得以保留。

3. 主要贡献

本文概述了以下贡献：

语义评估框架： 一种评估 LLM 生成的 SVA 与自然语言规范一致性的新颖方法，无需依赖应用于黄金 RTL 的形式验证。
迭代优化流程： 一个包含对齐检查、不一致性分析和 SVA 摘要提取的结构化框架，旨在集成到现有的基于 LLM 的生成工作流中。
量化对齐指标： 一种基于语义蕴含分类的对齐评分指标，用于衡量规范一致性，为传统 FV 正确性评估提供了一种可扩展的替代方案。
不一致性分析机制： 一种为矛盾属性和断言生成具体、可操作反馈的方法，支持人工审查和自动优化。
实证验证： 实验结果表明，通过语义优化，APB 和 UART 设计中的矛盾断言有所减少。

4. 实验结果

作者在两个硬件设计上评估了 SpecAlign：APB（APB 到 I2C 接口）和UART（UART 到总线接口）。将该框架与AssertionForge进行了比较，后者是一种使用知识图谱并将 RTL 纳入生成的基线方法。

APB 结果：
- 基线（AssertionForge）： 生成了 442 个 SVA，对齐分数为 0.02。仅 8 个为蕴含，148 个为矛盾。
- SpecAlign： 保持了 442 个 SVA，但将对齐分数提升至 0.15。关键在于，矛盾断言的数量降至 0，蕴含断言达到 66 个。其余 376 个被归类为未知。
UART 结果：
- 基线： 生成了 325 个 SVA，对齐分数为 0.06（21 个蕴含，142 个矛盾）。
- SpecAlign： 生成了 319 个 SVA，对齐分数为 0.28。矛盾断言减少至 6，而蕴含断言增加至 92 个。

结果分析：
实验表明，基线方法生成的断言往往要么与规范矛盾，要么严重依赖自然语言规范中未发现的实现特定细节（RTL）。SpecAlign 有效地过滤掉了这些矛盾。SpecAlign 中“未知”分类的增加（例如 APB 的 376 个）并非失败，而是一种更保守和准确的分类策略，它将实现特定的假设与规范支持的行为区分开来。这种区分防止了将不支持的行为错误地标记为“蕴含”。

5. 意义与主张

本文主张 SpecAlign 是传统形式验证的可扩展补充。通过将语义正确性与 RTL 证明结果分离，它解决了仅靠形式验证无法确定断言是否捕捉到规范中描述的预期行为的局限性。

作者强调，虽然形式验证对于证明断言在 RTL 上成立是必要的，但它不足以评估断言意图的质量。SpecAlign 通过以下方式提高了对 LLM 生成断言的信心：

检测形式工具可能遗漏的语义不一致性（例如，空洞真理）。
通过在 RTL 仿真或形式证明之前识别矛盾，减少调试工作。
提供一种机制，无需黄金模型即可迭代优化断言。

本文结论较为谦逊，指出虽然该框架改善了对齐，但未来的工作仍需优化分类方法，更好地捕捉语法错误，并将该方法扩展到其他硬件设计自动化任务，如 RTL 生成和调试。