K*BMDs: A New Data Structure for Verification
Rolf Drechsler, Bernd Becker, Stefan Ruppertz · 1996
Recently, two new data structures have been proposed in the area of Computer Aided Design #CAD#, i.e. OrderedKronecker Functional Decision Diagrams #OKFDDs# and Multiplicative Binary Moment Diagrams #*BMDs#. OKFDDs are the most general ordered data structure for representing Boolean functions at the bit-level. *BMDs are especially applicable to integer valued functions. In this paper we propose a new data structure, called Kronecker Multiplicative BMDs #K*BMDs#, that is a generalization of OKFDDs to the word-level. Using K*BMDs it is possible to represent functions e#- ciently, that have a good word-level description, since K*BMDs are a generalization of *BMDs. On the other hand they are also applicable to veri#cation problems at the bit-level. We present experimental results to demonstrate the e#ciency of our approach including a comparison of K*BMDs to several other data structures, like EVBDD, OKFDDs and *BMDs. Additionally, experiments on veri#cation of fast multipliers, i.e. mul...