Applications of Multi-Terminal Binary Decision Diagrams
Edmund M. Clarke, Masahiro Fujita, Xudong Zhao · 1995
Functions that map boolean vectors into the integers are important for the design and verification of arithmetic circuits. MTBDDs and BMDs have been proposed for representing this class of functions. We discuss the relationship between these methods and describe a generalization called hybrid decision diagrams which is often much more concise. The Walsh transform and Reed-Muller transform have numerous applications in computeraided design, but the usefulness of these techniques in practice has been limited by the size of the boolean functions that can be transformed. Currently available techniques limit the functions to less than 20 variables. In this paper, we show how to compute concise representations of the Walsh transform and Reed-Muller transform for functions with several hundred variables. We show how to implement arithemetic operations efficiently for hybrid decision diagrams. In practice, this is one of the main limitations of BMDs since performing arithmetic operations on fu...