  With the race to build large-scale quantum computers and efforts to exploit
quantum algorithms for efficient problem solving in science and engineering
disciplines, the requirement to have efficient and scalable verification
methods are of vital importance. We propose a novel formal verification method
that is targeted at Quantum Fourier Transform (QFT) circuits. QFT is a
fundamental quantum algorithm that forms the basis of many quantum computing
applications. The verification method employs abstractions of quantum gates
used in QFT that leads to a reduction of the verification problem from Hilbert
space to the quantifier free logic of bit-vectors. Very efficient decision
procedures are available to reason about bit-vectors. Therefore, our method is
able to scale up to the verification of QFT circuits with 10,000 qubits and 50
million quantum gates, providing a meteoric advance in the size of QFT circuits
thus far verified using formal verification methods.
