| blob | d7a60ba0c6d366195783fd836ae9a4ea95d18bf8 |
3 <!--Converted with jLaTeX2HTML 2002-2-1 (1.70) JA patch-2.0
4 patched version by: Kenshi Muto, Debian Project.
5 * modified by: Shige TAKENO
6 LaTeX2HTML 2002-2-1 (1.70),
7 original version by: Nikos Drakos, CBLU, University of Leeds
8 * revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
9 * with significant contributions from:
10 Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
11 <HTML>
12 <HEAD>
28 </HEAD>
30 <BODY >
31 <!--Navigation Panel-->
48 <BR>
57 <BR>
58 <BR>
59 <!--End of Navigation Panel-->
60 <!--Table of Child-Links-->
63 <UL>
68 <UL>
72 HREF="node4.html#SECTION00042200000000000000"><I>Cudd_RecursiveDeref</I> vs. <I>Cudd_Deref</I></A>
74 HREF="node4.html#SECTION00042300000000000000">When Increasing the Reference Count is Unnecessary</A>
77 </UL>
78 <BR>
83 <UL>
88 </UL>
89 <BR>
98 <UL>
105 </UL>
106 <BR>
109 </UL>
110 <!--End of Table of Child-Links-->
111 <HR>
115 <BR>
116 Programmer's Manual
117 </H1>
119 <P>
120 This section provides additional detail on the working of the CUDD
121 package and on the programming conventions followed in its writing.
122 The additional detail should help those who want to write procedures
123 that directly manipulate the CUDD data structures.
125 <P>
129 <BR>
130 Compiling and Linking
131 </H2>
133 <P>
135 (for instance, you want to write a procedure that traverses a decision
136 diagram) you need to add
137 <PRE>
138 #include "cuddInt.h"
139 </PRE>
141 your executable. Some platforms require specific compiler and linker
143 the distribution.
145 <P>
149 <BR>
150 Reference Counts
151 </H2>
153 <P>
155 based on reference counts. Each node stores the sum of the external
156 references and internal references. An internal BDD or ADD node is
158 internal ZDD node is created by a call to
162 these functions is new, its reference count is zero. The function
166 increasing the reference count of the node. This is accomplished by
169 <P>
170 When a function is no longer needed by an application, the memory used
171 by its diagram can be recycled by calling
174 (ZDDs). These functions decrease the reference <A NAME="724"></A> count of the node passed to them. If the reference count
175 becomes 0, then two things happen:
177 <OL>
181 node belongs, and one global counter for the
183 node itself is not affected.
184 </LI>
185 <LI>The function is recursively called on the two children of the
186 node.
187 </LI>
188 </OL>
189 For instance, if the diagram of a function does not share any nodes
190 with other diagrams, then calling
193 root will cause all the nodes of the diagram to become dead.
195 <P>
196 When the number of dead nodes reaches a given level (dynamically
197 determined by the package) garbage collection takes place. During
201 <P>
202 When a new node is created, it is important to increase its
204 following events occurs:
206 <OL>
210 function that may eventually cause a call to them.
211 </LI>
212 <LI>A call to
215 a function that may eventually cause a call to them.
216 </LI>
217 </OL>
218 In practice, it is recommended to increase the reference count as soon
219 as the returned pointer has been tested for not being NULL.
221 <P>
225 <BR>
226 NULL Return Values
227 </H3>
229 <P>
230 The interface to the memory management functions (e.g., malloc) used
231 by CUDD intercepts NULL return values and calls a handler. The
232 default handler exits with an error message. If the application does
233 not install another handler, therefore, a NULL return value from an
234 exported function of CUDD signals an internal error.
236 <P>
237 If the aplication, however, installs another handler that lets
238 execution continue, a NULL pointer returned by an exported function
239 typically indicates that the process has run out of memory.
241 ascertain the nature of the problem.
243 <P>
244 An application that tests for the result being NULL can try some
245 remedial action, if it runs out of memory. For instance, it may free
246 some memory that is not strictly necessary, or try a slower algorithm
247 that takes less space. As an example, CUDD overrides the default
248 handler when trying to enlarge the cache or increase the number of
249 slots of the unique table. If the allocation fails, the package prints
250 out a message and continues without resizing the cache.
252 <P>
256 <BR>
258 </H3>
260 <P>
261 It is often the case that a recursive procedure has to protect the
262 result it is going to return, while it disposes of intermediate
263 results. (See the previous discussion on when to increase reference
264 counts.) Once the intermediate results have been properly disposed
265 of, the final result must be returned to its pristine state, in which
266 the root node may have a reference count of 0. One cannot use
269 erroneously make some nodes dead. Therefore, the package provides a
271 function is not recursive, and does not change the dead node counts.
272 Its use is almost exclusively the one just described: Decreasing the
273 reference count of the root of the final result before returning from
274 a recursive procedure.
276 <P>
280 <BR>
281 When Increasing the Reference Count is Unnecessary
282 </H3>
284 <P>
286 simple BDD variable is needed for comparison purposes, then calling
288 simple functions are guaranteed to have reference counts greater than
290 attempt to free the diagram by calling
293 made.
295 <P>
299 <BR>
300 Saturating Increments and Decrements
301 </H3>
303 <P>
304 On 32-bit machines, the CUDD package stores the
306 For large diagrams, it is possible for some reference counts to exceed
307 the capacity of an unsigned short int. Therefore, increments and
309 once a reference count has reached the maximum possible value, it is
314 that have no references may not be declared dead. This may result in a
315 small waste of memory, which is normally more than offset by the
316 reduction in size of the node structure.
318 <P>
319 When using 64-bit pointers, there is normally no memory advantage from
320 using short int's instead of int's in a DdNode. Therefore, increments
321 and decrements are not saturating in that case. What option is in
325 increments and decrements of the reference counts are performed using
331 <P>
335 <BR>
336 Complement Arcs
337 </H2>
339 <P>
341 like BDDs without complement arcs. It is normally easier to write code
343 complementation is trivial with complement arcs, and is not trivial
344 without. As a consequence, with complement arcs it is possible to
345 check for more terminal cases and it is possible to apply De Morgan's
346 laws to reduce problems that are essentially identical to a standard
349 <P>
350 The complement attribute is stored in the least significant bit of the
351 ``else'' pointer of each node. An external pointer to a function can
352 also be complemented. The ``then'' pointer to a node, on the other
355 memory. Instead, it is always necessary to obtain a regular version
356 of it. This is normally done by calling
359 ``then'' child as argument. The calling procedure must apply De
360 Morgan's laws by complementing both pointers passed to
362 complement of the result.
364 <P>
368 <BR>
369 The Cache
370 </H2>
372 <P>
373 Each entry of the cache consists of five fields: The operator, three
374 pointers to operands and a pointer to the result. The operator and the
375 three pointers to the operands are combined to form three words. The
376 combination relies on two facts:
378 <UL>
379 <LI>Most operations have one or two operands. A few bits are
380 sufficient to discriminate all three-operands operations.
381 </LI>
383 if 64-bit pointers are used.) Hence, there are a few bits available
384 to distinguish the three-operand operations from te others and to
385 assign unique codes to them.
386 </LI>
387 </UL>
389 <P>
390 The cache does not contribute to the reference
392 counts of the nodes. The fact that the cache contains a
393 pointer to a node does not imply that the node is alive. Instead, when
397 <P>
398 The cache is also cleared (of all entries) when dynamic
400 removed from the cache are about to become invalid.
402 <P>
403 All operands and results in a cache entry must be pointers to
405 or uses more than three arguments, there are currently two solutions:
407 <UL>
410 </LI>
411 <LI>Combine multiple results, or multiple operands, into a single
412 diagram, by building a ``multiplexing structure'' with reserved
413 variables.
414 </LI>
415 </UL>
416 Support of the former solution is under development. (See
418 provided in future versions of the package.
420 <P>
422 the cache. The first set is for functions with three operands:
425 functions with two operands:
428 functions with one operand:
431 slightly faster than the first, and the third set is slightly faster
432 than the second.
434 <P>
438 <BR>
439 Cache Sizing
440 </H3>
442 <P>
443 The size of the cache can increase during the execution of an
444 application. (There is currently no way to decrease the size of the
445 cache, though it would not be difficult to do it.) When a cache miss
446 occurs, the package uses the following criteria to decide whether to
447 resize the cache:
449 <OL>
450 <LI>If the cache already exceeds the limit given by the
452 takes place. The limit is the minimum of two values: a value set at
453 initialization time and possibly modified by the application, which
454 constitutes the hard limit beyond which the cache will never grow;
455 and a number that depends on the current total number of slots in
457 </LI>
458 <LI>If the cache is not too large already, resizing is decided based
459 on the hit rate. The policy adopted by the CUDD package is
461 rate is high, then it is worthwhile to increase the size of the
462 cache.
463 </LI>
464 </OL>
465 When resizing takes place, the statistical counters <A NAME="846"></A> used to compute the hit rate are reinitialized so as to
466 prevent immediate resizing. The number of entries is doubled.
468 <P>
470 policy is as follows. In many BDD/ADD applications the hit rate is
471 not very sensitive to the size of the cache: It is primarily a
472 function of the problem instance at hand. If a large hit rate is
473 observed, chances are that by using a large cache, the results of
474 large problems (those that would take longer to solve) will survive in
475 the cache without being overwritten long enough to cause a valuable
476 cache hit. Notice that when a large problem is solved more than once,
477 so are its recursively generated subproblems. If the hit rate is
478 low, the probability of large problems being solved more than once is
479 low.
481 <P>
482 The other observation about the cache sizing policy is that there is
483 little point in keeping a cache which is much larger than the unique
484 table. Every time the unique table ``fills up,'' garbage collection is
485 invoked and the cache is cleared of all dead entries. A cache that is
487 less than fully utilized.
489 <P>
493 <BR>
494 Local Caches
495 </H3>
497 <P>
498 Sometimes it may be necessary or convenient to use a local cache. A
500 overwritten), or it may store objects for which
502 important fact to keep in mind when using a local cache is that local
504 collection or before reordering. Therefore, it is necessary to
506 pointed by a local cache. (Unless their reference counts are
507 guaranteed positive in some other way. One such way is by including
508 all partial results in the global result.) Before disposing of the
509 local cache, all elements stored in it must be passed to
511 of the fact that all results in a local cache are referenced, it is
512 generally convenient to store in the local cache also the result of
513 trivial problems, which are not usually stored in the global cache.
514 Otherwise, after a recursive call, it is difficult to tell whether the
515 result is in the cache, and therefore referenced, or not in the cache,
516 and therefore not referenced.
518 <P>
519 An alternative approach to referencing the results in the local caches
521 executed before garbage collection.
523 <P>
527 <BR>
528 The Unique Table
529 </H2>
531 <P>
532 A recursive procedure typically splits the operands by expanding with
533 respect to the topmost variable. Topmost in this context refers to the
534 variable that is closest to the roots in the current variable order.
535 The nodes, on the other hand, hold the index, which is invariant with
536 reordering. Therefore, when splitting, one must use the
538 package to get the right level. Access to the permutation array is
542 <P>
544 there are variables in use. These has tables are called <I>unique
545 subtables</I>. The sizes of the unique subtables are determined by two
546 criteria:
548 <OL>
550 to keep access time down.
551 </LI>
554 </LI>
555 </OL>
556 While the first criterion is fairly straightforward to implement, the
557 second leaves more room to creativity. The CUDD package tries to
558 figure out whether more dead node should be allowed to increase
560 reasons for not doing garbage collection too often. The obvious one is
561 that it is expensive. The second is that dead nodes may be
563 successful cache lookup. Hence dead nodes may provide a substantial
564 speed-up if they are kept around long enough. The usefulness of
565 keeping many dead nodes around varies from application to application,
566 and from problem instance to problem instance. As in the sizing of the
567 cache, the CUDD package adopts a
569 decide how much room should be used for the unique table. If the
570 number of dead nodes reclaimed is large compared to the number of
571 nodes directly requested from the memory manager, then the CUDD
572 package assumes that it will be beneficial to allow more room for the
573 subtables, thereby reducing the frequency of garbage collection. The
574 package does so by switching between two modes of operation:
576 <OL>
578 ratio of dead nodes to total nodes required for garbage collection
579 is higher than in the slow growth mode to favor resizing
580 of the subtables.
581 </LI>
583 mode keeping many dead nodes around is not as important as
584 keeping memory requirements low.
585 </LI>
586 </OL>
587 Switching from one mode to the other is based on the following
588 criteria:
590 <OL>
591 <LI>If the unique table is already large, only slow growth is
592 possible.
593 </LI>
594 <LI>If the table is small and many dead nodes are being reclaimed,
595 then fast growth is selected.
596 </LI>
597 </OL>
598 This policy is especially effective when the diagrams being
599 manipulated have lots of recombination. Notice the interplay of the
600 cache sizing and unique sizing: Fast growth normally occurs when the
601 cache hit rate is large. The cache and the unique table then grow in
602 concert, preserving a healthy balance between their sizes.
604 <P>
608 <BR>
609 Allowing Asynchronous Reordering
610 </H2>
612 <P>
613 Asynchronous reordering is the reordering that is triggered
614 automatically by the increase of the number of nodes. Asynchronous
615 reordering takes place when a new internal node must be created, and
616 the number of nodes has reached a given
618 the package every time reordering takes place.)
620 <P>
621 Those procedures that do not create new nodes (e.g., procedures that
623 not worry about asynchronous reordering: No special precaution is
624 necessary in writing them.
626 <P>
627 Procedures that only manipulate decision diagrams through the exported
628 functions of the CUDD package also need not concern themselves with
630 exceptions.)
632 <P>
633 The remaining class of procedures is composed of functions that visit
634 the diagrams and may create new nodes. All such procedures in the CUDD
635 package are written so that they can be interrupted by dynamic
636 reordering. The general approach followed goes under the name of
638 implies, a computation that is interrupted by dynamic reordering is
639 aborted and tried again.
641 <P>
642 A recursive procedure that can be interrupted by dynamic reordering
644 from now on) is composed of two functions. One is responsible for the
645 real computation. The other is a simple
647 reordering occurred and restarts the computation if it did.
649 <P>
650 Asynchronous reordering of BDDs and ADDs can only be triggered inside
652 to be created. Likewise, asynchronous reordering of ZDDs can only be
654 When reordering is triggered, three things happen:
656 <OL>
658 value;
659 </LI>
661 no reordering, while 2 indicates an error occurred during
662 reordering.)
663 </LI>
665 The counter is initialized to 0 when the manager is started and can
666 be accessed by calling
668 two readings of the counter, an application can determine if
669 variable reordering has taken place between the first and the second
670 reading. The package itself, however, does not make use of the
671 counter: It is mentioned here for completeness.
672 </LI>
673 </OL>
675 <P>
676 The recursive procedure that receives a NULL value from
678 intermediate results that it may have computed before, and return NULL
679 in its turn.
681 <P>
683 decide whether reordering occurred based on the NULL return value,
684 because the NULL value may be the result of lack of memory. Instead,
687 <P>
688 When a recursive procedure calls another recursive procedure that may
689 cause reordering, it should bypass the wrapper and call the recursive
690 procedure directly. Otherwise, the calling procedure will not know
691 whether reordering occurred, and will not be able to restart. This is
692 the main reason why most recursive procedures are internal, rather
693 than static. (The wrappers, on the other hand, are mostly exported.)
695 <P>
699 <BR>
700 Debugging
701 </H2>
703 <P>
705 numerous checks are added to the code. In addition, the procedures
709 point to verify the consistency of the data structure.
713 useful when CUDD reports that during garbage collection the number of
714 nodes actually deleted from the unique table is different from the
715 count of dead nodes kept by the manager. The error causing the
716 discrepancy may have occurred much earlier than it is discovered. A
717 few strategicaly placed calls to the debugging procedures can
718 considerably narrow down the search for the source of the problem.
722 <P>
723 One of the most common problems encountered in debugging code based on
724 the CUDD package is a missing call to
726 identify this type of problems, the package provides a function called
728 should be called immediately before shutting down the manager.
732 functions, and nodes whose reference counts are
735 <P>
736 For this function to be effective the application must explicitly
737 dispose of all diagrams to which it has pointers before calling it.
739 <P>
743 <BR>
744 Gathering and Interpreting Statistics
745 </H2>
747 <P>
749 print out the values of parameters and statistics for a manager. The
751 first reports the values of parameters that are under the application
752 control. The second reports the values of statistical counters and
753 other non-modifiable parameters. A quick guide to the interpretation
754 of all these quantities follows. For ease of exposition, we reverse
755 the order and describe the non-modifiable parameters first. We'll use
756 a sample run as example. There is nothing special about this run.
758 <P>
762 <BR>
763 Non Modifiable Parameters
764 </H3>
766 <P>
767 The list of non-modifiable parameters starts with:
768 <PRE>
769 **** CUDD non-modifiable parameters ****
770 Memory in use: 32544220
771 </PRE>
772 This is the memory used by CUDD for three things mainly: Unique table
773 (including all DD nodes in use), node free list, and computed table.
774 This number almost never decreases in the lifetime of a CUDD manager,
775 because CUDD does not release memory when it frees nodes. Rather, it
776 puts the nodes on its own free list. This number is in bytes. It does
777 not represent the peak memory occupation, because it does not include
778 the size of data structures created temporarily by some functions (e.g.,
779 local look-up tables).
781 <P>
782 <PRE>
783 Peak number of nodes: 837018
784 </PRE>
785 This number is the number of nodes that the manager has allocated.
786 This is not the largest size of the BDDs, because the manager will
787 normally have some dead nodes and some nodes on the free list.
789 <P>
790 <PRE>
791 Peak number of live nodes: 836894
792 </PRE>
793 This is the largest number of live nodes that the manager has held
794 since its creation.
796 <P>
797 <PRE>
798 Number of BDD variables: 198
799 Number of ZDD variables: 0
800 </PRE>
801 These numbers tell us this run was not using ZDDs.
803 <P>
804 <PRE>
805 Number of cache entries: 1048576
806 </PRE>
807 Current number of slots of the computed table. If one has a
808 performance problem, this is one of the numbers to look at. The cache
809 size is always a power of 2.
811 <P>
812 <PRE>
813 Number of cache look-ups: 2996536
814 Number of cache hits: 1187087
815 </PRE>
816 These numbers give an indication of the hit rate in the computed
817 table. It is not unlikely for model checking runs to get
818 hit rates even higher than this one (39.62%).
820 <P>
821 <PRE>
822 Number of cache insertions: 1809473
823 Number of cache collisions: 961208
824 Number of cache deletions: 0
825 </PRE>
828 occurs when a cache entry is invalidated (e.g., during garbage
829 collection). If the number of deletions is high compared to the
830 number of collisions, it means that garbage collection occurs too
831 often. In this case there were no garbage collections; hence, no
832 deletions.
834 <P>
835 <PRE>
837 </PRE>
838 Percentage of cache slots that contain a valid entry. If this
839 number is small, it may signal one of three conditions:
841 <OL>
842 <LI>The cache may have been recently resized and it is still filling
843 up.
844 </LI>
845 <LI>The cache is too large for the BDDs. This should not happen if
846 the size of the cache is determined by CUDD.
847 </LI>
848 <LI>The hash function is not working properly. This is accompanied
849 by a degradation in performance. Conversely, a degradation in
850 performance may be due to bad hash function behavior.
851 </LI>
852 </OL>
853 The expected value is computed assuming a uniformly random
854 distribution of the accesses. If the difference between the measured
855 value and the expected value is large (unlike this case), the cache is
856 not working properly.
858 <P>
859 <PRE>
860 Soft limit for cache size: 1318912
861 </PRE>
862 This number says how large the cache can grow. This limit is based on
863 the size of the unique table. CUDD uses a reward-based policy for
865 hit rate for resizing is 30% and the value in effect is reported
866 among the modifiable parameters.
868 <P>
869 <PRE>
870 Number of buckets in unique table: 329728
871 </PRE>
872 This number is exactly one quarter of the one above. This is indeed
873 how the soft limit is determined currently, unless the computed table
874 hits the specified hard limit. (See below.)
876 <P>
877 <PRE>
879 </PRE>
880 Percentage of unique table buckets that contain at least one
881 node. Remarks analogous to those made about the used cache slots apply.
883 <P>
884 <PRE>
885 Number of BDD and ADD nodes: 836894
886 Number of ZDD nodes: 0
887 </PRE>
888 How many nodes are currently in the unique table, either alive or dead.
890 <P>
891 <PRE>
892 Number of dead BDD and ADD nodes: 0
893 Number of dead ZDD nodes: 0
894 </PRE>
895 Subtract these numbers from those above to get the number of live
896 nodes. In this case there are no dead nodes because the application
897 uses delayed dereferencing
900 <P>
901 <PRE>
902 Total number of nodes allocated: 836894
903 </PRE>
904 This is the total number of nodes that were requested and obtained
905 from the free list. It never decreases, and is not an indication of
906 memory occupation after the first garbage collection. Rather, it is a
907 measure of the package activity.
909 <P>
910 <PRE>
911 Total number of nodes reclaimed: 0
912 </PRE>
913 These are the nodes that were resuscitated from the dead. If they are
914 many more than the allocated nodes, and the total
915 number of slots is low relative to the number of nodes, then one may
916 want to increase the limit for fast unique table growth. In this case,
917 the number is 0 because of delayed dereferencing.
919 <P>
920 <PRE>
921 Garbage collections so far: 0
922 Time for garbage collections: 0.00 sec
923 Reorderings so far: 0
924 Time for reordering: 0.00 sec
925 </PRE>
926 There is a GC for each reordering. Hence the first count will always be
927 at least as large as the second.
929 <P>
930 <PRE>
931 Node swaps in reordering: 0
932 </PRE>
933 This is the number of elementary reordering steps. Each step consists
934 of the re-expression of one node while swapping two adjacent
935 variables. This number is a good measure of the amount of work done in
936 reordering.
938 <P>
942 <BR>
943 Modifiable Parameters
944 </H3>
946 <P>
947 Let us now consider the modifiable parameters, that is, those settings on
948 which the application or the user has control.
950 <P>
951 <PRE>
952 **** CUDD modifiable parameters ****
953 Hard limit for cache size: 8388608
954 </PRE>
955 This number counts entries. Each entry is 16 bytes if CUDD is compiled
956 to use 32-bit pointers. Two important observations are in order:
958 <OL>
959 <LI>If the datasize limit is set, CUDD will use it to determine this
960 number automatically. On a Unix system, one can type ``limit'' or
961 ``ulimit'' to verify if this value is set. If the datasize limit is
962 not set, CUDD uses a default which is rather small. If you have
963 enough memory (say 64MB or more) you should seriously consider
965 override the default with
967 </LI>
968 <LI>If a process seems to be going nowhere, a small value for
969 this parameter may be the culprit. One cannot overemphasize the
970 importance of the computed table in BDD algorithms.
971 </LI>
972 </OL>
973 In this case the limit was automatically set for a target maximum
974 memory occupation of 104 MB.
976 <P>
977 <PRE>
978 Cache hit threshold for resizing: 15%
979 </PRE>
980 This number can be changed if one suspects performance is hindered by
981 the small size of the cache, and the cache is not growing towards the
982 soft limit sufficiently fast. In such a case one can change the
985 <P>
986 <PRE>
987 Garbage collection enabled: yes
988 </PRE>
989 One can disable it, but there are few good reasons for doing
990 so. It is normally preferable to raise the limit for fast unique table
991 growth. (See below.)
993 <P>
994 <PRE>
995 Limit for fast unique table growth: 1363148
996 </PRE>
998 nodes and hard limit for the cache size. This value was chosen
999 automatically by CUDD for a datasize limit of 1 GB.
1001 <P>
1002 <PRE>
1003 Maximum number of variables sifted per reordering: 1000
1004 Maximum number of variable swaps per reordering: 2000000
1005 Maximum growth while sifting a variable: 1.2
1006 </PRE>
1007 Lowering these numbers will cause reordering to be less accurate and
1008 faster. Results are somewhat unpredictable, because larger BDDs after one
1009 reordering do not necessarily mean the process will go faster or slower.
1011 <P>
1012 <PRE>
1013 Dynamic reordering of BDDs enabled: yes
1014 Default BDD reordering method: 4
1015 Dynamic reordering of ZDDs enabled: no
1016 Default ZDD reordering method: 4
1017 </PRE>
1018 These lines tell whether automatic reordering can take place and what
1019 method would be used. The mapping from numbers to methods is in
1021 methods. If variable groups are used, however, one should not expect
1022 to see big differences, because CUDD uses the reported method only to
1023 reorder each leaf variable group (typically corresponding present and
1024 next state variables). For the relative order of the groups, it
1025 always uses the same algorithm, which is effectively sifting.
1027 <P>
1028 As for enabling dynamic reordering or not, a sensible recommendation is the
1029 following: Unless the circuit is rather small or one has a pretty good
1030 idea of what the order should be, reordering should be enabled.
1032 <P>
1033 <PRE>
1034 Realignment of ZDDs to BDDs enabled: no
1035 Realignment of BDDs to ZDDs enabled: no
1036 Dead nodes counted in triggering reordering: no
1037 Group checking criterion: 7
1038 Recombination threshold: 0
1039 Symmetry violation threshold: 0
1040 Arc violation threshold: 0
1041 GA population size: 0
1042 Number of crossovers for GA: 0
1043 </PRE>
1044 Parameters for reordering. See the documentation of the functions used
1045 to control these parameters for the details.
1047 <P>
1048 <PRE>
1049 Next reordering threshold: 100000
1050 </PRE>
1051 When the number of nodes crosses this threshold, reordering will be
1052 triggered. (If enabled; in this case it is not.) This parameter is
1053 updated by the package whenever reordering takes place. The
1054 application can change it, for instance at start-up. Another
1055 possibility is to use a hook function (see Section <A HREF="node3.html#sec:hooks">3.16</A>) to
1056 override the default updating policy.
1058 <P>
1062 <BR>
1063 Extended Statistics and Reporting
1064 </H3>
1066 <P>
1067 The following symbols can be defined during compilation to increase
1068 the amount of statistics gathered and the number of messages produced
1069 by the package:
1071 <UL>
1073 </LI>
1075 </LI>
1077 </LI>
1079 </LI>
1080 </UL>
1081 Defining DD_CACHE_PROFILE causes each entry of the cache to include
1082 an access counter, which is used to compute simple statistics on the
1083 distribution of the keys.
1085 <P>
1089 <BR>
1090 Guidelines for Documentation
1091 </H2>
1093 <P>
1094 The documentation of the CUDD functions is extracted automatically
1095 from the sources by Stephen Edwards's extdoc. (The Ext system is
1099 The following guidelines are followed in CUDD to insure consistent and
1100 effective use of automatic extraction. It is recommended that
1101 extensions to CUDD follow the same documentation guidelines.
1103 <UL>
1104 <LI>The documentation of an exported procedure should be sufficient
1105 to allow one to use it without reading the code. It is not necessary
1106 to explain how the procedure works; only what it does.
1107 </LI>
1109 fields should be space-separated lists of function names. The
1112 procedure may reference other internal procedures as well as
1113 exported procedures, but no static procedures.
1114 </LI>
1115 <LI>The return values are detailed in the
1117 field, not in the
1119 </LI>
1120 <LI>The parameters are documented alongside their declarations.
1122 </LI>
1124 normal case for an exported procedure--then the synopsis is
1125 repeated--possibly slightly changed--at the beginning of the
1128 the description.
1129 </LI>
1131 </LI>
1132 </UL>
1134 <P>
1135 <HR>
1136 <!--Navigation Panel-->
1153 <BR>
1162 <!--End of Navigation Panel-->
1163 <ADDRESS>
1164 Fabio Somenzi
1166 </ADDRESS>
1167 </BODY>
1168 </HTML>