MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering
Soumik Guha Roy, Sumana Ghosh, Ansuman Banerjee, Raj Kumar Gajavelly, Sudhakar Surendran

TL;DR
This paper introduces MPBMC, a novel approach that uses GNN-guided clustering of properties to enhance the efficiency of multi-property bounded model checking in hardware verification.
Contribution
It presents a hybrid method combining GNN-based functional embeddings and runtime statistics for effective property clustering in multi-property verification.
Findings
Achieves significant speedup in verification times.
Outperforms existing clustering strategies on HWMCC benchmarks.
Demonstrates the effectiveness of GNN-guided clustering in BMC.
Abstract
Formal verification of designs with multiple properties has been a long-standing challenge for the verification research community. The task of coming up with an effective strategy that can efficiently cluster properties to be solved together has inspired a number of proposals, ranging from structural clustering based on the property cone of influence (COI) to leverage runtime design and verification statistics. In this paper, we present an attempt towards functional clustering of properties utilizing graph neural network (GNN) embeddings for creating effective property clusters. We propose a hybrid approach that can exploit neural functional representations of hardware circuits and runtime design statistics to speed up the performance of Bounded Model Checking (BMC) in the context of multi-property verification (MPV). Our method intelligently groups properties based on their functional…
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 · Physical Unclonable Functions (PUFs) and Hardware Security · Adversarial Robustness in Machine Learning
