Collaborative Research: SPV: Synthesis, Profiling, and Verification of Quantum Circuits

About This Grant

Today's quantum circuit designs are akin to classical circuits in their early stages, which were designed by hand and manually laid out, while the power of classical computing hardware was not fully unleashed until the emergence of Electronic Design Automation (EDA) in the 1950s, enabling the scalable design of integrated circuits. Although quantum computing holds great promise to dramatically speed up many chemical, financial, cryptographic, and machine-learning applications, we are witnessing that the existing quantum computing design workflow significantly relies on human designs, such as manually implementing and verifying quantum circuits on the gate level for quantum algorithms. As such, domain experts from other fields without a sufficient fundamental understanding of quantum operations can hardly leverage the power of quantum computers for their domain applications, and more importantly, they lack toolkits to test the correctness of an ad-hoc designed quantum circuit. Furthermore, since quantum computing has a fundamentally different computing scheme, which relies on superposition and entanglement, the traditional EDA techniques cannot be directly applied to quantum circuits. To close the gap between quantum hardware (in physics) and quantum algorithms (in computer science), we envision the necessity of a quantum EDA framework, which will play a role similar to that of EDA in revolutionizing classical Silicon-based hardware design. Beyond the technical impact, the fundamentals of the design automation tools can help beginners understand how a quantum system is designed and how it works, which are compiled in the education activities in this project for public access. To carry out pilot research on the quantum EDA, this project proposes to develop an automated framework, namely SPV, to efficiently synthesize, profile, and verify quantum circuits, which include a set of quantum EDA tools: (1) We develop an automated quantum circuit construction toolset to optimize quantum circuit design in modern quantum processors. The toolset supports end-to-end quantum circuit design, including both quantum state preparation and function synthesis using available quantum gates. (2) We develop both formal and simulation-based approaches to verify quantum circuits at scale. Specifically, we utilize the widely adopted ZX calculus to optimize quantum circuits for equivalence checking, and we develop a scalable, simulation-based verification methodology tailored for larger circuits. Moreover, it will comprise methodologies to verify quantum circuits in the presence of quantum error correction (QEC). And (3) we build a benchmark test platform with circuit property profiling and performance validation. To address the shortage of QEC designs in existing benchmarks for quantum verification, we integrate a set of state-of-the-art QEC code designs into the benchmark tool. After all the synthesis, profiling, verification, and benchmarking tools are developed, we integrate them into a holistic quantum design automation toolchain. With a completed toolchain, SPV can benefit researchers in deploying and testing domain-specific quantum algorithms on available quantum computers. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.