cuddcheck.c

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

/**CFile***********************************************************************

  FileName    [cuddCheck.c]

  PackageName [cudd]

  Synopsis    [Functions to check consistency of data structures.]

  Description [External procedures included in this module:
		<ul>
		<li> Cudd_DebugCheck()
		<li> Cudd_CheckKeys()
		</ul>
	       Internal procedures included in this module:
		<ul>
		<li> cuddHeapProfile()
		<li> cuddPrintNode()
		<li> cuddPrintVarGroups()
		</ul>
	       Static procedures included in this module:
		<ul>
		<li> debugFindParent()
		</ul>
		]

  SeeAlso     []

  Author      [Fabio Somenzi]

  Copyright [This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

******************************************************************************/

#include "util.h"
#include "cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddCheck.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static void debugFindParent ARGS((DdManager *table, DdNode *node));
#if 0
static void debugCheckParent ARGS((DdManager *table, DdNode *node));
#endif

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


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

  Synopsis    [Checks for inconsistencies in the DD heap.]

  Description [Checks for inconsistencies in the DD heap:
  <ul>
  <li> node has illegal index
  <li> live node has dead children
  <li> node has illegal Then or Else pointers
  <li> BDD/ADD node has identical children
  <li> ZDD node has zero then child
  <li> wrong number of total nodes
  <li> wrong number of dead nodes
  <li> ref count error at node
  </ul>
  Returns 0 if no inconsistencies are found; DD_OUT_OF_MEM if there is
  not enough memory; 1 otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_CheckKeys]

