Partial Equivalence Checking of Quantum Circuits

For Boolean connectives, we denote conjunction by “$\wedge$” (sometimes omitted in a Boolean expression for brevity), disjunction by “$\vee$,” exclusive-or by “$\oplus$,” and negation by an overline. Given a Boolean function $f(x_{1},x_{2},...,x_{n})$, the positive cofactor of $f$ on $x_{i}$, denoted $f|_{x_{i}}$, is

Similarly, the negative cofactor of $f$ on $x_{i}$, denoted $f|_{\overline{x_{i}}}$, is

The reduced ordered binary decision diagram (ROBDD), referred to as BDD in the sequel, is a canonical form for Boolean function representation [35]. There are efficient BDD packages for Boolean function manipulation. A BDD is a directed acyclic graph consisting of non-terminal nodes and terminal-0 and terminal-1 nodes. Each non-terminal node $v$ is associated with a decision variable and has two children $v_{0}$ and $v_{1}$ pointed to by the 0-branch and 1-branch of $v$, respectively. Each node in a BDD corresponds to a Boolean function. Let $f_{v},f_{v_{0}},f_{v_{1}}$ be the functions of node $v$ with decision variable $x$ and its two children $v_{0},v_{1}$, respectively. Then $f_{v_{0}}=f|_{\overline{x}}$ and $f_{v_{1}}=f|_{x}$, and the Shannon expansion $f_{v}=xf_{v_{1}}\vee\overline{x}f_{v_{0}}$ holds. Fig. 2 shows a BDD of function $f=ac\vee\overline{a}bc\vee\overline{a}\overline{b}\overline{c}$.

For a quantum system, at the input end, a qubit is called a data qubit if it is associated with the input data and a non-data qubit otherwise. At the output end, a qubit is called a measured qubit if it is to be measured and a non-measured qubit otherwise. In an $n$-qubit quantum system, a quantum state can be represented by a $2^{n}\times 1$ vector $\phi=[a_{0},a_{1},...,a_{2^{n}-1}]^{\rm T}$, where each $a_{i}$ is a complex number and the norm of $\phi$ satisfies $\left\lVert\phi\right\rVert=1$. We use $|0\rangle$ to represent the vector $[1,0,...,0]^{\rm T}$, $|1\rangle$ to represent the vector $[0,1,0,...,0]^{\rm T}$, and so on. For state $|i\rangle$, we let the binary number of integer $i$ be expressed by qubits $q_{0},\ldots,q_{n-1}$ with $q_{0}$ being the most significant bit. In the sequel, we assume that non-data qubits are fixed to the initial state $|0\rangle$ and refer to them as ancilla qubits. This assumption is general in that any other initial state can be transformed from $|0\rangle$.

The evolution of the state of a closed quantum system can be described by quantum gates. For an $n$-qubit quantum system, a quantum gate can be defined by a $2^{n}\times 2^{n}$ unitary matrix $U$ of complex numbers. A unitary matrix $U$ is a matrix satisfying $U^{\dagger}U=I$, where $U^{\dagger}$ is the conjugate transpose of $U$ and $I$ is the identity matrix. Thus, $U^{\dagger}$ is also the inverse of $U$. A quantum circuit is made up of a series of quantum gates $G_{1},G_{2},...G_{d}$. Let their corresponding unitary matrices be $U_{1},U_{2},...,U_{d}$ and let $\phi_{0}$ be the initial state. Then the final output state $\phi_{out}$ of the circuit is derived by the product

Therefore, we can view the whole circuit as a quantum gate with the unitary matrix

Particularly, when an $n$-qubit quantum circuit with unitary matrix $U$ yields a permutation of the computational basis $\{|0\rangle,...,|2^{n}-1\rangle\}$, it is referred to as a reversible circuit [36, 37, 38, 39].

Because only the global unitary operator of a quantum circuit matters in our discussion, for simplicity we abstract away gate implementation details and denote an $n$-qubit quantum circuit $C$ as a 4-tuple $C=(d,m,k,U)$ for $n=d+k$, where

• •

  $d$ is the number of data qubits, specifically, $q_{0},\ldots,q_{d-1}$,

• •

  $m$ is the number of measured qubits, specifically, $q_{0},\ldots,q_{m-1}$,

• •

  $k$ is the number of non-data qubits, and

• •

  $U$ is the global unitary operator of $C$ of size $2^{n}\times 2^{n}$.

Note that above we make the data qubits and measured qubits follow the same order. This arrangement is without loss of generality as the qubits can be reordered by swap gates.

We remark that a matrix can be represented numerically or algebraically, and explicitly or implicitly for different computation choices. In this work, we adopt an algebraic and implicit approach to matrix representation and manipulation based on [40, 8].

