Source-linked AI summary
Beyond Flat Netlist: Hierarchical Graph Representation Learning for Scalable Analysis of Sequential Circuits
Jingyi Zhou, Zhengyuan Shi, Jiaying Zhu, Ziyang Zheng, Qiang Xu
TL;DR
Circuit representation learning is difficult to deploy on industrial-scale sequential netlists because existing methods lack scalability and explicit register-level temporal modeling. DeepSeq3 uses flip-flop-partitioned combinational subgraphs, a Super-Node Graph, dual GNNs, and state-centric reachability pretraining. Experiments report richer register-level representations, faster pretraining, and an 18% average BMC solving-time reduction while preserving correctness.
Problem
Sequential CRL is challenged by poor scalability on industrial netlists and insufficient explicit modeling of register-level behavior and reachable states.
Method
DeepSeq3 hierarchically encodes flip-flop-partitioned combinational subgraphs and a Super-Node Graph, using dual GNNs and state-centric reachability pretraining.
Results
DeepSeq3 demonstrates improved scalability and richer register-level semantics across downstream tasks, including BMC, with correctness preserved.
Takeaways & Limitations
DeepSeq3 provides a hierarchical representation for sequential circuits that supports scalable analysis and register-level temporal modeling.
Abstract
from arXiv · showhide
Circuit Representation Learning (CRL) offers a powerful paradigm to guide and optimize core Electronic Design Automation (EDA) tasks, but its practical adoption is hindered by the immense scale of industrial netlists and a failure to explicitly model register-level temporal dynamics. To overcome these barriers, we introduce DeepSeq3, a novel hierarchical framework that abstracts circuits into a two-level representation: fine-grained combinational subgraphs partitioned by flip-flops (FFs), and a high-level Super-Node Graph (SNG) that models the register-transfer structure. A dual Graph Neural Network (GNN) architecture learns representations at both levels, capturing local Boolean logic and global state transitions. Crucially, we introduce a state-centric pre-training scheme that predicts the reachability between FF states, endowing the model with a deep understanding of temporal behavior. Demonstrated on large-scale benchmarks, DeepSeq3's approach yields superior scalability and richer representations, reducing bounded model checking (BMC) solving time by 18% while guaranteeing correctness.
1 Introduction
DeepSeq3 addresses sequential CRL’s scalability and register-level temporal-modeling challenges with a hierarchical representation and state-centric pretraining. The framework targets downstream EDA tasks, including BMC, while preserving correctness.
- Motivation: Sequential CRL remains limited by flat graph processing that cannot scale effectively to industrial netlists with millions or billions of gates and wires.Prior models struggle with designs exceeding 10K gates because of memory ceilings, over-squashing, and oversized neighborhoods.
- Motivation: Gate-centric models mix flip-flops with combinational logic, weakening register semantics and under-representing when and how state transitions occur.Without explicit register-level abstraction, models emphasize local Boolean structure over reachable-state behavior.
- DeepSeq3 Framework: DeepSeq3 partitions circuits at flip-flop boundaries, encodes combinational subgraphs, and assembles their embeddings into a Super-Node Graph processed by a second GNN.This abstraction compresses local combinational information while making register-level structure explicit.
- DeepSeq3 Framework: State-centric pretraining predicts reachable flip-flop states, providing supervision for temporal semantics in the hierarchical representation.The pretraining task targets register-level reachability and successor-state behavior.
- Evaluation: DeepSeq3 is evaluated on gate-level dynamic power estimation and register-level BMC, with reported scalability and register-level semantic improvements over prior approaches.The BMC deployment is described as reducing solving time while preserving correctness.
- Evaluation: 18% average BMC solving-time reduction is reported on HWMCC benchmarks after deploying DeepSeq3 as a plug-in to the BMC engine.The contribution summary reports this average speedup for Hardware Model Checking Competition benchmarks.
2 Related Work
CRL has developed strong graph-based methods for combinational circuits, while sequential-circuit learning and BMC acceleration remain constrained by limited global and reachable-state modeling. Recent approaches motivate explicit structural and temporal representations.
- Combinational CRL: CRL represents netlists as graphs to encode complex circuit information into low-dimensional vectors for downstream EDA tasks.The cited examples emphasize the graph-structured nature of netlists and their use in circuit analysis.
- Combinational CRL: Combinational-circuit methods improve Boolean and structural representations through attention, skip connections, truth-table supervision, functionality-aware losses, and contrastive learning.Examples include DeepGate, DeepGate2, and FGNN across test point insertion, SAT, classification, and subgraph localization.
- Sequential CRL: DeepSeq and DeepSeq2 model sequential circuits through flip-flops, combinational logic, unrolling, and sequential message passing, but lack explicit graph-level modeling of global connectivity.This limits their ability to capture long-range dependencies according to the related-work passage.
- Bounded Model Checking: BMC unrolls sequential circuits across bounded time frames and encodes reachability as SAT, offering efficient bug detection but potentially incurring prohibitive temporal overhead on large industrial designs.The method detects property violations without constructing a complete symbolic model.
- Bounded Model Checking: Prior BMC acceleration methods lack prior knowledge of reachable states and therefore rely on default heuristics for state-space exploration.The related-work passage identifies reachable-state guidance as a missing capability in previous approaches.
3 Methodology
DeepSeq3 builds sequential-circuit representations hierarchically, encoding partitioned combinational subgraphs and then modeling their register-level dependencies in an SNG. Transition-probability and reachability supervision supplies temporal information for global state modeling.
- Hierarchical representation: DeepSeq3 decouples combinational logic from flip-flops, learning subgraph representations before assembling a super-node graph for the full circuit.The two-stage framework applies one GNN within partitioned subgraphs and another on the SNG.
- Combinational logic subgraph learning: A layer-wise GNN learns each combinational subgraph’s functional representation using gate-type features and logic-0 and logic-1 supervision.Inverter messages use the opposite predecessor state, while AND-gate messages aggregate corresponding predecessor states.
- SNG construction: Each SNG super-node represents a combinational logic block between registers, while directed super-edges encode FF-to-FF driving relationships.The resulting graph captures high-order dependencies and approximates state propagation across clock cycles.
- Sequential modeling: The circuit is modeled as a finite-state system whose state vector contains FF and output values, with temporal evolution represented by a transition-probability matrix P.The state space has cardinality |S| = 2^(n+m), and P characterizes transitions between circuit states.
- Sequential modeling: The infinite-step reachability matrix A∞ complements P by indicating whether one state can reach another over any number of time steps.Together, P and A∞ supervise both local transitions and the global organization of circuit dynamics.
- Scalable temporal supervision: For large circuits, transition supervision samples states from simulation traces and records observed transitions, while reachable regions are sampled to avoid global state explosion.Small- and medium-scale circuits can instead use full transition matrices and Floyd-Warshall transitive closure.
4 Experiments
DeepSeq3 is evaluated on pre-training, dynamic power estimation, and BMC, with results showing stronger register-level representation, faster pre-training, improved power prediction, and faster guided verification.
- 4.2 Model Pre-training Results: DeepSeq3 achieves R2 values of 0.9869 and 0.9916 for logic-1 and logic-0 probability prediction, respectively.The corresponding MAE values are 0.01936 and 0.01687.
- 4.2 Model Pre-training Results: DeepSeq3 substantially outperforms DeepSeq2 on register-level tasks, reaching IR F1 of 0.8429 and OT R of 0.8413.DeepSeq2 achieves 0.3048 on IR F1 and 0.2922 on OT R.
- 4.2 Model Pre-training Results: Removing Stage1 reduces IR F1 to 0.7752, while removing IR or OT supervision creates a trade-off between OT R and IR F1.Without IR, OT R reaches 0.8695 but IR F1 drops to 0.0341; without OT, IR F1 remains 0.8249 while OT R declines to 0.6442.
- 4.2 Model Pre-training Results: DeepSeq3 reduces total pre-training cost to 9896 seconds from DeepSeq2’s 40486 seconds, an approximate four-fold acceleration.The reported efficiency is attributed to parallelizable FF-boundary feature extraction and SNG graph compression.
- 4.3 Evaluation on Dynamic Power Prediction: DeepSeq3 achieves 4.58% average MAPE and 6.64% error standard deviation for dynamic power estimation, compared with DeepSeq2’s 7.49% standard deviation.The reported average MAPE corresponds to an approximate 38.4% improvement in relative accuracy.
- 4.4 Evaluation on Bounded Model Checking: Guided BMC achieves 18.6% average speedup on 31 easy instances and averages 191.11 seconds on nine hard cases versus 255.03 seconds for Raw BMC.The hard-case evaluation also reports successful solutions for instances on which Raw BMC times out; model inference time is excluded from the easy-instance speedup.
5 Conclusion and Future Work
DeepSeq3 addresses sequential CRL’s scalability and temporal-modeling challenges by partitioning circuits along FF boundaries into an SNG and applying state-centric pretraining. Experiments support its advantages for scalable, semantic-rich sequential analysis.
- 5 Conclusion and Future Work: DeepSeq3 partitions circuits along FF boundaries into a Super-Node Graph and uses state-centric pretraining to capture register-level semantics at scale.The framework targets limited scalability and insufficient temporal modeling in sequential CRL.
- 5 Conclusion and Future Work: Experiments confirm DeepSeq3’s advantages and establish a foundation for semantic-rich sequential analysis in industrial settings.
- 5 Conclusion and Future Work: Future work may use DeepSeq3’s temporal representations for retiming, state encoding, and advanced formal verification.