Advanced BDD Optimization

VLSI CADhas greatly bene? ted from the use of reduced ordered Binary Decision Diagrams (BDDs) and the clausal representation as a problem of Boolean Satis? ability (SAT), e. g. in logic synthesis, ver- cation or design-for-testability. In recent practical applications, BDDs are optimized with respect to new objective functions for design space exploration. The latest trends show a growing number of proposals to fuse the concepts of BDD and SAT. This book gives a modern presentation of the established as well as of recent concepts. Latest results in BDD optimization are given, c- ering di? erent aspects of paths in BDDs and the use of e? cient lower bounds during optimization. The presented algorithms include Branch ? and Bound and the generic A -algorithm as e? cient techniques to - plore large search spaces. ? The A -algorithm originates from Arti? cial Intelligence (AI), and the EDA community has been unaware of this concept for a long time. Re- ? cently, the A -algorithm has been introduced as a new paradigm to explore design spaces in VLSI CAD. Besides AI search techniques, the book also discusses the relation to another ? eld of activity bordered to VLSI CAD and BDD optimization: the clausal representation as a SAT problem.