Binary Decision Diagrams (BDDs) are instrumental in many electronic design automation (EDA) tasks thanks to their compact representation of Boolean functions. In BDD‑based reversible‑circuit synthesis, which is critical for quantum computing, the chosen variable ordering governs the number of BDD nodes and thus the key metrics of resource consumption, such as Quantum Cost. Because finding an optimal variable ordering for BDDs is an NP‑complete problem, existing heuristics often degrade as circuit complexity grows. We introduce BDD2Seq, a graph‑to‑sequence framework that couples a Graph Neural Network encoder with a Pointer‑Network decoder and Diverse Beam Search to predict high‑quality orderings. By treating the circuit netlist as a graph, BDD2Seq learns structural dependencies that conventional heuristics overlooked, yielding smaller BDDs and faster synthesis. Extensive experiments on three public benchmarks show that BDD2Seq achieves around 1.4 times lower Quantum Cost and 3.7 times faster synthesis than modern heuristic algorithms. To the best of our knowledge, this is the first work to tackle the variable‑ordering problem in BDD‑based reversible‑circuit synthesis with a graph‑based generative model and diversity‑promoting decoding.

Abstract The IC3 algorithm represents the state-of-the-art (SOTA) hardware model checking technique, owing to its robust performance and scalability. A significant body of research has focused on enhancing the solving efficiency of the IC3 algorithm, with particular attention to the inductive generalization process—a critical phase wherein the algorithm seeks to generalize a counterexample to inductiveness (CTI), which typically is a state leading to a bad state, into a broader set of states. This inductive generalization is a primary source of clauses in IC3 and thus plays a pivotal role in determining the overall effectiveness of the algorithm. Despite its importance, existing approaches often rely on fixed inductive generalization strategies, overlooking the dynamic and context-sensitive nature of the verification environment in which spurious counterexamples arise. This rigidity can limit the quality of generated clauses and, consequently, the performance of IC3. To address this limitation, we propose a lightweight machine-learning-based framework that dynamically selects appropriate inductive generalization strategies in response to the evolving verification context. Specifically, we employ a multi-armed bandit (MAB) algorithm to adaptively choose inductive generalization strategies based on real-time feedback from the verification process. The agent is updated by evaluating the quality of generalization outcomes, thereby refining its strategy selection over time. Empirical evaluation on a benchmark suite comprising 914 instances, primarily drawn from the latest HWMCC collection, demonstrates the efficacy of our approach. When implemented on the state-of-the-art model checker rIC3, our method solves 26 to 50 more cases than the baselines and improves the PAR-2 score by 194.72 to 389.29.

Majority-Inverter Graph (MIG) emerges as a promising data structure for logic optimization and synthesis, offering a more compact representation for logic functions compared to traditional AND/OR-Inverter graphs. Consequently, the MIG finds widespread application in digital circuit design, particularly in quantum circuits and superconducting adiabatic quantum-flux-parametron logic circuits. Currently, logic optimization techniques for MIG mainly fall into two categories: (i) logic rewriting with predefined more compact sub-structures and (ii) logic resubstitution with already existing logic in the Boolean network. However, the inherent complexity of MIG logic and the limitation imposed by the input scale of sub-structures significantly impact the performance of these methods. To address these challenges, this paper proposes eLogic, a novel depth-oriented MIG logic rewriting framework using e-graphs, to minimize the depth and size of MIG. The eLogic utilizes the e-graphs, a data structure for efficient computation with equalities between terms, to minimize the depth and size of the cone delimited by the cut. The experimental results on the EPFL benchmark demonstrate the effectiveness of eLogic. It is noteworthy that eLogic is open-sourced on https://github.com/Flians/eLogic.

