GROOT: Graph Edge Re-growth and Partitioning for the Verification of Large Designs in Logic Synthesis

AI summary

Overview

Research area: Machine learning for electronic design automation (EDA), specifically GNN-based verification of large arithmetic circuits in logic synthesis, combined with graph partitioning and custom GPU kernel design.

Technical level: Advanced. The paper assumes familiarity with And-Inverter Graphs, graph neural networks, message passing, sparse matrix multiplication (SpMM), and GPU memory hierarchies.

Scope: A single-GPU algorithm-and-system co-design framework (GROOT) that redesigns circuit node features, partitions large EDA graphs with boundary edge re-growth for accuracy recovery, and introduces two specialized GPU kernels (HD-kernel and LD-kernel), benchmarked against ABC, GAMORA, cuSPARSE, MergePath-SpMM, and GNNAdvisor.

What This Paper Is About

Verifying that a synthesized chip design actually implements its intended function is extremely slow and memory-hungry for large circuits: the paper cites a 2048-bit multiplier taking 8.6×10⁵ seconds (more than nine days) with the open-source tool ABC, and Booth multipliers taking over 100 hours with the OneSpin commercial equivalence checker. GNN-based approaches such as GAMORA cut that to under a second in one reported case, but they ignore EDA domain knowledge in feature design, run out of memory on very large graphs, and rely on multiple GPUs. GROOT's goal is to make large-design verification accurate and memory-feasible on a single GPU by combining circuit-aware features, graph partitioning with edge re-growth, and redesigned GPU kernels.

Key Contributions

1. EDA-domain node feature redesign. The authors build node features from circuit node types (Primary Input, internal AND node, Primary Output) plus the polarity of input edges in And-Inverter Graphs, forming a 4-bit vector per node. They note this contrasts with the three-node features used by GAMORA, and that Primary Inputs and Primary Outputs are not distinguished by GAMORA.

2. Graph partitioning with boundary edge re-growth. They use a graph partitioning algorithm to split large graphs into smaller sub-graphs for GPU processing, then apply a boundary edge re-growth algorithm (Algorithm 1) that identifies boundary nodes, collects crossing edges, and forms augmented node and edge sets to recover verification accuracy.

3. Two redesigned GPU kernels. After profiling EDA graph workloads and observing a polarized distribution of high-degree (HD) and low-degree (LD) nodes, they design an HD-kernel and an LD-kernel, programmed in CUDA C, to fit EDA graph learning on a single GPU.

4. An integrated evaluation of accuracy, memory, and runtime. They compare against ABC, GAMORA, cuSPARSE, MergePath-SpMM, and GNNAdvisor across CSA, Booth, 7nm-mapped, and FPGA 4LUT multiplier datasets, and against large CSA multipliers up to 1,024 bits with batch size 16.

Main Findings

