Meta-BDDs: a decomposed representation for layered symbolic manipulation of Boolean functions

Gianpiero Cabodi

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


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.

Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Start Conference Manager
Conference Systems