cuddgroup.c

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

    return(1);

} /* end of ddGroupSiftingBackward */


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

  Synopsis    [Merges groups in the DD table.]

  Description [Creates a single group from low to high and adjusts the
  index field of the tree node.]

  SideEffects [None]

******************************************************************************/
static void
ddMergeGroups(
  DdManager * table,
  MtrNode * treenode,
  int  low,
  int  high)
{
    int i;
    MtrNode *auxnode;
    int saveindex;
    int newindex;

    /* Merge all variables from low to high in one group, unless
    ** this is the topmost group. In such a case we do not merge lest
    ** we lose the symmetry information. */
    if (treenode != table->tree) {
	for (i = low; i < high; i++)
	    table->subtables[i].next = i+1;
	table->subtables[high].next = low;
    }

    /* Adjust the index fields of the tree nodes. If a node is the
    ** first child of its parent, then the parent may also need adjustment. */
    saveindex = treenode->index;
    newindex = table->invperm[low];
    auxnode = treenode;
    do {
	auxnode->index = newindex;
	if (auxnode->parent == NULL ||
		(int) auxnode->parent->index != saveindex)
	    break;
	auxnode = auxnode->parent;
    } while (1);
    return;

} /* end of ddMergeGroups */


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

  Synopsis    [Dissolves a group in the DD table.]

  Description [x and y are variables in a group to be cut in two. The cut
  is to pass between x and y.]

  SideEffects [None]

******************************************************************************/
static void
ddDissolveGroup(
  DdManager * table,
  int  x,
  int  y)
{
    int topx;
    int boty;

    /* find top and bottom of the two groups */
    boty = y;
    while ((unsigned) boty < table->subtables[boty].next)
	boty = table->subtables[boty].next;
    
    topx = table->subtables[boty].next;

    table->subtables[boty].next = y;
    table->subtables[x].next = topx;

    return;

} /* end of ddDissolveGroup */


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

  Synopsis    [Pretends to check two variables for aggregation.]

  Description [Pretends to check two variables for aggregation. Always
  returns 0.]

  SideEffects [None]

