LOCAL CUDD Tutorial

This page is intended as a guide to using CUDD, at a VERY simple level. Please note the links to the "official" CUDD documentation along the left. These pages were created by Jackie Rice, please email j.rice@uleth.ca if you have any comments.

CUDD stands for Colorado University Decision Diagram, and is a package of functions for use with manipulating decision diagrams (BDDs, ADDs and ZBDDs). It was written by Fabio Somenzi at the Dept. of Electrical and Computer Engineering, U of Colorado at Boulder. I take no credit whatsoever for any thing in this package!!

All examples below are based on version 2.1.2, although as you can see version 2.3.1 and now 2.4.0 is now available (and recommended). UPDATE: CUDD 2.4.0 is installed here at the University of Lethbridge. The links below to the function headers connect to the local documentation, which is for version 2.3.1. On the left I have created links to the new documentation from the University of Colorado; this is not a local copy.

In order to use the package you must know where the include files and libraries have been installed. In your source code you must have the following:

 #include <cudd.h> 

In your makefile you must link in all of the libraries util, mtr and st. See the sample makefile for an example.

Programming with CUDD

There are many complex routines available in the CUDD package. Most of these routines are used for reordering, or for building ADDs or ZDDs. The sample program shows how the reordering routines may be used, but only uses BDDs. Please see the user manual or programmer's manual for info on creating ADDs or ZDDs.

The basic use of CUDD is easy: you initialize a DdManager using Cudd_Init, you create your DD (see below), do some reordering, and then shut down the DdManager using Cudd_Quit(DdManager* ddmanager).

The hardest part of using CUDD is creating the DD. Once that is done, the routines supplied in the package are quite straightforward to use. The sample program that I have written reads in a list of cubes from a file, and builds the BDD from this list. The file may have more than one output, so my program must keep track of the DDManager object that manages all the BDDs, and of a list of DDNodes that are the roots of the DD for each function. The sample below shows the basics:

  // -----------------------------------------------
  // first build a DD for just this cube, call it cube
  // -----------------------------------------------

  DdNode *cube, *var, *tmp, *tmp2;

  cube = Cudd_ReadOne(ddman);
  Cudd_Ref(cube);

  for (int i=0; i<numvars; i++) {
    switch(inputs[ordering[i]])
    {
    case '0':
      var = Cudd_Not(Cudd_bddIthVar(ddman,i)); 

if it's a zero, create a new variable for that index level, and invert it.

      break;
    case '1':
      var = Cudd_bddIthVar(ddman, i); 

if it's a one in the cube, create a new variable for that index level.

      break;
    case '-':
      var = Cudd_ReadOne(ddman);
      break;
    } 

if it's a don't care value, create the constant 1 node.

    tmp = Cudd_bddAnd(ddman, cube, var); 

AND the newly created variable with the already existing cube node (remember it started out as the constant one).

    Cudd_Ref(tmp); 

IMPORTANT: update the reference count for the node just created.

    Cudd_RecursiveDeref(ddman, cube); 

ALSO IMPORTANT: decrement the reference count for the old cube node (because we don't need it any more, it's now part of the DD we created by ANDING the cube with the new variable).

    cube = tmp; 

And lastly update the cube node to point to the new DD we just created and updated the reference count for.

That creates the decision diagram for JUST ONE CUBE...

  }

  // ---------------------------------------
  // now add the cube to the appropriate DDs
  // (only the ones with 1 in the outputs for
  // this cube)
  // ---------------------------------------

  for (int j=0; j<numfunctions; j++) {
    if (outputs[j] == '1') { 

So, for each function in the file, if the output for that cube is a one...

      tmp2 = Cudd_bddOr(ddman, ddnodearray[j], cube); 

OR the existing root of the function (stored in the ddnodearray) with the newly created cube from above.

      Cudd_Ref(tmp2); 

update the reference count for the result of the OR operation...

      Cudd_RecursiveDeref(ddman, ddnodearray[j]);
      Cudd_RecursiveDeref(ddman, cube); 

and decrement the reference count for the old root of the function, and for the cube. Neither of these are needed any longer, as they are part of the the new decision diagram just created, which is pointed to by tmp. NOTE: I didn't think that cube should be dereferenced at this point, but the program doesn't work without doing so!! I you can point out my error, please do so.

      ddnodearray[j] = tmp2; 

Finally, update the list of function roots to point to the newly created function.

    }
  }

The entire program, without my interjections, is shown in the sample program listed in the links on the left.

	Cudd_PrintDebug();

It takes as parameters the following (in the listed order):

• DdManager* ddmanager
• DdNode* ddnode
• int val
• int level

The ddmanager is a pointer to the DdManager object that you must create before doing anything with CUDD. See the section on Initializing and Shutting Down a DdManager. The ddnode is a pointer to a DdNode object that is the root of your decision diagram. I do not know the use of the next value; I simply set it to zero. The level is the level of debugging output you would like. 0 is the lowest (nothing) and 4 is the highest (lots of output). See the section on Cudd_PrintDebug for details on the output.

The other useful tool for debugging is a routine that checks if you have dereferenced all your nodes properly. I found this most useful to use right before shutting down the DdManager. Here is a sample of the code that used it:

  if (debug) 
  {
    // dereferencing all the function roots...
    for (int i=0; i<numfunctions; i++) 
      Cudd_RecursiveDeref(ddman, ddnodearray[i]);
    cout << "nodes with non-zero reference counts: ";
    cout << Cudd_CheckZeroRef(ddman) << "\n\n";
  }

  Cudd_Quit(ddman);

The routine Cudd_CheckZeroRef(DdManager* ddman) takes a pointer to a DdManager and checks to see if there are any referenced nodes within it. After dereferencing all of the function roots, as I did above, there should be no more referenced nodes. This function is said to take into acount certain special cases like the constant nodes. This will help you identify memory leaks due to missing dereferences.

university of lethbridge
dept. of math & computer science

maintainer
updated Nov. 2004