******************************************************************************/
int
Cudd_DebugCheck(
  DdManager * table)
{
    unsigned int i;
    int		j,count;
    int		slots;
    DdNodePtr	*nodelist;
    DdNode	*f;
    DdNode	*sentinel = &(table->sentinel);
    st_table	*edgeTable;	/* stores internal ref count for each node */
    st_generator	*gen;
    int		flag = 0;
    int		totalNode;
    int		deadNode;
    int		index;
    

    edgeTable = st_init_table(st_ptrcmp,st_ptrhash);
    if (edgeTable == NULL) return(CUDD_OUT_OF_MEM);

    /* Check the BDD/ADD subtables. */
    for (i = 0; i < (unsigned) table->size; i++) {
	index = table->invperm[i];
	if (i != (unsigned) table->perm[index]) {
	    (void) fprintf(table->err,
			   "Permutation corrupted: invperm[%d] = %d\t perm[%d] = %d\n",
			   i, index, index, table->perm[index]);
	}
	nodelist = table->subtables[i].nodelist;
	slots = table->subtables[i].slots;

	totalNode = 0;
	deadNode = 0;
	for (j = 0; j < slots; j++) {	/* for each subtable slot */
	    f = nodelist[j];
	    while (f != sentinel) {
		totalNode++;
		if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) { 
		    if ((int) f->index != index) {
			(void) fprintf(table->err,
				       "Error: node has illegal index\n");
			cuddPrintNode(f,table->err);
			flag = 1;
		    }
		    if ((unsigned) cuddI(table,cuddT(f)->index) <= i ||
			(unsigned) cuddI(table,Cudd_Regular(cuddE(f))->index)
			<= i) {
			(void) fprintf(table->err,
				       "Error: node has illegal children\n");
			cuddPrintNode(f,table->err);
			flag = 1;
		    }
		    if (Cudd_Regular(cuddT(f)) != cuddT(f)) {
			(void) fprintf(table->err,
				       "Error: node has illegal form\n");
			cuddPrintNode(f,table->err);
			flag = 1;
		    }
		    if (cuddT(f) == cuddE(f)) {
			(void) fprintf(table->err,
				       "Error: node has identical children\n");
			cuddPrintNode(f,table->err);
			flag = 1;
		    }
		    if (cuddT(f)->ref == 0 || Cudd_Regular(cuddE(f))->ref == 0) {
			(void) fprintf(table->err,
				       "Error: live node has dead children\n");
			cuddPrintNode(f,table->err);
			flag =1;
		    }
		    /* Increment the internal reference count for the
		    ** then child of the current node.
		    */
		    if (st_lookup(edgeTable,(char *)cuddT(f),(char **)&count)) {
			count++;
		    } else {
			count = 1;
		    }
		    if (st_insert(edgeTable,(char *)cuddT(f),
		    (char *)(long)count) == ST_OUT_OF_MEM) {
			st_free_table(edgeTable);
			return(CUDD_OUT_OF_MEM);
		    }
		
		    /* Increment the internal reference count for the
		    ** else child of the current node.
		    */
		    if (st_lookup(edgeTable,(char *)Cudd_Regular(cuddE(f)),(char **)&count)) {
			count++;
		    } else {
			count = 1;
		    }
		    if (st_insert(edgeTable,(char *)Cudd_Regular(cuddE(f)),
		    (char *)(long)count) == ST_OUT_OF_MEM) {
			st_free_table(edgeTable);
			return(CUDD_OUT_OF_MEM);
		    }
		} else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) {
		    deadNode++;
#if 0
		    debugCheckParent(table,f);
#endif
		} else {
		    fprintf(table->err,
			    "Error: node has illegal Then or Else pointers\n");
		    cuddPrintNode(f,table->err);
		    flag = 1;
		}

		f = f->next;
	    }	/* for each element of the collision list */
	}	/* for each subtable slot */

	if ((unsigned) totalNode != table->subtables[i].keys) {
	    fprintf(table->err,"Error: wrong number of total nodes\n");
	    flag = 1;
	}
	if ((unsigned) deadNode != table->subtables[i].dead) {
	    fprintf(table->err,"Error: wrong number of dead nodes\n");
	    flag = 1;
	}
    }	/* for each BDD/ADD subtable */

    /* Check the ZDD subtables. */
    for (i = 0; i < (unsigned) table->sizeZ; i++) {
	index = table->invpermZ[i];
	if (i != (unsigned) table->permZ[index]) {
	    (void) fprintf(table->err,
			   "Permutation corrupted: invpermZ[%d] = %d\t permZ[%d] = %d in ZDD\n",
			   i, index, index, table->permZ[index]);
	}
	nodelist = table->subtableZ[i].nodelist;
	slots = table->subtableZ[i].slots;

	totalNode = 0;
	deadNode = 0;
	for (j = 0; j < slots; j++) {	/* for each subtable slot */
	    f = nodelist[j];
	    while (f != NULL) {
		totalNode++;
		if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref != 0) { 
		    if ((int) f->index != index) {
			(void) fprintf(table->err,
				       "Error: ZDD node has illegal index\n");
			cuddPrintNode(f,table->err);
			flag = 1;
		    }
		    if (Cudd_IsComplement(cuddT(f)) ||
			Cudd_IsComplement(cuddE(f))) {
			(void) fprintf(table->err,
				       "Error: ZDD node has complemented children\n");
			cuddPrintNode(f,table->err);
			flag = 1;
		    }
		    if ((unsigned) cuddIZ(table,cuddT(f)->index) <= i ||
		    (unsigned) cuddIZ(table,cuddE(f)->index) <= i) {
			(void) fprintf(table->err,
				       "Error: ZDD node has illegal children\n");
			cuddPrintNode(f,table->err);
			cuddPrintNode(cuddT(f),table->err);
			cuddPrintNode(cuddE(f),table->err);
			flag = 1;
		    }
		    if (cuddT(f) == DD_ZERO(table)) {
			(void) fprintf(table->err,
				       "Error: ZDD node has zero then child\n");
			cuddPrintNode(f,table->err);
			flag = 1;
		    }
		    if (cuddT(f)->ref == 0 || cuddE(f)->ref == 0) {
			(void) fprintf(table->err,
				       "Error: ZDD live node has dead children\n");
			cuddPrintNode(f,table->err);
			flag =1;
		    }
		    /* Increment the internal reference count for the
		    ** then child of the current node.
		    */
		    if (st_lookup(edgeTable,(char *)cuddT(f),(char **)&count)) {
			count++;
		    } else {
			count = 1;
		    }
		    if (st_insert(edgeTable,(char *)cuddT(f),
		    (char *)(long)count) == ST_OUT_OF_MEM) {
			st_free_table(edgeTable);
			return(CUDD_OUT_OF_MEM);
		    }
		
		    /* Increment the internal reference count for the
		    ** else child of the current node.
		    */
		    if (st_lookup(edgeTable,(char *)cuddE(f),(char **)&count)) {
			count++;
		    } else {
			count = 1;
		    }
		    if (st_insert(edgeTable,(char *)cuddE(f),
		    (char *)(long)count) == ST_OUT_OF_MEM) {
			st_free_table(edgeTable);
			table->errorCode = CUDD_MEMORY_OUT;
			return(CUDD_OUT_OF_MEM);
		    }
		} else if (cuddT(f) != NULL && cuddE(f) != NULL && f->ref == 0) {
		    deadNode++;
#if 0
		    debugCheckParent(table,f);
#endif
		} else {
		    fprintf(table->err,
			    "Error: ZDD node has illegal Then or Else pointers\n");
		    cuddPrintNode(f,table->err);
		    flag = 1;
		}

		f = f->next;
	    }	/* for each element of the collision list */
	}	/* for each subtable slot */

	if ((unsigned) totalNode != table->subtableZ[i].keys) {
	    fprintf(table->err,
		    "Error: wrong number of total nodes in ZDD\n");
	    flag = 1;
	}
	if ((unsigned) deadNode != table->subtableZ[i].dead) {
	    fprintf(table->err,
		    "Error: wrong number of dead nodes in ZDD\n");
	    flag = 1;
	}
    }	/* for each ZDD subtable */

    /* Check the constant table. */
    nodelist = table->constants.nodelist;
    slots = table->constants.slots;

    totalNode = 0;
    deadNode = 0;
    for (j = 0; j < slots; j++) {
	f = nodelist[j];
	while (f != NULL) {
	    totalNode++;
	    if (f->ref != 0) { 
		if (f->index != CUDD_CONST_INDEX) {
		    fprintf(table->err,"Error: node has illegal index\n");
#if SIZEOF_VOID_P == 8
		    fprintf(table->err,
			    "       node 0x%lx, id = %d, ref = %d, value = %g\n",
			    (unsigned long)f,f->index,f->ref,cuddV(f));
#else
		    fprintf(table->err,
			    "       node 0x%x, id = %d, ref = %d, value = %g\n",
			    (unsigned)f,f->index,f->ref,cuddV(f));
#endif
		    flag = 1;
		}
	    } else {
		deadNode++;
	    }
	    f = f->next;
	}
    }
    if ((unsigned) totalNode != table->constants.keys) {
	(void) fprintf(table->err,
		       "Error: wrong number of total nodes in constants\n");
	flag = 1;
    }
    if ((unsigned) deadNode != table->constants.dead) {
	(void) fprintf(table->err,
		       "Error: wrong number of dead nodes in constants\n");
	flag = 1;
    }
    gen = st_init_gen(edgeTable);
    while (st_gen(gen,(char **)&f,(char **)&count)) {
	if (count > (int)(f->ref) && f->ref != DD_MAXREF) {
#if SIZEOF_VOID_P == 8
	    fprintf(table->err,"ref count error at node 0x%lx, count = %d, id = %d, ref = %d, then = 0x%lx, else = 0x%lx\n",(unsigned long)f,count,f->index,f->ref,(unsigned long)cuddT(f),(unsigned long)cuddE(f));
#else
	    fprintf(table->err,"ref count error at node 0x%x, count = %d, id = %d, ref = %d, then = 0x%x, else = 0x%x\n",(unsigned)f,count,f->index,f->ref,(unsigned)cuddT(f),(unsigned)cuddE(f));
#endif
	    debugFindParent(table,f);
	    flag = 1;
	}
    }
    st_free_gen(gen);
    st_free_table(edgeTable);

    return (flag);

} /* end of Cudd_DebugCheck */


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

  Synopsis    [Checks for several conditions that should not occur.]

  Description [Checks for the following conditions:
  <ul>
  <li>Wrong sizes of subtables.
  <li>Wrong number of keys found in unique subtable.
  <li>Wrong number of dead found in unique subtable.
  <li>Wrong number of keys found in the constant table
  <li>Wrong number of dead found in the constant table
  <li>Wrong number of total slots found
  <li>Wrong number of maximum keys found
  <li>Wrong number of total dead found
  </ul>
  Reports the average length of non-empty lists. Returns the number of
  subtables for which the number of keys is wrong.]

  SideEffects [None]

  SeeAlso     [Cudd_DebugCheck]

******************************************************************************/
int
Cudd_CheckKeys(