Manipulation algorithms for K*BMDs

Abstract

Bit-level and word-level based Decision Diagrams (DDs) have led to significant advances in the area of Computer Aided Design (CAD). Recently, a new data structure for the word-level, called Kronecker Multiplicative BMDs (K*BMDs), has been presented. We study manipulation algorithms for K*BMDs: Using K*BMDs it is possible to represent functions efficiently, that have a good word-level description (like multipliers). On the the other hand K*BMDs are also applicable to verification problems at the bit-level. We clarify the relation between bit- and word-level representation which is of importance in particular in the context of verification. Experiments show that *BMDs are not wellsuited for the bit-level. On the other hand OBDDs are not applicable on the word-level. We present algorithms that allow to dynamically switch between bit-level and word-level. We discuss a method for changing the decomposition type and variable order. First experiments demonstrate the efficiency of K*BMDs as a data structure that is suitable for bit-level and word-level functions as well, e.g. K*BMDs can efficiently represent all of the LGSynth91, ISCAS85, and ISCASS9 benchmarks.