cuddzddsymm.c

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

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

  FileName    [cuddZddSymm.c]

  PackageName [cudd]

  Synopsis    [Functions for symmetry-based ZDD variable reordering.]

  Description [External procedures included in this module:
		    <ul>
		    <li> Cudd_zddSymmProfile()
		    </ul>
	       Internal procedures included in this module:
		    <ul>
		    <li> cuddZddSymmCheck()
		    <li> cuddZddSymmSifting()
		    <li> cuddZddSymmSiftingConv()
		    </ul>
	       Static procedures included in this module:
		    <ul>
		    <li> cuddZddUniqueCompare()
		    <li> cuddZddSymmSiftingAux()
		    <li> cuddZddSymmSiftingConvAux()
		    <li> cuddZddSymmSifting_up()
		    <li> cuddZddSymmSifting_down()
		    <li> zdd_group_move()
		    <li> cuddZddSymmSiftingBackward()
		    <li> zdd_group_move_backward()
		    </ul>
	      ]

  SeeAlso     [cuddSymmetry.c]

  Author      [Hyong-Kyoon Shin, In-Ho Moon]

  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                                                     */
/*---------------------------------------------------------------------------*/

#define ZDD_MV_OOM (Move *)1

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

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

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

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

extern int   	*zdd_entry;

extern int	zddTotalNumberSwapping;

static DdNode	*empty;

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


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

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

