Equivalence Checking of Sequential Quantum Circuits

Abstract

We define a formal framework for equivalence checking of sequential quantum circuits. The model we adopt is a quantum state machine, which is a natural quantum generalisation of Mealy machines. A major difficulty in checking quantum circuits (but not present in checking classical circuits) is that the state spaces of quantum circuits are continuums. This difficulty is resolved by our main theorem showing that equivalence checking of two quantum Mealy machines can be done with input sequences that are taken from some chosen basis (which are finite) and have a length quadratic in the dimensions of the state Hilbert spaces of the machines. Based on this theoretical result, we develop an (and to the best of our knowledge, the first) algorithm for checking equivalence of sequential quantum circuits with running time $\mathcal{O}(2^{3m+5l}(2^{3m}+2^{3l}))$, where $m$ and $l$ denote the numbers of input and internal qubits, respectively. The complexity of our algorithm is comparable with that of the known algorithms for checking classical sequential circuits in the sense that both are exponential in the number of (qu)bits. Several case studies and experiments are presented.

Full version. 33 pages, 8 figures, 2 tables, 1 algorithm

References in corpus (11)

• Quantum Computing in the NISQ era and beyond
• Supplementary information for "Quantum supremacy using a programmable superconducting processor"
• A fast, low-leakage, high-fidelity two-qubit gate for a programmable superconducting quantum computer
• Quantum Feedback Networks: Hamiltonian Formulation
• Towards Large-scale Functional Verification of Universal Quantum Circuits
• Time-domain characterization and correction of on-chip distortion of control pulses in a quantum processor
• Hardware for Dynamic Quantum Computing
• Equivalence Checking of Sequential Quantum Circuits
• Quantum finite automata: survey, status and research directions
• A Specification Format and a Verification Method of Fault-Tolerant Quantum Circuits
• Equivalence Checking of Quantum Finite-State Machines

Cited by in corpus (6)

• Equivalence Checking of Sequential Quantum Circuits
• Parallel Quantum Algorithm for Hamiltonian Simulation
• Automatic Test Pattern Generation for Robust Quantum Circuit Testing
• Equivalence Checking of Quantum Finite-State Machines
• Symbolic Verification of Quantum Circuits
• Quantum Büchi Automata