A Survey of Abstract BDDs

摘要

We survey and unify recent work about abstraction within BDD packages. Abstract BDDs (aBDDs) are obtained from ordinary BDDs by merging BDD nodes whose abstract values coincide. We discuss four types of abstract BDDs (called S-type, 0-type, 1-type and V-type aBDDs) which have found applications in many CAD-related areas such as equivalence checking, variable ordering and model checking. Experimental results demonstrate the usefulness of our method.