[Paper] LeGend：用于硬件模型检查中引理生成的数据驱动框架

Source: arXiv - 2602.24010v1

Overview

本文介绍了 LeGend，一个数据驱动的框架，用于加速 IC3/PDR‑基硬件模型检查中的引理生成。LeGend 通过将原本对每个子句进行的图分析，转变为对电路闩锁一次性的全局嵌入，大幅降低推理开销，使现有的验证引擎在实际 RTL 设计上运行得更快。

关键贡献

• Global latch embeddings: 引入一种自监督预训练步骤，为电路中的每个闩锁学习紧凑的向量表示，捕获其结构和功能上下文。
• Lightweight lemma predictor: 使用预先计算的嵌入来训练一个小型神经模型，能够即时为任意归纳反例（CTI）立方体建议高质量的引理。
• Decoupled training/inference: 昂贵的表示学习在每个设计上只执行一次，而在模型检查期间的推理几乎是免费（微秒级）。
• Empirical speed‑up: 在广泛的基准套件上展示了对两款最先进的 IC3/PDR 工具的一致加速，总验证时间最高可降低 2.3 倍。
• Open‑source prototype: 提供参考实现和用于复现实验的脚本，便于验证社区采纳。

方法论

1. 电路预处理: 将 RTL 网表解析为图，其中节点是闩锁（状态元件），边表示组合连接。
2. 自监督预训练: 在整个电路上使用掩码节点预测任务训练图神经网络（GNN）——随机隐藏闩锁的类型或连通性，让模型重建它。这迫使 GNN 学习能够编码全局电路属性的嵌入。
3. 嵌入提取: 训练完成后，每个闩锁获得一个固定大小的向量（例如 128 维），存储以供后续使用。无需进一步的图遍历。
4. 引理生成模型: 一个轻量级前馈网络以出现在 CTI 立方体中的闩锁嵌入为输入，输出每个可能子句（引理）的概率分数。选择得分最高的子句作为广义引理。
5. 与 IC3/PDR 的集成: 预测器取代传统的每子句图分析步骤。当引擎需要对 CTI 进行概括时，只需查找相关嵌入并运行预测器，耗时仅几微秒。

整体流水线将重学习阶段（每个设计一次）与快速推理阶段（每次验证运行多次）分离。

结果与发现

• 推理开销： 引理预测每个 CTI 只增加 < 0.01 s，而之前的图分析方法则超过 > 0.3 s。
• 质量权衡： LeGend 生成的引理平均更通用（文字更少），且不牺牲证明的完整性。
• 可扩展性： 预训练时间随触发器数量线性增长，并在同一设计的多次验证运行中摊销。

Practical Implications

• 更快的验证周期： 团队可以更快速地迭代 RTL 更改，因为模型检查步骤不再是瓶颈。
• 降低计算成本： 更少的 CPU 时间意味着更便宜的云端或本地验证平台，特别对大规模 ASIC 项目价值显著。
• 即插即用的集成： 由于 LeGend 只替换引理生成模块，现有的 IC3/PDR 工具（如 ABC、CoSA）可以在几乎不改动代码的情况下采用它。
• 持续学习的潜力： 预训练的嵌入可以缓存并在同一设计的多次验证运行中重复使用，或在添加新模块时进行微调，从而实现“学习加速”的验证工作流。
• 更广泛的 AI‑for‑EDA 采纳： 证明一次性的全局表示学习步骤能够克服以往机器学习辅助验证技术的可扩展性瓶颈。

局限性与未来工作

• Design‑specific training: 嵌入必须为每个新的 RTL 设计重新训练；当前方法尚不支持跨设计的迁移学习。
• Model size vs. hardware constraints: 虽然推理轻量，但 GNN 预训练仍需要 GPU 或强大的 CPU，这对小团队可能是障碍。
• Clause space exploration: LeGend 为每个 CTI 预测单个引理；将其扩展为提出多个多样化候选可能进一步提升证明搜索。
• Integration with other engines: 未来工作将探索将相同的嵌入策略应用于基于 SAT 的 BMC 或基于插值的模型检查。
• Robustness to aggressive optimizations: 作者指出，经过激进逻辑综合的高度优化网表有时会降低嵌入质量；自适应再训练策略正在研究中。

作者

• Mingkai Miao
• Guangyu Hu
• Wei Zhang
• Hongce Zhang

论文信息

• arXiv ID: 2602.24010v1
• Categories: cs.AR, cs.SE
• Published: 2026年2月27日
• PDF: 下载 PDF