The research seeks to extend the effective use of binary decision diagrams (BDDs), which have already proved an effective method for symbolically representing and manipulating Boolean functions. A number of researchers worldwide have found novel applications of BDDs to such areas as synthesis, formal verification, and testing of digital circuits. Extensions to allow more compact forms and to represent the behavior of arithmetic circuits have improved the performance and extended the range BDDs, leading to a broader class of those diagrams. The U.S. and German group collaborating in this effort have had a synergistic relationship, with each group building on the work of the other. This new effort will enable a more formal collaboration between the two groups.
