Technical Report No. 102, May 1998 - Abstract

Scholl, Christoph; Becker, Bernd; Weis, Thomas M.
Word-Level Decision Diagrams, WLCDs and Division

Several types of Decision Diagrams (DDs) have been proposed for the verification of Integrated Circuits. Recently, word-level DDs like BMDs, *BMDs, HDDs, K*BMDs and *PHDDs have been attracting more and more interest, e.g., by using *BMDs and *PHDDs it was for the first time possible to formally verify integer multipliers and floating point multipliers of ``significant'' bitlengths, respectively.
On the other hand, it has been unknown, whether division, the operation inverse to multiplication, can be efficiently represented by some type 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 division. Thus, neither a clever choice of the variable ordering, the decomposition type or the edge weights, can lead to a polynomial DD size for division. For the proof we introduce Word-Level Linear Combination Diagrams (WLCDs), a DD, which may be viewed as a ``generic'' word-level DD. We derive an exponential lower bound on the WLCD representation size for integer dividers and show how this bound transfers to all other word-level DDs.