The partial equivalence relation is formally defined as follows.

Note that, without loss of generality, we assume two circuits have the same number of ancilla qubits because we can always add dummy ancilla qubits to the one with fewer ancilla qubits. The partial equivalence checking problem can be stated as follows.

Partial equivalence can be applied to check the conformance between two quantum circuits that compute the same function but may produce different output states.

We remark that, in prior work [32], the notion of m-equivalence and q-equivalence are defined. For m-equivalent circuits, it requires that all qubits have fixed initial states, and it allows that we only measure on part of the qubits. Two circuits are m-equivalent if they have the same probability distribution of measurement outcomes. That is, m-equivalence is a special case of partial equivalence when we set $d=0$ for the circuits under verification. On the other hand, for q-equivalence, ancilla qubits are allowed. Besides, the output qubits are divided into two groups, the main output qubits and the garbage qubits. It is required that if we measure the garbage qubits, the quantum states of the main output qubits cannot be affected by the measurement outcomes of the garbage qubits. Two circuits are q-equivalent if the output states of the main output qubits between the two circuits are the same for any input state.

To demonstrate the usefulness of partial equivalence, we take the period-finding quantum algorithm [42] as an example. In Fig. 3 (a), the circuit computes the function

In Fig. 3 (b), the circuit computes the function

It can be seen that the $U_{1}$ and $U_{2}$ have the same period 4 (for $U_{1}$ mapping $|1\rangle\mapsto|3\rangle\mapsto|4\rangle\mapsto|2\rangle\mapsto|1\rangle$ and $U_{2}$ mapping $|1\rangle\mapsto|0\rangle\mapsto|2\rangle\mapsto|3\rangle\mapsto|1\rangle$). For the circuit in Fig. 3 (c), let the first register as the data qubits and the second register as the ancilla qubits. Let $C_{1}$ (resp. $C_{2}$) be the circuit of Fig. 3 (c) with the oracle blocks $U$ being substituted with function $U_{1}$ (resp. $U_{2}$). Then $C_{1}$ and $C_{2}$ are partially equivalent under $d=m=3$ despite the fact that neither of total equivalence and q-equivalence holds and m-equivalence is not applicable them. The fact that $C_{1}$ and $C_{2}$ are not totally equivalent is immediate. Also, we verify that the q-equivalence [32] does not hold because the output state of the $1^{\rm st}$ register is affected by the $2^{\rm nd}$ register; the m-equivalence is not applicable because only the $2^{\rm nd}$ register is taken as the ancilla qubits. To the best of our knowledge, no previous tools can check this equivalence.

We observe that when the two circuits under verification have no ancilla qubits, the computation of their partial equivalence checking can be simplified. It motivates the consideration of the following special case.

For instance, consider the aforementioned $C_{1}$ and $C_{2}$ circuits. If we properly add some quantum gates to the beginning of the second register of $C_{2}$ (e.g., achieving the mapping $|x\rangle\mapsto|x-1\mod 5\rangle$ for $x<5$ and $|x\rangle\mapsto|x\rangle$ for $x\geq 5$), then $C_{1}$ and $C_{2}$ can remain partially equivalent even if all qubits are taken as data qubits. In this case both circuits have no ancilla qubits (i.e., $k=0$).

There have been several quantum circuit equivalences being studied. We compare them with the partial equivalence.

Besides the previously mentioned m-equivalence and q-equivalence, the most common definition of quantum circuit equivalence is total equivalence, which requires that two circuits produce the same state vector (up to a global-phase difference) for any input state [8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19]. That is, the output states of the two circuits should be numerically identical except for a scalar multiplication factor.

Another well-known equivalence is functional equivalence of reversible circuits. In reversible circuits, they may also include ancilla qubits, and some qubits may be discarded in the end (i.e., we do not care about their measurement results). Some may even include don’t-care conditions, which means that we do not care about all of or part of the measurement results under some input states [36].

Though partial equivalence looks similar to functional equivalence of reversible circuits and m-equivalence, we note that partial equivalence is much more complex, because measurement is a non-linear operation and does not have superposition property. That is, even if we know

for $i=1,2$, we cannot infer

Therefore, even with a brute-force search to enumerate the probability distribution under $\psi=e_{i,2^{d}}$ for all $i$, the partial equivalence relation is still not guaranteed. Some other approaches to checking partial equivalence are essential.

