An efficient functional verification method for quantum Boolean circuits

Functional verification is an important design method for verifying functional equivalence between a simplified quantum Boolean circuit and original one. During the design process, checking the equivalence of two quantum Boolean circuits is necessary. In this paper, we present an algorithm that can efficiently and easily verify two quantum Boolean circuits by using the back propagation method. For a set of input vectors, the idea of the algorithm is to find the checking vectors that output vectors are different from input vectors by a backward tracking process.