Help -
Help for Webmasters
« back to results for ""
Below is a cache of http://www.research.ibm.com/da/papers/bdd-paper.pdf. It's a snapshot of the page taken as our search engine crawled the Web.
The web site itself may have changed. You can check the current page or check for previous versions at the Internet Archive. Yahoo! is not affiliated with the authors of this page or responsible for its content. Design of a Pointerless BDD Package Abstract In this paper a pointerless BDD package is pro posed. The new design is inspired by the 1998
ICCAD paper of David Long [Long98]. The main
idea is to enforce a strict ordering on the BDD node
identifiers and cleverly reap the advantageous
consequences of that decision, such as a better
memory locality of the nodes and faster unique
table lookup. The down side is a more complicated
garbage collection scheme, although it offers some
extra flexibility. It will also be shown how dynamic
variable ordering fits into this new context. The
ultimate goal is to exceed the performance of a
pointerbased package and have reproducible results across different platforms. Introduction BDDs are effectively deployed in many EDA tools, in particular in the area of formal verification.
A plethora of public domain BDD packages are
available on the web [bddportal]. In this paper we
propose a new design for a BDD package in the
programming language C that uses indices (non
negative integers) to identify the nodes. This fact in
itself is already a deviation from Longs paper; he
still insists on using pointers and also defines his
node ordering based on the addresses of the
memory where the nodes reside. Using indices we
obtain better control over node allocation and can
easily achieve platform independence. In the following sections we shall detail our decisions and discuss their consequences w.r.t. the
main data structures: the unique table and the
computed table. Next we show how we implement
garbage collection and do dynamic variable order
ing. We close with some experimental results. Related work As stated before, the main thrust to investigate a new design for a BDD package was the publication
by David Long [Long98]. Long introduces the notion of nodeage and rearranges his node
allocation and garbage collection accordingly. He
uses pointers to identify nodes and therefore runs
into problems when the memory allocator issues
outoforder blocks. His reference objects (our
handles) use a hash table to ensure unique
ness [Long99]; in our approach no intermediate data
structure is necessary. We use a slightly different
garbage collection algorithm. Longs paper does not
address dynamic variable ordering. The BDDs as
implemented in earlier versions of SMV [McMillan93], do not use node reference counts; a
marksweep garbage collector is used. Variable
reordering is using Rudells algorithm [Rudell] but
does excessive BDD traversals to calculate accurate
live node counts because no explicit reference
counts are used. Armin Bieres package called
ABCD [Biere] focusses on compactness of repre
sentation (only 64 bits per node) and uses indices to
achieve this. It does not take advantage of the node
order and does not offer dynamic variable ordering.
Also its memory management is rather rigid. Preliminaries We assume the common terminology of BDDs to be known [Bryant]: Boolean functions are
canonically represented by a multirooted directed
acyclic graph (DAG); nodes are kept in a unique
table; operations are sped up by employing a
computed table. Occasionally, the order of variables
may be changed to reduce the total number of
nodes. We furthermore assume the reader to be
familiar with the "classical" way of implementing a
BDD package in an imperative programming
language like C, see e.g. [Brace]: nodes are C
structs that contain a variable identifier and THEN
and ELSE children pointers; a NEXT pointer strings
nodes together that belong to the same collision
chain in the unique table. Recycling of nodes is
easily implemented by keeping a reference count for
each node. In the following we will discard most of the classical implementation decisions and start afresh
with a new set of requirements. Why would one 1 Design of a Pointerless BDD Package Geert Janssen IBM T.J. Watson Research Center geert@watson.ibm.com Submitted to 10 th Intl. Workshop on Logic & Synthesis Granlibakken, Lake Tahoe, CA, June 1215, 2001 want to do this? Whats wrong with the current
BDD packages? For one (and this is a very impor
tant point in many commercial applications), a
pointer based BDD package almost invariably will
use hashing on pointer values. This means that even
on the same machine, a repeated invocation of the
same program using such a package need not
exhibit exactly the same behavior: nodes get
allocated to different addresses, these pointers get
hashed to different table indices, this causes a
different pattern of hits and misses in the computed
table, and ultimately the usage of nodes and the
sizes of the resultant BDDs might differ because of
(presumably unpredictable) calls to garbage collec
tions and dynamic variable orderings that are
triggered by heuristics depending on node usage.
On a different machine, the behavior might even get
more erratic because of different memory alignment
requirements, different direction of runtime stack
growth, et cetera. All in all, it could be said that
debugging such a BDD package is a programmers
nightmare. A second important reason to deviate from a pointer based implementation is the opportunity to
uniquely identify nodes by (consecutive) integer
numbers and thereby achieve better control over
node allocation. Being able to control the assignment of numbers to identify nodes, naturally
imposes a strict order on the nodes. This order can
be used to our advantage: keep the DAG ordered
like a priority queue, hence searching for a
particular node will obviously benefit; keep collision chains ordered, then on average less time
is spent searching. Since BDDs are typically
constructed bottomup in a recursive depthfirst
fashion and since traversal of BDDs is a common
operation that proceeds in a similar fashion, it pays
off to keep adjacent (parent and children) nodes
close in memory as well. Ground rules for the new package Clearly, our first rule should be: no more pointers. We identify a node by a number and the
easiest is of course to let this number coincide with
the index in the memory array where the node
resides. We assume the availability of a single,
contiguous array of nodes. Conceptually this is the
easiest way to implement the node memory; in
reality we find that repeatedly having to reallocate
such a large contiguous array is not feasible. Unlike
David Longs proposal, we decided against a
complicated scheme of memory blocks, but opted for a paging oriented solution. Consequently, when
the need for more nodes arises, we only have to
allocate a much smaller stretch of nodes. Any
reference to a BDD node will be done by means of
its index: the THEN, ELSE, and NEXT fields of a
node are therefore also indices. We will insist that nodes be handed out in order of increasing indices, so that the newest (or
youngest) node has the largest index. Think of the
index of a node as its date of birth, then a young
node has a recent date of birth. In the BDD DAG,
where we naturally allocate the parent node later
than the children nodes, we will have the counterintuitive situation that a parent node is
younger than its two children (Figure 1). Complemented edges are handled in a way that is similar to what has been used in pointerbased
packages. We define complemented edges by
merely flipping the most significant bit of the 32
bit unsigned integer index value of a node. Complemented edges are of course not a necessity, but, as Fabio Somenzi [Somenzi01]
pointed out, they do offer more advantages than just
a simple way of representing the negated function
and a trivial implementation for the logical not
operation. Indeed, because we are able to do
complementation and test for complement both in
constant time, we can define more bottom cases to
speedup other operations as well, e.g. the and
operation can now test for complemented operands
and immediately return the 0 (zero/false) BDD.
Rules of DeMorgan can be used at negligible cost to
reduce the number of distinct cases that need be
implemented. Also, some applications rely on the
fact that the root nodes of a pair of complemented
BDDs are in fact the same and in this way share
certain attributes. The next departure from the classical approach is to refrain from using reference counts. They would
not be of much use anyway because dead nodes,
i.e., nodes with a 0 reference count, cannot be
(directly) reused when we require node indices to
obey the age requirement. The consequences are
rather severe: we no longer have a precise notion of
whether a node is alive or dead. It will be harder to
find useful metrics to be used in heuristics that 2 Figure 1: Node memory and the concept of node age. 0 1 2 3 next free x y v 3 2 old young control invocation of garbage collection and dy
namic variable ordering calls. When implementing
dynamic variable ordering based on local level
swaps, it is crucial to have a precise measure for the
number of nodes gained by that swap. More on this
in a subsequent section. Not using reference counts obviously saves space in the node (typically 16 bits are used for a
reference count) and saves time: directly, because
no increments and decrements need be performed;
and indirectly, because the referred node itself need
not be accessed and therefore we have less moves
across the memory hierarchy. Actually, in some
modelchecking benchmarks [Yang98] it was observed that it often happens that one and the same
BDD is repeatedly constructed and immediately
disposed off. It was the reason of the invention of a
socalled death row data structure. Its purpose is to
queue BDDs that are candidates to be freed. The
actual freeing is postponed in the hope that they
might get resurrected and put to use again before the
queue is full and the real freeing kicks in. Without
reference counts, there is no longer a need to worry
about this behavior. Figure 2 outlines the various
fields in the BDD node. In order for garbage collection to be meaningful, we do need to have a means of gathering all BDD
nodes currently referenced by an application. These
external references are the starting points of a node
marking scheme that identifies all live nodes. Such
external references are captured by handle objects.
A handle implements the external view of a BDD.
For simplicity, handles will have reference counts
and therefore can easily be recycled. It is expected
that the number of live handles at any time will be
much less than the current number of live BDD
nodes. Handles are to be interpreted as the Boolean
functions of interest, and each function typically
comprises many BDD nodes. Obviously, a handle
should be unique w.r.t. the node it refers to.
Handles are the ideal place to cache additional data
about the Boolean function, e.g. its size and its set
of support variables. With the ground rules laid down, it is now time to explore their consequences. The next sections
discuss the impact our new requirements have on
the rest of the framework. Unique table Strong canonicity is achieved by ensuring that the triple <v,T,E> is associated with a unique node.
The triple <v,T,E> consists of the variable identifier
v and the edges to the THEN and NEXT subBDDs
which themselves are assumed to consist of unique
nodes. Of course in our case, T and E are the
(possibly complemented) indices of the children
nodes. A simple and fast implementation applies a
hash function to the triple to obtain the index in the
unique table of the start of a collision chain of
nodes. Comparing the triple against the nodes in the
chain resolves the look up. Note that instead of
hashing on the children indices, hashing on a not
necessarily unique signature kept in a node would
work just as well, provided we do search for
matching children indices in the collision chain.
The reason why we would want to do this, is to
make the hash key independent of the memory
position of the node; when garbage collection
moves the node in memory, at least its signature
would stay the same. However, since we empty and
rebuilt the unique table during garbage collection,
theres no real need to assure hash key independ
ence. This doesnt hold for the computed table
though, as we will see shortly. Computed table The computed table, a.k.a. operation cache, records results of operations on BDDs. Typically it
stores the fact that R = op(F,G,H), i.e., the BDD R
is the result of the operation op applied to three
BDD arguments F, G, and H, in a hash table. The
hash key should obviously be composed of the
operation and its operands. But should we use the
indices of the operand BDDs? If we did, and
garbage collection alters indices, we need to rehash
those entries in the computed table. If the hash key
were independent of the indices, then we merely
need to invalidate entries that refer to dead nodes.
Like David Long does, we decided to define a
signature for each node which consists of the
variable associated with that node and a pseudo
random number (whose sequence is of course
deterministic). Computed table hashing takes the
signature of the operands and their complement bit 3 Figure 2: Memory layout of a BDD node. F RC Signature Variable 0 C H Then Else Next 31 0 27 0 Cl as a key. Note that incorporating the complement
bit is vital: it is easy to construct a case involving
the calculation of the and of two parity functions
which exhibits exponential behavior if the comple
ment bit is left out. 2bit reference count Proper utilization of the computed table is vital for efficiency. One should avoid storing facts that
are either trivial (typically these concern operations
where some of the operands are constant) or facts
that are very unlikely to ever be retrieved. The
negative effect of storing too much is that crucial
facts might get overwritten. Facts concerning
operands with low, in particular a single, reference
count should be ignored. Unfortunately, in our new
design we no longer have a reference count per
node. Instead, we reintroduce a 2bit saturating
reference count with the sole purpose of indicating
whether a node has no, a single, or more references.
It is not necessary to keep this count accurate (we
dont even bother to decrement the count when
nodes are freed). Garbage collection Most BDD packages use a reference counting garbage collector. The idea is simple: if we keep
count of the number of references to each BDD
node, then a count of 0 means that the node is no
longer in use and thus can be recycled. Often the
recycling does not occur immediately. The dead
node would have to be unlinked from the unique
table and the entries in the computed table referring
to this node would have to be invalidated; both of
which is considered prohibitively costly. Instead,
occasionally, when a certain percentage of the nodes
is dead, the unique table is swept and all dead nodes
are moved to a free list. The disadvantage of
reference counting is the extra memory needed for
each node and the overhead in increment and
decrement operations. The great advantage is that at
any time we have an accurate knowledge of the
number of references for each node. In a marksweep garbage collector, a marking phase that identifies all live nodes is proceeded by a
sweeping phase that cleans up the garbage (= dead)
nodes. A prerequisite for this to work is that we
know all external references to the nodes. Also, if
we consider garbage collection as if it were an
asynchronous process (which it would be if we
decided to run it as a separate thread), every inter mediate BDD that occurs during a (recursive)
operation needs to be explicitly protected. In our
new design, there are actually two reasons why
certain local variables in the program code need to
be protected: 1. The obvious reason: if we do not protect a variable that holds an index to a BDD node that
will be needed later, that node might be consid
ered garbage by the collector. 2. The not so obvious reason: our garbage collector compacts the node memory and hence nodes get
moved and their indices change. We need a
mechanism to be able to report back the "change
of address" of a node. We use a marksweepupdatesweep ap proach: the marking phase does the obvious; in the
first sweep over the node memory, from lower
indices to higher indices, live nodes are assigned a
forwarding address at their original position and are
then moved over to the left to fill the holes created
by the dead nodes. At the same time, the THEN and
ELSE fields are updated to reflect the new positions
of the children nodes. Note that in the node memory
the direction of the "pointers" THEN, ELSE, and
NEXT is always from right to left (because of the
nodeage rule). During the update phase, all
external references and all explicitly protected
internal references are notified of any change of
address. Then the second sweep phase cleans the
marks and reestablishes the unique table. See
Algorithm 1 for more details. The way we do
compaction has the nice property that it preserves
nodeage, moreover it even improves node 4 void gc(void)
{
mark_phase();
new_nextfree = 0;
for (i = 0; i < nextfree; i++)
if (marked(i)) {
n = new_nextfree++;
THEN(i) = FORWARD(THEN(i));
ELSE(i) = FORWARD(ELSE(i));
mem[n] = mem[i], but retain
ns mark and forwarding address;
FORWARD(i) = n;
}
invalidate_computed_table();
update_phase();
for (i = 0; i < new_nextfree; i++) {
unmark(i);
add i to unique table;
}
} Algorithm 1: marksweepupdatemark garbage collection. proximity, see Figure 3. There is no obvious need to
always consider all nodes for garbage collection; we
allow a user to set a breakpoint below which nodes
will be frozen. This might be beneficial in those
applications that keep some initial BDDs around for
most of their lifetime, e.g. in model checking one
could set the breakpoint after the nextstate
function BDDs. Figure 3: Node memory during garbage collection. Dynamic variable ordering Dynamic variable ordering is the process of changing the rank order of the variables in the
presence of BDDs. This implies that all existing
BDDs need to be modified to reflect the new
variable positions. The objective is to decrease the
overall size of the BDDs. Like garbage collection,
dynamic variable ordering should best be considered an asynchronous process that potentially
can be invoked at any time during the construction
and manipulation of BDDs. We will here sketch
how the popular Rudell sifting algorithm [Rudell] is
implemented in our new package. We concentrate
on the basic operation of swapping two neighboring
variables. Clearly, exchanging parent and children
nodes destroys the nodeage property. Moreover,
we need an accurate measure of the number of
nodes gained (or lost) by a swap. We propose the
following solutions:
The web site itself may have changed. You can check the current page or check for previous versions at the Internet Archive. Yahoo! is not affiliated with the authors of this page or responsible for its content. Design of a Pointerless BDD Package Abstract In this paper a pointerless BDD package is pro posed. The new design is inspired by the 1998
ICCAD paper of David Long [Long98]. The main
idea is to enforce a strict ordering on the BDD node
identifiers and cleverly reap the advantageous
consequences of that decision, such as a better
memory locality of the nodes and faster unique
table lookup. The down side is a more complicated
garbage collection scheme, although it offers some
extra flexibility. It will also be shown how dynamic
variable ordering fits into this new context. The
ultimate goal is to exceed the performance of a
pointerbased package and have reproducible results across different platforms. Introduction BDDs are effectively deployed in many EDA tools, in particular in the area of formal verification.
A plethora of public domain BDD packages are
available on the web [bddportal]. In this paper we
propose a new design for a BDD package in the
programming language C that uses indices (non
negative integers) to identify the nodes. This fact in
itself is already a deviation from Longs paper; he
still insists on using pointers and also defines his
node ordering based on the addresses of the
memory where the nodes reside. Using indices we
obtain better control over node allocation and can
easily achieve platform independence. In the following sections we shall detail our decisions and discuss their consequences w.r.t. the
main data structures: the unique table and the
computed table. Next we show how we implement
garbage collection and do dynamic variable order
ing. We close with some experimental results. Related work As stated before, the main thrust to investigate a new design for a BDD package was the publication
by David Long [Long98]. Long introduces the notion of nodeage and rearranges his node
allocation and garbage collection accordingly. He
uses pointers to identify nodes and therefore runs
into problems when the memory allocator issues
outoforder blocks. His reference objects (our
handles) use a hash table to ensure unique
ness [Long99]; in our approach no intermediate data
structure is necessary. We use a slightly different
garbage collection algorithm. Longs paper does not
address dynamic variable ordering. The BDDs as
implemented in earlier versions of SMV [McMillan93], do not use node reference counts; a
marksweep garbage collector is used. Variable
reordering is using Rudells algorithm [Rudell] but
does excessive BDD traversals to calculate accurate
live node counts because no explicit reference
counts are used. Armin Bieres package called
ABCD [Biere] focusses on compactness of repre
sentation (only 64 bits per node) and uses indices to
achieve this. It does not take advantage of the node
order and does not offer dynamic variable ordering.
Also its memory management is rather rigid. Preliminaries We assume the common terminology of BDDs to be known [Bryant]: Boolean functions are
canonically represented by a multirooted directed
acyclic graph (DAG); nodes are kept in a unique
table; operations are sped up by employing a
computed table. Occasionally, the order of variables
may be changed to reduce the total number of
nodes. We furthermore assume the reader to be
familiar with the "classical" way of implementing a
BDD package in an imperative programming
language like C, see e.g. [Brace]: nodes are C
structs that contain a variable identifier and THEN
and ELSE children pointers; a NEXT pointer strings
nodes together that belong to the same collision
chain in the unique table. Recycling of nodes is
easily implemented by keeping a reference count for
each node. In the following we will discard most of the classical implementation decisions and start afresh
with a new set of requirements. Why would one 1 Design of a Pointerless BDD Package Geert Janssen IBM T.J. Watson Research Center geert@watson.ibm.com Submitted to 10 th Intl. Workshop on Logic & Synthesis Granlibakken, Lake Tahoe, CA, June 1215, 2001 want to do this? Whats wrong with the current
BDD packages? For one (and this is a very impor
tant point in many commercial applications), a
pointer based BDD package almost invariably will
use hashing on pointer values. This means that even
on the same machine, a repeated invocation of the
same program using such a package need not
exhibit exactly the same behavior: nodes get
allocated to different addresses, these pointers get
hashed to different table indices, this causes a
different pattern of hits and misses in the computed
table, and ultimately the usage of nodes and the
sizes of the resultant BDDs might differ because of
(presumably unpredictable) calls to garbage collec
tions and dynamic variable orderings that are
triggered by heuristics depending on node usage.
On a different machine, the behavior might even get
more erratic because of different memory alignment
requirements, different direction of runtime stack
growth, et cetera. All in all, it could be said that
debugging such a BDD package is a programmers
nightmare. A second important reason to deviate from a pointer based implementation is the opportunity to
uniquely identify nodes by (consecutive) integer
numbers and thereby achieve better control over
node allocation. Being able to control the assignment of numbers to identify nodes, naturally
imposes a strict order on the nodes. This order can
be used to our advantage: keep the DAG ordered
like a priority queue, hence searching for a
particular node will obviously benefit; keep collision chains ordered, then on average less time
is spent searching. Since BDDs are typically
constructed bottomup in a recursive depthfirst
fashion and since traversal of BDDs is a common
operation that proceeds in a similar fashion, it pays
off to keep adjacent (parent and children) nodes
close in memory as well. Ground rules for the new package Clearly, our first rule should be: no more pointers. We identify a node by a number and the
easiest is of course to let this number coincide with
the index in the memory array where the node
resides. We assume the availability of a single,
contiguous array of nodes. Conceptually this is the
easiest way to implement the node memory; in
reality we find that repeatedly having to reallocate
such a large contiguous array is not feasible. Unlike
David Longs proposal, we decided against a
complicated scheme of memory blocks, but opted for a paging oriented solution. Consequently, when
the need for more nodes arises, we only have to
allocate a much smaller stretch of nodes. Any
reference to a BDD node will be done by means of
its index: the THEN, ELSE, and NEXT fields of a
node are therefore also indices. We will insist that nodes be handed out in order of increasing indices, so that the newest (or
youngest) node has the largest index. Think of the
index of a node as its date of birth, then a young
node has a recent date of birth. In the BDD DAG,
where we naturally allocate the parent node later
than the children nodes, we will have the counterintuitive situation that a parent node is
younger than its two children (Figure 1). Complemented edges are handled in a way that is similar to what has been used in pointerbased
packages. We define complemented edges by
merely flipping the most significant bit of the 32
bit unsigned integer index value of a node. Complemented edges are of course not a necessity, but, as Fabio Somenzi [Somenzi01]
pointed out, they do offer more advantages than just
a simple way of representing the negated function
and a trivial implementation for the logical not
operation. Indeed, because we are able to do
complementation and test for complement both in
constant time, we can define more bottom cases to
speedup other operations as well, e.g. the and
operation can now test for complemented operands
and immediately return the 0 (zero/false) BDD.
Rules of DeMorgan can be used at negligible cost to
reduce the number of distinct cases that need be
implemented. Also, some applications rely on the
fact that the root nodes of a pair of complemented
BDDs are in fact the same and in this way share
certain attributes. The next departure from the classical approach is to refrain from using reference counts. They would
not be of much use anyway because dead nodes,
i.e., nodes with a 0 reference count, cannot be
(directly) reused when we require node indices to
obey the age requirement. The consequences are
rather severe: we no longer have a precise notion of
whether a node is alive or dead. It will be harder to
find useful metrics to be used in heuristics that 2 Figure 1: Node memory and the concept of node age. 0 1 2 3 next free x y v 3 2 old young control invocation of garbage collection and dy
namic variable ordering calls. When implementing
dynamic variable ordering based on local level
swaps, it is crucial to have a precise measure for the
number of nodes gained by that swap. More on this
in a subsequent section. Not using reference counts obviously saves space in the node (typically 16 bits are used for a
reference count) and saves time: directly, because
no increments and decrements need be performed;
and indirectly, because the referred node itself need
not be accessed and therefore we have less moves
across the memory hierarchy. Actually, in some
modelchecking benchmarks [Yang98] it was observed that it often happens that one and the same
BDD is repeatedly constructed and immediately
disposed off. It was the reason of the invention of a
socalled death row data structure. Its purpose is to
queue BDDs that are candidates to be freed. The
actual freeing is postponed in the hope that they
might get resurrected and put to use again before the
queue is full and the real freeing kicks in. Without
reference counts, there is no longer a need to worry
about this behavior. Figure 2 outlines the various
fields in the BDD node. In order for garbage collection to be meaningful, we do need to have a means of gathering all BDD
nodes currently referenced by an application. These
external references are the starting points of a node
marking scheme that identifies all live nodes. Such
external references are captured by handle objects.
A handle implements the external view of a BDD.
For simplicity, handles will have reference counts
and therefore can easily be recycled. It is expected
that the number of live handles at any time will be
much less than the current number of live BDD
nodes. Handles are to be interpreted as the Boolean
functions of interest, and each function typically
comprises many BDD nodes. Obviously, a handle
should be unique w.r.t. the node it refers to.
Handles are the ideal place to cache additional data
about the Boolean function, e.g. its size and its set
of support variables. With the ground rules laid down, it is now time to explore their consequences. The next sections
discuss the impact our new requirements have on
the rest of the framework. Unique table Strong canonicity is achieved by ensuring that the triple <v,T,E> is associated with a unique node.
The triple <v,T,E> consists of the variable identifier
v and the edges to the THEN and NEXT subBDDs
which themselves are assumed to consist of unique
nodes. Of course in our case, T and E are the
(possibly complemented) indices of the children
nodes. A simple and fast implementation applies a
hash function to the triple to obtain the index in the
unique table of the start of a collision chain of
nodes. Comparing the triple against the nodes in the
chain resolves the look up. Note that instead of
hashing on the children indices, hashing on a not
necessarily unique signature kept in a node would
work just as well, provided we do search for
matching children indices in the collision chain.
The reason why we would want to do this, is to
make the hash key independent of the memory
position of the node; when garbage collection
moves the node in memory, at least its signature
would stay the same. However, since we empty and
rebuilt the unique table during garbage collection,
theres no real need to assure hash key independ
ence. This doesnt hold for the computed table
though, as we will see shortly. Computed table The computed table, a.k.a. operation cache, records results of operations on BDDs. Typically it
stores the fact that R = op(F,G,H), i.e., the BDD R
is the result of the operation op applied to three
BDD arguments F, G, and H, in a hash table. The
hash key should obviously be composed of the
operation and its operands. But should we use the
indices of the operand BDDs? If we did, and
garbage collection alters indices, we need to rehash
those entries in the computed table. If the hash key
were independent of the indices, then we merely
need to invalidate entries that refer to dead nodes.
Like David Long does, we decided to define a
signature for each node which consists of the
variable associated with that node and a pseudo
random number (whose sequence is of course
deterministic). Computed table hashing takes the
signature of the operands and their complement bit 3 Figure 2: Memory layout of a BDD node. F RC Signature Variable 0 C H Then Else Next 31 0 27 0 Cl as a key. Note that incorporating the complement
bit is vital: it is easy to construct a case involving
the calculation of the and of two parity functions
which exhibits exponential behavior if the comple
ment bit is left out. 2bit reference count Proper utilization of the computed table is vital for efficiency. One should avoid storing facts that
are either trivial (typically these concern operations
where some of the operands are constant) or facts
that are very unlikely to ever be retrieved. The
negative effect of storing too much is that crucial
facts might get overwritten. Facts concerning
operands with low, in particular a single, reference
count should be ignored. Unfortunately, in our new
design we no longer have a reference count per
node. Instead, we reintroduce a 2bit saturating
reference count with the sole purpose of indicating
whether a node has no, a single, or more references.
It is not necessary to keep this count accurate (we
dont even bother to decrement the count when
nodes are freed). Garbage collection Most BDD packages use a reference counting garbage collector. The idea is simple: if we keep
count of the number of references to each BDD
node, then a count of 0 means that the node is no
longer in use and thus can be recycled. Often the
recycling does not occur immediately. The dead
node would have to be unlinked from the unique
table and the entries in the computed table referring
to this node would have to be invalidated; both of
which is considered prohibitively costly. Instead,
occasionally, when a certain percentage of the nodes
is dead, the unique table is swept and all dead nodes
are moved to a free list. The disadvantage of
reference counting is the extra memory needed for
each node and the overhead in increment and
decrement operations. The great advantage is that at
any time we have an accurate knowledge of the
number of references for each node. In a marksweep garbage collector, a marking phase that identifies all live nodes is proceeded by a
sweeping phase that cleans up the garbage (= dead)
nodes. A prerequisite for this to work is that we
know all external references to the nodes. Also, if
we consider garbage collection as if it were an
asynchronous process (which it would be if we
decided to run it as a separate thread), every inter mediate BDD that occurs during a (recursive)
operation needs to be explicitly protected. In our
new design, there are actually two reasons why
certain local variables in the program code need to
be protected: 1. The obvious reason: if we do not protect a variable that holds an index to a BDD node that
will be needed later, that node might be consid
ered garbage by the collector. 2. The not so obvious reason: our garbage collector compacts the node memory and hence nodes get
moved and their indices change. We need a
mechanism to be able to report back the "change
of address" of a node. We use a marksweepupdatesweep ap proach: the marking phase does the obvious; in the
first sweep over the node memory, from lower
indices to higher indices, live nodes are assigned a
forwarding address at their original position and are
then moved over to the left to fill the holes created
by the dead nodes. At the same time, the THEN and
ELSE fields are updated to reflect the new positions
of the children nodes. Note that in the node memory
the direction of the "pointers" THEN, ELSE, and
NEXT is always from right to left (because of the
nodeage rule). During the update phase, all
external references and all explicitly protected
internal references are notified of any change of
address. Then the second sweep phase cleans the
marks and reestablishes the unique table. See
Algorithm 1 for more details. The way we do
compaction has the nice property that it preserves
nodeage, moreover it even improves node 4 void gc(void)
{
mark_phase();
new_nextfree = 0;
for (i = 0; i < nextfree; i++)
if (marked(i)) {
n = new_nextfree++;
THEN(i) = FORWARD(THEN(i));
ELSE(i) = FORWARD(ELSE(i));
mem[n] = mem[i], but retain
ns mark and forwarding address;
FORWARD(i) = n;
}
invalidate_computed_table();
update_phase();
for (i = 0; i < new_nextfree; i++) {
unmark(i);
add i to unique table;
}
} Algorithm 1: marksweepupdatemark garbage collection. proximity, see Figure 3. There is no obvious need to
always consider all nodes for garbage collection; we
allow a user to set a breakpoint below which nodes
will be frozen. This might be beneficial in those
applications that keep some initial BDDs around for
most of their lifetime, e.g. in model checking one
could set the breakpoint after the nextstate
function BDDs. Figure 3: Node memory during garbage collection. Dynamic variable ordering Dynamic variable ordering is the process of changing the rank order of the variables in the
presence of BDDs. This implies that all existing
BDDs need to be modified to reflect the new
variable positions. The objective is to decrease the
overall size of the BDDs. Like garbage collection,
dynamic variable ordering should best be considered an asynchronous process that potentially
can be invoked at any time during the construction
and manipulation of BDDs. We will here sketch
how the popular Rudell sifting algorithm [Rudell] is
implemented in our new package. We concentrate
on the basic operation of swapping two neighboring
variables. Clearly, exchanging parent and children
nodes destroys the nodeage property. Moreover,
we need an accurate measure of the number of
nodes gained (or lost) by a swap. We propose the
following solutions:
