next up previous index
Next: Guidelines for Documentation Up: Programmer's Manual Previous: Debugging

Gathering and Interpreting Statistics

  

Function Cudd_PrintInfo  can be called to print out the values of parameters and statistics for a manager. The output of Cudd_PrintInfo is divided in two sections. The first reports the values of parameters that are under the application control. The second reports the values of statistical counters and other non-modifiable parameters. A quick guide to the interpretation of all these quantities follows. For ease of exposition, we reverse the order and describe the non-modifiable parameters first. We'll use a sample run as example. There is nothing special about this run.

Non Modifiable Parameters

 

The list of non-modifiable parameters starts with:

    **** CUDD non-modifiable parameters ****
    Memory in use: 36282948
This is the memory used by CUDD for three things mainly: Unique table (including all DD nodes in use), node free list, and computed table. This number almost never decreases in the lifetime of a CUDD manager, because CUDD does not release memory when it frees nodes. Rather, it puts the nodes on its own free list. This number is in bytes. It does not represent the peak memory occupation, because it does not include the size of data structures created temporarily by some functions (e.g., local look-up tables).

    Peak number of nodes: 837018
This number is the number of nodes that the manager has allocated. This is not the largest size of the BDDs, because the manager will normally have some dead nodes and some nodes on the free list.

    Number of BDD variables: 198
    Number of ZDD variables: 0
These numbers tell us this run was not using ZDDs.

    Number of cache entries: 1048576
Current number of slots of the computed table. If one has a performance problem, this is one of the numbers to look at. The cache size is always a power of 2.

    Number of cache look-ups: 5357600
    Number of cache hits: 3761921
These numbers give an indication of the hit rate in the computed table. It is not unlikely for model checking runs to get very high hit rates like this one (69.95%).

    Number of cache insertions: 1595768
    Number of cache collisions: 859151
    Number of cache deletions: 0
A collision  occurs when a cache entry is overwritten. A deletion  occurs when a cache entry is invalidated (e.g., during garbage collection). If the number of deletions is high compared to the number of collisions, it means that garbage collection occurs too often. In this case there were no garbage collections; hence, no deletions.

    Cache used slots = 70.25%
Percentage of cache slots that do not contain a valid entry. If this number is small, it may signal one of three conditions:
  1. The cache may have been recently resized and it is still filling up.
  2. The cache is too large for the BDDs. This should not happen if the size of the cache is determined by CUDD.
  3. The hash function is not working properly. This is accompanied by a degradation in performance. Conversely, a degradation in performance may be due to bad hash function behavior if the number of unused cache slots is large.

    Soft limit for cache size: 956416
This number says how large the cache can grow. This limit is based on the size of the unique table and is to be interpreted as the largest size for which a resizing is still possible. Hence, as in our case, the cache can exceed this limit, but by less than a factor of 2. CUDD uses a reward-based policy for growing the cache. (See Section 4.4.1.) The default hit rate for resizing is 30% and the value in effect is reported among the modifiable parameters.

    Number of buckets in unique table: 478208
This number is exactly half the one above. This is indeed how the soft limit is determined currently, unless the computed table hits the specified hard limit. (See below.)

    Used buckets in unique table: 77.86%
Percentage of unique table buckets that contain at least one node. Remarks analogous to those made about the used cache slots apply.

    Number of BDD and ADD nodes: 836894
    Number of ZDD nodes: 0
How many nodes are currently in the unique table, either alive or dead.

    Number of dead BDD and ADD nodes: 836496
    Number of dead ZDD nodes: 0
Subtract these numbers from those above to get the number of live nodes.

    Total number of nodes allocated: 836894
This is the total number of nodes that were requested and obtained from the free list. It never decreases, and is not an indication of memory occupation after the first garbage collection. Rather, it is a measure of the package activity.

    Total number of nodes reclaimed: 18499505
