Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits

Arun Govindankutty, Sudarshan K. Srinivasan

We present a scalable formal verification methodology for Quantum Phase Estimation (QPE) circuits. Our approach uses a symbolic qubit abstraction based on quantifier-free bit-vecto…