QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis

该论文提出了一种基于 RTL 引导和双向翻译数据合成的框架，以解决硬件断言生成中数据稀缺与语义等价性验证难题，并据此训练出在自然语言转 SystemVerilog 断言任务上表现卓越甚至超越 GPT-5 和 DeepSeek-R1 的专用模型 CodeV-SVA。

要点

这篇论文介绍了一个名为 QiMeng-CodeV-SVA 的新项目，它的核心目标是教人工智能（AI）像经验丰富的硬件工程师一样，自动写出“硬件安全守则”。

为了让你更容易理解，我们可以把整个硬件设计过程想象成建造一座巨大的、复杂的摩天大楼。

1. 背景：为什么要写“安全守则”？

在建造大楼（设计芯片/硬件）时，工程师必须确保大楼不会塌，电梯不会乱跑，火灾时警报会响。在芯片设计里，这些规则叫做 SVA（系统验证断言）。

• SVA 是什么？ 就像是大楼的“安全说明书”。比如：“如果电梯门开着，电梯绝对不能动”或者“如果按下火警按钮，所有灯必须闪烁”。
• 痛点： 以前，这些规则全靠人类工程师手写。这非常累，而且容易出错。一旦漏写一条规则，大楼（芯片）造好后可能就会出大问题，甚至导致数亿美元的损失。

2. 问题：AI 为什么以前学不会？

最近，大家想用通用的 AI（比如 ChatGPT 这类大模型）来自动写这些规则。但是，通用的 AI 就像是一个读过很多书但没干过活的“书呆子”：

• 缺乏实战经验： 它们读过很多书，但没见过真实的“大楼图纸”（RTL 代码），所以写出来的规则要么太简单（像“电梯永远不动”这种废话），要么逻辑混乱。
• 数据太少： 想要教 AI 写规则，需要大量的“真实案例”（高质量的 SVA 数据）。但现实是，这些珍贵的案例就像失传的秘籍，市面上很少，而且很难判断 AI 写出来的规则到底对不对。

3. 解决方案：CodeV-SVA 的“特训营”

为了解决这个问题，作者们设计了一套**“数据合成与特训”的框架，就像给 AI 建了一个超级特训营**。

第一步：找“工地”练手（RTL 接地合成）

• 以前的做法： 在图书馆里找几本旧书（教科书）里的例子，让 AI 模仿。
• CodeV-SVA 的做法： 直接带 AI 去真实的建筑工地（开源的 RTL 代码库）。
  • 他们让 AI 看着真实的“大楼图纸”（RTL 代码），然后问 AI：“你觉得这里需要什么安全规则？”
  • AI 试着写出来，然后交给**“监理工具”**（形式化验证工具，像 JasperGold）检查。如果规则能通过监理的严格测试，就保留下来。
  • 比喻： 这就像让 AI 在真实的工地上实习，而不是只在教室里背理论。

第二步：双向翻译“照镜子”（双向数据合成）

这是论文最精彩的部分，用来解决“怎么判断 AI 写的规则对不对”的问题。

• 问题： 有时候 AI 写的规则虽然通过了监理检查，但它可能写得太简单，或者根本没理解人类的需求（比如人类说“电梯不能动”，AI 写了“电梯永远不动”，虽然逻辑上没错，但没意义）。
• 方法（双向翻译）：
  1. 让 AI 把写好的规则（SVA）翻译回人类语言（自然语言）。
  2. 再让 AI 把翻译回的人类语言，重新翻译成新的规则。
  3. 核心逻辑： 如果新的规则和原来的规则逻辑完全一样，说明 AI 真的理解了意思，没有“传话传丢了”。如果不一样，说明 AI 在瞎编，直接扔掉。
  • 比喻： 就像玩“传声筒”游戏。如果第一个人说的话，经过两个人转述后，意思还完全一样，说明这两个人都听懂了。如果意思变了，说明中间有人没听清，就把这个“传话员”（数据）淘汰掉。

第三步：精英筛选与“思考过程”增强

• 去粗取精： 用更聪明的 AI 当“考官”，把那些太简单、太无聊的规则删掉，只留下有挑战性的。
• 加入“思考链”： 就像教学生做题，不仅给答案，还要让 AI 写出解题思路（Reasoning Trajectory）。这样 AI 在写规则时，会先像工程师一样“思考”一遍，再下笔，准确率更高。

