Manjushri: A Tool for Equivalence Checking of Quantum Circuits

Verifying whether two quantum circuits are equivalent is a central challenge in the compilation and optimization of quantum programs. We introduce $\text{textsc}Manjushri$, a new automated framework for scalable quantum-circuit equivalence checking. $\text{textsc}Manjushri$ uses local projections as discriminative circuit fingerprints, implemented with weighted binary decision diagrams (WBDDs), yielding a compact and efficient symbolic representation of quantum behavior. We present an extensive experimental evaluation that, for random 1D Clifford+$T$ circuits, explores the trade-off between $\text{textsc}Manjushri$ and $\text{textsc}ECMC$, a tool for equivalence checking based on a much different approach. $\text{textsc}Manjushri$ is much faster up to depth 30 (with the crossover point varying from 39–49, depending on the number of qubits and whether the input circuits are equivalent or inequivalent): when inputs are equivalent, $\text{textsc}Manjushri$ is about 10$\times$ faster (or more); when inputs are inequivalent, $\text{textsc}Manjushri$ is about 8$\times$ faster (or more). For both kinds of equivalence-checking outcomes, $\text{textsc}ECMC$'s success rate out to depth 50 is impressive on 32- and 64-qubit circuits: on such circuits, $\text{textsc}ECMC$ is almost uniformly successful. However, $\text{textsc}ECMC$ struggled on 128-qubit circuits for some depths. $\text{textsc}Manjushri$ is almost uniformly successful out to about depth 38, before tailing off to about 75% at depth 50 (falling to 0% at depth 48 for 128-qubit circuits that are equivalent). These results establish that $\text{textsc}Manjushri$ is a practical and scalable solution for large-scale quantum-circuit verification, and would be the preferred choice unless clients need to check equivalence of circuits of depth $>$38.