Paper
LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking
Authors
Mingkai Miao, Guangyu Hu, Wei Zhang, Hongce Zhang
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.
Metadata
Related papers
Fractal universe and quantum gravity made simple
Fabio Briscese, Gianluca Calcagni • 2026-03-25
POLY-SIM: Polyglot Speaker Identification with Missing Modality Grand Challenge 2026 Evaluation Plan
Marta Moscati, Muhammad Saad Saeed, Marina Zanoni, Mubashir Noman, Rohan Kuma... • 2026-03-25
LensWalk: Agentic Video Understanding by Planning How You See in Videos
Keliang Li, Yansong Li, Hongze Shen, Mengdi Liu, Hong Chang, Shiguang Shan • 2026-03-25
Orientation Reconstruction of Proteins using Coulomb Explosions
Tomas André, Alfredo Bellisario, Nicusor Timneanu, Carl Caleman • 2026-03-25
The role of spatial context and multitask learning in the detection of organic and conventional farming systems based on Sentinel-2 time series
Jan Hemmerling, Marcel Schwieder, Philippe Rufin, Leon-Friedrich Thomas, Mire... • 2026-03-25
Raw Data (Debug)
{
"raw_xml": "<entry>\n <id>http://arxiv.org/abs/2602.24010v1</id>\n <title>LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking</title>\n <updated>2026-02-27T13:34:48Z</updated>\n <link href='https://arxiv.org/abs/2602.24010v1' rel='alternate' type='text/html'/>\n <link href='https://arxiv.org/pdf/2602.24010v1' rel='related' title='pdf' type='application/pdf'/>\n <summary>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.</summary>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.AR'/>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.SE'/>\n <published>2026-02-27T13:34:48Z</published>\n <arxiv:primary_category term='cs.AR'/>\n <author>\n <name>Mingkai Miao</name>\n </author>\n <author>\n <name>Guangyu Hu</name>\n </author>\n <author>\n <name>Wei Zhang</name>\n </author>\n <author>\n <name>Hongce Zhang</name>\n </author>\n </entry>"
}