Search

Today, 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.

A Majority-Inverter Graph (MIG) is a directed acyclic graph in which every vertex represents a three-input majority operation and edges may be complemented to indicate operand inversion. MIGs have algebraic and Boolean properties that enable efficient logic optimization. They have been shown to obtain superior synthesis results as compared to state-of-the- art And-Inverter Graph (AIG) based algorithms. In this paper, we extend MIGs to Functionally Reduced MIGs (FRMIGs), analogous to the extension of AIGs to Functionally Reduced AIGs (FRAIGs). This enables the use of MIGs in a lossless synthesis design flow. We present an FRMIG based technology mapper for lookup tables (LUTs). Any MIG may be mapped to a k- LUT network. Using exact synthesis we may decompose the k- LUT network back into an equivalent MIG. We show how LUT mapping and exact k-LUT decomposition can be used to create an MIG optimization method. Finally, we present the results of applying our new optimization method and LUT mapper to both logic optimization and technology mapping.

Majority-inverter graphs (MIGs) are a multi-level logic representation of Boolean functions with remarkable algebraic and Boolean properties that enable efficient logic optimizations beyond the capabilities of conventional logic representations. In this paper, we survey two state-of-the-art logic optimization methods for MIGs: cut rewriting and cut resubstitution. Both algorithms are generic and can be applied to arbitrary graph-based logic representations. We describe them in a unified framework and show experimental results for MIG size optimization using the EPFL combinational benchmark suite.

The study of the complexity of Boolean functions has recently found applications in logic synthesis and optimization algorithms, as for instance in logic rewriting. Previous works have focused on the minimum length of Boolean chains for functions up to 5 inputs, being represented in terms of 2- and 3-input operators. In this work, we study the complexity of selfdual monotone 7-input Boolean functions in terms of 3-input majority operators. We use enumeration-based and SAT-based exact methods to find (i) the minimum number of operators in the shortest formula of a Boolean function, and (ii) the minimum length of its Boolean chain. Different generalizations and restrictions of majority Boolean chains are considered to represent functions. For instance, we consider leafy Boolean chains in which each step has at least one fanin that is an input variable, or majority Boolean chains that use complemented edges.