Ordered binary decision diagrams have already proved useful for example in the verification of ocmbinational 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 tow polynomial time algorithms given are motivated by the fact that Parity-OBDD representation size essentially dependson the variable ordering. The one decides the equivalence oftwo Parity-OBDDs of possibly disinct 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.
展开▼
