{'fraction_non_alphanumeric': 0.043094136870966845, 'fraction_numerical': 0.020494640928351845, 'mean_word_length': 4.024071239738417, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Partial Equivalence Checking of Quantum Circuits

Equivalence checking of quantum circuits is an essential element in quantum program compilation, in which a quantum program can be synthesized into different quantum circuits that may vary in the number of qubits, initialization requirements, and output states. Verifying the equivalences among the implementation variants requires proper generality. Although different notions of quantum circuit equivalence have been defined, prior methods cannot check observational equivalence between two quantum circuits whose qubits are partially initialized, which is referred to as partial equivalence. In this work, we prove a necessary and sufficient condition for two circuits to be partially equivalent. Based on the condition, we devise algorithms for checking quantum circuits whose partial equivalence cannot be verified by prior approaches. Experiment results confirm the generality and demonstrate the efficiency and effectiveness of our method. Our result may unleash the optimization power of quantum program compilation to take more aggressive steps.


I. INTRODUCTION
Equivalence checking plays an important role in the design flow of modern integrated circuits. It ensures the transformations done in the corresponding synthesis steps do not introduce errors. Many scalable techniques, such as random simulation, satisfiability solving, decision diagrams, and structural similarity detection, have been developed and widely applied in classical circuit verification [1]- [7]. Due to the rapid progress of hardware and software developments in quantum computation, quantum circuit verification, especially equivalence checking, arises as an important issue in quantum program compilation. Although practical quantum circuits remain relatively small until now, it remains challenging to their equivalence checking due to extraordinary quantum properties. Moreover, as quantum computing technology evolves, the size of quantum circuits will continue growing. Efficient equivalence checking tools for quantum circuits are essential.
Many approaches to equivalence checking of quantum circuits have been proposed [8]- [19]. Among them, decision diagrams are a widely adopted data structure for quantum state and operator representation and manipulation [8]- [10], [13], [19]. Also, techniques, such as miter construction [8], [10], [12], [13], [18] or tensor network computation [11], have been applied. Some of them focus on the equivalence of reversible circuits, which realize permutation functions, whereas others address the equivalence of more general quantum circuits. For the latter, most of them require total equivalence, namely, the identity of the output states (modulo a global phase difference) between the two circuits under verification. However, since measurement is the only way to extract information from a quantum system, total quantum state equivalence may be unnecessary and only observational equivalence matters. That is, two circuits exhibit the same probability for every possible measurement outcome under a fixed measurement basis. Furthermore, not all qubits of a circuit need to be measured and there can be a set of initial states to be verified not just a particular single initial state. To accommodate such different design constraints, we relax the notion of quantum circuit equivalence and define a generalization, called partial equivalence. That is, two circuits are partially equivalent if, given any valid initial input state, they exhibit the same probability for each measurement outcome. Therefore, two partially equivalent circuits do not exhibit statistical differences by observed measurements. Essentially, the generality of partial equivalence allows more flexibility for quantum circuit synthesis. Fig. 1 shows an example where C 1 and C 2 are partially equivalent, but not totally equivalent.
Apart from its application in quantum circuit synthesis, partial equivalence checking has its natural application in quantum program compilation. As the quantum computing technology evolves, many quantum programming languages have been developed, e.g., [20]- [31]. Although nowadays most quantum programming languages are abstracted at the gate level, high-level languages will get their increasing presence in the future. Their compilation may require making tradeoffs between ancilla bits and quantum gates. To verify the correctness of different compilation choices may require the defined partial equivalence.
Equivalence based on measurement results is not new, nor is the relaxation requiring only some of the input qubits to be data qubits and some of the output qubits to be measured qubits. In fact, partial equivalence can be seen as the case that all principal output qubits in Definition 3 of [32] are to be measured. However, there are no corresponding checking methods so far, and none of the prior work [18], [19], [32]- [34] can fully resolve the partial equivalence checking problem. In particular, equivalence up to a relative phase discussed in [18] can only cover the case that all output qubits are measured; the method considering measurement-based equivalence in [19] is used for reversible circuits only; the initial state is given and fixed in [32] and [33]; sequential circuit verification in [34] is limited to the assumption that the number of measured output qubits cannot be smaller than the number of data input qubits. In this work, we are not constrained by these limitations. Our methods can be applied to general cases of checking partial equivalence relations. Moreover, they are compatible with the state-of-the-art SliQEC [8] system, which uses Boolean functions represented by decision diagrams to store and manipulate matrices.
The main results of this work include: 1) We characterize partial equivalence (in Section III), which subsumes prior notions of quantum circuit equivalence. 2) We prove a necessary and sufficient condition for two circuits to be partially equivalent (in Section IV). 3) We develop algorithms for partial equivalence checking under general and special settings (in Section V). 4) We conduct experiments to demonstrate the feasibility and effectiveness of our algorithms and the practical applicability of partial equivalence (in Section VI).

