Presentation
Legend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking
DescriptionThe IC3/PDR algorithm is a cornerstone of hardware model checking, and machine learning (ML) has been explored to guide its critical inductive generalization step. However, prior ML methods are built upon a per-clause graph analysis paradigm, requiring repetitive and costly graph processing for every clause, creating a severe scalability bottleneck. Therefore, we introduce LeGend, a framework that completely replaces this paradigm with one-time global representation learning. LeGend architects a domain-adapted self-supervised learning task to generate latch embeddings that encode global circuit properties. These pre-computed embeddings enable a lightweight model to predict high-quality lemmas with negligible overhead, effectively decoupling expensive learning from fast inference. Experiments show our approach accelerates two state-of-the-art IC3/PDR engines across a diverse set of benchmarks, presenting a promising path to scale up formal verification.
Event Type
Research Manuscript
TimeWednesday, July 2911:06am - 11:18am PDT
LocationMtg Room 202AB