<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<!--Converted with LaTeX2HTML 2K.1beta (1.47)
original version by: Nikos Drakos, CBLU, University of Leeds
* revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
* with significant contributions from:
Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
<HTML>
<HEAD>
<TITLE>Programmer's Manual</TITLE>
<META NAME="description" CONTENT="Programmer's Manual">
<META NAME="keywords" CONTENT="cuddIntro">
<META NAME="resource-type" CONTENT="document">
<META NAME="distribution" CONTENT="global">
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
<META NAME="Generator" CONTENT="LaTeX2HTML v2K.1beta">
<META HTTP-EQUIV="Content-Style-Type" CONTENT="text/css">
<LINK REL="STYLESHEET" HREF="cuddIntro.css">
<LINK REL="next" HREF="node5.html">
<LINK REL="previous" HREF="node3.html">
<LINK REL="up" HREF="cuddIntro.html">
<LINK REL="next" HREF="node5.html">
</HEAD>
<BODY >
<!--Navigation Panel-->
<A NAME="tex2html313"
HREF="node5.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<A NAME="tex2html309"
HREF="cuddIntro.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up.png"></A>
<A NAME="tex2html303"
HREF="node3.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev.png"></A>
<A NAME="tex2html311"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html314"
HREF="node5.html">The C++ Interface</A>
<B> Up:</B> <A NAME="tex2html310"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
<B> Previous:</B> <A NAME="tex2html304"
HREF="node3.html">User's Manual</A>
  <B> <A NAME="tex2html312"
