cuddsubsetsp.c

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

    /* each node has one table entry */
    /* update as you go down the min dist of each node from
       the root in each (odd and even) parity */
    if (!st_lookup(pathTable, (char *)N, (char **)&nodeStat)) {
	fprintf(fp, "Something wrong, the entry doesn't exist\n");
	return(0);
    }

    /* compute length of odd parity distances */
    if ((nodeStat->oddTopDist != MAXSHORTINT) &&
	(nodeStat->oddBotDist != MAXSHORTINT))
	oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
    else
	oddLen = MAXSHORTINT;

    /* compute length of even parity distances */
    if (!((nodeStat->evenTopDist == MAXSHORTINT) ||
	  (nodeStat->evenBotDist == MAXSHORTINT)))
	evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
    else
	evenLen = MAXSHORTINT;

    /* assign pathlength to minimum of the two */
    pathLength = (oddLen <= evenLen) ? oddLen : evenLen;

    Nv = Cudd_T(N);
    Nnv = Cudd_E(N);

    /* process each child */
    processingDone = 0;
    while (processingDone != 2) {
	if (!processingDone) {
	    child = Nv;
	} else {
	    child = Nnv;
	}

	realChild = Cudd_NotCond(child, Cudd_IsComplement(node));
	regChild = Cudd_Regular(child);
	if (Cudd_IsConstant(realChild)) {
	    /* Found a minterm; count parity and shortest distance
	    ** from the constant.
	    */
	    if (Cudd_IsComplement(child))
		nodeStat->oddBotDist = 1;
	    else
		nodeStat->evenBotDist = 1;
	} else { 
	    /* If node not in table, recur. */
	    if (!st_lookup(pathTable, (char *) regChild,
			   (char **)&nodeStatChild)) {
		fprintf(fp, "Something wrong, node in table should have been created in top dist proc.\n");
		return(0);
	    }

	    if (nodeStatChild->oddBotDist == MAXSHORTINT) {
		if (nodeStatChild->evenBotDist == MAXSHORTINT) {
		    if (!CreateBotDist(realChild, pathTable, pathLengthArray, fp))
			return(0);
		} else {
		    fprintf(fp, "Something wrong, both bot nodeStats should be there\n");
		    return(0);
		}
	    }

	    /* Update shortest distance from the constant depending on
	    **  parity. */

	    if (Cudd_IsComplement(child)) {
		/* If parity on the edge then add 1 to even distance
		** of child to get odd parity distance and add 1 to
		** odd distance of child to get even parity
		** distance. Change distance of current node only if
		** the calculated distance is less than existing
		** distance. */
		if (nodeStatChild->oddBotDist != MAXSHORTINT)
		    botDist = nodeStatChild->oddBotDist + 1;
		else
		    botDist = MAXSHORTINT;
		if (nodeStat->evenBotDist > botDist )
		    nodeStat->evenBotDist = botDist;

		if (nodeStatChild->evenBotDist != MAXSHORTINT)
		    botDist = nodeStatChild->evenBotDist + 1;
		else
		    botDist = MAXSHORTINT;
		if (nodeStat->oddBotDist > botDist)
		    nodeStat->oddBotDist = botDist;

	    } else {
		/* If parity on the edge then add 1 to even distance
		** of child to get even parity distance and add 1 to
		** odd distance of child to get odd parity distance.
		** Change distance of current node only if the
		** calculated distance is lesser than existing
		** distance. */
		if (nodeStatChild->evenBotDist != MAXSHORTINT)
		    botDist = nodeStatChild->evenBotDist + 1;
		else
		    botDist = MAXSHORTINT;
		if (nodeStat->evenBotDist > botDist)
		    nodeStat->evenBotDist = botDist;

		if (nodeStatChild->oddBotDist != MAXSHORTINT)
		    botDist = nodeStatChild->oddBotDist + 1;
		else
		    botDist = MAXSHORTINT;
		if (nodeStat->oddBotDist > botDist)
		    nodeStat->oddBotDist = botDist;
	    }
	} /* end of else (if not constant child ) */
	processingDone++;
    } /* end of while processing Nv, Nnv */

    /* Compute shortest path length on the fly. */
    if ((nodeStat->oddTopDist != MAXSHORTINT) &&
	(nodeStat->oddBotDist != MAXSHORTINT))
	oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
    else
	oddLen = MAXSHORTINT;

    if ((nodeStat->evenTopDist != MAXSHORTINT) &&
	(nodeStat->evenBotDist != MAXSHORTINT))
	evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
    else
	evenLen = MAXSHORTINT;

    /* Update path length array that has number of nodes of a particular
    ** path length. */
    if (oddLen < pathLength ) {
	if (pathLength != MAXSHORTINT)
	    pathLengthArray[pathLength]--;
	if (oddLen != MAXSHORTINT)
	    pathLengthArray[oddLen]++;
	pathLength = oddLen;
    }
    if (evenLen < pathLength ) {
	if (pathLength != MAXSHORTINT)
	    pathLengthArray[pathLength]--;
	if (evenLen != MAXSHORTINT)
	    pathLengthArray[evenLen]++;
    }

    return(1);

} /*end of CreateBotDist */


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

  Synopsis    [ The outer procedure to label each node with its shortest
  distance from the root and constant]

  Description [ The outer procedure to label each node with its shortest
  distance from the root and constant. Calls CreateTopDist and CreateBotDist.
  The basis for computing the distance between root and constant is that
  the distance may be the sum of even distances from the node to the root
  and constant or the sum of odd distances from the node to the root and
  constant.  Both CreateTopDist and CreateBotDist create the odd and
  even parity distances from the root and constant respectively.]

  SideEffects [None]

  SeeAlso     [CreateTopDist CreateBotDist]

