extrabddmisc.c

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

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

  FileName    [extraBddMisc.c]

  PackageName [extra]

  Synopsis    [Various BDD manipulating procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - February 1, 2003.]

  Revision    [$Id: extraBddMisc.c,v 1.2 2003/05/27 23:14:38 alanmi Exp $]

***********************************************************************/

#include "util.h"
#include "cuddInt.h"
#include "time.h"
#include "extra.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

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

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

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

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


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

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/
static void ddProfileNode( DdManager * dd, DdNode * F, int * Profile, st_table * Visited );
static void ddProfileEdge( DdManager * dd, DdNode * F, int * Profile, st_table * Visited );
static DdNode * extraBddPermuteToAdd( DdManager * dd, DdNode * bFunc, int * Permute, st_table * Visited, DdNode ** paVars );
static DdNode * cuddBddPermuteRecur ARGS( ( DdManager * manager, DdHashTable * table, DdNode * node, int *permut ) );

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


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

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

  Synopsis    [Returns 1 if the BDD has at least one complemented edge.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int Extra_WithComplementedEdges( DdNode * bFunc )
{
	if ( Cudd_IsComplement(bFunc) )
		return 1;
	if ( cuddIsConstant(bFunc) )
		return 0;
	if ( Extra_WithComplementedEdges( cuddE(bFunc) ) )
		return 1;
	return Extra_WithComplementedEdges( cuddT(bFunc) );
}

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

  Synopsis    [Remaps the function to depend on the topmost variables on the manager.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_bddRemapUp(
  DdManager * dd,
  DdNode * bF )
{
	static int Permute[MAXINPUTS];
	DdNode * bSupp, * bTemp, * bRes;
	int Counter;

	// get support
	bSupp = Cudd_Support( dd, bF );    Cudd_Ref( bSupp );

	// create the variable map
	// to remap the DD into the upper part of the manager
	Counter = 0;
	for ( bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp) )
		Permute[bTemp->index] = dd->invperm[Counter++];

	// transfer the BDD and remap it
	bRes = Cudd_bddPermute( dd, bF, Permute );  Cudd_Ref( bRes );

	// remove support
	Cudd_RecursiveDeref( dd, bSupp );

	// return
	Cudd_Deref( bRes );
	return bRes;
}


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

  Synopsis    [Find any cube belonging to the on-set of the function.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode *  Extra_bddFindOneCube( DdManager * dd, DdNode * bF )
{
	static char s_Temp[MAXINPUTS];
	DdNode * bCube, * bTemp;
	int v;

	// get the vector of variables in the cube
	Cudd_bddPickOneCube( dd, bF, s_Temp );

	// start the cube
	bCube = b1; Cudd_Ref( bCube );

	for ( v = 0; v < dd->size; v++ )
		if ( s_Temp[v] == 0 )
		{
//			Cube &= !s_XVars[v];
			bCube = Cudd_bddAnd( dd, bTemp = bCube, Cudd_Not(dd->vars[v]) ); Cudd_Ref( bCube );
			Cudd_RecursiveDeref( dd, bTemp );
		}
		else if ( s_Temp[v] == 1 )
		{
//			Cube &=  s_XVars[v];
			bCube = Cudd_bddAnd( dd, bTemp = bCube,          dd->vars[v]  ); Cudd_Ref( bCube );
			Cudd_RecursiveDeref( dd, bTemp );
		}
	Cudd_Deref(bCube);
	return bCube;
}


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

  Synopsis    [Returns one minterm contained in the given BDD.]

  Description [This function differs from Cudd_bddPickOneMinterm in that it 
  returns the minterm with the smallest bits-to-integer value.]

  SideEffects []

******************************************************************************/
DdNode * Extra_bddGetOneMinterm( DdManager * dd, DdNode * bFunc, DdNode * bSupp )
{
	DdNode * bSuppReal, * bSuppCube, * bSuppDiff, * bSuppTemp;
	DdNode * bCube, * bTemp;

	// make sure the support of bFunc is contained in bSupp
	bSuppReal = Cudd_Support( dd, bFunc );                      Cudd_Ref( bSuppReal );
	bTemp     = Cudd_bddExistAbstract( dd, bSuppReal, bSupp );  Cudd_Ref( bTemp );
	if ( bTemp != b1 )
	{
		printf( "Extra_bddGetOneMinterm(): Support is not valid!\n" );
		fflush( stdout );
		assert(0);
	}
	Cudd_RecursiveDeref( dd, bTemp );
	Cudd_RecursiveDeref( dd, bSuppReal );

	// get one cube
	bCube     = Extra_bddGetOneCube( dd, bFunc );               Cudd_Ref( bCube );
	// find the cube support
	bSuppCube = Cudd_Support( dd, bCube );                      Cudd_Ref( bSuppCube );
	// get the support difference (vars in bSupp and not in bCube )
	bSuppDiff = Cudd_bddExistAbstract( dd, bSupp, bSuppCube );  Cudd_Ref( bSuppDiff );
	// these vars should be added to the cube in the negative polarity
	for ( bSuppTemp = bSuppDiff; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
	{
		bCube = Cudd_bddAnd( dd, bTemp = bCube, Cudd_Not(dd->vars[bSuppTemp->index]) );    Cudd_Ref( bCube );
		Cudd_RecursiveDeref( dd, bTemp );
	}
	Cudd_RecursiveDeref( dd, bSuppCube );
	Cudd_RecursiveDeref( dd, bSuppDiff );
	Cudd_Deref(bCube);
	return bCube;
}

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

  Synopsis    [Returns one cube contained in the given BDD.]

  Description [This function returns the cube with the smallest 
  bits-to-integer value.]

  SideEffects []

******************************************************************************/
DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc )
{
	DdNode * bFuncR, * bFunc0, * bFunc1;
	DdNode * bRes0,  * bRes1,  * bRes;

	bFuncR = Cudd_Regular(bFunc);
	if ( cuddIsConstant(bFuncR) )
		return bFunc;

	// cofactor
	if ( Cudd_IsComplement(bFunc) )
	{
		bFunc0 = Cudd_Not( cuddE(bFuncR) );
		bFunc1 = Cudd_Not( cuddT(bFuncR) );
	}
	else
	{
		bFunc0 = cuddE(bFuncR);
		bFunc1 = cuddT(bFuncR);
	}

	// try to find the cube with the negative literal
	bRes0 = Extra_bddGetOneCube( dd, bFunc0 );  Cudd_Ref( bRes0 );

	if ( bRes0 != b0 )
	{
		bRes = Cudd_bddAnd( dd, bRes0, Cudd_Not(dd->vars[bFuncR->index]) ); Cudd_Ref( bRes );
		Cudd_RecursiveDeref( dd, bRes0 );
	}
	else
	{
		Cudd_RecursiveDeref( dd, bRes0 );
		// try to find the cube with the positive literal
		bRes1 = Extra_bddGetOneCube( dd, bFunc1 );  Cudd_Ref( bRes1 );
		assert( bRes1 != b0 );
		bRes = Cudd_bddAnd( dd, bRes1, dd->vars[bFuncR->index] ); Cudd_Ref( bRes );
		Cudd_RecursiveDeref( dd, bRes1 );
	}

	Cudd_Deref( bRes );
	return bRes;
}

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

  Synopsis    [Find any minterm belonging to the on-set of the function.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode *  Extra_bddFindOneMinterm( DdManager * dd, DdNode * bF, int nVars )
{
	static char s_Temp[MAXINPUTS];
	DdNode * bCube, * bTemp;
	int v;

	// get the vector of variables in the cube
	Cudd_bddPickOneCube( dd, bF, s_Temp );

	// start the cube
	bCube = b1; Cudd_Ref( bCube );

	assert( nVars <= dd->size );
	for ( v = 0; v < nVars; v++ )
		if ( s_Temp[v] == 1 )
		{
//			Cube &=  s_XVars[v];
			bCube = Cudd_bddAnd( dd, bTemp = bCube,          dd->vars[v]  ); Cudd_Ref( bCube );
			Cudd_RecursiveDeref( dd, bTemp );
		}
		else // if ( s_Temp[v] == 0 )
		{
//			Cube &= !s_XVars[v];
			bCube = Cudd_bddAnd( dd, bTemp = bCube, Cudd_Not(dd->vars[v]) ); Cudd_Ref( bCube );
			Cudd_RecursiveDeref( dd, bTemp );
		}
	Cudd_Deref(bCube);
	return bCube;
}


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

  Synopsis    [Generates a random function.]

  Description [Given the number of variables n and the density of on-set minterms,
  this function generates a random function and returns its BDD. The variables are
  taken from the first variables of the DD manager. Returns NULL if density is 
  less than 0.0 or more than 1.0.]

  SideEffects [Allocates new BDD variables if their current number is less than n.]

  SeeAlso     []

******************************************************************************/
DdNode* Extra_bddRandomFunc( 
  DdManager * dd,   /* the DD manager */
  int n,            /* the number of variables */
  double d)         /* average density of on-set minterms */
{
	DdNode *Result, *TempCube, *Aux, **VarBdds;
	int c, v, Limit, *VarValues;
	int nMinterms;

	/* sanity check the parameters */
	if ( n <= 0 || d < 0.0 || d > 1.0 )
		return NULL;

	/* allocate temporary storage for variables and variable values */
	VarBdds = ALLOC( DdNode*, n );
	VarValues = ALLOC( int, n );
	if (VarBdds == NULL || VarValues == NULL) 
	{
		dd->errorCode = CUDD_MEMORY_OUT;
		return NULL;
	}
	/* set elementary BDDs corresponding to variables */
	for ( v = 0; v < n; v++ )
		VarBdds[v] = Cudd_bddIthVar( dd, v );

	/* start the function */
	Result = Cudd_Not( dd->one );
	Cudd_Ref( Result );

	/* seed random number generator */
	Cudd_Srandom( time(NULL) );
//	Cudd_Srandom( 4 );
	/* determine the number of minterms */
	nMinterms = (int)(d*(1<<n));
	/* determine the limit below which var belongs to the minterm */
	Limit = (int)(0.5 * 2147483561.0);

	/* add minterms one by one */
	for ( c = 0; c < nMinterms; c++ )
	{
		for ( v = 0; v < n; v++ )
			if ( Cudd_Random() <= Limit )
				VarValues[v] = 1;
			else
				VarValues[v] = 0;

		TempCube = Cudd_bddComputeCube( dd, VarBdds, VarValues, n );
		Cudd_Ref( TempCube );

		/* make sure that this combination is not already in the set */
		if ( c )
		{ /* at least one combination is already included */

			Aux = Cudd_bddAnd( dd, Result, TempCube );
			Cudd_Ref( Aux );
			if ( Aux != Cudd_Not( dd->one ) )
			{
				Cudd_RecursiveDeref( dd, Aux );
				Cudd_RecursiveDeref( dd, TempCube );
				c--;
				continue;
			}
			else 
			{ /* Aux is the same node as Result */
				Cudd_Deref( Aux );
			}
		}

		Result = Cudd_bddOr( dd, Aux = Result, TempCube );
		Cudd_Ref( Result );
		Cudd_RecursiveDeref( dd, Aux );
		Cudd_RecursiveDeref( dd, TempCube );
	}

	FREE( VarValues );
	FREE( VarBdds );
	Cudd_Deref( Result );
	return Result;

} /* end of Extra_bddRandomFunc */


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

  Synopsis    [Generates a random function.]

  Description [Given the number of variables n and the density of on-set minterms,
  this function generates a random function and returns its BDD. The variables are
  taken from the first variables of the DD manager. Returns NULL if density is 
  less than 0.0 or more than 1.0.]

  SideEffects [Allocates new BDD variables if their current number is less than n.]

  SeeAlso     []

******************************************************************************/
DdNode * Extra_bddGetRandomTransform( DdManager * dd, DdNode ** XVars, DdNode ** YVars, int nVars )
{
	DdNode * bRes, * bTemp, * bCubeX, * bCubeY, * bCube;
	// go through all the minterms
	int m, mRand;
	int nMints = (1<<nVars);
	int * fMintUsed = (int*)malloc( nMints * sizeof(int) );

	assert( nVars <= 10 );

	// set all minterms to be unused
	for ( m = 0; m < nMints; m++ )
		fMintUsed[m] = 0;

	bRes = b0; Cudd_Ref( bRes );
	for ( m = 0; m < nMints; m++ )
	{
		// get a random minterm that is not used
		mRand = Cudd_Random() % nMints;
		while ( fMintUsed[mRand] )
			mRand = (mRand+1) % nMints;
		// set as used
		fMintUsed[mRand] = 1;

		// create the cubes
		bCubeX = Extra_bddBitsToCube(dd,m,nVars,XVars);      Cudd_Ref( bCubeX );
		bCubeY = Extra_bddBitsToCube(dd,mRand,nVars,YVars);  Cudd_Ref( bCubeY );

		bCube =  Cudd_bddAnd(dd,bCubeX,bCubeY);      Cudd_Ref( bCube );
		Cudd_RecursiveDeref( dd, bCubeX );
		Cudd_RecursiveDeref( dd, bCubeY );

		bRes  = Cudd_bddOr( dd, bTemp = bRes, bCube);Cudd_Ref( bRes );
		Cudd_RecursiveDeref( dd, bTemp );
		Cudd_RecursiveDeref( dd, bCube );
	}

	free( fMintUsed );
	Cudd_Deref( bRes );
	return bRes;
}  /* end of Extra_bddGetRandomTransform */


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

  Synopsis    [Computes the cube of BDD variables corresponding to bits it the bit-code]

  Description [Returns a bdd composed of elementary bdds found in array BddVars[] such 
  that the bdd vars encode the number Value of bit length CodeWidth (most significant bit 
  is encoded with the first bdd variable). If the variables BddVars are not specified,
  takes the first CodeWidth variables of the manager]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars )
{
	int z;
	DdNode * bTemp, * bVar, * bVarBdd, * bResult;

	bResult = b1; 	Cudd_Ref( bResult );
	for ( z = 0; z < CodeWidth; z++ )
	{
		bVarBdd = (pbVars)? pbVars[z]: dd->vars[z];
		bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (CodeWidth-1-z)))==0 );
		bResult = Cudd_bddAnd( dd, bTemp = bResult, bVar ); 	Cudd_Ref( bResult );
		Cudd_RecursiveDeref( dd, bTemp );
	}
	Cudd_Deref( bResult );

	return bResult;
}  /* end of Extra_bddBitsToCube */


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

  Synopsis    [Computes the positive polarty cube composed of the first vars in the array.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars )
{
	DdNode * bRes;
	DdNode * bTemp;
	int i;

	bRes = b1; Cudd_Ref( bRes );
	for ( i = 0; i < nVars; i++ )
	{
		bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] );  Cudd_Ref( bRes );
		Cudd_RecursiveDeref( dd, bTemp );
	}

	Cudd_Deref( bRes );
	return bRes;
}

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

  Synopsis    [Visualize the BDD.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void Extra_bddShow( DdManager * dd, DdNode * bFunc )
{ 
    FILE * pFileDot = fopen( "bdd.dot", "w" );
    Cudd_DumpDot( dd, 1, &bFunc, NULL, NULL, pFileDot );
    fclose( pFileDot );
}

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

  Synopsis    [Visualize the BDD.]

  Description []

  SideEffects []

  SeeAlso     []