H3Match: A Hybrid Heterogeneous Hypergraph Matching Method for Subcircuit Identification

Subcircuit matching is widely applied in logic synthesis, design verification, hardware security, etc. Previous works employ redundant circuit representations, coupled with timeconsuming enumerative search methods. Subsequent works use a hybrid “approximate filtering - exact verification” framework, but the numerous false negatives predicted by the graph neural network (GNN) based filtering lead to severe matching failure. In this paper, an improved hybrid method named H3Match is proposed to achieve a better tradeoff between runtime, accuracy, and false negative rate. First, we model the circuits as hypergraphs to fully capture the topology and construct diverse heterogeneous hyperedge features to facilitate the learning of circuit topologies. Second, to reduce the false negatives, we reformulate the subgraph matching problem as matching directed acyclic graphs (DAGs) with embedded circular structure information and develop a directed GNN-based approximate matching approach to identify potential matching subcircuits. Finally, we propose a general mixed integer nonlinear programming (MINLP) formulation for exact verification, with convergency speed accelerated by extracting the initial solution from the results in approximate matching. Experimental results show that our approximate method outperforms state-of-the-art (SOTA) methods by 4.31% in accuracy while achieving virtually zero false negatives. Our exact verification is on average $4.16 \times$ faster than SOTA exact methods. Overall, the end-to-end flow achieves a $7.08 \times$ speedup compared to existing approaches.