QuaSi: A Scalable and Reliable Quantum Simulation-based Equivalence Checking Framework

Quantum circuit transpilation facilitates the decomposition of complex operations into simpler hardware-compatible gates. This results in significant changes to the input circuit, and consequently, it becomes imperative to verify the correctness of the transpilation process. Quantum circuit equivalence checking is used to verify the operational equivalence of large quantum circuits to ensure the correctness of computation. Although small quantum circuits can be simulated easily on a classical computer without transpilation, this approach is unscalable for larger, more complex quantum circuits. Furthermore, a scalable quantum equivalence checking algorithm exhibiting subpar performance when applied to larger quantum circuits lacks reliability. Therefore, an equivalence-checking algorithm with scalability and acceptable performance is necessary to verify large quantum circuits. In this paper, we propose QuaSi, a simulation-based verification methodology designed to generate distinct test cases to achieve a scalable and reliable quantum circuit equivalence-checking. Our proposed approach surpasses existing state-of-the-art simulation-based methodologies by boosting the success rate of verification, in addition to reducing the verification latency. When evaluating using large benchmarks with up to 130 qubits, QuaSi furnished significantly improved performance compared to existing approaches in all types of scenarios. Furthermore, we proposed an algorithm to locate the erroneous gates to facilitate debugging the transpilation process.