Ordered Binary Decision Diagrams (OBDDs) are the first choice in manipulating and representing Boolean functions in CAD. Since the size of an OBDD heavily depends on the chosen variable order, much effort is spent in finding good and improving existing variable orders. If these optimizing techniques are used in OBDD applications, one has to cope with OBDDs of different variable orders very often (e.g., representing the transition relation and the reachable state set in sequential verification). For an efficient manipulation and represention of OBDDs as a multi rooted OBDD, a common variable order is desired. In this paper we present approaches for the solution of the multiple variable order problem, i.e., we present heuristics that compute a well suited intermediate variable order based on the original variable orders of the involved OBDDs.

Binary Decision Diagrams and the Multiple Variable Order Problem / Cabodi, Gianpiero; Quer, Stefano; Meinel, C.; Sack, H.; Slobodova, A.; Stangier, C.. - STAMPA. - (1998). (Intervento presentato al convegno IEEE/ACM International Workshop on Logic Synthesis (IWLS 1998) tenutosi a Lake Tahoe, California, USA nel June 1998).

Binary Decision Diagrams and the Multiple Variable Order Problem

CABODI, Gianpiero;QUER, Stefano;
1998

Abstract

Ordered Binary Decision Diagrams (OBDDs) are the first choice in manipulating and representing Boolean functions in CAD. Since the size of an OBDD heavily depends on the chosen variable order, much effort is spent in finding good and improving existing variable orders. If these optimizing techniques are used in OBDD applications, one has to cope with OBDDs of different variable orders very often (e.g., representing the transition relation and the reachable state set in sequential verification). For an efficient manipulation and represention of OBDDs as a multi rooted OBDD, a common variable order is desired. In this paper we present approaches for the solution of the multiple variable order problem, i.e., we present heuristics that compute a well suited intermediate variable order based on the original variable orders of the involved OBDDs.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/2654247
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo