decision diagrams

With the emergence of more and more applications for quantum computing, also the development of corresponding methods for design automation is receiving increasing interest. In this respect, decision diagrams provide a promising basis for many design tasks such as simulation, synthesis, verification, and more. However, users of the corresponding tools often do not have a proper background or an intuition about how these methods based on decision diagrams work and what their strengths and limits are. In an effort to make decision diagrams for quantum computing more accessible, we present a visualization tool which visualizes quantum decision diagrams and allows to explore their behavior when used in the design tasks mentioned above. The installation-free web-tool allows users to interactively learn how decision diagrams can be used in quantum computing, e.g., to (1) compactly represent quantum states and the functionality of quantum circuits, (2) to efficiently simulate quantum circuits, and (3) to verify the …

In the not-so-distant future, quantum computing will change the way we tackle certain problems. It promises to dramatically speed-up many chemical, financial, cryptographical, and machine-learning applications. However, in order to capitalize on those promises, complex design flows composed of steps such as compilation, decomposition, mapping, or transpilation need to be employed before being able to execute a conceptual quantum algorithm on an actual device. This results in many descriptions at various levels of abstraction which may significantly differ from each other. The complexity of the underlying design problems makes it ever more important to not only provide efficient solutions for the single steps, but also to verify that the originally intended functionality is preserved throughout all levels of abstraction. This motivates methods for equivalence checking of quantum circuits. However, most existing methods for this are inspired by equivalence checking in the classical realm and have merely been …

Realizing a conceptual quantum algorithm on an actual physical device necessitates the algorithm’s quantum circuit description to undergo certain transformations in order to adhere to all constraints imposed by the hardware. In this regard, the individual high-level circuit components are first synthesized to the supported low-level gate-set of the quantum computer, before being mapped to the target’s architecture—utilizing several optimizations in order to improve the compilation result. Specialized tools for this complex task exist, e.g., IBM’s Qiskit, Google’s Cirq, Microsoft’s QDK, or Rigetti’s Forest. However, to date, the circuits resulting from these tools are hardly verified, which is mainly due to the immense complexity of checking if two quantum circuits indeed realize the same functionality. In this paper, we propose an efficient scheme for quantum circuit equivalence checking—specialized for verifying results of the IBM Qiskit quantum circuit …

Despite the recent progress in the physical implementation of quantum computers, a significant amount of research still depends on the use of quantum circuit simulators running on classical hardware. While there are several techniques for quantum circuit simulation, many state-of-the-art simulators rely on an array-based simulation approach. However, this array-based approach has exponential memory complexity with respect to the number of simulated qubits. To address this drawback, complementary approaches based on decision diagrams have been proposed. While these approaches allow simulating circuits that could not be simulated before, they come with their own drawbacks. Unfortunately, no detailed case study has been conducted to date, which compares those complementary approaches and their respective strengths and weaknesses. In this work, we are addressing this by providing a survey on both approaches as well as a detailed case study on their respective performances.

Abstract—Quantum computing is gaining considerable momentum through the recent progress in physical realizations of quantum computers. This led to rather sophisticated design flows in which the originally specified quantum functionality is compiled through different abstractions. This increasingly raises the question whether the respectively resulting quantum circuits indeed realize the originally intended function. Accordingly, efficient methods for equivalence checking are gaining importance. However, existing solutions still suffer from significant shortcomings such as their exponential worst case performance and an increased effort to obtain counterexamples in case of non-equivalence. In this work, we propose an improved DD-based equivalence checking approach which addresses these shortcomings. To this end, we utilize decision diagrams and exploit the fact that quantum operations are inherently reversible – allowing for dedicated strategies that keep the overhead moderate in many cases. Experimental …