体系结构论文（112）：AssertLLM: Generating Hardware Verification Assertions fromDesign Specifications via Mu

AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs

1. 这篇文章想解决什么问题
传统 ABV 很依赖验证工程师手写 SVA，但这件事很耗时，而且容易漏、容易写错。已有方法大致分两类：
一类是从仿真轨迹里“挖” assertion，但这种方式依赖 RTL，本身可能把设计里的错误也“学进去”；
另一类是从自然语言规格生成 assertion，但通常只处理人工挑出来的句子，难以直接应对真实、完整、非结构化的 specification。并且以前几乎没有方法去利用规格书里的waveform diagrams。作者把现有瓶颈总结为三点：规格书自然语言不结构化、从文本到 SVA 本身很难、波形图里的行为信息没有被利用。

2. 它的核心思路是什么
作者提出了一个多 LLM 协同的流水线，把“从规格书到 assertion”拆成三个子任务：
一是从自然语言规格中抽取结构化的信号信息；
二是从 waveform 图中抽取行为描述；
三是根据前两步得到的信息生成 SVA。
论文中的图 1 就是在展示这个工作流：左边输入完整 SPEC 文件，中间是三个 LLM 分工协作，右边再把生成的断言送进 model checker 做验证。

一. Introduction

1）为什么 assertion generation 很难

引言先把整个验证流程交代清楚了：

• 架构师先用自然语言写 specification
• 设计工程师根据 specification 写 RTL
• 验证工程师再检查 RTL 是否符合 specification
• 其中 ABV 是很常见的一种方式
• 而 assertion 通常写成SVA的形式

难点就在于：
高质量 assertion 的生成本身就是个瓶颈。
人工写 SVA 成本高、耗时长，而且容易漏掉或写错。

现有方法

作者把已有自动生成 SVA 的工作分成两类：

1）动态方法：从仿真轨迹里挖断言

这种方法利用 simulation traces，再结合一些静态约束分析去挖 assertion。
但问题是：它依赖 RTL。
如果 RTL 本身就有 bug，那么你从它身上“学”出来的 assertion 也可能是错的。

2）静态方法：从 specification 出发生成断言

静态方法一般基于：

• predefined templates
• 或 NLP / ML 技术

最近也开始有工作尝试用 LLM 来做 assertion generation。

这个表是全文很关键的一张综述表，它是在对比现有方法和作者方法的差异。表题已经直接点明：
AssertLLM 是第一个能处理 full-size specification files，并且能为每个 architectural signal 生成更全面类型 SVA 的方法。

可以这样理解：

1）RTL stage 方法

这类方法通常在RTL 阶段工作，也就是输入里不只是规格文本，还会用到 RTL。
优点是能结合代码；
缺点是如果 RTL 还不可靠，那么生成的 assertion 也可能被污染。
而且其中有些工作更偏security assertion，有些虽然做 functional assertion，但常常只靠少量例子。

2）Pre-RTL stage 方法

这类方法更接近作者关心的场景：
在 RTL 还没写出来，或者不依赖 RTL 的情况下，只从 specification 生成 assertion。
但此前这些方法大都只处理：

• specification 里的句子级文本
• 而且往往需要人工先筛句子
• 评估时也常依赖 design-specific checkers 或 artificial cases，泛化性有限。

3）作者方法的不同点

作者的方法有三个明显优势：

• 自动处理完整文档，不需要工程师先人工抽句子
• 处理 full design spec，而不只是零碎句子
• 面向的是general designs，不是某个特定设计类型的 checker 环境

三个挑战

这部分很重要，因为它基本定义了整篇文章的问题意识。

挑战一：自然语言规格书是非结构化的

VLSI specification 往往是面向人写的，自然语言很多、组织松散，不能直接拿来生成 assertion。

挑战二：即使结构化了，文本到断言的映射也很难

从 specification 到 assertion 不是简单翻译，而是要同时理解：

• 设计功能逻辑
• SVA 的写法和语义
  所以这个任务本身就很复杂。

