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

Source: arXiv - 2602.24010v1

Overview

The paper presents LeGend, a data‑driven framework that speeds up lemma generation in IC3/PDR‑based hardware model checking. By moving from per‑clause graph analysis to a one‑time global embedding of circuit latches, LeGend cuts the inference overhead dramatically, enabling existing verification engines to run faster on real‑world RTL designs.

Key Contributions

• Global latch embeddings: Introduces a self‑supervised pre‑training step that learns a compact vector representation for every latch in a circuit, capturing its structural and functional context.
• Lightweight lemma predictor: Uses the pre‑computed embeddings to train a tiny neural model that can instantly suggest high‑quality lemmas for any counterexample‑to‑induction (CTI) cube.
• Decoupled training/inference: The expensive representation learning is performed once per design, while inference during model checking is essentially free (microseconds).
• Empirical speed‑up: Demonstrates consistent acceleration of two state‑of‑the‑art IC3/PDR tools across a broad benchmark suite, with up to 2.3× reduction in total verification time.
• Open‑source prototype: Provides a reference implementation and scripts for reproducing the experiments, facilitating adoption by the verification community.

Methodology

1. Circuit preprocessing: The RTL netlist is parsed into a graph where nodes are latches (state elements) and edges represent combinational connections.
2. Self‑supervised pre‑training: A graph neural network (GNN) is trained on the whole circuit using a masked‑node prediction task—randomly hide a latch’s type or connectivity and ask the model to reconstruct it. This forces the GNN to learn embeddings that encode global circuit properties.
3. Embedding extraction: After training, each latch receives a fixed‑size vector (e.g., 128‑dim) that is stored for later use. No further graph traversal is needed.
4. Lemma generation model: A lightweight feed‑forward network takes as input the embeddings of the latches that appear in a CTI cube and outputs a probability score for each possible clause (lemma). The top‑scoring clause is selected as the generalized lemma.
5. Integration with IC3/PDR: The predictor replaces the traditional per‑clause graph analysis step. When the engine needs to generalize a CTI, it simply looks up the relevant embeddings and runs the predictor, which takes only a few microseconds.

The overall pipeline separates the heavy learning phase (once per design) from the fast inference phase (many times per verification run).

Results & Findings

• Inference overhead: Lemma prediction adds < 0.01 s per CTI, compared to > 0.3 s for the previous graph‑analysis approach.
• Quality trade‑off: The lemmas produced by LeGend are on average more general (fewer literals) without sacrificing proof completeness.
• Scalability: The pre‑training time grows linearly with the number of latches and is amortized across many verification runs on the same design.

Practical Implications

• Faster verification cycles: Teams can iterate on RTL changes more quickly because the model‑checking step becomes less of a bottleneck.
• Reduced compute cost: Lower CPU time translates to cheaper cloud or on‑premise verification farms, especially valuable for large‑scale ASIC projects.
• Plug‑and‑play integration: Since LeGend only replaces the lemma‑generation module, existing IC3/PDR tools (e.g., ABC, CoSA) can adopt it with minimal code changes.
• Potential for continuous learning: The pre‑trained embeddings can be cached and reused across multiple verification runs of the same design, or fine‑tuned when new modules are added, enabling a “learning‑accelerated” verification workflow.
• Broader AI‑for‑EDA adoption: Demonstrates that a one‑time global representation learning step can overcome the scalability issues that have limited previous ML‑assisted verification techniques.

Limitations & Future Work

• Design‑specific training: The embeddings must be re‑trained for each new RTL design; the current approach does not yet support cross‑design transfer learning.
• Model size vs. hardware constraints: While inference is lightweight, the GNN pre‑training still requires a GPU or a powerful CPU, which may be a hurdle for small teams.
• Clause space exploration: LeGend predicts a single lemma per CTI; extending it to propose multiple diverse candidates could further improve proof search.
• Integration with other engines: Future work will explore applying the same embedding strategy to SAT‑based BMC or interpolation‑based model checking.
• Robustness to aggressive optimizations: The authors note that heavily optimized netlists (e.g., after aggressive logic synthesis) sometimes degrade embedding quality; adaptive retraining strategies are under investigation.

Authors

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

Paper Information

• arXiv ID: 2602.24010v1
• Categories: cs.AR, cs.SE
• Published: February 27, 2026
• PDF: Download PDF