Modern circuit design process increasingly adopts high-level hardware construction languages and parameterized design methodologies to shorten development cycles and maintain high reusability, in contrast to traditional hardware description languages. Such designs often involve complex datapath with arithmetic operations, wide bit-vectors, and on-chip memories, whose scale and level of modeling often pose significant challenges to formal datapath verification. Traditional bit-level SAT sweeping techniques lack the necessary abstraction and adaptability that are required to establish equivalence at a higher level. In this paper, we propose FORWORD, a novel word-level sweeping verification engine tailored explicitly to formal datapath verification. FORWORD integrates randomized and constraint-driven word-level simulations, leveraging adaptive optimization to dynamically refine equivalent candidates identified during simulation. Experimental results demonstrate that FORWORD significantly outperforms state-of-the-art bit-level SAT sweeping engines and the monolithic SMT solving method, thanks to its enhanced capability in effectively identifying equivalent pairs. To the best of our knowledge, FORWORD is the first word-level sweeping engine explicitly designed for datapath verification, offering improved efficiency and adaptability to modern circuit designs.

Formal verification of HLS-generated RTL often suffers from poor scalability due to large state spaces and complex control structures. We present AutoINV, a framework that generates and prioritizes helper assertions from HLS-specific design features to guide IC3/PDR. Experiments on diverse HLS benchmarks show that AutoINV accelerates verification over vanilla model checking and enables proving more challenging cases that vanilla IC3/PDR cannot finish within the timeout.

In technology mapping, the quality of the final implementation heavily relies on the circuit structure after technologyindependent optimization. Recent studies have introduced equality saturation as a novel optimization approach. However, its efficiency remains a hurdle against its wide adoption in logic synthesis. This paper proposes a highly scalable and efficient framework named E-morphic. It is the first work that employs equality saturation for resynthesis after conventional technology-independent logic optimizations, enabling structure exploration before technology mapping. Powered by several key enhancements to the equality saturation framework, such as direct e-graph-circuit conversion, solution-space pruning, and simulated annealing for e-graph extraction, this approach not only improves the scalability and extraction efficiency of e-graph rewriting but also addresses the structural bias issue present in conventional logic synthesis flows through parallel structural exploration and resynthesis. Experiments show that, compared to the state-of-the-art delay optimization flow in ABC, E-morphic on average achieves 12.54% area saving and 7.29% delay reduction on the large-scale circuits in the EPFL benchmark.

Functional verification is critical in ensuring the correctness of register transfer level (RTL) models. Formal methods, such as model checkers, are powerful tools that help achieve high coverage in functional validation by transforming the coverage problem into property verification tasks. However, these methods typically demand significant memory usage and long verification times. One major issue is that the satisfiability problem for each unsolved property always starts from the reset state of a design, leading to repeated solving of the same subset of clauses across different properties. In this paper, we propose an open-source semi-formal framework based on model checkers that accelerates test stimulus generation through two techniques: assertion ordering and strategic selection of starting states. These techniques enable model checkers to intelligently select starting states that are much closer to the final state, thereby reducing unnecessary computations. Through comprehensive experiments on ITC'99 benchmarks and modern complex processor designs, including OpenCores 1200 and Rocket-Chip, we demonstrate that our proposed techniques can achieve higher coverage with less than half of the test generation time.

In recent years, machine learning has demonstrated its potential in many challenging problems. In this paper, we extend its use to hardware formal property verification and propose DeepIC3, a method that takes advantage of graph learning in the classic IC3/PDR algorithm. In DeepIC3, graph neural networks are integrated to improve the result of local inductive generalization. This helps provide a global view of the state transition system and can potentially lead the algorithm out of local optima in the search of inductive invariants. Our experiments demonstrate that DeepIC3 accelerates the vanilla algorithm in nontrivial test cases of hardware model checking competition benchmarks (HWMCC2020) with up to 10. 8x speed-up. The proposed machine-learning integration preserves soundness and is universally applicable to various IC3/PDR implementations.

