Model Checking @CMU

[Home]

[People]

[Software]

[Publications]

[Support]

[Links]

[Internal]

 

The BDD Library

The BDD library is available in a gzip'ed tar archive:

bddlib.tar.gz (103K)
Clicking on the reference above retrieves the file automatically.

Get bddlib.tar.gz. Uncompress and untar: 


     gunzip -c bddlib.tar.gz | tar xfv -
There are two subdirectories, one called mem and the other called bddlib. Each contains a tar file. After untarring these, build the library in mem (a memory management library) first and then build the BDD library itself. You will need to edit the Makefiles a bit. If you have GNU make, all you need to do is set the variables at the top of the Makefiles to indicate where you want things installed. If you have a more vanilla make, you will also need to fix up the various conditionals within each Makefile and append the file dependencies to the end.

The library is written in C. Its main features include:

  • Stuff for sequential verification, such as routines for relational product and frontier set simplification
  • Unified result cache for all operations. All operations, including things like multi-variable quantification and simultaneous substitution, cache across calls
  • Routines for node profiles (histograms of the number of nodes at each level) and function profiles (histograms of the number of functions obtainable by restricting variables above each level) for analyzing BDD sizes.
  • Routines for dumping BDDs to files and loading them again
  • Some support for multi-terminal BDDs (MTBDDs)
  • Garbage collection via either reference counting or "keep only these"
  • Settable node limit. Operations abort and clean up their intermediates if they cannot finish without the total number of nodes exceeding the limit.
  • Support for dynamic variable reordering. Variables can be automatically shifted around in the middle of operations to minimize the number of nodes in use.
  • Very small and fast. Should be fairly portable across 32-bit machines running UNIX. If you're not running UNIX, you'll have to modify the memory management routines (the package implements a buddy scheme and calls sbrk directly).

    • CMU-SCS Model Checking home page

     

    Please send any comments and suggestions to Nishant Sinha - nishants at cs dot cmu dot edu.