挑战三：波形图里的行为信息过去几乎没被用起来

规格书里经常会有 waveform，但此前没有工作专门去从这些图里捕捉行为，再生成相应的 SVA。
这就是作者认为的一个“空白点”。

核心思路

作者的核心策略不是“一个大模型端到端全做完”，而是把任务拆解。

三步流程

第一步：处理自然语言 specification

用一个 LLM 把 specification 中无结构的自然语言，按照统一模板转成结构化信息。

第二步：处理 waveform diagrams

再用另一个 LLM 去分析波形图。
这里有两个关键点：

• 它会先自动生成描述波形行为的自然语言模板
• 再据此抽取 waveform descriptions

作者特别强调：不像以前一些模板方法需要人工先写模板，AssertLLM 不需要额外人工输入模板。

第三步：生成 SVA

最后再用定制化 LLM，把前两步提取出来的信息翻译成 SVA。
生成出的断言可以覆盖不同类型检查：

• bit-width
• connectivity
• functionality

二、方法

这张图是全文最核心的总览图，你可以把它理解成一个generation + evaluation的流水线。

1）输入是什么

最左边输入的是SPEC files，里面可能包含：

• function description
• microarchitecture
• IO definition
• architecture register
• interconnection
• operation
• waveform diagram

也就是说，输入不是单一文本，而是一整份多模态规格文档。

2）中间怎么处理

中间有三个 LLM：

• LLM 1 – Natural Language Analyzer
  负责从自然语言规格中抽取结构化信息
• LLM 2 – Waveform Analyzer
  负责从 waveform 图中提取行为描述
• LLM 3 – SVA Generator
  根据前两步得到的 descriptions 生成 SVA

其中前两个模块的输出都是Description 1 / 2 / ... / n，可以理解为：
它们先把规格书转换成“适合断言生成的中间表示”，再交给最后一个模型。
这说明作者并不是端到端直接生成，而是采用了分阶段、显式中间表示的方案。

3）最后怎么评估

生成出来的 SVAs 会和golden RTL design一起送到model checker里，最终评估三个指标：

• SVA Syntax
• FPV Pass/Fail
• COI Coverage

2.1 Workflow Overview

这部分其实就是对 Figure 1 的文字说明。

核心三步

作者明确说了三个任务：

第一步

从 specification 的自然语言中提取与 SVA 生成有关的信息。

第二步

从 waveform diagrams 中提取行为描述。

第三步

根据前两步抽取的信息，生成高质量 SVA。

这部分最值得注意的点

作者其实在强调一个思想：
SVA generation 不是简单的文本生成任务，而是一个复杂信息抽取 + 形式化翻译任务。
所以必须先把输入分解处理，再做最终生成。

2.2 Natural Language Analyzer

1）为什么需要这个模块

作者先说，一份完整的 natural language specification 通常包含很多部分，比如：

• introduction
• IO ports
• registers
• operation
• architecture
• usage examples
• waveform diagram

问题在于：
关于某一个 signal 的信息，往往分散在不同章节里。
比如位宽在 IO ports 里，功能在 operation 里，连接关系在 architecture 里。
所以不能直接从原始文档一步生成 assertion。

2）它怎么做

作者让 LLM 直接读完整 specification file，然后针对每个 signal抽取相关信息。
为此他们设计了一个统一模板，要求模型输出三大部分：

• Name：信号名
• Description：关于信号的说明
• Interconnection Signals：与该信号相关的其他信号列表

3）Description 又分成什么

为了更适合后续 SVA 生成，Description 被进一步拆成四类：

• definition：位宽、信号类型等基本属性
• functionality：该 signal 的功能语义
• interconnection relationship：它与其他信号的关系
• additional information：其他补充信息

Figure 2 展示的是一个具体 prompt/response 样例。
它让模型对Control Register (CTR)提取信息，最后整理出：

• signal name：CTR
• definition：8 bit、register、RW
• functionality：比如 bit7 控制 core enable，bit6 控制 interrupt enable
• interconnection：它和 EN、IEN 等信号相关
• additional info：reset value 是 0x00

