Summary: The goal of this project is to implement a reduced-ordered binary decision diagram (ROBDD) package. As opposed to the description in the book, the implementation should contain complement edges. On the other hand some simplifications are introduced to keep the project feasible.

Detailed Description

• Study first Chapter 11 of the book and then the following paper:

Brace, K.S., R.L. Rudell and R.E. Bryant, "Efficient Implementation of a BDD Package", 27th ACM/IEEE Design Automation Conference, pp 40-45, (1990).

as well as Chapter 16 (on hashing) of:

Sedgewick, R., "Algorithms, Second Edition", Addison-Wesley, Reading, Massachusetts, (1988).

• This project does not consider the conversion from an external description; so the function robdd_build (from the book) and the associated formula manipulations do not need to be implemented. The main procedures to implemented from the book are apply_ite, positive_cofactor and negative_cofactor (not explicitly given in pseudo-code in the book) adapted for the use of complement edges as described by Brace et al.
• In the one-person project, you don't necessarily need to implement hashing. You can replace the actual hashing by a linear scan of the list of entries. For the two-person project the implementation of hashing is mandatory.
• Not all issues from the paper by Brace et al. are relevant. You can ignore the more advanced issues like the "computed table", "garbage collection" and the "merging of the unique table and DAG".
• The user interface should be kept simple. It is a textual interface consisting of a variable ordering declaration, calls to "ite" and "print" commands to dump the ROBDD representation of some function. The following conventions are used:
• variables are indicated by x<n> where <n>is a positive integer; examples of variables are: x1, x23, x103.
• functions (the results of calls to "ite") are indicated by F<m>; for example: F23, F4, F534.
• the constant functions are indicated by "0" and "1" (without the surronding quotes) The program is conrolled by an input text file. It has the following structure:
• the first line gives the number of variables
• the second the number of functions
• the third lists all variables in the order as used for ROBDD construction (the top variable first).
• a number of calls (each on a separate line) to the "ite" function using the following syntax: <fun>= ite(<arg>, <arg>, <arg>). Either argument of "ite" <arg> is either a function name, a restricted function name or a variable. For a restricted function name, the following syntax is used for a positive cofactor <fun>+<var> and for a negative cofactor <fun>-<var>.
• a number of calls (each on a separate line) to "print" to dump the ROBDD structure using the syntax: print <fun>. This command prints the properties of each vertex in an ROBDD (per vertex: variable name, whether incoming edge is complemented or not, identifications of low and high children vertices). Example of an input file (the file first defines an AND gate (F1) and an OR gate (F2) and then builds the function F3 = and (or(x3,x4), x2) using "composition", see Equaton 11.12):

  4
  3
  x1 x3 x4 x2
  F1 = ite(x1, x2, 0)  
  F2 = ite(x3, x4, 1)
  F3 = ite(F2, F1+x1, F1-x1)
  print F3

• The test of the program should at least contain a proof of the equivalence of Equations 11.1 and 11.2 from the book. Any other tests (include experiments with different variable orderings) are welcome.