cuddsubsethb.c

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

    /* find the minterm counts for the THEN and ELSE branches */
    if (Cudd_IsConstant(Nv)) {
	if (Nv == zero) {
	    minNv = 0.0;
	} else {
	    minNv = max;
	}
    } else {
	if (st_lookup(table, (char *)Nv, (char **)&dummyNv) == 1)
	    minNv = *(dummyNv->mintermPointer);
	else {
	    return(0);
	}
    }
    if (Cudd_IsConstant(Nnv)) {
	if (Nnv == zero) {
	    minNnv = 0.0;
	} else {
	    minNnv = max;
	}
    } else {
	if (st_lookup(table, (char *)Nnv, (char **)&dummyNnv) == 1) {
	    minNnv = *(dummyNnv->mintermPointer);
	}
	else {
	    return(0);
	}
    }


    /* recur based on which has larger minterm, */
    if (minNv >= minNnv) {
	tval = SubsetCountNodesAux(Nv, table, max);
	if (memOut) return(0);
	eval = SubsetCountNodesAux(Nnv, table, max);
	if (memOut) return(0);

	/* store the node count of the lighter child. */
	if (pageIndex == pageSize) ResizeCountNodePages();
	if (memOut) {
	    for (i = 0; i <= page; i++) FREE(mintermPages[i]);
	    FREE(mintermPages);
	    for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
	    FREE(nodeDataPages);
	    st_free_table(table);
	    return(0);
	}
	pmin = currentLightNodePage + pageIndex;
	*pmin = eval; /* Here the ELSE child is lighter */
	dummyN->lightChildNodesPointer = pmin;

    } else {
	eval = SubsetCountNodesAux(Nnv, table, max);
	if (memOut) return(0);
	tval = SubsetCountNodesAux(Nv, table, max);
	if (memOut) return(0);

	/* store the node count of the lighter child. */
	if (pageIndex == pageSize) ResizeCountNodePages();
	if (memOut) {
	    for (i = 0; i <= page; i++) FREE(mintermPages[i]);
	    FREE(mintermPages);
	    for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
	    FREE(nodeDataPages);
	    st_free_table(table);
	    return(0);
	}
	pmin = currentLightNodePage + pageIndex;
	*pmin = tval; /* Here the THEN child is lighter */
	dummyN->lightChildNodesPointer = pmin;

    }
    /* updating the page index for node count storage. */
    pmin = currentNodePage + pageIndex;
    *pmin = tval + eval + 1;
    dummyN->nodesPointer = pmin;

    /* pageIndex is parallel page index for count_nodes and count_lightNodes */
    pageIndex++;

    /* if this node has been reached first, it belongs to a heavier
       branch. Its complement will be reached later on a lighter branch.
       Hence the complement has zero node count. */

    if (st_lookup(table, (char *)Cudd_Not(node), (char **)&dummyNBar) == 1)  {
	if (pageIndex == pageSize) ResizeCountNodePages();
	if (memOut) {
	    for (i = 0; i < page; i++) FREE(mintermPages[i]);
	    FREE(mintermPages);
	    for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
	    FREE(nodeDataPages);
	    st_free_table(table);
	    return(0);
	}
	pminBar = currentLightNodePage + pageIndex;
	*pminBar = 0;
	dummyNBar->lightChildNodesPointer = pminBar;
	/* The lighter child has less nodes than the parent.
	 * So if parent 0 then lighter child zero
	 */
	if (pageIndex == pageSize) ResizeCountNodePages();
	if (memOut) {
	    for (i = 0; i < page; i++) FREE(mintermPages[i]);
	    FREE(mintermPages);
	    for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
	    FREE(nodeDataPages);
	    st_free_table(table);
	    return(0);
	}
	pminBar = currentNodePage + pageIndex;
	*pminBar = 0;
	dummyNBar->nodesPointer = pminBar ; /* maybe should point to zero */

	pageIndex++;
    }
    return(*pmin);
} /*end of SubsetCountNodesAux */


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

  Synopsis    [Counts the nodes under the current node and its lighter child]

  Description [Counts the nodes under the current node and its lighter
  child. Calls a recursive procedure to count the number of nodes of
  a DAG rooted at a particular node and the number of nodes taken by its
  lighter child.]

  SideEffects [None]

  SeeAlso     [SubsetCountNodesAux]