Logic synthesis plays a crucial role in the digital design flow. It has a decisive influence on the final Quality of Results (QoR) of the circuit implementations. However, existing multi-level logic optimization algorithms often employ greedy approaches with a series of local optimization steps. Each step breaks the circuit into small pieces (e.g.,k-feasible cuts) and applies incremental changes to individual pieces separately. These local optimization steps could limit the exploration space and may miss opportunities for significant improvements. To address the limitation, this paper proposes using e-graph in logic synthesis. The new workflow, named E-Syn, makes use of the well-established e-graph infrastructure to efficiently perform logic rewriting. It explores a diverse set of equivalent Boolean representations while allowing technology-aware cost functions to better support delay-oriented and area-oriented logic synthesis. Experiments over a wide range of benchmark designs show our proposed logic optimization approach reaches a wider design space compared to the commonly used AIG-based logic synthesis flow. It achieves on average 15.29% delay saving in delay-oriented synthesis and 6.42% area saving for area-oriented synthesis.

The introduction of satellite Internet resource-slicing technology can efficiently allocate satellite network resources and meet the personalized needs of different users. This article proposes a trust-based satellite Internet resource-slicing access authentication scheme, which solves the efficient and secure access requirements in situations where satellite communication and service resources are relatively limited. The working idea of this article is to provide users with access authentication protocols with different efficiencies through trust as a standard. Firstly, The user’s trust value is calculated by establishing a trust metric model based on Beta function, communication byte fluctuations, and centralized trend measurements. Drawing on the requirements of the security policy function in the resource slicing technology standard, assigning different security policies to users can both improve the fast access ability of high-trust users and reduce the priority of low trust users’ access. After that, based on the results of trust metrics, this paper proposes a two-factor-based no certificate satellite Internet slicing access authentication protocol for users with moderate trust levels. This protocol achieves the ability for users to access slicing services anonymously and efficiently through the use of resource-slicing credentials and managers. Final, this article verify the correctness and security of the protocol. Through communication cost comparison, it is shown that this protocol has fewer costs. Through trust simulation, the effectiveness of the trust scheme is analyzed and compared.

Refinement checking is an important formal verification method that checks if a hardware implementation complies with (in other words, refines) a given specification. It has been widely used in processor and nonprocessor verification. In refinement checking, a refinement mapping is needed to relate the implementation and the specification. Despite the wide adoption of refinement checking, there is currently no general format or standard for the mapping—most prior works employed a certain property specification language (e.g., the SystemVerilog assertion) to write ad-hoc properties that describe the mapping relation. These manually written properties are usually not well structured and are often difficult to design or understand. In this article, we present${\tt r{-}map}$, a language for refinement mapping.${\tt r{-}map}$relates the implementation and the specification in a more concise and comprehensible way. We evaluate${\tt r{-}map}$in the refinement checking of practical hardware designs. In our case study,${\tt r{-}map}$shows a significant reduction of human efforts compared to manually writing refinement properties. We also show how${\tt r{-}map}$can help to scale up formal verification.

Smart grid is the intelligent power grid, in which Scheduling system is the most important part. In this paper, we will introduce a new schedule system based on contract net protocol improved scheduling efficiency. As one of the most important coordination mechanism, contract net protocol (CNP) has been extensively studied in many areas, and many other techniques can also be used to improve the quality of decision. The new CNP is based on trust mechanism, that makes the system more efficient scheduling. Experimental results show that the initiators with trust model almost steadily get the best participants no matter the environment is honest-dominated or dishonest-dominated. Even in the dishonest-dominated environment, this approach gets better results and is proved valuable.

Data traversing packet networks experience varying delays, resulting in noticeable delay jitters. This significantly degrades overall system performance in a real-time multimedia network. This paper proposes TSJC, a novel traffic shaping algorithm with delay jitter constraints for real-time multimedia networks, on the basis of traditional shaping algorithms and their traffic characteristics. TSJC computes the queuing delay and queuing delay variation on line by monitoring the token bucket states, such as the queue length and token arrival rate. TSJC adaptively configures system parameters based on the queuing delay and time jitter, to provide universally low jitter outputs. Simulations have shown that TSJC can both smooth traffic fluctuation and decrease the delay jitter.