We briefly summarize the main differences between the equivalence types mentioned above in Table I. We further illustrate the relations between partial equivalence and other equivalences in Fig. 4. Note that partial equivalence subsumes total equivalence, functional equivalence of reversible circuits, and q-equivalence as these equivalences are special cases of partial equivalence. Specifically, it is evident that totally equivalent circuits must be partially equivalent. For reversible circuits, it can be derived from definition that $P(t|\psi,C)$ is either 0 or 1 for all $\psi=|0\rangle,|1\rangle,...,|2^{d}-1\rangle$, so Eq. (12) holds. Therefore, functionally equivalent reversible circuits without don’t care conditions must be partially equivalent. As for m-equivalence, it can be clearly seen that we can apply partial equivalence to m-equivalence by setting $d=0$. For q-equivalence, as the states of main output qubits between two circuits are identical, we must get the same probability distribution of the two circuits if we measure on the main output qubits. Thus, q-equivalent circuits must be partially equivalent.

To solve Problem 1, we first derive the condition when $C_{1}\sim C_{2}$ holds.

As mentioned before, brute-force search does not work for partial equivalence. Therefore, Theorem 1 provides the first way to formally verify the partial equivalence relation.

From Theorem 1, we can see that whether $C_{1}\sim C_{2}$ only depends on the $v_{i,j}(U)$’s of two matrices, and is not related to other entries.

For the case that both circuits have no ancilla qubits, we provide another necessary and sufficient condition for partial equivalence as follows.

If $U_{1}$ and $U_{2}$ are given in their explicit numerical form, we can easily extract $v_{i,j}(U)$’s and enumerate all $(t,p,q)$ triples to check whether $C_{1}\sim C_{2}$ by Theorem 1, with $O(2^{3d+k})$ steps of complex number multiplications. However, as $U_{1}$ and $U_{2}$ may be in an implicit form, we give another approach by using matrix entry manipulation and matrix multiplication, as shown in Algorithm 1.

To better illustrate steps 5 and 6, we note that after step 6, each $v_{i,j}(U_{1})$ for different $i$ and $j$ should be separated into different columns, and all entries not storing values of $v_{i,j}(U_{1})$ are 0. An example of $U_{1}^{\prime}$ with $d=m=k=1$ after this step is shown as follows.

To see the correctness of Algorithm 1, we first consider the case $m\geq k$. It can be easily checked that after step 8, the $(2^{k}p,\>2^{k}q+t)^{\mathrm{th}}$ entry of $U_{1}^{\prime\prime}\>$will store the value of $v_{t,p}(U_{1})^{\dagger}v_{t,q}(U_{1})$, while the other entries are 0. Note that in step 2 we have added some ancilla qubits and now $k=m$. Therefore, we can easily check whether $U_{1}^{\prime\prime}=U_{2}^{\prime\prime}$ holds to determine whether $C_{1}\sim C_{2}$.

For the case $m<k$, the $(2^{k}p,\>2^{k}q+t)^{\mathrm{th}}$ entry of $U_{1}^{\prime\prime}\>$still stores the value of $v_{t,p}(U_{1})^{\dagger}v_{t,q}(U_{1})$, but only for those with $t=0,1,...,2^{m-1}$. For $t=2^{m},...,2^{k-1}$, the value of $v_{t,q}(U_{1})^{\dagger}v_{t,q}(U_{1})$ does not exist, but we can see that the $(2^{k}p,\>2^{k}q+t)^{\mathrm{th}}$ entry of $U_{1}^{\prime\prime}\>$will always be 0 because the entries in the ${(2^{k}q+t)}^{\rm{th}}$ column of $U_{1}^{\prime}$ are all 0’s after step 6. That is, though we do not clear these entries in step 8, they are automatically set to 0. Therefore, we can still determine whether $C_{1}\sim C_{2}$ by checking whether $U_{1}^{\prime\prime}=U_{2}^{\prime\prime}$.

We further point out that this can be done quite easily using bit-sliced algebraic representation of a matrix [8], as shown in Algorithm 2. As introduced before, a matrix is represented by multiple BDDs, but here we use single $F_{1}$ and $F_{2}$ as representatives for all BDDs in $C_{1}$ and $C_{2}$ respectively for convenience. In steps 5, 7, 10, 13, we mean to do the same operation on each BDD, and in step 15, we need all corresponding BDDs of the two circuits to be the same.

We use steps 4 to 10 in Algorithm 2 to replace steps 5 and 6 in Algorithm 1. In steps 4 to 5, we divide the columns of $U_{1}$ into $2^{d}$ parts. For each part, we use cofactor operation to copy the leftmost columns to the other columns. In steps 6 to 9, we remove unwanted entries to ensure that each column only contains different $v_{i,j}(U_{1})$’s. The remaining steps have similar functions as in Algorithm 1 but are rewritten in Boolean form.