******************************************************************************/
static int
SubsetCountNodes(
  DdNode * node /* function to be analyzed */,
  st_table * table /* node quality table */,
  int  nvars /* number of variables node depends on */)
{
    int	num;
    int i;

#ifdef DEBUG
    num_calls = 0;
#endif

    max = pow(2.0,(double) nvars);
    maxPages = INITIAL_PAGES;
    nodePages = ALLOC(int *,maxPages);
    if (nodePages == NULL)  {
	goto OUT_OF_MEM;
    }

    lightNodePages = ALLOC(int *,maxPages);
    if (lightNodePages == NULL) {
	for (i = 0; i <= page; i++) FREE(mintermPages[i]);
	FREE(mintermPages);
	for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
	FREE(nodeDataPages);
	FREE(nodePages);
	goto OUT_OF_MEM;
    }

    page = 0;
    currentNodePage = nodePages[page] = ALLOC(int,pageSize);
    if (currentNodePage == NULL) {
	for (i = 0; i <= page; i++) FREE(mintermPages[i]);
	FREE(mintermPages);
	for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
	FREE(nodeDataPages);
	FREE(lightNodePages);
	FREE(nodePages);
	goto OUT_OF_MEM;
    }

    currentLightNodePage = lightNodePages[page] = ALLOC(int,pageSize);
    if (currentLightNodePage == NULL) {
	for (i = 0; i <= page; i++) FREE(mintermPages[i]);
	FREE(mintermPages);
	for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
	FREE(nodeDataPages);
	FREE(currentNodePage);
	FREE(lightNodePages);
	FREE(nodePages);
	goto OUT_OF_MEM;
    }

    pageIndex = 0;
    num = SubsetCountNodesAux(node,table,max);
    if (memOut) goto OUT_OF_MEM;
    return(num);

OUT_OF_MEM:
    memOut = 1;
    return(0);

} /* end of SubsetCountNodes */


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

  Synopsis    [Procedure to recursively store nodes that are retained in the subset.]

  Description [rocedure to recursively store nodes that are retained in the subset.]

  SideEffects [None]

  SeeAlso     [StoreNodes]

