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.

翻译：寄存器传输级设计的属性检查是形式化验证的核心任务。在现有引擎中，IC3/PDR是广泛使用的基础框架，其性能关键依赖于归纳泛化步骤——该步骤将具体的反归纳立方体泛化为引理。先前研究已探索使用机器学习指导该步骤并取得了鼓舞人心的成果，但多数方法采用逐子句图分析范式：针对每个子句重复构建和分析图，产生巨大开销并造成可扩展性瓶颈。本文提出LeGend框架，通过一次性全局表示学习替代该范式。LeGend预训练领域适配的自监督模型以生成捕获电路全局特性的锁存器嵌入向量。这些预计算的嵌入使得轻量级模型能以可忽略的开销预测高质量引理，有效实现昂贵学习与快速推理的解耦。实验表明，LeGend在多样化基准测试中加速了两个最先进的IC3/PDR引擎，为扩展形式化验证规模提供了可行路径。