• Memory footprint reduction: GROOT reports a 59.38% reduction in memory footprint for the 1,024-bit CSA multiplier at batch size 16 (134,103,040 nodes and 268,140,544 edges) when partitioned into 64 sub-graphs. Without partitioning, even an NVIDIA A100-SXM with 80 GB cannot perform verification on this graph, whereas GAMORA runs out of memory.
• High accuracy: The abstract reports 99.96% accuracy on the very large 1,024-bit CSA multiplier with batch size 16. Without partitioning, accuracy reaches 100% for multipliers of 128 bits and above on CSA with batch size one, and 99.94% for the 32-bit multiplier.
• Memory scaling in Table II: For batch size 16, GAMORA uses 8,263 MB on 256-bit and 29,375 MB on 512-bit, and goes OOM on 1,024-bit. GROOT with 16, 32, or 64 partitions uses 2,901 MB (256-bit), 7,909 MB (512-bit), and 27,997 MB (1,024-bit).
• Accuracy recovery from edge re-growth: Boundary edge re-growth achieves a maximum recovery of 8.7% accuracy on a 32-bit CSA multiplier and 12.62% on a 32-bit Booth multiplier. On the irregular ASAP 7nm netlist dataset (161 standard cell gates including a multi-output gate), GROOT maintains more than 76% accuracy after edge re-growth.
• Partitioning has little effect up to 16 partitions on very large graphs: For the large CSA multiplier, accuracy stays at 100% up until 16 partitions, attributed to the large number of edges so that removing a small number does not disrupt message passing; a slight drop appears after the 16-partition mark.
• Training on larger designs helps: For FPGA-mapped CSA multipliers, training on an 8-bit multiplier yields low accuracy across datasets; training on a 64-bit multiplier raises 64-bit accuracy from 71.82% (one partition) to 90.8% (one partition), an 18.98% boost. Training a 64-bit FPGA for 100 epochs takes 2914.42 seconds.
• Runtime versus ABC and GAMORA: For 1,024-bit CSA multipliers partitioned into 64 subgraphs, GROOT achieves a speedup of 1.23×10⁵ over ABC. Verification times for partitioned graphs closely align with GAMORA, and GROOT's time slightly increases with more partitions due to partitioning overhead.
• GPU kernel speedups: Against cuSPARSE, MergePath-SpMM, and GNNAdvisor, the abstract reports up to 1.104×, 5.796×, and 1.469× runtime improvement respectively; the introduction lists the MergePath-SpMM figure as 5.872×. In the kernel comparison figure, GROOT-GPU achieves its highest acceleration ratio of 10.28 on the Booth dataset at bit width 512 on the A100, outperforming the second-fastest MergePath-SpMM by 1.67× and the third-fastest cuSPARSE by 1.95×.
• Additional memory savings: Maximum memory reduction of 64.94% for the 1,024-bit multiplier at batch size one with 64 sub-graphs, 41.84% for the 512-bit Booth multiplier, 70.15% for the 768-bit 7nm-mapped multiplier, and 57.62% for the 512-bit FPGA-mapped multiplier.

Methodology in Plain English

The pipeline has five stages. First, a circuit netlist is converted into an And-Inverter Graph (a directed acyclic graph of two-input AND gates and inverters) using ABC. Second, each node gets a 4-bit feature vector: the first two bits encode whether the node is a Primary Input ('00'), an internal AND gate ('11'), or a Primary Output ('0X' inheriting polarity from the preceding internal node); the last two bits encode whether the two input edges are both non-inverted ('00'), exactly one is inverted ('01' or '10'), or both are inverted ('11'). Ground-truth labels come from ABC: Primary Inputs are labeled 4, two-input AND gates 3, XOR nodes 2, MAJ (majority) nodes 1, and Primary Outputs 0.

Third, because large graphs do not fit on a GPU, the graph is partitioned (using METIS) into subgraphs. Partitioning removes edges that cross partition boundaries, which loses information, so Algorithm 1 re-grows them: it finds all nodes one hop outside each partition (boundary nodes), collects the edges crossing between the partition and its boundary, and adds both back to form augmented node and edge sets. The authors observe that EDA graphs contain approximately 10% boundary edges and that this recovery does not add significant complexity to inference.

Fourth, a GraphSAGE model aggregates features and performs message passing over these augmented subgraphs. Fifth, the GNN classifies each node as XOR or MAJ, and those classified nodes are fed into the algebraic re-writing verification technique, where polynomial representations of XOR and MAJ (and their combination) cancel out nonlinear terms. The paper stresses that node classification accuracy directly translates to verification accuracy.

For the GPU side, the authors note that EDA graphs have a polarized degree distribution, with extremely high-degree macro nodes (≥ 512) and low-degree macro nodes (≤ 12). The HD-kernel statically partitions each row's non-zero elements across warps (for example, a block of 64 warps splits each row into 32 equal workloads, assigning row 1 to warps 1–32 and row 2 to warps 33–64). The LD-kernel first sorts rows by degree (achievable in O(n) with count sort), then assigns multiple small-degree rows to the same warp, with 6m warps per block and warps handling 6m, 3m, and 2m rows for degrees 1, 2, and 3, allowing coalesced writes of results to global memory. Experiments run on a Linux host with an AMD EPYC 7543 32-Core Processor and an NVIDIA A100-SXM 80 GB.

Why This Matters