******************************************************************************/
static st_table *
CreatePathTable(
  DdNode * node /* root of function */,
  unsigned int * pathLengthArray /* array of path lengths to store nodes labeled with the various path lengths */,
  FILE *fp /* where to write messages */)
{

    st_table *pathTable;
    NodeDist_t *nodeStat;
    DdHalfWord topLen;
    DdNode *N;
    int i, numParents;
    int insertValue;
    DdNode **childPage;
    int parentPage;
    int childQueueIndex, parentQueueIndex;

    /* Creating path Table for storing data about nodes */
    pathTable = st_init_table(st_ptrcmp,st_ptrhash);

    /* initializing pages for info about each node */
    maxNodeDistPages = INITIAL_PAGES;
    nodeDistPages = ALLOC(NodeDist_t *, maxNodeDistPages);
    if (nodeDistPages == NULL) {
	goto OUT_OF_MEM;
    }
    nodeDistPage = 0;
    currentNodeDistPage = nodeDistPages[nodeDistPage] =
	ALLOC(NodeDist_t, nodeDistPageSize);
    if (currentNodeDistPage == NULL) {
	for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]);
	FREE(nodeDistPages);
	goto OUT_OF_MEM;
    }
    nodeDistPageIndex = 0;

    /* Initializing pages for the BFS search queue, implemented as an array. */
    maxQueuePages = INITIAL_PAGES;
    queuePages = ALLOC(DdNode **, maxQueuePages);
    if (queuePages == NULL) {
	goto OUT_OF_MEM;
    }
    queuePage = 0;
    currentQueuePage  = queuePages[queuePage] = ALLOC(DdNode *, queuePageSize);
    if (currentQueuePage == NULL) {
	for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
	FREE(queuePages);
	goto OUT_OF_MEM;
    }
    queuePageIndex = 0;

    /* Enter the root node into the queue to start with. */
    parentPage = queuePage;
    parentQueueIndex = queuePageIndex;
    topLen = 0;
    *(currentQueuePage + queuePageIndex) = node;
    queuePageIndex++;
    childPage = currentQueuePage;
    childQueueIndex = queuePageIndex;

    N = Cudd_Regular(node);

    if (nodeDistPageIndex == nodeDistPageSize) ResizeNodeDistPages();
    if (memOut) {
	for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]);
	FREE(nodeDistPages);
	for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
	FREE(queuePages);
	st_free_table(pathTable);
	goto OUT_OF_MEM;
    }

    nodeStat = currentNodeDistPage + nodeDistPageIndex;
    nodeDistPageIndex++;

    nodeStat->oddTopDist = MAXSHORTINT;
    nodeStat->evenTopDist = MAXSHORTINT;
    nodeStat->evenBotDist = MAXSHORTINT;
    nodeStat->oddBotDist = MAXSHORTINT;
    nodeStat->regResult = NULL;
    nodeStat->compResult = NULL;

    insertValue = st_insert(pathTable, (char *)N, (char *)nodeStat);
    if (insertValue == ST_OUT_OF_MEM) {
	memOut = 1;
	for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]);
	FREE(nodeDistPages);
	for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
	FREE(queuePages);
	st_free_table(pathTable);
	goto OUT_OF_MEM;
    } else if (insertValue == 1) {
	fprintf(fp, "Something wrong, the entry exists but didnt show up in st_lookup\n");
	return(NULL);
    }

    if (Cudd_IsComplement(node)) {
	nodeStat->oddTopDist = 0;
    } else {
	nodeStat->evenTopDist = 0;
    }
    numParents = 1;
    /* call the function that counts the distance of each node from the
     * root
     */