这说明这个模块的本质是：
把原始 specification 里的分散描述，整理为按 signal 组织的结构化知识卡片。

这一模块解决的是前面说的第一个挑战：
自然语言 specification 太散、太乱、太不结构化。
只有先做 signal-level 信息归纳，后面的 assertion generation 才可能稳定。

2.3 Waveform Analyzer

这一节讲第二个 LLM，也是这篇文章比较新颖的部分。

1）为什么波形图难处理

作者指出，规格书中的 waveform 通常是图片，不是结构化的数值波形。
和 VCD 这种现成结构化波形不同，图片里的波形需要先“看懂”，再转成行为描述。

OCR 虽然可以读文字，但很难适应各种波形风格；
通用多模态 LLM 虽然能看图，但普通图像 captioning 并不适合做时序行为理解。
所以他们专门设计了Waveform Analyzer。

2）它的两步法是什么

Waveform Analyzer 分两步：

第一步：Template Generation

先自动生成一组波形行为描述模板。
比如：

• If<signal>is high, then<variable>must be low in the next cycle
• When<condition>occurs,<variable1>should equal<variable2>
• <variable>should remain stable for<number>cycles after<event>

这些模板本质上是“时序行为句型”。

第二步：Description Generation

再把这些模板和实际 waveform 图一起喂给模型，让它生成具体行为描述。
例如论文举的例子包括：

• 当byte_controller.dcnt == 3'b000时，cnt_done拉高
• ien拉高后，下一拍irq_flag有效
• wb_inta_o在特定条件下被置高或拉低

这些描述最后会交给第三个 LLM 变成 SVA。

3）Figure 3 和 Figure 4 分别展示什么

• Figure 3展示模板生成
• Figure 4展示根据模板和波形图生成具体行为描述

这两张图的意思是：
作者不是让模型直接“看图写断言”，而是先抽象出模板，再套模板做行为归纳，这样更稳定，也更接近工程化流程。

这个模块最有价值的地方在于：
它第一次把specification 里的 waveform 图系统性纳入 assertion generation 流程。
也就是说，它不再只依赖文字规格，而是开始利用时序图中的行为信息。

2.4 Automatic Assertion Generation

这是第三个 LLM，即真正负责生成 SVA 的模块。

1）为什么还要专门做这一层

作者先回顾说，传统 NLP 方法不够灵活，LLM 直接从 RTL 或描述生成 assertion 又容易不可靠。
尤其是 SVA 是形式化语言，语法和语义要求都比较严格，普通 LLM 容易生成：

• 语法不合法的 assertion
• 看起来像 assertion 但语义不对的 assertion

2）它怎么增强 LLM

作者引入了RAG（Retrieval-Augmented Generation）。
也就是在生成 SVA 时，不只是靠大模型记忆，而是让它可以检索 SVA 和 FPV 相关教材、教程中的知识。
这样做的目的是增强模型对 SVA 语法和 formal verification 规则的掌握。

3）输入有哪些

这个 SVA Generator 的输入包括：

• 设计整体 architecture diagram
• 前两个 LLM 输出的结构化描述
• 每个 signal 的相关 specification 信息

4）生成哪几类 assertion

作者把生成的 SVA 分成三类：

width

检查 bit width 是否符合 specification。
例如$bits(ctr) == 8。

connectivity

检查信号能否正确驱动，以及值是否正确传播到相关信号。
例如ctr[7]改变后，core_en在下一拍应与之对应。

function

检查 specification 里定义的功能行为是否实现正确。
例如 reset 后寄存器是否清零，某个控制位使能后功能是否被激活。

Figure 5 给出了针对CTR的 SVA 生成例子。你可以这么理解：

• width assertion：检查ctr是否是 8 位
• connectivity assertion：检查ctr[7]是否正确控制core_en，ctr[6]是否正确控制ien
• function assertion：检查 reset 行为、传播行为、波形图里描述的时序功能行为

这说明作者不是只生成一种简单 property，而是尝试构建一个比较完整的断言集合。

