Manipulation of *BMDs

Multiplicative Binary Moment Diagrams (*BMDs) have recently been introduced as a data structure for verification. Using *BMDs it was for the first time possible to verify multiplier circuits with up to 256 bits. In this paper we use a modification of *BMDs, called positive *BMDs (p*BMDs), that allows to apply dynamic variable ordering, that is the most promising minimization technique for decision diagrams, to *BMDs. Furthermore, we study *BMDs representing Boolean functions. We show that in this case for some operations polynomial algorithms can be given, while the general case of integer-valued functions requires exponential effort. Experimental results demonstrate that p*BMDs clearly outperform *BMDs with respect to runtime during dynamic minimization, while keeping (nearly) all advantages