This award supports Dr. Gary Hachtel, the co-PI, Dr. Fabio Somenzi, and a graduate student from the University of Colorado-Boulder in a collaboration with Christopher Meinel of the Department of Information Technology at the University of Trier. Both groups are working on the efficient representation and manipulation of Boolean functions, primarily through the development of Ordered Binary Decision Diagrams (OBDDs). The German group has focused primarily on the theoretical foundations of OBDDs and the connections between OBDDs and complexity theory. The U.S. group has focused on the development of efficient BDD manipulation techniques and their application to synthesis and formal verification. The combined and complementary expertise of the groups promises progress in the efficient implementation of Very Large-Scale Integrated (VLSI) systems. The research is also of importance to current academic and commercial interests in computer-aided instruction.
