[13] | 1 | <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN"> |
---|
| 2 | |
---|
| 3 | <!--Converted with LaTeX2HTML 2K.1beta (1.47) |
---|
| 4 | original version by: Nikos Drakos, CBLU, University of Leeds |
---|
| 5 | * revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan |
---|
| 6 | * with significant contributions from: |
---|
| 7 | Jens Lippmann, Marek Rouchal, Martin Wilck and others --> |
---|
| 8 | <HTML> |
---|
| 9 | <HEAD> |
---|
| 10 | <TITLE>Programmer's Manual</TITLE> |
---|
| 11 | <META NAME="description" CONTENT="Programmer's Manual"> |
---|
| 12 | <META NAME="keywords" CONTENT="cuddIntro"> |
---|
| 13 | <META NAME="resource-type" CONTENT="document"> |
---|
| 14 | <META NAME="distribution" CONTENT="global"> |
---|
| 15 | |
---|
| 16 | <META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1"> |
---|
| 17 | <META NAME="Generator" CONTENT="LaTeX2HTML v2K.1beta"> |
---|
| 18 | <META HTTP-EQUIV="Content-Style-Type" CONTENT="text/css"> |
---|
| 19 | |
---|
| 20 | <LINK REL="STYLESHEET" HREF="cuddIntro.css"> |
---|
| 21 | |
---|
| 22 | <LINK REL="next" HREF="node5.html"> |
---|
| 23 | <LINK REL="previous" HREF="node3.html"> |
---|
| 24 | <LINK REL="up" HREF="cuddIntro.html"> |
---|
| 25 | <LINK REL="next" HREF="node5.html"> |
---|
| 26 | </HEAD> |
---|
| 27 | |
---|
| 28 | <BODY > |
---|
| 29 | <!--Navigation Panel--> |
---|
| 30 | <A NAME="tex2html313" |
---|
| 31 | HREF="node5.html"> |
---|
| 32 | <IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next" |
---|
| 33 | SRC="icons/next.png"></A> |
---|
| 34 | <A NAME="tex2html309" |
---|
| 35 | HREF="cuddIntro.html"> |
---|
| 36 | <IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up" |
---|
| 37 | SRC="icons/up.png"></A> |
---|
| 38 | <A NAME="tex2html303" |
---|
| 39 | HREF="node3.html"> |
---|
| 40 | <IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous" |
---|
| 41 | SRC="icons/prev.png"></A> |
---|
| 42 | <A NAME="tex2html311" |
---|
| 43 | HREF="node8.html"> |
---|
| 44 | <IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index" |
---|
| 45 | SRC="icons/index.png"></A> |
---|
| 46 | <BR> |
---|
| 47 | <B> Next:</B> <A NAME="tex2html314" |
---|
| 48 | HREF="node5.html">The C++ Interface</A> |
---|
| 49 | <B> Up:</B> <A NAME="tex2html310" |
---|
| 50 | HREF="cuddIntro.html">CUDD: CU Decision Diagram</A> |
---|
| 51 | <B> Previous:</B> <A NAME="tex2html304" |
---|
| 52 | HREF="node3.html">User's Manual</A> |
---|
| 53 |   <B> <A NAME="tex2html312" |
---|
| 54 | HREF="node8.html">Index</A></B> |
---|
| 55 | <BR> |
---|
| 56 | <BR> |
---|
| 57 | <!--End of Navigation Panel--> |
---|
| 58 | <!--Table of Child-Links--> |
---|
| 59 | <A NAME="CHILD_LINKS"><STRONG>Subsections</STRONG></A> |
---|
| 60 | |
---|
| 61 | <UL> |
---|
| 62 | <LI><A NAME="tex2html315" |
---|
| 63 | HREF="#SECTION00041000000000000000">Compiling and Linking</A> |
---|
| 64 | <LI><A NAME="tex2html316" |
---|
| 65 | HREF="#SECTION00042000000000000000">Reference Counts</A> |
---|
| 66 | <UL> |
---|
| 67 | <LI><A NAME="tex2html317" |
---|
| 68 | HREF="#SECTION00042100000000000000">NULL Return Values</A> |
---|
| 69 | <LI><A NAME="tex2html318" |
---|
| 70 | HREF="#SECTION00042200000000000000"><EM>Cudd_RecursiveDeref</EM> vs. <EM>Cudd_Deref</EM></A> |
---|
| 71 | <LI><A NAME="tex2html319" |
---|
| 72 | HREF="#SECTION00042300000000000000">When Increasing the Reference Count is Unnecessary</A> |
---|
| 73 | <LI><A NAME="tex2html320" |
---|
| 74 | HREF="#SECTION00042400000000000000">Saturating Increments and Decrements</A> |
---|
| 75 | </UL> |
---|
| 76 | <BR> |
---|
| 77 | <LI><A NAME="tex2html321" |
---|
| 78 | HREF="#SECTION00043000000000000000">Complement Arcs</A> |
---|
| 79 | <LI><A NAME="tex2html322" |
---|
| 80 | HREF="#SECTION00044000000000000000">The Cache</A> |
---|
| 81 | <UL> |
---|
| 82 | <LI><A NAME="tex2html323" |
---|
| 83 | HREF="#SECTION00044100000000000000">Cache Sizing</A> |
---|
| 84 | <LI><A NAME="tex2html324" |
---|
| 85 | HREF="#SECTION00044200000000000000">Local Caches</A> |
---|
| 86 | </UL> |
---|
| 87 | <BR> |
---|
| 88 | <LI><A NAME="tex2html325" |
---|
| 89 | HREF="#SECTION00045000000000000000">The Unique Table</A> |
---|
| 90 | <LI><A NAME="tex2html326" |
---|
| 91 | HREF="#SECTION00046000000000000000">Allowing Asynchronous Reordering</A> |
---|
| 92 | <LI><A NAME="tex2html327" |
---|
| 93 | HREF="#SECTION00047000000000000000">Debugging</A> |
---|
| 94 | <LI><A NAME="tex2html328" |
---|
| 95 | HREF="#SECTION00048000000000000000">Gathering and Interpreting Statistics</A> |
---|
| 96 | <UL> |
---|
| 97 | <LI><A NAME="tex2html329" |
---|
| 98 | HREF="#SECTION00048100000000000000">Non Modifiable Parameters</A> |
---|
| 99 | <LI><A NAME="tex2html330" |
---|
| 100 | HREF="#SECTION00048200000000000000">Modifiable Parameters</A> |
---|
| 101 | <LI><A NAME="tex2html331" |
---|
| 102 | HREF="#SECTION00048300000000000000">Extended Statistics and Reporting</A> |
---|
| 103 | </UL> |
---|
| 104 | <BR> |
---|
| 105 | <LI><A NAME="tex2html332" |
---|
| 106 | HREF="#SECTION00049000000000000000">Guidelines for Documentation</A> |
---|
| 107 | </UL> |
---|
| 108 | <!--End of Table of Child-Links--> |
---|
| 109 | <HR> |
---|
| 110 | |
---|
| 111 | <H1><A NAME="SECTION00040000000000000000"></A> |
---|
| 112 | <A NAME="sec:prog"></A> |
---|
| 113 | <BR> |
---|
| 114 | Programmer's Manual |
---|
| 115 | </H1> |
---|
| 116 | |
---|
| 117 | <P> |
---|
| 118 | This section provides additional detail on the working of the CUDD |
---|
| 119 | package and on the programming conventions followed in its writing. |
---|
| 120 | The additional detail should help those who want to write procedures |
---|
| 121 | that directly manipulate the CUDD data structures. |
---|
| 122 | |
---|
| 123 | <P> |
---|
| 124 | |
---|
| 125 | <H2><A NAME="SECTION00041000000000000000"></A> |
---|
| 126 | <A NAME="793"></A><A NAME="sec:compileInt"></A> |
---|
| 127 | <BR> |
---|
| 128 | Compiling and Linking |
---|
| 129 | </H2> |
---|
| 130 | |
---|
| 131 | <P> |
---|
| 132 | If you plan to use the CUDD package as a clear box<A NAME="795"></A> |
---|
| 133 | (for instance, you want to write a procedure that traverses a decision |
---|
| 134 | diagram) you need to add |
---|
| 135 | <PRE> |
---|
| 136 | #include "cuddInt.h" |
---|
| 137 | </PRE> |
---|
| 138 | to your source files. In addition, you should link <code>libcudd.a</code> to |
---|
| 139 | your executable. Some platforms require specific compiler and linker |
---|
| 140 | flags. Refer to the <TT>Makefile</TT> in the top level directory of the |
---|
| 141 | distribution. |
---|
| 142 | |
---|
| 143 | <P> |
---|
| 144 | |
---|
| 145 | <H2><A NAME="SECTION00042000000000000000"></A> |
---|
| 146 | <A NAME="800"></A><A NAME="sec:ref"></A> |
---|
| 147 | <BR> |
---|
| 148 | Reference Counts |
---|
| 149 | </H2> |
---|
| 150 | |
---|
| 151 | <P> |
---|
| 152 | Garbage<A NAME="802"></A> collection in the CUDD package is |
---|
| 153 | based on reference counts. Each node stores the sum of the external |
---|
| 154 | references and internal references. An internal BDD or ADD node is |
---|
| 155 | created by a call to <A NAME="tex2html110" |
---|
| 156 | HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1605"></A>, an |
---|
| 157 | internal ZDD node is created by a call to <A NAME="tex2html111" |
---|
| 158 | HREF="cuddAllDet.html#cuddUniqueInterZdd"><EM> cuddUniqueInterZdd</EM></A><A NAME="1607"></A>, and a |
---|
| 159 | terminal<A NAME="809"></A> node is created by a call to <A NAME="tex2html112" |
---|
| 160 | HREF="cuddAllDet.html#cuddUniqueConst"><EM> cuddUniqueConst</EM></A><A NAME="1609"></A>. If the node returned by |
---|
| 161 | these functions is new, its reference count is zero. The function |
---|
| 162 | that calls <A NAME="tex2html113" |
---|
| 163 | HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1611"></A>, <A NAME="tex2html114" |
---|
| 164 | HREF="cuddAllDet.html#cuddUniqueInterZdd"><EM> cuddUniqueInterZdd</EM></A><A NAME="1613"></A>, or <A NAME="tex2html115" |
---|
| 165 | HREF="cuddAllDet.html#cuddUniqueConst"><EM> cuddUniqueConst</EM></A><A NAME="1615"></A> is responsible for |
---|
| 166 | increasing the reference count of the node. This is accomplished by |
---|
| 167 | calling <A NAME="tex2html116" |
---|
| 168 | HREF="cuddExtDet.html#Cudd_Ref"><EM>Cudd_Ref</EM></A><A NAME="1617"></A>. |
---|
| 169 | |
---|
| 170 | <P> |
---|
| 171 | When a function is no longer needed by an application, the memory used |
---|
| 172 | by its diagram can be recycled by calling <A NAME="tex2html117" |
---|
| 173 | HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1619"></A> (BDDs and |
---|
| 174 | ADDs) or <A NAME="tex2html118" |
---|
| 175 | HREF="cuddExtDet.html#Cudd_RecursiveDerefZdd"><EM> Cudd_RecursiveDerefZdd</EM></A><A NAME="1621"></A> |
---|
| 176 | (ZDDs). These functions decrease the reference |
---|
| 177 | <A NAME="831"></A> count of the node passed to them. |
---|
| 178 | If the reference count becomes 0, then two things happen: |
---|
| 179 | |
---|
| 180 | <OL> |
---|
| 181 | <LI>The node is declared ``dead<A NAME="833"></A>;" this entails |
---|
| 182 | increasing the counters<A NAME="834"></A> of the dead |
---|
| 183 | nodes. (One counter for the subtable<A NAME="835"></A> to which the |
---|
| 184 | node belongs, and one global counter for the |
---|
| 185 | unique<A NAME="836"></A> table to which the node belongs.) The |
---|
| 186 | node itself is not affected. |
---|
| 187 | </LI> |
---|
| 188 | <LI>The function is recursively called on the two children of the |
---|
| 189 | node. |
---|
| 190 | </LI> |
---|
| 191 | </OL> |
---|
| 192 | For instance, if the diagram of a function does not share any nodes |
---|
| 193 | with other diagrams, then calling <A NAME="tex2html119" |
---|
| 194 | HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1623"></A> or <A NAME="tex2html120" |
---|
| 195 | HREF="cuddExtDet.html#Cudd_RecursiveDerefZdd"><EM> Cudd_RecursiveDerefZdd</EM></A><A NAME="1625"></A> on |
---|
| 196 | its root will cause all the nodes of the diagram to become dead. |
---|
| 197 | |
---|
| 198 | <P> |
---|
| 199 | When the number of dead nodes reaches a given level (dynamically |
---|
| 200 | determined by the package) garbage collection takes place. During |
---|
| 201 | garbage<A NAME="844"></A> collection dead nodes are returned |
---|
| 202 | to the node free list<A NAME="845"></A>. |
---|
| 203 | |
---|
| 204 | <P> |
---|
| 205 | When a new node is created, it is important to increase its |
---|
| 206 | reference<A NAME="846"></A> count before one of the two |
---|
| 207 | following events occurs: |
---|
| 208 | |
---|
| 209 | <OL> |
---|
| 210 | <LI>A call to <A NAME="tex2html121" |
---|
| 211 | HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1627"></A>, |
---|
| 212 | |
---|
| 213 | to <A NAME="tex2html122" |
---|
| 214 | HREF="cuddAllDet.html#cuddUniqueInterZdd"><EM>cuddUniqueInterZdd</EM></A><A NAME="1629"></A>, to |
---|
| 215 | |
---|
| 216 | <A NAME="tex2html123" |
---|
| 217 | HREF="cuddAllDet.html#cuddUniqueConst"><EM>cuddUniqueConst</EM></A><A NAME="1631"></A>, or to a |
---|
| 218 | |
---|
| 219 | function that may eventually cause a call to them. |
---|
| 220 | </LI> |
---|
| 221 | <LI>A call to <A NAME="tex2html124" |
---|
| 222 | HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1633"></A>, to <A NAME="tex2html125" |
---|
| 223 | HREF="cuddExtDet.html#Cudd_RecursiveDerefZdd"><EM> Cudd_RecursiveDerefZdd</EM></A><A NAME="1635"></A>, or |
---|
| 224 | |
---|
| 225 | to a function that may eventually cause a call to them. |
---|
| 226 | </LI> |
---|
| 227 | </OL> |
---|
| 228 | In practice, it is recommended to increase the reference count as soon |
---|
| 229 | as the returned pointer has been tested for not being NULL. |
---|
| 230 | |
---|
| 231 | <P> |
---|
| 232 | |
---|
| 233 | <H3><A NAME="SECTION00042100000000000000"></A> |
---|
| 234 | <A NAME="sec:null"></A> |
---|
| 235 | <BR> |
---|
| 236 | NULL Return Values |
---|
| 237 | </H3> |
---|
| 238 | |
---|
| 239 | <P> |
---|
| 240 | The interface to the memory management functions (e.g., malloc) used by CUDD |
---|
| 241 | intercepts NULL return values and calls a handler. The default handler |
---|
| 242 | exits with an error message. If the application does not install |
---|
| 243 | another handler, therefore, a NULL return value from an exported |
---|
| 244 | function of CUDD signals an internal error. |
---|
| 245 | |
---|
| 246 | <P> |
---|
| 247 | If the aplication, however, installs another handler that lets |
---|
| 248 | execution continue, a NULL pointer returned by an exported function |
---|
| 249 | typically indicates that the process has run out of memory. <A NAME="tex2html126" |
---|
| 250 | HREF="cuddExtDet.html#Cudd_ReadErrorCode"><EM> Cudd_ReadErrorCode</EM></A><A NAME="1637"></A> can be used to |
---|
| 251 | ascertain the nature of the problem. |
---|
| 252 | |
---|
| 253 | <P> |
---|
| 254 | An application that tests for the result being NULL can try some |
---|
| 255 | remedial action, if it runs out of memory. For instance, it may free |
---|
| 256 | some memory that is not strictly necessary, or try a slower algorithm |
---|
| 257 | that takes less space. As an example, CUDD overrides the default |
---|
| 258 | handler when trying to enlarge the cache or increase the number of |
---|
| 259 | slots of the unique table. If the allocation fails, the package prints |
---|
| 260 | out a message and continues without resizing the cache. |
---|
| 261 | |
---|
| 262 | <P> |
---|
| 263 | |
---|
| 264 | <H3><A NAME="SECTION00042200000000000000"></A> |
---|
| 265 | <A NAME="sec:deref"></A> |
---|
| 266 | <BR> |
---|
| 267 | <EM>Cudd_RecursiveDeref</EM> vs. <EM>Cudd_Deref</EM> |
---|
| 268 | </H3> |
---|
| 269 | |
---|
| 270 | <P> |
---|
| 271 | It is often the case that a recursive procedure has to protect the |
---|
| 272 | result it is going to return, while it disposes of intermediate |
---|
| 273 | results. (See the previous discussion on when to increase reference |
---|
| 274 | counts.) Once the intermediate results have been properly disposed |
---|
| 275 | of, the final result must be returned to its pristine state, in which |
---|
| 276 | the root node may have a reference count of 0. One cannot use <A NAME="tex2html127" |
---|
| 277 | HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1639"></A> (or <A NAME="tex2html128" |
---|
| 278 | HREF="cuddExtDet.html#Cudd_RecursiveDerefZdd"><EM> Cudd_RecursiveDerefZdd</EM></A>) for this purpose, because it may |
---|
| 279 | erroneously make some nodes dead. Therefore, the package provides a |
---|
| 280 | different function: <A NAME="tex2html129" |
---|
| 281 | HREF="cuddExtDet.html#Cudd_Deref"><EM>Cudd_Deref</EM></A><A NAME="1641"></A>. This |
---|
| 282 | function is not recursive, and does not change the dead node counts. |
---|
| 283 | Its use is almost exclusively the one just described: Decreasing the |
---|
| 284 | reference count of the root of the final result before returning from |
---|
| 285 | a recursive procedure. |
---|
| 286 | |
---|
| 287 | <P> |
---|
| 288 | |
---|
| 289 | <H3><A NAME="SECTION00042300000000000000"></A> |
---|
| 290 | <A NAME="881"></A><A NAME="sec:noref"></A> |
---|
| 291 | <BR> |
---|
| 292 | When Increasing the Reference Count is Unnecessary |
---|
| 293 | </H3> |
---|
| 294 | |
---|
| 295 | <P> |
---|
| 296 | When a copy of a predefined constant<A NAME="883"></A> or of a |
---|
| 297 | simple BDD variable is needed for comparison purposes, then calling |
---|
| 298 | <A NAME="tex2html130" |
---|
| 299 | HREF="cuddExtDet.html#Cudd_Ref"><EM>Cudd_Ref</EM></A><A NAME="1643"></A> is not necessary, because |
---|
| 300 | these simple functions are guaranteed to have reference counts greater |
---|
| 301 | than 0 at all times. If no call to <A NAME="tex2html131" |
---|
| 302 | HREF="cuddExtDet.html#Cudd_Ref"><EM>Cudd_Ref</EM></A> |
---|
| 303 | is made, then no |
---|
| 304 | attempt to free the diagram by calling <A NAME="tex2html132" |
---|
| 305 | HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1645"></A> or <A NAME="tex2html133" |
---|
| 306 | HREF="cuddExtDet.html#Cudd_RecursiveDerefZdd"><EM> Cudd_RecursiveDerefZdd</EM></A><A NAME="1647"></A> |
---|
| 307 | should be made. |
---|
| 308 | |
---|
| 309 | <P> |
---|
| 310 | |
---|
| 311 | <H3><A NAME="SECTION00042400000000000000"></A> |
---|
| 312 | <A NAME="896"></A><A NAME="897"></A><A NAME="sec:satur"></A> |
---|
| 313 | <BR> |
---|
| 314 | Saturating Increments and Decrements |
---|
| 315 | </H3> |
---|
| 316 | |
---|
| 317 | <P> |
---|
| 318 | On 32-bit machines, the CUDD package stores the |
---|
| 319 | reference<A NAME="899"></A> counts in unsigned short int's. |
---|
| 320 | For large diagrams, it is possible for some reference counts to exceed |
---|
| 321 | the capacity of an unsigned short int. Therefore, increments and |
---|
| 322 | decrements of reference counts are <EM>saturating</EM>. This means that |
---|
| 323 | once a reference count has reached the maximum possible value, it is |
---|
| 324 | no longer changed by calls to <A NAME="tex2html134" |
---|
| 325 | HREF="cuddExtDet.html#Cudd_Ref"><EM>Cudd_Ref</EM></A>, <A NAME="tex2html135" |
---|
| 326 | HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1649"></A>, <A NAME="tex2html136" |
---|
| 327 | HREF="cuddExtDet.html#Cudd_RecursiveDerefZdd"><EM> Cudd_RecursiveDerefZdd</EM></A><A NAME="1651"></A>, or |
---|
| 328 | <A NAME="tex2html137" |
---|
| 329 | HREF="cuddExtDet.html#Cudd_Deref"><EM>Cudd_Deref</EM></A><A NAME="1653"></A>. As a consequence, some |
---|
| 330 | nodes that have no references may not be declared dead. This may |
---|
| 331 | result in a small waste of memory, which is normally more than offset |
---|
| 332 | by the reduction in size of the node structure. |
---|
| 333 | |
---|
| 334 | <P> |
---|
| 335 | When using 64-bit pointers, there is normally no memory advantage from |
---|
| 336 | using short int's instead of int's in a DdNode. Therefore, increments |
---|
| 337 | and decrements are not saturating in that case. What option is in |
---|
| 338 | effect depends on two macros, SIZEOF_VOID_P<A NAME="912"></A> |
---|
| 339 | and SIZEOF_INT<A NAME="913"></A>, defined in the external |
---|
| 340 | header<A NAME="914"></A> file (<EM>cudd.h</EM><A NAME="916"></A>). The |
---|
| 341 | increments and decrements of the reference counts are performed using |
---|
| 342 | two macros: <A NAME="tex2html138" |
---|
| 343 | HREF="cuddAllDet.html#cuddSatInc"><EM>cuddSatInc</EM></A><A NAME="1655"></A> and <A NAME="tex2html139" |
---|
| 344 | HREF="cuddAllDet.html#cuddSatDec"><EM> cuddSatDec</EM></A><A NAME="1657"></A>, whose definitions depend on |
---|
| 345 | SIZEOF_VOID_P<A NAME="923"></A> and |
---|
| 346 | SIZEOF_INT<A NAME="924"></A>. |
---|
| 347 | |
---|
| 348 | <P> |
---|
| 349 | |
---|
| 350 | <H2><A NAME="SECTION00043000000000000000"></A> |
---|
| 351 | <A NAME="926"></A><A NAME="sec:compl"></A> |
---|
| 352 | <BR> |
---|
| 353 | Complement Arcs |
---|
| 354 | </H2> |
---|
| 355 | |
---|
| 356 | <P> |
---|
| 357 | If ADDs are restricted to use only the constants 0 and 1, they behave |
---|
| 358 | like BDDs without complement arcs. It is normally easier to write code |
---|
| 359 | that manipulates 0-1 ADDs, than to write code for BDDs. However, |
---|
| 360 | complementation is trivial with complement arcs, and is not trivial |
---|
| 361 | without. As a consequence, with complement arcs it is possible to |
---|
| 362 | check for more terminal cases and it is possible to apply De Morgan's |
---|
| 363 | laws to reduce problems that are essentially identical to a standard |
---|
| 364 | form. This in turn increases the utilization of the cache<A NAME="928"></A>. |
---|
| 365 | |
---|
| 366 | <P> |
---|
| 367 | The complement attribute is stored in the least significant bit of the |
---|
| 368 | ``else" pointer of each node. An external pointer to a function can |
---|
| 369 | also be complemented. The ``then" pointer to a node, on the other |
---|
| 370 | hand, is always <EM>regular<A NAME="929"></A></EM>. It is a mistake to |
---|
| 371 | use a<A NAME="930"></A> pointer as it is to address memory. Instead, it |
---|
| 372 | is always necessary to obtain a regular version of it. This is |
---|
| 373 | normally done by calling <A NAME="tex2html140" |
---|
| 374 | HREF="cuddExtDet.html#Cudd_Regular"><EM> Cudd_Regular</EM></A><A NAME="1659"></A>. It is also a mistake to |
---|
| 375 | call <A NAME="tex2html141" |
---|
| 376 | HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1661"></A> with a |
---|
| 377 | complemented ``then" child as argument. The calling procedure must |
---|
| 378 | apply De Morgan's laws by complementing both pointers passed to <A NAME="tex2html142" |
---|
| 379 | HREF="cuddAllDet.html#cuddUniqueInter"><EM> cuddUniqueInter</EM></A><A NAME="1663"></A> and then taking the |
---|
| 380 | complement of the result. |
---|
| 381 | |
---|
| 382 | <P> |
---|
| 383 | |
---|
| 384 | <H2><A NAME="SECTION00044000000000000000"></A> |
---|
| 385 | <A NAME="941"></A><A NAME="sec:cache"></A> |
---|
| 386 | <BR> |
---|
| 387 | The Cache |
---|
| 388 | </H2> |
---|
| 389 | |
---|
| 390 | <P> |
---|
| 391 | Each entry of the cache consists of five fields: The operator, three |
---|
| 392 | pointers to operands and a pointer to the result. The operator and the |
---|
| 393 | three pointers to the operands are combined to form three words. The |
---|
| 394 | combination relies on two facts: |
---|
| 395 | |
---|
| 396 | <UL> |
---|
| 397 | <LI>Most operations have one or two operands. A few bits are |
---|
| 398 | sufficient to discriminate all three-operands operations. |
---|
| 399 | </LI> |
---|
| 400 | <LI>All nodes are aligned to 16-byte boundaries. (32-byte boundaries |
---|
| 401 | if 64-bit pointers are used.) Hence, there are a few bits available |
---|
| 402 | to distinguish the three-operand operations from te others and to |
---|
| 403 | assign unique codes to them. |
---|
| 404 | </LI> |
---|
| 405 | </UL> |
---|
| 406 | |
---|
| 407 | <P> |
---|
| 408 | The cache does not contribute to the reference |
---|
| 409 | <A NAME="945"></A> |
---|
| 410 | counts of the nodes. The fact that the cache contains a |
---|
| 411 | pointer to a node does not imply that the node is alive. Instead, when |
---|
| 412 | garbage<A NAME="946"></A> collection takes place, all entries |
---|
| 413 | of the cache pointing to dead<A NAME="947"></A> nodes are cleared. |
---|
| 414 | |
---|
| 415 | <P> |
---|
| 416 | The cache is also cleared (of all entries) when dynamic |
---|
| 417 | reordering<A NAME="948"></A> takes place. In both cases, the entries |
---|
| 418 | removed from the cache are about to become invalid. |
---|
| 419 | |
---|
| 420 | <P> |
---|
| 421 | All operands and results in a cache entry must be pointers to |
---|
| 422 | DdNodes<A NAME="949"></A>. If a function produces more than one result, |
---|
| 423 | or uses more than three arguments, there are currently two solutions: |
---|
| 424 | |
---|
| 425 | <UL> |
---|
| 426 | <LI>Build a separate, local, cache<A NAME="951"></A>. (Using, for |
---|
| 427 | instance, the <EM>st</EM> library<A NAME="953"></A>.) |
---|
| 428 | </LI> |
---|
| 429 | <LI>Combine multiple results, or multiple operands, into a single |
---|
| 430 | diagram, by building a ``multiplexing structure" with reserved |
---|
| 431 | variables. |
---|
| 432 | </LI> |
---|
| 433 | </UL> |
---|
| 434 | Support of the former solution is under development. (See <TT> cuddLCache.c</TT>..) Support for the latter solution may be provided |
---|
| 435 | in future versions of the package. |
---|
| 436 | |
---|
| 437 | <P> |
---|
| 438 | There are three sets of interface<A NAME="956"></A> functions to |
---|
| 439 | the cache. The first set is for functions with three operands: <A NAME="tex2html143" |
---|
| 440 | HREF="cuddAllDet.html#cuddCacheInsert"><EM> cuddCacheInsert</EM></A><A NAME="1665"></A> and <A NAME="tex2html144" |
---|
| 441 | HREF="cuddAllDet.html#cuddCacheLookup"><EM> cuddCacheLookup</EM></A><A NAME="1667"></A>. The second set is for |
---|
| 442 | functions with two operands: <A NAME="tex2html145" |
---|
| 443 | HREF="cuddAllDet.html#cuddCacheInsert2"><EM> cuddCacheInsert2</EM></A><A NAME="1669"></A> and <A NAME="tex2html146" |
---|
| 444 | HREF="cuddAllDet.html#cuddCacheLookup2"><EM> cuddCacheLookup2</EM></A><A NAME="1671"></A>. |
---|
| 445 | The second set is for |
---|
| 446 | functions with one operand: <A NAME="tex2html147" |
---|
| 447 | HREF="cuddAllDet.html#cuddCacheInsert1"><EM> cuddCacheInsert1</EM></A><A NAME="1673"></A> and <A NAME="tex2html148" |
---|
| 448 | HREF="cuddAllDet.html#cuddCacheLookup1"><EM> cuddCacheLookup1</EM></A><A NAME="1675"></A>. |
---|
| 449 | The second set is |
---|
| 450 | slightly faster than the first, and the third set is slightly faster |
---|
| 451 | than the second. |
---|
| 452 | |
---|
| 453 | <P> |
---|
| 454 | |
---|
| 455 | <H3><A NAME="SECTION00044100000000000000"></A> |
---|
| 456 | <A NAME="976"></A><A NAME="sec:cache-sizing"></A> |
---|
| 457 | <BR> |
---|
| 458 | Cache Sizing |
---|
| 459 | </H3> |
---|
| 460 | |
---|
| 461 | <P> |
---|
| 462 | The size of the cache can increase during the execution of an |
---|
| 463 | application. (There is currently no way to decrease the size of the |
---|
| 464 | cache, though it would not be difficult to do it.) When a cache miss |
---|
| 465 | occurs, the package uses the following criteria to decide whether to |
---|
| 466 | resize the cache: |
---|
| 467 | |
---|
| 468 | <OL> |
---|
| 469 | <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 |
---|
| 470 | place. The limit is the minimum of two values: a value set at |
---|
| 471 | initialization time and possibly modified by the application, which |
---|
| 472 | constitutes the hard limit beyond which the cache will never grow; |
---|
| 473 | and a number that depends on the current total number of slots in |
---|
| 474 | the unique<A NAME="980"></A> table. |
---|
| 475 | </LI> |
---|
| 476 | <LI>If the cache is not too large already, resizing is decided based |
---|
| 477 | on the hit rate. The policy adopted by the CUDD package is |
---|
| 478 | ``reward-based<A NAME="981"></A>." If the cache hit |
---|
| 479 | rate is high, then it is worthwhile to increase the size of the |
---|
| 480 | cache. |
---|
| 481 | </LI> |
---|
| 482 | </OL> |
---|
| 483 | When resizing takes place, the statistical counters <A NAME="983"></A> used to compute the hit rate are reinitialized so as to |
---|
| 484 | prevent immediate resizing. The number of entries is doubled. |
---|
| 485 | |
---|
| 486 | <P> |
---|
| 487 | The rationale for the ``reward-based<A NAME="984"></A>" |
---|
| 488 | policy is as follows. In many BDD/ADD applications the hit rate is |
---|
| 489 | not very sensitive to the size of the cache: It is primarily a |
---|
| 490 | function of the problem instance at hand. If a large hit rate is |
---|
| 491 | observed, chances are that by using a large cache, the results of |
---|
| 492 | large problems (those that would take longer to solve) will survive in |
---|
| 493 | the cache without being overwritten long enough to cause a valuable |
---|
| 494 | cache hit. Notice that when a large problem is solved more than once, |
---|
| 495 | so are its recursively generated subproblems. If the hit rate is |
---|
| 496 | low, the probability of large problems being solved more than once is |
---|
| 497 | low. |
---|
| 498 | |
---|
| 499 | <P> |
---|
| 500 | The other observation about the cache sizing policy is that there is |
---|
| 501 | little point in keeping a cache which is much larger than the unique |
---|
| 502 | table. Every time the unique table ``fills up," garbage collection is |
---|
| 503 | invoked and the cache is cleared of all dead entries. A cache that is |
---|
| 504 | much larger than the unique<A NAME="985"></A> table is therefore |
---|
| 505 | less than fully utilized. |
---|
| 506 | |
---|
| 507 | <P> |
---|
| 508 | |
---|
| 509 | <H3><A NAME="SECTION00044200000000000000"></A> |
---|
| 510 | <A NAME="987"></A><A NAME="sec:local-caches"></A> |
---|
| 511 | <BR> |
---|
| 512 | Local Caches |
---|
| 513 | </H3> |
---|
| 514 | |
---|
| 515 | <P> |
---|
| 516 | Sometimes it may be necessary or convenient to use a local cache. A |
---|
| 517 | local cache can be lossless<A NAME="989"></A> (no results are ever |
---|
| 518 | overwritten), or it may store objects for which |
---|
| 519 | canonical<A NAME="990"></A> representations are not available. One |
---|
| 520 | important fact to keep in mind when using a local cache is that local |
---|
| 521 | caches are not cleared during garbage<A NAME="991"></A> |
---|
| 522 | collection or before reordering. Therefore, it is necessary to |
---|
| 523 | increment the reference<A NAME="992"></A> count of all nodes |
---|
| 524 | pointed by a local cache. (Unless their reference counts are |
---|
| 525 | guaranteed positive in some other way. One such way is by including |
---|
| 526 | all partial results in the global result.) Before disposing of the |
---|
| 527 | local cache, all elements stored in it must be passed to <A NAME="tex2html149" |
---|
| 528 | HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1677"></A>. As |
---|
| 529 | consequence of the fact that all results in a local cache are |
---|
| 530 | referenced, it is generally convenient to store in the local cache |
---|
| 531 | also the result of trivial problems, which are not usually stored in |
---|
| 532 | the global cache. Otherwise, after a recursive call, it is difficult |
---|
| 533 | to tell whether the result is in the cache, and therefore referenced, |
---|
| 534 | or not in the cache, and therefore not referenced. |
---|
| 535 | |
---|
| 536 | <P> |
---|
| 537 | An alternative approach to referencing the results in the local caches |
---|
| 538 | is to install hook functions (see Section <A HREF="node3.html#sec:hooks">3.16</A>) to be |
---|
| 539 | executed before garbage collection. |
---|
| 540 | |
---|
| 541 | <P> |
---|
| 542 | |
---|
| 543 | <H2><A NAME="SECTION00045000000000000000"></A> |
---|
| 544 | <A NAME="998"></A><A NAME="sec:unique"></A> |
---|
| 545 | <BR> |
---|
| 546 | The Unique Table |
---|
| 547 | </H2> |
---|
| 548 | |
---|
| 549 | <P> |
---|
| 550 | A recursive procedure typically splits the operands by expanding with |
---|
| 551 | respect to the topmost variable. Topmost in this context refers to the |
---|
| 552 | variable that is closest to the roots in the current variable order. |
---|
| 553 | The nodes, on the other hand, hold the index, which is invariant with |
---|
| 554 | reordering. Therefore, when splitting, one must use the |
---|
| 555 | permutation<A NAME="1000"></A> array maintained by the |
---|
| 556 | package to get the right level. Access to the permutation array is |
---|
| 557 | provided by the macro <A NAME="tex2html150" |
---|
| 558 | HREF="cuddAllDet.html#cuddI"><EM>cuddI</EM></A><A NAME="1679"></A> for BDDs and ADDs, |
---|
| 559 | and by the macro <A NAME="tex2html151" |
---|
| 560 | HREF="cuddAllDet.html#cuddIZ"><EM>cuddIZ</EM></A><A NAME="1681"></A> for ZDDs. |
---|
| 561 | |
---|
| 562 | <P> |
---|
| 563 | The unique table consists of as many hash<A NAME="1007"></A> tables as there are |
---|
| 564 | variables in use. These has tables are called <EM>unique subtables</EM>. |
---|
| 565 | The sizes of the unique subtables are determined by two criteria: |
---|
| 566 | |
---|
| 567 | <OL> |
---|
| 568 | <LI>The collision<A NAME="1010"></A> lists should be short |
---|
| 569 | to keep access time down. |
---|
| 570 | </LI> |
---|
| 571 | <LI>There should be enough room for dead<A NAME="1011"></A> nodes, to |
---|
| 572 | prevent too frequent garbage<A NAME="1012"></A> collections. |
---|
| 573 | </LI> |
---|
| 574 | </OL> |
---|
| 575 | While the first criterion is fairly straightforward to implement, the |
---|
| 576 | second leaves more room to creativity. The CUDD package tries to |
---|
| 577 | figure out whether more dead node should be allowed to increase |
---|
| 578 | performance. (See also Section <A HREF="node3.html#sec:params">3.4</A>.) There are two |
---|
| 579 | reasons for not doing garbage collection too often. The obvious one is |
---|
| 580 | that it is expensive. The second is that dead nodes may be |
---|
| 581 | reclaimed<A NAME="1015"></A>, if they are the result of a |
---|
| 582 | successful cache lookup. Hence dead nodes may provide a substantial |
---|
| 583 | speed-up if they are kept around long enough. The usefulness of |
---|
| 584 | keeping many dead nodes around varies from application to application, |
---|
| 585 | and from problem instance to problem instance. As in the sizing of the |
---|
| 586 | cache, the CUDD package adopts a |
---|
| 587 | ``reward-based<A NAME="1016"></A>" policy to |
---|
| 588 | decide how much room should be used for the unique table. If the |
---|
| 589 | number of dead nodes reclaimed is large compared to the number of |
---|
| 590 | nodes directly requested from the memory manager, then the CUDD |
---|
| 591 | package assumes that it will be beneficial to allow more room for the |
---|
| 592 | subtables, thereby reducing the frequency of garbage collection. The |
---|
| 593 | package does so by switching between two modes of operation: |
---|
| 594 | |
---|
| 595 | <OL> |
---|
| 596 | <LI>Fast growth<A NAME="1018"></A>: In this mode, the |
---|
| 597 | ratio of dead nodes to total nodes required for garbage collection |
---|
| 598 | is higher than in the slow growth mode to favor resizing |
---|
| 599 | of the subtables. |
---|
| 600 | </LI> |
---|
| 601 | <LI>Slow growth<A NAME="1019"></A>: In this |
---|
| 602 | mode keeping many dead nodes around is not as important as |
---|
| 603 | keeping memory requirements low. |
---|
| 604 | </LI> |
---|
| 605 | </OL> |
---|
| 606 | Switching from one mode to the other is based on the following |
---|
| 607 | criteria: |
---|
| 608 | |
---|
| 609 | <OL> |
---|
| 610 | <LI>If the unique table is already large, only slow growth is |
---|
| 611 | possible. |
---|
| 612 | </LI> |
---|
| 613 | <LI>If the table is small and many dead nodes are being reclaimed, |
---|
| 614 | then fast growth is selected. |
---|
| 615 | </LI> |
---|
| 616 | </OL> |
---|
| 617 | This policy is especially effective when the diagrams being |
---|
| 618 | manipulated have lots of recombination. Notice the interplay of the |
---|
| 619 | cache sizing and unique sizing: Fast growth normally occurs when the |
---|
| 620 | cache hit rate is large. The cache and the unique table then grow in |
---|
| 621 | concert, preserving a healthy balance between their sizes. |
---|
| 622 | |
---|
| 623 | <P> |
---|
| 624 | |
---|
| 625 | <H2><A NAME="SECTION00046000000000000000"></A> |
---|
| 626 | <A NAME="1024"></A><A NAME="sec:async"></A> |
---|
| 627 | <BR> |
---|
| 628 | Allowing Asynchronous Reordering |
---|
| 629 | </H2> |
---|
| 630 | |
---|
| 631 | <P> |
---|
| 632 | Asynchronous reordering is the reordering that is triggered |
---|
| 633 | automatically by the increase of the number of nodes. Asynchronous |
---|
| 634 | reordering takes place when a new internal node must be created, and |
---|
| 635 | the number of nodes has reached a given |
---|
| 636 | threshold<A NAME="1026"></A>. (The threshold is adjusted by |
---|
| 637 | the package every time reordering takes place.) |
---|
| 638 | |
---|
| 639 | <P> |
---|
| 640 | Those procedures that do not create new nodes (e.g., procedures that |
---|
| 641 | count the number of nodes or minterms<A NAME="1027"></A>) need |
---|
| 642 | not worry about asynchronous reordering: No special precaution is |
---|
| 643 | necessary in writing them. |
---|
| 644 | |
---|
| 645 | <P> |
---|
| 646 | Procedures that only manipulate decision diagrams through the exported |
---|
| 647 | functions of the CUDD package also need not concern themselves with |
---|
| 648 | asynchronous reordering. (See Section <A HREF="node3.html#sec:nodes">3.2.1</A> for the |
---|
| 649 | exceptions.) |
---|
| 650 | |
---|
| 651 | <P> |
---|
| 652 | The remaining class of procedures is composed of functions that visit |
---|
| 653 | the diagrams and may create new nodes. All such procedures in the CUDD |
---|
| 654 | package are written so that they can be interrupted by dynamic |
---|
| 655 | reordering. The general approach followed goes under the name of |
---|
| 656 | ``abort and retry<A NAME="1029"></A>." As the name |
---|
| 657 | implies, a computation that is interrupted by dynamic reordering is |
---|
| 658 | aborted and tried again. |
---|
| 659 | |
---|
| 660 | <P> |
---|
| 661 | A recursive procedure that can be interrupted by dynamic reordering |
---|
| 662 | (an interruptible<A NAME="1030"></A> procedure |
---|
| 663 | from now on) is composed of two functions. One is responsible for the |
---|
| 664 | real computation. The other is a simple |
---|
| 665 | wrapper<A NAME="1031"></A>, which tests whether |
---|
| 666 | reordering occurred and restarts the computation if it did. |
---|
| 667 | |
---|
| 668 | <P> |
---|
| 669 | Asynchronous reordering of BDDs and ADDs can only be triggered inside |
---|
| 670 | <A NAME="tex2html152" |
---|
| 671 | HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1683"></A>, when a new node |
---|
| 672 | is about to be created. Likewise, asynchronous reordering of ZDDs can |
---|
| 673 | only be triggered inside <A NAME="tex2html153" |
---|
| 674 | HREF="cuddAllDet.html#cuddUniqueInterZdd"><EM> cuddUniqueInterZdd</EM></A><A NAME="1685"></A>. When |
---|
| 675 | reordering is triggered, three things happen: |
---|
| 676 | |
---|
| 677 | <OL> |
---|
| 678 | <LI><A NAME="tex2html154" |
---|
| 679 | HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1687"></A> returns a |
---|
| 680 | |
---|
| 681 | NULL value; |
---|
| 682 | </LI> |
---|
| 683 | <LI>The flag <EM>reordered</EM> of the manager is set to 1. (0 means |
---|
| 684 | no reordering, while 2 indicates an error occurred during |
---|
| 685 | reordering.) |
---|
| 686 | </LI> |
---|
| 687 | <LI>The counter <EM>reorderings</EM> of the manager is incremented. |
---|
| 688 | The counter is initialized to 0 when the manager is started and can |
---|
| 689 | be accessed by calling <A NAME="tex2html155" |
---|
| 690 | HREF="cuddExtDet.html#Cudd_ReadReorderings"><EM> Cudd_ReadReorderings</EM></A><A NAME="1689"></A>. By |
---|
| 691 | |
---|
| 692 | taking two readings of the counter, an application can determine if |
---|
| 693 | variable reordering has taken place between the first and the second |
---|
| 694 | reading. The package itself, however, does not make use of the |
---|
| 695 | counter: It is mentioned here for completeness. |
---|
| 696 | </LI> |
---|
| 697 | </OL> |
---|
| 698 | |
---|
| 699 | <P> |
---|
| 700 | The recursive procedure that receives a NULL value from <A NAME="tex2html156" |
---|
| 701 | HREF="cuddAllDet.html#cuddUniqueInter"><EM> cuddUniqueInter</EM></A><A NAME="1691"></A> must free all intermediate |
---|
| 702 | results that it may have computed before, and return NULL in its turn. |
---|
| 703 | |
---|
| 704 | <P> |
---|
| 705 | The wrapper<A NAME="1051"></A> function does not |
---|
| 706 | decide whether reordering occurred based on the NULL return value, |
---|
| 707 | because the NULL value may be the result of lack of memory. Instead, |
---|
| 708 | it checks the <EM>reordered</EM> flag. |
---|
| 709 | |
---|
| 710 | <P> |
---|
| 711 | When a recursive procedure calls another recursive procedure that may |
---|
| 712 | cause reordering, it should bypass the wrapper and call the recursive |
---|
| 713 | procedure directly. Otherwise, the calling procedure will not know |
---|
| 714 | whether reordering occurred, and will not be able to restart. This is |
---|
| 715 | the main reason why most recursive procedures are internal, rather |
---|
| 716 | than static. (The wrappers, on the other hand, are mostly exported.) |
---|
| 717 | |
---|
| 718 | <P> |
---|
| 719 | |
---|
| 720 | <H2><A NAME="SECTION00047000000000000000"></A> |
---|
| 721 | <A NAME="1054"></A><A NAME="sec:debug"></A> |
---|
| 722 | <BR> |
---|
| 723 | Debugging |
---|
| 724 | </H2> |
---|
| 725 | |
---|
| 726 | <P> |
---|
| 727 | By defining the symbol DD_DEBUG<A NAME="1056"></A> during compilation, |
---|
| 728 | numerous checks are added to the code. In addition, the procedures |
---|
| 729 | <A NAME="tex2html157" |
---|
| 730 | HREF="cuddExtDet.html#Cudd_DebugCheck"><EM>Cudd_DebugCheck</EM></A><A NAME="1693"></A>, <A NAME="tex2html158" |
---|
| 731 | HREF="cuddExtDet.html#Cudd_CheckKeys"><EM> Cudd_CheckKeys</EM></A><A NAME="1695"></A>, and <A NAME="tex2html159" |
---|
| 732 | HREF="cuddAllDet.html#cuddHeapProfile"><EM> cuddHeapProfile</EM></A><A NAME="1697"></A> can be called at any point |
---|
| 733 | to verify the consistency of the data structure. (<A NAME="tex2html160" |
---|
| 734 | HREF="cuddAllDet.html#cuddHeapProfile"><EM> cuddHeapProfile</EM></A> |
---|
| 735 | is an internal procedure. It is declared in <EM> cuddInt.h</EM><A NAME="1069"></A>.) Procedures <A NAME="tex2html161" |
---|
| 736 | HREF="cuddExtDet.html#Cudd_DebugCheck"><EM>Cudd_DebugCheck</EM></A> |
---|
| 737 | and <A NAME="tex2html162" |
---|
| 738 | HREF="cuddExtDet.html#Cudd_CheckKeys"><EM>Cudd_CheckKeys</EM></A> |
---|
| 739 | are especially useful when CUDD reports |
---|
| 740 | that during garbage collection the number of nodes actually deleted |
---|
| 741 | from the unique table is different from the count of dead nodes kept |
---|
| 742 | by the manager. The error causing the discrepancy may have occurred |
---|
| 743 | much earlier than it is discovered. A few strategicaly placed calls |
---|
| 744 | to the debugging procedures can considerably narrow down the search |
---|
| 745 | for the source of the problem. (For instance, a call to <A NAME="tex2html163" |
---|
| 746 | HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A> |
---|
| 747 | where one to <A NAME="tex2html164" |
---|
| 748 | HREF="cuddExtDet.html#Cudd_Deref"><EM>Cudd_Deref</EM></A> |
---|
| 749 | was required |
---|
| 750 | may be identified in this way.) |
---|
| 751 | |
---|
| 752 | <P> |
---|
| 753 | One of the most common problems encountered in debugging code based on |
---|
| 754 | the CUDD package is a missing call to <A NAME="tex2html165" |
---|
| 755 | HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A><A NAME="1699"></A>. To help |
---|
| 756 | identify this type of problems, the package provides a function called |
---|
| 757 | <A NAME="tex2html166" |
---|
| 758 | HREF="cuddExtDet.html#Cudd_CheckZeroRef"><EM>Cudd_CheckZeroRef</EM></A><A NAME="1701"></A>. This |
---|
| 759 | function should be called immediately before shutting down the |
---|
| 760 | manager. <A NAME="tex2html167" |
---|
| 761 | HREF="cuddExtDet.html#Cudd_CheckZeroRef"><EM>Cudd_CheckZeroRef</EM></A> |
---|
| 762 | checks that the only nodes left |
---|
| 763 | with non-zero reference<A NAME="1086"></A> counts are the |
---|
| 764 | predefined constants, the BDD projection<A NAME="1087"></A> |
---|
| 765 | functions, and nodes whose reference counts are |
---|
| 766 | saturated<A NAME="1088"></A>. |
---|
| 767 | |
---|
| 768 | <P> |
---|
| 769 | For this function to be effective the application must explicitly |
---|
| 770 | dispose of all diagrams to which it has pointers before calling it. |
---|
| 771 | |
---|
| 772 | <P> |
---|
| 773 | |
---|
| 774 | <H2><A NAME="SECTION00048000000000000000"></A> |
---|
| 775 | <A NAME="1090"></A><A NAME="sec:stats"></A> |
---|
| 776 | <BR> |
---|
| 777 | Gathering and Interpreting Statistics |
---|
| 778 | </H2> |
---|
| 779 | |
---|
| 780 | <P> |
---|
| 781 | Function <A NAME="tex2html168" |
---|
| 782 | HREF="cuddExtDet.html#Cudd_PrintInfo"><EM>Cudd_PrintInfo</EM></A><A NAME="1703"></A> can be called |
---|
| 783 | to print out the values of parameters and statistics for a manager. |
---|
| 784 | The output of <A NAME="tex2html169" |
---|
| 785 | HREF="cuddExtDet.html#Cudd_PrintInfo"><EM>Cudd_PrintInfo</EM></A> |
---|
| 786 | is divided in two sections. The |
---|
| 787 | first reports the values of parameters that are under the application |
---|
| 788 | control. The second reports the values of statistical counters and |
---|
| 789 | other non-modifiable parameters. A |
---|
| 790 | quick guide to the interpretation of all these quantities follows. For |
---|
| 791 | ease of exposition, we reverse the order and describe the |
---|
| 792 | non-modifiable parameters first. We'll use a sample run as |
---|
| 793 | example. There is nothing special about this run. |
---|
| 794 | |
---|
| 795 | <P> |
---|
| 796 | |
---|
| 797 | <H3><A NAME="SECTION00048100000000000000"></A> |
---|
| 798 | <A NAME="sec:nonModPar"></A> |
---|
| 799 | <BR> |
---|
| 800 | Non Modifiable Parameters |
---|
| 801 | </H3> |
---|
| 802 | |
---|
| 803 | <P> |
---|
| 804 | The list of non-modifiable parameters starts with: |
---|
| 805 | <PRE> |
---|
| 806 | **** CUDD non-modifiable parameters **** |
---|
| 807 | Memory in use: 32544220 |
---|
| 808 | </PRE> |
---|
| 809 | This is the memory used by CUDD for three things mainly: Unique table |
---|
| 810 | (including all DD nodes in use), node free list, and computed table. |
---|
| 811 | This number almost never decreases in the lifetime of a CUDD manager, |
---|
| 812 | because CUDD does not release memory when it frees nodes. Rather, it |
---|
| 813 | puts the nodes on its own free list. This number is in bytes. It does |
---|
| 814 | not represent the peak memory occupation, because it does not include |
---|
| 815 | the size of data structures created temporarily by some functions (e.g., |
---|
| 816 | local look-up tables). |
---|
| 817 | |
---|
| 818 | <P> |
---|
| 819 | <PRE> |
---|
| 820 | Peak number of nodes: 837018 |
---|
| 821 | </PRE> |
---|
| 822 | This number is the number of nodes that the manager has allocated. |
---|
| 823 | This is not the largest size of the BDDs, because the manager will |
---|
| 824 | normally have some dead nodes and some nodes on the free list. |
---|
| 825 | |
---|
| 826 | <P> |
---|
| 827 | <PRE> |
---|
| 828 | Peak number of live nodes: 836894 |
---|
| 829 | </PRE> |
---|
| 830 | This is the largest number of live nodes that the manager has held |
---|
| 831 | since its creation. |
---|
| 832 | |
---|
| 833 | <P> |
---|
| 834 | <PRE> |
---|
| 835 | Number of BDD variables: 198 |
---|
| 836 | Number of ZDD variables: 0 |
---|
| 837 | </PRE> |
---|
| 838 | These numbers tell us this run was not using ZDDs. |
---|
| 839 | |
---|
| 840 | <P> |
---|
| 841 | <PRE> |
---|
| 842 | Number of cache entries: 1048576 |
---|
| 843 | </PRE> |
---|
| 844 | Current number of slots of the computed table. If one has a |
---|
| 845 | performance problem, this is one of the numbers to look at. The cache |
---|
| 846 | size is always a power of 2. |
---|
| 847 | |
---|
| 848 | <P> |
---|
| 849 | <PRE> |
---|
| 850 | Number of cache look-ups: 2996536 |
---|
| 851 | Number of cache hits: 1187087 |
---|
| 852 | </PRE> |
---|
| 853 | These numbers give an indication of the hit rate in the computed |
---|
| 854 | table. It is not unlikely for model checking runs to get |
---|
| 855 | hit rates even higher than this one (39.62%). |
---|
| 856 | |
---|
| 857 | <P> |
---|
| 858 | <PRE> |
---|
| 859 | Number of cache insertions: 1809473 |
---|
| 860 | Number of cache collisions: 961208 |
---|
| 861 | Number of cache deletions: 0 |
---|
| 862 | </PRE> |
---|
| 863 | A collision<A NAME="1113"></A> occurs when a cache entry is |
---|
| 864 | overwritten. A deletion<A NAME="1114"></A> |
---|
| 865 | occurs when a cache entry is invalidated (e.g., during garbage |
---|
| 866 | collection). If the number of deletions is high compared to the |
---|
| 867 | number of collisions, it means that garbage collection occurs too |
---|
| 868 | often. In this case there were no garbage collections; hence, no |
---|
| 869 | deletions. |
---|
| 870 | |
---|
| 871 | <P> |
---|
| 872 | <PRE> |
---|
| 873 | Cache used slots = 80.90% (expected 82.19%) |
---|
| 874 | </PRE> |
---|
| 875 | Percentage of cache slots that contain a valid entry. If this |
---|
| 876 | number is small, it may signal one of three conditions: |
---|
| 877 | |
---|
| 878 | <OL> |
---|
| 879 | <LI>The cache may have been recently resized and it is still filling |
---|
| 880 | up. |
---|
| 881 | </LI> |
---|
| 882 | <LI>The cache is too large for the BDDs. This should not happen if |
---|
| 883 | the size of the cache is determined by CUDD. |
---|
| 884 | </LI> |
---|
| 885 | <LI>The hash function is not working properly. This is accompanied |
---|
| 886 | by a degradation in performance. Conversely, a degradation in |
---|
| 887 | performance may be due to bad hash function behavior. |
---|
| 888 | </LI> |
---|
| 889 | </OL> |
---|
| 890 | The expected value is computed assuming a uniformly random |
---|
| 891 | distribution of the accesses. If the difference between the measured |
---|
| 892 | value and the expected value is large (unlike this case), the cache is |
---|
| 893 | not working properly. |
---|
| 894 | |
---|
| 895 | <P> |
---|
| 896 | <PRE> |
---|
| 897 | Soft limit for cache size: 1318912 |
---|
| 898 | </PRE> |
---|
| 899 | This number says how large the cache can grow. This limit is based on |
---|
| 900 | the size of the unique table. CUDD uses a reward-based policy for |
---|
| 901 | growing the cache. (See Section <A HREF="node4.html#sec:cache-sizing">4.4.1</A>.) The default |
---|
| 902 | hit rate for resizing is 30% and the value in effect is reported |
---|
| 903 | among the modifiable parameters. |
---|
| 904 | |
---|
| 905 | <P> |
---|
| 906 | <PRE> |
---|
| 907 | Number of buckets in unique table: 329728 |
---|
| 908 | </PRE> |
---|
| 909 | This number is exactly one quarter of the one above. This is indeed |
---|
| 910 | how the soft limit is determined currently, unless the computed table |
---|
| 911 | hits the specified hard limit. (See below.) |
---|
| 912 | |
---|
| 913 | <P> |
---|
| 914 | <PRE> |
---|
| 915 | Used buckets in unique table: 87.96% (expected 87.93%) |
---|
| 916 | </PRE> |
---|
| 917 | Percentage of unique table buckets that contain at least one |
---|
| 918 | node. Remarks analogous to those made about the used cache slots apply. |
---|
| 919 | |
---|
| 920 | <P> |
---|
| 921 | <PRE> |
---|
| 922 | Number of BDD and ADD nodes: 836894 |
---|
| 923 | Number of ZDD nodes: 0 |
---|
| 924 | </PRE> |
---|
| 925 | How many nodes are currently in the unique table, either alive or dead. |
---|
| 926 | |
---|
| 927 | <P> |
---|
| 928 | <PRE> |
---|
| 929 | Number of dead BDD and ADD nodes: 0 |
---|
| 930 | Number of dead ZDD nodes: 0 |
---|
| 931 | </PRE> |
---|
| 932 | Subtract these numbers from those above to get the number of live |
---|
| 933 | nodes. In this case there are no dead nodes because the application |
---|
| 934 | uses delayed dereferencing |
---|
| 935 | <A NAME="tex2html170" |
---|
| 936 | HREF="cuddExtDet.html#Cudd_DelayedDerefBdd"><EM>Cudd_DelayedDerefBdd</EM></A><A NAME="1705"></A>. |
---|
| 937 | |
---|
| 938 | <P> |
---|
| 939 | <PRE> |
---|
| 940 | Total number of nodes allocated: 836894 |
---|
| 941 | </PRE> |
---|
| 942 | This is the total number of nodes that were requested and obtained |
---|
| 943 | from the free list. It never decreases, and is not an indication of |
---|
| 944 | memory occupation after the first garbage collection. Rather, it is a |
---|
| 945 | measure of the package activity. |
---|
| 946 | |
---|
| 947 | <P> |
---|
| 948 | <PRE> |
---|
| 949 | Total number of nodes reclaimed: 0 |
---|
| 950 | </PRE> |
---|
| 951 | These are the nodes that were resuscitated from the dead. If they are |
---|
| 952 | many more than the allocated nodes, and the total |
---|
| 953 | number of slots is low relative to the number of nodes, then one may |
---|
| 954 | want to increase the limit for fast unique table growth. In this case, |
---|
| 955 | the number is 0 because of delayed dereferencing. |
---|
| 956 | |
---|
| 957 | <P> |
---|
| 958 | <PRE> |
---|
| 959 | Garbage collections so far: 0 |
---|
| 960 | Time for garbage collections: 0.00 sec |
---|
| 961 | Reorderings so far: 0 |
---|
| 962 | Time for reordering: 0.00 sec |
---|
| 963 | </PRE> |
---|
| 964 | There is a GC for each reordering. Hence the first count will always be |
---|
| 965 | at least as large as the second. |
---|
| 966 | |
---|
| 967 | <P> |
---|
| 968 | <PRE> |
---|
| 969 | Node swaps in reordering: 0 |
---|
| 970 | </PRE> |
---|
| 971 | This is the number of elementary reordering steps. Each step consists |
---|
| 972 | of the re-expression of one node while swapping two adjacent |
---|
| 973 | variables. This number is a good measure of the amount of work done in |
---|
| 974 | reordering. |
---|
| 975 | |
---|
| 976 | <P> |
---|
| 977 | |
---|
| 978 | <H3><A NAME="SECTION00048200000000000000"></A> |
---|
| 979 | <A NAME="sec:modPar"></A> |
---|
| 980 | <BR> |
---|
| 981 | Modifiable Parameters |
---|
| 982 | </H3> |
---|
| 983 | |
---|
| 984 | <P> |
---|
| 985 | Let us now consider the modifiable parameters, that is, those settings on |
---|
| 986 | which the application or the user has control. |
---|
| 987 | |
---|
| 988 | <P> |
---|
| 989 | <PRE> |
---|
| 990 | **** CUDD modifiable parameters **** |
---|
| 991 | Hard limit for cache size: 8388608 |
---|
| 992 | </PRE> |
---|
| 993 | This number counts entries. Each entry is 16 bytes if CUDD is compiled |
---|
| 994 | to use 32-bit pointers. Two important observations are in order: |
---|
| 995 | |
---|
| 996 | <OL> |
---|
| 997 | <LI>If the datasize limit is set, CUDD will use it to determine this |
---|
| 998 | number automatically. On a Unix system, one can type ``limit" to |
---|
| 999 | verify if this value is set. If the datasize limit is not set, CUDD |
---|
| 1000 | uses a default which is rather small. If you have enough memory (say |
---|
| 1001 | 64MB or more) you should seriously consider <EM>not</EM> using the |
---|
| 1002 | default. So, either set the datasize limit, or override the default |
---|
| 1003 | with <A NAME="tex2html171" |
---|
| 1004 | HREF="cuddExtDet.html#Cudd_SetMaxCacheHard"><EM>Cudd_SetMaxCacheHard</EM></A><A NAME="1707"></A>. |
---|
| 1005 | </LI> |
---|
| 1006 | <LI>If a process seems to be going nowhere, a small value for |
---|
| 1007 | |
---|
| 1008 | this parameter may be the culprit. One cannot overemphasize the |
---|
| 1009 | importance of the computed table in BDD algorithms. |
---|
| 1010 | </LI> |
---|
| 1011 | </OL> |
---|
| 1012 | In this case the limit was automatically set for a target maximum |
---|
| 1013 | memory occupation of 104 MB. |
---|
| 1014 | |
---|
| 1015 | <P> |
---|
| 1016 | <PRE> |
---|
| 1017 | Cache hit threshold for resizing: 15% |
---|
| 1018 | </PRE> |
---|
| 1019 | This number can be changed if one suspects performance is hindered by |
---|
| 1020 | the small size of the cache, and the cache is not growing towards the |
---|
| 1021 | soft limit sufficiently fast. In such a case one can change the |
---|
| 1022 | default 30% to 15% (as in this case) or even 1%. |
---|
| 1023 | |
---|
| 1024 | <P> |
---|
| 1025 | <PRE> |
---|
| 1026 | Garbage collection enabled: yes |
---|
| 1027 | </PRE> |
---|
| 1028 | One can disable it, but there are few good reasons for doing |
---|
| 1029 | so. It is normally preferable to raise the limit for fast unique table |
---|
| 1030 | growth. (See below.) |
---|
| 1031 | |
---|
| 1032 | <P> |
---|
| 1033 | <PRE> |
---|
| 1034 | Limit for fast unique table growth: 1363148 |
---|
| 1035 | </PRE> |
---|
| 1036 | See Section <A HREF="node4.html#sec:unique">4.5</A> and the comments above about reclaimed |
---|
| 1037 | nodes and hard limit for the cache size. This value was chosen |
---|
| 1038 | automatically by CUDD for a datasize limit of 1 GB. |
---|
| 1039 | |
---|
| 1040 | <P> |
---|
| 1041 | <PRE> |
---|
| 1042 | Maximum number of variables sifted per reordering: 1000 |
---|
| 1043 | Maximum number of variable swaps per reordering: 2000000 |
---|
| 1044 | Maximum growth while sifting a variable: 1.2 |
---|
| 1045 | </PRE> |
---|
| 1046 | Lowering these numbers will cause reordering to be less accurate and |
---|
| 1047 | faster. Results are somewhat unpredictable, because larger BDDs after one |
---|
| 1048 | reordering do not necessarily mean the process will go faster or slower. |
---|
| 1049 | |
---|
| 1050 | <P> |
---|
| 1051 | <PRE> |
---|
| 1052 | Dynamic reordering of BDDs enabled: yes |
---|
| 1053 | Default BDD reordering method: 4 |
---|
| 1054 | Dynamic reordering of ZDDs enabled: no |
---|
| 1055 | Default ZDD reordering method: 4 |
---|
| 1056 | </PRE> |
---|
| 1057 | These lines tell whether automatic reordering can take place and |
---|
| 1058 | what method would be used. The mapping from numbers to methods is in |
---|
| 1059 | <TT>cudd.h</TT>. One may want to try different BDD |
---|
| 1060 | reordering methods. If variable groups are used, however, one should |
---|
| 1061 | not expect to see big differences, because CUDD uses the reported |
---|
| 1062 | method only to reorder each leaf variable group (typically corresponding |
---|
| 1063 | present and next state variables). For the relative order of the |
---|
| 1064 | groups, it always uses the same algorithm, which is effectively |
---|
| 1065 | sifting. |
---|
| 1066 | |
---|
| 1067 | <P> |
---|
| 1068 | As for enabling dynamic reordering or not, a sensible recommendation is the |
---|
| 1069 | following: Unless the circuit is rather small or one has a pretty good |
---|
| 1070 | idea of what the order should be, reordering should be enabled. |
---|
| 1071 | |
---|
| 1072 | <P> |
---|
| 1073 | <PRE> |
---|
| 1074 | Realignment of ZDDs to BDDs enabled: no |
---|
| 1075 | Realignment of BDDs to ZDDs enabled: no |
---|
| 1076 | Dead nodes counted in triggering reordering: no |
---|
| 1077 | Group checking criterion: 7 |
---|
| 1078 | Recombination threshold: 0 |
---|
| 1079 | Symmetry violation threshold: 0 |
---|
| 1080 | Arc violation threshold: 0 |
---|
| 1081 | GA population size: 0 |
---|
| 1082 | Number of crossovers for GA: 0 |
---|
| 1083 | </PRE> |
---|
| 1084 | Parameters for reordering. See the documentation of the functions used |
---|
| 1085 | to control these parameters for the details. |
---|
| 1086 | |
---|
| 1087 | <P> |
---|
| 1088 | <PRE> |
---|
| 1089 | Next reordering threshold: 100000 |
---|
| 1090 | </PRE> |
---|
| 1091 | When the number of nodes crosses this threshold, reordering will be |
---|
| 1092 | triggered. (If enabled; in this case it is not.) This parameter is |
---|
| 1093 | updated by the package whenever reordering takes place. The |
---|
| 1094 | application can change it, for instance at start-up. Another |
---|
| 1095 | possibility is to use a hook function (see Section <A HREF="node3.html#sec:hooks">3.16</A>) to |
---|
| 1096 | override the default updating policy. |
---|
| 1097 | |
---|
| 1098 | <P> |
---|
| 1099 | |
---|
| 1100 | <H3><A NAME="SECTION00048300000000000000"></A> |
---|
| 1101 | <A NAME="sec:extendedStats"></A> |
---|
| 1102 | <BR> |
---|
| 1103 | Extended Statistics and Reporting |
---|
| 1104 | </H3> |
---|
| 1105 | |
---|
| 1106 | <P> |
---|
| 1107 | The following symbols can be defined during compilation to increase |
---|
| 1108 | the amount of statistics gathered and the number of messages produced |
---|
| 1109 | by the package: |
---|
| 1110 | |
---|
| 1111 | <UL> |
---|
| 1112 | <LI>DD_STATS<A NAME="1171"></A>; |
---|
| 1113 | </LI> |
---|
| 1114 | <LI>DD_CACHE_PROFILE<A NAME="1172"></A>; |
---|
| 1115 | </LI> |
---|
| 1116 | <LI>DD_UNIQUE_PROFILE<A NAME="1173"></A>. |
---|
| 1117 | </LI> |
---|
| 1118 | <LI>DD_VERBOSE<A NAME="1174"></A>; |
---|
| 1119 | </LI> |
---|
| 1120 | </UL> |
---|
| 1121 | Defining DD_CACHE_PROFILE causes each entry of the cache to include |
---|
| 1122 | an access counter, which is used to compute simple statistics on the |
---|
| 1123 | distribution of the keys. |
---|
| 1124 | |
---|
| 1125 | <P> |
---|
| 1126 | |
---|
| 1127 | <H2><A NAME="SECTION00049000000000000000"></A> |
---|
| 1128 | <A NAME="sec:doc"></A><A NAME="1178"></A> |
---|
| 1129 | <BR> |
---|
| 1130 | Guidelines for Documentation |
---|
| 1131 | </H2> |
---|
| 1132 | |
---|
| 1133 | <P> |
---|
| 1134 | The documentation of the CUDD functions is extracted automatically |
---|
| 1135 | from the sources by Stephen Edwards's extdoc. (The Ext system is |
---|
| 1136 | available via anonymous FTP<A NAME="1179"></A> from |
---|
| 1137 | <A NAME="tex2html172" |
---|
| 1138 | HREF="ftp://ic.eecs.berkeley.edu"><TT>ic.eecs.berkeley.edu</TT></A>.) |
---|
| 1139 | The following guidelines are followed in CUDD to insure consistent and |
---|
| 1140 | effective use of automatic extraction. It is recommended that |
---|
| 1141 | extensions to CUDD follow the same documentation guidelines. |
---|
| 1142 | |
---|
| 1143 | <UL> |
---|
| 1144 | <LI>The documentation of an exported procedure should be sufficient |
---|
| 1145 | to allow one to use it without reading the code. It is not necessary |
---|
| 1146 | to explain how the procedure works; only what it does. |
---|
| 1147 | </LI> |
---|
| 1148 | <LI>The <I>SeeAlso</I><A NAME="1411"></A> |
---|
| 1149 | fields should be space-separated lists of function names. The |
---|
| 1150 | <I>SeeAlso</I> field of an exported procedure should only reference |
---|
| 1151 | other exported procedures. The <I>SeeAlso</I> field of an internal |
---|
| 1152 | procedure may reference other internal procedures as well as |
---|
| 1153 | exported procedures, but no static procedures. |
---|
| 1154 | </LI> |
---|
| 1155 | <LI>The return values are detailed in the |
---|
| 1156 | <I>Description</I><A NAME="1412"></A> |
---|
| 1157 | field, not in the |
---|
| 1158 | <I>Synopsis</I><A NAME="1413"></A> field. |
---|
| 1159 | </LI> |
---|
| 1160 | <LI>The parameters are documented alongside their declarations. |
---|
| 1161 | Further comments may appear in the <I>Description</I> field. |
---|
| 1162 | </LI> |
---|
| 1163 | <LI>If the <I>Description</I> field is non-empty--which is the |
---|
| 1164 | normal case for an exported procedure--then the synopsis is |
---|
| 1165 | repeated--possibly slightly changed--at the beginning of the |
---|
| 1166 | <I>Description</I> field. This is so because extdoc will not put the |
---|
| 1167 | synopsis in the same HTML file<A NAME="1194"></A> as |
---|
| 1168 | the description. |
---|
| 1169 | </LI> |
---|
| 1170 | <LI>The <I>Synopsis</I> field should be about one line long. |
---|
| 1171 | </LI> |
---|
| 1172 | </UL> |
---|
| 1173 | |
---|
| 1174 | <P> |
---|
| 1175 | <HR> |
---|
| 1176 | <!--Navigation Panel--> |
---|
| 1177 | <A NAME="tex2html313" |
---|
| 1178 | HREF="node5.html"> |
---|
| 1179 | <IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next" |
---|
| 1180 | SRC="icons/next.png"></A> |
---|
| 1181 | <A NAME="tex2html309" |
---|
| 1182 | HREF="cuddIntro.html"> |
---|
| 1183 | <IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up" |
---|
| 1184 | SRC="icons/up.png"></A> |
---|
| 1185 | <A NAME="tex2html303" |
---|
| 1186 | HREF="node3.html"> |
---|
| 1187 | <IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous" |
---|
| 1188 | SRC="icons/prev.png"></A> |
---|
| 1189 | <A NAME="tex2html311" |
---|
| 1190 | HREF="node8.html"> |
---|
| 1191 | <IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index" |
---|
| 1192 | SRC="icons/index.png"></A> |
---|
| 1193 | <BR> |
---|
| 1194 | <B> Next:</B> <A NAME="tex2html314" |
---|
| 1195 | HREF="node5.html">The C++ Interface</A> |
---|
| 1196 | <B> Up:</B> <A NAME="tex2html310" |
---|
| 1197 | HREF="cuddIntro.html">CUDD: CU Decision Diagram</A> |
---|
| 1198 | <B> Previous:</B> <A NAME="tex2html304" |
---|
| 1199 | HREF="node3.html">User's Manual</A> |
---|
| 1200 |   <B> <A NAME="tex2html312" |
---|
| 1201 | HREF="node8.html">Index</A></B> |
---|
| 1202 | <!--End of Navigation Panel--> |
---|
| 1203 | <ADDRESS> |
---|
| 1204 | Fabio Somenzi |
---|
| 1205 | 2005-05-17 |
---|
| 1206 | </ADDRESS> |
---|
| 1207 | </BODY> |
---|
| 1208 | </HTML> |
---|