Word-level decision diagrams, WLCDs and division
Christoph Scholl, Bernd Becker, Thomas M. Weis · 1998
Several types of Decision Diagrams (DDs) have been proposed for the verijcation of Integrated Circuits. Recently word-level DDs libBblDs, *BhfDs, HDDs, K*BhiDs and *PHDDs have been attracting more and more interest, e.g., by using *BMDsand *PHDDsit wasfor thejrst time possible to formally verifi integer multipliers and Joating point multipliers of "signi&ant" bitlengths, respectively.On the other hat~it has been unhewn, whether division, the operation inverse to multiplication, can be efiiently represented by some ppe of word-level DDs.In this paper we show that the representational power of any word-level DD is too weak to efficiently represent integer divisiok Thus, neither a clever choice of the variable orderins, the decomposition type or the edse weights, can lead to a polynotnial DD size for divisio~ For the proof we introduce Word-Level Linear Combination Dia-gr~(JVLCDS), a DD, which maybe viewed as a "generic" wordlevel DD. \i@derive an uponential lower bound on the WLCD representation sizefor integer dividers atrdshow how this bound transfers to all other word-level DDs.