II. PRELIMINARIES
We briefly provide some background and define notations.

A. Boolean Function and Decision Diagram
For Boolean connectives, we denote conjunction by "^" (sometimes omitted in a Boolean expression for brevity), disjunction by "_," exclusive-or by "'," and negation by an overline. Given a Boolean function f px 1 , x 2 , ..., x n q, the positive cofactor of f on Similarly, the negative cofactor of f on 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 v0 , f v1 be the functions of node v with decision variable x and its two children v 0 , v 1 , respectively. Then f v0 " f | x and f v1 " f | x , and the Shannon expansion f v " xf v1 _ xf v0 holds. Fig. 2 shows a BDD of function f " ac _ abc _ abc.

B. Quantum States and Quantum Circuits
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ˆ1 vector φ " ra 0 , a 1 , ..., a 2 n´1 s T , where each a i is a complex number and the norm of φ satisfies φ " 1. We use |0y to represent the vector r1, 0, ..., 0s T , |1y to represent the vector r0, 1, 0, ..., 0s T , and so on. For state |iy, we let the binary number of integer i be expressed by qubits q 0 , . . . , 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 |0y and refer to them as ancilla qubits. This assumption is general in that any other initial state can be transformed from |0y.
If we measure all the qubits of φ under the computational basis, there will be a probability |a i | 2 for the system to get into state |iy. Also, if we measure only the first (more significant) m qubits, for m ď n, of φ, the probability of obtaining a state |jy, for j P t0, 1, ..., 2 m´1 u, of the measured qubits equals where g " 2 n´m . 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ˆ2n unitary matrix U of complex numbers. A unitary matrix U is a matrix satisfying U : U " I, where U : is the conjugate transpose of U and I is the identity matrix. Thus, U : 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 φ 0 be the initial state. Then the final output state φ 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 t|0y, ..., |2 n´1 yu, it is referred to as a reversible circuit [36]- [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 " pd, m, k, U q for n " d`k, where ‚ d is the number of data qubits, specifically, q 0 , . . . , q d´1 , ‚ m is the number of measured qubits, specifically, q 0 , . . . , q m´1 , ‚ k is the number of non-data qubits, and ‚ U is the global unitary operator of C of size 2 nˆ2n . 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.
Given a quantum circuit C " pd, m, k, U q with the data qubits prepared at initial state ψ, we denote the probability of C collapsing to state |ty upon a measurement on the measured qubits under the computational basis as P pt|ψ, Cq, which can be calculated by where g " 2 pd`k´mq and u x,y denotes the px, yq th entry of U . 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 [8], [40].

C. Algebraic and Implicit Representation of Matrices
Following [41], we represent a complex number α P C algebraically by where ω " e iπ{4 and a, b, c, d P Z. In [8], the bit-slicing technique [40] is applied to represent a 2 nˆ2n complex matrix by one integer-type variable for the k-coefficient and 4r 2nvariable BDDs for the a-, b-, c-, d-coefficients, assuming an integer is encoded with a bit-vector of size r. Let the BDDs of the i th bit of the a, b, c, d-coefficient Boolean matrices be F ai , F bi , F ci , F di , respectively, for i " 0, . . . , r´1. In the sequel, we do not distinguish among F ai , F bi , F ci , F di and simply use F to refer to every individual of these BDDs. Essentially, such a function F of 2n variables implicitly represents a 2 nˆ2n Boolean matrix, whose rows and columns are indexed by the output qubits and input qubits, respectively, in our context. For qubit q i , two variables x i and y i are introduced to encode its corresponding output qubit and input qubit, respectively, for the Boolean matrix. The variables X " tx 0 , . . . , x n´1 u and Y " ty 0 , . . . , y n´1 u are referred to as the row-variables and column-variables, respectively. Effectively, F is a function over variables X Y Y . That is, the pi, jq th entry of the Boolean matrix corresponds to the Boolean value of F for X and Y being substituted with the n-bit binary numbers of i and j, respectively. In addition to the implicit matrix representation using Boolean functions, the multiplication of matrices can be done effectively through Boolean function manipulations as shown in [8].

III. PARTIAL EQUIVALENCE PROBLEM
In this section, we formally define partial equivalence between two quantum circuits, and compare it to other equivalence notions in the literature.

A. Problem Statement
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.
Problem 1 (Partial Equivalence Checking). Given two circuits C 1 " pd, m, k, U 1 q and C 2 " pd, m, k, U 2 q, we are asked to check whether C 1 and C 2 are partially equivalent.
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 mequivalence 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 qequivalence, 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 |1y Þ Ñ |3y Þ Ñ |4y Þ Ñ |2y Þ Ñ |1y and U 2 mapping |1y Þ Ñ |0y Þ Ñ |2y Þ Ñ |3y Þ Ñ |1y). 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 mequivalence is not applicable them. The fact that C 1 and C 2 are not totally equivalent is immediate. Also, we verify that the qequivalence [32] does not hold because the output state of the 1 st register is affected by the 2 nd register; the m-equivalence is not applicable because only the 2 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.
Problem 2 (Zero-Ancilla Partial Equivalence Checking). Given two circuits C 1 " pd, m, 0, U 1 q and C 2 " pd, m, 0, U 2 q, we are asked to check whether C 1 and C 2 are partially equivalent.
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 |xy Þ Ñ |x´1 mod 5y for x ă 5 and |xy Þ Ñ |xy for x ě 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).

