cuddlinear.c

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

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

  FileName    [cuddLinear.c]

  PackageName [cudd]

  Synopsis    [Functions for DD reduction by linear transformations.]

  Description [ Internal procedures included in this module:
		<ul>
		<li> cuddLinearAndSifting()
		</ul>
	Static procedures included in this module:
		<ul>
		<li> ddLinearUniqueCompare()
		<li> ddLinearAndSiftingAux()
		<li> ddLinearAndSiftingUp()
		<li> ddLinearAndSiftingDown()
		<li> ddLinearAndSiftingBackward()
		<li> ddUndoMoves()
		<li> ddUpdateInteractionMatrix()
		<li> cuddLinearInPlace()
		<li> cuddInitLinear()
		<li> cuddResizeLinear()
		<li> cuddXorLinear()
		</ul>]

  Author      [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 CUDD_SWAP_MOVE 0
#define CUDD_LINEAR_TRANSFORM_MOVE 1
#define CUDD_INVERSE_TRANSFORM_MOVE 2
#if SIZEOF_LONG == 8
#define BPL 64
#define LOGBPL 6
#else
#define BPL 32
#define LOGBPL 5
#endif

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

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

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

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

static	int	*entry;

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

#ifdef DD_DEBUG
static	int	zero = 0;
#endif

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

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

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

static int ddLinearUniqueCompare ARGS((int *ptrX, int *ptrY));
static int ddLinearAndSiftingAux ARGS((DdManager *table, int x, int xLow, int xHigh));
static Move * ddLinearAndSiftingUp ARGS((DdManager *table, int y, int xLow, Move *prevMoves));
static Move * ddLinearAndSiftingDown ARGS((DdManager *table, int x, int xHigh, Move *prevMoves));
static int ddLinearAndSiftingBackward ARGS((DdManager *table, int size, Move *moves));
static Move* ddUndoMoves ARGS((DdManager *table, Move *moves));
static int cuddLinearInPlace ARGS((DdManager *table, int x, int y));
static void ddUpdateInteractionMatrix ARGS((DdManager *table, int xindex, int yindex));
static int cuddInitLinear ARGS((DdManager *table));
static int cuddResizeLinear ARGS((DdManager *table));
static void cuddXorLinear ARGS((DdManager *table, int x, int y));

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


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


/**Function********************************************************************
 
  Synopsis    [Prints the linear transform matrix.]

  Description [Prints the linear transform matrix. Returns 1 in case of
  success; 0 otherwise.]

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
int
Cudd_PrintLinear(
  DdManager * table)
{
    int i,j,k;
    int retval;
    int nvars = table->linearSize;
    int wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
    long word;

    for (i = 0; i < nvars; i++) {
	for (j = 0; j < wordsPerRow; j++) {
	    word = table->linear[i*wordsPerRow + j];
	    for (k = 0; k < BPL; k++) {
		retval = fprintf(table->out,"%ld",word & 1);
		if (retval == 0) return(0);
		word >>= 1;
	    }
	}
	retval = fprintf(table->out,"\n");
	if (retval == 0) return(0);
    }
    return(1);

} /* end of Cudd_PrintLinear */


/**Function********************************************************************
 
  Synopsis    [Reads an entry of the linear transform matrix.]

  Description [Reads an entry of the linear transform matrix.]

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
int
Cudd_ReadLinear(
  DdManager * table /* CUDD manager */,
  int  x /* row index */,
  int  y /* column index */)
{
    int nvars = table->size;
    int wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
    long word;
    int bit;
    int result;

    assert(table->size == table->linearSize);

    word = wordsPerRow * x + (y >> LOGBPL);
    bit  = y & (BPL-1);
    result = (int) ((table->linear[word] >> bit) & 1);
    return(result);

} /* end of Cudd_ReadLinear */


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


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

  Synopsis    [BDD reduction based on combination of sifting and linear
  transformations.]

  Description [BDD reduction based on combination of sifting and linear
  transformations.  Assumes that no dead nodes are present.
    <ol>
    <li> Order all the variables according to the number of entries
    in each unique table.
    <li> Sift the variable up and down, remembering each time the
    total size of the DD heap. At each position, linear transformation
    of the two adjacent variables is tried and is accepted if it reduces
    the size of the DD.
    <li> Select the best permutation.
    <li> Repeat 3 and 4 for all variables.
    </ol>
  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

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

#ifdef DD_STATS
    ddTotalNumberLinearTr = 0;
#endif

    size = table->size;

    var = NULL;
    entry = NULL;
    if (table->linear == NULL) {
	result = cuddInitLinear(table);
	if (result == 0) goto cuddLinearAndSiftingOutOfMem; 
#if 0
	(void) fprintf(table->out,"\n");
	result = Cudd_PrintLinear(table);
	if (result == 0) goto cuddLinearAndSiftingOutOfMem; 
#endif
    } else if (table->size != table->linearSize) {
	result = cuddResizeLinear(table);
	if (result == 0) goto cuddLinearAndSiftingOutOfMem; 
#if 0
	(void) fprintf(table->out,"\n");
	result = Cudd_PrintLinear(table);
	if (result == 0) goto cuddLinearAndSiftingOutOfMem; 
#endif
    }

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

    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 *))ddLinearUniqueCompare);

    /* Now sift. */
    for (i = 0; i < ddMin(table->siftMaxVar,size); i++) {
	x = table->perm[var[i]];
	if (x < lower || x > upper) continue;
#ifdef DD_STATS
	previousSize = table->keys - table->isolated;
#endif
	result = ddLinearAndSiftingAux(table,x,lower,upper);
	if (!result) goto cuddLinearAndSiftingOutOfMem; 
#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 */
	    (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i]);
	} else {
	    (void) fprintf(table->out,"=");
	}
	fflush(table->out);
