MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering
This work provides an incremental improvement in formal verification efficiency for hardware designers by intelligently grouping properties for Bounded Model Checking.
The paper addresses the challenge of multi-property formal verification by proposing a GNN-guided clustering method for properties. This approach combines neural functional representations of hardware circuits with runtime design statistics to group properties, leading to speedups in Bounded Model Checking (BMC) performance on HWMCC benchmarks.
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 respect to the state-of-the-art.