******************************************************************************/
static int
ddNoCheck(
  DdManager * table,
  int  x,
  int  y)
{
    return(0);

} /* end of ddNoCheck */


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

  Synopsis    [Checks two variables for aggregation.]

  Description [Checks two variables for aggregation. The check is based
  on the second difference of the number of nodes as a function of the
  layer. If the second difference is lower than a given threshold
  (typically negative) then the two variables should be aggregated.
  Returns 1 if the two variables pass the test; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddSecDiffCheck(
  DdManager * table,
  int  x,
  int  y)
{
    double Nx,Nx_1;
    double Sx;
    double threshold;
    int    xindex,yindex;

    if (x==0) return(0);

#ifdef DD_STATS
    secdiffcalls++;
#endif
    Nx = (double) table->subtables[x].keys;
    Nx_1 = (double) table->subtables[x-1].keys;
    Sx = (table->subtables[y].keys/Nx) - (Nx/Nx_1);

    threshold = table->recomb / 100.0;
    if (Sx < threshold) {
	xindex = table->invperm[x];
	yindex = table->invperm[y];
	if (cuddTestInteract(table,xindex,yindex)) {
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
	    (void) fprintf(table->out,
			   "Second difference for %d = %g Pos(%d)\n",
			   table->invperm[x],Sx,x);
#endif
#ifdef DD_STATS
	    secdiff++;
#endif
	    return(1);
	} else {
#ifdef DD_STATS
	    secdiffmisfire++;
#endif
	    return(0);
	}

    }
    return(0);

} /* end of ddSecDiffCheck */


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

  Synopsis    [Checks for extended symmetry of x and y.]

  Description [Checks for extended symmetry of x and y. Returns 1 in
  case of extended symmetry; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddExtSymmCheck(
  DdManager * table,
  int  x,
  int  y)
{
    DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;
    DdNode *one;
    int comple;		/* f0 is complemented */
    int notproj;	/* f is not a projection function */
    int arccount;	/* number of arcs from layer x to layer y */
    int TotalRefCount;	/* total reference count of layer y minus 1 */
    int counter;	/* number of nodes of layer x that are allowed */
    			/* to violate extended symmetry conditions */
    int arccounter;	/* number of arcs into layer y that are allowed */
			/* to come from layers other than x */
    int i;
    int xindex;
    int yindex;
    int res;
    int slots;
    DdNodePtr *list;
    DdNode *sentinel = &(table->sentinel);

    xindex = table->invperm[x];
    yindex = table->invperm[y];

    /* If the two variables do not interact, we do not want to merge them. */
    if (!cuddTestInteract(table,xindex,yindex))
	return(0);

#ifdef DD_DEBUG
    /* Checks that x and y do not contain just the projection functions.
    ** With the test on interaction, these test become redundant,
    ** because an isolated projection function does not interact with
    ** any other variable.
    */
    if (table->subtables[x].keys == 1) {
	assert(table->vars[xindex]->ref != 1);
    }
    if (table->subtables[y].keys == 1) {
	assert(table->vars[yindex]->ref != 1);
    }
#endif

#ifdef DD_STATS
    extsymmcalls++;
#endif

    arccount = 0;
    counter = (int) (table->subtables[x].keys *
	      (table->symmviolation/100.0) + 0.5);
    one = DD_ONE(table);

    slots = table->subtables[x].slots;
    list = table->subtables[x].nodelist;
    for (i = 0; i < slots; i++) {
	f = list[i];
	while (f != sentinel) {
	    /* Find f1, f0, f11, f10, f01, f00. */
	    f1 = cuddT(f);
	    f0 = Cudd_Regular(cuddE(f));
	    comple = Cudd_IsComplement(cuddE(f));
	    notproj = f1 != one || f0 != one || f->ref != (DdHalfWord) 1;
	    if (f1->index == yindex) {
		arccount++;
		f11 = cuddT(f1); f10 = cuddE(f1);
	    } else {
		if ((int) f0->index != yindex) {
		    /* If f is an isolated projection function it is
		    ** allowed to bypass layer y.
		    */
		    if (notproj) {
			if (counter == 0)
			    return(0);
			counter--; /* f bypasses layer y */
		    }
		}
		f11 = f10 = f1;
	    }
	    if ((int) f0->index == yindex) {
		arccount++;
		f01 = cuddT(f0); f00 = cuddE(f0);
	    } else {
		f01 = f00 = f0;
	    }
	    if (comple) {
		f01 = Cudd_Not(f01);
		f00 = Cudd_Not(f00);
	    }

	    /* Unless we are looking at a projection function
	    ** without external references except the one from the
	    ** table, we insist that f01 == f10 or f11 == f00
	    */
	    if (notproj) {
		if (f01 != f10 && f11 != f00) {
		    if (counter == 0)
			return(0);
		    counter--;
		}
	    }

	    f = f->next;
	} /* while */
    } /* for */

    /* Calculate the total reference counts of y */
    TotalRefCount = -1;	/* -1 for projection function */
    slots = table->subtables[y].slots;
    list = table->subtables[y].nodelist;
    for (i = 0; i < slots; i++) {
	f = list[i];
	while (f != sentinel) {
	    TotalRefCount += f->ref;
	    f = f->next;
	}
    }

    arccounter = (int) (table->subtables[y].keys *
		 (table->arcviolation/100.0) + 0.5);
    res = arccount >= TotalRefCount - arccounter;

#if defined(DD_DEBUG) && defined(DD_VERBOSE)
    if (res) {
	(void) fprintf(table->out,
		       "Found extended symmetry! x = %d\ty = %d\tPos(%d,%d)\n",
		       xindex,yindex,x,y);
    }
#endif

#ifdef DD_STATS
    if (res)
	extsymm++;
#endif
    return(res);

} /* end ddExtSymmCheck */


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

  Synopsis    [Checks for grouping of x and y.]

  Description [Checks for grouping of x and y. Returns 1 in
  case of grouping; 0 otherwise. This function is used for lazy sifting.]

  SideEffects [None]

******************************************************************************/
static int
ddVarGroupCheck(
  DdManager * table,
  int x,
  int y)
{
    int xindex = table->invperm[x];
    int yindex = table->invperm[y];

    if (Cudd_bddIsVarToBeUngrouped(table, xindex)) return(0);

    if (Cudd_bddReadPairIndex(table, xindex) == yindex) {
	if (ddIsVarHandled(table, xindex) ||
	    ddIsVarHandled(table, yindex)) {
	    if (Cudd_bddIsVarToBeGrouped(table, xindex) ||
		Cudd_bddIsVarToBeGrouped(table, yindex) ) {
		if (table->keys - table->isolated <= originalSize) {
		    return(1);
		}
	    }
	}
    }

    return(0);

} /* end of ddVarGroupCheck */


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

  Synopsis    [Sets a variable to already handled.]

  Description [Sets a variable to already handled. This function is used
  for lazy sifting.]

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
static int
ddSetVarHandled(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].varHandled = 1;
    return(1);

} /* end of ddSetVarHandled */


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

  Synopsis    [Resets a variable to be processed.]

  Description [Resets a variable to be processed. This function is used
  for lazy sifting.]

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
static int
ddResetVarHandled(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].varHandled = 0;
    return(1);

} /* end of ddResetVarHandled */


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

  Synopsis    [Checks whether a variables is already handled.]

  Description [Checks whether a variables is already handled. This
  function is used for lazy sifting.]

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
static int
ddIsVarHandled(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(-1);
    return dd->subtables[dd->perm[index]].varHandled;

} /* end of ddIsVarHandled */