Equivalence Checking of Sequential Quantum Circuits

Wang, Q; Li, R; Ying, M

Equivalence Checking of Sequential Quantum Circuits

Wang, Q Li, R Ying, M

Permalink

Publisher:: Institute of Electrical and Electronics Engineers
Publication Type:: Journal Article
Citation:: IEEE Transactions on Computer - Aided Design of Integrated Circuits and Systems, 2022, 41, (9), pp. 3143-3156
Issue Date:: 2022-01-01

Closed Access

	Filename	Description	Size
	Equivalence_Checking_of_Sequential_Quantum_Circuits_Accepted version.pdf		934.77 kB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Closed Access

This item is closed access and not available.

Full metadata record

Field	Value	Language
dc.contributor.author	Wang, Q
dc.contributor.author	Li, R
dc.contributor.author	Ying, M https://orcid.org/0000-0003-4847-702X
dc.date.accessioned	2023-02-22T04:30:37Z
dc.date.available	2023-02-22T04:30:37Z
dc.date.issued	2022-01-01
dc.identifier.citation	IEEE Transactions on Computer - Aided Design of Integrated Circuits and Systems, 2022, 41, (9), pp. 3143-3156
dc.identifier.issn	0278-0070
dc.identifier.issn	1937-4151
dc.identifier.uri	http://hdl.handle.net/10453/166313
dc.description.abstract	We define a formal framework for equivalence checking of sequential quantum circuits. The model we adopt is a quantum state machine, which is a natural quantum generalisation of Mealy machines. A major difficulty in checking quantum circuits (but not present in checking classical circuits) is that the state spaces of quantum circuits are continuums. This difficulty is resolved by our main theorem showing that equivalence checking of two quantum Mealy machines can be done with input sequences that are taken from some chosen basis (which are finite) and have a length quadratic in the dimensions of the state Hilbert spaces of the machines. Based on this theoretical result, we develop an (and to the best of our knowledge, the first) algorithm for checking equivalence of sequential quantum circuits with running time O(23m+5l(23m+23l)), where m and l denote the numbers of input and internal qubits, respectively. The complexity of our algorithm is comparable with that of the known algorithms for checking classical sequential circuits in the sense that both are exponential in the number of (qu)bits. Several case studies and experiments are presented.
dc.language	English
dc.publisher	Institute of Electrical and Electronics Engineers
dc.relation	National Natural Science Foundation of China61832015
dc.relation.ispartof	IEEE Transactions on Computer - Aided Design of Integrated Circuits and Systems
dc.relation.isbasedon	10.1109/TCAD.2021.3117506
dc.rights	info:eu-repo/semantics/closedAccess
dc.subject	0906 Electrical and Electronic Engineering, 1006 Computer Hardware
dc.subject.classification	Computer Hardware & Architecture
dc.title	Equivalence Checking of Sequential Quantum Circuits
dc.type	Journal Article
utslib.citation.volume	41
utslib.for	0906 Electrical and Electronic Engineering
utslib.for	1006 Computer Hardware
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Strength - QSI - Centre for Quantum Software and Information
utslib.copyright.status	closed_access	*
pubs.consider-herdc	false
dc.date.updated	2023-02-22T04:30:35Z
pubs.issue	9
pubs.publication-status	Published
pubs.volume	41
utslib.citation.issue	9

Abstract:

We define a formal framework for equivalence checking of sequential quantum circuits. The model we adopt is a quantum state machine, which is a natural quantum generalisation of Mealy machines. A major difficulty in checking quantum circuits (but not present in checking classical circuits) is that the state spaces of quantum circuits are continuums. This difficulty is resolved by our main theorem showing that equivalence checking of two quantum Mealy machines can be done with input sequences that are taken from some chosen basis (which are finite) and have a length quadratic in the dimensions of the state Hilbert spaces of the machines. Based on this theoretical result, we develop an (and to the best of our knowledge, the first) algorithm for checking equivalence of sequential quantum circuits with running time O(23m+5l(23m+23l)), where m and l denote the numbers of input and internal qubits, respectively. The complexity of our algorithm is comparable with that of the known algorithms for checking classical sequential circuits in the sense that both are exponential in the number of (qu)bits. Several case studies and experiments are presented.

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

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