We can see that with the help of BDD, the operations can be simplified and are more efficient. To be precise, two applications of inverse circuit operations $U^{-1}$ are required, and only $O(m+k)$ Boolean AND, OR, and cofactor operations are needed, which is linear to $m$ and $k$. As BDDs often give a good data compression, there may be a significant speedup for Algorithm 2.

Similarly, we can directly use Theorem 2 to solve Problem 2 if $U_{1}$ and $U_{2}$ are explicitly given. Here we emphasize that it is also easy to check this property using bit-sliced algebraic representation of the matrix. The checking procedure is shown in Algorithm 3. Again, we mean to do the same operation on each BDD in step 5, and we require all BDDs to be constant $false$ in step 6.

We can see that in Algorithm 3, we do not have to build BDDs for $C_{1}$ and $C_{2}$ respectively, but rather merge them into one quantum circuit $C_{1}C_{2}^{-1}$. As there may be some gates canceled out in $C_{1}C_{2}^{-1}$, Algorithm 3 may be more efficient than Algorithm 2.

We used the tool proposed in [39] to implement the reversible circuits realizing $U|x\rangle=|ax\mod N\rangle$ for $x<N$ and $U|x\rangle=|a(x+1)-1\mod N\rangle$ for $x<N$, which have the same period with input state $|1\rangle$. We then substituted the reversible circuits into the oracle used in the period finding algorithm. We let the first register consist of 3 qubits, and used one extra ancilla qubit to implement quantum Fourier transform. We then used Algorithm 2 to test the equivalence relation. As mentioned above, this type of equivalence cannot be verified by previous tools, and Algorithm 2 is the only way to check their equivalence relation. We have tested the $(a,N)$ pairs for all $a\in\{3,5,7,11\},N\in\{5,7,11,13\}$ and $a<N$. The parameters are set to $d=m=3$ and $k=\lceil\log_{2}N\rceil+1$.

The results are shown in Table II. All test cases yield correct answers. As these test cases are relatively small, we can see that the runtime is roughly proportional to the gate count. On the other hand, the memory usages are roughly the same because all test cases have similar numbers of qubits.

To further test the scalability of our algorithms, we generated some benchmarks with Clifford+T gates (H, S, T, CNOT gates) and 2-control Toffoli gates. The numbers of data qubits of the benchmarks range from $d=5,10,15,20,25,30,35,40,$ $50,60,70,80,90,100$. The number $m$ of measured qubits was fixed to $\lfloor 0.5d\rfloor$, and the gate number was set to about $6.5d$. For each $d$, 20 groups of circuits were generated, and each group includes two conditions: ancilla qubits existing or non-existing. We used the latter condition to test Algorithm 3, and both conditions to test Algorithm 2.

The structure of the benchmarks is shown in Fig. 5. Let the partially equivalent circuit pair be $C_{1}$ and $C_{2}$, both with $d$ data qubits and $m$ measured qubits. The circuits are divided into five parts: H (H gates), T (totally equivalent), P (partially equivalent), A (arbitrary) and C (CNOT gates). If $C_{1}$ and $C_{2}$ are in the condition without ancilla qubits, only the first four parts are contained. Otherwise, they both contain all five parts.

In part H, an H gate is firstly applied to each data qubit to impose superposition. In part T, we generate a random sub-circuit with $d$ qubits and $3d$ gates to apply on both circuits, but all the Toffoli gates in $C_{2}$ are decomposed in the way proposed in [44]. In part P, we divide the data qubits into several groups, where each group may contain one or two adjacent qubits. For each group, we apply $X_{1}$ and $X_{2}$ on $C_{1}$ and $C_{2}$, respectively, where $X_{1}$ and $X_{2}$ are pre-generated subcircuits satisfying $X_{1}\sim X_{2}$ when all qubits are set to data qubits and measured qubits. $X_{1}$ and $X_{2}$ are exhaustively searched with up to five gates in total. In part A, different random sub-circuits with $d-m$ qubits and $d-m$ gates are applied on $C_{1}$ and $C_{2}$. These gates trivially do not affect the measurement results of the measured qubits. In part C, we use the ancilla qubits as the control bits to control the upper $d$ qubits. As ancilla qubits are initially set to 0, these CNOT gates do not affect the circuit.

Although the circuit generation is simple, there are no known circuit simplification methods exploiting partial equivalence. The generated circuits are used to test our algorithms. Furthermore, to validate the correctness of the benchmarks, we use the same generating method to generate some test cases with $3\leq d\leq 9$. For each test case, we use Qiskit [27] to randomly set an initial state and get the final state vector numerically. We calculate for all possible outputs and make sure that $C_{1}$ and $C_{2}$ have the same probability distribution under this random initial state.