Is Simulation the only Alternative for Effective Verification of Dynamic Quantum Circuits?

This paper investigates the verification gap of Dynamic Quantum Circuits (DQC) by analyzing state-of-the-art equivalence checking approaches. Today’s Noisy Intermediate-Scale Quantum (NISQ) devices are limited in the number of qubits. DQCs drastically reduce the number of qubits required by guiding the outcome based on the intermediate results of the computations. Investigation of feasibility of existing verification tools with respect to DQC verification is needed. In order to verify the equivalence of DQCs, verification tools often transform dynamic primitives in order to reveal the underlying functionality of the circuits. This leads to restoration of their unitary functionality and allows existing equivalence checkers to reason about DQCs. Our objective is to provide empirical data that can be used to improve these tools by examining their capabilities and effectiveness. Equivalence checking methods that use ZX-Calculus, Quantum Multi Valued Decision Diagrams (QMDD) and simulators are considered in this regard. In order to gauge the effectiveness of the present tools, we use the Bernstein-Vazirani, Deutsch-Jozsa and Quantum Phase Estimation algorithms and their dynamic variants. Experiments reveal that the existing equivalence checking tools are limited in their effectiveness, while simulation based approaches provide correct verifications at the expense of high runtime overhead. Our results show that the different verification methods never achieves accuracy of more than 50%.