LLM生成的SystemVerilog断言对语义保持RTL变换的鲁棒性

# LLM生成的SystemVerilog断言对语义保持RTL转换的鲁棒性
来源：https://arxiv.org/html/2609.05658
###### 摘要

大型语言模型（LLM）正越来越多地被探索用于自动化SystemVerilog断言（SVA）生成，但大多数评估仅针对输入的单一语法表示报告正确性。这种点准确率无法揭示当相同RTL行为以不同方式书写时，模型的正确输出是否稳定。本文提出了一种受控的变元测试评估框架，用于衡量基于LLM的SVA生成在语义保持的RTL转换下的表现。我们从VERT数据集出发，构建了一个质量过滤的条件控制库和一个分层的40程序评估集，包含295个赋值行为。我们使用相同的评估提示和贪心解码，评估了两个开源代码模型：Qwen2.5-Coder-7B和DeepSeek-Coder-V2-Lite。研究了三种转换：操作数重排、确定性标识符重命名和冗余括号化。除了基线准确率和转换后准确率，我们还测量了条件鲁棒性、不变性失败率和任何翻转率，并使用了RTL程序层级的10,000样本聚类自举区间。在所有六种模型-转换条件中，9.7%–27.0%在原始RTL上正确的行为，在语义保持的转换后变得不正确。因此，聚合准确率可能掩盖了相当大的不稳定性：在标识符重命名下，DeepSeek-Coder-V2-Lite的准确率从53.9%提升至63.7%，但同时有19.5%原本正确的行为失败。对30个采样的正确转错误案例的手动审查，识别出了路径谓词丢失、分支极性错误、布尔结构损坏和输出契约违反等问题。结果表明，仅凭点准确率不足以表征LLM在断言生成中的可靠性，并为AI辅助的硬件验证中需要基于鲁棒性的评估提供了动力。

关键词：SystemVerilog断言，硬件验证，大型语言模型，变元测试，鲁棒性，RTL。

## 1引言

基于断言的验证（ABV）是一种广泛使用的机制，用于将设计意图表达为可执行属性。在SystemVerilog中，断言用于仿真和形式验证，以检查寄存器传输级（RTL）设计是否遵守时序和逻辑要求。难点不仅在于编写语法有效的SVA。一个有用的断言必须为所检查的行为编码正确的控制流前提条件、时序关系和结果。