4. 成果：小模型打败大模型

经过这套“特训”，作者训练出了 CodeV-SVA 模型（有 8B 和 14B 两个版本，指参数量大小）。

• 惊人的表现： 这个专门训练的小模型，在写“安全守则”的任务上，打败了像 GPT-5 和 DeepSeek-R1 这样昂贵且巨大的通用 AI 模型。
• 性价比： 它不需要像那些大模型那样消耗巨大的算力和金钱，就能干得更好。
• 实际应用： 在真实的端到端验证流程中（从看图纸到生成规则），CodeV-SVA 生成的有效规则数量是通用 AI 的 2 到 3.5 倍。

总结

这篇论文就像是在说：

“与其让一个博学的‘书呆子’去猜怎么盖大楼，不如让它去真实的工地实习，通过**‘翻译 - 回译’的镜子照出它的真本事，再让它学会‘先思考后行动’。最后，我们得到了一个懂行、靠谱且便宜**的 AI 工程师，能自动帮人类写出完美的硬件安全规则。”

这不仅解决了芯片设计中的痛点，也为如何训练专用 AI 提供了一个非常聪明的新思路。

技术摘要

这篇论文提出了一种名为 QiMeng-CodeV-SVA 的框架，旨在通过基于 RTL（寄存器传输级）代码的双向数据合成方法，训练专门用于硬件断言（SystemVerilog Assertions, SVA）生成的专用大语言模型（LLM）。

以下是对该论文的详细技术总结：

1. 研究背景与问题 (Problem)

