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> |
---|