#endif
#ifdef DD_DEBUG
	(void) Cudd_DebugCheck(table);
#endif
    }

    FREE(var);
    FREE(entry);

#ifdef DD_STATS
    (void) fprintf(table->out,"\n#:L_LINSIFT %8d: linear trans.",
		   ddTotalNumberLinearTr);
#endif

    return(1);

cuddLinearAndSiftingOutOfMem:

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

    return(0); 

} /* end of cuddLinearAndSifting */


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


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

  Synopsis    [Comparison function used by qsort.]

  Description [Comparison function used by qsort to order the
  variables according to the number of keys in the subtables.
  Returns the difference in number of keys between the two
  variables being compared.]

  SideEffects [None]

******************************************************************************/
static int
ddLinearUniqueCompare(
  int * ptrX,
  int * ptrY)
{
#if 0
    if (entry[*ptrY] == entry[*ptrX]) {
	return((*ptrX) - (*ptrY));
    }
#endif
    return(entry[*ptrY] - entry[*ptrX]);

} /* end of ddLinearUniqueCompare */


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

  Synopsis    [Given xLow <= x <= xHigh moves x up and down between the
  boundaries.]

  Description [Given xLow <= x <= xHigh moves x up and down between the
  boundaries. At each step a linear transformation is tried, and, if it
  decreases the size of the DD, it is accepted. Finds the best position
  and does the required changes.  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
ddLinearAndSiftingAux(
  DdManager * table,
  int  x,
  int  xLow,
  int  xHigh)
{

    Move	*move;
    Move	*moveUp;		/* list of up moves */
    Move	*moveDown;		/* list of down moves */
    int		initialSize;
    int		result;

    initialSize = table->keys - table->isolated;

    moveDown = NULL;
    moveUp = NULL;

    if (x == xLow) {
	moveDown = ddLinearAndSiftingDown(table,x,xHigh,NULL);
	/* At this point x --> xHigh unless bounding occurred. */
	if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
	/* Move backward and stop at best position. */	
	result = ddLinearAndSiftingBackward(table,initialSize,moveDown);
	if (!result) goto ddLinearAndSiftingAuxOutOfMem;

    } else if (x == xHigh) {
	moveUp = ddLinearAndSiftingUp(table,x,xLow,NULL);
	/* At this point x --> xLow unless bounding occurred. */
	if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
	/* Move backward and stop at best position. */
	result = ddLinearAndSiftingBackward(table,initialSize,moveUp);
	if (!result) goto ddLinearAndSiftingAuxOutOfMem;

    } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
	moveDown = ddLinearAndSiftingDown(table,x,xHigh,NULL);
	/* At this point x --> xHigh unless bounding occurred. */
	if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
	moveUp = ddUndoMoves(table,moveDown);
#ifdef DD_DEBUG
	assert(moveUp == NULL || moveUp->x == x);
#endif
	moveUp = ddLinearAndSiftingUp(table,x,xLow,moveUp);
	if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
	/* Move backward and stop at best position. */	
	result = ddLinearAndSiftingBackward(table,initialSize,moveUp);
	if (!result) goto ddLinearAndSiftingAuxOutOfMem;

    } else { /* must go up first: shorter */
	moveUp = ddLinearAndSiftingUp(table,x,xLow,NULL);
	/* At this point x --> xLow unless bounding occurred. */
	if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
	moveDown = ddUndoMoves(table,moveUp);
#ifdef DD_DEBUG
	assert(moveDown == NULL || moveDown->y == x);
#endif
	moveDown = ddLinearAndSiftingDown(table,x,xHigh,moveDown);
	if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
	/* Move backward and stop at best position. */	
	result = ddLinearAndSiftingBackward(table,initialSize,moveDown);
	if (!result) goto ddLinearAndSiftingAuxOutOfMem;
    }

    while (moveDown != NULL) {
	move = moveDown->next;
	cuddDeallocNode(table, (DdNode *) moveDown);
	moveDown = move;
    }
    while (moveUp != NULL) {
	move = moveUp->next;
	cuddDeallocNode(table, (DdNode *) moveUp);
	moveUp = move;
    }

    return(1);

ddLinearAndSiftingAuxOutOfMem:
    while (moveDown != NULL) {
	move = moveDown->next;
	cuddDeallocNode(table, (DdNode *) moveDown);
	moveDown = move;
    }