Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2009.02376 · IEEE International Conference on Quantum Computing and Engineering (QCE)

Verifying Results of the IBM Qiskit Quantum Circuit Compilation Flow

Lukas Burgholzer, Rudy Raymond, Robert Wille

Published Oct 1, 2020• 60 citations
arXivHTMLPDF

Abstract

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 compilation flow. To this end, we combine characteristics unique to quantum computing, e.g., its inherent reversibility, and certain knowledge about the compilation flow into a dedicated equivalence checking strategy. Experimental evaluations confirm that the proposed scheme allows to verify even large circuit instances with tens of thousands of operations within seconds or even less, whereas state-of-the-art techniques frequently time-out or require substantially more runtime. A corresponding open source implementation of the proposed method is publicly available at https://github.com/iic-jku/qcec.

DOI
10.1109/qce49297.2020.00051

Related papers

Advanced Equivalence Checking for Quantum Circuits

Lukas Burgholzer, Robert Wille

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 extended to support quantum circuits (i.e., circuits which do not only rely on 0's and 1's but also employ superposition and entanglement). In this work, we propose an advanced methodology that takes the different paradigms of quantum circuits not only as a burden but as an opportunity. In fact, the proposed methodology explicitly utilizes characteristics unique to quantum computing in order to overcome the shortcomings of existing approaches. We show that by exploiting the reversibility of quantum circuits, complexity can be kept feasible in many cases. Moreover, we show that, in contrast to the classical realm, simulation is very powerful in verifying quantum circuits. Experimental evaluations confirm that the resulting methodology allows one to conduct equivalence checking dramatically faster than ever before-in many cases just a single simulation run is sufficient. An implementation of the proposed equivalence checking flow is publicly available at https://iic.jku.at/eda/research/quantum_verification/.

arXiv:2004.08420•Springer eBooks•Oct 21, 2020•112 citations

Equivalence Checking of Quantum Circuits With the ZX-Calculus

Tom Peham, Lukas Burgholzer, Robert Wille

