Binary decision diagrams (BDDs) are the state-of-the-art core technique for the symbolic representation and manipulation of Boolean functions, relations and finite sets. Many applications resort to them in the field of CAD, but size and time complexity are a strong limitation to a wider applicability. In this paper we primarily address the problem of memory limits. In particular, we first include an experimental observation of memory usage and running time for some basic operators used in reachability analysis of finite state machines. Then we describe how disjunctive partitioning allows us to decompose large problems into sub-problems. Finally, we show the benefits in terms of memory requirements, CPU time, and overall performance.
Reducing Operation Complexity in Symbolic Techniques throughPartitioning / Cabodi, Gianpiero; Camurati, Paolo Enrico; Quer, Stefano. - STAMPA. - 6:(1998), pp. 322-325. (Intervento presentato al convegno ISCAS'98: IEEE International Symposium on Circuits and Systems tenutosi a Monterey, California, US nel June 1998) [10.1109/ISCAS.1998.705276].
Reducing Operation Complexity in Symbolic Techniques throughPartitioning
CABODI, Gianpiero;CAMURATI, Paolo Enrico;QUER, Stefano
1998
Abstract
Binary decision diagrams (BDDs) are the state-of-the-art core technique for the symbolic representation and manipulation of Boolean functions, relations and finite sets. Many applications resort to them in the field of CAD, but size and time complexity are a strong limitation to a wider applicability. In this paper we primarily address the problem of memory limits. In particular, we first include an experimental observation of memory usage and running time for some basic operators used in reachability analysis of finite state machines. Then we describe how disjunctive partitioning allows us to decompose large problems into sub-problems. Finally, we show the benefits in terms of memory requirements, CPU time, and overall performance.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11583/2501448
Attenzione
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo