Abstract

Quantum computing systems promise to increase the efficiency of solving problems which classical computers cannot handle efficiently, such as integers factorization. In this paper, we introduce the idea of design automation for quantum circuits, where we develop a rich library of quantum gates and a robust decision procedure in higher-order logic, to reason about quantum circuits formally. We adopt a low level modeling approach of quantum gates at the optics physics. Interestingly, this approach facilitates the modeling of optimized implementations for certain quantum gates that cannot be optimally modeled with available analysis tools. The constructed library contains a variety of quantum gates ranging from 1-qubit to 3-qubit gates that are sufficient to model most of existing quantum circuits. To eliminate the user's interaction with the theorem prover, we develop a decision procedure and tactics that fully automate the analysis process. As real world applications, we present the formal analysis of several quantum circuits including the quantum full adder and the Grover's oracle circuits, for which we have proved the behavioral correctness and calculated the operational success rate which has never been provided in the literature.