HREF="node8.html">Index</A></B>
<BR>
<BR>
<!--End of Navigation Panel-->
<!--Table of Child-Links-->
<A NAME="CHILD_LINKS"><STRONG>Subsections</STRONG></A>
<UL>
<LI><A NAME="tex2html315"
HREF="#SECTION00041000000000000000">Compiling and Linking</A>
<LI><A NAME="tex2html316"
HREF="#SECTION00042000000000000000">Reference Counts</A>
<UL>
<LI><A NAME="tex2html317"
HREF="#SECTION00042100000000000000">NULL Return Values</A>
<LI><A NAME="tex2html318"
HREF="#SECTION00042200000000000000"><EM>Cudd_RecursiveDeref</EM> vs. <EM>Cudd_Deref</EM></A>
<LI><A NAME="tex2html319"
HREF="#SECTION00042300000000000000">When Increasing the Reference Count is Unnecessary</A>
<LI><A NAME="tex2html320"
HREF="#SECTION00042400000000000000">Saturating Increments and Decrements</A>
</UL>
<BR>
<LI><A NAME="tex2html321"
HREF="#SECTION00043000000000000000">Complement Arcs</A>
<LI><A NAME="tex2html322"
HREF="#SECTION00044000000000000000">The Cache</A>
<UL>
<LI><A NAME="tex2html323"
HREF="#SECTION00044100000000000000">Cache Sizing</A>
<LI><A NAME="tex2html324"
HREF="#SECTION00044200000000000000">Local Caches</A>
</UL>
<BR>
<LI><A NAME="tex2html325"
HREF="#SECTION00045000000000000000">The Unique Table</A>
<LI><A NAME="tex2html326"
HREF="#SECTION00046000000000000000">Allowing Asynchronous Reordering</A>
<LI><A NAME="tex2html327"
HREF="#SECTION00047000000000000000">Debugging</A>
<LI><A NAME="tex2html328"
HREF="#SECTION00048000000000000000">Gathering and Interpreting Statistics</A>
<UL>
<LI><A NAME="tex2html329"
HREF="#SECTION00048100000000000000">Non Modifiable Parameters</A>
<LI><A NAME="tex2html330"
HREF="#SECTION00048200000000000000">Modifiable Parameters</A>
<LI><A NAME="tex2html331"
HREF="#SECTION00048300000000000000">Extended Statistics and Reporting</A>
</UL>
<BR>
<LI><A NAME="tex2html332"
HREF="#SECTION00049000000000000000">Guidelines for Documentation</A>
</UL>
<!--End of Table of Child-Links-->
<HR>
<H1><A NAME="SECTION00040000000000000000"></A>
<A NAME="sec:prog"></A>
<BR>
Programmer's Manual
</H1>
<P>
This section provides additional detail on the working of the CUDD
package and on the programming conventions followed in its writing.
The additional detail should help those who want to write procedures
that directly manipulate the CUDD data structures.
<P>
<H2><A NAME="SECTION00041000000000000000"></A>
<A NAME="793"></A><A NAME="sec:compileInt"></A>
<BR>
Compiling and Linking
</H2>
<P>
If you plan to use the CUDD package as a clear box<A NAME="795"></A>
(for instance, you want to write a procedure that traverses a decision
diagram) you need to add
<PRE>
#include "cuddInt.h"
</PRE>
to your source files. In addition, you should link <code>libcudd.a</code> to
your executable. Some platforms require specific compiler and linker
flags. Refer to the <TT>Makefile</TT> in the top level directory of the
distribution.
<P>
<H2><A NAME="SECTION00042000000000000000"></A>
<A NAME="800"></A><A NAME="sec:ref"></A>
<BR>
Reference Counts
</H2>
<P>
Garbage<A NAME="802"></A> collection in the CUDD package is
based on reference counts. Each node stores the sum of the external
references and internal references. An internal BDD or ADD node is
created by a call to <A NAME="tex2html110"
HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1605"></A>, an
internal ZDD node is created by a call to <A NAME="tex2html111"
HREF="cuddAllDet.html#cuddUniqueInterZdd"><EM> cuddUniqueInterZdd</EM></A><A NAME="1607"></A>, and a
terminal<A NAME="809"></A> node is created by a call to <A NAME="tex2html112"
HREF="cuddAllDet.html#cuddUniqueConst"><EM> cuddUniqueConst</EM></A><A NAME="1609"></A>. If the node returned by
these functions is new, its reference count is zero. The function
that calls <A NAME="tex2html113"
HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1611"></A>, <A NAME="tex2html114"
HREF="cuddAllDet.html#cuddUniqueInterZdd"><EM> cuddUniqueInterZdd</EM></A><A NAME="1613"></A>, or <A NAME="tex2html115"
HREF="cuddAllDet.html#cuddUniqueConst"><EM> cuddUniqueConst</EM></A><A NAME="1615"></A> is responsible for
increasing the reference count of the node. This is accomplished by
calling <A NAME="tex2html116"
HREF="cuddExtDet.html#Cudd_Ref"><EM>Cudd_Ref</EM></A><A NAME="1617"></A>.
<P>
When a function is no longer needed by an application, the memory used
by its diagram can be recycled by calling <A NAME="tex2html117"
HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1619"></A> (BDDs and
ADDs) or <A NAME="tex2html118"
HREF="cuddExtDet.html#Cudd_RecursiveDerefZdd"><EM> Cudd_RecursiveDerefZdd</EM></A><A NAME="1621"></A>
(ZDDs). These functions decrease the reference
<A NAME="831"></A> count of the node passed to them.
If the reference count becomes 0, then two things happen:
<OL>
<LI>The node is declared ``dead<A NAME="833"></A>;" this entails
increasing the counters<A NAME="834"></A> of the dead
nodes. (One counter for the subtable<A NAME="835"></A> to which the
node belongs, and one global counter for the
unique<A NAME="836"></A> table to which the node belongs.) The
node itself is not affected.
</LI>
<LI>The function is recursively called on the two children of the
node.
</LI>
</OL>
For instance, if the diagram of a function does not share any nodes
with other diagrams, then calling <A NAME="tex2html119"
HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1623"></A> or <A NAME="tex2html120"
HREF="cuddExtDet.html#Cudd_RecursiveDerefZdd"><EM> Cudd_RecursiveDerefZdd</EM></A><A NAME="1625"></A> on
its root will cause all the nodes of the diagram to become dead.
<P>
When the number of dead nodes reaches a given level (dynamically
determined by the package) garbage collection takes place. During
garbage<A NAME="844"></A> collection dead nodes are returned
to the node free list<A NAME="845"></A>.
<P>
When a new node is created, it is important to increase its
reference<A NAME="846"></A> count before one of the two
following events occurs:
<OL>
<LI>A call to <A NAME="tex2html121"
HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1627"></A>,
to <A NAME="tex2html122"
HREF="cuddAllDet.html#cuddUniqueInterZdd"><EM>cuddUniqueInterZdd</EM></A><A NAME="1629"></A>, to
<A NAME="tex2html123"
HREF="cuddAllDet.html#cuddUniqueConst"><EM>cuddUniqueConst</EM></A><A NAME="1631"></A>, or to a
function that may eventually cause a call to them.
</LI>
<LI>A call to <A NAME="tex2html124"
HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1633"></A>, to <A NAME="tex2html125"
HREF="cuddExtDet.html#Cudd_RecursiveDerefZdd"><EM> Cudd_RecursiveDerefZdd</EM></A><A NAME="1635"></A>, or
to a function that may eventually cause a call to them.
</LI>
</OL>
In practice, it is recommended to increase the reference count as soon
as the returned pointer has been tested for not being NULL.
<P>
<H3><A NAME="SECTION00042100000000000000"></A>
<A NAME="sec:null"></A>
<BR>
NULL Return Values
</H3>
<P>
The interface to the memory management functions (e.g., malloc) used by CUDD
intercepts NULL return values and calls a handler. The default handler
exits with an error message. If the application does not install
another handler, therefore, a NULL return value from an exported
function of CUDD signals an internal error.
<P>
If the aplication, however, installs another handler that lets
execution continue, a NULL pointer returned by an exported function
typically indicates that the process has run out of memory. <A NAME="tex2html126"
HREF="cuddExtDet.html#Cudd_ReadErrorCode"><EM> Cudd_ReadErrorCode</EM></A><A NAME="1637"></A> can be used to
ascertain the nature of the problem.
<P>
An application that tests for the result being NULL can try some
remedial action, if it runs out of memory. For instance, it may free
some memory that is not strictly necessary, or try a slower algorithm
that takes less space. As an example, CUDD overrides the default
handler when trying to enlarge the cache or increase the number of
slots of the unique table. If the allocation fails, the package prints
out a message and continues without resizing the cache.
<P>
<H3><A NAME="SECTION00042200000000000000"></A>
<A NAME="sec:deref"></A>
<BR>
<EM>Cudd_RecursiveDeref</EM> vs. <EM>Cudd_Deref</EM>
</H3>
<P>
It is often the case that a recursive procedure has to protect the
result it is going to return, while it disposes of intermediate
results. (See the previous discussion on when to increase reference
counts.) Once the intermediate results have been properly disposed
of, the final result must be returned to its pristine state, in which
the root node may have a reference count of 0. One cannot use <A NAME="tex2html127"
HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1639"></A> (or <A NAME="tex2html128"
HREF="cuddExtDet.html#Cudd_RecursiveDerefZdd"><EM> Cudd_RecursiveDerefZdd</EM></A>) for this purpose, because it may
erroneously make some nodes dead. Therefore, the package provides a
different function: <A NAME="tex2html129"
HREF="cuddExtDet.html#Cudd_Deref"><EM>Cudd_Deref</EM></A><A NAME="1641"></A>. This
function is not recursive, and does not change the dead node counts.
Its use is almost exclusively the one just described: Decreasing the
reference count of the root of the final result before returning from
a recursive procedure.
<P>
<H3><A NAME="SECTION00042300000000000000"></A>
<A NAME="881"></A><A NAME="sec:noref"></A>
<BR>
When Increasing the Reference Count is Unnecessary
</H3>
<P>
When a copy of a predefined constant<A NAME="883"></A> or of a
simple BDD variable is needed for comparison purposes, then calling
<A NAME="tex2html130"
HREF="cuddExtDet.html#Cudd_Ref"><EM>Cudd_Ref</EM></A><A NAME="1643"></A> is not necessary, because
these simple functions are guaranteed to have reference counts greater
than 0 at all times. If no call to <A NAME="tex2html131"
HREF="cuddExtDet.html#Cudd_Ref"><EM>Cudd_Ref</EM></A>
is made, then no
attempt to free the diagram by calling <A NAME="tex2html132"
HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1645"></A> or <A NAME="tex2html133"
HREF="cuddExtDet.html#Cudd_RecursiveDerefZdd"><EM> Cudd_RecursiveDerefZdd</EM></A><A NAME="1647"></A>
should be made.
<P>
<H3><A NAME="SECTION00042400000000000000"></A>
<A NAME="896"></A><A NAME="897"></A><A NAME="sec:satur"></A>
<BR>
Saturating Increments and Decrements
</H3>
<P>
On 32-bit machines, the CUDD package stores the
reference<A NAME="899"></A> counts in unsigned short int's.
For large diagrams, it is possible for some reference counts to exceed
the capacity of an unsigned short int. Therefore, increments and
decrements of reference counts are <EM>saturating</EM>. This means that
once a reference count has reached the maximum possible value, it is
no longer changed by calls to <A NAME="tex2html134"
HREF="cuddExtDet.html#Cudd_Ref"><EM>Cudd_Ref</EM></A>, <A NAME="tex2html135"
HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1649"></A>, <A NAME="tex2html136"
HREF="cuddExtDet.html#Cudd_RecursiveDerefZdd"><EM> Cudd_RecursiveDerefZdd</EM></A><A NAME="1651"></A>, or
<A NAME="tex2html137"
HREF="cuddExtDet.html#Cudd_Deref"><EM>Cudd_Deref</EM></A><A NAME="1653"></A>. As a consequence, some
nodes that have no references may not be declared dead. This may
result in a small waste of memory, which is normally more than offset
by the reduction in size of the node structure.
<P>
When using 64-bit pointers, there is normally no memory advantage from
using short int's instead of int's in a DdNode. Therefore, increments
and decrements are not saturating in that case. What option is in
effect depends on two macros, SIZEOF_VOID_P<A NAME="912"></A>
and SIZEOF_INT<A NAME="913"></A>, defined in the external
header<A NAME="914"></A> file (<EM>cudd.h</EM><A NAME="916"></A>). The
increments and decrements of the reference counts are performed using
two macros: <A NAME="tex2html138"
HREF="cuddAllDet.html#cuddSatInc"><EM>cuddSatInc</EM></A><A NAME="1655"></A> and <A NAME="tex2html139"
HREF="cuddAllDet.html#cuddSatDec"><EM> cuddSatDec</EM></A><A NAME="1657"></A>, whose definitions depend on
SIZEOF_VOID_P<A NAME="923"></A> and
SIZEOF_INT<A NAME="924"></A>.
<P>
<H2><A NAME="SECTION00043000000000000000"></A>
<A NAME="926"></A><A NAME="sec:compl"></A>
<BR>
Complement Arcs
</H2>
<P>
If ADDs are restricted to use only the constants 0 and 1, they behave
like BDDs without complement arcs. It is normally easier to write code
that manipulates 0-1 ADDs, than to write code for BDDs. However,
complementation is trivial with complement arcs, and is not trivial
without. As a consequence, with complement arcs it is possible to
check for more terminal cases and it is possible to apply De Morgan's
laws to reduce problems that are essentially identical to a standard
form. This in turn increases the utilization of the cache<A NAME="928"></A>.
<P>
The complement attribute is stored in the least significant bit of the
``else" pointer of each node. An external pointer to a function can
also be complemented. The ``then" pointer to a node, on the other
hand, is always <EM>regular<A NAME="929"></A></EM>. It is a mistake to
use a<A NAME="930"></A> pointer as it is to address memory. Instead, it
is always necessary to obtain a regular version of it. This is
normally done by calling <A NAME="tex2html140"
HREF="cuddExtDet.html#Cudd_Regular"><EM> Cudd_Regular</EM></A><A NAME="1659"></A>. It is also a mistake to
call <A NAME="tex2html141"
HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1661"></A> with a
complemented ``then" child as argument. The calling procedure must
apply De Morgan's laws by complementing both pointers passed to <A NAME="tex2html142"
HREF="cuddAllDet.html#cuddUniqueInter"><EM> cuddUniqueInter</EM></A><A NAME="1663"></A> and then taking the
complement of the result.
<P>
<H2><A NAME="SECTION00044000000000000000"></A>
<A NAME="941"></A><A NAME="sec:cache"></A>
<BR>
The Cache
</H2>
<P>
Each entry of the cache consists of five fields: The operator, three
pointers to operands and a pointer to the result. The operator and the
three pointers to the operands are combined to form three words. The
combination relies on two facts:
<UL>
<LI>Most operations have one or two operands. A few bits are
sufficient to discriminate all three-operands operations.
</LI>
<LI>All nodes are aligned to 16-byte boundaries. (32-byte boundaries
if 64-bit pointers are used.) Hence, there are a few bits available
to distinguish the three-operand operations from te others and to
assign unique codes to them.
</LI>
</UL>
<P>
The cache does not contribute to the reference
<A NAME="945"></A>
counts of the nodes. The fact that the cache contains a
pointer to a node does not imply that the node is alive. Instead, when
garbage<A NAME="946"></A> collection takes place, all entries
of the cache pointing to dead<A NAME="947"></A> nodes are cleared.
<P>
The cache is also cleared (of all entries) when dynamic
reordering<A NAME="948"></A> takes place. In both cases, the entries
removed from the cache are about to become invalid.
<P>
All operands and results in a cache entry must be pointers to
DdNodes<A NAME="949"></A>. If a function produces more than one result,
or uses more than three arguments, there are currently two solutions:
<UL>
<LI>Build a separate, local, cache<A NAME="951"></A>. (Using, for
instance, the <EM>st</EM> library<A NAME="953"></A>.)
</LI>
<LI>Combine multiple results, or multiple operands, into a single
diagram, by building a ``multiplexing structure" with reserved
variables.
</LI>
</UL>
Support of the former solution is under development. (See <TT> cuddLCache.c</TT>..) Support for the latter solution may be provided
in future versions of the package.
<P>
There are three sets of interface<A NAME="956"></A> functions to
the cache. The first set is for functions with three operands: <A NAME="tex2html143"
HREF="cuddAllDet.html#cuddCacheInsert"><EM> cuddCacheInsert</EM></A><A NAME="1665"></A> and <A NAME="tex2html144"
HREF="cuddAllDet.html#cuddCacheLookup"><EM> cuddCacheLookup</EM></A><A NAME="1667"></A>. The second set is for
functions with two operands: <A NAME="tex2html145"
HREF="cuddAllDet.html#cuddCacheInsert2"><EM> cuddCacheInsert2</EM></A><A NAME="1669"></A> and <A NAME="tex2html146"
HREF="cuddAllDet.html#cuddCacheLookup2"><EM> cuddCacheLookup2</EM></A><A NAME="1671"></A>.
The second set is for
functions with one operand: <A NAME="tex2html147"
HREF="cuddAllDet.html#cuddCacheInsert1"><EM> cuddCacheInsert1</EM></A><A NAME="1673"></A> and <A NAME="tex2html148"
HREF="cuddAllDet.html#cuddCacheLookup1"><EM> cuddCacheLookup1</EM></A><A NAME="1675"></A>.
The second set is
slightly faster than the first, and the third set is slightly faster
than the second.
<P>
<H3><A NAME="SECTION00044100000000000000"></A>
<A NAME="976"></A><A NAME="sec:cache-sizing"></A>
<BR>
Cache Sizing
</H3>
<P>
The size of the cache can increase during the execution of an
application. (There is currently no way to decrease the size of the
cache, though it would not be difficult to do it.) When a cache miss
occurs, the package uses the following criteria to decide whether to
resize the cache:
<OL>
<LI>If the cache already exceeds the limit given by the <TT> maxCache<A NAME="979"></A></TT> field of the manager, no resizing takes
place. The limit is the minimum of two values: a value set at
initialization time and possibly modified by the application, which
constitutes the hard limit beyond which the cache will never grow;
and a number that depends on the current total number of slots in
the unique<A NAME="980"></A> table.
</LI>
<LI>If the cache is not too large already, resizing is decided based
on the hit rate. The policy adopted by the CUDD package is
``reward-based<A NAME="981"></A>." If the cache hit
rate is high, then it is worthwhile to increase the size of the
cache.
</LI>
</OL>
When resizing takes place, the statistical counters <A NAME="983"></A> used to compute the hit rate are reinitialized so as to
prevent immediate resizing. The number of entries is doubled.
<P>
The rationale for the ``reward-based<A NAME="984"></A>"
policy is as follows. In many BDD/ADD applications the hit rate is
not very sensitive to the size of the cache: It is primarily a
function of the problem instance at hand. If a large hit rate is
observed, chances are that by using a large cache, the results of
large problems (those that would take longer to solve) will survive in
the cache without being overwritten long enough to cause a valuable
cache hit. Notice that when a large problem is solved more than once,
so are its recursively generated subproblems. If the hit rate is
low, the probability of large problems being solved more than once is
low.
<P>
The other observation about the cache sizing policy is that there is
little point in keeping a cache which is much larger than the unique
table. Every time the unique table ``fills up," garbage collection is
invoked and the cache is cleared of all dead entries. A cache that is
much larger than the unique<A NAME="985"></A> table is therefore
less than fully utilized.
<P>
<H3><A NAME="SECTION00044200000000000000"></A>
<A NAME="987"></A><A NAME="sec:local-caches"></A>
<BR>
Local Caches
</H3>
<P>
Sometimes it may be necessary or convenient to use a local cache. A
local cache can be lossless<A NAME="989"></A> (no results are ever
overwritten), or it may store objects for which
canonical<A NAME="990"></A> representations are not available. One
important fact to keep in mind when using a local cache is that local
caches are not cleared during garbage<A NAME="991"></A>
collection or before reordering. Therefore, it is necessary to
increment the reference<A NAME="992"></A> count of all nodes
pointed by a local cache. (Unless their reference counts are
guaranteed positive in some other way. One such way is by including
all partial results in the global result.) Before disposing of the
local cache, all elements stored in it must be passed to <A NAME="tex2html149"
HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1677"></A>. As
consequence of the fact that all results in a local cache are
referenced, it is generally convenient to store in the local cache
also the result of trivial problems, which are not usually stored in
the global cache. Otherwise, after a recursive call, it is difficult
to tell whether the result is in the cache, and therefore referenced,
or not in the cache, and therefore not referenced.
<P>
An alternative approach to referencing the results in the local caches
is to install hook functions (see Section <A HREF="node3.html#sec:hooks">3.16</A>) to be
executed before garbage collection.
<P>
<H2><A NAME="SECTION00045000000000000000"></A>
<A NAME="998"></A><A NAME="sec:unique"></A>
<BR>
The Unique Table
</H2>
<P>
A recursive procedure typically splits the operands by expanding with
respect to the topmost variable. Topmost in this context refers to the
variable that is closest to the roots in the current variable order.
The nodes, on the other hand, hold the index, which is invariant with
reordering. Therefore, when splitting, one must use the
permutation<A NAME="1000"></A> array maintained by the
package to get the right level. Access to the permutation array is
provided by the macro <A NAME="tex2html150"
HREF="cuddAllDet.html#cuddI"><EM>cuddI</EM></A><A NAME="1679"></A> for BDDs and ADDs,
and by the macro <A NAME="tex2html151"
HREF="cuddAllDet.html#cuddIZ"><EM>cuddIZ</EM></A><A NAME="1681"></A> for ZDDs.
<P>
The unique table consists of as many hash<A NAME="1007"></A> tables as there are
variables in use. These has tables are called <EM>unique subtables</EM>.
The sizes of the unique subtables are determined by two criteria:
<OL>
<LI>The collision<A NAME="1010"></A> lists should be short
to keep access time down.
</LI>
<LI>There should be enough room for dead<A NAME="1011"></A> nodes, to
prevent too frequent garbage<A NAME="1012"></A> collections.
</LI>
</OL>
While the first criterion is fairly straightforward to implement, the
second leaves more room to creativity. The CUDD package tries to
figure out whether more dead node should be allowed to increase
performance. (See also Section <A HREF="node3.html#sec:params">3.4</A>.) There are two
reasons for not doing garbage collection too often. The obvious one is
that it is expensive. The second is that dead nodes may be
reclaimed<A NAME="1015"></A>, if they are the result of a
successful cache lookup. Hence dead nodes may provide a substantial
speed-up if they are kept around long enough. The usefulness of
keeping many dead nodes around varies from application to application,
and from problem instance to problem instance. As in the sizing of the
cache, the CUDD package adopts a
``reward-based<A NAME="1016"></A>" policy to
decide how much room should be used for the unique table. If the
number of dead nodes reclaimed is large compared to the number of
nodes directly requested from the memory manager, then the CUDD
package assumes that it will be beneficial to allow more room for the
subtables, thereby reducing the frequency of garbage collection. The
package does so by switching between two modes of operation:
<OL>
<LI>Fast growth<A NAME="1018"></A>: In this mode, the
ratio of dead nodes to total nodes required for garbage collection
is higher than in the slow growth mode to favor resizing
of the subtables.
</LI>
<LI>Slow growth<A NAME="1019"></A>: In this
mode keeping many dead nodes around is not as important as
keeping memory requirements low.
</LI>
</OL>
Switching from one mode to the other is based on the following
criteria:
<OL>
<LI>If the unique table is already large, only slow growth is
possible.
</LI>
<LI>If the table is small and many dead nodes are being reclaimed,
then fast growth is selected.
</LI>
</OL>
This policy is especially effective when the diagrams being
manipulated have lots of recombination. Notice the interplay of the
cache sizing and unique sizing: Fast growth normally occurs when the
cache hit rate is large. The cache and the unique table then grow in
concert, preserving a healthy balance between their sizes.
<P>
<H2><A NAME="SECTION00046000000000000000"></A>
<A NAME="1024"></A><A NAME="sec:async"></A>
<BR>
Allowing Asynchronous Reordering
</H2>
<P>
Asynchronous reordering is the reordering that is triggered
automatically by the increase of the number of nodes. Asynchronous
reordering takes place when a new internal node must be created, and
the number of nodes has reached a given
threshold<A NAME="1026"></A>. (The threshold is adjusted by
the package every time reordering takes place.)
<P>
Those procedures that do not create new nodes (e.g., procedures that
count the number of nodes or minterms<A NAME="1027"></A>) need
not worry about asynchronous reordering: No special precaution is
necessary in writing them.
<P>
Procedures that only manipulate decision diagrams through the exported
functions of the CUDD package also need not concern themselves with
asynchronous reordering. (See Section <A HREF="node3.html#sec:nodes">3.2.1</A> for the
exceptions.)
<P>
The remaining class of procedures is composed of functions that visit
the diagrams and may create new nodes. All such procedures in the CUDD
package are written so that they can be interrupted by dynamic
reordering. The general approach followed goes under the name of
``abort and retry<A NAME="1029"></A>." As the name
implies, a computation that is interrupted by dynamic reordering is
aborted and tried again.
<P>
A recursive procedure that can be interrupted by dynamic reordering
(an interruptible<A NAME="1030"></A> procedure
from now on) is composed of two functions. One is responsible for the
real computation. The other is a simple
wrapper<A NAME="1031"></A>, which tests whether
reordering occurred and restarts the computation if it did.
<P>
Asynchronous reordering of BDDs and ADDs can only be triggered inside
<A NAME="tex2html152"
HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1683"></A>, when a new node
is about to be created. Likewise, asynchronous reordering of ZDDs can
only be triggered inside <A NAME="tex2html153"
HREF="cuddAllDet.html#cuddUniqueInterZdd"><EM> cuddUniqueInterZdd</EM></A><A NAME="1685"></A>. When
reordering is triggered, three things happen:
<OL>
<LI><A NAME="tex2html154"
HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1687"></A> returns a
NULL value;
</LI>
<LI>The flag <EM>reordered</EM> of the manager is set to 1. (0 means
no reordering, while 2 indicates an error occurred during
reordering.)
</LI>
<LI>The counter <EM>reorderings</EM> of the manager is incremented.
The counter is initialized to 0 when the manager is started and can
be accessed by calling <A NAME="tex2html155"
HREF="cuddExtDet.html#Cudd_ReadReorderings"><EM> Cudd_ReadReorderings</EM></A><A NAME="1689"></A>. By
taking two readings of the counter, an application can determine if
variable reordering has taken place between the first and the second
reading. The package itself, however, does not make use of the
counter: It is mentioned here for completeness.
</LI>
</OL>
<P>
The recursive procedure that receives a NULL value from <A NAME="tex2html156"
HREF="cuddAllDet.html#cuddUniqueInter"><EM> cuddUniqueInter</EM></A><A NAME="1691"></A> must free all intermediate
results that it may have computed before, and return NULL in its turn.
<P>
The wrapper<A NAME="1051"></A> function does not
decide whether reordering occurred based on the NULL return value,
because the NULL value may be the result of lack of memory. Instead,
it checks the <EM>reordered</EM> flag.
<P>
When a recursive procedure calls another recursive procedure that may
cause reordering, it should bypass the wrapper and call the recursive
procedure directly. Otherwise, the calling procedure will not know
whether reordering occurred, and will not be able to restart. This is
the main reason why most recursive procedures are internal, rather
than static. (The wrappers, on the other hand, are mostly exported.)
<P>
<H2><A NAME="SECTION00047000000000000000"></A>
<A NAME="1054"></A><A NAME="sec:debug"></A>
<BR>
Debugging
</H2>
<P>
By defining the symbol DD_DEBUG<A NAME="1056"></A> during compilation,
numerous checks are added to the code. In addition, the procedures
<A NAME="tex2html157"
HREF="cuddExtDet.html#Cudd_DebugCheck"><EM>Cudd_DebugCheck</EM></A><A NAME="1693"></A>, <A NAME="tex2html158"
HREF="cuddExtDet.html#Cudd_CheckKeys"><EM> Cudd_CheckKeys</EM></A><A NAME="1695"></A>, and <A NAME="tex2html159"
HREF="cuddAllDet.html#cuddHeapProfile"><EM> cuddHeapProfile</EM></A><A NAME="1697"></A> can be called at any point
to verify the consistency of the data structure. (<A NAME="tex2html160"
HREF="cuddAllDet.html#cuddHeapProfile"><EM> cuddHeapProfile</EM></A>
is an internal procedure. It is declared in <EM> cuddInt.h</EM><A NAME="1069"></A>.) Procedures <A NAME="tex2html161"
HREF="cuddExtDet.html#Cudd_DebugCheck"><EM>Cudd_DebugCheck</EM></A>
and <A NAME="tex2html162"
HREF="cuddExtDet.html#Cudd_CheckKeys"><EM>Cudd_CheckKeys</EM></A>
are especially useful when CUDD reports
that during garbage collection the number of nodes actually deleted
from the unique table is different from the count of dead nodes kept
by the manager. The error causing the discrepancy may have occurred
much earlier than it is discovered. A few strategicaly placed calls
to the debugging procedures can considerably narrow down the search
for the source of the problem. (For instance, a call to <A NAME="tex2html163"
HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A>
where one to <A NAME="tex2html164"
HREF="cuddExtDet.html#Cudd_Deref"><EM>Cudd_Deref</EM></A>
was required
may be identified in this way.)
<P>
One of the most common problems encountered in debugging code based on
the CUDD package is a missing call to <A NAME="tex2html165"
HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1699"></A>. To help
identify this type of problems, the package provides a function called
<A NAME="tex2html166"
HREF="cuddExtDet.html#Cudd_CheckZeroRef"><EM>Cudd_CheckZeroRef</EM></A><A NAME="1701"></A>. This
function should be called immediately before shutting down the
manager. <A NAME="tex2html167"
HREF="cuddExtDet.html#Cudd_CheckZeroRef"><EM>Cudd_CheckZeroRef</EM></A>
checks that the only nodes left
with non-zero reference<A NAME="1086"></A> counts are the
predefined constants, the BDD projection<A NAME="1087"></A>
functions, and nodes whose reference counts are
saturated<A NAME="1088"></A>.
<P>
For this function to be effective the application must explicitly
dispose of all diagrams to which it has pointers before calling it.
<P>
<H2><A NAME="SECTION00048000000000000000"></A>
<A NAME="1090"></A><A NAME="sec:stats"></A>
<BR>
Gathering and Interpreting Statistics
</H2>
<P>
Function <A NAME="tex2html168"
HREF="cuddExtDet.html#Cudd_PrintInfo"><EM>Cudd_PrintInfo</EM></A><A NAME="1703"></A> can be called
to print out the values of parameters and statistics for a manager.
The output of <A NAME="tex2html169"
HREF="cuddExtDet.html#Cudd_PrintInfo"><EM>Cudd_PrintInfo</EM></A>
is divided in two sections. The
first reports the values of parameters that are under the application
control. The second reports the values of statistical counters and
other non-modifiable parameters. A
quick guide to the interpretation of all these quantities follows. For
ease of exposition, we reverse the order and describe the
non-modifiable parameters first. We'll use a sample run as
example. There is nothing special about this run.
<P>
<H3><A NAME="SECTION00048100000000000000"></A>
<A NAME="sec:nonModPar"></A>
<BR>
Non Modifiable Parameters
</H3>
<P>
The list of non-modifiable parameters starts with:
<PRE>
**** CUDD non-modifiable parameters ****
Memory in use: 32544220
</PRE>
This is the memory used by CUDD for three things mainly: Unique table
(including all DD nodes in use), node free list, and computed table.
This number almost never decreases in the lifetime of a CUDD manager,
because CUDD does not release memory when it frees nodes. Rather, it
puts the nodes on its own free list. This number is in bytes. It does
not represent the peak memory occupation, because it does not include
the size of data structures created temporarily by some functions (e.g.,
local look-up tables).
<P>
<PRE>
Peak number of nodes: 837018
</PRE>
This number is the number of nodes that the manager has allocated.
This is not the largest size of the BDDs, because the manager will
normally have some dead nodes and some nodes on the free list.
<P>
<PRE>
Peak number of live nodes: 836894
</PRE>
This is the largest number of live nodes that the manager has held
since its creation.
<P>
<PRE>
Number of BDD variables: 198
Number of ZDD variables: 0
</PRE>
These numbers tell us this run was not using ZDDs.
<P>
<PRE>
Number of cache entries: 1048576
</PRE>
Current number of slots of the computed table. If one has a
performance problem, this is one of the numbers to look at. The cache
size is always a power of 2.
<P>
<PRE>
Number of cache look-ups: 2996536
Number of cache hits: 1187087
</PRE>
These numbers give an indication of the hit rate in the computed
table. It is not unlikely for model checking runs to get
hit rates even higher than this one (39.62%).
<P>
<PRE>
Number of cache insertions: 1809473
Number of cache collisions: 961208
Number of cache deletions: 0
</PRE>
A collision<A NAME="1113"></A> occurs when a cache entry is
overwritten. A deletion<A NAME="1114"></A>
occurs when a cache entry is invalidated (e.g., during garbage
collection). If the number of deletions is high compared to the
number of collisions, it means that garbage collection occurs too
often. In this case there were no garbage collections; hence, no
deletions.
<P>
<PRE>
Cache used slots = 80.90% (expected 82.19%)
</PRE>
Percentage of cache slots that contain a valid entry. If this
number is small, it may signal one of three conditions:
<OL>
<LI>The cache may have been recently resized and it is still filling
up.
</LI>
<LI>The cache is too large for the BDDs. This should not happen if
the size of the cache is determined by CUDD.
</LI>
<LI>The hash function is not working properly. This is accompanied
by a degradation in performance. Conversely, a degradation in
performance may be due to bad hash function behavior.
</LI>
</OL>
The expected value is computed assuming a uniformly random
distribution of the accesses. If the difference between the measured
value and the expected value is large (unlike this case), the cache is
not working properly.
<P>
<PRE>
Soft limit for cache size: 1318912
</PRE>
This number says how large the cache can grow. This limit is based on
the size of the unique table. CUDD uses a reward-based policy for
growing the cache. (See Section <A HREF="node4.html#sec:cache-sizing">4.4.1</A>.) The default
hit rate for resizing is 30% and the value in effect is reported
among the modifiable parameters.
<P>
<PRE>
Number of buckets in unique table: 329728
</PRE>
This number is exactly one quarter of the one above. This is indeed
how the soft limit is determined currently, unless the computed table
hits the specified hard limit. (See below.)
<P>
<PRE>
Used buckets in unique table: 87.96% (expected 87.93%)
</PRE>
Percentage of unique table buckets that contain at least one
node. Remarks analogous to those made about the used cache slots apply.
<P>
<PRE>
Number of BDD and ADD nodes: 836894
Number of ZDD nodes: 0
</PRE>
How many nodes are currently in the unique table, either alive or dead.
<P>
<PRE>
Number of dead BDD and ADD nodes: 0
Number of dead ZDD nodes: 0
</PRE>
Subtract these numbers from those above to get the number of live
nodes. In this case there are no dead nodes because the application
uses delayed dereferencing
<A NAME="tex2html170"
HREF="cuddExtDet.html#Cudd_DelayedDerefBdd"><EM>Cudd_DelayedDerefBdd</EM></A><A NAME="1705"></A>.
<P>
<PRE>
Total number of nodes allocated: 836894
</PRE>
This is the total number of nodes that were requested and obtained
from the free list. It never decreases, and is not an indication of
memory occupation after the first garbage collection. Rather, it is a
measure of the package activity.
<P>
<PRE>
Total number of nodes reclaimed: 0
</PRE>
These are the nodes that were resuscitated from the dead. If they are
many more than the allocated nodes, and the total
number of slots is low relative to the number of nodes, then one may
want to increase the limit for fast unique table growth. In this case,
the number is 0 because of delayed dereferencing.
<P>
<PRE>
Garbage collections so far: 0
Time for garbage collections: 0.00 sec
Reorderings so far: 0
Time for reordering: 0.00 sec
</PRE>
There is a GC for each reordering. Hence the first count will always be
at least as large as the second.
<P>
<PRE>
Node swaps in reordering: 0
</PRE>
This is the number of elementary reordering steps. Each step consists
of the re-expression of one node while swapping two adjacent
variables. This number is a good measure of the amount of work done in
reordering.
<P>
<H3><A NAME="SECTION00048200000000000000"></A>
<A NAME="sec:modPar"></A>
<BR>
Modifiable Parameters
</H3>
<P>
Let us now consider the modifiable parameters, that is, those settings on
which the application or the user has control.
<P>
<PRE>
**** CUDD modifiable parameters ****
Hard limit for cache size: 8388608
</PRE>
This number counts entries. Each entry is 16 bytes if CUDD is compiled
to use 32-bit pointers. Two important observations are in order:
<OL>
<LI>If the datasize limit is set, CUDD will use it to determine this
number automatically. On a Unix system, one can type ``limit" to
verify if this value is set. If the datasize limit is not set, CUDD
uses a default which is rather small. If you have enough memory (say
64MB or more) you should seriously consider <EM>not</EM> using the
default. So, either set the datasize limit, or override the default
with <A NAME="tex2html171"
HREF="cuddExtDet.html#Cudd_SetMaxCacheHard"><EM>Cudd_SetMaxCacheHard</EM></A><A NAME="1707"></A>.
</LI>
<LI>If a process seems to be going nowhere, a small value for
this parameter may be the culprit. One cannot overemphasize the
importance of the computed table in BDD algorithms.
</LI>
</OL>
In this case the limit was automatically set for a target maximum
memory occupation of 104 MB.
<P>
<PRE>
Cache hit threshold for resizing: 15%
</PRE>
This number can be changed if one suspects performance is hindered by
the small size of the cache, and the cache is not growing towards the
soft limit sufficiently fast. In such a case one can change the
default 30% to 15% (as in this case) or even 1%.
<P>
<PRE>
Garbage collection enabled: yes
</PRE>
One can disable it, but there are few good reasons for doing
so. It is normally preferable to raise the limit for fast unique table
growth. (See below.)
<P>
<PRE>
Limit for fast unique table growth: 1363148
</PRE>
See Section <A HREF="node4.html#sec:unique">4.5</A> and the comments above about reclaimed
nodes and hard limit for the cache size. This value was chosen
automatically by CUDD for a datasize limit of 1 GB.
<P>
<PRE>
Maximum number of variables sifted per reordering: 1000
Maximum number of variable swaps per reordering: 2000000
Maximum growth while sifting a variable: 1.2
</PRE>
Lowering these numbers will cause reordering to be less accurate and
faster. Results are somewhat unpredictable, because larger BDDs after one
reordering do not necessarily mean the process will go faster or slower.
<P>
<PRE>
Dynamic reordering of BDDs enabled: yes
Default BDD reordering method: 4
Dynamic reordering of ZDDs enabled: no
Default ZDD reordering method: 4
</PRE>
These lines tell whether automatic reordering can take place and
what method would be used. The mapping from numbers to methods is in
<TT>cudd.h</TT>. One may want to try different BDD
reordering methods. If variable groups are used, however, one should
not expect to see big differences, because CUDD uses the reported
method only to reorder each leaf variable group (typically corresponding
present and next state variables). For the relative order of the
groups, it always uses the same algorithm, which is effectively
sifting.
<P>
As for enabling dynamic reordering or not, a sensible recommendation is the
following: Unless the circuit is rather small or one has a pretty good
idea of what the order should be, reordering should be enabled.
<P>
<PRE>
Realignment of ZDDs to BDDs enabled: no
Realignment of BDDs to ZDDs enabled: no
Dead nodes counted in triggering reordering: no
Group checking criterion: 7
Recombination threshold: 0
Symmetry violation threshold: 0
Arc violation threshold: 0
GA population size: 0
Number of crossovers for GA: 0
</PRE>
Parameters for reordering. See the documentation of the functions used
to control these parameters for the details.
<P>
<PRE>
Next reordering threshold: 100000
</PRE>
When the number of nodes crosses this threshold, reordering will be
triggered. (If enabled; in this case it is not.) This parameter is
updated by the package whenever reordering takes place. The
application can change it, for instance at start-up. Another
possibility is to use a hook function (see Section <A HREF="node3.html#sec:hooks">3.16</A>) to
override the default updating policy.
<P>
<H3><A NAME="SECTION00048300000000000000"></A>
<A NAME="sec:extendedStats"></A>
<BR>
Extended Statistics and Reporting
</H3>
<P>
The following symbols can be defined during compilation to increase
the amount of statistics gathered and the number of messages produced
by the package:
<UL>
<LI>DD_STATS<A NAME="1171"></A>;
</LI>
<LI>DD_CACHE_PROFILE<A NAME="1172"></A>;
</LI>
<LI>DD_UNIQUE_PROFILE<A NAME="1173"></A>.
</LI>
<LI>DD_VERBOSE<A NAME="1174"></A>;
</LI>
</UL>
Defining DD_CACHE_PROFILE causes each entry of the cache to include
an access counter, which is used to compute simple statistics on the
distribution of the keys.
<P>
<H2><A NAME="SECTION00049000000000000000"></A>
<A NAME="sec:doc"></A><A NAME="1178"></A>
<BR>
Guidelines for Documentation
</H2>
<P>
The documentation of the CUDD functions is extracted automatically
from the sources by Stephen Edwards's extdoc. (The Ext system is
available via anonymous FTP<A NAME="1179"></A> from
<A NAME="tex2html172"
HREF="ftp://ic.eecs.berkeley.edu"><TT>ic.eecs.berkeley.edu</TT></A>.)
The following guidelines are followed in CUDD to insure consistent and
effective use of automatic extraction. It is recommended that
extensions to CUDD follow the same documentation guidelines.
<UL>
<LI>The documentation of an exported procedure should be sufficient
to allow one to use it without reading the code. It is not necessary
to explain how the procedure works; only what it does.
</LI>
<LI>The <I>SeeAlso</I><A NAME="1411"></A>
fields should be space-separated lists of function names. The
<I>SeeAlso</I> field of an exported procedure should only reference
other exported procedures. The <I>SeeAlso</I> field of an internal
procedure may reference other internal procedures as well as
exported procedures, but no static procedures.
</LI>
<LI>The return values are detailed in the
<I>Description</I><A NAME="1412"></A>
field, not in the
<I>Synopsis</I><A NAME="1413"></A> field.
</LI>
<LI>The parameters are documented alongside their declarations.
Further comments may appear in the <I>Description</I> field.
</LI>
<LI>If the <I>Description</I> field is non-empty--which is the
normal case for an exported procedure--then the synopsis is
repeated--possibly slightly changed--at the beginning of the
<I>Description</I> field. This is so because extdoc will not put the
synopsis in the same HTML file<A NAME="1194"></A> as
the description.
</LI>
<LI>The <I>Synopsis</I> field should be about one line long.
</LI>
</UL>
<P>
<HR>
<!--Navigation Panel-->
<A NAME="tex2html313"
HREF="node5.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<A NAME="tex2html309"
HREF="cuddIntro.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up.png"></A>
<A NAME="tex2html303"
HREF="node3.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev.png"></A>
<A NAME="tex2html311"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html314"
HREF="node5.html">The C++ Interface</A>
<B> Up:</B> <A NAME="tex2html310"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
<B> Previous:</B> <A NAME="tex2html304"
HREF="node3.html">User's Manual</A>
  <B> <A NAME="tex2html312"
HREF="node8.html">Index</A></B>
<!--End of Navigation Panel-->
<ADDRESS>
Fabio Somenzi
2005-05-17
</ADDRESS>
</BODY>
</HTML>
distrib
>
Mandriva
>
2010.0
>
i586
>
media
>
contrib-release
>
by-pkgid
>
a24e1a39141f9b4ca49bd1e2e23a54ba
>
files
>
1092
