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.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11583/2654247
Attenzione
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo