Formal verification of quantum logic circuits

Formal Verification of Quantum Logic Circuits: Algorithms and Software Tools (DP220102059)

Aims and background

The rapid growth of quantum computing hardware makes it a timely task to develop verification techniques for quantum hardware design and quantum compilers. While we have seen important works on synthesis and optimisation, verification of quantum circuits is still underdeveloped. 

The project aims to develop a comprehensive theory and effective techniques for formal modelling, equivalence checking, and model checking of quantum circuits. 

Almost all digital devices contain (classical) sequential circuits. Recently, the sequential circuit model has also started to play an essential role in quantum computing (for example, the RUS (Repeat-Until-Success) scheme [1] physically implemented on superconducting qubits [2]). However, current research on quantum hardware verification is limited to considering combinational circuits, leaving the verification of sequential quantum circuits totally unexplored.

Building upon our previous work on model checking quantum systems [3], this project will research the verification of both combinational and sequential quantum circuits.

Our aims are:

1. To develop formal representation of combinational and sequential quantum logic circuits.
2. To design efficient algorithms and effective prototype software tools for verification of quantum circuits.

Research objectives

1. The first objective is to establish a comprehensive theory of tensor network based decision diagrams (TDDs) and use TDD as a compact data structure in the verification of (combinational and sequential) quantum circuits, with and without noise. Specifically, studying the construction, addition, multiplication, contraction, and optimisation of parameterised TDDs, and developing equivalence checking and model checking algorithms based on TDD representation of quantum circuits.
2. The second objective is to systemically build the theory and techniques for verification of sequential quantum circuits. To be precise, by investigating two semantic models for sequential quantum circuits with different memory systems and then studying the (approximate) equivalence checking of them. Model checking techniques will also be developed for more general properties of sequential quantum circuits, other than equivalence.
3. The third objective is to develop efficient prototype software tools for the verification of quantum hardware design and circuit optimisation in quantum compilers. Specifically, the plan is to implement basic functions and optimisation techniques of TDDs in C++. Verification algorithms developed in the preceding objectives will be implemented and tested on existing quantum circuit benchmarks. Interfaces to existing quantum computing platforms such as IBM’s Qiskit and Google’s CirQ will be provided.

Expected outcomes

The successful development of the algorithms and software tools proposed in this project will significantly advance the knowledge on formal verification of quantum circuits and help Australian quantum startups build and maintain an internationally leading position in the rapidly emerging quantum electronic design automation (EDA) industry.

Investigators

• QSI’s Distinguished Professor Mingsheng Ying (CI)
• QSI’s Professor Yuan Feng (CI)
• QSI’s Professor Sanjiang Li (CI)
• A/Prof Robert Rand (PI) of The University of Chicago

Dates

December 2022 to December 2025

PhD Scholarships

PhD scholarships are available. Interested students may contact Yuan (yuan.feng@uts.edu.au) and Sanjiang (sanjiang.li@uts.edu.au).

References

[1] Bocharov, A., Roetteler, M., and Svore, K. M. (2015). Efficient synthesis of universal repeat-until-success quantum circuits. Phys. Rev. Lett., 114:080502.

[2] Ryan, C. A., Johnson, B. R., Rist`e, D., Donovan, B., and Ohki, T. A. (2017). Hardware for dynamic quantum computing. Review of Scientific Instruments, 88(10):104703.

[3] Ying, M. and Feng, Y. (2021). Model Checking Quantum Systems: Principles and Algorithms. Cambridge University Press.