In the field of Electronic Design Automation (EDA), managing circuit complexity is a crucial task for efficient circuit verification, testing, and optimization. Increasing design complexity presents challenges for tasks such as formal verification, fault detection, and circuit optimization. Therefore, reducing circuit complexity becomes crucial in improving the efficiency and scalability of these tasks. These circuits are typically represented as graphs. In the field of parameterized complexity, CutWidth (CW) and TreeWidth (TW) are well-studied decomposition techniques that have been used in analyzing graph algorithms. In this paper, we introduce the TW decomposition technique to the field of EDA for the first time and demonstrate its impact on reducing the circuit complexity of circuits. Additionally, we present a new decomposition technique that combines both decompositions, resulting in a further reduction in circuit complexity. Furthermore, we present experimental results comparing complexity upper bounds from various decompositions to highlight the efficacy of our approach on the ISCAS’85 and EPFL benchmark circuits. Our results show that our decomposition technique outperforms the complexity upper bounds of CW by 90.16× and the complexity upper bounds of TW by 9.34× for the ISCAS’85 benchmarks. Additionally, it outperforms the complexity upper bounds of CW by 1986.37× and the complexity upper bounds of TW by 94.13× for the EPFL benchmarks. Finally, to demonstrate the applicability of the decomposition techniques in solving various EDA problems, we propose a new Formal Verification (FV) approach that leverages these techniques to provide an upper bound for the verification process. We also conduct an experimental evaluation on the ITC’99 , MCNC’91 , and VHDL Library of Arithmetic Units ( ELAU ) benchmark circuits, adder circuits of various sizes (up to 3072-bit width), and Genmul multipliers of different sizes (up to 10×10), to demonstrate the scalability of our approach.

The hardware complexity in electronic devices has increased significantly in recent decades due to technological advancements. To ensure correct behavior of such devices and meet time-to-market constraints, modern circuit verification and testing tools rely on formal proof techniques. The two most popular methods in this context are Binary Decision Diagrams (BDDs) and Boolean Satisfiability (SAT) solvers. Even though these methods share some similarities, they are fundamentally different. Whereas BDDs usually require a large amount of memory to represent all solutions, SAT solvers are memory-efficient but they typically compute only a single solution. To tackle these issues, a hybrid approach called Binary Hybrid Diagram (BHD) is proposed for efficient generation of multiple solutions. BHDs combine the major advantages of BDDs and SAT solvers, and generate distinct solutions heuristically via algorithms. Experiments demonstrate that feasible solutions are generated rapidly by using BHDs while the memory requirement remains small compared to state-of-the-art methods.

As hardware designs are getting more complex, verification becomes ever more important to prevent producing chips which do not behave according to their specification. This increasing complexity also impacts the verification process, resulting in a longer time-to-market. Ensuring that the verification itself can be conducted efficiently helps facing these challenges. Additionally, taking the efficient verification into consideration during the design phase further enables the optimization of the whole process. In this paper, we present a SAT-based verification flow and how it can ensure polynomial bounds for the verification of circuits with limited cutwidth. To demonstrate our approach, the flow is applied to three different adder architectures. Addition is one of the most essential operations in digital computations and the simplicity of its circuit realizations makes it a good starting point to explore their efficient verification using SAT. We provide theoretical proofs that SAT can be used for Polynomial Formal Verification (PFV) of circuits with limited cutwidth. We then show that for the considered adder circuits, a linear time complexity of the verification process can be ensured and confirm our findings by experimental evaluation with our own SAT solver.

Quantum computers offer enormous speed advantages over their classical counterparts. Still, optimization on quantum circuits is necessary to further increase their potential. Additionally, physical realizations of quantum computers place restrictions on quantum circuits, regarding the available quantum gates. In order to satisfy these restrictions, non-native gates need to be expressed as an equivalent cascade of natively available quantum gates which induces a mapping overhead. Two complementary approaches to this problem are to move around the qubits (using SWAP gates) or to apply so-called remote gates, i.e. pre-computed cascades of native gates which keep the qubit placement.In this paper, we explore how combinations of movements and remote gates can be employed to reduce the required overhead regarding the number of native gates as well as the circuit depth. We also discuss ways to find out which qubits to address with the movements in order to optimize these metrics. Our general evaluation is supplemented by evaluations on two IBM quantum computer architectures to show how quantum circuits can be optimized by the presented patterns.