The problem of extracting small BDDs from function intervals is encountered in several applications. These include the fix point computations used in reachability analysis and model checking, and the design of so-called telescopic units.

We distinguish two sub-problems: In the first, called BDD minimization, an interval is given as either a lower and an upper bound, or as an on-set and a don't care set. A function from the interval with a small BDD is sought.

In the second sub-problem, called subsetting/supersetting, one of the bounds is trivial (zero or one) and the objective is to find a function in the interval that is as close as possible to the non-trivial bound, and has a "better" BDD than the non-trivial bound.

To measure the quality of the result in this second case we normally use the notion of density, that is, the ratio of minterms to nodes of a BDD.

We review classical and recent algorithms for the minimization and subsetting/supersetting problems, and present some work in progress.

Copies of Slides

The slides in MS Powerpoint format

You are not logged in 
©2002-2017 U.C. Regents