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

This paper proposes MPBMC, a hybrid approach that leverages Graph Neural Network embeddings and runtime design statistics to functionally cluster properties, thereby significantly accelerating multi-property Bounded Model Checking verification on HWMCC benchmarks compared to state-of-the-art methods.

The Gist

Imagine you are a detective trying to solve a massive, complex crime scene. You have a list of 50 different clues (properties) you need to investigate.

The Old Way (The "Solo Detective" Approach):
Traditionally, you would pick one clue, investigate it from start to finish, write your report, and then move to the next clue.

• The Problem: You keep re-reading the same witness statements and re-walking the same hallways for every single clue. It's slow and redundant.
• The "Group" Approach: Alternatively, you could try to investigate all 50 clues at the exact same time.
• The New Problem: This creates chaos. The clues might contradict each other, or the "hard" clues might slow down the "easy" ones. You end up overwhelmed with notes (conflict clauses) that don't help anyone, and you solve nothing faster.

The Paper's Solution (MPBMC):
This paper introduces a smart system called MPBMC (Multi-Property Bounded Model Checking with GNN-guided Clustering). Think of it as a Smart Detective Squad Manager that uses a "Crystal Ball" (Artificial Intelligence) to decide which clues should be investigated together.

Here is how it works, broken down into simple steps:

1. The "Crystal Ball" (Graph Neural Networks)

The system uses a type of AI called a Graph Neural Network (GNN). Imagine the circuit design (the crime scene) as a giant, complex map of roads and intersections.

• Instead of just looking at the map's shape (structural), the AI learns the meaning of the roads (functional). It understands that "Road A" and "Road B" might look different but lead to the same destination.
• The AI creates a "fingerprint" (embedding) for every clue based on how it actually works within the circuit.

2. The "Training Camp" (Offline Phase)

Before the real investigation starts, the system runs a training camp.

• It takes thousands of past cases (benchmark designs) and tries different combinations of clues.
• It learns: "Hey, when we investigate Clue X and Clue Y together, we solve them 50% faster because they share the same secret path."
• It also learns: "Never put Clue Z with Clue W; they fight each other and slow everything down."
• It builds a massive "Best Practice Book" (Database) that tells it which clues are best friends.

3. The "Matchmaker" (Online Phase)

Now, a new, unknown case arrives.

• The Look-Alike: The system looks at the new case and finds a past case in its "Best Practice Book" that looks very similar (like finding a twin).
• The Grouping: It doesn't just copy the groups; it maps the new clues to the old ones. If Clue A in the new case is similar to Clue X in the old case, it knows Clue A should be grouped with Clue B (just like X was grouped with Y).
• The Squad: It creates small, perfect teams of clues that are "functional soulmates."

4. The "Super-Squad" (Verification)

Now, the investigation happens.

• Instead of checking clues one by one or all at once, the system checks these smartly grouped teams.
• Because the clues in the team are so similar, they share their findings instantly. If the AI finds a contradiction in one clue, it immediately helps solve the others in the same group.
• The Result: The "conflict notes" (conflict clauses) that usually pile up and slow things down are drastically reduced. The team moves faster, digs deeper, and solves the mystery in less time.

The Real-World Impact

The authors tested this on a famous set of challenges (HWMCC benchmarks).

• The Result: Their method solved problems significantly faster than the old ways. In some cases, they dug 2,600% deeper into the problem than the standard method could in the same amount of time.
• Why it matters: In the world of chip design (like the chips in your phone or car), finding bugs early is crucial. This method acts like a turbocharger for the verification process, saving time, money, and preventing faulty chips from reaching the market.

In a Nutshell:
This paper teaches computers how to be better team leaders. Instead of letting AI solve problems alone or in a chaotic crowd, it uses deep learning to find the perfect "study groups" for problems, allowing them to learn from each other and solve the puzzle much faster.

Technical Summary

Here is a detailed technical summary of the paper "MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering."

1. Problem Statement

Multi-Property Verification (MPV) is a significant challenge in formal verification. Existing approaches face a trade-off:

• Sequential Verification: Verifying properties one by one lacks information sharing and leads to redundant computations.
• Parallel Verification: Verifying all properties simultaneously often causes a "balancing concern" where difficult properties slow down the entire process. Furthermore, unrelated properties may not share useful conflict clauses (CCs), leading to an explosion in the learned clause repository and degrading performance.

The core objective is to create effective property clusters where functionally similar properties are verified together. This allows the SAT solver to leverage Conflict Directed Clause Learning (CDCL) across properties, where clauses learned for one property benefit the verification of others in the same cluster, thereby reducing verification time and increasing the unrolling depth.

