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

TL;DR

This paper proposes 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).

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.

Figures (5)

• Figure 1: Conflict Clause plot on 6s154.aig from HWMCC
• Figure 2: Our Framework - MPBMC
• Figure 3: Conflict Clause (CC) Analysis
• Figure 4: Verification Time (V Time) Comparison
• Figure 5: Stand-alone vs MPBMC UNDET Depth Comparison