extraaddspectra.c

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

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

  FileName    [extraAddSpectra.c]

  PackageName [extra]

  Synopsis    [Computation of Walsh, Haar, and Reed-Muller spectra from 
  the BDD. The theory underlying the current implementation is developed in 
  M.A.Thornton, D.M.Miller, R.Drechsler, "Transformations amongst the Walsh, 
  Haar, Arithmetic and Reed-Muller Spectral Domains". Proc. of RM-01.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

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

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

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

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

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

static int s_CacheHit;
static int s_CacheMiss;

static long s_TimeLimit;

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

#define DD_ADD_UPDATE_ZERO_CUBE_TAG	  0x2e /* former DD_BDD_COMPOSE_RECUR_TAG */
#define DD_ADD_WALSH_SUBSET_TAG   	  0x6a /* former DD_BDD_ITE_CONSTANT_TAG */
#define DD_ADD_HAAR_INVERSE_TAG       0x06 /* former DD_BDD_AND_ABSTRACT_TAG */
#define DD_ADD_ITE_GENERAL_TAG 	      0x0a /* former DD_BDD_XOR_EXIST_ABSTRACT_TAG */
// there is no harm in reusing these tags, because originally they are supposed
// to work for BDDs; even if used in their original role in the same BDD manager,
// there is no risk of cache collision, because in this file they are used for ADDs, 
// which are topologically different from BDDs


/**Automaticstart*************************************************************/

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

/**Automaticend***************************************************************/
static DdNode * extraCachingCube( DdManager * dd, DdNode * bVarsAll, DdNode * bVars );

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

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

  Synopsis    [Returns the ADD of the Reed-Muller spectrum of the function represented as a BDD.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_bddWalsh( 
  DdManager * dd,    /* the manager */
  DdNode * bFunc,    /* the function whose spectrum is being computed */
  DdNode * bVars)    /* the variables on which the function depends */
{
    DdNode	*aRes;

	s_TimeLimit = (int)(1.0 /* time in secs */ * (float)(CLOCKS_PER_SEC)) + clock();

    do 
	{
		dd->reordered = 0;
		aRes = extraBddWalsh(dd, bFunc, bVars);
		if ( clock() > s_TimeLimit )
			break;
    } 
	while (dd->reordered == 1);
    return(aRes);

} /* end of Extra_bddWalsh */


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

  Synopsis    [Returns the ADD of the Reed-Muller spectrum of the function represented as a BDD.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_bddReedMuller( 
  DdManager * dd,    /* the manager */
  DdNode * bFunc,    /* the function whose spectrum is being computed */
  DdNode * bVars)    /* the variables on which the function depends */
{
    DdNode	*aRes;
    do 
	{
		dd->reordered = 0;
		aRes = extraBddReedMuller(dd, bFunc, bVars);
    } 
	while (dd->reordered == 1);
    return(aRes);

} /* end of Extra_bddReedMuller */


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

  Synopsis    [Returns the ADD of the Haar spectrum of the function represented as a BDD.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_bddHaar( 
  DdManager * dd,    /* the manager */
  DdNode * bFunc,    /* the function whose spectrum is being computed */
  DdNode * bVars)    /* the variables on which the function depends */
{
    DdNode	*aRes;
    do 
	{
		dd->reordered = 0;
		aRes = extraBddHaar(dd, bFunc, bVars);
    } 
	while (dd->reordered == 1);
    return(aRes);

} /* end of Extra_bddHaar */

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

  Synopsis    [Takes the ADD of Haar and returns the ADD of inverse Haar.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_bddHaarInverse( 
  DdManager * dd,    /* the manager */
  DdNode * aFunc,    /* the Haar that should be inverted */
  DdNode * bVars)    /* the variables on which the function depends */
{
	static int Vars[MAXINPUTS];
	static int InverseMap[MAXINPUTS];
	int k, nVars = 0;
	DdNode * bTemp;
	DdNode * aStepFirst;
    DdNode * aRes;

	/////////////////////////////////////////////////////////
	// create the array of variables in the set bVars
	for ( bTemp = bVars; bTemp != b1; bTemp = cuddT(bTemp) )
		Vars[nVars++] = bTemp->index;

	// compute the inverse mapping of variable into the one that 
	// has the same distance from the bottom as this one from the top
	k = 0;
	for ( bTemp = bVars; bTemp != b1; bTemp = cuddT(bTemp), k++ )
		InverseMap[bTemp->index] = Vars[nVars-1-k];
	/////////////////////////////////////////////////////////

	// get the constant ADD representing the first step
	aStepFirst = cuddUniqueConst( dd, 0.0 ); Cudd_Ref(aStepFirst);

    do 
	{
		dd->reordered = 0;
		aRes = extraBddHaarInverse(dd, aFunc, aStepFirst, bVars, bVars, nVars, InverseMap);
    } 
	while (dd->reordered == 1);

	Cudd_RecursiveDeref( dd, aStepFirst );
    return(aRes);

} /* end of Extra_bddHaarInverse */

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_addRemapNatural2Sequential( DdManager * dd, DdNode * aSource, DdNode * bVars )
{
	static int Vars[MAXINPUTS];
	static int Permute[MAXINPUTS];
	int k, nVars = 0;
	DdNode * bTemp;

	// create the array of variables in the set bVars
	for ( bTemp = bVars; bTemp != b1; bTemp = cuddT(bTemp) )
		Vars[nVars++] = bTemp->index;

	k = 0;
	for ( bTemp = bVars; bTemp != b1; bTemp = cuddT(bTemp), k++ )
		Permute[bTemp->index] = Vars[nVars-1-k];

	return Cudd_addPermute( dd, aSource, Permute );
}

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

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

  Synopsis    [Performs the reordering-sensitive step of Extra_bddWalsh().]

  Description [Generates in a bottom-up fashion an ADD for all spectral
               coefficients of the functions represented by a BDD.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode* extraBddWalsh( 
  DdManager * dd,    /* the manager */
  DdNode * bFunc,    /* the function whose spectrum is being computed */
  DdNode * bVars)    /* the variables on which the function depends */
{
	DdNode * aRes;
    statLine(dd); 

	if ( clock() > s_TimeLimit )
		return NULL;

	/* terminal cases */
	if ( bVars == b1 )
	{
		assert( Cudd_IsConstant(bFunc) );
		if ( bFunc == b0 )
			return a1;
		else
			return Cudd_addConst(dd,-1.0);
	}

    /* check cache */
//	if ( bFunc->ref != 1 )
    if ( aRes = cuddCacheLookup2(dd, extraBddWalsh, bFunc, bVars) )
	{
	    s_CacheHit++;
    	return aRes;
	}
	else
	{
		DdNode * bFunc0,  * bFunc1;   /* cofactors of the function */
		DdNode * aWalsh0, * aWalsh1;   /* partial solutions of the problem */
		DdNode * aRes0,   * aRes1;    /* partial results to be composed by ITE */
		DdNode * bFuncR = Cudd_Regular(bFunc); /* the regular pointer to the function */

	    s_CacheMiss++;

	    /* bFunc cannot depend on a variable that is not in bVars */
		assert( cuddI(dd,bFuncR->index) >= cuddI(dd,bVars->index) );


		/* cofactor the BDD */
		if ( bFuncR->index == bVars->index )
		{
			if ( bFuncR != bFunc ) /* bFunc is complemented */
			{
				bFunc0 = Cudd_Not( cuddE(bFuncR) );
				bFunc1 = Cudd_Not( cuddT(bFuncR) );
			}
			else
			{
				bFunc0 = cuddE(bFuncR);
				bFunc1 = cuddT(bFuncR);
			}
		}
		else /* bVars is higher in the variable order */
			bFunc0 = bFunc1 = bFunc;


		/* solve subproblems */
		aWalsh0 = extraBddWalsh( dd, bFunc0, cuddT(bVars) );
		if ( aWalsh0 == NULL )
			return NULL;
		cuddRef( aWalsh0 );

		aWalsh1 = extraBddWalsh( dd, bFunc1, cuddT(bVars) );
		if ( aWalsh1 == NULL )
		{
			Cudd_RecursiveDeref( dd, aWalsh0 );
			return NULL;
		}
		cuddRef( aWalsh1 );


		/* compute  aRes0 = aWalsh0 + aWalsh1 */
		aRes0 = cuddAddApplyRecur( dd, Cudd_addPlus, aWalsh0, aWalsh1 );
		if ( aRes0 == NULL )
		{
			Cudd_RecursiveDeref( dd, aWalsh0 );
			Cudd_RecursiveDeref( dd, aWalsh1 );
			return NULL;
		}
		cuddRef( aRes0 );

		/* compute  aRes1 = aWalsh0 - aWalsh1 */
		aRes1 = cuddAddApplyRecur( dd, Cudd_addMinus, aWalsh0, aWalsh1 );
		if ( aRes1 == NULL )
		{
			Cudd_RecursiveDeref( dd, aWalsh0 );
			Cudd_RecursiveDeref( dd, aWalsh1 );
			Cudd_RecursiveDeref( dd, aRes0 );
			return NULL;
		}
		cuddRef( aRes1 );

		Cudd_RecursiveDeref(dd, aWalsh0);
		Cudd_RecursiveDeref(dd, aWalsh1);


		/* only aRes0 and aRes1 are referenced at this point */

		/* consider the case when Res0 and Res1 are the same node */
		aRes = (aRes1 == aRes0) ? aRes1 : cuddUniqueInter( dd, bVars->index, aRes1, aRes0 );
		if (aRes == NULL) 
		{
			Cudd_RecursiveDeref(dd, aRes1);
			Cudd_RecursiveDeref(dd, aRes0);
			return NULL;
		}
		cuddDeref(aRes1);
		cuddDeref(aRes0);