This work targets a well-known bottleneck in the chip design flow. It matters because it shows that verification of very large arithmetic circuits—previously infeasible on a single GPU—can be performed with high accuracy and roughly 59% less memory, using only one GPU rather than the multi-GPU setups prior GNN approaches required, which the authors frame as broadening accessibility to economically disadvantaged districts.

Real-world applications, as listed in the paper:

• Homomorphic encryption, which relies on large integer multipliers.
• Security tasks such as malicious hardware detection.
• Cryptography and financial operations.
• Multimedia and signal processing, plus scientific computing.

Industry relevance: logic synthesis is described as the bridge between high-level synthesis and physical design, and verification is presented as the step that reduces costly errors and time-to-market. The paper uses an open-source tool (ABC) as one baseline and a GNN-based state-of-the-art method (GAMORA) as the other, and reports speedups over commercial-style SpMM kernel baselines (cuSPARSE, MergePath-SpMM, GNNAdvisor), which is the kind of comparison an EDA tool vendor or GPU library developer would use to judge practicality.

Future Directions

• Extending the boundary edge re-growth analysis beyond 16 partitions. The paper observes that memory savings shrink at larger partition counts because re-grown edges consume memory, and that accuracy begins to drop after 16 partitions on large multipliers; the trade-off between partition count, memory, and accuracy remains an open design decision.
• Reducing training time for large designs. Training on a 64-bit FPGA design for 100 epochs takes 2914.42 seconds, and the authors propose specialized kernels for faster matrix multiplication as the mitigation, implying that a more complete solution to training cost is still open.
• Generalizing beyond multipliers. The paper argues that multipliers are the challenging combinational arithmetic case and that performance on them suggests suitability for simpler blocks such as full adders, but broader circuit classes (beyond CSA, Booth, 7nm-mapped, and FPGA 4LUT datasets) are not evaluated.
• Improving accuracy on irregular and FPGA-mapped netlists. FPGA-mapped CSA accuracy is described as low across all datasets before the switch to larger-design training, and the irregular 7nm netlist maintains only above 76% accuracy after edge re-growth, leaving headroom.

Target Audience

Researchers and practitioners working at the intersection of machine learning and electronic design automation: GNN researchers interested in domain-aware graph features and partitioning, EDA engineers working on formal and equivalence verification of arithmetic circuits, and GPU/systems researchers focused on sparse matrix multiplication kernels and single-GPU scaling for graph workloads. It is also relevant to readers tracking the accessibility of AI hardware, since a stated motivation is enabling large-design verification on a single, lower-cost GPU.

Authors’ abstract

Traditional verification methods in chip design are highly time-consuming and computationally demanding, especially for large scale circuits. Graph neural networks (GNNs) have gained popularity as a potential solution to improve verification efficiency. However, there lacks a joint framework that considers all chip design domain knowledge, graph theory, and GPU kernel designs. To address this challenge, we introduce GROOT, an algorithm and system co-design framework that contains chip design domain knowledge and redesigned GPU kernels, to improve verification efficiency. More specifically, we create node features utilizing the circuit node types and the polarity of the connections between the input edges to nodes in And-Inverter Graphs (AIGs). We utilize a graph partitioning algorithm to divide the large graphs into smaller sub-graphs for fast GPU processing and develop a graph edge re-growth algorithm to recover verification accuracy. We carefully profile the EDA graph workloads and observe the uniqueness of their polarized distribution of high degree (HD) nodes and low degree (LD) nodes. We redesign two GPU kernels (HD-kernel and LD-kernel), to fit the EDA graph learning workload on a single GPU. We compare the results with state-of-the-art (SOTA) methods: GAMORA, a GNN-based approach, and the traditional ABC framework. Results show that GROOT achieves a significant reduction in memory footprint (59.38 %), with high accuracy (99.96%) for a very large CSA multiplier, i.e. 1,024 bits with a batch size of 16, which consists of 134,103,040 nodes and 268,140,544 edges. We compare GROOT with GPU-based GPU Kernel designs SOTAs such as cuSPARSE, MergePath-SpMM, and GNNAdvisor. We achieve up to 1.104x, 5.796x, and 1.469x improvement in runtime, respectively.