LeGend: 一种数据驱动的硬件模型检验中引理生成框架
LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking
AI总结：
LeGend通过全局表示学习提升硬件模型检验中引理生成效率，减少计算开销并提高可扩展性。
摘要：
RTL设计的属性检验是形式验证中的核心任务。在可用引擎中，IC3/PDR是广泛使用的骨干，其性能关键依赖于归纳泛化，即把具体的反归纳例子（CTI）立方体泛化为引理。先前的工作探索了利用机器学习指导这一步骤，并取得了令人鼓舞的结果，但大多数方法采用每子句图分析范式：对每个子句反复构建和分析图，导致高额开销并形成可扩展性瓶颈。我们引入LeGend，用一次性全局表示学习替代这种范式。LeGend预训练一个领域适应的自监督模型，生成锁嵌入，以捕捉全局电路属性。这些预计算的嵌入允许轻量模型以极小的开销预测高质量引理，有效地将昂贵的学习与快速推断解耦。实验显示LeGend在多个基准上加速了两种最先进的IC3/PDR引擎，展示了形式验证扩展的有前途的路径。
英文摘要：
Property checking of RTL designs is a central task in formal verification. Among available engines, IC3/PDR is a widely used backbone whose performance critically depends on inductive generalization, the step that generalizes a concrete counterexample-to-induction (CTI) cube into a lemma. Prior work has explored machine learning to guide this step and achieved encouraging results, yet most methods adopt a per-clause graph analysis paradigm: for each clause they repeatedly build and analyze graphs, incurring heavy overhead and creating a scalability bottleneck. We introduce LeGend, which replaces this paradigm with one-time global representation learning. LeGend pre-trains a domain-adapted self-supervised model to produce latch embeddings that capture global circuit properties. These precomputed embeddings allow a lightweight model to predict high-quality lemmas with negligible overhead, effectively decoupling expensive learning from fast inference. Experiments show LeGend accelerates two state-of-the-art IC3/PDR engines across a diverse set of benchmarks, presenting a promising path to scale up formal verification.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
