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

TL;DR

LeGend pre-trains a domain-adapted self-supervised model to produce latch embeddings that capture global circuit properties, which allow a lightweight model to predict high-quality lemmas with negligible overhead, effectively decoupling expensive learning from fast inference.

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.

Figures (3)

• Figure 1: Overview of the LeGend pipeline with three stages. Stage 1: Preprocessing. For each circuit we build a global graph and run a pre‑trained self‑supervised GNN once offline to obtain per‑latch embeddings, which are cached and augmented with a dynamic flip‑rate feature. An oracle solver finds the inductive invariants (as a set of clauses) for those instances in the training set. Stage 2: Training. A permutation‑invariant DeepSets aggregator with global pooling produces a clause‑context vector, and a lightweight MLP scores each literal conditioned on this context. Stage 3: Inference. For an AIG file, the encoder is kept frozen and is executed once to obtain that circuit’s per‑latch embeddings; these precomputed vectors are then reused across all candidate clauses within the same circuit, so there is no per‑clause graph construction, graph convolutions, or message passing. CTIs are sampled and minimally reduced, literal scores are thresholded to assemble predicted clauses, and clauses that pass the sanity checks (initiation and first-step consistency) are side‑loaded into the IC3/PDR solver.
• Figure 2: The latch embedding pipeline. We start with a gate-level AIGER circuit, which is converted into a graph, and we use a pre-trained GraphCL model to generate structural latch embeddings. These are further enhanced with signal flip rates, the dynamic functional feature to capture both static structure and dynamic behavior.
• Figure 3: Ablation study of LeGend side-load lemma quality