cuddcheck.c

主要进行大规模的电路综合

  DdManager * table)
{
    int size;
    int i,j;
    DdNodePtr *nodelist;
    DdNode *node;
    DdNode *sentinel = &(table->sentinel);
    DdSubtable *subtable;
    int keys;
    int dead;
    int count = 0;
    int totalKeys = 0;
    int totalSlots = 0;
    int totalDead = 0;
    int nonEmpty = 0;
    unsigned int slots;
    int logSlots;
    int shift;

    size = table->size;

    for (i = 0; i < size; i++) {
	subtable = &(table->subtables[i]);
	nodelist = subtable->nodelist;
	keys = subtable->keys;
	dead = subtable->dead;
	totalKeys += keys;
	slots = subtable->slots;
	shift = subtable->shift;
	logSlots = sizeof(int) * 8 - shift;
	if (((slots >> logSlots) << logSlots) != slots) {
	    (void) fprintf(table->err,
			   "Unique table %d is not the right power of 2\n", i);
	    (void) fprintf(table->err,
			   "    slots = %u shift = %d\n", slots, shift);
	}
	totalSlots += slots;
	totalDead += dead;
	for (j = 0; (unsigned) j < slots; j++) {
	    node = nodelist[j];
	    if (node != sentinel) {
		nonEmpty++;
	    }
	    while (node != sentinel) {
		keys--;
		if (node->ref == 0) {
		    dead--;
		}
		node = node->next;
	    }
	}
	if (keys != 0) {
	    (void) fprintf(table->err, "Wrong number of keys found \
in unique table %d (difference=%d)\n", i, keys);
	    count++;
	}
	if (dead != 0) {
	    (void) fprintf(table->err, "Wrong number of dead found \
in unique table no. %d (difference=%d)\n", i, dead);
	}
    }	/* for each BDD/ADD subtable */

    /* Check the ZDD subtables. */
    size = table->sizeZ;

    for (i = 0; i < size; i++) {
	subtable = &(table->subtableZ[i]);
	nodelist = subtable->nodelist;
	keys = subtable->keys;
	dead = subtable->dead;
	totalKeys += keys;
	totalSlots += subtable->slots;
	totalDead += dead;
	for (j = 0; (unsigned) j < subtable->slots; j++) {
	    node = nodelist[j];
	    if (node != NULL) {
		nonEmpty++;
	    }
	    while (node != NULL) {
		keys--;
		if (node->ref == 0) {
		    dead--;
		}
		node = node->next;
	    }
	}
	if (keys != 0) {
	    (void) fprintf(table->err, "Wrong number of keys found \
in ZDD unique table no. %d (difference=%d)\n", i, keys);
	    count++;
	}
	if (dead != 0) {
	    (void) fprintf(table->err, "Wrong number of dead found \
in ZDD unique table no. %d (difference=%d)\n", i, dead);
	}
    }	/* for each ZDD subtable */

    /* Check the constant table. */
    subtable = &(table->constants);
    nodelist = subtable->nodelist;
    keys = subtable->keys;
    dead = subtable->dead;
    totalKeys += keys;
    totalSlots += subtable->slots;
    totalDead += dead;
    for (j = 0; (unsigned) j < subtable->slots; j++) {
	node = nodelist[j];
	if (node != NULL) {
	    nonEmpty++;
	}
	while (node != NULL) {
	    keys--;
	    if (node->ref == 0) {
		dead--;
	    }
	    node = node->next;
	}
    }
    if (keys != 0) {
	(void) fprintf(table->err, "Wrong number of keys found \
in the constant table (difference=%d)\n", keys);
	count++;
    }
    if (dead != 0) {
	(void) fprintf(table->err, "Wrong number of dead found \
in the constant table (difference=%d)\n", dead);
    }
    if ((unsigned) totalKeys != table->keys + table->keysZ) {
	(void) fprintf(table->err, "Wrong number of total keys found \
(difference=%d)\n", totalKeys-table->keys);
    }
    if ((unsigned) totalSlots != table->slots) {
	(void) fprintf(table->err, "Wrong number of total slots found \
(difference=%d)\n", totalSlots-table->slots);
    }
    if (table->minDead != (unsigned) (table->gcFrac * table->slots)) {
	(void) fprintf(table->err, "Wrong number of minimum dead found \
(%d vs. %d)\n", table->minDead,
	(unsigned) (table->gcFrac * (double) table->slots));
    }
    if ((unsigned) totalDead != table->dead + table->deadZ) {
	(void) fprintf(table->err, "Wrong number of total dead found \
(difference=%d)\n", totalDead-table->dead);
    }
    (void)printf("Average length of non-empty lists = %g\n",
    (double) table->keys / (double) nonEmpty);

    return(count);

} /* end of Cudd_CheckKeys */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Prints information about the heap.]

  Description [Prints to the manager's stdout the number of live nodes for each
  level of the DD heap that contains at least one live node.  It also
  prints a summary containing:
  <ul>
  <li> total number of tables;
  <li> number of tables with live nodes;
  <li> table with the largest number of live nodes;
  <li> number of nodes in that table.
  </ul>
  If more than one table contains the maximum number of live nodes,
  only the one of lowest index is reported. Returns 1 in case of success
  and 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
cuddHeapProfile(
  DdManager * dd)
{
    int ntables = dd->size;
    DdSubtable *subtables = dd->subtables;
    int i,		/* loop index */
	nodes,		/* live nodes in i-th layer */
	retval,		/* return value of fprintf */
	largest = -1,	/* index of the table with most live nodes */
	maxnodes = -1,	/* maximum number of live nodes in a table */
	nonempty = 0;	/* number of tables with live nodes */

    /* Print header. */
#if SIZEOF_VOID_P == 8
    retval = fprintf(dd->out,"*** DD heap profile for 0x%lx ***\n",
		     (unsigned long) dd);
#else
    retval = fprintf(dd->out,"*** DD heap profile for 0x%x ***\n",
		     (unsigned) dd);
#endif
    if (retval == EOF) return 0;

    /* Print number of live nodes for each nonempty table. */
    for (i=0; i<ntables; i++) {
	nodes = subtables[i].keys - subtables[i].dead;
	if (nodes) {
	    nonempty++;
	    retval = fprintf(dd->out,"%5d: %5d nodes\n", i, nodes);
	    if (retval == EOF) return 0;
	    if (nodes > maxnodes) {
		maxnodes = nodes;
		largest = i;
	    }
	}
    }

    nodes = dd->constants.keys - dd->constants.dead;
    if (nodes) {
	nonempty++;
	retval = fprintf(dd->out,"const: %5d nodes\n", nodes);
	if (retval == EOF) return 0;
	if (nodes > maxnodes) {
	    maxnodes = nodes;
	    largest = CUDD_CONST_INDEX;
	}
    }

    /* Print summary. */
    retval = fprintf(dd->out,"Summary: %d tables, %d non-empty, largest: %d ",
	  ntables+1, nonempty, largest);
    if (retval == EOF) return 0;
    retval = fprintf(dd->out,"(with %d nodes)\n", maxnodes);
    if (retval == EOF) return 0;

    return(1);

} /* end of cuddHeapProfile */


/**Function********************************************************************

  Synopsis    [Prints out information on a node.]

  Description [Prints out information on a node.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void
cuddPrintNode(
  DdNode * f,
  FILE *fp)
{
    f = Cudd_Regular(f);
#if SIZEOF_VOID_P == 8
    (void) fprintf(fp,"       node 0x%lx, id = %d, ref = %d, then = 0x%lx, else = 0x%lx\n",(unsigned long)f,f->index,f->ref,(unsigned long)cuddT(f),(unsigned long)cuddE(f));
#else
    (void) fprintf(fp,"       node 0x%x, id = %d, ref = %d, then = 0x%x, else = 0x%x\n",(unsigned)f,f->index,f->ref,(unsigned)cuddT(f),(unsigned)cuddE(f));
#endif

} /* end of cuddPrintNode */



/**Function********************************************************************

  Synopsis    [Prints the variable groups as a parenthesized list.]

  Description [Prints the variable groups as a parenthesized list.
  For each group the level range that it represents is printed. After
  each group, the group's flags are printed, preceded by a `|'.  For
  each flag (except MTR_TERMINAL) a character is printed.
  <ul>
  <li>F: MTR_FIXED
  <li>N: MTR_NEWNODE
  <li>S: MTR_SOFT
  </ul>
  The second argument, silent, if different from 0, causes
  Cudd_PrintVarGroups to only check the syntax of the group tree.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void
cuddPrintVarGroups(
  DdManager * dd /* manager */,
  MtrNode * root /* root of the group tree */,
  int zdd /* 0: BDD; 1: ZDD */,
  int silent /* flag to check tree syntax only */)
{
    MtrNode *node;
    int level;

    assert(root != NULL);
    assert(root->younger == NULL || root->younger->elder == root);
    assert(root->elder == NULL || root->elder->younger == root);
    if (zdd) {
	level = dd->permZ[root->index];
    } else {
	level = dd->perm[root->index];
    }
    if (!silent) (void) printf("(%d",level);
    if (MTR_TEST(root,MTR_TERMINAL) || root->child == NULL) {
	if (!silent) (void) printf(",");
    } else {
	node = root->child;
	while (node != NULL) {
	    assert(node->low >= root->low && (int) (node->low + node->size) <= (int) (root->low + root->size));
	    assert(node->parent == root);
	    cuddPrintVarGroups(dd,node,zdd,silent);
	    node = node->younger;
	}
    }
    if (!silent) {
	(void) printf("%d", level + root->size - 1);
	if (root->flags != MTR_DEFAULT) {
	    (void) printf("|");
	    if (MTR_TEST(root,MTR_FIXED)) (void) printf("F");
	    if (MTR_TEST(root,MTR_NEWNODE)) (void) printf("N");
	    if (MTR_TEST(root,MTR_SOFT)) (void) printf("S");
	}
	(void) printf(")");
	if (root->parent == NULL) (void) printf("\n");
    }
    assert((root->flags &~(MTR_TERMINAL | MTR_SOFT | MTR_FIXED | MTR_NEWNODE)) == 0);
    return;

} /* end of cuddPrintVarGroups */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Searches the subtables above node for its parents.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static void
debugFindParent(
  DdManager * table,
  DdNode * node)
{
    int         i,j;
    int		slots;
    DdNodePtr	*nodelist;
    DdNode	*f;
	
    for (i = 0; i < cuddI(table,node->index); i++) {
	nodelist = table->subtables[i].nodelist;
	slots = table->subtables[i].slots;

	for (j=0;j<slots;j++) {
	    f = nodelist[j];
	    while (f != NULL) {
		if (cuddT(f) == node || Cudd_Regular(cuddE(f)) == node) {
#if SIZEOF_VOID_P == 8
		    (void) fprintf(table->out,"parent is at 0x%lx, id = %d, ref = %d, then = 0x%lx, else = 0x%lx\n",
			(unsigned long)f,f->index,f->ref,(unsigned long)cuddT(f),(unsigned long)cuddE(f));
#else
		    (void) fprintf(table->out,"parent is at 0x%x, id = %d, ref = %d, then = 0x%x, else = 0x%x\n",
			(unsigned)f,f->index,f->ref,(unsigned)cuddT(f),(unsigned)cuddE(f));
#endif
		}
		f = f->next;
	    }
	}
    }

} /* end of debugFindParent */