These are the nodes that were resuscitated from the dead. If they are many more than the allocated nodes, and the total number of slots is low relative to the number of nodes, then one may want to increase the limit for fast unique table growth.

    Garbage collections so far: 0
    Time for garbage collections: 0.00 sec
    Reorderings so far: 0
    Time for reordering: 0.00 sec
There is a GC for each reordering. Hence the first count will always be at least as large as the second.

    Next reordering threshold: 4004
When the number of nodes crosses this threshold, reordering will be triggered. (If enabled; in this case it is not.)

Modifiable Parameters

 

Let us now consider the modifiable parameters, that is, those settings on which the application or the user has control.

    **** CUDD modifiable parameters ****
    Hard limit for cache size: 13421772
This number counts entries. Each entry is 20 bytes if CUDD is compiled to use 32-bit pointers. Two important observations are in order:
  1. If the datasize limit is set, CUDD will use it to determine this number automatically. On a Unix system, one can type ``limit" to verify if this value is set. If the datasize limit is not set, CUDD uses a default which is rather small. If you have enough memory (say 64MB or more) you should seriously consider not using the default. So, either set the datasize limit, or override the default with Cudd_SetMaxCacheHard .
  2. If a process seems to be going nowhere, a small value for this parameter may be the culprit. One cannot overemphasize the importance of the computed table in BDD algorithms.
In this case the limit was set automatically for a target maximum memory occupation of 1 GB.

    Cache hit threshold for resizing: 15%
This number can be changed if one suspects performance is hindered by the small size of the cache, and the cache is not growing towards the soft limit sufficiently fast. In such a case one can change the default 30% to 15% (as in this case) or even 1%.

    Garbage collection enabled: yes
One can disable it, but there are few good reasons for doing so. It is normally preferable to raise the limit for fast unique table growth. (See below.)

    Limit for fast unique table growth: 8388608
See Section 4.5 and the comments above about reclaimed nodes and hard limit for the cache size. This value was chosen automatically by CUDD for a datasize limit of 1 GB.

    Maximum number of variables sifted per reordering: 1000
    Maximum number of variable swaps per reordering: 2000000
    Maximum growth while sifting a variable: 1.2
Lowering these numbers will cause reordering to be less accurate and faster. Results are somewhat unpredictable, because larger BDDs after one reordering do not necessarily mean the process will go faster or slower.

    Dynamic reordering of BDDs enabled: yes
    Default BDD reordering method: 4
    Dynamic reordering of ZDDs enabled: no
    Default ZDD reordering method: 4
These lines tell whether automatic reordering can take place and what method would be used. The mapping from numbers to methods is in cudd.h. One may want to try different BDD reordering methods. If variable groups are used, however, one should not expect to see big differences, because CUDD uses the reported method only to reorder each leaf variable group (typically corresponding present and next state variables). For the relative order of the groups, it always uses the same algorithm, which is effectively sifting.

As for enabling dynamic reordering or not, a sensible recommendation is the following: Unless the circuit is rather small or one has a pretty good idea of what the order should be, reordering should be enabled.

    Realignment of ZDDs to BDDs enabled: no
    Realignment of BDDs to ZDDs enabled: no
    Dead nodes counted in triggering reordering: no
    Group checking criterion: 7
    Recombination threshold: 0
    Symmetry violation threshold: 0
    Arc violation threshold: 0
    GA population size: 0
    Number of crossovers for GA: 0
Parameters for reordering. See the documentation of the functions used to control these parameters for the details.

Extended Statistics and Reporting

 

The following symbols can be defined during compilation to increase the amount of statistics gathered and the number of messages produced by the package:

Defining DD_CACHE_PROFILE causes each entry of the cache to include an access counter, which is used to compute simple statistics on the distribution of the keys.


next up previous index
Next: Guidelines for Documentation Up: Programmer's Manual Previous: Debugging

Fabio Somenzi
Tue May 12 18:47:58 MDT 1998