Summary

An Introduction to Binary Decision Diagrams by Henrik Reif Andersen

CUDD: Manipulating BDDs, ADDs and ZDDs, variable reordering methods.

BuDDy: Dynamic variable reordering

JavaBDD: based on BuDDy, Object-Oriented, advanced variable reordering.

bddbddb: Program Analysis, implemented with JavaBDD, Datalog Programming Language

PPBF: parallel, breadth-first manipulation algorithm, unfinished

CAL: breadth-first manipulation algorithm

CUDD

Introduction

CU Decision Diagram Package

CUDD is a package for the manipulation of Binary Decision Diagrams (BDDs), Algebraic Decision Diagrams (ADDs) and Zero-suppressed Binary Decision Diagrams (ZDDs). BDDs are used to repre- sent switching functions; ADDs are used to represent functions from {0, 1}^n to an arbitrary set. ZDDs represent switching functions like BDDs; how- ever, they are much more efficient than BDDs when the functions to be represented are characteristic functions of cube sets, or in general, when the ON-set of the function to be represented is very sparse. They are inferior to BDDs in other cases. The package provides a large set of operations on BDDs, ADDs, and ZDDs, functions to convert BDDs into ADDs or ZDDs and vice versa, and a large assortment of variable reordering methods. The CUDD package can be used in three ways:

  • As a black box. In this case, the application program that needs to manipulate decision diagrams only uses the exported functions of the package. The rich set of functions included in the CUDD package allows many applications to be written in this way.

  • As a clear box. When writing a sophisticated application based on decision diagrams, efficiency often dictates that some functions be im- plemented as direct recursive manipulation of the diagrams, instead of being written in terms of existing primitive functions.

  • Through an interface. Object-oriented languages like C++ and Perl5 can free the programmer from the burden of memory management. A C++ interface is included in the distribution of CUDD. It automati- cally frees decision diagrams that are no longer used by the applica- tion and overloads operators. Almost all the functionality provided by the CUDD exported functions is available through the C++ inter- face, which is especially recommended for fast prototyping.

Two CUDD extensions are available via anonymous FTP from vlsi.Colorado.EDU.

  • PerlDD is an object-oriented Perl5 interface to CUDD. It is organized as a standard Perl extension module. The Perl interface is at a some- what higher level than the C++ interface, but it is not as complete.

  • DDcal is a graphic BDD calculator based on CUDD, Perl-Tk, and dot.

Source Code Documentation

User Manual

Download Package

BuDDy

Introduction

The BDD package presented here was made as part of a ph.d. project on model checking of finite state machines. The package has evolved from a simple introduction to BDDs to a full blown BDD package with all the standard BDD operations, reordering and a wealth of documentation. The package is extremely simple to use; for C/C++ programs you just include “bdd.h” and link with “bdd” and then you are up and running. With the C++ interface you don’t even have to think about reference counting and garbage collection.

BuDDy has been used succesfully to verify finite state machine systems with up to 1400 concurrent machines working in parallel (see the paper “Verification of Large State/Event systems Using Compositionality and Dependency Analysis”, Tools and Algorithms for the Construction and Analysis of Systems ‘98 (TACAS’98). LICS 1384, Springer-Verlag).

Projects for integrating BuDDy with both Moscow ML and New Jersey ML have resulted in really efficient BDD operations in ML. See the MuDDy page for more information. BuDDy is now also part of the HOL theorem prover!

Highlights

  • All standard BDD operations (and, or, ite, replace, quantification, support, compose etc.)
  • Many highly efficient vectorized BDD operations.
  • Dynamic variable reordering.
  • Dumps BDD as input for the graph printing program DOT.
  • Lots of printing functions.
  • Automated garbage collection.
  • A C++ interface with automatic reference counting.
  • An interface for encoding integer values and arithmetics with BDDs.
  • Compiles on both Unix and Windows NT/9x platforms.

Source Code with documentation

JavaBDD