#if 0
/**Function********************************************************************

  Synopsis    [Reports an error if a (dead) node has a non-dead parent.]

  Description [Searches all the subtables above node. Very expensive.
  The same check is now implemented more efficiently in ddDebugCheck.]

  SideEffects [None]

  SeeAlso     [debugFindParent]

******************************************************************************/
static void
debugCheckParent(
  DdManager * table,
  DdNode * node)
{
    int         i,j;
    int		slots;
    DdNode	**nodelist,*f;
    
    for (i = 0; i < cuddI(table,node->index); i++) {
	nodelist = table->subtables[i].nodelist;
	slots = table->subtables[i].slots;

	for (j=0;j<slots;j++) {
	    f = nodelist[j];
	    while (f != NULL) {
		if ((Cudd_Regular(cuddE(f)) == node || cuddT(f) == node) && f->ref != 0) {
		    (void) fprintf(table->err,
				   "error with zero ref count\n");
		    (void) fprintf(table->err,"parent is 0x%x, id = %d, ref = %d, then = 0x%x, else = 0x%x\n",f,f->index,f->ref,cuddT(f),cuddE(f));
		    (void) fprintf(table->err,"child  is 0x%x, id = %d, ref = %d, then = 0x%x, else = 0x%x\n",node,node->index,node->ref,cuddT(node),cuddE(node));
		}
		f = f->next;
	    }
	}
    }
}
#endif