quantum computing

With quantum computers promising advantages even in the near-term NISQ era, there is a lively community that develops software and toolkits for the design of corresponding quantum circuits. Although the underlying problems are different, expertise from the design automation community, which developed sophisticated design solutions for the conventional realm in the past decades, can help here. In this respect, decision diagrams provide a promising foundation for tackling many design tasks such as simulation, synthesis, and verification of quantum circuits. 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 this work, we first review the concepts of how decision diagrams can be employed, e.g., for the simulation and verification of quantum circuits. Afterwards, in an effort to make decision diagrams for quantum computing more accessible, we then present a visualization …

Quantum computing is gaining serious momentum in these days. With increasing capabilities of corresponding devices also comes the need for efficient and automated tools to design them. Verification, i.e., ensuring that the originally intended functionality of a quantum algorithm/circuit is preserved throughout all layers of abstraction during the design process, is a vital part of the quantum software stack. In this work, we present QCEC, a tool for quantum circuit equivalence checking which is part of the JKQ toolset for quantum computing. By exploiting characteristics unique to quantum computing, the tool allows users to efficiently verify the equivalence of two quantum circuits using a variety of methods and strategies.

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 …

Verification of quantum circuits is essential for guaranteeing correctness of quantum algorithms and/or quantum descriptions across various levels of abstraction. In this work, we show that there are promising ways to check the correctness of quantum circuits using simulative verification and random stimuli. To this end, we investigate how to properly generate stimuli for efficiently checking the correctness of a quantum circuit. More precisely, we introduce, illustrate, and analyze three schemes for quantum stimuli generation—offering a trade-off between the error detection rate (as well as the required number of stimuli) and efficiency. In contrast to the verification in the classical realm, we show (both, theoretically and empirically) that even if only a few randomly-chosen stimuli (generated from the proposed schemes) are considered, high error detection rates can be achieved for quantum circuits. The results of these conceptual and theoretical considerations have also been empirically confirmed—with a …

With quantum computers on the brink of practical applicability, there is a lively community that develops toolkits for the design of corresponding quantum circuits. Many of the problems to be tackled here are similar to design problems from the classical realm for which sophisticated design automation tools have been developed in the previous decades. In this paper, we present JKQ—a set of tools for quantum computing developed at the Johannes Kepler University (JKU) Linz which utilizes this design automation expertise. By this, we offer complementary approaches for many design problems in quantum computing such as simulation, compilation, or verification. In the following, we provide an introduction of the tools for potential users who would like to work with them as well as potential developers aiming to extend them.

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 …

High-level descriptions of quantum algorithms do not take the restrictions of physical hardware into account. Therefore actually executing an algorithm in the form of a quantum circuit on a quantum computer requires compiling it for the desired target architecture first. The compilation of quantum circuits depends on efficient methods to be feasible for all but the trivial instances. To this end, different compiling methods have been introduced in the past, but room for improvement still exists. Moreover, just an efficient compilation process itself is not sufficient—the resulting circuits must be correct as well. In this summary paper, we review how existing compilation approaches can be optimized by utilizing heuristic search algorithms or exact reasoning engines. Furthermore, we review how the correctness of the obtained results can be verified afterwards by clever data structures such as decision diagrams. This illustrates core steps of a compilation flow which can generate minimal or close-to-minimal …

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.

The rapid rate of progress in the physical realization of quantum computers sparked the development of elaborate design flows for quantum computations on such devices. Each stage of these flows comes with its own representation of the intended functionality. Ensuring that each design step preserves this intended functionality is of utmost importance. However, existing solutions for equivalence checking of quantum computations heavily struggle with the complexity of the underlying problem and, thus, no conclusions on the equivalence may be reached with reasonable efforts in many cases. In this work, we uncover the power of simulation for equivalence checking in quantum computing. We show that, in contrast to classical computing, it is in general not necessary to compare the complete representation of the respective computations. Even small errors frequently affect the entire representation and, thus, can be detected within a couple of simulations. The resulting equivalence checking flow substantially improves …