source: vis_dev/glu-2.1/src/cuBdd/doc/node4.html@ 8

Last change on this file since 8 was 8, checked in by cecile, 15 years ago

src glu
File size: 46.4 KB
Line 
1<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
2
3<!--Converted with LaTeX2HTML 2K.1beta (1.47)
4original 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 &nbsp <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>
114Programmer's Manual
115</H1>
116
117<P>
118This section provides additional detail on the working of the CUDD
119package and on the programming conventions followed in its writing.
120The additional detail should help those who want to write procedures
121that 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>
128Compiling and Linking
129</H2>
130
131<P>
132If 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
134diagram) you need to add
135<PRE>
136#include "cuddInt.h"
137</PRE>
138to your source files. In addition, you should link <code>libcudd.a</code> to
139your executable. Some platforms require specific compiler and linker
140flags. Refer to the <TT>Makefile</TT> in the top level directory of the
141distribution.
142
143<P>
144
145<H2><A NAME="SECTION00042000000000000000"></A>
146<A NAME="800"></A><A NAME="sec:ref"></A>
147<BR>
148Reference Counts
149</H2>
150
151<P>
152Garbage<A NAME="802"></A> collection in the CUDD package is
153based on reference counts. Each node stores the sum of the external
154references and internal references. An internal BDD or ADD node is
155created by a call to <A NAME="tex2html110"
156 HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1605"></A>, an
157internal 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
159terminal<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
161these functions is new, its reference count is zero. The function
162that 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
166increasing the reference count of the node. This is accomplished by
167calling <A NAME="tex2html116"
168 HREF="cuddExtDet.html#Cudd_Ref"><EM>Cudd_Ref</EM></A><A NAME="1617"></A>.
169
170<P>
171When a function is no longer needed by an application, the memory used
172by 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
174ADDs) 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.
178If 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>
192For instance, if the diagram of a function does not share any nodes
193with 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
196its root will cause all the nodes of the diagram to become dead.
197
198<P>
199When the number of dead nodes reaches a given level (dynamically
200determined by the package) garbage collection takes place. During
201garbage<A NAME="844"></A> collection dead nodes are returned
202to the node free list<A NAME="845"></A>.
203
204<P>
205When a new node is created, it is important to increase its
206reference<A NAME="846"></A> count before one of the two
207following 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
213to <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
219function 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
225to a function that may eventually cause a call to them.
226</LI>
227</OL>
228In practice, it is recommended to increase the reference count as soon
229as 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>
236NULL Return Values
237</H3>
238
239<P>
240The interface to the memory management functions (e.g., malloc) used by CUDD
241intercepts NULL return values and calls a handler. The default handler
242exits with an error message. If the application does not install
243another handler, therefore, a NULL return value from an exported
244function of CUDD signals an internal error.
245
246<P>
247If the aplication, however, installs another handler that lets
248execution continue, a NULL pointer returned by an exported function
249typically 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
251ascertain the nature of the problem.
252
253<P>
254An application that tests for the result being NULL can try some
255remedial action, if it runs out of memory. For instance, it may free
256some memory that is not strictly necessary, or try a slower algorithm
257that takes less space. As an example, CUDD overrides the default
258handler when trying to enlarge the cache or increase the number of
259slots of the unique table. If the allocation fails, the package prints
260out 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>
271It is often the case that a recursive procedure has to protect the
272result it is going to return, while it disposes of intermediate
273results. (See the previous discussion on when to increase reference
274counts.) Once the intermediate results have been properly disposed
275of, the final result must be returned to its pristine state, in which
276the 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
279erroneously make some nodes dead. Therefore, the package provides a
280different function: <A NAME="tex2html129"
281 HREF="cuddExtDet.html#Cudd_Deref"><EM>Cudd_Deref</EM></A><A NAME="1641"></A>. This
282function is not recursive, and does not change the dead node counts.
283Its use is almost exclusively the one just described: Decreasing the
284reference count of the root of the final result before returning from
285a recursive procedure.
286
287<P>
288
289<H3><A NAME="SECTION00042300000000000000"></A>
290<A NAME="881"></A><A NAME="sec:noref"></A>
291<BR>
292When Increasing the Reference Count is Unnecessary
293</H3>
294
295<P>
296When a copy of a predefined constant<A NAME="883"></A> or of a
297simple 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
300these simple functions are guaranteed to have reference counts greater
301than 0 at all times. If no call to <A NAME="tex2html131"
302 HREF="cuddExtDet.html#Cudd_Ref"><EM>Cudd_Ref</EM></A>
303is made, then no
304attempt 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>
307should 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>
314Saturating Increments and Decrements
315</H3>
316
317<P>
318On 32-bit machines, the CUDD package stores the
319reference<A NAME="899"></A> counts in unsigned short int's.
320For large diagrams, it is possible for some reference counts to exceed
321the capacity of an unsigned short int. Therefore, increments and
322decrements of reference counts are <EM>saturating</EM>. This means that
323once a reference count has reached the maximum possible value, it is
324no 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
330nodes that have no references may not be declared dead. This may
331result in a small waste of memory, which is normally more than offset
332by the reduction in size of the node structure.
333
334<P>
335When using 64-bit pointers, there is normally no memory advantage from
336using short int's instead of int's in a DdNode. Therefore, increments
337and decrements are not saturating in that case. What option is in
338effect depends on two macros, SIZEOF_VOID_P<A NAME="912"></A>
339and SIZEOF_INT<A NAME="913"></A>, defined in the external
340header<A NAME="914"></A> file (<EM>cudd.h</EM><A NAME="916"></A>). The
341increments and decrements of the reference counts are performed using
342two 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
345SIZEOF_VOID_P<A NAME="923"></A> and
346SIZEOF_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>
353Complement Arcs
354</H2>
355
356<P>
357If ADDs are restricted to use only the constants 0 and 1, they behave
358like BDDs without complement arcs. It is normally easier to write code
359that manipulates 0-1 ADDs, than to write code for BDDs. However,
360complementation is trivial with complement arcs, and is not trivial
361without. As a consequence, with complement arcs it is possible to
362check for more terminal cases and it is possible to apply De Morgan's
363laws to reduce problems that are essentially identical to a standard
364form. This in turn increases the utilization of the cache<A NAME="928"></A>.
365
366<P>
367The complement attribute is stored in the least significant bit of the
368``else" pointer of each node. An external pointer to a function can
369also be complemented. The ``then" pointer to a node, on the other
370hand, is always <EM>regular<A NAME="929"></A></EM>. It is a mistake to
371use a<A NAME="930"></A> pointer as it is to address memory. Instead, it
372is always necessary to obtain a regular version of it. This is
373normally 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
375call <A NAME="tex2html141"
376 HREF="cuddAllDet.html#cuddUniqueInter"><EM>cuddUniqueInter</EM></A><A NAME="1661"></A> with a
377complemented ``then" child as argument. The calling procedure must
378apply 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
380complement 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>
387The Cache
388</H2>
389
390<P>
391Each entry of the cache consists of five fields: The operator, three
392pointers to operands and a pointer to the result. The operator and the
393three pointers to the operands are combined to form three words. The
394combination 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>
408The cache does not contribute to the reference
409<A NAME="945"></A>
410counts of the nodes. The fact that the cache contains a
411pointer to a node does not imply that the node is alive. Instead, when
412garbage<A NAME="946"></A> collection takes place, all entries
413of the cache pointing to dead<A NAME="947"></A> nodes are cleared.
414
415<P>
416The cache is also cleared (of all entries) when dynamic
417reordering<A NAME="948"></A> takes place. In both cases, the entries
418removed from the cache are about to become invalid.
419
420<P>
421All operands and results in a cache entry must be pointers to
422DdNodes<A NAME="949"></A>. If a function produces more than one result,
423or 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>
434Support of the former solution is under development. (See <TT> cuddLCache.c</TT>..) Support for the latter solution may be provided
435in future versions of the package.
436
437<P>
438There are three sets of interface<A NAME="956"></A> functions to
439the 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
442functions 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>.
445The second set is for
446functions 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>.
449The second set is
450slightly faster than the first, and the third set is slightly faster
451than 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>
458Cache Sizing
459</H3>
460
461<P>
462The size of the cache can increase during the execution of an
463application. (There is currently no way to decrease the size of the
464cache, though it would not be difficult to do it.) When a cache miss
465occurs, the package uses the following criteria to decide whether to
466resize 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>
483When resizing takes place, the statistical counters <A NAME="983"></A> used to compute the hit rate are reinitialized so as to
484prevent immediate resizing. The number of entries is doubled.
485
486<P>
487The rationale for the ``reward-based<A NAME="984"></A>"
488policy is as follows. In many BDD/ADD applications the hit rate is
489not very sensitive to the size of the cache: It is primarily a
490function of the problem instance at hand. If a large hit rate is
491observed, chances are that by using a large cache, the results of
492large problems (those that would take longer to solve) will survive in
493the cache without being overwritten long enough to cause a valuable
494cache hit. Notice that when a large problem is solved more than once,
495so are its recursively generated subproblems. If the hit rate is
496low, the probability of large problems being solved more than once is
497low.
498
499<P>
500The other observation about the cache sizing policy is that there is
501little point in keeping a cache which is much larger than the unique
502table. Every time the unique table ``fills up," garbage collection is
503invoked and the cache is cleared of all dead entries. A cache that is
504much larger than the unique<A NAME="985"></A> table is therefore
505less 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>
512Local Caches
513</H3>
514
515<P>
516Sometimes it may be necessary or convenient to use a local cache. A
517local cache can be lossless<A NAME="989"></A> (no results are ever
518overwritten), or it may store objects for which
519canonical<A NAME="990"></A> representations are not available. One
520important fact to keep in mind when using a local cache is that local
521caches are not cleared during garbage<A NAME="991"></A>
522collection or before reordering. Therefore, it is necessary to
523increment the reference<A NAME="992"></A> count of all nodes
524pointed by a local cache. (Unless their reference counts are
525guaranteed positive in some other way. One such way is by including
526all partial results in the global result.) Before disposing of the
527local 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
529consequence of the fact that all results in a local cache are
530referenced, it is generally convenient to store in the local cache
531also the result of trivial problems, which are not usually stored in
532the global cache. Otherwise, after a recursive call, it is difficult
533to tell whether the result is in the cache, and therefore referenced,
534or not in the cache, and therefore not referenced.
535
536<P>
537An alternative approach to referencing the results in the local caches
538is to install hook functions (see Section&nbsp;<A HREF="node3.html#sec:hooks">3.16</A>) to be
539executed 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>
546The Unique Table
547</H2>
548
549<P>
550A recursive procedure typically splits the operands by expanding with
551respect to the topmost variable. Topmost in this context refers to the
552variable that is closest to the roots in the current variable order.
553The nodes, on the other hand, hold the index, which is invariant with
554reordering. Therefore, when splitting, one must use the
555permutation<A NAME="1000"></A> array maintained by the
556package to get the right level. Access to the permutation array is
557provided by the macro <A NAME="tex2html150"
558 HREF="cuddAllDet.html#cuddI"><EM>cuddI</EM></A><A NAME="1679"></A> for BDDs and ADDs,
559and by the macro <A NAME="tex2html151"
560 HREF="cuddAllDet.html#cuddIZ"><EM>cuddIZ</EM></A><A NAME="1681"></A> for ZDDs.
561
562<P>
563The unique table consists of as many hash<A NAME="1007"></A> tables as there are
564variables in use. These has tables are called <EM>unique subtables</EM>.
565The 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>
575While the first criterion is fairly straightforward to implement, the
576second leaves more room to creativity. The CUDD package tries to
577figure out whether more dead node should be allowed to increase
578performance. (See also Section&nbsp;<A HREF="node3.html#sec:params">3.4</A>.) There are two
579reasons for not doing garbage collection too often. The obvious one is
580that it is expensive. The second is that dead nodes may be
581reclaimed<A NAME="1015"></A>, if they are the result of a
582successful cache lookup. Hence dead nodes may provide a substantial
583speed-up if they are kept around long enough. The usefulness of
584keeping many dead nodes around varies from application to application,
585and from problem instance to problem instance. As in the sizing of the
586cache, the CUDD package adopts a
587``reward-based<A NAME="1016"></A>" policy to
588decide how much room should be used for the unique table. If the
589number of dead nodes reclaimed is large compared to the number of
590nodes directly requested from the memory manager, then the CUDD
591package assumes that it will be beneficial to allow more room for the
592subtables, thereby reducing the frequency of garbage collection. The
593package 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>
606Switching from one mode to the other is based on the following
607criteria:
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>
617This policy is especially effective when the diagrams being
618manipulated have lots of recombination. Notice the interplay of the
619cache sizing and unique sizing: Fast growth normally occurs when the
620cache hit rate is large. The cache and the unique table then grow in
621concert, 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>
628Allowing Asynchronous Reordering
629</H2>
630
631<P>
632Asynchronous reordering is the reordering that is triggered
633automatically by the increase of the number of nodes. Asynchronous
634reordering takes place when a new internal node must be created, and
635the number of nodes has reached a given
636threshold<A NAME="1026"></A>. (The threshold is adjusted by
637the package every time reordering takes place.)
638
639<P>
640Those procedures that do not create new nodes (e.g., procedures that
641count the number of nodes or minterms<A NAME="1027"></A>) need
642not worry about asynchronous reordering: No special precaution is
643necessary in writing them.
644
645<P>
646Procedures that only manipulate decision diagrams through the exported
647functions of the CUDD package also need not concern themselves with
648asynchronous reordering. (See Section&nbsp;<A HREF="node3.html#sec:nodes">3.2.1</A> for the
649exceptions.)
650
651<P>
652The remaining class of procedures is composed of functions that visit
653the diagrams and may create new nodes. All such procedures in the CUDD
654package are written so that they can be interrupted by dynamic
655reordering. The general approach followed goes under the name of
656``abort and retry<A NAME="1029"></A>." As the name
657implies, a computation that is interrupted by dynamic reordering is
658aborted and tried again.
659
660<P>
661A recursive procedure that can be interrupted by dynamic reordering
662(an interruptible<A NAME="1030"></A> procedure
663from now on) is composed of two functions. One is responsible for the
664real computation. The other is a simple
665wrapper<A NAME="1031"></A>, which tests whether
666reordering occurred and restarts the computation if it did.
667
668<P>
669Asynchronous 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
672is about to be created. Likewise, asynchronous reordering of ZDDs can
673only be triggered inside <A NAME="tex2html153"
674 HREF="cuddAllDet.html#cuddUniqueInterZdd"><EM> cuddUniqueInterZdd</EM></A><A NAME="1685"></A>. When
675reordering 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
681NULL 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
692taking 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>
700The 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
702results that it may have computed before, and return NULL in its turn.
703
704<P>
705The wrapper<A NAME="1051"></A> function does not
706decide whether reordering occurred based on the NULL return value,
707because the NULL value may be the result of lack of memory. Instead,
708it checks the <EM>reordered</EM> flag.
709
710<P>
711When a recursive procedure calls another recursive procedure that may
712cause reordering, it should bypass the wrapper and call the recursive
713procedure directly. Otherwise, the calling procedure will not know
714whether reordering occurred, and will not be able to restart. This is
715the main reason why most recursive procedures are internal, rather
716than 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>
723Debugging
724</H2>
725
726<P>
727By defining the symbol DD_DEBUG<A NAME="1056"></A> during compilation,
728numerous 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
733to verify the consistency of the data structure. (<A NAME="tex2html160"
734 HREF="cuddAllDet.html#cuddHeapProfile"><EM> cuddHeapProfile</EM></A>
735is 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>
737and <A NAME="tex2html162"
738 HREF="cuddExtDet.html#Cudd_CheckKeys"><EM>Cudd_CheckKeys</EM></A>
739are especially useful when CUDD reports
740that during garbage collection the number of nodes actually deleted
741from the unique table is different from the count of dead nodes kept
742by the manager. The error causing the discrepancy may have occurred
743much earlier than it is discovered. A few strategicaly placed calls
744to the debugging procedures can considerably narrow down the search
745for the source of the problem. (For instance, a call to <A NAME="tex2html163"
746 HREF="cuddExtDet.html#Cudd_RecursiveDeref"><EM> Cudd_RecursiveDeref</EM></A>
747where one to <A NAME="tex2html164"
748 HREF="cuddExtDet.html#Cudd_Deref"><EM>Cudd_Deref</EM></A>
749was required
750may be identified in this way.)
751
752<P>
753One of the most common problems encountered in debugging code based on
754the 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
756identify 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
759function should be called immediately before shutting down the
760manager. <A NAME="tex2html167"
761 HREF="cuddExtDet.html#Cudd_CheckZeroRef"><EM>Cudd_CheckZeroRef</EM></A>
762checks that the only nodes left
763with non-zero reference<A NAME="1086"></A> counts are the
764predefined constants, the BDD projection<A NAME="1087"></A>
765functions, and nodes whose reference counts are
766saturated<A NAME="1088"></A>.
767
768<P>
769For this function to be effective the application must explicitly
770dispose 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>
777Gathering and Interpreting Statistics
778</H2>
779
780<P>
781Function <A NAME="tex2html168"
782 HREF="cuddExtDet.html#Cudd_PrintInfo"><EM>Cudd_PrintInfo</EM></A><A NAME="1703"></A> can be called
783to print out the values of parameters and statistics for a manager.
784The output of <A NAME="tex2html169"
785 HREF="cuddExtDet.html#Cudd_PrintInfo"><EM>Cudd_PrintInfo</EM></A>
786is divided in two sections. The
787first reports the values of parameters that are under the application
788control. The second reports the values of statistical counters and
789other non-modifiable parameters. A
790quick guide to the interpretation of all these quantities follows. For
791ease of exposition, we reverse the order and describe the
792non-modifiable parameters first. We'll use a sample run as
793example. 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>
800Non Modifiable Parameters
801</H3>
802
803<P>
804The list of non-modifiable parameters starts with:
805<PRE>
806 **** CUDD non-modifiable parameters ****
807 Memory in use: 32544220
808</PRE>
809This 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.
811This number almost never decreases in the lifetime of a CUDD manager,
812because CUDD does not release memory when it frees nodes. Rather, it
813puts the nodes on its own free list. This number is in bytes. It does
814not represent the peak memory occupation, because it does not include
815the size of data structures created temporarily by some functions (e.g.,
816local look-up tables).
817
818<P>
819<PRE>
820 Peak number of nodes: 837018
821</PRE>
822This number is the number of nodes that the manager has allocated.
823This is not the largest size of the BDDs, because the manager will
824normally 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>
830This is the largest number of live nodes that the manager has held
831since its creation.
832
833<P>
834<PRE>
835 Number of BDD variables: 198
836 Number of ZDD variables: 0
837</PRE>
838These numbers tell us this run was not using ZDDs.
839
840<P>
841<PRE>
842 Number of cache entries: 1048576
843</PRE>
844Current number of slots of the computed table. If one has a
845performance problem, this is one of the numbers to look at. The cache
846size 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>
853These numbers give an indication of the hit rate in the computed
854table. It is not unlikely for model checking runs to get
855hit 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>
863A collision<A NAME="1113"></A> occurs when a cache entry is
864overwritten. A deletion<A NAME="1114"></A>
865occurs when a cache entry is invalidated (e.g., during garbage
866collection). If the number of deletions is high compared to the
867number of collisions, it means that garbage collection occurs too
868often. In this case there were no garbage collections; hence, no
869deletions.
870
871<P>
872<PRE>
873 Cache used slots = 80.90% (expected 82.19%)
874</PRE>
875Percentage of cache slots that contain a valid entry. If this
876number 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>
890The expected value is computed assuming a uniformly random
891distribution of the accesses. If the difference between the measured
892value and the expected value is large (unlike this case), the cache is
893not working properly.
894
895<P>
896<PRE>
897 Soft limit for cache size: 1318912
898</PRE>
899This number says how large the cache can grow. This limit is based on
900the size of the unique table. CUDD uses a reward-based policy for
901growing the cache. (See Section&nbsp;<A HREF="node4.html#sec:cache-sizing">4.4.1</A>.) The default
902hit rate for resizing is 30% and the value in effect is reported
903among the modifiable parameters.
904
905<P>
906<PRE>
907 Number of buckets in unique table: 329728
908</PRE>
909This number is exactly one quarter of the one above. This is indeed
910how the soft limit is determined currently, unless the computed table
911hits the specified hard limit. (See below.)
912
913<P>
914<PRE>
915 Used buckets in unique table: 87.96% (expected 87.93%)
916</PRE>
917Percentage of unique table buckets that contain at least one
918node. 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>
925How 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>
932Subtract these numbers from those above to get the number of live
933nodes. In this case there are no dead nodes because the application
934uses 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>
942This is the total number of nodes that were requested and obtained
943from the free list. It never decreases, and is not an indication of
944memory occupation after the first garbage collection. Rather, it is a
945measure of the package activity.
946
947<P>
948<PRE>
949 Total number of nodes reclaimed: 0
950</PRE>
951These are the nodes that were resuscitated from the dead. If they are
952many more than the allocated nodes, and the total
953number of slots is low relative to the number of nodes, then one may
954want to increase the limit for fast unique table growth. In this case,
955the 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>
964There is a GC for each reordering. Hence the first count will always be
965at least as large as the second.
966
967<P>
968<PRE>
969 Node swaps in reordering: 0
970</PRE>
971This is the number of elementary reordering steps. Each step consists
972of the re-expression of one node while swapping two adjacent
973variables. This number is a good measure of the amount of work done in
974reordering.
975
976<P>
977
978<H3><A NAME="SECTION00048200000000000000"></A>
979<A NAME="sec:modPar"></A>
980<BR>
981Modifiable Parameters
982</H3>
983
984<P>
985Let us now consider the modifiable parameters, that is, those settings on
986which 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>
993This number counts entries. Each entry is 16 bytes if CUDD is compiled
994to 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
1008this parameter may be the culprit. One cannot overemphasize the
1009 importance of the computed table in BDD algorithms.
1010</LI>
1011</OL>
1012In this case the limit was automatically set for a target maximum
1013memory occupation of 104 MB.
1014
1015<P>
1016<PRE>
1017 Cache hit threshold for resizing: 15%
1018</PRE>
1019This number can be changed if one suspects performance is hindered by
1020the small size of the cache, and the cache is not growing towards the
1021soft limit sufficiently fast. In such a case one can change the
1022default 30% to 15% (as in this case) or even 1%.
1023
1024<P>
1025<PRE>
1026 Garbage collection enabled: yes
1027</PRE>
1028One can disable it, but there are few good reasons for doing
1029so. It is normally preferable to raise the limit for fast unique table
1030growth. (See below.)
1031
1032<P>
1033<PRE>
1034 Limit for fast unique table growth: 1363148
1035</PRE>
1036See Section&nbsp;<A HREF="node4.html#sec:unique">4.5</A> and the comments above about reclaimed
1037nodes and hard limit for the cache size. This value was chosen
1038automatically 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>
1046Lowering these numbers will cause reordering to be less accurate and
1047faster. Results are somewhat unpredictable, because larger BDDs after one
1048reordering 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>
1057These lines tell whether automatic reordering can take place and
1058what method would be used. The mapping from numbers to methods is in
1059<TT>cudd.h</TT>. One may want to try different BDD
1060reordering methods. If variable groups are used, however, one should
1061not expect to see big differences, because CUDD uses the reported
1062method only to reorder each leaf variable group (typically corresponding
1063present and next state variables). For the relative order of the
1064groups, it always uses the same algorithm, which is effectively
1065sifting.
1066
1067<P>
1068As for enabling dynamic reordering or not, a sensible recommendation is the
1069following: Unless the circuit is rather small or one has a pretty good
1070idea 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>
1084Parameters for reordering. See the documentation of the functions used
1085to control these parameters for the details.
1086
1087<P>
1088<PRE>
1089 Next reordering threshold: 100000
1090</PRE>
1091When the number of nodes crosses this threshold, reordering will be
1092triggered. (If enabled; in this case it is not.) This parameter is
1093updated by the package whenever reordering takes place. The
1094application can change it, for instance at start-up. Another
1095possibility is to use a hook function (see Section&nbsp;<A HREF="node3.html#sec:hooks">3.16</A>) to
1096override the default updating policy.
1097
1098<P>
1099
1100<H3><A NAME="SECTION00048300000000000000"></A>
1101<A NAME="sec:extendedStats"></A>
1102<BR>
1103Extended Statistics and Reporting
1104</H3>
1105
1106<P>
1107The following symbols can be defined during compilation to increase
1108the amount of statistics gathered and the number of messages produced
1109by 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>
1121Defining DD_CACHE_PROFILE causes each entry of the cache to include
1122an access counter, which is used to compute simple statistics on the
1123distribution 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>
1130Guidelines for Documentation
1131</H2>
1132
1133<P>
1134The documentation of the CUDD functions is extracted automatically
1135from the sources by Stephen Edwards's extdoc. (The Ext system is
1136available 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>.)
1139The following guidelines are followed in CUDD to insure consistent and
1140effective use of automatic extraction. It is recommended that
1141extensions 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 &nbsp <B> <A NAME="tex2html312"
1201 HREF="node8.html">Index</A></B>
1202<!--End of Navigation Panel-->
1203<ADDRESS>
1204Fabio Somenzi
12052005-05-17
1206</ADDRESS>
1207</BODY>
1208</HTML>
Note: See TracBrowser for help on using the repository browser.