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 applications.
