We propose a BDD based representation for Boolean functions, which extends conjunctive/disjunctive decompositions. The model introduced (Meta-BDD) can be considered as a symbolic representation of k-Layer automata describing Boolean functions. A layer is the set of BDD nodes labeled by a given variable, and its characteristic function is represented using BDDs. Meta-BDDs are implemented upon a standard BDD library and they support layered (decomposed) processing of Boolean operations used in formal verification problems. Besides targeting reduced BDD size, the theoretical advantage of this form over other decompositions is being closed under complementation, which makes Meta-BDDs applicable to a broader range of problems.

Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions / Cabodi, Gianpiero. - 2102:(2001), pp. 118-130. (Intervento presentato al convegno Computer Aided Verification 13th International Conference, CAV 2001 tenutosi a Paris (FRA) nel July 18–22, 2001) [10.1007/3-540-44585-4_11].

Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions

CABODI, Gianpiero
2001

Abstract

We propose a BDD based representation for Boolean functions, which extends conjunctive/disjunctive decompositions. The model introduced (Meta-BDD) can be considered as a symbolic representation of k-Layer automata describing Boolean functions. A layer is the set of BDD nodes labeled by a given variable, and its characteristic function is represented using BDDs. Meta-BDDs are implemented upon a standard BDD library and they support layered (decomposed) processing of Boolean operations used in formal verification problems. Besides targeting reduced BDD size, the theoretical advantage of this form over other decompositions is being closed under complementation, which makes Meta-BDDs applicable to a broader range of problems.
2001
3540423451
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/1408556
 Attenzione

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