LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking
Mingkai Miao, Guangyu Hu, Wei Zhang, and Hongce Zhang

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,…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Adversarial Robustness in Machine Learning · Physical Unclonable Functions (PUFs) and Hardware Security
