当前位置：首页 > news >正文

基于RTL的双向数据合成训练专用LLM生成硬件断言

news 2026/5/10 1:55:58

1. 项目概述：基于RTL的双向数据合成训练专用LLM生成硬件断言

在数字硬件设计流程中，SystemVerilog断言(SVA)是验证RTL设计是否符合规范的关键工具。传统SVA编写高度依赖验证工程师的专业技能，不仅效率低下，还容易出错。近年来，大语言模型(LLM)在EDA领域的应用为解决这一问题提供了新思路，但通用LLM在NL2SVA任务上表现不佳，主要受限于两个核心问题：

高质量SVA语料稀缺：公开可用的SVA数据主要来自教科书和少量开源仓库，规模有限（如Hybrid-NL2SVA仅含4070条SVA），而RTL代码数据集（如DeepCircuitX）规模可达10^5量级
NL-SVA语义对齐验证困难：现有验证方法（如形式验证工具、LLM自评估）难以准确判断生成的SVA是否真实反映NL属性的语义

针对这些问题，我们提出了QiMeng-CodeV-SVA框架，通过RTL代码引导的LLM双向数据合成方法，实现了高质量NL2SVA数据集的构建和专用模型的训练。实验表明，CodeV-SVA-14B在Func.@1指标上达到75.8%（人工测试集）和84.0%（机器测试集），媲美GPT-5等先进通用LLM，同时部署成本显著降低。

关键创新点：不同于传统方法直接使用通用LLM，我们通过数据合成框架专门优化了LLM在硬件断言生成任务上的表现，使其在保持高精度的同时更适合实际工程部署。

2. 核心方法解析：RTL引导的双向数据合成框架

2.1 数据合成整体流程

我们的数据合成框架包含四个关键阶段，形成完整的数据生产流水线：

基于RTL的SVA合成：从开源RTL代码出发，使用通用LLM生成候选NL属性和SVA对，通过形式验证工具筛选可验证的SVA
双向数据选择：将SVA反向翻译为NL，再重新生成SVA，保留逻辑等价的样本
数据质量精炼：结合LLM自评估、难度过滤和推理增强进一步提升数据质量
监督微调：使用合成数据训练专用CodeV-SVA模型

图：数据合成框架的四个核心阶段，最终产出83K高质量NL-SVA训练样本

2.2 关键技术实现细节

2.2.1 RTL引导的SVA生成

我们从CodeV数据集中筛选42K带有时钟和复位信号的RTL设计作为基础。对每个设计，使用DeepSeek-V3.1执行以下步骤：

属性分析：将RTL规格分解为多个独立验证属性

# 示例：计数器设计的属性分解 def analyze_properties(spec): # 输入：RTL规格说明 # 输出：验证属性列表 properties = [ "当使能信号为高时，计数器每个时钟周期递增1", "当复位信号有效时，计数器值重置为0" ] return properties

SVA生成：为每个属性生成候选SVA

// 生成的计数器验证SVA示例 assert_counter_enable: assert property ( @(posedge clk) disable iff (reset) en |-> (count == $past(count) + 1) );

形式验证筛选：使用JasperGold验证SVA在对应RTL下的可满足性，从324K初始属性中筛选出159K有效SVA

2.2.2 双向数据选择机制

双向翻译是保证NL-SVA语义对齐的核心技术，其工作原理如下：

SVA→NL反向翻译：使用few-shot提示指导LLM生成高级NL描述而非直接信号关系

输入SVA： assert property (@(posedge clk) cmd_valid && !busy |=> busy); 输出NL： "当命令有效且控制器空闲时，下一周期必须进入忙状态"

NL→SVA重新生成：将反向翻译的NL再次转换为SVA，并验证新旧SVA的逻辑等价性

实际案例：图2展示了双向翻译如何发现运算符优先级导致的语义偏差。原始SVA因"and"优先级高于"|->"成为恒真式，通过双向翻译后生成的SVA暴露了这一错误。

