Introduction

This is an experimental package providing a basis for implementing different variants of binary decision diagrams (BDDs) in C++. Currently, the only supported concrete type of decision diagrams are ordered binary decision diagrams (OBDDs). The package supports the basic operations on these diagrams known from literature, among them boolean binary synthesis and synthesis with the ITE-operator, input and output of BDDs as ASCII text files and import from circuits in SLIF format. Support of complemented edges may be turned on or off by compiler switch.

The main classes of the package are:

• BDDManager: This is a base class realizing binary decision diagrams (BDDs) which have boolean variables and internal nodes with two outgoing edges. It provides low-level data structures and is not intended to be used directly but only through more complete, derived BDD types.

  The class interface consists of protected member functions whose names start with an underscore ("_") such that the respective names can be overriden by concrete versions without underscore in derived classes. This primitive form of inheritance is used instead of a true virtual base class for efficiency reasons.

• OBDD: This is currently the only supported concrete type of BDDs derived from BDDManager. Ordered binary decision diagrams are BDDs with a variable order, multiple labeled start nodes and boolean sinks. This type of BDDs is further described in the section Using the Package.

The original version of the package borrowed many ideas from the BDD package of Brace, Rudell, and Bryant written in C which is still reflected in some of the low-level fine-tuning decisions. (See K. S. Brace, R. L. Rudell, and R. E. Bryant, "Efficient implementation of a BDD package". In Proc. of 27th DAC, 40-45, 1990.)