2. Methodology

The authors propose MPBMC, a hybrid framework that combines Graph Neural Network (GNN) embeddings with runtime verification statistics. The workflow is divided into two phases:

A. Offline Database Preparation

This phase builds a knowledge base from a set of benchmark circuits ($C$) to guide future verifications.

1. Data Collection: For each design in $C$, standalone BMC runs are performed to collect verification metrics (time, unrolling depth, status: SAT/UNSAT/UNDET) and Cone of Influence (COI) sizes.
2. Tensor Generation (GNN Embeddings):
   • The authors use DeepGate2 (DG2), a GNN model, to generate functional embeddings for the COI of each property.
   • Sequential circuits are converted to combinational netlists via inductive unfolding before embedding.
   • These embeddings capture the semantic/functional behavior of the properties, moving beyond simple structural similarity.
3. Cluster Construction:
   • K-means and K-medoids clustering are applied to the GNN embeddings to group functionally similar properties.
   • Non-Disjoint Clusters: Unlike traditional methods, properties can belong to multiple clusters. A property is solved in the cluster where it yields the highest performance gain.
4. Influencing Cluster Identification:
   • The system evaluates the "gain" of verifying a property within a specific cluster versus standalone.
   • Gain Metrics: Defined based on status transitions (e.g., UNDET $\to$ SAT, SAT $\to$ SAT with reduced time, UNDET $\to$ deeper UNDET).
   • For each property, the cluster providing the maximum gain is identified as its "Influencing Cluster." This information is stored in a database (DB3).

B. Online Verification

When an unknown design ($\hat{U}$) with a set of properties needs verification:

1. Design Matching: The system identifies the most similar benchmark design ($B$) from the offline database based on structural metrics (gate count, latch count, COI size).
2. Property Mapping: Properties in $\hat{U}$ are mapped to properties in $B$ based on COI size similarity.
3. Cluster Transfer: The "Influencing Clusters" identified for $B$ are transferred to $\hat{U}$ using the property mapping.
4. Execution: BMC is executed on these transferred clusters. Each cluster is verified with a time budget proportional to its size ($T \times \text{cluster size}$).

3. Key Contributions

• GNN-Guided Functional Clustering: The paper introduces the use of GNN embeddings (specifically DG2) to capture the functional similarity of property COIs, addressing the limitations of purely structural (COI-based) clustering.
• Hybrid Approach: It uniquely combines offline neural representations with online runtime statistics to dynamically determine the best property groupings.
• Non-Disjoint Clustering Strategy: The framework allows properties to belong to multiple clusters, selecting the specific cluster that maximizes the verification gain for that property.
• Influencing Cluster Concept: A novel metric-based method to identify which specific cluster configuration yields the best performance for a given property, rather than just grouping them statically.

4. Experimental Results

The method was evaluated on 30 HWMCC 2012-13 benchmarks (using 20 for training/offline and 10 for testing).

• Performance Gain:
  • The proposed method achieved UNDET depth gains (maximum unrolling depth within a time bound) ranging from 34.37% to 2647.76% for individual properties.
  • Average gains ranged from 13.61% to 430.23%.
  • Over 51% of the influenced properties achieved higher unrolling depths compared to standalone verification.
• Comparison with State-of-the-Art (SOTA):
  • MPBMC outperformed existing clustering techniques (based on structural grouping) in 8 out of 10 test cases.
  • Notably, for the complex design 6s329 (with ~1.7M gates), SOTA methods failed to generate any clusters, while MPBMC successfully formed clusters and verified the design.
• Conflict Clause Analysis:
  • Experiments showed that MPBMC generates significantly fewer conflict clauses (CCs) per frame compared to standalone verification. This confirms that grouped properties successfully share learned clauses, reducing the search space.
• Verification Time:
  • The method reduced verification time for influencing clusters compared to the sum of standalone verification times for the constituent properties.

5. Significance

This work represents a significant step forward in Formal Verification by bridging Deep Learning and SAT-based Model Checking.

• Scalability: By intelligently grouping properties, MPBMC mitigates the "curse of dimensionality" in multi-property verification, allowing tools to verify larger and more complex designs within practical time limits.
• Efficiency: The reduction in conflict clauses and redundant computations translates directly to resource savings (CPU/GPU time and memory).
• Generalization: The use of GNN embeddings suggests that the approach can generalize well across different circuit topologies, moving beyond rigid structural heuristics to semantic understanding of circuit behavior.

The paper concludes that leveraging functional representations via GNNs, combined with runtime feedback, creates a robust framework for accelerating multi-property bounded model checking. Future work aims to incorporate dynamic clustering and sensitivity analysis of hyperparameters.