FRAIG: A new datastructure for formal verification and circuit synthesis

Functionally-Reduced And-Inverter Graphs (FRAIGs) can represent Boolean functions and support efficient logic operations, including equivalence checking. FRAIGs and related algorithms are gaining popularity in several applications where Reduced Ordered Binary Decision Diagrams (ROBDDs) and Satisfiability-solvers are used. While empirical results for FRAIGs are convincing and a software implementation is available from UC Berkeley, no theoretical results for FRAIGs are currently known.
Igor L. Markov is an assistant professor of Electrical Engineering and Computer Science at
the University of Michigan. He received his M.A. in Mathematics and Ph.D. in Computer
Science from UCLA.

Prof. Markov's interests are in combinatorial optimization with applications to the
design and verification of integrated circuits, as well as in quantum logic circuits.
Prof. Markov's research contributions include new algorithmic techniques for Boolean
satisfiability, hypergraph partitioning, block packing, large-scale circuit layout,
the synthesis of reversible and quantum circuits, as well as quantum-mechanical simulation
with compressed matrices. Some of these algorithms lead to order-of-magnitude improvements
in practice, and many of them are implemented in software, including open-source projects
and major commercial tools.

Prof. Markov is an associate editor of the ACM SIGDA newsletter and the maintainer of the
online GSRC bookshelf for fundamental CAD algorithms. He has co-authored more than 90
refereed publications. In 2001, Prof. Markov was awarded the DAC Fellowship and received
the IBM University Partership Award. Prof. Markov received the 2004 IEEE CAS Donald O.
Pederson paper-of-the-year award for work on reversible logic, and the 2004 ACM SIGDA
Outstanding New Faculty Award. He won the best paper award at DATE 2005 in the Circuit
Test category, as well as the NSF CAREER and the Synplicity Inc. Faculty Awards.

Prof. Markov served on program committees of most major conferences in Electronic Design
Automation. He was the technical program chair of SLIP 2004, the general chair of SLIP
2005 and a benchmarking chair of IWLS 2005.

Prof. Markov graduated two Ph.D. and two M.S. students, and is now working with seven
graduate students. Current and former students interned at or are employed by AMD,
Amazon.com, Cadence, Calypto, the Department of Defense, US Department
of Energy, Google, IBM, Microsoft, Qualcomm, UC Berkeley, and Synplicity.