2.2.3 数据精炼策略

为提高训练效率，我们采用三级过滤机制：

LLM自评估：基于专家总结的4类错误模式（逻辑错位、信号不一致等）过滤低质量样本
难度过滤：使用能力较弱的Qwen3-8B生成多个SVA，保留至少存在一个差异的样本
推理增强：使用DeepSeek-R1添加推理轨迹，仅保留最终答案正确的样本

3. 模型训练与实验结果

3.1 CodeV-SVA训练配置

我们基于Qwen3-8B/14B进行监督微调，关键参数如下：

参数项	配置值
训练框架	LlamaFactory
学习率	2e-5
批量大小	128
上下文长度	32,768
训练时长(8B)	8小时@8×H800
训练时长(14B)	12小时@8×H800

训练目标函数：

\mathcal{L}_{\text{SFT}}(\theta) = -\sum_{i=1}^N \sum_{j=1}^{M_i} \sum_{t=1}^{T_{ij}} \log P(\tilde{y}_{ij}^{(t)} | \tilde{y}_{ij}^{(<t)}, c_i || x_{ij}^*; \theta)

3.2 基准测试结果

在FVEval-NL2SVA基准上的性能对比（Func.@1指标）：

模型	NL2SVA-Human	NL2SVA-Machine
GPT-5	71.8%	81.8%
DeepSeek-R1-671B	74.6%	81.0%
Qwen3-14B(基础)	61.6%	75.3%
CodeV-SVA-8B	72.0%	83.5%
CodeV-SVA-14B	75.8%	84.0%

关键发现：

CodeV-SVA-14B在两项测试集上均达到SOTA，超越GPT-5和DeepSeek-R1
8B版本相比基础Qwen3-8B提升达39.7%（人工集）和37.4%（机器集）
模型规模与性能非严格正相关，显示数据质量的关键作用

3.3 消融实验分析

通过系统性的消融实验验证各组件贡献：

数据源对比（5K样本训练）：

数据源	NL2SVA-Human(F@1)
合成数据(本方法)	55.4%
DeepCircuitX	22.3%
VERT规则改写	1.9%

数据精炼组件影响：

配置	数据量	F@1
完整框架	83K	72.0%
移除推理增强	89K	63.9%
移除双向选择	159K	51.2%
仅保留形式验证	324K	44.1%

实验表明：

LLM合成的SVA质量显著优于开源收集或规则改写
双向选择带来最大性能增益（+12.3%）
推理增强虽减少数据量但提升模型推理能力

4. 工程实践与应用案例

4.1 端到端验证工作流集成

我们将CodeV-SVA集成到AssertionForge框架中，形成两阶段流程：

Spec2NL：通用LLM分析设计规格生成NL属性
NL2SVA：CodeV-SVA将NL转换为可验证SVA

在OpenMSP430复杂设计（129页规格，29个RTL文件）上的对比：

NL生成模型	SVA生成模型	可验证SVA数
GPT-4o	GPT-4o	106
DeepSeek-R1	DeepSeek-R1	122
DeepSeek-R1	CodeV-SVA-8B	211

CodeV-SVA使可验证断言数量提升73%，显著减少人工验证工作量。

4.2 实际开发中的经验技巧

RTL筛选策略：
- 优先选择包含时钟和复位信号的设计
- 使用Yosys分析信号拓扑，过滤过于简单的模块
```
yosys -p "read_verilog design.v; synth; stat"
```
Prompt设计要点：
- SVA生成时在prompt中包含关键信号列表
- SVA→NL翻译使用few-shot示例引导高级语义描述
形式验证加速：
- 对大型设计采用增量验证策略
- 并行化验证任务以利用多核服务器
模型部署优化：
- 使用vLLM实现高吞吐量推理
- 对14B模型进行GPTQ量化（4bit）后仅需12GB显存