This dissertation is in the area of Computer-Aided Design (CAD) of digital Integrated Circuits (ICs). Today's digital ICs, such as microprocessors, memories, digital signal processors (DSPs), etc., range from a few thousands to billions of logic gates, flip-flops, and other components, packed in a few millimeters of area. The creation of such highly complex systems would not be possible without the use of CAD tools. CAD tools play the key role in determining the area, speed and power consumption of the resulting circuits. We address several problems related to the logic synthesis step of the CAD flow. First, we investigate properties of double-vertex dominators in directed acyclic graphs. We present an O(n) algorithm for identifying all O(n2) double-vertex dominators of a given vertex, where n is the size of the graph. The key to the algorithm's efficiency is a new data structure for representing double-vertex dominators which has O(n) size and can be efficiently manipulated. This work improves the state of the art in double-vertex dominators identification in terms of both space and time complexity. We also show how dominators can be used for structural decomposition of Boolean functions represented by circuit graphs. Next, we present a depth-optimal technology mapping algorithm for look-up table (LUT) based Field Programmable Gate Arrays. This algorithm is two orders of magnitude faster than previous technology mapping algorithms while achieving solution with a smaller number of LUTs. We also consider level-limited decomposition of Boolean functions which is of particular interest for applications which require circuit representations of a limited depth, such as control logic of microprocessors. We present an efficient algorithm for computing the decomposition of type f = g * h + r, where f, g, h and r are Boolean functions. Another contribution of the dissertation is an algorithm for identifying and removing redundancy in combinational circuits. This algorithm provides a quick partial solution which might be more suitable than exact ATPG and SAT-based approaches for redundancy removal runs at the intermediate steps of the CAD flow. It is embedded into the internal logic synthesis tool of IBM. Other contributions of the dissertation are a proof that, for some Reduced Ordered Binary Decision Diagrams, none of the bound-set preserving orderings is best, a proof of the existence of a perfect input assignment which guarantees that two non-equivalent Boolean functions hash to two different values, and a set of efficient algorithms for the analysis of random Boolean networks. / QC 20100914

Today's EDA (Electronic Design Automation) industry faces enormous challenges. Their primary cause is the tremendous increase of the complexity of modern digital designs. Graph algorithms are widely applied to solve various EDA problems. In particular, graph dominators, which provide information about the origin and the end of reconverging paths in a circuit graph, proved to be useful in various CAD (Computer Aided Design) applications such as equivalence checking, ATPG, technology mapping, and power optimization. This thesis provides a study on graph dominators in logic synthesis and verification. The thesis contributes a set of algorithms for computing dominators in circuit graphs. An algorithm is proposed for finding absolute dominators in circuit graphs. The achieved speedup of three orders of magnitude on several designs enables the computation of absolute dominators in large industrial designs in a few seconds. Moreover, the computation of single-vertex dominators in large multiple-output circuit graphs is considerably improved. The proposed algorithm reduces the overall runtime by efficiently recognizing and re-using isomorphic structures in dominator trees rooted at different outputs of the circuit graph. Finally, common multiple-vertex dominators are introduced. The algorithm to compute them is faster and finds more multiple-vertex dominators than previous approaches. The thesis also proposes new dominator-based algorithms in the area of decomposition and combinational equivalence checking. A structural decomposition technique is introduced, which finds all simple-disjoint decompositions of a Boolean function which are reflected in the circuit graph. The experimental results demonstrate that the proposed technique outperforms state-of-the-art functional decomposition techniques. Finally, an approach to check the equivalence of two Boolean functions probabilistically is investigated. The proposed algorithm partitions the equivalence check employing dominators in the circuit graph. The experimental results confirm that, in comparison to traditional BDD-based equivalence checking methods, the memory consumption is considerably reduced by using the proposed technique. / QC 20100804