Equivalence Checking of Quantum Circuits

Hong, Xin

Equivalence Checking of Quantum Circuits

Hong, Xin

Permalink

Publication Type:: Thesis
Issue Date:: 2023

Embargoed

	Filename	Description	Size
	thesis.pdf	thesis	1.95 MB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Embargoed
Open Access

This item is currently unavailable due to the publisher's embargo.

The embargo period expires on 1 Aug 2025

Full metadata record

Field	Value	Language
dc.contributor.author	Hong, Xin
dc.date.accessioned	2024-04-11T03:33:17Z
dc.date.available	2024-04-11T03:33:17Z
dc.date.issued	2023
dc.identifier.uri	http://hdl.handle.net/10453/177717
dc.description	University of Technology Sydney. Faculty of Engineering and Information Technology.	en_US.UTF-8
dc.description.abstract	Equivalence checking plays a crucial role in the electronic design automation processes of classical systems, and as quantum devices and circuits continue to grow in scale, the importance of verifying quantum circuits is growing rapidly. It is anticipated that equivalence checking will also become a vital technique in the quantum realm. In this thesis, we explore various types of equivalence checking, encompassing exact equivalence, approximate equivalence, and symbolic equivalence checking. To facilitate these verification tasks, we introduce a novel data structure called the Tensor Decision Diagram (TDD) as a representation for quantum circuits. The TDD provides a compact and canonical framework for manipulating tensor networks, leveraging the benefits of both decision diagrams and tensor networks. By harnessing the uniqueness and compactness of TDDs, we achieve an efficient and canonical representation that captures the essential information of a circuit while minimising computational and memory complexity. Furthermore, we develop specialised algorithms and tools that utilise TDD representation to verify different types of quantum circuits, including combinational quantum circuits, dynamic quantum circuits, noisy quantum circuits, and parameterised quantum circuits. These tools enable us to perform exact equivalence checking, approximate equivalence checking, and symbolic equivalence checking on quantum circuits, empowering researchers and practitioners to ensure the correctness and functionality of their designs. Additionally, we explore the realm of symbolic execution for quantum circuits, offering a novel approach to verify the behaviour and outputs of quantum circuits with symbolic inputs. This work gives us more opportunities to learn the functionality of a quantum circuit clearly. Moreover, we explore the concept of quantum image computation, which enables the calculation of the image of a subspace under a quantum transition system. This technique provides further verification capabilities for quantum circuits.	en_US.UTF-8
dc.format	Thesis (PhD)
dc.language.iso	en_US	en_US.UTF-8
dc.relation	https://opus.lib.uts.edu.au/bitstream/10453/177717/1/thesis.pdf
dc.rights	info:eu-repo/semantics/embargoedAccess
dc.rights	The author owns the copyright in this thesis including all reproduction and reuse rights for the work. The work may not be altered without the permission of the copyright owner. Attribution is essential when quoting or paraphrasing from this thesis.
dc.rights	© 2023 Xin Hong
dc.rights	au.edu.uts.lib/nph
dc.title	Equivalence Checking of Quantum Circuits	en_US.UTF-8
dc.type	Thesis
utslib.copyright.status	embargoed	*
utslib.copyright.embargo	2025-08-01T00:00:00+1000

Abstract:

Equivalence checking plays a crucial role in the electronic design automation processes of classical systems, and as quantum devices and circuits continue to grow in scale, the importance of verifying quantum circuits is growing rapidly. It is anticipated that equivalence checking will also become a vital technique in the quantum realm. In this thesis, we explore various types of equivalence checking, encompassing exact equivalence, approximate equivalence, and symbolic equivalence checking. To facilitate these verification tasks, we introduce a novel data structure called the Tensor Decision Diagram (TDD) as a representation for quantum circuits. The TDD provides a compact and canonical framework for manipulating tensor networks, leveraging the benefits of both decision diagrams and tensor networks. By harnessing the uniqueness and compactness of TDDs, we achieve an efficient and canonical representation that captures the essential information of a circuit while minimising computational and memory complexity. Furthermore, we develop specialised algorithms and tools that utilise TDD representation to verify different types of quantum circuits, including combinational quantum circuits, dynamic quantum circuits, noisy quantum circuits, and parameterised quantum circuits. These tools enable us to perform exact equivalence checking, approximate equivalence checking, and symbolic equivalence checking on quantum circuits, empowering researchers and practitioners to ensure the correctness and functionality of their designs. Additionally, we explore the realm of symbolic execution for quantum circuits, offering a novel approach to verify the behaviour and outputs of quantum circuits with symbolic inputs. This work gives us more opportunities to learn the functionality of a quantum circuit clearly. Moreover, we explore the concept of quantum image computation, which enables the calculation of the image of a subspace under a quantum transition system. This technique provides further verification capabilities for quantum circuits.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/177717