B. Comparison of Different Equivalences
There have been several quantum circuit equivalences being studied. We compare them with the partial equivalence.
Besides the previously mentioned m-equivalence and qequivalence, 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]- [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 ψ " 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 pt|ψ, Cq is either 0 or 1 for all ψ " |0y, |1y, ..., |2 d´1 y, 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.

IV. NECESSARY AND SUFFICIENT CONDITIONS OF PARTIAL EQUIVALENCE
In this section, we derive a necessary and sufficient condition for partial equivalence, which can be directly used to solve Problem 1 if the matrices of both circuits are explicitly given. For the special case with no ancilla qubits, we show that a simpler necessary and sufficient condition exists. We define the following notation to locate some submatrices.
Definition 2. Given a circuit C " pd, m, k, U q, let u p,q represents the pp, qq th entry of U and g " 2 pd`k´mq , then v i,j pU q of size g is defined to be v i,j pU q " ru gi,2 k j , u gi`1,2 k j , ..., u gi`g´1,2 k j s T , where i " 0, 1, ..., 2 m´1 , j " 0, 1, ..., 2 d´1 . An example for d " m " k " 1 is illustrated as follows. In addition, we use e i,l to represent the unit vector r0, 0, ..., 0, 1, 0, ..., 0s of length l and the i th position (i starts from 0) being 1.
We remark that the definition of tv i,j pU qu is critical in deriving the necessary and sufficient condition for the partial equivalence. We will show this point in the following section.

A. Property of Partial Equivalence
To solve Problem 1, we first derive the condition when C 1 " C 2 holds.
Proof. Let the input state vector ψ " ra 0 , a 1 , ..., a p2 d´1 q s T . The matrix U 1 and U 2 will respectively be applied on ψbe 0,2 k . Let's consider the output |ty " t 0 t 1 ...t m´1 . Let g " 2 pd`k´mq and u 1,x,y denotes the px, yq entry of U 1 , then Re ap a q¨vt,p pU 1 q : v t,q pU 1 q ( , where Re txu denotes the real part of the complex number x. Similarly, we get Re ap a q¨vt,p pU 2 q : v t,q pU 2 q ( . (16) If C 1 " C 2 , then P pt|ψ, C 1 q " P pt|ψ, C 2 q must hold for all ψ, so v t,p pU 1 q : v t,q pU 1 q " v t,p pU 2 q : v t,q pU 2 q must hold for all p and q. We also need the above equality hold for any t " 0, 1, ..., 2 m´1 . Thus, C 1 " C 2 ô P pt|ψ, C 1 q " P pt|ψ, C 2 q @t@ψ ô v t,p pU 1 q : v t,q pU 1 q " v t,p pU 2 q : v t,q pU 2 q @t@p@q.
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 " C 2 only depends on the v i,j pU q's of two matrices, and is not related to other entries.

B. Property of Zero-Ancilla Partial Equivalence
For the case that both circuits have no ancilla qubits, we provide another necessary and sufficient condition for partial equivalence as follows.
where each U i,i is a 2 d´mˆ2d´m square matrix, and the other entries in U 1 U´1 2 not labeled are 0.
Proof. Firstly we show a transformed problem. By definition, C 1 " C 2 if and only if P pt|ψ, C 1 q " P pt|ψ, C 2 q for any ψ and t. Let U 1 ψ " φ 1 , U 2 ψ " φ 2 , and then we have U 1 U´1 2 φ 2 " φ 1 . Because U 1 and U 2 are both reversible matrices, φ 1 and φ 2 can be any vector of size 2 d (and satisfying φ 1 " φ 2 " 1). Thus, C 1 " C 2 if and only if P pt|φ 2 , C 1 C´1 2 q " P pt|φ 2 , Iq for any φ 2 and any t, where C 1 C´1 2 is the circuit with unitary matrix U 1 U´1 2 , and I is the identity circuit that directly sends the input to the output. We will use the transformed problem in the following proof.
(ii) the "if " part: (17), we firstly note that: Because U " U 1 U´1 2 is a unitary matrix, U : i,i U i,i must be identity for all i. Thus, each U i,i must be a unitary matrix. Now for any φ 2 , let φ 2 " ra 0 , a 1 , ..., a 2 d´1 s T " rA 0 , A 1 , ..., A 2 m´1s T , where each A i is of length 2 d´m . That is, we equally divide φ 2 into 2 m groups. Then Because U t,t is unitary, it is true that Because A t " P pt|φ 2 , Iq, P pt|φ 2 , C 1 C´1 2 q " P pt|φ 2 , Iq holds for all φ 2 and t. Therefore, C 1 " C 2 .

V. ALGORITHMS FOR PARTIAL EQUIVALENCE CHECKING
In this section, we present algorithms to solve Problems 1 and 2 based on the theorems established in Section IV. We emphasize that these algorithms can be realized by using the bit-sliced algebraic representation of matrices [8].

A. Partial Equivalence Checking Algorithm
If U 1 and U 2 are given in their explicit numerical form, we can easily extract v i,j pU q's and enumerate all pt, p, qq triples to check whether C 1 " C 2 by Theorem 1, with Op2 3d`k q 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 pU 1 q for different i and j should be separated into different columns, and all entries not storing values of v i,j pU 1 q are 0. An example of U 1 1 with d " m " k " 1 after this step is shown as follows.
Algorithm 1 PEC(C 1 ,C 2 ) Input: C1: C1 " pd, m, k, U1q, C2: C2 " pd, m, k, U2q Output: Whether C1 " C2 or not 1: extra :" maxtm´k, 0u 2: k :" k`extra 3: U1 :" U1 b I 2 extra 4: U 1 1 :" U1 5: Equally divide the columns of U 1 1 into 2 d parts. For each part, keep the leftmost column unchanged, and set the remains to 0. 6: Equally divide the rows of U 1 1 into 2 m parts. For the i th part (i starts from 0), right shift the contents for i columns. 7 To see the correctness of Algorithm 1, we first consider the case m ě k. It can be easily checked that after step 8, the p2 k p, 2 k q`tq th entry of U 2 1 will store the value of v t,p pU 1 q : v t,q pU 1 q, 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 2 1 " U 2 2 holds to determine whether C 1 " C 2 .
For the case m ă k, the p2 k p, 2 k q`tq th entry of U 2 1 still stores the value of v t,p pU 1 q : v t,q pU 1 q, but only for those with t " 0, 1, ..., 2 m´1 . For t " 2 m , ..., 2 k´1 , the value of v t,q pU 1 q : v t,q pU 1 q does not exist, but we can see that the p2 k p, 2 k q`tq th entry of U 2 1 will always be 0 because the entries in the p2 k q`tq th column of U 1 1 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 " C 2 by checking whether U 2 1 " U 2 2 . 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 pU 1 q'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 for i " d, d`1, ..., d`k´m´1 10: F1 :" F1^yi 11: Apply the inverse circuit C´1 1 on F1 using the method in [8] 12: for i " d, d`1, ..., d`k´1 13: F1 :" F1^xi 14: Repeat step 3 to 13 for C2 and get F2 15: return whether F1 " F2 or not can be simplified and are more efficient. To be precise, two applications of inverse circuit operations U´1 are required, and only Opm`kq 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.

B. Zero-Ancilla Partial Equivalence Checking Algorithm
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 f alse in step 6.
Algorithm 3 PEC BDD noAncilla(C 1 ,C 2 ) Input: C1: C1 " pd, m, 0, U1q, C2: C2 " pd, m, 0, U2q Output: Whether C1 " C2 or not 1: Build the BDDs F representing C1C´1 2 using the method in [8]  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´1 2 . As there may be some gates canceled out in C 1 C´1 2 , Algorithm 3 may be more efficient than Algorithm 2.

VI. EXPERIMENTAL EVALUATION
We implemented Algorithms 2 and 3 in C/C++ under the framework of SliQEC [8], and adopted CUDD [43] package for BDD manipulation. All experiments were conducted on a server with Intel Xeon Silver 4210 CPU at 2.20 GHz and 128 GB RAM. The reported runtime refers to CPU time in seconds. The time-out (TO) limit is set to 600 seconds.
We conducted experiments of partial equivalence checking on benchmarks of period-finding instances, randomly generated instances, Grover search instances, and reversible circuit instances. We also experimented total equivalence checking on randomly generated instances. The results are discussed as follows.

A. Checking Period-Finding Algorithm
We used the tool proposed in [39] to implement the reversible circuits realizing U |xy " |ax mod N y for x ă N and U |xy " |apx`1q´1 mod N y for x ă N , which have the same period with input state |1y. 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 pa, N q pairs for all a P t3, 5, 7, 11u, N P t5, 7, 11, 13u and a ă N . The parameters are set to d " m " 3 and k " rlog 2 N s`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.

B. Checking Random Benchmarks
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 t0.5du, 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 nonexisting. 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 subcircuit 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 " 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 ď d ď 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.
The experimental results are shown in Table III. The runtime and memory usage shown are averaged over the 20 test cases excluding those timed out. As seen, Algorithm 3 can easily scale up to tens of qubits. However, for d ą 20, Algorithm 2 can hardly finish the computation within the time limit. It may be because, for Algorithm 3, F keeps representing a unitary matrix of a quantum circuit almost during the whole process, which may be more "regular" for BDDs to represent. Moreover, due to the structure of C 1 C´1 2 , some gates may be canceled out and the BDDs are more likely to be maintained as an identity matrix, as mentioned in [8]. In contrast, the   entries of the final matrix in Algorithm 2 contain the values of v t,p pU 1 q : v t,q pU 1 q, which can be arbitrary real numbers. Besides, we fix m to t0.5du in our benchmarks, and the second step in Algorithm 2 may further increase the number of qubits. Thus, the runtime and memory usage of Algorithm 2 grow more rapidly than those of Algorithm 3.

C. Checking Reversible Circuits
As mentioned, functionally equivalent reversible circuits without don't-care conditions must be partially equivalent. For those with ancilla inputs, Algorithm 2 is needed. On the other hand, Algorithm 3 is sufficient if no ancilla inputs exist. We used some test cases from RevLib [45] and used Algorithms 2 and 3 to test their partial equivalence to justify this point. The experimental results are shown in Table IV. It is justified that all functionally equivalent reversible circuits are indeed partially equivalent. The runtime and memory usage mainly grow proportional to the gate-count increase.

D. Checking Grover's Algorithm
If reversible circuits are used as part of a quantum circuit, the entire quantum circuit may not be a reversible circuit anymore, and its verification becomes more complex. We took Grover's algorithm as an example for case study. In the experiment, we created a reversible circuit as the oracle function in Grover's algorithm. We also used the way proposed in [38] to implement the same function with one ancilla qubit. Then, Algorithm 2 was applied to check the equivalence of the two circuit. The data qubit number d and measured qubit number m range from d " m " 6, 10, 14, 18, 22, 26.
The experimental results are shown in Table V. The runtime and memory usage grow as d increases. It is reasonable because the circuit size is larger. We note that quantum circuits of Grover's algorithm with the same oracle function but implemented by different reversible circuits are q-equivalent. In this experiment, we show that they are also partially equivalent. Apart from equivalent test cases, we also try to remove one gate from the second circuit to make them not partially equivalent. The runtime and memory usage for nonequivalent test cases are still close to equivalent test cases.

E. Checking Total Equivalent Circuits
Because totally equivalent circuits must be partially equivalent, under these circumstances we use totally equivalent circuits as the benchmarks to test Algorithm 3 and compare it against SliQEC [8]. Because Algorithm 3 is extended from SliQEC, we expect that they would perform similarly. We generated some benchmarks with qubit number d " 10, 20, 30, 40, 50, 60, 70, 80, 90, 100, and set all qubits to be measured qubits for partial equivalence checking. The generating method is similar to how we generate partially equivalent pairs, except that only part H and part T are included to make them totally equivalent. The results shown in Table VI confirm the expectation that Algorithm 3 and SliQEC behave similarly in both runtime and memory usage on these instances.

VII. CONCLUSIONS
In this work, we defined partial equivalence, which is concerned with observational equivalence with respect to partial measurement and a set of initial input states. We obtained the necessary and sufficient conditions of partial equivalence, and exploited them to develop partial equivalence checking algorithms. Experimental results demonstrate the usefulness and strengths of our methods. For future work, it may be interesting to explore partial equivalence in applications such as quantum circuit synthesis and quantum program compilation.