Verifying Results of the IBM Qiskit Quantum Circuit Compilation Flow

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.

arXiv comment10 pages, to be published at International Conference on Quantum Computing and Engineering (QCE20)

References in corpus (6)

• Elementary gates for quantum computation
• A universal quantum circuit for two-qubit transformations with three CNOT gates
• On the advantages of using relative phase Toffolis with an application to multiple control Toffoli optimization
• Mapping Quantum Circuits to IBM QX Architectures Using the Minimal Number of SWAP and H Operations
• How to Efficiently Handle Complex Values? Implementing Decision Diagrams for Quantum Computing
• staq -- A full-stack quantum processing toolkit

Cited by in corpus (6)

• MQT Bench: Benchmarking Software and Design Automation Tools for Quantum Computing
• Tools for Quantum Computing Based on Decision Diagrams
• Equivalence Checking of Parameterized Quantum Circuits: Verifying the Compilation of Variational Quantum Algorithms
• Simulation Paths for Quantum Circuit Simulation with Decision Diagrams
• As Accurate as Needed, as Efficient as Possible: Approximations in DD-based Quantum Circuit Simulation
• Efficient Construction of Functional Representations for Quantum Algorithms