cuddsplit.c

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

	cuddRef(q);
	r = cuddBddIteRecur(manager,v,Nv,q);
	if (r == NULL) {
	    Cudd_RecursiveDeref(manager,q);
	    Cudd_RecursiveDeref(manager,v);
	    return(NULL);
	}
	cuddRef(r);
	Cudd_RecursiveDeref(manager,q);
	Cudd_RecursiveDeref(manager,v);
	cuddDeref(r);
	return(r);
    }
    /* If n is greater than numE, extract the difference from the THEN child
    ** and retain the function represented by the ELSE branch.
    */
    if (numE < n) {
	q = cuddSplitSetRecur(manager,mtable,varSeen,
			      Nv, (n-numE),max,index+1);
	if (q == NULL) {
	    Cudd_RecursiveDeref(manager,v);
	    return(NULL);
	}
	cuddRef(q);
	r = cuddBddIteRecur(manager,v,q,Nnv);
	if (r == NULL) {
	    Cudd_RecursiveDeref(manager,q);
	    Cudd_RecursiveDeref(manager,v);
	    return(NULL);
	}
	cuddRef(r);
	Cudd_RecursiveDeref(manager,q);
	Cudd_RecursiveDeref(manager,v);
	cuddDeref(r);    
	return(r);
    }

    /* None of the above cases; (n < numT and n < numE) and either of
    ** the Nv, Nnv or both are not constants. If possible extract the
    ** required minterms the constant branch.
    */
    if (Cudd_IsConstant(Nv) && !Cudd_IsConstant(Nnv)) {
	q = selectMintermsFromUniverse(manager,varSeen,n);
	if (q == NULL) {
	    Cudd_RecursiveDeref(manager,v);
	    return(NULL);
	}
	cuddRef(q);
	result = cuddBddAndRecur(manager,v,q);
	if (result == NULL) {
	    Cudd_RecursiveDeref(manager,q);
	    Cudd_RecursiveDeref(manager,v);
	    return(NULL);
	}
	cuddRef(result);
	Cudd_RecursiveDeref(manager,q);
	Cudd_RecursiveDeref(manager,v);
	cuddDeref(result);
	return(result);
    } else if (!Cudd_IsConstant(Nv) && Cudd_IsConstant(Nnv)) {
	q = selectMintermsFromUniverse(manager,varSeen,n);
	if (q == NULL) {
	    Cudd_RecursiveDeref(manager,v);
	    return(NULL);
	}
	cuddRef(q);
	result = cuddBddAndRecur(manager,Cudd_Not(v),q);
	if (result == NULL) {
	    Cudd_RecursiveDeref(manager,q);
	    Cudd_RecursiveDeref(manager,v);
	    return(NULL);
	}
	cuddRef(result);
	Cudd_RecursiveDeref(manager,q);
	Cudd_RecursiveDeref(manager,v);
	cuddDeref(result);
	return(result);
    }

    /* Both Nv and Nnv are not constants. So choose the one which
    ** has fewer minterms in its onset.
    */
    positive = 0;
    if (numT < numE) {
	q = cuddSplitSetRecur(manager,mtable,varSeen,
			      Nv,n,max,index+1);
	positive = 1;
    } else {
	q = cuddSplitSetRecur(manager,mtable,varSeen,
			      Nnv,n,max,index+1);
    }

    if (q == NULL) {
	Cudd_RecursiveDeref(manager,v);
	return(NULL);
    }
    cuddRef(q);

    if (positive) {
	result = cuddBddAndRecur(manager,v,q);
    } else {
	result = cuddBddAndRecur(manager,Cudd_Not(v),q);
    }
    if (result == NULL) {
	Cudd_RecursiveDeref(manager,q);
	Cudd_RecursiveDeref(manager,v);
	return(NULL);
    }
    cuddRef(result);
    Cudd_RecursiveDeref(manager,q);
    Cudd_RecursiveDeref(manager,v);
    cuddDeref(result);

    return(result);

} /* end of cuddSplitSetRecur */


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

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

  Synopsis [This function prepares an array of variables which have not been
  encountered so far when traversing the procedure cuddSplitSetRecur.]

  Description [This function prepares an array of variables which have not been
  encountered so far when traversing the procedure cuddSplitSetRecur. This
  array is then used to extract the required number of minterms from a constant
  1. The algorithm guarantees that the size of BDD will be utmost \log(n).]

  SideEffects [None]

