Our group focuses on a range of fundamental issues in computing, including major challenges in the design and verification of next-generation integrated circuits (microprocessors, ASICs, SoCs), and obstacles to solving specific instances of hard combinatorial problems arising in design and verification (such as Boolean Satisfiability, ILP, graph coloring, circuit synthesis). We also maintain an active research program in the design and analysis of quantum circuits.

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.

- J. A. Roy and I. L. Markov,
``Seeing the Forest and the Trees: Steiner Wirelength Optimization
in Placement''
(.pdf),
to appear in
*IEEE Trans. on Computer-Aided Design*, 2007. - J. A. Roy, S. N. Adya, D. A. Papa and I. L. Markov,
"Min-cut Floorplacement", (.pdf),
*IEEE Trans. on Computer-Aided Design*, vol.25, no.7, pp. 1313-1326, July 2006. - S. N. Adya et al.,
``Benchmarking for Large-Scale VLSI Placement and Beyond''
(.pdf)
*IEEE Trans. on CAD*, vol.23 no.4, April 2004, pp. 472-488. - A. E. Caldwell, A. B. Kahng, I. L. Markov,
"Optimal Partitioners and End-case Placers for Standard-cell Layout"
(.pdf),
*IEEE Trans. on Computer-Aided Design*, vol.19, no.11, pp. 1304-1314, 2000.

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.

- A. Ramani, F. A. Aloul, I. L. Markov and K. A. Sakallah,
``Breaking Instance-Independent Symmetries in Exact Graph Coloring''
(.pdf),
*Journal of Artificial Intelligence Research*, vol. 26, pp. 191-224, 2006. - A. Ramani and I. L. Markov,
``Automatically Exploiting Symmetries in Constraint Programming'',
(.pdf)
*Symmetries in Constraints*(SymCon) Toronto 2004. - D. B. Motter, J. A. Roy, and I. L. Markov,
``Resolution Cannot Polynomially Simulate Compressed-BFS''
(.pdf),
*Annals of Mathematics and Artificial Intelligence*, vol.44, no.1-2, pp. 121-166, May 2005. - F. A. Aloul, A. Ramani, I. L. Markov and K. A. Sakallah,
``Solving Difficult Instances of Boolean Satisfiability
in the Presence of Symmetry''
(.pdf),
*IEEE Trans. on CAD*, vol. 22(9), Sept 2003, pp. 1117-1137. - F. A. Aloul, A. Ramani, I. L. Markov and K. A. Sakallah,
``Generic ILP versus Specialized 0-1 ILP: an Update'',
(.pdf)
in Proc.
*ACM/IEEE Intl. Conf. Comp.-Aided Design (ICCAD)*, pp. 450-457, November 2002.

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.

- G. F. Viamontes, I. L. Markov and J. P. Hayes,
``Is Quantum Search Practical?''
(.pdf),
*IEEE/AIP Computing in Science and Engineering*, May/June 2005, pp. 62-70. - V. V. Shende, S. S. Bullock, I. L. Markov,
``Synthesis of Quantum Logic Circuits''
(.pdf),
*IEEE Trans. on Computer-Aided Design*, vol.25, no.6, June 2006, pp. 1000-1010. - V. V. Shende and I. L. Markov,
``Quantum Circuits for Incompletely Specified Two-Qubit Operators''
(.pdf),
*Quantum Information and Computation*, vol.5, no.1, pp. 49-57, January 2005. - G. F. Viamontes, I. L. Markov and J. P. Hayes,
``Graph-based Simulation of Quantum Computation
in the Density Matrix Representation''
(.pdf),
*Quantum Information and Computation*, vol.5, no.2 pp. 113-130, February 2005.