Paper Info
Title
K*BMDs: A New Data Structure for Verification
Abstract
Recently, two new data structures have been proposed in the area of Computer Aided Design (CAD), i.e. Ordered Kronecker 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 efficiently, that have a good word-level description, since K*BMDs are a generalization of *BMDs. On the other hand they are also applicable to verification problems at the bit-level. We present experimental results to demonstrate the efficiency of our approach including a comparison of K*BMDs to several other data structures, like EVBDD, OKFDDs and *BMDs. Additionally, experiments on verification of fast multipliers, i.e. multipliers with worst case running time O(log(n)), are reported.
Year
DOI
Venue
1996
10.1109/EDTC.1996.494118
ED&TC
Field
DocType
ISSN
Logic synthesis,Graph theory,Boolean function,Integer,Kronecker delta,Data structure,Discrete mathematics,Multiplicative function,Algorithm,Electronic engineering,Mathematics,Binary number
Conference
1066-1409
ISBN
Citations 
PageRank 
0-8186-7423-7
43
1.68
References 
Authors
18
3
Name
Order
Citations
PageRank
Rolf Drechsler13707351.36
Bernd Becker2431.68
Stefan Ruppertz3763.81