1,721,088 research outputs found
Exact Synthesis of ESOP Forms
No full textWe present an exact synthesis approach for computing Exclusive-or Sum-of-Products (ESOP) forms with a minimum number of product terms using Boolean satisfiability. Our approach finds one or more ESOP forms for a given Boolean function. The approach can deal with incompletely specified Boolean functions defined over many Boolean variables and is particularly fast if the Boolean function can be expressed with only a few product terms. We describe the formalization of the ESOP synthesis problem with a fixed number of terms as a decision problem and present search procedures for determining ESOP forms of minimum size. We further discuss how the search procedures can be relaxed to find ESOP forms of small sizes in reasonable time. We experimentally evaluate the performance of the SAT-based synthesis procedures on completely and incompletely specified Boolean functions.LSI
SAT-Based Exact Synthesis for Multi-Level Logic Networks
Full text linkToday, the design of electronic systems is largely automated. The practice of using software automation technologies for the design of electronic hardware is commonly referred to as Electronic Design Automation (EDA). EDA comprises a large set of tools, from languages that specify high-level hardware designs, to software that determines the layout of nanoscale devices on an integrated circuit. Within this collection, an important role is played by so-called logic synthesis algorithms. A substantial field of research onto itself, logic synthesis can be roughly thought of as the problem of finding good representations for Boolean functions. Such functions are the backbone of digital circuits, which can be thought of, to a first approximation, as devices that compute with Boolean values. In other words, circuits can be viewed simply as large Boolean functions. Logic synthesis, then, is assigned the important task of finding good structural representations for such circuits. Choosing the right logic synthesis algorithm can have a significant impact on the efficiency of an electronic design.
In this thesis, we consider a special type of logic synthesis algorithm known as exact synthesis. Specifically, we analyze and develop multi-level exact synthesis algorithms based on a SAT formulation. Such algorithms attempt to solve a very difficult problem in which, given any Boolean function, they find the optimum (i.e. best possible) circuit that represents it. Our contributions can be roughly split into two parts: (i) core exact synthesis algorithms, and (ii) applications of exact synthesis. In the first part, we start by examining, in detail, different ways to encode the exact synthesis problem into CNF formulas. These formulas are given as input to SAT solvers, which solve them to find solutions. Finally, the solutions to these formulas can be decoded to obtain optimum Boolean circuits. We will compare and contrast the different encodings and show, quantitatively and experimentally, that a proper encoding can greatly influence the efficiency of exact synthesis algorithms. Next, we will show how such exact synthesis algorithms can be improved by adding domain-specific information. This information takes the form of families of DAG topologies which contain some additional structure to guide the SAT solver in its search. Furthermore, using these DAG topology families, we show how the exact synthesis problem can be transformed into an embarrassingly parallel one. This essentially means that, as long as we have processors available, we can throw more and more parallel computing power at the problem to solve it more quickly. After analyzing and improving the core exact synthesis algorithm, we arrive at the second part of the thesis. In this part, we show how exact synthesis can be applied to different problems that are of both theoretical and practical interest. On the theoretical side, we show how exact synthesis can be used to classify Boolean functions in terms of their intrinsic difficulty. On the practical side, we introduce a new data structure and logic representation called XOR-Majority Graphs (XMGs). We use XMGs, in concert with exact synthesis, to develop a novel logic rewriting methodology which achieves significant improvements over the state-of-the-art. We then generalize this methodology into one that can be used to restructure arbitrary Boolean networks, again enabling new improvements in logic synthesis.LSI
Practical Compilation of Quantum Programs
No full textIt's been a little more than 40 years since researchers first suggested exploiting quantum physics to build more powerful computers. During this time, we have seen the development of many quantum algorithms and significant technological advances to make these devices. As a result, at this point, large-scale quantum computers, capable of providing valuable solutions to complex problems, seem like a certainty, even if still distant.
Nonetheless, there is a great gap between the communities of quantum algorithms and quantum devices researchers. On the one hand, algorithm designers most often describe algorithms in a high level of abstraction, using a mixture of natural language, pseudocode, and mathematical formulas---a form deriving asymptotic complexity estimates while shielding researchers from the low-level complexities and restrictions. On the other hand, physical devices only understand algorithms implemented using the primitive low-level abstractions they support.
Most programming systems available for quantum computing are intertwined with the quantum circuit model, so developers must implement algorithms in terms of low-level unitary operators. Not surprisingly, the implementation of quantum algorithms on such a low level of abstraction is very time-consuming, error-prone, and results in non-portable programs---given the technological diversity of quantum devices.
In this thesis, I study problems related to the compilation of quantum programs, seeking forms of augmenting the expressive power of current frameworks and narrowing the gap between algorithmic research and concrete implementations. I focus on scalability and practicality---in particular, together with theoretical investigations, I developed concrete algorithms that are performant and scalable. The embodiment of my research contribution is a compiler companion library for the synthesis and compilation of quantum circuits called tweedledum.LSI
Data Structures and Algorithms for Logic Synthesis in Advanced Technologies
No full textLogic synthesis is a key component of digital design and modern EDA tools; it is thus an essential instrument for the design of leading-edge chips and to push the limits of their performance. In the last decades, the electronic circuits community has evolved dramatically, facing many technological changes. Consequently, EDA and logic synthesis have adapted to accurately design the new generation of digital systems. In the present day, logic synthesis is an important area of research for two main reasons: (i) Diverse ways of computation, alternative to CMOS, have been presented in the last years. Post-silicon technologies have been shown to be feasible and may provide us with better electronic devices. Similarly, novel areas of applications are emerging, ranging from deep learning to cryptography applications. (ii) The current computing and storage means make it possible to solve exactly problems that were only approximated before. Moreover, new reasoning engines, covering from deep learning to new SAT-solvers, can be used as a mean of computation, thus possibly unlocking novel optimization opportunities.
The objective of this thesis is to advance state-of-the-art logic synthesis and present a variety of novel data structures and algorithms, addressing diverse types of applications in modern logic synthesis flows, considering standard CMOS design as well as emerging technology and cryptography.
Motivated by the many emerging technologies that implement majority gates, we first focus on majority-based logic synthesis. We present algorithms over the recently introduced majority-inverter graphs. First, a size optimization flow based on Boolean transformations is proposed. Then, we demonstrate how technology-dependent logic synthesis is an essential step for the abstraction of majority-based emerging technologies and, more important, their technological constraints. Moreover, we advance theoretical results on majority logic. In particular, we mainly focus on the problem of ''how best can the n-argument majority function (majority-n) be realized with a network of 3-input majority gates?'' . For this purpose, we present general upper bounds and decompositions, together with optimum results for majority-5 and -7 and best-known results for the majority-9. In the second part, we shift into more pragmatic results and show practical aspects of logic synthesis, designed to be successful in modern logic synthesis flows. We focus on XOR-based logic synthesis. Motivated by the novel computing capabilities, we propose an optimization flow based on the Boolean difference for area optimization of standard CMOS technologies. Finally, we establish a novel application of logic synthesis to cryptography. It has been demonstrated that the number of AND gates in a xor-and graph (XAG) correlates with the degree of vulnerability (security) of cryptography benchmarks and plays an important role for high-level cryptography protocols. We thus introduce a complete and automatic synthesis flow which consists of the main transformations of logic synthesis but aims instead at minimization of the number of AND gates over XAGs, obtaining significant results over cryptography benchmarks.
We argue that given the progress and novel opportunities of technology, logic synthesis has to be revisited to consider the plurality of primitives and novel engines that can be of interest, and, consequently, the corresponding objective functions and optimisation problems.LSI
Program compilation for large-scale quantum computers
No full textPractical 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.LSI
A Birkhoff connection between quantum circuits and linear classical reversible circuits
Full text linkBirkhoff's theorem tells how any doubly stochastic matrix can be decomposed as a weighted sum of permutation matrices. Similar theorems on unitary matrices reveal a connection between quantum circuits and linear classical reversible circuits. It triggers the question whether a quantum computer can be regarded as a superposition of classical reversible computers
Inversion, Iteration, and the Art of Dual Wielding
No full textThe humble (Formula presented) (“dagger”) is used to denote two different operations in category theory: Taking the adjoint of a morphism (in dagger categories) and finding the least fixed point of a functional (in categories enriched in domains). While these two operations are usually considered separately from one another, the emergence of reversible notions of computation shows the need to consider how the two ought to interact. In the present paper, we wield both of these daggers at once and consider dagger categories enriched in domains. We develop a notion of a monotone dagger structure as a dagger structure that is well behaved with respect to the enrichment, and show that such a structure leads to pleasant inversion properties of the fixed points that arise as a result. Notably, such a structure guarantees the existence of fixed point adjoints, which we show are intimately related to the conjugates arising from a canonical involutive monoidal structure in the enrichment. Finally, we relate the results to applications in the design and semantics of reversible programming languages.</p
Reversible in-place carry-lookahead addition with few ancillae
No full textWe present a reversible, in-place carry-lookahead adder that uses fewer ancillae than previous designs. Specifically, an N-bit adder uses only roughly N ancillae, where previous designs have used roughly 2N ancillae. The cost is 20% higher gate count and 50% higher gate delay.</p
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
