Dr. Rolf Drechsler Stefan Ruppertz

Abstract

In this paper 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 well-suited 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 ISCAS85 and ISCAS89 benchmarks.