Equivalence test and ordering transformation for parity-OBDDs of different variable ordering

Abstract

Ordered binary decision diagrams (OBDDs) have already proved useful for example in the verification of combinational and sequential circuits. But the applications are limited, since the decriptive power of OBDDs is limited. Therefore several more general BDD models are studied. In this paper the so-called Parity-OBDDs are considered. The two polynomial time algorithms given are motivated by the fact that Parity-OBDD representation size essentially depends on the variable ordering. The one decides the equivalence of two Parity-OBDDS of possibly distinct variable ordering. The other one transforms a Parity-OBDD with respect to one variable ordering into an equivalent Parity-OBDD with respect to another preassigned variable ordering.