Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

IEEE International Conference on Soft Computing and Measurements (SCM)

Quantum circuits specifications design with lexical verification

В. А. Калмычков, Aleksandr V. Krasilnikov, I. V. Matveeva

Published May 1, 2015• 5 citations
Publisher

Abstract

In this paper we present our experience in quantum circuits design automation on the different notations basis. The need of rules and methods for generation of primitive quantum gates sequence for the quantum circuits on the basis of the Linear Nearest Neighbor (LNN) notation is shown. Our lexical verification methodology for quantum circuit specifications in each stage of its design is represented.

DOI
10.1109/scm.2015.7190419

Related papers

Lexical analyzer in CAD for Quantum symbolic model of QFT

Irina V. Matveeva, Anatoly Dorokhov, В. А. Калмычков

In this paper we present our experience in quantum circuits design automation on the example of quantum symbolic model for Quantum Fourier transform (QFT). The lexeme set for base gates is introduced. Our quantum circuit verification by means of lexical analyzer is represented.

IEEE International Conference on Soft Computing and Measurements (SCM)•May 1, 2016•1 citation

Model Design of Quantum Logic Circuits Based on Reed-Muller Expressions

Irina Matveeva, В. А. Калмычков, Anatolii Dorokhov

The article considers the design flow for automatic generation of the quantum circuit model specifications as a fragment of the logical unit of a quantum computer. Reed-Muller expressions is base for this generation. The model representation takes into account the features of the quantum circuit realization in the notation of the linear nearest neighborhood (LNN), the proposed templates provide the automatic selection of the optimal gates composition.

International Russian Automation Conference (RusAutoCon)•Sep 1, 2018•2 citations

Synthesis of Linear Nearest Neighbor Quantum Circuits

Md. Mazder Rahman, Gerhard W. Dueck

This paper presents models for transforming standard reversible circuits into Linear Nearest Neighbor (LNN) architecture without inserting SWAP gates. Templates to optimize the transformed LNN circuits are proposed. All minimal LNN circuits for all 3-qubit functions have been generated to serve as benchmarks to evaluate heuristic optimization algorithms. The minimal results generated are compared with optimized LNN circuits obtained from the post synthesis algorithm --- template matching with LNN templates. Experiments show that the suggested synthesis flow significantly improves the quantum cost of circuits.

arXiv:1508.05430•Aug 21, 2015•19 citations

The basis of design tools for quantum computing

Robert Wille, Lukas Burgholzer, Stefan Hillmich +3 more

Quantum computers promise to efficiently solve important problems classical computers never will. However, in order to capitalize on these prospects, a fully automated quantum software stack needs to be developed. This involves a multitude of complex tasks from the classical simulation of quantum circuits, over their compilation to specific devices, to the verification of the circuits to be executed as well as the obtained results. All of these tasks are highly non-trivial and necessitate efficient data structures to tackle the inherent complexity. Starting from rather straight-forward arrays over decision diagrams (inspired by the design automation community) to tensor networks and the ZX-calculus, various complementary approaches have been proposed. This work provides a look "under the hood" of today's tools and showcases how these means are utilized in them, e.g., for simulation, compilation, and verification of quantum circuits.

arXiv:2301.04147•ACM/IEEE Design Automation Conference (DAC)•Jul 10, 2022•11 citations

Towards the Design Automation of Quantum Circuits

Sidi Mohamed Beillahi

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. \nSpecifically, 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.

•Jun 17, 2016•0 citations

Multithreading programming for FPRM quantum circuits design

I. V. Matveeva, В. А. Калмычков, A. V. Dorokhov

In this paper we examined the separate aspects of design and analysis of the quantum circuits specifications on the computer platforms with the parallelism support. Idea of multi-thread programming for the quantum circuits synthesis and selection is shown, taking into consideration the subsequent use of the Linear Nearest Neighbor (LNN) approach. Our experience on some multi-core platforms is represented.

IEEE International Conference on Soft Computing and Measurements (SCM)•May 1, 2017•1 citation
In this paper we present our experience in quantum circuits design automation on the different notations basis. The need of rules and methods for generation of primitive quantum gates sequence for the quantum circuits on the basis of the Linear Nearest Neighbor (LNN) notation is shown. Our lexical verification methodology for quantum circuit specifications in each stage of its design is represented.
This paper presents models for transforming standard reversible circuits into Linear Nearest Neighbor (LNN) architecture without inserting SWAP gates. Templates to optimize the transformed LNN circuits are proposed. All minimal LNN circuits for all 3-qubit functions have been generated to serve as benchmarks to evaluate heuristic optimization algorithms. The minimal results generated are compared with optimized LNN circuits obtained from the post synthesis algorithm --- template matching with LNN templates. Experiments show that the suggested synthesis flow significantly improves the quantum cost of circuits.
Quantum computers promise to efficiently solve important problems classical computers never will. However, in order to capitalize on these prospects, a fully automated quantum software stack needs to be developed. This involves a multitude of complex tasks from the classical simulation of quantum circuits, over their compilation to specific devices, to the verification of the circuits to be executed as well as the obtained results. All of these tasks are highly non-trivial and necessitate efficient data structures to tackle the inherent complexity. Starting from rather straight-forward arrays over decision diagrams (inspired by the design automation community) to tensor networks and the ZX-calculus, various complementary approaches have been proposed. This work provides a look "under the hood" of today's tools and showcases how these means are utilized in them, e.g., for simulation, compilation, and verification of quantum circuits.
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. \nSpecifically, 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.