******************************************************************************/
static void
StoreNodes(
  st_table * storeTable,
  DdManager * dd,
  DdNode * node)
{
    char *dummy;
    DdNode *N, *Nt, *Ne;
    if (Cudd_IsConstant(dd)) {
	return;
    }
    N = Cudd_Regular(node);
    if (st_lookup(storeTable, (char *)N, (char **)&dummy)) {
	return;
    }
    cuddRef(N);
    if (st_insert(storeTable, (char *)N, NIL(char)) == ST_OUT_OF_MEM) {
	fprintf(dd->err,"Something wrong, st_table insert failed\n");
    }

    Nt = Cudd_T(N);
    Ne = Cudd_E(N);

    StoreNodes(storeTable, dd, Nt);
    StoreNodes(storeTable, dd, Ne);
    return;

}


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

  Synopsis    [Builds the subset BDD using the heavy branch method.] 

  Description [The procedure carries out the building of the subset BDD
  starting at the root. Using the three different counts labelling each node,
  the procedure chooses the heavier branch starting from the root and keeps
  track of the number of nodes it discards at each step, thus keeping count
  of the size of the subset BDD dynamically. Once the threshold is satisfied,
  the procedure then calls ITE to build the BDD.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
BuildSubsetBdd(
  DdManager * dd /* DD manager */,
  DdNode * node /* current node */,
  int * size /* current size of the subset */,
  st_table * visitedTable /* visited table storing all node data */,
  int  threshold,
  st_table * storeTable,
  st_table * approxTable)
{

    DdNode *Nv, *Nnv, *N, *topv, *neW;
    double minNv, minNnv;
    NodeData_t *currNodeQual;
    NodeData_t *currNodeQualT;
    NodeData_t *currNodeQualE;
    DdNode *ThenBranch, *ElseBranch;
    unsigned int topid;
    char *dummy;

#ifdef DEBUG
    num_calls++;
#endif
    /*If the size of the subset is below the threshold, dont do
      anything. */
    if ((*size) <= threshold) {
      /* store nodes below this, so we can recombine if possible */
      StoreNodes(storeTable, dd, node);
      return(node);
    }

    if (Cudd_IsConstant(node))
	return(node);

    /* Look up minterm count for this node. */
    if (!st_lookup(visitedTable, (char *)node, (char **)&currNodeQual)) {
	fprintf(dd->err,
		"Something is wrong, ought to be in node quality table\n");
    }

    /* Get children. */
    N = Cudd_Regular(node);
    Nv = Cudd_T(N);
    Nnv = Cudd_E(N);

    /* complement if necessary */
    Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
    Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));

    if (!Cudd_IsConstant(Nv)) {
        /* find out minterms and nodes contributed by then child */
        if (!st_lookup(visitedTable, (char *)Nv,
		       (char **)&currNodeQualT)) {
		fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
		dd->errorCode = CUDD_INTERNAL_ERROR;
		return(NULL);
	    }
	else {
	    minNv = *(((NodeData_t *)currNodeQualT)->mintermPointer);
	}
    } else {
	if (Nv == zero) {
	    minNv = 0;
	} else  {
	    minNv = max;
	}
    }
    if (!Cudd_IsConstant(Nnv)) {
        /* find out minterms and nodes contributed by else child */
	if (!st_lookup(visitedTable, (char *)Nnv, (char **)&currNodeQualE)) {
	    fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
	    dd->errorCode = CUDD_INTERNAL_ERROR;
	    return(NULL);
	} else {
	    minNnv = *(((NodeData_t *)currNodeQualE)->mintermPointer);
	}
    } else {
	if (Nnv == zero) {
	    minNnv = 0;
	} else {
	    minNnv = max;
	}
    }

    /* keep track of size of subset by subtracting the number of
     * differential nodes contributed by lighter child
     */
    *size = (*(size)) - (int)*(currNodeQual->lightChildNodesPointer);
    if (minNv >= minNnv) { /*SubsetCountNodesAux procedure takes
			     the Then branch in case of a tie */

        /* recur with the Then branch */
	ThenBranch = (DdNode *)BuildSubsetBdd(dd, Nv, size,
	      visitedTable, threshold, storeTable, approxTable);
	if (ThenBranch == NULL) {
	    return(NULL);
	}
	cuddRef(ThenBranch);
	/* The Else branch is either a node that already exists in the
	 * subset, or one whose approximation has been computed, or
	 * Zero.
	 */
	if (st_lookup(storeTable, (char *)Cudd_Regular(Nnv), (char **)&dummy)) {
	  ElseBranch = Nnv;
	  cuddRef(ElseBranch);
	} else {
	  if (st_lookup(approxTable, (char *)Nnv, (char **)&dummy)) {
	    ElseBranch = (DdNode *)dummy;
	    cuddRef(ElseBranch);
	  } else {
	    ElseBranch = zero;
	    cuddRef(ElseBranch);
	  }
	}
	
    }
    else {
        /* recur with the Else branch */
        ElseBranch = (DdNode *)BuildSubsetBdd(dd, Nnv, size,
		      visitedTable, threshold, storeTable, approxTable);
	if (ElseBranch == NULL) {
	    return(NULL);
	}
	cuddRef(ElseBranch);
	/* The Then branch is either a node that already exists in the
	 * subset, or one whose approximation has been computed, or
	 * Zero.
	 */
	if (st_lookup(storeTable, (char *)Cudd_Regular(Nv), (char **)&dummy)) {
	  ThenBranch = Nv;
	  cuddRef(ThenBranch);
	} else {
	  if (st_lookup(approxTable, (char *)Nv, (char **)&dummy)) {
	    ThenBranch = (DdNode *)dummy;
	    cuddRef(ThenBranch);
	  } else {
	    ThenBranch = zero;
	    cuddRef(ThenBranch);
	  }
	}
    }

    /* construct the Bdd with the top variable and the two children */
    topid = Cudd_NodeReadIndex(N);
    topv = Cudd_ReadVars(dd, topid);
    cuddRef(topv);
    neW =  cuddBddIteRecur(dd, topv, ThenBranch, ElseBranch);
    if (neW != NULL) {
      cuddRef(neW);
    }
    Cudd_RecursiveDeref(dd, topv);
    Cudd_RecursiveDeref(dd, ThenBranch);
    Cudd_RecursiveDeref(dd, ElseBranch);

      
    if (neW == NULL)
	return(NULL);
    else {
        /* store this node in the store table */
        if (!st_lookup(storeTable, (char *)Cudd_Regular(neW), (char **)&dummy)) {
	  cuddRef(neW);
	  st_insert(storeTable, (char *)Cudd_Regular(neW), (char *)NIL(char));
	  
        }
	/* store the approximation for this node */
	if (N !=  Cudd_Regular(neW)) {
  	    if (st_lookup(approxTable, (char *)node, (char **)&dummy)) {
	        fprintf(dd->err, "This node should not be in the approximated table\n");
	    } else {
	        cuddRef(neW);
	        st_insert(approxTable, (char *)node, (char *)neW);
	    }
	}
        cuddDeref(neW);
        return(neW);
    }
} /* end of BuildSubsetBdd */