[论文] 基于断言的验证中的自动断言挖掘：技术、挑战与未来方向

Source: arXiv - 2601.02248v1

概述

基于断言的验证（ABV）已成为检查复杂硬件设计的事实标准方法，但手工编写高质量的断言既耗时又容易出错。本文调查了最先进的自动断言挖掘工具，比较了它们的工作方式，并指出了它们的不足之处——为下一代验证工具提供了路线图。

关键贡献

• 现代断言挖掘技术的综合分类（基于模式、机器学习驱动、混合等）。
• 正面对比基准套件，在一组公共 RTL 设计上评估挖掘工具，衡量覆盖率、误报率和运行时间。
• 对优势与劣势的深入分析（例如，可扩展性、语言支持、捕获时序属性的能力）。
• 识别开放挑战，如处理多时钟域、与形式求解器集成以及降低标注开销。
• 未来方向路线图，概述有前景的研究路径（深度学习模型、增量式挖掘、跨设计复用）。

方法论

1. 文献整理 – 作者从会议、期刊和开源仓库中收集了 28 个近期的矿工实现，重点关注在工业或学术界广泛采用的实现。
2. 特征提取 – 将每个矿工拆分为核心组件（前处理、属性推断、后处理），并标注其能力（例如，支持 SystemVerilog、能够推断时序约束）。
3. 基准设计 – 汇编了一套精选的 12 个 RTL 项目（从简单算术核到全尺度 SoC），并提供手工编写的断言作为真实标签集。
4. 评估指标 – 覆盖率（恢复的真实断言比例）、精确度（误报率）、可扩展性（代码行数 vs. 运行时间）和可用性（工具链集成工作量）。
5. 对比分析 – 结果以热图和雷达图可视化，作者还对验证工程师进行定性“痛点”调查，以验证数值。

方法论刻意保持工具无关性，以便开发者使用自己的设计复现研究。

结果与发现

• Hybrid 矿工 始终提供最高的覆盖率，同时将误报率控制在可接受范围内。
• 纯 ML 方法 擅长发现不明显的时序关系，但会产生更高的噪声并且训练时间更长。
• Formal‑guided 矿工 能生成非常干净的断言，但在大规模设计上的可扩展性较差。
• 整体来看，多时钟和异步域 仍是盲点；大多数矿工要么忽略它们，要么生成过于保守的属性。
• 工程师们报告称，集成摩擦（例如，需要自定义脚本将 RTL 输入矿工）比原始性能更是主要阻碍。

实际影响

• 更快的验证周期 – 采用混合矿工可以将手动断言编写工作量减少约 70 %，让团队专注于边缘案例调试。
• 更高的缺陷检测率 – 覆盖率的提升意味着能够捕获细微的协议违规，这些往往会被手工检查遗漏。
• 工具链兼容性 – 论文中的基准套件可以作为即插即用的验证集，适用于任何新矿工，帮助 EDA 供应商认证其产品。
• 多时钟设计的风险缓解 – 所识别的空白提示开发者仍需在这些地方依赖手动断言或补充形式化方法。
• 开源入门套件 – 作者发布了脚本，将常见的 RTL 仓库转换为基准格式，使团队能够快速在自己的 IP 上评估矿工。

局限性与未来工作

• 本研究聚焦于 基于 SystemVerilog 的设计；未评估 VHDL 或混合语言项目。
• 真值断言仅限于少数专家编写的集合，可能导致覆盖率数据产生偏差。
• 运行时测量在单节点工作站上完成，分布式或基于云的挖掘场景尚未探讨。
• 未来研究方向包括：
  • 深度学习模型，能够摄取层次化的设计信息（例如块图），更好地处理多时钟域。
  • 增量式挖掘，在设计演进时更新断言，降低重新运行的成本。
  • 跨设计知识迁移，使在一个 IP 系列上训练的挖掘器能够为另一个系列的断言生成提供启动支持。

通过揭示当前挖掘器的优势与不足，本文为验证工程师提供了选择合适工具的当下依据，并为工具开发者指明了应对未来硬件复杂性所需的突破方向。

作者

• Mohammad Reza Heidari Iman
• Giorgio Di Natale
• Katell Morin-Allory

论文信息

• arXiv ID: 2601.02248v1
• 类别: cs.SE
• 出版日期: 2026年1月5日
• PDF: 下载 PDF