static int cuddZddSymmSiftingAux ARGS((DdManager *table, int x, int x_low, int x_high));
static int cuddZddSymmSiftingConvAux ARGS((DdManager *table, int x, int x_low, int x_high));
static Move * cuddZddSymmSifting_up ARGS((DdManager *table, int x, int x_low, int initial_size));
static Move * cuddZddSymmSifting_down ARGS((DdManager *table, int x, int x_high, int initial_size));
static int cuddZddSymmSiftingBackward ARGS((DdManager *table, Move *moves, int size));
static int zdd_group_move ARGS((DdManager *table, int x, int y, Move **moves));
static int zdd_group_move_backward ARGS((DdManager *table, int x, int y));
static void cuddZddSymmSummary ARGS((DdManager *table, int lower, int upper, int *symvars, int *symgroups));

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


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


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

  Synopsis [Prints statistics on symmetric ZDD variables.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void
Cudd_zddSymmProfile(
  DdManager * table,
  int  lower,
  int  upper)
{
    int		i, x, gbot;
    int		TotalSymm = 0;
    int 	TotalSymmGroups = 0;
    int 	nvars;

    nvars = table->sizeZ;

    for (i = lower; i < upper; i++) {
	if (table->subtableZ[i].next != (unsigned) i) {
	    x = i;
	    (void) fprintf(table->out,"Group:");
	    do {
		(void) fprintf(table->out,"  %d", table->invpermZ[x]);
		TotalSymm++;
		gbot = x;
		x = table->subtableZ[x].next;
	    } while (x != i);
	    TotalSymmGroups++;
#ifdef DD_DEBUG
	    assert(table->subtableZ[gbot].next == (unsigned) i);
#endif
	    i = gbot;
	    (void) fprintf(table->out,"\n");
	}
    }
    (void) fprintf(table->out,"Total Symmetric = %d\n", TotalSymm);
    (void) fprintf(table->out,"Total Groups = %d\n", TotalSymmGroups);

} /* end of Cudd_zddSymmProfile */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


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

  Synopsis [Checks for symmetry of x and y.]

  Description [Checks for symmetry of x and y. Ignores projection
  functions, unless they are isolated. Returns 1 in case of
  symmetry; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
cuddZddSymmCheck(
  DdManager * table,
  int  x,
  int  y)
{
    int		i;
    DdNode	*f, *f0, *f1, *f01, *f00, *f11, *f10;
    int		yindex;
    int 	xsymmy = 1;
    int		xsymmyp = 1;
    int 	arccount = 0;
    int 	TotalRefCount = 0;
    int 	symm_found;

    empty = table->zero;

    yindex = table->invpermZ[y];
    for (i = table->subtableZ[x].slots - 1; i >= 0; i--) {
	f = table->subtableZ[x].nodelist[i];
	while (f != NULL) {
	    /* Find f1, f0, f11, f10, f01, f00 */
	    f1 = cuddT(f);
	    f0 = cuddE(f);
	    if ((int) f1->index == yindex) {
		f11 = cuddT(f1);
		f10 = cuddE(f1);
		if (f10 != empty)
		    arccount++;
	    } else {
		if ((int) f0->index != yindex) {
		    return(0); /* f bypasses layer y */
		}
		f11 = empty;
		f10 = f1;
	    }
	    if ((int) f0->index == yindex) {
		f01 = cuddT(f0);
		f00 = cuddE(f0);
		if (f00 != empty)
		    arccount++;
	    } else {
		f01 = empty;
		f00 = f0;
	    }
	    if (f01 != f10)
		xsymmy = 0;
	    if (f11 != f00)
		xsymmyp = 0;
	    if ((xsymmy == 0) && (xsymmyp == 0))
		return(0);

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

    /* Calculate the total reference counts of y
    ** whose else arc is not empty.
    */
    for (i = table->subtableZ[y].slots - 1; i >= 0; i--) {
	f = table->subtableZ[y].nodelist[i];
	while (f != NIL(DdNode)) {
	    if (cuddE(f) != empty)
		TotalRefCount += f->ref;
	    f = f->next;
	}
    }

    symm_found = (arccount == TotalRefCount);
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
    if (symm_found) {
	int xindex = table->invpermZ[x];
	(void) fprintf(table->out,
		       "Found symmetry! x =%d\ty = %d\tPos(%d,%d)\n",
		       xindex,yindex,x,y);
    }
#endif

    return(symm_found);

} /* end cuddZddSymmCheck */


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

  Synopsis [Symmetric sifting algorithm for ZDDs.]

  Description [Symmetric sifting algorithm.
  Assumes that no dead nodes are present.
    <ol>
    <li> Order all the variables according to the number of entries in
    each unique subtable.
    <li> Sift the variable up and down, remembering each time the total
    size of the ZDD heap and grouping variables that are symmetric.
    <li> Select the best permutation.
    <li> Repeat 3 and 4 for all variables.
    </ol>
  Returns 1 plus the number of symmetric variables if successful; 0
  otherwise.]

  SideEffects [None]

  SeeAlso     [cuddZddSymmSiftingConv]

******************************************************************************/
int
cuddZddSymmSifting(
  DdManager * table,
  int  lower,
  int  upper)
{
    int		i;
    int		*var;
    int		nvars;
    int		x;
    int		result;
    int		symvars;
    int		symgroups;
    int		iteration;
#ifdef DD_STATS
    int		previousSize;
#endif

    nvars = table->sizeZ;

    /* Find order in which to sift variables. */
    var = NULL;
    zdd_entry = ALLOC(int, nvars);
    if (zdd_entry == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	goto cuddZddSymmSiftingOutOfMem;
    }
    var = ALLOC(int, nvars);
    if (var == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	goto cuddZddSymmSiftingOutOfMem;
    }

    for (i = 0; i < nvars; i++) {
	x = table->permZ[i];
	zdd_entry[i] = table->subtableZ[x].keys;
	var[i] = i;
    }

    qsort((void *)var, nvars, sizeof(int), (int (*)(const void *, const void *))cuddZddUniqueCompare);

    /* Initialize the symmetry of each subtable to itself. */
    for (i = lower; i <= upper; i++)
	table->subtableZ[i].next = i;

    iteration = ddMin(table->siftMaxVar, nvars);
    for (i = 0; i < iteration; i++) {
	if (zddTotalNumberSwapping >= table->siftMaxSwap)
	    break;
	x = table->permZ[var[i]];
#ifdef DD_STATS
	previousSize = table->keysZ;
#endif
	if (x < lower || x > upper) continue;
	if (table->subtableZ[x].next == (unsigned) x) {
	    result = cuddZddSymmSiftingAux(table, x, lower, upper);
	    if (!result)
		goto cuddZddSymmSiftingOutOfMem;
#ifdef DD_STATS
	    if (table->keysZ < (unsigned) previousSize) {
		(void) fprintf(table->out,"-");
	    } else if (table->keysZ > (unsigned) previousSize) {
		(void) fprintf(table->out,"+");
#ifdef DD_VERBOSE
		(void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]);
#endif
	    } else {
		(void) fprintf(table->out,"=");
	    }
	    fflush(table->out);
#endif
	}
    }

    FREE(var);
    FREE(zdd_entry);

    cuddZddSymmSummary(table, lower, upper, &symvars, &symgroups);

#ifdef DD_STATS
    (void) fprintf(table->out,"\n#:S_SIFTING %8d: symmetric variables\n",symvars);
    (void) fprintf(table->out,"#:G_SIFTING %8d: symmetric groups\n",symgroups);
#endif

    return(1+symvars);

cuddZddSymmSiftingOutOfMem:

    if (zdd_entry != NULL)
	FREE(zdd_entry);
    if (var != NULL)
	FREE(var);

    return(0);

} /* end of cuddZddSymmSifting */


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

  Synopsis [Symmetric sifting to convergence algorithm for ZDDs.]

  Description [Symmetric sifting to convergence algorithm for ZDDs.
  Assumes that no dead nodes are present.
    <ol>
    <li> Order all the variables according to the number of entries in
    each unique subtable.
    <li> Sift the variable up and down, remembering each time the total
    size of the ZDD heap and grouping variables that are symmetric.
    <li> Select the best permutation.
    <li> Repeat 3 and 4 for all variables.
    <li> Repeat 1-4 until no further improvement.
    </ol>
  Returns 1 plus the number of symmetric variables if successful; 0
  otherwise.]

  SideEffects [None]

  SeeAlso     [cuddZddSymmSifting]

******************************************************************************/
int
cuddZddSymmSiftingConv(
  DdManager * table,
  int  lower,
  int  upper)
{
    int		i;
    int		*var;
    int		nvars;
    int		initialSize;
    int		x;
    int		result;
    int		symvars;
    int		symgroups;
    int		classes;
    int		iteration;
#ifdef DD_STATS
    int         previousSize;
#endif

    initialSize = table->keysZ;

    nvars = table->sizeZ;

    /* Find order in which to sift variables. */
    var = NULL;
    zdd_entry = ALLOC(int, nvars);
    if (zdd_entry == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	goto cuddZddSymmSiftingConvOutOfMem;
    }
    var = ALLOC(int, nvars);
    if (var == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	goto cuddZddSymmSiftingConvOutOfMem;
    }

    for (i = 0; i < nvars; i++) {
	x = table->permZ[i];
	zdd_entry[i] = table->subtableZ[x].keys;
	var[i] = i;
    }

    qsort((void *)var, nvars, sizeof(int), (int (*)(const void *, const void *))cuddZddUniqueCompare);

    /* Initialize the symmetry of each subtable to itself
    ** for first pass of converging symmetric sifting.
    */
    for (i = lower; i <= upper; i++)
	table->subtableZ[i].next = i;

    iteration = ddMin(table->siftMaxVar, table->sizeZ);
    for (i = 0; i < iteration; i++) {
	if (zddTotalNumberSwapping >= table->siftMaxSwap)
	    break;
	x = table->permZ[var[i]];
	if (x < lower || x > upper) continue;
	/* Only sift if not in symmetry group already. */
	if (table->subtableZ[x].next == (unsigned) x) {
#ifdef DD_STATS
	    previousSize = table->keysZ;
#endif
	    result = cuddZddSymmSiftingAux(table, x, lower, upper);
	    if (!result)
		goto cuddZddSymmSiftingConvOutOfMem;
#ifdef DD_STATS
	    if (table->keysZ < (unsigned) previousSize) {
		(void) fprintf(table->out,"-");
	    } else if (table->keysZ > (unsigned) previousSize) {
		(void) fprintf(table->out,"+");
#ifdef DD_VERBOSE
		(void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]);
#endif
	    } else {
		(void) fprintf(table->out,"=");
	    }
	    fflush(table->out);
#endif
	}
    }

    /* Sifting now until convergence. */
    while ((unsigned) initialSize > table->keysZ) {
	initialSize = table->keysZ;
#ifdef DD_STATS
	(void) fprintf(table->out,"\n");
#endif
	/* Here we consider only one representative for each symmetry class. */
	for (x = lower, classes = 0; x <= upper; x++, classes++) {
	    while ((unsigned) x < table->subtableZ[x].next)
		x = table->subtableZ[x].next;
	    /* Here x is the largest index in a group.
	    ** Groups consists of adjacent variables.
	    ** Hence, the next increment of x will move it to a new group.
	    */
	    i = table->invpermZ[x];
	    zdd_entry[i] = table->subtableZ[x].keys;
	    var[classes] = i;
	}

	qsort((void *)var,classes,sizeof(int),(int (*)(const void *, const void *))cuddZddUniqueCompare);

	/* Now sift. */
	iteration = ddMin(table->siftMaxVar, nvars);
	for (i = 0; i < iteration; i++) {
	    if (zddTotalNumberSwapping >= table->siftMaxSwap)
		break;
	    x = table->permZ[var[i]];
	    if ((unsigned) x >= table->subtableZ[x].next) {
#ifdef DD_STATS
		previousSize = table->keysZ;
#endif
		result = cuddZddSymmSiftingConvAux(table, x, lower, upper);
		if (!result)
		    goto cuddZddSymmSiftingConvOutOfMem;
#ifdef DD_STATS
		if (table->keysZ < (unsigned) previousSize) {
		    (void) fprintf(table->out,"-");
		} else if (table->keysZ > (unsigned) previousSize) {
		    (void) fprintf(table->out,"+");
#ifdef DD_VERBOSE
		(void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]);
#endif
		} else {
		    (void) fprintf(table->out,"=");
		}
		fflush(table->out);
#endif
	    }
	} /* for */
    }

    cuddZddSymmSummary(table, lower, upper, &symvars, &symgroups);

#ifdef DD_STATS
    (void) fprintf(table->out,"\n#:S_SIFTING %8d: symmetric variables\n",
		   symvars);
    (void) fprintf(table->out,"#:G_SIFTING %8d: symmetric groups\n",
		   symgroups);
#endif

    FREE(var);
    FREE(zdd_entry);

    return(1+symvars);

cuddZddSymmSiftingConvOutOfMem:

    if (zdd_entry != NULL)
	FREE(zdd_entry);
    if (var != NULL)
	FREE(var);

    return(0);

} /* end of cuddZddSymmSiftingConv */


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


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

  Synopsis [Given x_low <= x <= x_high moves x up and down between the
  boundaries.]