2.5 Evaluation of Generated Assertions

这一节讲评估方法。

1）为什么不用特定 checker

作者说，以前有些工作会用专门针对某类设计的 checker 去判断 assertion 好不好，但那样泛化性太差。
因为协议类、处理器类设计可以有专门 checker，但一般 VLSI 设计未必有。

2）他们的评估思路

他们假设有golden RTL implementation，而且这个 RTL 已经经过充分测试，可以看作 bug-free 参考实现。
然后把：

• 生成的 SVAs
• golden RTL一起送进 model checker 做FPV（Formal Property Verification）。

3）三个评估指标是什么

SVA Syntax

看生成的断言有没有语法错误。

FPV Pass/Fail

如果 golden RTL 无 bug，那么：

• assertion 能通过 FPV，说明它在语义上大概率正确
• assertion 失败，则说明这条 assertion 可能有问题

COI Coverage

Cone of Influence coverage，衡量这些 assertion 在结构上连接并覆盖了多少设计逻辑。
这个指标反映的不只是“对不对”，还反映“有不有用、覆盖广不广”。

三、实验

1）输入和工具

作者说明他们的实验输入包括三类东西：

• 原始 specification documents：PDF 格式，里面有文本、表格、图片等多模态内容
• signal definition files：Verilog 格式
• golden RTL designs：也是 Verilog 格式

评估生成的 SVA 时，用的是Cadence JasperGold，具体是其中的FPV app。这说明作者不是做语言层面评估，而是直接放到正式的形式验证工具里检验。

2）比较了哪些模型

实验比较了三类模型：

• GPT-3.5 Turbo
• GPT-4o
• AssertLLM：本质上是加入了 RAG 和定制 instruction 的 GPT-4o 版本，专门面向 SVA generation 任务做了增强。

3.2 Evaluation Metrics

这一节定义了实验指标。

1）单个 signal 上看什么

对每个 signal 的每类 assertion，作者统计：

• 生成了多少条 SVA
• 多少条syntax correct
• 多少条FPV passed
• 所有通过 FPV 的 SVA 的COI coverage

2）什么叫“pass”

作者给了一个很关键的定义：
如果 JasperGold 在5 小时内找不到 counterexample，这条 assertion 就算passed。

3）还有一个细节

论文强调：
所有 SVAs 都是由 LLM 直接生成的，没有后期人工修改。
这意味着实验结果更能反映模型本身的能力，而不是“人机协同修正后的结果”。

4）整体上怎么统计

每个 signal 验证完以后，再汇总到design level，计算：

• 语法正确比例
• FPV 通过比例
• 所有 passed SVA 的 COI coverage

3.3 Assertion Generation Quality

这部分是最核心的实验结果。

1）I2C 设计的规格是什么样

I2C 这个设计的 specification 文档分成六个主要部分，和前文 2.2 节讲的一致。
同时作者还提供了 signal definition file，其中包含：

• IO ports
• architecture registers
• 以及 RTL 实现里定义的内部 wires 和 registers

2）I2C 里有多少 signals

I2C 规格中一共定义了23 个 signals，包括：

• 17 个 IO ports
• 6 个 architecture-level registers

其中 IO ports 又被分成：

• clock
• reset
• control
• data

architecture-level registers 也按功能分成：

• control
• data

3）waveform 的作用

这个 I2C 规格里还有2 个 waveform diagrams，描述了5 个不同 signal的行为。
AssertLLM 会把这些行为提取出来，再为这些 signals 生成 SVA。

这张表是最重要的一张实验表。

1）AssertLLM 一共生成了多少条

在 I2C 上，AssertLLM 总共生成了65 条 properties，其中：

• 23 条 width
• 14 条 connectivity
• 28 条 function

2）最终有效的有多少

这 65 条里：

• 65 条语法都正确
• 56 条 FPV 通过

也就是86%的生成断言同时满足：

• 语法正确
• 功能正确（通过 FPV）

3）哪类断言最好

width 最稳