JavaBDD is a Java library for manipulating BDDs (Binary Decision Diagrams). Binary decision diagrams are widely used in model checking, formal verification, optimizing circuit diagrams, etc. For an excellent overview of the BDD data structure, see this set of lecture notes by Henrik Reif Andersen.

The JavaBDD API is based on that of the popular BuDDy package, a BDD package written in C by J?rn Lind-Nielsen. However, JavaBDD’s API is designed to be object-oriented. The ugly C function interface and reference counting schemes have been hidden underneath a uniform, object-oriented interface.

JavaBDD includes a 100% Java implementation. It can also interface with the JDD library, or with three popular BDD libraries written in C via a JNI interface: BuDDy, CUDD, and CAL. JavaBDD provides a uniform interface to all of these libraries, so you can easily switch between them without having to make changes to your application.

JavaBDD is designed for high performance applications, so it also exposes many of the lower level options of the BDD library, like cache sizes and advanced variable reordering.

Source Code

Package for Linux

bddbddb

Introduction

bddbddb stands for BDD-Based Deductive DataBase. It is an implementation of Datalog, a declarative programming language similar to Prolog for talking about relations. What makes bddbddb unique is that it represents the relations using binary decision diagrams (BDDs). BDDs are a data structure that can efficiently represent large relations and provide efficient set operations. This allows bddbddb to efficient represent and operate on extremely large relations - relations that are too large to represent explicitly.

We use bddbddb primarily as a tool for easily and efficiently specifying program analyses. We represent the entire program as database relations. Developing a program analysis becomes as simple as writing the specification for the analysis in a declarative style and then feeding that specification to bddbddb, which automatically transforms your specification into efficient BDD operations.

Using bddbddb for program analysis has a number of advantages:

  • First, it closes the gap between the algorithm specification and its implementation. In bddbddb, the algorithm specification is automatically translated into an implementation, so as long as your algorithm specification is correct you can be reasonably sure that your implementation will also be correct.

  • Second, because BDDs can efficiently handle exponential relations, it allows us to solve heretofore unsolved problems in program analysis, such as context-sensitive pointer analysis for large programs.

  • Third, it makes program analysis accessible, and dare I say it, actually fun. Trying out a new idea in program analysis used to be confined to the realm of experts and compiler writers, and would take weeks to months of tedious effort to implement and debug. With bddbddb, writing a new analysis is simply a matter of writing a few straightforward inference rules. The tool takes care of most of the tedious part and helps you develop powerful program analyses easily.

bddbddb was written by John Whaley, a Ph.D. student working in the Stanford SUIF Compiler group, as part of his research with Professor Monica Lam. He releases this software as open source with the hope that it will take program analysis to a new level by accelerating the development of new advanced analyses, enabling non-specialists to easily develop their own program analyses, and facilitating collaboration between programming language researchers.

Source Code Documentation

Using Datalog with Binary Decision Diagrams for Program Analysis

bddbddb Slides: Using Datalog and BDDs for Program Analysis

Alias Analysis with bddbddb

Download Package

Checkout source code by:

svn checkout https://svn.code.sf.net/p/bddbddb/code/trunk bddbddb-code

PBF of Bwolen Yang

This package is a parallel BDD package based on partial breadth-first expansion. PPBF targets small scale Symmetric Multi-Processor (SMP) machines. Currently, only combinational operations are implemented.

This package uses posix thread interface and require shared memory support (in either hardware or software). It is targeted for small scale symmetric multi-processor (SMP) systems. For distributed shared memory (DSM) systems, I tested this on SGI’s Origin 2000 and found this package performs poorly. For SMPs like SGI Power Challenge (8 procesoors), Sun’s Ultra Enterprise 3000 (6 processors), DEC 8400 (4 processors), and 200MHz PentiumPro (2 processors) machines, PPBF gets close to speedups of 2 on 2 processors and around 3 on 4 processors and up to 4 on 8 processors.

CAL

CAL (dedicated to our alma-mater) BDD package provides routines for manipulating BDDs based on breadth-first manipulation algorithm. Download

Geert Janssen’s BDD package

Download

BDD package in groundness analyser

Github