Johannes Kepler University Linz
Integrated Circuit and System Design
Univ.-Prof. Dr. Robert Wille
Altenberger Straße 69 | SCP4 0331
4040 Linz | Austria
Tel: +43 732 2468 4739

Map and directions to JKU

↑ Quantum Computing

Verification of Quantum Circuits

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 synthesis, mapping, or optimizations 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).

On this page, we summarize our work on the verification of quantum circuits which takes the different paradigms of quantum computing not only as a burden, but as an opportunity. To this end, we first introduce the developed advanced equivalence checking methodology; afterwards, we describe its application to the verification of compilation results, which clearly demonstrates its effectiveness.

All proposed methods have been implemented into the quantum circuit equivalence checking tool QCEC as part of the open-source JKQ quantum toolset. QCEC is also designed to natively integrate with IBM Qiskit. Moreover, in order to allow interested researchers and designers to quickly get an understanding of how decision diagrams can be employed for the simulation and verification of quantum circuits, we additionally provide an installation-free web-tool visualizing decision diagrams for quantum computing. In case of questions/problems, don’t hesitate to contact us via, or by creating an issue on GitHub.

Advanced Equivalence Checking Methodology

The proposed methodology explicitly utilizes characteristics unique to quantum computing in order to overcome the shortcomings of existing approaches. By exploiting the reversibility of quantum circuits, complexity can be kept feasible in many cases. Moreover, in contrast to the classical realm, simulation proves very powerful in verifying quantum circuits. The resulting methodology allows to conduct equivalence checking drastically faster than ever before—in many cases just a single simulation run is sufficient.

Details of the methodology are summarized in the paper entitled “Advanced Equivalence Checking for Quantum Circuits” [pdf].

If you use this tool for your research, we will be thankful if you refer to it by citing the following publication:

    author = {Burgholzer, Lukas and Wille, Robert},
    title = {Advanced Equivalence Checking for Quantum Circuits},
    year = 2021,
    journaltitle = {{IEEE} Trans. on {CAD} of Integrated Circuits and Systems}

Verification of Compilation Flow Results

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.

Details of the verification scheme are summarized in the paper entitled “Verifying Results of the IBM Qiskit Quantum Circuit Compilation Flow” [pdf].

If you use this verification scheme for your research, we will be thankful if you refer to it by citing the following publication:

  title = {Verifying results of the {{IBM Qiskit}} quantum circuit compilation flow},
  booktitle = {International Conference on Quantum Computing and Engineering},
  author = {Burgholzer, Lukas and Raymond, Rudy and Wille, Robert},
  year = {2020}

Integration with IBM Qiskit

The JKQ QCEC tool is designed to natively integrate with IBM Qiskit. After installing the tool using pip install jkq.qcec, verifying the results of IBM Qiskit’s quantum circuit compilation flow is as easy as running the following Python script:

from jkq import qcec
from qiskit import QuantumCircuit, transpile

# create your quantum circuit

qc = <...> 

# append measurements to save output mapping of physical to logical (qu)bits


# compile circuit to appropriate backend using some optimization level

qc_comp = transpile(qc, backend=<...>, optimization_level=<0 | 1 | 2 | 3>) 

# verify the compilation result

qcec.verify(qc, qc_comp, method=qcec.Method.compilationflow, statistics=True)

JKQ DDVis Online Tool

In an effort to make decision diagrams for quantum computing more accessible, we present JKQ DDVis—an installation-free web-tool which visualizes quantum decision diagrams and allows to explore their behavior when used in design tasks such as simulation, synthesis, and verification.