Advanced Equivalence Checking for Quantum Circuits

Lukas Burgholzer, Robert Wille

Published 2020-04-17Version 1

Quantum computing will change the way we tackle certain problems. It promises to drastically speed-up many chemical, financial, cryptographical, or machine-learning applications. However, to capitalize on those promises, complex design flows composed of steps such as compilation, decomposition, or mapping need to be employed before being able to execute a conceptual quantum algorithm on an actual device. This results in descriptions at various levels of abstraction which may significantly differ from each other. The complexity of the underlying design problems necessitates 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 are inspired by equivalence checking in the classical realm and have merely been extended to support quantum 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 which takes the different paradigms of quantum circuits not as a burden, but as a chance. 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 unveil that, in contrast to the classical realm, simulation is very powerful in verifying quantum circuits. Experimental evaluations confirm that the resulting methodology allows to conduct equivalence checking drastically faster than ever before -- in many cases just a single simulation run is sufficient. An implementation of the proposed methodology is available at http://iic.jku.at/eda/research/quantum_verification/.