• 核心任务：将自然语言（NL）描述的设计规范转换为 SystemVerilog 断言（SVA），即 NL2SVA 任务。这是硬件形式化验证中的关键环节，用于确保 RTL 实现满足设计规范。
• 现有挑战：
  1. 高质量数据稀缺：现有的 SVA 语料库规模极小（主要来自教科书或少量开源仓库），远小于 RTL 代码的规模。通用 LLM 缺乏领域知识，直接用于 NL2SVA 翻译效果不佳。
  2. 语义等价性验证困难：在合成数据时，难以自动判断生成的 SVA 是否真正对应自然语言描述。
     • 仅靠形式化验证工具（如 JasperGold）检查 SVA 在 RTL 下是否通过是不够的，因为 trivial（平凡）或 vacuous（空洞）的断言（如 assert property (1'b1)）也能通过验证，但与 NL 描述不符。
     • 使用 LLM 作为裁判（LLM-as-a-judge）存在歧义，难以识别 SVA 语法中的细微错误（如操作符优先级问题）。

2. 方法论 (Methodology)

作者提出了一套高效的数据合成与模型训练框架，主要包含四个阶段：

阶段一：基于真实世界 RTL 的 SVA 合成 (SVA Synthesis from Real-World RTL)

• 数据源：利用大规模开源 RTL 代码（来自 CodeV 数据集，约 16.5 万行），筛选出包含时钟和复位信号的 4.2 万实例，这些通常涉及时序约束。
• 生成过程：
  1. 使用通用 LLM（DeepSeek-V3.1）分析 RTL 及其规格说明，生成多条自然语言验证属性。
  2. 基于这些 NL 属性和 RTL 代码，让 LLM 生成对应的 SVA。
  3. 初步过滤：使用形式化验证工具（JasperGold）验证生成的 SVA 在对应 RTL 下是否通过，保留通过的 SVA 作为种子数据（约 15.9 万条）。

阶段二：NL-SVA 对的双向选择 (Bidirectional Selection)

这是解决“语义对齐”问题的核心创新：

• 原理：利用双向翻译的一致性来筛选高质量数据。如果 SVA 转回 NL 再转回 SVA，且新 SVA 与原 SVA 逻辑等价，则说明该 NL-SVA 对语义对齐良好。
• 流程：
  1. SVA $\to$ NL：将种子 SVA 翻译为自然语言（使用 Few-shot 提示引导生成高层属性而非信号细节）。
  2. NL $\to$ SVA：将生成的 NL 再次翻译为新的 SVA。
  3. 等价性检查：使用形式化工具检查新 SVA 与原 SVA 是否逻辑等价。
  4. 结果：仅保留通过等价性检查的样本。此步骤将数据量从 15.9 万筛选至 10.5 万，显著提升了数据质量。

阶段三：进一步的数据质量 refinement (Further Data Quality Refinement)

• LLM-as-a-judge + 专家先验：人工分析双向翻译无法识别的错误类型（如逻辑错位、信号不一致等），训练 LLM 过滤此类错误。
• 难度过滤：使用较弱的 LLM（Qwen3-8B）尝试生成 SVA，如果所有尝试都等价于原 SVA，则视为过于简单（trivial）的数据并剔除。
• 推理轨迹增强 (Reasoning Augmentation)：使用强推理模型（DeepSeek-R1）为每个样本生成包含推理过程（Chain-of-Thought）的 SVA 答案，仅保留最终答案正确的样本，将推理轨迹作为训练标签的一部分。

阶段四：监督微调 (Supervised Fine-Tuning)

• 使用合成后的 8.3 万高质量 NL2SVA 数据集，对开源基座模型（Qwen3-8B/14B）进行监督微调（SFT），得到 CodeV-SVA 系列模型。

3. 主要贡献 (Key Contributions)

1. 数据合成框架：提出了一种利用大规模开源 RTL 指导 LLM 生成 SVA，并通过双向翻译 + 形式化等价检查来筛选高质量 NL-SVA 对的方法，解决了 SVA 数据稀缺和语义验证难的问题。
2. 专用模型训练：训练了 CodeV-SVA-8B 和 CodeV-SVA-14B 两个专用模型，证明了在特定硬件领域，通过高质量合成数据微调开源模型，性能可超越甚至匹配昂贵的闭源通用大模型。
3. 开源与基准：计划开源数据集、模型及训练流程，并展示了在 FVEval 基准上的 SOTA 表现。

4. 实验结果 (Results)

在 FVEval-NL2SVA 基准（包含 NL2SVA-Human 和 NL2SVA-Machine 两个子集）上的评估结果：

• 性能表现：
  • CodeV-SVA-14B 在 Func.@1（一次尝试即正确的概率）上取得了 75.8% (Human) 和 84.0% (Machine) 的得分。
  • 超越 SOTA：该性能超越了 DeepSeek-R1 (671B)、GPT-5 等顶级通用大模型，以及专门的 RTL 生成模型。
  • 提升幅度：相比基座模型 Qwen3-14B，CodeV-SVA-14B 在 Human 测试集上提升了约 14.2%，在 Machine 测试集上提升了约 8.7%。
• 消融实验：
  • 双向选择：贡献最大，使 Human 测试集的 Func.@1 提升了 12.3%。
  • 推理增强：显著提升了模型性能，证明了推理轨迹的重要性。
  • 数据质量：使用合成数据训练的模型性能远优于直接使用开源仓库中收集的 SVA 数据训练的模型。
• 端到端验证：在 AssertionForge 框架的端到端测试中，CodeV-SVA-8B 在复杂设计（如 OPENMSP430）上生成的可验证 SVA 数量是 GPT-4o 的 2.5 倍，DeepSeek-R1 的 3.5 倍。

5. 意义与影响 (Significance)

• 解决数据瓶颈：证明了利用 RTL 代码作为“设计待测对象（DUT）”来合成 SVA 数据是可行的，且能保持数据的多样性和真实性，打破了高质量 SVA 数据稀缺的瓶颈。
• 低成本高性能：展示了通过精心设计的合成数据 pipeline，中小参数量的开源模型（14B）可以在特定垂直领域（硬件验证）超越参数量大得多的通用闭源模型，降低了硬件公司的部署成本。
• 验证流程自动化：为自动化硬件形式化验证提供了强有力的工具，能够显著减少人工编写断言的工作量，提高芯片设计的验证覆盖率。

总结：QiMeng-CodeV-SVA 通过“RTL 引导生成 + 双向语义校验 + 推理增强”的创新 pipeline，成功构建了高质量的硬件断言数据集，并训练出了目前最强的开源 SVA 生成模型，为 EDA 领域的 AI 应用树立了新的标杆。