As state-of-the-art quantum computers are capable of running increasingly complex algorithms, the need for automated methods to design and test potential applications rises. Equivalence checking of quantum circuits is an important, yet hardly automated, task in the development of the quantum software stack. Recently, new methods have been proposed that tackle this problem from widely different perspectives. One of them is based on the ZX-calculus, a graphical rewriting system for quantum computing. However, the power and capability of this equivalence checking method has barely been explored. The aim of this work is to evaluate the ZX-calculus as a tool for equivalence checking of quantum circuits. To this end, it is demonstrated how the ZX-calculus based approach for equivalence checking can be expanded in order to verify the results of compilation flows and optimizations on quantum circuits. It is also shown that the ZX-calculus based method is not complete—especially for quantum circuits with ancillary qubits. In order to properly evaluate the proposed method, we conduct a detailed case study by comparing it to two other state-of-the-art methods for equivalence checking: one based on path-sums and another based on decision diagrams. The proposed methods have been integrated into the publicly available QCEC tool (https://github.com/cda-tum/qcec) which is part of the Munich Quantum Toolkit (MQT).

arXiv:2208.12820•IEEE Journal on Emerging and Selected Topics in Circuits and Systems•Aug 26, 2022•46 citations

Compiling SU(4) quantum circuits to IBM QX architectures

Alwin Zulehner, Robert Wille

The Noisy Intermediate-Scale Quantum (NISQ) technology is currently investigated by major players in the field to build the first practically useful quantum computer. IBM QX architectures are the first ones which are already publicly available today. However, in order to use them, the respective quantum circuits have to be compiled for the respectively used target architecture. While first approaches have been proposed for this purpose, they are infeasible for a certain set of SU(4) quantum circuits which have recently been introduced to benchmark corresponding compilers. In this work, we analyze the bottlenecks of existing compilers and provide a dedicated method for compiling this kind of circuits to IBM QX architectures. Our experimental evaluation (using tools provided by IBM) shows that the proposed approach significantly outperforms IBM's own solution regarding fidelity of the compiled circuit as well as runtime. Moreover, the solution proposed in this work has been declared winner of the IBM QISKit Developer Challenge. An implementation of the proposed methodology is publicly available at http://iic.jku.at/eda/research/ibm_qx_mapping.

arXiv:1808.05661•Asia and South Pacific Design Automation Conference (ASP-DAC)•Jan 18, 2019•100 citations

Quantum Circuit Equivalence Checking: A Tractable Bridge From Unitary to Hybrid Circuits

Jérome Ricciardi, Sébastien Bardin, Christophe Chareton +1 more

Equivalence checking of hybrid quantum circuits is of primary importance, given that quantum circuit transformations are omnipresent along the quantum compiler chain. While some approaches exist for automating this task, most focus on the simple case of unitary circuits. At the same time, real quantum computing requires hybrid circuits equipped with measurement operators. Moreover, the few approaches targeting the hybrid case are limited to a restricted class of problems. We propose tackling the Quantum Hybrid Circuit Equivalence Checking problem through lifting unitary circuit verification using a transformation known as deferred measurement. We show that this approach alone significantly outperforms prior work, and that, with the addition of specific unitary-level techniques we call separation and projection, it can handle much larger classes of hybrid circuit equivalence problems. We have implemented and evaluated our method over standard circuit transformations such as teleportation, one-way measurement, or the IBM Qiskit compiler, demonstrating its promises. As a side finding, we have identified and reported several unexpected behaviours with the Qiskit compiler.

quant-pharXiv:2511.22523•Nov 28, 2025•1 citation

Improved DD-based Equivalence Checking of Quantum Circuits

Lukas Burgholzer, Robert Wille

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 results confirm that the proposed strategies lead to substantial speed-ups - allowing to perform equivalence checking of quantum circuits factors or even magnitudes faster than the state of the art.

Asia and South Pacific Design Automation Conference (ASP-DAC)•Jan 1, 2020•37 citations

Efficient and Correct Compilation of Quantum Circuits

Robert Wille, Stefan Hillmich, Lukas Burgholzer

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 results for many instances and, additionally, guarantees correctness throughout the process.

IEEE International Symposium on Circuits and Systems proceedings•Sep 29, 2020•23 citations
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 compilation flow. To this end, we combine characteristics unique to quantum computing, e.g., its inherent reversibility, and certain knowledge about the compilation flow into a dedicated equivalence checking strategy. Experimental evaluations confirm that the proposed scheme allows to verify even large circuit instances with tens of thousands of operations within seconds or even less, whereas state-of-the-art techniques frequently time-out or require substantially more runtime. A corresponding open source implementation of the proposed method is publicly available at https://github.com/iic-jku/qcec.
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 extended to support quantum circuits (i.e., circuits which do not only rely on 0's and 1's but also employ superposition and entanglement). In this work, we propose an advanced methodology that takes the different paradigms of quantum circuits not only as a burden but as an opportunity. In fact, the proposed methodology explicitly utilizes characteristics unique to quantum computing in order to overcome the shortcomings of existing approaches. We show that by exploiting the reversibility of quantum circuits, complexity can be kept feasible in many cases. Moreover, we show that, in contrast to the classical realm, simulation is very powerful in verifying quantum circuits. Experimental evaluations confirm that the resulting methodology allows one to conduct equivalence checking dramatically faster than ever before-in many cases just a single simulation run is sufficient. An implementation of the proposed equivalence checking flow is publicly available at https://iic.jku.at/eda/research/quantum_verification/.
As state-of-the-art quantum computers are capable of running increasingly complex algorithms, the need for automated methods to design and test potential applications rises. Equivalence checking of quantum circuits is an important, yet hardly automated, task in the development of the quantum software stack. Recently, new methods have been proposed that tackle this problem from widely different perspectives. One of them is based on the ZX-calculus, a graphical rewriting system for quantum computing. However, the power and capability of this equivalence checking method has barely been explored. The aim of this work is to evaluate the ZX-calculus as a tool for equivalence checking of quantum circuits. To this end, it is demonstrated how the ZX-calculus based approach for equivalence checking can be expanded in order to verify the results of compilation flows and optimizations on quantum circuits. It is also shown that the ZX-calculus based method is not complete—especially for quantum circuits with ancillary qubits. In order to properly evaluate the proposed method, we conduct a detailed case study by comparing it to two other state-of-the-art methods for equivalence checking: one based on path-sums and another based on decision diagrams. The proposed methods have been integrated into the publicly available QCEC tool (https://github.com/cda-tum/qcec) which is part of the Munich Quantum Toolkit (MQT).
The Noisy Intermediate-Scale Quantum (NISQ) technology is currently investigated by major players in the field to build the first practically useful quantum computer. IBM QX architectures are the first ones which are already publicly available today. However, in order to use them, the respective quantum circuits have to be compiled for the respectively used target architecture. While first approaches have been proposed for this purpose, they are infeasible for a certain set of SU(4) quantum circuits which have recently been introduced to benchmark corresponding compilers. In this work, we analyze the bottlenecks of existing compilers and provide a dedicated method for compiling this kind of circuits to IBM QX architectures. Our experimental evaluation (using tools provided by IBM) shows that the proposed approach significantly outperforms IBM's own solution regarding fidelity of the compiled circuit as well as runtime. Moreover, the solution proposed in this work has been declared winner of the IBM QISKit Developer Challenge. An implementation of the proposed methodology is publicly available at http://iic.jku.at/eda/research/ibm_qx_mapping.
Equivalence checking of hybrid quantum circuits is of primary importance, given that quantum circuit transformations are omnipresent along the quantum compiler chain. While some approaches exist for automating this task, most focus on the simple case of unitary circuits. At the same time, real quantum computing requires hybrid circuits equipped with measurement operators. Moreover, the few approaches targeting the hybrid case are limited to a restricted class of problems. We propose tackling the Quantum Hybrid Circuit Equivalence Checking problem through lifting unitary circuit verification using a transformation known as deferred measurement. We show that this approach alone significantly outperforms prior work, and that, with the addition of specific unitary-level techniques we call separation and projection, it can handle much larger classes of hybrid circuit equivalence problems. We have implemented and evaluated our method over standard circuit transformations such as teleportation, one-way measurement, or the IBM Qiskit compiler, demonstrating its promises. As a side finding, we have identified and reported several unexpected behaviours with the Qiskit compiler.
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 results confirm that the proposed strategies lead to substantial speed-ups - allowing to perform equivalence checking of quantum circuits factors or even magnitudes faster than the state of the art.
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 results for many instances and, additionally, guarantees correctness throughout the process.