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

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 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.