最近的工作越来越多地将机器学习和LLM应用于此任务。早期系统使用规则和学习模型的组合将自然语言需求翻译成断言[1 (https://arxiv.org/html/2609.05658#bib.bib1), 2 (https://arxiv.org/html/2609.05658#bib.bib2)]。后续的LLM方法针对安全断言、完整设计规范、结构化规范/RTL表示和领域特定数据集[3 (https://arxiv.org/html/2609.05658#bib.bib3), 4 (https://arxiv.org/html/2609.05658#bib.bib4), 5 (https://arxiv.org/html/2609.05658#bib.bib6), 6 (https://arxiv.org/html/2609.05658#bib.bib5)]。这些系统表明LLM可以产生有用的硬件验证工件，但主流的评估模式仍然是*点正确性*：模型接收输入的一种表示，生成的断言被判断为正确或不正确。

点正确性没有回答第二个实际重要的问题：*在语义保持的输入重写下，正确的生成是否稳定？*考虑一个条件如
`if(a&&b&&c) begin x=y; end`
将同质的合取重排为`c && b && a`不会改变布尔条件。同样，一致地重命名标识符或添加冗余括号不应改变SVA必须捕获的路径条件。如果模型在此类重写后将正确断言变为不正确，则原始的成功对表示敏感。

这种区分在硬件验证中很重要。RTL经常被工具和工程师重新格式化、重构、生成、重命名或规范化。两个源片段可能表示相同的设计行为，但在词元级别上有显著差异。仅在一种表面形式上成功的验证助手，在基准测试中可能显得准确，但在部署中仍然脆弱。

变元测试为这个问题提供了一个自然的视角。它不仅询问单个输出是否正确，而是检查相关输入之间输出的必要关系[7 (https://arxiv.org/html/2609.05658#bib.bib8)]。对于语义保持的RTL转换，所需的关系很简单：生成的断言行为应保持语义正确。近期文献已将变元测试应用于深度代码模型，使用标识符更改和结构重写等转换[8 (https://arxiv.org/html/2609.05658#bib.bib9)]，但这种鲁棒性视角在基于LLM的SVA生成中受到的关注很少。

因此，本文研究以下问题：*LLM生成的SVA正确性在多大程度上对语义保持的RTL表示是不变的？*我们使用两个开源代码模型、相同的评估提示、确定性解码、三种输入转换、行为级语义评分器和聚类自举统计，对VERT[6 (https://arxiv.org/html/2609.05658#bib.bib5)]的分层子集进行了受控实验。

贡献在于：
- •一个用于衡量RTL到SVA生成中表示敏感性的变元评估框架；
- •三种受控的语义保持RTL转换，涵盖操作数顺序、标识符名称和冗余括号化；
- •区分聚合准确率与保留正确性、正确转错误失败和总预测翻转的鲁棒性指标；
- •一项实证研究，显示在六种模型-转换条件下存在9.7%–27.0%的不变性失败，包括聚合准确率提高而先前正确行为退化的情况。

核心主张是刻意狭隘的。我们并未推断模型“不理解”RTL语义，也未尝试识别特定故障的原因。我们表明，在本文研究的受控集合上，SVA正确性对源级表示（这些表示保留了预期的布尔行为）存在实质性的敏感性。

## 2背景与相关工作

### 2.1 SVA生成

对于此处考虑的条件控制模式，断言生成需要重构赋值执行所依据的路径条件。例如：
`if(a) begin x=y; end else if(b) begin x=z; end`
第二个赋值不仅仅由`b`保护，而是由`!a && b`保护。省略对先前分支取反的模型会为该赋值行为产生逻辑上较弱、因此不正确的断言。

Aditi和Hsiao使用混合的基于规则和机器学习技术探索了自然语言到SVA的生成[1 (https://arxiv.org/html/2609.05658#bib.bib1)]，后来又开发了一个可验证的生成流程[2 (https://arxiv.org/html/2609.05658#bib.bib2)]。Kande等人评估了LLM用于安全重点的硬件断言生成，并构建了一个大型自动评估框架[3 (https://arxiv.org/html/2609.05658#bib.bib3)]。AssertLLM使用多个LLM驱动的阶段处理完整设计规范[4 (https://arxiv.org/html/2609.05658#bib.bib4)]。最近的工作整合了RTL结构、知识图谱、渐进式正则化或更丰富的评估信号[5 (https://arxiv.org/html/2609.05658#bib.bib6), 9 (https://arxiv.org/html/2609.05658#bib.bib7)]。

VERT通过提供大型开源的RTL/SVA对数据集并评估微调的开源模型，直接针对SystemVerilog断言生成[6 (https://arxiv.org/html/2609.05658#bib.bib5)]。VERT对本研究特别有用，因为它包含多样化的条件结构、同步和异步变体以及显式的断言引用。我们的工作并非提出另一种生成架构或微调方法。相反，它使用VERT作为鲁棒性研究的基础：给定一个在原始RTL上产生特定正确率水平的模型，该正确率有多少能在语义保持的输入重写下存活？

更广泛的EDA文献越来越多地将LLM视为代码生成、验证、调试和知识检索的工具[10 (https://arxiv.org/html/2609.05658#bib.bib12)]。这种广度使得可靠性评估日益重要：模型输出可能在语法上合理且在基准测试中正确，但在无害的表示变化下仍然不稳定。

### 2.2变元测试与代码模型鲁棒性

变元测试的引入是为了解决难以直接判断单个输出的情况，转而检查多次执行之间的必要关系[7 (https://arxiv.org/html/2609.05658#bib.bib8)]。此后该技术已被应用于许多软件和机器学习领域。在源代码的上下文中，语义保持的转换尤其有吸引力，因为它们允许在保留程序行为的同时进行受控扰动。

最近一篇关于深度代码模型变元测试的系统综述，将变量重命名和其他语义保持的代码转换确定为评估鲁棒性的常见机制[8 (https://arxiv.org/html/2609.05658#bib.bib9)]。这种直觉很自然地带入到硬件描述语言中：标识符名称、冗余的分组语法以及可交换布尔操作数的顺序可以改变词元序列而不改变预期行为。

本研究与标准的代码生成变元测试在两方面有所不同。首先，生成的对象是一种形式属性，其前件与RTL控制流具有明确的逻辑关系。其次，正确性可以在赋值行为级别进行分解，使我们能够区分聚合收益和已经正确行为的损失。这使得正确转错误的过渡成为一个首等指标，而不仅仅是头条准确率的变化。

## 3研究设计

### 3.1研究问题

我们围绕三个研究问题组织研究：

RQ1：聚合准确率。在语义保持的RTL转换下，整体SVA行为级准确率如何变化？
RQ2：不变性。在原始RTL上正确的行为中，转换后仍保持正确的比例是多少？
RQ3：故障模式。在采样的正确转错误过渡中出现了哪些定性错误？

图1 (https://arxiv.org/html/2609.05658#S3.F1)总结了受控流程。

数据集和评估集20,000 VERT记录10,400条件候选9,157合格记录40个受控RTL程序语义保持转换T1: 操作数重排T2: 标识符重命名T3: 冗余括号受控生成Qwen2.5-Coder-7BDeepSeek-Coder-V2-Lite相同提示；贪心解码评分与分析行为级语义评分准确率，CR，IF，翻转聚类自举置信区间

图1：受控的变元评估。VERT记录在构建分层的40程序评估集之前，经过过滤以支持条件控制片段。然后，每个适用的原始/转换对都使用相同的模型、提示和生成设置进行处理。转换改变了源表示，同时保留了预期的布尔行为。

### 3.2数据集预处理与质量过滤

我们使用公开发布的VERT数据集[6 (https://arxiv.org/html/2609.05658#bib.bib5)]，在本研究审计的版本中包含20,000条RTL/SVA记录，均匀分为10,000个同步示例和10,000个异步示例。每条记录提供一个RTL代码片段、一个或多个参考断言、一个同步/异步指示符，以及适用时的时钟信息。

我们重点关注由嵌套if语句和多分支if/else树表示的条件控制结构，因为这些程序揭示了此处研究的推理问题：重构赋值执行所依据的完整布尔路径条件。对case风格族的探索性审计显示，频繁依赖于X/Z通配符语义，同时存在基准质量问题，如属性语法错误、缺少分号和括号不平衡。因此，这些族超出了本研究受控布尔范围的边界，不被视为经过质量过滤的条件库的一部分。

将VERT限制为嵌套if和if/else树族产生10,400个条件控制候选。在此库中，我们应用质量过滤器，移除具有重复属性名称和/或意外属性数量的记录，因为任何一种情况都会妨碍评估器所要求的赋值行为的一对一可靠分解。这排除了1,243条记录，剩下9,157个合格示例，占条件控制候选库的88.05%。

过滤程序的目的是为参考行为、转换和语义评分器能够一致应用定义一个受控片段。这不应被解释为超出此片段的记录总体上不适合SVA生成的主张。

### 3.3受控评估集

9,157条合格记录构成*源库*；并非所有记录都在受控实验中进行评估。为了在保持推断成本可控的同时减少重复或近乎相同模板的主导性，我们使用唯一的标准化结构模板构建了一个40程序评估集。该集合在四个组之间均匀分层：嵌套if异步、嵌套if同步、if/else树异步和if/else树同步。每个层贡献10个程序。

在这40个RTL程序中，参考断言分解为295个独立的赋值行为。T1适用于38个程序和280个行为，因为两个程序不包含可重新排列的合格同质顶层合取或析取。T2和T3适用于所有40个程序和所有295个行为。表1 (https://arxiv.org/html/2609.05658#S3.T1)总结了完整的预处理和抽样过程。

表1：数据集构建和实验范围。阶段计数原始VERT记录20,000同步/异步10,000 / 10,000条件控制候选10,400质量过滤排除1,243质量过滤后合格库9,157受控RTL程序40赋值行为（T2/T3）295T1适用程序38T1赋值行为280生成的评估集是有意为之的受控样本，而非对所有VERT记录的总体估计。因此，统计重采样将RTL程序/对作为实验单元，而非将数百个赋值行为视为独立观测。

### 3.4语义保持转换

表2 (https://arxiv.org/html/2609.05658#S3.T2)定义了三种转换。

表2：受控RTL转换。示例是示意性的；实现会转换完整的RTL条件，同时保留其预期的布尔含义。

#### T1：操作数重排

我们反转安全、同质的顶层逻辑合取或析取的操作数。此转换不更改运算符，也不引入分配重写。受限于