Quantum computing, once just a theoretical field, is quickly advancing as physical quantum technology increases in size, capability, and reliability. In order to fully harness the power of a general quantum computer or an application-specific device, compilers and tools must be developed that optimize specifications and map them to a realization on a specific architecture. In this work, a technique and prototype tool for synthesizing algorithms into a quantum computer is described and evaluated. Most recently reported methods produce technologically-independent reversible cascades comprised of a functionally complete set of operators with no regard to actual technologically-dependent cell libraries or constraints due to a device's pre-configured interconnectivity. In contrast, our prototype tool synthesizes algorithms into technologically-dependent specifications that consist of a set of primitives and connectivity constraints present in the computer architecture. The tool performs optimizations based on actual architectural constraints, and a high-quality technology-dependent synthesized result is achieved through the use of optimizing cost functions derived from real hardware and architecture parameters. Additionally, another important aspect of our tool is the incorporation of internal formal equivalence checking that ensures the initially specified algorithm is functionally equivalent to the optimized, technologically-mapped output. Experimental results are provided that target the IBM Q family of quantum computers.
Quantum computing, once just a theoretical field, is quickly advancing as physical quantum technology increases in size, capability, and reliability. In order to fully harness the power of a general quantum computer or an application-specific device, compilers and tools must be developed that optimize specifications and map them to a realization on a specific architecture. In this work, a technique and prototype tool for synthesizing algorithms into a quantum computer is described and evaluated. Most recently reported methods produce technologically-independent reversible cascades comprised of a functionally complete set of operators with no regard to actual technologically-dependent cell libraries or constraints due to a device's pre-configured interconnectivity. In contrast, our prototype tool synthesizes algorithms into technologically-dependent specifications that consist of a set of primitives and connectivity constraints present in the computer architecture. The tool performs optimizations based on actual architectural constraints, and a high-quality technology-dependent synthesized result is achieved through the use of optimizing cost functions derived from real hardware and architecture parameters. Additionally, another important aspect of our tool is the incorporation of internal formal equivalence checking that ensures the initially specified algorithm is functionally equivalent to the optimized, technologically-mapped output. Experimental results are provided that target the IBM Q family of quantum computers.
The models and rules of quantum computation and quantum information processing (QIP) differ greatly from those that govern classical computation, and these differences have caused the implementation of quantum processing devices with a variety of new technologies. Many platforms have been developed in parallel, but at the time of writing, one method of quantum computing has not shown to be superior to the rest. Because of the variation that exists between quantum platforms, even between those of the same technology, there must be a way to automatically synthesize technology-independent quantum designs into forms that are capable of physical realization on a quantum computer (QC) with specific operating parameters. Additionally, results of synthesis must be formally verified to confirm that output technology-dependent specifications are logically identical to their original, technology-independent forms. The first contribution of this work to the field of quantum computing is the creation of such a methodology. Quantum technology mapping and optimization for machines with fixed coupling maps and libraries of gates can be performed with an automatic quantum compiler, and the development and test of this compiler will be explored in this dissertation. Furthermore, this compiler can be considered in a more general context to be a synthesis tool for QIP circuits in a specific realization technology, many of which are capable of implementing systems where the radix of computation, r, is greater than two. As a result of this ability, the second contribution of this work is the presentation of architectures for higher-dimensional quantum entanglement.
Quantum computers capable of practical information processing are emerging rapidly. As these devices become more advanced, tools will be needed for converting generalized quantum algorithms into formally-verified forms that are executable on real quantum machines. In this work, a prototype tool is presented that transforms quantum algorithms into executable specifications where optimization procedures yield 9-24 % cost improvement on a range of benchmarks. Additionally, the tool incorporates formal verification internally with Quantum Multiple-valued Decision Diagrams to confirm that the generated technology-dependent executable is functionally equivalent to the original, technology-independent algorithm. Experimental results are provided that target the Rigetti family of quantum processing units although the tool may also target other architectures.
Realizing a conceptual quantum algorithm on an actual physical device necessitates the algorithm's quantum circuit description to undergo certain transformations in order to adhere to all constraints imposed by the hardware. In this regard, the individual high-level circuit components are first synthesized to the supported low-level gate-set of the quantum computer, before being mapped to the target's architecture-utilizing several optimizations in order to improve the compilation result. Specialized tools for this complex task exist, e.g., IBM's Qiskit, Google's Cirq, Microsoft's QDK, or Rigetti's Forest. However, to date, the circuits resulting from these tools are hardly verified, which is mainly due to the immense complexity of checking if two quantum circuits indeed realize the same functionality. In this paper, we propose an efficient scheme for quantum circuit equivalence checking-specialized for verifying results of the IBM Qiskit quantum circuit compilation flow. To this end, we combine characteristics unique to quantum computing, e.g., its inherent reversibility, and certain knowledge about the compilation flow into a dedicated equivalence checking strategy. Experimental evaluations confirm that the proposed scheme allows to verify even large circuit instances with tens of thousands of operations within seconds or even less, whereas state-of-the-art techniques frequently time-out or require substantially more runtime. A corresponding open source implementation of the proposed method is publicly available at https://github.com/iic-jku/qcec.
Quantum computing is a revolutionary approach to computation that leverages the principles of quantum mechanics, enabling computers to process information in fundamentally different ways than classical computers. Unlike traditional bits, which represent data as either 0s or 1s, quantum bits, or qubits, can exist in multiple states simultaneously due to superposition. Additionally, qubits can be entangled, allowing them to be interconnected in ways that enhance computational power and efficiency. This unique behavior has the potential to run certain types of computation tasks much faster than classical computers can, marking a significant leap forward in technology. When building actual quantum computers to run practical quantum algorithms, one needs efficient ways to map the algorithms to the hardware components, similar to compiling classical algorithms onto CPU/GPU hardware. This thesis aims to tackle some of the important problems in the mapping process. First, can we address hardware errors and algorithm errors at the same time? Second, can we build a better circuit complexity metric to inspire better quantum architecture design, and can we design better quantum algorithms and compilation techniques using this improved metric? Lastly, can we use physics-level simulation results to inspire better circuit-level optimization techniques? We hope to provide positive answers to all three questions above through three separate architectural innovations.
Practical realizations of quantum computers are poised to deliver outstanding computational capabilities far beyond the reach of any classical supercomputer. While classical systems are reliably implemented using CMOS technology, the fabrication of quantum hardware has not yet reached a commercially viable level of maturity. Nowadays, many different technologies are being developed as competing candidates to build the first error-corrected quantum computer. Among the software resources required to operate such a system, quantum compilers translate a high-level description of a quantum algorithm into low-level, technology-dependent quantum instructions. Many quantum algorithms, including Shor's and Grover's algorithms, require to compute some classical logic functions on the quantum computer. The first part of this thesis deals with the problem of compiling quantum circuits that perform such classical Boolean functions, called oracles, into a fault-tolerant set of instructions. Oracle circuits often demand many resources in terms of the number of qubits and gates. The focus is on compiling quantum circuits starting from multi-level logic networks representing large Boolean functions while minimizing the resource footprint of the obtained quantum circuits. At the same time, the trade-off between memory resources and the number of operations typical of such a compilation process is explored. As part of the effort in reducing the resources required to perform a given quantum program, I also present some quantum circuit optimization techniques. The researched algorithms leverage data structures and techniques borrowed and adapted from classical logic synthesis, e.g., SAT solvers, LUT mapping, and multi-level logic networks. I implemented all the compilation algorithms presented in this thesis as part of open-source projects. In particular, I develop and maintain caterpillar---a C++ header-only library dedicated to the quantum compilation of oracles and quantum memory management. The second part of this thesis describes how to equip quantum programming language compilers with automatic accuracy management. Despite the availability of many of such languages, resource estimation of quantum algorithms does not yet support taking approximation errors into account. This general methodology is applicable to any programming language and I demonstrate its integration into the Q# compiler. The technique consists of providing language support to ease the accuracy-aware programming task. The user can define accuracy parameters that will be automatically optimized according to a constraint and a cost function directly generated from the source code. In the presented practical evaluations, the constraint function is the overall allowed accuracy, while the cost function is application-dependent and related to the number of gates. During the optimization process, such functions are evaluated hundreds of times. For this reason, we extract them as (near-)symbolic expressions, whose evaluation time does not depend on the quantum algorithm size. The algorithms and the methodologies presented in this thesis are part of a widespread effort of the research community to build a complete and efficient software stack to program and control the first practical universal quantum computer.
Quantum computing has recently transitioned from a theoretical prediction to a nascent technology. Nevertheless, there is still a gap between the computational ability and reliability of current QIP technologies and the requirements of the first useful quantum computing applications. It will require tremendous efforts and investment to solve the engineering and research challenges to close the gap. Because of the uncertainties and difficulties in relying on hardware breakthroughs, it will also be crucial to close the gap using higher-level quantum optimizations and software-hardware co-design, which could maximally utilize noisy devices and potentially provide an accelerated pathway to real-world quantum computing applications. This thesis develops methods to explore the vast design space for highly optimized and reliable quantum computing architectures and software and focuses on the compilation, verification, and error correction aspects of the quantum computing stack. Specifically, the three main chapters in this thesis discuss, respectively, a direct-to-pulse compiler, a protocol to fault-tolerantly prepare approximate GKP (Gottesman-Kitave-Preskill) qubit states, and a verification framework that helps quantum programmers write provably correct compiler components through formal verification. Though touching many aspects of the stack and based on different technologies in physics and computer science, the majority of this thesis can be connected by a main theme --- improving the efficiency of existing quantum computing stacks by breaking the abstraction between layers in the quantum computing stack.