Login | Register

Towards the Design Automation of Quantum Circuits


Towards the Design Automation of Quantum Circuits

Beillahi, Sidi Mohamed (2016) Towards the Design Automation of Quantum Circuits. Masters thesis, Concordia University.

[thumbnail of Beillahi_MASc_F2016.pdf]
Text (application/pdf)
Beillahi_MASc_F2016.pdf - Accepted Version
Available under License Spectrum Terms of Access.


Quantum mechanics based computing systems are expected to have high capabilities and are considered good candidates to replace classical cryptography and supercomputing systems. Among many implementations, quantum optics systems provide a promising platform to implement universal quantum computers, since they link quantum computation and quantum communication in the same framework. Recently, several quantum gates, circuits, and protocols have been experimentally realized using optics. Despite the fact that big advances in building the physical quantum computers were achieved, there are no currently available industrial computer aided tools that can perform the modeling, analysis, and verification of optical quantum computing systems. In this thesis, we tackle the idea of design automation for quantum circuits, where we use a sound language, higher order logic, to model and reason about quantum circuits formally. In particular, we propose a framework for the hierarchical modeling and automated verification of quantum computing circuits. The modeling approach captures quantum models built hierarchically from quantum gates, which models are readily available in a library. The analysis and verification of composed circuits is done seamlessly based on dedicated mathematical foundations formalized in the theorem prover.
Specifically, the tensor product and linear projection are used to extract the quantum circuit outputs. Subsequently, a rich library of quantum gates which includes 1-qubit, 2-qubit, and 3-qubit gates is formalized. In order to automate the analysis process, we developed a decision procedure to eliminate the need of user guidance throughout the formal proofs. To demonstrate the effectiveness of the proposed framework, we conduct the formal analysis of a benchmark of quantum circuits including the Shor's integer factorization algorithm, the Grover's oracle, and the quantum full adder.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Beillahi, Sidi Mohamed
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Date:17 June 2016
Thesis Supervisor(s):Tahar, Sofiène
ID Code:981375
Deposited On:08 Nov 2016 14:49
Last Modified:26 Aug 2019 20:39
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top