Programming Project (for one or two persons): A Simple ROBDD Package
with Complement Edges
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.
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,
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
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
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
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):
x1 x3 x4 x2
F1 = ite(x1, x2, 0)
F2 = ite(x3, x4, 1)
F3 = ite(F2, F1+x1, F1-x1)
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.
Last update on:
Mon Sep 22 11:34:10 CEST 2003