******************************************************************************/
static DdNode *
selectMintermsFromUniverse(
  DdManager * manager,
  int * varSeen,
  double  n)
{
    int numVars;
    int i, size, j;
     DdNode *one, *zero, *result;
    DdNode **vars;

    numVars = 0;
    size = manager->size;
    one = DD_ONE(manager);
    zero = Cudd_Not(one);

    /* Count the number of variables not encountered so far in procedure
    ** cuddSplitSetRecur.
    */
    for (i = size-1; i >= 0; i--) {
	if(varSeen[i] == 0)
	    numVars++;
    }
    vars = ALLOC(DdNode *, numVars);
    if (!vars) {
	manager->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }

    j = 0;
    for (i = size-1; i >= 0; i--) {
	if(varSeen[i] == 0) {
	    vars[j] = cuddUniqueInter(manager,manager->perm[i],one,zero);
	    cuddRef(vars[j]);
	    j++;
	}
    }

    /* Compute a function which has n minterms and depends on at most
    ** numVars variables.
    */
    result = mintermsFromUniverse(manager,vars,numVars,n, 0);
    if (result) 
	cuddRef(result);

    for (i = 0; i < numVars; i++)
	Cudd_RecursiveDeref(manager,vars[i]);
    FREE(vars);

    return(result);

} /* end of selectMintermsFromUniverse */


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

  Synopsis    [Recursive procedure to extract n mintems from constant 1.]

  Description [Recursive procedure to extract n mintems from constant 1.]

  SideEffects [None]

******************************************************************************/
static DdNode *
mintermsFromUniverse(
  DdManager * manager,
  DdNode ** vars,
  int  numVars,
  double  n,
  int  index)
{
    DdNode *one, *zero;
    DdNode *q, *result;
    double max, max2;
    
    statLine(manager);
    one = DD_ONE(manager);
    zero = Cudd_Not(one);

    max = pow(2.0, (double)numVars);
    max2 = max / 2.0;

    if (n == max)
	return(one);
    if (n == 0.0)
	return(zero);
    /* if n == 2^(numVars-1), return a single variable */
    if (n == max2)
	return vars[index];
    else if (n > max2) {
	/* When n > 2^(numVars-1), a single variable vars[index]
	** contains 2^(numVars-1) minterms. The rest are extracted
	** from a constant with 1 less variable.
	*/
	q = mintermsFromUniverse(manager,vars,numVars-1,(n-max2),index+1);
	if (q == NULL)
	    return(NULL);
	cuddRef(q);
	result = cuddBddIteRecur(manager,vars[index],one,q);
    } else {
	/* When n < 2^(numVars-1), a literal of variable vars[index]
	** is selected. The required n minterms are extracted from a
	** constant with 1 less variable.
	*/
	q = mintermsFromUniverse(manager,vars,numVars-1,n,index+1);
	if (q == NULL)
	    return(NULL);
	cuddRef(q);
	result = cuddBddAndRecur(manager,vars[index],q);
    }
    
    if (result == NULL) {
	Cudd_RecursiveDeref(manager,q);
	return(NULL);
    }
    cuddRef(result);
    Cudd_RecursiveDeref(manager,q);
    cuddDeref(result);
    return(result);

} /* end of mintermsFromUniverse */


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

  Synopsis    [Annotates every node in the BDD node with its minterm count.]

  Description [Annotates every node in the BDD node with its minterm count.
  In this function, every node and the minterm count represented by it are
  stored in a hash table.]

  SideEffects [Fills up 'table' with the pair <node,minterm_count>.]

******************************************************************************/
static double
bddAnnotateMintermCount(
  DdManager * manager,
  DdNode * node,
  double  max,
  st_table * table)
{

    DdNode *N,*Nv,*Nnv;
    register double min_v,min_nv;
    register double min_N;
    double *pmin;
    double *dummy;

    statLine(manager);
    N = Cudd_Regular(node);
    if (cuddIsConstant(N)) {
	if (node == DD_ONE(manager)) {
	    return(max);
	} else {
	    return(0.0);
	}
    }

    if (st_lookup(table,(char *)node,(char **)&dummy)) {
	return(*dummy);
    }	
  
    Nv = cuddT(N);
    Nnv = cuddE(N);
    if (N != node) {
	Nv = Cudd_Not(Nv);
	Nnv = Cudd_Not(Nnv);
    }

    /* Recur on the two branches. */
    min_v  = bddAnnotateMintermCount(manager,Nv,max,table) / 2.0;
    if (min_v == (double)CUDD_OUT_OF_MEM)
	return ((double)CUDD_OUT_OF_MEM);
    min_nv = bddAnnotateMintermCount(manager,Nnv,max,table) / 2.0;
    if (min_nv == (double)CUDD_OUT_OF_MEM)
	return ((double)CUDD_OUT_OF_MEM);
    min_N  = min_v + min_nv;

    pmin = ALLOC(double,1);
    if (pmin == NULL) {
	manager->errorCode = CUDD_MEMORY_OUT;
	return((double)CUDD_OUT_OF_MEM);
    }
    *pmin = min_N;

    if (st_insert(table,(char *)node, (char *)pmin) == ST_OUT_OF_MEM) {
	FREE(pmin);
	return((double)CUDD_OUT_OF_MEM);
    }
    
    return(min_N);

} /* end of bddAnnotateMintermCount */