LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking

TL;DR

LeGend introduces a global representation learning approach to improve lemma generation in hardware model checking, significantly enhancing scalability and efficiency of IC3/PDR engines.

Contribution

LeGend replaces per-clause graph analysis with a pre-trained global embedding model, enabling faster and more scalable lemma prediction in formal verification.

Findings

Accelerates IC3/PDR engines across various benchmarks.

Reduces overhead by decoupling learning from inference.

Demonstrates scalability improvements in hardware model checking.

Abstract

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.