Our research on CAD algorithms and design methodologies for extremely large integrated circuits lead to integrated optimizations, such as a unification of partitioning, placement and floorplanning; we have also developed a simultaneous optimization of digital logic and layout by finding and exploiting functional symmetries. Our current work predicts and outlines major changes in how large circuits will be designed in the future. In particular, the dominance of wires over transistors (in terms of delay and power) will lead to devastating global effects, such as buffer flooding --- long wires must be buffered, but the inserted buffers may elongate other wires, thus requiring additional buffers. Such global effects will force a complete merger of logical and physical synthesis, and will also heavily impact micro-architecture. In turn, such a merger necessitates new datastructures that capture both evolving logic and evolving layout, as well as new algorithms to perform such evolution. In our current work, we seek effective solutions to the buffer flood problem, and are developing fully integrated logic and layout optimization at large scale. We are also actively looking at large-scale combinatorial optimization and constraint satisfaction relevant to VLSI applications, such as circuit partitioning and Boolean satisfiability. Our software has been included among CAD tools required for the design of LSI Logic's RapidChip integrated circuits (structured ASICs) and in this context was used to design successful chips at Hewlett Packard, Silicon Graphics, CISCO, Raytheon, Seagate, Fujitsu, Hitachi, 3COM, Nortel Networks, Alcatel, Cryptec and IP Wireless.
It is well-known that worst-case complexity of computational problems does not capture achievable performance in problem-solving because only a very small fraction of inputs can be realistically explored within the age of the universe. In this context, understanding commonly-occuring structure in instances of NP-hard problems offers hope in applications that require solving such instances. To this end, we have performed a comprehensive study of symmetries and symmetry-breaking in instances of Boolean satisfiability, and graph coloring. We developed the world's fastest Graph Automorphism solver that helps finding symmetries in a variety of problems and can be used in conjunction with our efficient techniques to handle symmetries. This often results in dramatic efficiency improvements. In one case (proving the pigeon-hole principle) a provably-exponential complexity was reduced to low-polynomial complexity, both provably and empirically. Significant improvements have been observed in the context of formal verification of digital circuits -- our algorithms are used at Siemens and our software implementation is used at Synopsys. We have also demonstrated speed-ups in SAT solving and formal verification by exploiting two different hypergraph structures extracted from input clauses.
Present technology trends decrease transistor size by a factor of two in less than two years, and will soon reach atomic scales, where physical reality is described by quantum-mechanical effects. While our current work is not concerned with incorporating quantum efforts into traditional circuit design, we are studying a more futuristic concept --- that of quantum circuits. The main difference is that quantum circuits process quantum information rather than zeros and ones, and possess a number of counter-intuitive features of quantum mechanics. Such circuits can break [keys of] the RSA crypto-system in polynomial time, therefore we are interested in understanding the potential and the limits of such quantum speed-ups as well as specific applications where quantum circuits can be useful. To this end, we have implemented a high-performance simulator of quantum circuits that is currently used in close to 20 research institutions in North America, Europe and Asia. It allows one to experiment with quantum circuits and algorithms, and in some cases can handle surprisingly large quantum computations.