#ifdef DD_DEBUG
    numCalls = 0;
#endif
    CreateTopDist(pathTable, parentPage, parentQueueIndex, (int) topLen,
		  childPage, childQueueIndex, numParents, fp);
    if (memOut) {
	fprintf(fp, "Out of Memory and cant count path lengths\n");
	goto OUT_OF_MEM;
    }

#ifdef DD_DEBUG
    numCalls = 0;
#endif
    /* call the function that counts the distance of each node from the
     * constant
     */
    if (!CreateBotDist(node, pathTable, pathLengthArray, fp)) return(NULL);

    /* free BFS queue pages as no longer required */
    for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
    FREE(queuePages);
    return(pathTable);

OUT_OF_MEM:
    (void) fprintf(fp, "Out of Memory, cannot allocate pages\n");
    memOut = 1;
    return(NULL);

} /*end of CreatePathTable */


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

  Synopsis    [Chooses the maximum allowable path length of nodes under the
  threshold.]

  Description [Chooses the maximum allowable path length under each node.
  The corner cases are when the threshold is larger than the number
  of nodes in the BDD iself, in which case 'numVars + 1' is returned.
  If all nodes of a particular path length are needed, then the
  maxpath returned is the next one with excess nodes = 0;]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static unsigned int
AssessPathLength(
  unsigned int * pathLengthArray /* array determining number of nodes belonging to the different path lengths */,
  int  threshold /* threshold to determine maximum allowable nodes in the subset */,
  int  numVars /* maximum number of variables */,
  unsigned int * excess /* number of nodes labeled maxpath required in the subset */,
  FILE *fp /* where to write messages */)
{
    unsigned int i, maxpath;
    int temp;

    temp = threshold;
    i = 0;
    maxpath = 0;
    /* quit loop if i reaches max number of variables or if temp reaches
     * below zero
     */
    while ((i < (unsigned) numVars+1) && (temp > 0)) {
	if (pathLengthArray[i] > 0) {
	    maxpath = i;
	    temp = temp - pathLengthArray[i];
	}
	i++;
    }
    /* if all nodes of max path are needed */
    if (temp >= 0) {
	maxpath++; /* now maxpath  becomes the next maxppath or max number
		      of variables */
	*excess = 0;
    } else { /* normal case when subset required is less than size of
		original BDD */
	*excess = temp + pathLengthArray[maxpath];
    }

    if (maxpath == 0) {
	fprintf(fp, "Path Length array seems to be all zeroes, check\n");
    }
    return(maxpath);

} /* end of AssessPathLength */


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

  Synopsis    [Builds the BDD with nodes labeled with path length less than or equal to maxpath]

  Description [Builds the BDD with nodes labeled with path length
  under maxpath and as many nodes labeled maxpath as determined by the
  threshold. The procedure uses the path table to determine which nodes
  in the original bdd need to be retained. This procedure picks a
  shortest path (tie break decided by taking the child with the shortest
  distance to the constant) and recurs down the path till it reaches the
  constant. the procedure then starts building the subset upward from
  the constant. All nodes labeled by path lengths less than the given
  maxpath are used to build the subset.  However, in the case of nodes
  that have label equal to maxpath, as many are chosen as required by
  the threshold. This number is stored in the info structure in the
  field thresholdReached. This field is decremented whenever a node
  labeled maxpath is encountered and the nodes labeled maxpath are
  aggregated in a maxpath table. As soon as the thresholdReached count
  goes to 0, the shortest path from this node to the constant is found.
  The extraction of nodes with the above labeling is based on the fact
  that each node, labeled with a path length, P, has at least one child
  labeled P or less. So extracting all nodes labeled a given path length
  P ensures complete paths between the root and the constant. Extraction
  of a partial number of nodes with a given path length may result in
  incomplete paths and hence the additional number of nodes are grabbed
  to complete the path. Since the Bdd is built bottom-up, other nodes
  labeled maxpath do lie on complete paths.  The procedure may cause the
  subset to have a larger or smaller number of nodes than the specified
  threshold. The increase in the number of nodes is caused by the
  building of a subset and the reduction by recombination. However in
  most cases, the recombination overshadows the increase and the
  procedure returns a result with lower number of nodes than specified.
  The subsetNodeTable is NIL when there is no hard limit on the number
  of nodes. Further efforts towards keeping the subset closer to the
  threshold number were abandoned in favour of keeping the procedure
  simple and fast.]

  SideEffects [SubsetNodeTable is changed if it is not NIL.]

  SeeAlso     []

******************************************************************************/
static DdNode *
BuildSubsetBdd(
  DdManager * dd /* DD manager */,
  st_table * pathTable /* path table with path lengths and computed results */,
  DdNode * node /* current node */,