Paper deep dive
MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering
Soumik Guha Roy, Sumana Ghosh, Ansuman Banerjee, Raj Kumar Gajavelly, Sudhakar Surendran
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 89%
Last extracted: 7/20/2026, 8:40:04 AM
Summary
The paper introduces MPBMC, a framework for Multi-Property Bounded Model Checking (BMC) that utilizes Graph Neural Networks (GNN) to cluster properties based on functional similarity. By leveraging GNN embeddings of property Cones of Influence (COI) and runtime statistics, the method identifies high-affinity property groups to speed up verification. The approach involves an offline phase to build databases of property clusters and an online phase to map unknown designs to similar benchmarks for efficient verification.
Entities (8)
Relation Signals (5)
MPBMC → appliesto → Bounded Model Checking
confidence 95% · speed up the performance of Bounded Model Checking (BMC) in the context of multi-property verification
MPBMC → uses → Graph Neural Network
confidence 95% · We propose a hybrid approach that can exploit neural functional representations of hardware circuits... utilizing graph neural network (GNN) embeddings
MPBMC → evaluatedon → HWMCC
confidence 90% · Experimental results on the HWMCC benchmarks show the efficacy of our proposal
DeepGate2 → generates → Cone of Influence
confidence 85% · We use DG2 model embeddings for circuit representation learning and property similarity evaluation... GNN-based embeddings identify functionally similar properties
MPBMC → groups → Cone of Influence
confidence 80% · Our method intelligently groups properties based on their functional embedding and design statistics
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2603.04450v1
- Canonical: https://arxiv.org/abs/2603.04450v1
Trouble viewing inline? Open PDF directly →
Full Text
34,539 characters extracted from source content.
Expand or collapse full text
MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering Soumik Guha Roy ∗ , Sumana Ghosh ∗ , Ansuman Banerjee ∗ , Raj Kumar Gajavelly ‡ , Sudhakar Surendran § ∗ Indian Statistical Institute, Kolkata, India, Email: soumikr,sumana,ansuman@isical.ac.in, ‡ IBM Systems,India, Email: rgajavel@in.ibm.com, § Texas Instruments,India, Email: sudhakars@ti.com Abstract—Formal verification of designs with multiple prop- erties 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. Index Terms—Multi-property Verification, Bounded Model Checking, Graph Neural Networks, Clustering 1 I. INTRODUCTION Multi-property verification [1] is a challenge for formal ver- ification tools. On one extreme, verification techniques that verify properties one at a time, lack information sharing and reuse, and thereby miss the chance to avoid redundant com- putations. On the other extreme, approaches that proceed with all properties together in tandem may suffer from a balancing concern, wherein hard-to-verify properties may slow down the overall progress. The key to solving this challenge is to create an effective property clusters consisting of properties that have high similarity and can be solved together. Each property depends on a specific part of the design’s logic, known as its cone of influence (COI) or fanin logic; this includes all signals that directly or transitively affect the computation of the property status. The insight behind solving structurally / functionally similar properties together in a verification run is to leverage the expected benefit that their proofs/counter- examples build along similar paths/substructures of the design, thereby avoiding redundant computations if the properties are taken up separately for verification. In this work, we consider Bounded Model Checking (BMC) [2] verifiers that take in a design description along with a set of properties to be verified and incrementally unfold the design and the properties across increasing depths beginning from the start, in an at- tempt to falsify the constituent properties using a Satisfiability 1 This work is supported by Semiconductor Research Corporation (SRC). (SAT) solver to solve at every depth. An important aspect in SAT-based verification is Conflict Directed Clause Learning (CDCL) [3] wherein a SAT solver learns conflict clauses from one part of the design space, which can be effective in other parts of the search. In the context of BMC, as we proceed with multiple properties together, an important objective is to ensure that the learnt clauses benefit all properties in the given run. This necessitates the importance of an effective clustering strategy which places functionally similar properties together and functionally different ones in different runs. A random set of properties, if placed together in the same BMC run, may impede progress, since the properties may not be able to benefit from common conflict clauses (C) and learnt clauses, thereby overwhelming the learnt clause repository, and slowing down the verification process. An example plot of C versus increasing verification depth (also called frames in BMC parlance) is shown in Fig. 1 on the design 6s154.aig selected from the Hardware Model Checking Competition (HWMCC) [4], [5] benchmarks, where the number of conflict clauses (C) using a random property cluster exceeds the individual C count (both the average and maximum when properties are run separately). This increase in conflict clauses can make concurrent verification much slower than verifying properties one by one, thereby asserting the importance of an efficient clustering mechanism that can take in a given set of properties on a given design and create high affinity functional property groups, with a hope that when such properties are verified together, the overlap in their COIs can be exploited to enhance the verification via mutually beneficial clause learning, saving both time and computational resources. 020406080100 # Frames # C Max C Avg C Random C Total C Fig. 1: Conflict Clause plot on 6s154.aig from HWMCC For effective multi-property verification, a number of research articles [6], [7] in literature have proposed to create small property groups consisting of similar properties to be solved together, leveraging common subproblem sharing typically through structural grouping (COI-based) of properties, but arXiv:2603.04450v1 [cs.LO] 26 Feb 2026 with limited benefits. These approaches often overlook the semantic functional similarity between properties or runtime verification statistics. While clustering of properties based on functional similarity is helpful, it is computationally challeng- ing to efficiently compute effective clusters that adequately capture functional similarities between properties. This work attempts to address these aspects towards clustering and effec- tive verification of multi-property designs. In this work, we use the graph neural network representation of circuits and property COIs to learn effective functionally similar property clusters. The rise of deep learning (DL) has influenced several stages of the circuit design lifecycle [8], with representation learning emerging as a key technique for generating embeddings that support tasks like verification and high-level synthesis [9]. With the recent rise in successful deployments of Graph Neural Networks (GNN), there is a growing interest in the research community to use GNN models as circuit representations [10], [11] and use the same for EDA tasks like testability analysis [12], SAT solving [13]. Despite the prevalence of GNN-based circuit representation methods, most of the circuit-based analysis approaches are dependent on the structural representation [14]–[16], runtime verification statistics [17], synergies of BMC engines [18], [19]. A recent work [20], [21], reports that the application of GNN-based circuit representations can speed up the verifi- cation. The key contribution of our paper is to show that by learning functional representations of COIs of properties and leveraging runtime statistics jointly, it is possible to enhance the BMC- based circuit verification workflow by creating a judiciously chosen group of properties that are mutually beneficial and contribute to verification scalability. Our method has an of- fline data preparation phase, wherein we analyze and create overlapping property clusters based on neural embeddings of the COIs of properties on a database of available designs, that serves as close approximations of an exact functional similarity based clustering. At runtime for the design to be verified with multiple properties, we utilize runtime unfolding statistics of the given properties towards creating effective property groups. We consider the And-Inverter-Graph (AIG) representation of logic circuits and build our solution on top of the publicly available FV tool ABC [22], having support for AIG. We use the principle of inductive unfolding [23], which gives us better performance as reported in [20]. We conduct extensive experiments on the HWMCC benchmarks to show the performance of our GNN-aided multi-property design verification. We compare our performance against stand-alone property verification and a state-of-the-art technique based on clustering [15], [16]. We have the following contributions. • Use of GNN embeddings for effective property clustering. • Use of property clusters in verification to speed up BMC. • Extensive experimental results on HWMCC benchmarks. The rest of the paper is organised as follows. Section I provides a background. Section I presents our methodology. Experiments are in Section IV. Section V concludes the paper. I. BACKGROUND A. Multi-Property Bounded Model Checking In multi-property verification, given an unknown design b U , and a set of properties S P , the model checker is tasked to verify if the design satisfies (or models) the properties. i.e., b U |= P, ∀P ∈ S P . A Bounded Model Checking (BMC) algorithm incrementally unfolds the design and the negation of a property to increasing depths (also called frames in BMC parlance) starting from the initial frame and searches for a counter-example (CEX) at each frame using a SATisfiability (SAT) solver. BMC tools are typically run with a maximum frame bound or time bound, within which it may either be able to conclude a property as proven (if the diameter of the design is reached), falsified (if it gets a counter-example at any depth) or report the status of a property as undetermined (UNDET), in which case it reports the maximum depth (also called the maximum unrolling depth) till which the property remained satisfiable and no counter-example could be found. The performance of a BMC engine is quantified either by the time taken to find the CEX (i.e., time metric) or by the maximum unrolling depth given a time bound if no CEX is found (i.e., unrolling depth metric). For a design with multiple properties, a BMC tool may work with one property at a time, or with all / subset of properties together in which case it proceeds breadthwise with all of the properties together. For individual runs, the time to CEX or maximum depth is reported, while for multiple properties together runs, the status of invididual properties (proven / falsified / UNDET) is reported along with the maximum unrolling depth. B. Functional Representation Learning of Circuits Functional representation of a circuit focuses on the input output behavior of a circuit, thus showing better capabilities towards generalization of circuit behavior. Graph Neural Net- works (GNN) offer a promising mechanism towards circuit representation learning. DeepGate [10], [11] is a GNN model for obtaining a general and effective circuit representation. DeepGate embeds the logic function and structural infor- mation using attention mechanisms that mimics the logic procedure for circuit learning from unique circuit properties. DeepGate uses the ratio of logic-1 in the truth table as a functionality-related supervision metric. Due to inadequacy of the functionality-related supervision metric, multiple rounds of message passing are needed to preserve the logical correlation of gates, which is often time-consuming for large circuits. DeepGate2 (DG2) [10] attempts to counter these challenges, employing pairwise truth table differences using Hamming Distance between sampled logic gates as a supplementary supervision, with a loss function that minimizes the disparity between pairwise node embedding and pairwise truth table difference. Moreover, this method introduces an efficient one- round GNN that captures both structural and functional prop- erties, leveraging the inherent circuit characteristics. We use DG2 model embeddings for circuit representation learning and property similarity evaluation. Tensor Generation DB1 DB2 DQ Q GNN (DG2) Cluster Construction Cluster Verification Influencing Cluster DB3 Phase 1: Offline Database Preparation Phase 2: Online Verification DQ Q COI Similarity DQ Q Property Affinity Property Match between U and B Cluster Convert Verification Best Design (B) Benchmark Design (B) Stand-alone Verification and COI size Extraction Unknown Design (U) Fig. 2: Our Framework - MPBMC I. DETAILED WORKFLOW Given an unknown design b U with a set of n properties, denoted as S P , our objective is to create high similarity property clusters to be verified in the same BMC run. With these property clusters, we aim to maximize the BMC unrolling depth within a given time bound for each property for which a CEX is not found, or minimize the time taken to generate a CEX otherwise. To build high similarity property clusters, we use popular machine learning algorithms for clustering on the functional tensors of the COIs of the properties. We assume we have a database C of already verified designs, each with multiple properties, for which the best performing clustering information is available when we verify b U . We use this information for creation of property clusters for b U . Our framework, shown in Fig. 2 consists of two main phases, (a) an offline database preparation phase on C and (b) an online phase with the objective of efficient verification for b U guided by a designB ∈C from offline information. The overall approach for the proposed framework is as below. In the offline phase, verification status and COI sizes of each property are collected for each reference circuit in C. GNN-based embeddings identify functionally similar properties, which are clustered and selectively retained based on verification results. In the online phase, the unknown design b U is matched to a similar benchmark B ∈C using COI-based similarity, and the top-performing clusters from B guide the verification of b U . The details of the proposed framework follow next. A. Offline Data Preparation This offline phase is done once to prepare three databases, DB 1 , DB 2 , and DB 3 based on the set of given benchmark circuits C. DB 1 stores the circuit’s structural data, DB 2 holds property embeddings of each design, and DB 3 stores influencing cluster information to guide the search for the best property group to be used for faster verification for design b U . We explain the construction of each below. For each design in C, we carry out the following steps to prepare the databases. Single Property Run and Information Collection: We per- form a standalone BMC of each property of the design for a fixedT amount of time and store the verification metric value (time / unrolling depth), verification status (SAT / UNSAT / UNDET), and property COI size information. We store this information in DB 1 for use at a later stage. Tensor Generation: In this phase, we find the functional representation of each property using the GNN embedding of each property COI. This is utilized in the cluster construction phase, with the representations helping us move to a different embedding space to perform cluster-based similarity analysis between properties. For creating these GNN embeddings, we use DG2. It may be noted that DG2 works only on combinational designs; thus, for a sequential circuit B ∈ C, we generate an inductive unfolding to get a combinational circuit netlist and generate the tensor. These GNN embeddings constitute the database DB 2 . Cluster Construction:Once the GNN embeddings of the COI of each property are available, we use K-means and K-medoids clustering to identify high-affinity groups of properties, based on their functional embeddings generated in the previous step. It may be noted that the cluster sets formed S cluster =S 1 ,S 2 ,...,S n where each S i is a set of functionally similar properties, with sizes ranging from 2 to the total number of properties in the design, are not necessarily mutually disjoint. This is what makes our approach distinctly different from other approaches that cluster properties into disjoint clusters. The unique idea that drives our approach is that a property may belong to multiple clusters; it is solved in one cluster where it gains the most, and its presence helps to expedite the solution of others in the other clusters where it is present. We explain this in detail at a later stage. Cluster Execution and Information Collection: This phase has a significant effect on the overall performance as it guides the detection of influencing clusters (defined next) along with their influenced properties. With the cluster configurations obtained above, we carry out a BMC run on each cluster separately with the design, and only the set of properties that belong to the cluster. The time allotted to this BMC run is T× cluster size, where cluster size is in terms of the number of properties present in the cluster, and T is the time value used above for a single property run. Influencing Cluster Identification: For each property, we now identify which cluster is the best performing one. As mentioned earlier, our clusters are not disjoint; thus, a property may belong to multiple clusters. We aim to identify which among these clusters gives the best benefit in performance in terms of a gain metric, which we define next. We refer to this as the influencing cluster for the property. The influencing cluster of a property depends on the verification result of the single property run (done above) and the runs of the clusters in which it belongs. The verification result of a property might change while verifying the same using a cluster of properties. Based on the transition of verification status and the property evaluation metric described below, the influencing cluster identification is done. We define the concept of property gain which is the basis behind this step. To identify the influencing cluster for a property, we need to quantify the gain of each property P i , i.e., Gain(P i ), when it is verified alone versus when it is verified in a cluster. With the results of the stand-alone and cluster execution obtained above, we have 5 possible transitions in the verification status, as below. • UNDET to SAT: This indicates a property P i is UNDET in a stand-alone run and becomes SAT in a cluster run with n other properties. If it takes t c time to derive SAT, then the gain for P i is taken as Gain(P i ) = t c /n. • SAT to SAT: Here, P i is SAT in both stand-alone and cluster run, assume the corresponding times to derive SAT are t s and t c respectively. In this case, the gain for P i is taken as Gain(P i ) = (t s − t c )/t s . Note that this is the relative change in SAT time with respect to its single run. A negative gain value indicates t s < t c . • UNDET to UNDET: In this case, the verification status is UNDET in both the standalone and cluster runs above. Let d s and d c denote the maximum unrolling depth in a given time bound in standalone and grouped verification for P i . Now the gain value for P i is Gain(P i ) = (d c − d s )/d s . A positive gain indicates that d c > d s . • SAT to UNDET: This indicates that a property is SAT in a stand-alone run but UNDET in cluster verification, which means that the presence of a set of properties degrades the verification of P i . The gain is defined like the UNDET- to-UNDET case, as Gain(P i ) = (d c − d s )/d s . • UNSAT to UNDET: Here, the property is found to be UNSAT in stand-alone verification but UNDET while verifying in a cluster. The gain Gain(P i ) is defined in the same way as in the SAT to UNDET case. • UNDET to UNSAT: Similar to the UNDET to SAT case, this transition indicates that a property P i , which is UNDET in a stand-alone run, becomes UNSAT when verified in a cluster with other properties. The gain for P i is defined analogously to the UNDET to SAT case. UNDET-to-SAT and UNDET-to-UNSAT cases are most de- sirable, while UNSAT-to-UNDET is not desirable. With the information above, we identify the influencing cluster for each property. As discussed in the cluster construction phase, a property P i ∈ S j ∈ S cluster can belong to multiple clusters, with different cluster-specific gains, denoted as Gain(P i ) S j . Among the associated clusters of P i , the cluster S I having the highest gain for P i is the influencing cluster or top performing cluster for P i . P i is termed as influenced by S I . To identify the influencing cluster S I for a property P i , we need to compare the gain values for P i , considering all clusters to which it belongs. The gain value for a property with respect to a cluster is a 6-element vector, with a non-zero entry in one of the positions only. For this comparison, we need to set up an order between the 6 fields above. We use the total order: UNDET- to-SAT = UNDET-to-UNSAT > SAT-to-SAT > UNDET-to- UNDET > SAT-to-UNDET > UNSAT-to-UNDET. Consider an example property P which belongs to 4 different clusters S 1 ,S 2 ,S 3 ,S 4 , resulting in 4 different cluster-specific gain values as Gain(P) S i where i ∈ 1, 2, 3, 4. For example, a cluster S 2 is an influencing cluster for the property P if Gain(P) S 2 > Gain(P) S i , where i ∈ 1, 3, 4 considering a vector to vector comparison. It may happen that due to different transitions in verification status, cluster-specific gains of P are different. In that case, the metric evaluation order, discussed above, is used to find the influencing cluster for P . To illustrate the evaluation order with an example, assume a property Q is associated with two different clusters S 1 and S 2 . The transition of verification status of Q in S 1 and S 2 is UNDET-to-UNDET and UNDET-to-SAT, respectively. Let the cluster specific gain for the property Q are Gain(Q) S 1 = 0.9 and Gain(Q) S 2 = 0.4. Although the cluster-specific gain for S 2 is less, but metric evaluation order gives priority to S 2 to be the influencing cluster for Q. The setup of DB 3 is completed hereafter. As an output of the above, we have identified the influencing cluster for each property in a design. DB 3 contains this information for all designs, for all constituent properties. As an example, consider a design B with the following clusters P 1 ,P 4 ,P 1 ,P 2 ,P 3 ,P 2 ,P 3 ,P 4 ,P 2 ,P 3 ,P 1 ,P 3 ,P 4 . Table I shows the influencing clusters for B. TABLE I: Influencing clusters for a design B PropertyP 1 P 2 P 3 P 4 Influencing Cluster P 1 , P 3 , P 4 P 2 , P 3 P 1 , P 3 , P 4 P 1 , P 4 B. Online verification Given an unknown circuit b U that hasP b U number of properties to be verified using BMC, we consider the time bound as T ×P b U , whereT is the fixed verification time bound (Sec. I) given to each property in b U . We now use the databases DB 1 and DB 3 to use the influencing cluster to accelerate the verification of b U . Our goal is to select the most similar design B from the database of known designs C, whose influencing cluster information will guide the BMC for verification of b U . This consists of two main steps. Initial Pruning: From DB 1 , we first extract the set of cir- cuitsS whose property count falls in the range [P b U −δ,P b U +δ], where δ > 0 is a tuning parameter that reduces the overall search space to a limited number of known circuits having a total number of properties close to P b U . Similarity Search and Cluster Construction: This part con- sists of three main steps as described below. • Most Similar Circuit Identification: First, we compare the design information (number of gates, sequential elements, inverters) of all the circuits inS with b U using the database DB 1 . The circuit having minimal difference in COI size information is used as the most similar circuit B. • Property Mapping: Next, we find the similarities between properties in B and b U . For this, we unfold each property of b U , extract its COI size, and compare it with the COI size of each property of B, stored in DB 1 . We find the differences in the information about the COI size between each pair of properties, and this gives us, for each property in b U , the most similar property in B. • Influencing Cluster Information Extraction:Next, the influencing cluster information for each property in B is extracted from DB 3 . Now, the extracted influencing Algorithm 1: Online Verification Input: Unknown design b U , Databases DB 1 , DB 3 ,threshold δ 1 DB pruned ← ∆ designinfo ←∅ ; 2 foreach design ∈DB 1 do 3if P b U − δ < P design < P b U + δ then 4 DB pruned ←DB pruned ∪design ; 5 foreach design ∈DB pruned do 6 designinfo 1 ← getInfo(design,DB 1 ) ; // Returns COI Size Info 7 design info 2 ← getInfo( b U,DB 1 ) ; // Returns COI Size Info After Unfolding 8 diff ←|designinfo 1 − designinfo 2 | ; // Finding COI Difference 9∆ design info ← ∆ designinfo ∪ (design,diff ) ; 10 B ← min(∆ design info ) ; // Most Similar Design 11 foreach prop 1 ∈B do 12forall prop 2 ∈ b U do 13info P 1 ← getInfo(P 1 ,D depth ,DB 1 ) ; // Find property COI after unfolding 14info P 2 ← getInfo(P 2 ,D depth ,DB 1 ) ; 15diff Matrix[i][j]←|info P 1 − info P 2 | ; // Store Property COI diff in Matrix 16 UD Map ← property_association(diffMatrix) ; // Find Property Association in terms of Smaller COI Diff 17 inf cluster ← getInfCluster(B,DB 3 ) ; // Find Influencing Cluster / * Cluster Conversion Starts * / 18 C ′ =∅ ; 19 foreach cls∈ inf cluster do 20 cls ′ = φ ; 21foreach p∈ cls do 22p ′ = UD Map (p) ; 23cls ′ = cls ′ ∪ p ′ ; 24 C ′ =C ′ ∪ cls ′ ; / * Verification Starts * / 25 Verify(C ′ ) ; clusters are converted to the corresponding cluster of properties using the properties of b U . Once the clusters are obtained for b U , BMC is run one cluster at a time, with all the properties in each cluster running together, with a total time per cluster as T× cluster-size as explained earlier. We record the verification status and time / unrolling depth for each cluster run, and compare these values with stand-alone runs of each property and a recent work, as explained in the following. Algorithm 1 summarizes the overall approach. IV. EXPERIMENTAL EVALUATION Benchmarks and Setup: To show the efficacy of the proposed framework, we conducted experiments on a set of 30 bench- mark circuit designs taken from the HWMCC 2012-13 [4], [5] benchmarks. The number of AND gates and latch count of these designs lie within the range of (1.5k − 16k) and (65−102k), respectively. Out of these 30 designs, 20 designs were used to prepare our 3 databasesDB 1 ,DB 2 andDB 3 . We applied the Principal Component Analysis (PCA) during DB 2 preparation with 95% of significant variations preserving the design embeddings. The remaining 10 designs were considered as the new (unknown) circuits b U on which the verification was done. Note that for all these 20 designs, we set the timeout time T to 15 minutes as discussed in Section I. The details (Circuit Name, AND gate, Latch counts, number of properties) of these 10 designs are reported in Columns 1-3 of Table I. In this work, bmc3g is considered as the underlying BMC engine which is available as part of the verification tool, ABC [22]. All experiments were carried out on an Intel 14700K processor, 16GB RAM, NVIDIA T100 8GB GPU. For GNN embeddings, we used DG2 [10] version 2.0.1. The total size of DB 1 ,DB 2 and DB 3 is nearly 600 MB. Additionally, the offline data preparation phase required an average of 210 seconds per design for functional embedding generation. The subsequent clustering step took an average of 28 seconds and 121 seconds per design using the k-means and the k-medoids algorithm, respectively. Result Analysis: Since all the benchmark designs consid- ered are of UNDET type (as reported in HWMCC reports), we consider UNDET (i.e., maximum unrolling depth) as the metric for the performance of BMC verification. Table I reports the respective results where the maximum gain across properties ranges between 34.37% to 2647.76% while the average gain ranges between 13.61% to 430.23%. We consider only those properties as influenced properties, where the UNDET depth in stand-alone verification is less than its associated cluster verification. In summary, we see that more than 51% of total influenced properties denoted as Inf-Prop in Table I (Col-V) achieve higher UNDET depth gain shown as Prop Gainer in Col-VI. We show that our gain achieved is better than the state-of-the-art method [15], [16] (Col X- XII), where we take the reported clusters and compare them with our framework. We achieve higher UNDET depths in 8 among the 10 cases. Notably, for the design 6s329 having maximum AND gate and latch count, our method successfully forms property clusters and outperforms [15], [16], which fail to generate any cluster. 020406080100 # Frames # C Max C Min C Total C MPBMC C Fig. 3: Conflict Clause (C) Analysis Conflict Clause Analysis: Figure 3 shows that for the design 6s409, conflict clause generation per frame in MPBMC is significantly less than in stand-alone verification. This result justifies that mutually beneficial clause learning among the grouped properties helps in reducing conflict clause genera- tion, thereby reducing verification effort. Verification Time Analysis: Here, we consider a cluster of TABLE I: Comparative results on HWMCC‘12-13 Benchmark Benchmark#AND#LAT#Prop#Inf-Prop #PropMPBMC UNDET Gain (%)[15], [16] UNDET Gain (%) Gainer(%)MinAvgMaxMinAvgMax 6s154181831283229761.81238.171200285.711110.982600 6s3291691790319473329932.3813.6134.37--- 6s3434399647744949591.2943.69138.98-88.14-4436.36 bob12m07m635031258535068420.3450-11.760.3612.5 6s3404229133377657513.2220.2264.75-2.3326.6155.56 6s3053651780001164336245.45183.82-88.49234.115065.16 nusmvdme1d16multi1616321120114850.7618.0846.36-16.785.6637.38 bob12m01m74234655514298805.8953.5164.28-1.43-13.337.69 6s42162949511508910021.90430.232647.7621.91404.442367.16 6s4091209171052318412210022100.75354.5569.6158.74345.07 Max gainMin GainSame or higher gain than SOTA the same design with 11 properties where 10 properties have an average 141.85% UNDET gain. Figure 4 indicates that the verification time of our proposed MPBMC method for the influencing cluster is less than all other verification times of all the constituent properties using stand-alone verification. UNDET Depth Analysis: Fig. 5 shows that all properties of the same design 6s409 achieve higher UNDET depth using our proposed method compared to the standalone one. 020406080100 # Frames V Time (sec) Min V Time MPBMC V Time Max V Time Avg V Time Fig. 4: Verification Time (V Time) Comparison 7085100 Stand-alone #Depth MPBMC #Depth MPBMC Depth Standalone Depth Fig. 5: Stand-alone vs MPBMC UNDET Depth Comparison V. CONCLUSION AND FUTURE WORK This work proposes a method for multiproperty verification using clustering and offline design information stored as tensor embeddings. Verifying functionally similar properties together helps in developing mutually beneficial conflict clauses and thus expedites verification. Going ahead, we plan to explore advanced clustering methods that leverage subproblem shar- ing between properties and incorporate dynamic clustering, where cluster configurations adapt over time based on runtime verification statistics. This enhances the effectiveness further and strengthens the overall verification flow. Additionally, we intend to perform a detailed sensitivity analysis of key hyperparameters such as cluster size, GNN architecture, and similarity thresholds to better understand their impact on verification efficiency and accuracy. REFERENCES [1] G. Cabodi and S. Nocco, “Optimized model checking of multiple properties,” in DATE, p. 1–4, 2011. [2] A. Biere et al., “Bounded model checking,” Advances in Computers, vol. 58, 2003. [3] J. Marques-Silva et al., “Conflict-driven clause learning sat solvers,” in Handbook of Satisfiability, vol. 336 of Frontiers in Artificial Intelligence and Applications, p. 133–182, IOS Press, 2021. [4] “Hardware model checking competition 2012 (hwmcc’12),” 2012. https: //fmv.jku.at/hwmcc12/index.html. [5] “Hardware model checking competition 2013 (hwmcc’13),” 2013. https: //fmv.jku.at/hwmcc13/. [6] G. Cabodi et al., “To split or to group: from divide-and-conquer to sub-task sharing for verifying multiple properties in model checking,” International Journal on Software Tools for Technology Transfer, vol. 20, no. 3, p. 313–325, 2018. [7] M. Chen and P. Mishra, “Functional test generation using efficient property clustering and learning techniques,” IEEE TCAD, vol. 29, no. 3, p. 396–404, 2010. [8] G. Huang et al., “Machine learning for electronic design automation: A survey,” ACM TODAES, vol. 26, no. 5, p. 1–46, 2021. [9] L. Ferretti et al., “Graph neural networks for high-level synthesis design space exploration,” ACM TODAES, vol. 28, no. 2, p. 25:1–25:20, 2023. [10] Z. Shi et al., “Deepgate2: Functionality-aware circuit representation learning,” in ICCAD, p. 1–9, 2023. [11] M. Li et al., “Representation learning of logic circuits,” CoRR, vol. abs/2111.14616, 2021. [12] Y. Ma et al., “High performance graph convolutional networks with applications in testability analysis,” in DAC, 2019. [13] W. Wang et al., “Neuroback: Improving CDCL SAT solving using graph neural networks,” in ICLR, 2024. [14] G. Cabodi and S. Nocco, “Optimized model checking of multiple properties,” in DATE, p. 1–4, 2011. [15] R. Dureja et al., “Boosting verification scalability via structural grouping and semantic partitioning of properties,” in FMCAD, p. 1–9, 2019. [16] R. Dureja et al., “Accelerating parallel verification via complementary property partitioning and strategy exploration,” in Proceedings of Formal Methods in Computer Aided Design, vol. 1, p. 16–25, 2020. [17] S. Das et al., “Purse: Property ordering using runtime statistics for efficient multi - property verification,” in DATE, p. 1–6, 2024. [18] D. Ghosh et al., “Harnessing multiple bmc engines together for efficient formal verification,” in MEMOCODE, p. 71–81, 2023. [19] D. Ghosh et al., “Mab-bmc: A formal verification enhancer by harness- ing multiple bmc engines together,” ACM TODAES, vol. 29, no. 5, 2024. [20] S. G. Roy et al., “Bmc engine sequencing with graph neural network embeddings of hardware circuits,” in VLSID, p. 163–168, 2025. [21] G. Hu et al., “Deepic3: Guiding ic3 algorithms by graph neural network clause prediction,” in ASP-DAC, p. 262–268, 2024. [22] B. L. Synthesis and V. Group, “Abc: A system for sequential synthesis and verification,” 2012. https://people.eecs.berkeley.edu/ ∼ alanmi/abc/. [23] A. Mishchenko et al., “Using speculation for sequential equivalence checking,” in Proceedings of IWLS, p. 139–145, 2012.