cuddsymmetry.c

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

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

  FileName    [cuddSymmetry.c]

  PackageName [cudd]

  Synopsis    [Functions for symmetry-based variable reordering.]

  Description [External procedures included in this file:
		<ul>
		<li> Cudd_SymmProfile()
		</ul>
	Internal procedures included in this module:
		<ul>
		<li> cuddSymmCheck()
		<li> cuddSymmSifting()
		<li> cuddSymmSiftingConv()
		</ul>
	Static procedures included in this module:
		<ul>
		<li> ddSymmUniqueCompare()
		<li> ddSymmSiftingAux()
		<li> ddSymmSiftingConvAux()
		<li> ddSymmSiftingUp()
		<li> ddSymmSiftingDown()
		<li> ddSymmGroupMove()
		<li> ddSymmGroupMoveBackward()
		<li> ddSymmSiftingBackward()
		<li> ddSymmSummary()
		</ul>]

  Author      [Shipra Panda, Fabio Somenzi]

  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 MV_OOM (Move *)1

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

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

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

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

static	int	*entry;

extern  int	ddTotalNumberSwapping;
#ifdef DD_STATS
extern	int	ddTotalNISwaps;
#endif

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

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

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

static int ddSymmUniqueCompare ARGS((int *ptrX, int *ptrY));
static int ddSymmSiftingAux ARGS((DdManager *table, int x, int xLow, int xHigh));
static int ddSymmSiftingConvAux ARGS((DdManager *table, int x, int xLow, int xHigh));
static Move * ddSymmSiftingUp ARGS((DdManager *table, int y, int xLow));
static Move * ddSymmSiftingDown ARGS((DdManager *table, int x, int xHigh));
static int ddSymmGroupMove ARGS((DdManager *table, int x, int y, Move **moves));
static int ddSymmGroupMoveBackward ARGS((DdManager *table, int x, int y));
static int ddSymmSiftingBackward ARGS((DdManager *table, Move *moves, int size));
static void ddSymmSummary ARGS((DdManager *table, int lower, int upper, int *symvars, int *symgroups));

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


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


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

  Synopsis    [Prints statistics on symmetric variables.]

  Description []

  SideEffects [None]

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

    for (i = lower; i <= upper; i++) {
	if (table->subtables[i].next != (unsigned) i) {
	    x = i;
	    (void) fprintf(table->out,"Group:");
	    do {
		(void) fprintf(table->out,"  %d",table->invperm[x]);
		TotalSymm++;
		gbot = x;
		x = table->subtables[x].next;
	    } while (x != i);
	    TotalSymmGroups++;
#ifdef DD_DEBUG
	    assert(table->subtables[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_SymmProfile */


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

******************************************************************************/
int
cuddSymmCheck(
  DdManager * table,
  int  x,
  int  y)
{
    DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;
    int comple;		/* f0 is complemented */
    int xsymmy;		/* x and y may be positively symmetric */
    int xsymmyp;	/* x and y may be negatively symmetric */
    int arccount;	/* number of arcs from layer x to layer y */
    int TotalRefCount;	/* total reference count of layer y minus 1 */
    int yindex;
    int i;
    DdNodePtr *list;
    int slots;
    DdNode *sentinel = &(table->sentinel);
#ifdef DD_DEBUG
    int xindex;
#endif

    /* Checks that x and y are not the projection functions.
    ** For x it is sufficient to check whether there is only one
    ** node; indeed, if there is one node, it is the projection function
    ** and it cannot point to y. Hence, if y isn't just the projection
    ** function, it has one arc coming from a layer different from x.
    */
    if (table->subtables[x].keys == 1) {
	return(0);
    }
    yindex = table->invperm[y];
    if (table->subtables[y].keys == 1) {
	if (table->vars[yindex]->ref == 1)
	    return(0);
    }

    xsymmy = xsymmyp = 1;
    arccount = 0;
    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));
	    if ((int) 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 (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1)
			return(0); /* 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);
	    }

	    if (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1) {
		xsymmy &= f01 == f10;
		xsymmyp &= f11 == f00;
		if ((xsymmy == 0) && (xsymmyp == 0))
		    return(0);
	    }

	    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;
	}
    }

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

    return(arccount == TotalRefCount);

} /* end of cuddSymmCheck */


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

  Synopsis    [Symmetric sifting algorithm.]

  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 DD 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     [cuddSymmSiftingConv]

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

    size = table->size;

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

    for (i = 0; i < size; i++) {
	x = table->perm[i];
	entry[i] = table->subtables[x].keys;
	var[i] = i;
    }

    qsort((void *)var,size,sizeof(int),(int (*)(const void *, const void *))ddSymmUniqueCompare);

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

    for (i = 0; i < ddMin(table->siftMaxVar,size); i++) {
	if (ddTotalNumberSwapping >= table->siftMaxSwap)
	    break;
	x = table->perm[var[i]];
#ifdef DD_STATS
	previousSize = table->keys - table->isolated;
#endif
	if (x < lower || x > upper) continue;
	if (table->subtables[x].next == (unsigned) x) {
	    result = ddSymmSiftingAux(table,x,lower,upper);
	    if (!result) goto ddSymmSiftingOutOfMem;
#ifdef DD_STATS
	    if (table->keys < (unsigned) previousSize + table->isolated) {
		(void) fprintf(table->out,"-");
	    } else if (table->keys > (unsigned) previousSize +
		       table->isolated) {
		(void) fprintf(table->out,"+"); /* should never happen */
	    } else {
		(void) fprintf(table->out,"=");
	    }
	    fflush(table->out);
#endif
	}
    }

    FREE(var);
    FREE(entry);

    ddSymmSummary(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",
		   symgroups);
#endif

    return(1+symvars);

ddSymmSiftingOutOfMem:

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

    return(0);

} /* end of cuddSymmSifting */


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

  Synopsis    [Symmetric sifting to convergence algorithm.]

  Description [Symmetric sifting to convergence 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 DD 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     [cuddSymmSifting]

******************************************************************************/
int
cuddSymmSiftingConv(
  DdManager * table,
  int  lower,
  int  upper)
{
    int		i;
    int		*var;
    int		size;
    int		x;
    int		result;
    int		symvars;