所有 bit-width checking 的 SVA 全都表现正确。
这说明只要 specification 里位宽信息明确，这类断言比较容易生成。

connectivity 和 function 会出错

有一小部分 connectivity 和 function assertions 出错。
作者分析错误来源有两类：

• 从自然语言生成的 assertion：错误主要来自
  • specification 误解
  • 语言模型 hallucination
• 从 waveform 生成的 assertion：错误主要来自
  • 模型无法推断出波形图中没有显式画出来的行为
  • 因而生成了不完整的 assertion，导致 FPV 不通过

4）和 GPT-4o 对比怎么样

GPT-4o 在 I2C 上一共生成了75 条 assertions，但只有8 条 FPV passed，整体有效率只有11%。
也就是说，它虽然“写了很多”，但真正可用的很少。

5）GPT-4o 为什么这么差

作者给了两个原因：

原因一：没有结构化 signal extraction

在自然语言规格上，GPT-4o 缺乏把 specification 转成 structured signal spec 的机制，因此几乎没法为 I/O ports 生成正确 assertion。
它基本只能成功生成少量 reset check assertions。

原因二：没有专门的 waveform analysis

面对 waveform diagrams 时，因为没有专门的 waveform behavior extraction 方法，GPT-4o 生成的 assertions 更少，而且 FPV pass rate 更低。

6）GPT-3.5 为什么不行

GPT-3.5 因为没有多模态处理能力，不能直接处理原始多模态 specification files。
所以这篇文章里，它在这个任务上基本不成立。

这张图展示的是不同 signal-type 的 COI coverage。

1）整体 coverage 很高

AssertLLM 在 I2C 上的总COI coverage 是 93.44%。
注意作者特别说明：
不同类型断言覆盖的逻辑区域可能不同，所以总体 coverage 会高于单类断言的 coverage。

2）为什么 register 相关断言覆盖更高

作者观察到：
针对registers生成的 assertions，COI coverage 普遍高于 IO signals。
原因很自然：
register 通常连接到更多内部逻辑，因此它的断言更容易覆盖到更大的 cone of influence。

3）和 GPT-4o 比

GPT-4o 在 I2C 上的 COI coverage 只有82.05%。
根本原因不是它覆盖机制差，而是它没有生成足够多、足够正确的 assertions。

3.4 Assertion Generation for More Designs：扩展到更多设计后怎样

作者为了验证方法的泛化性，又在两个设计上做了实验：

• ECG：做椭圆曲线群中两个元素加法
• Pairing：实现 Tate bilinear pairing in elliptic curve group

I2C

• AssertLLM：65/65/56，coverage 93%
• GPT-4o：75/27/8，coverage 82%

ECG

• AssertLLM：22/22/20，coverage 99%
• GPT-4o：11/7/0，coverage 0%

Pairing

• AssertLLM：15/15/14，coverage 100%
• GPT-4o：12/8/1，coverage 0%

平均结果

• AssertLLM：平均100% syntax correct / 90% FPV passed，平均97% coverage
• GPT-4o：平均56% syntax correct / 6% FPV passed，平均27% coverage

3.5 Discussion

这一节很有意思，它是在反思“是不是模型强就一定行”。

作者的核心观点

高质量 assertion generation 不仅依赖 LLM 能力，也非常依赖 specification document 本身的质量。

1）如果规格书只写得很粗

如果 specification 只给：

• signal 名字
• 一两句简单描述

却不写清楚：

• functionality
• connectivity

那么无论 LLM 多强，也很难生成有意义的 SVA。

2）如果规格书写得很完整

如果 specification 对信号功能和互连关系描述得很明确，那么即使 LLM 比较简单，也更容易生成高质量 assertion。

3）I2C 和 ECG/Pairing 的差异说明了这一点

作者指出：

• I2C的 specification 对 registers 和 functionality 写得更详细，所以能生成更多 SVA
• ECG和Pairing的 specification 没那么细，因此 AssertLLM 和 GPT-4o 都只能生成较少的 assertions，只不过 AssertLLM 质量更高一些