[2603.04450] MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering

Computer Science > Logic in Computer Science arXiv:2603.04450 (cs) [Submitted on 26 Feb 2026] Title:MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering Authors:Soumik Guha Roy, Sumana Ghosh, Ansuman Banerjee, Raj Kumar Gajavelly, Sudhakar Surendran View a PDF of the paper titled MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering, by Soumik Guha Roy and 3 other authors View PDF 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 embedding and design statistics, resulting in speedup in verification results. Experimental results on the HWMCC benchmarks show the efficacy of our proposal with resp...