extraddtimed.c

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

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

  FileName    [extraDdTimed.c]

  PackageName [extra]

  Synopsis    [Procedures with the timeout.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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


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

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

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

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

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

// the signature counter
int s_Signature = 1;

// the universal hash table
typedef struct HashEntry_t
{
	int Sign;           // signature of the current cache operation
	unsigned Arg1;      // the first argument
	unsigned Arg2;      // the second argument
	unsigned Arg3;      // the second argument
} HashEntry;


// HASH TABLE data structure and variables
#define g_TABLESIZE 11111
//int g_TableSize  = 11111;
HashEntry HTable[g_TABLESIZE];
static int HashSuccess = 0;
static int HashFailure = 0;

// lists of nodes to be referenced
static DdNode ** s_pRefDDs = NULL;
static int s_nRefDDs = 0;
static int s_nRefDDsAlloc = 0;



static int s_KeysAbsoluteLimit   = 1000000000;
static int s_KeysAllowedIncrease = 0;
static int s_Timeout             = 0;

static int s_TimeLimit = 0; 
static int s_KeysLimit = 0; 

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


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

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

// static functions
static DdNode * extraBddVectorCompose_rec( DdManager * dd, DdNode * f, DdNode ** vector, int deepest );
static void Extra_RefListAdd( DdNode * bF );
static void Extra_RefListRecursiveDeref( DdManager * dd );
static DdNode * extraZddIsopCoverAltTimed( DdManager * dd, DdNode * bA, DdNode * bB);
static DdNode * extraZddIsopCoverAltLimited( DdManager * dd, DdNode * bA, DdNode * bB, int *pnBTracks);

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


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


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

  Synopsis    [Sets the timeout.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void Extra_OperationTimeoutSet( int timeout )
{
	s_Timeout = timeout;
}

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

  Synopsis    [Sets the space.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void Extra_OperationSpaceoutSet( int MaxNodeIncrease )
{
	s_KeysAllowedIncrease = MaxNodeIncrease;
}


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

  Synopsis    [Resets the timeout.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void Extra_OperationTimeoutReset()
{
	s_Timeout = 0;
}

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

  Synopsis    [Resets the spaceout.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void Extra_OperationSpaceoutReset()
{
	s_KeysAllowedIncrease = 0;
}



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

  Synopsis    [Computes the conjunction of two BDDs f and g.]

  Description [Computes the conjunction of two BDDs f and g. Returns a
  pointer to the resulting BDD if successful; NULL if the intermediate
  result blows up.]

  SideEffects [None]

  SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAndAbstract Cudd_bddIntersect
  Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor]

******************************************************************************/
DdNode * Extra_bddAnd( DdManager * dd, DdNode * f, DdNode * g )
{
	DdNode *res;

	s_TimeLimit = (int)(s_Timeout /* in miliseconds*/ * (float)(CLOCKS_PER_SEC) / 1000 ) + clock();
	s_KeysLimit = ddMin( (int)dd->keys + s_KeysAllowedIncrease, s_KeysAbsoluteLimit );

	do
	{
		dd->reordered = 0;
		res = extraBddAndRecur( dd, f, g );
	}
	while ( dd->reordered == 1 );
	return ( res );

}								/* end of Extra_bddAnd */


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

  Synopsis    [Computes the disjunction of two BDDs f and g.]

  Description [Computes the disjunction of two BDDs f and g. Returns a
  pointer to the resulting BDD if successful; NULL if the intermediate
  result blows up.]

  SideEffects [None]

  SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddNand Cudd_bddNor
  Cudd_bddXor Cudd_bddXnor]

******************************************************************************/
DdNode * Extra_bddOr( DdManager * dd, DdNode * f, DdNode * g )
{
	DdNode *res;

	s_TimeLimit = (int)(s_Timeout /* in miliseconds*/ * (float)(CLOCKS_PER_SEC) / 1000 ) + clock();
	s_KeysLimit = ddMin( (int)dd->keys + s_KeysAllowedIncrease, s_KeysAbsoluteLimit );

	do
	{
		dd->reordered = 0;
		res = extraBddAndRecur( dd, Cudd_Not( f ), Cudd_Not( g ) );
	}
	while ( dd->reordered == 1 );
	res = Cudd_NotCond( res, res != NULL );
	return ( res );

}								/* end of Extra_bddOr */


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

  Synopsis    [Computes the boolean difference of f with respect to x.]

  Description [Computes the boolean difference of f with respect to the
  variable with index x.  Returns the BDD of the boolean difference if
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode * Extra_bddBooleanDiff( DdManager * manager, DdNode * f, int x )
{
	DdNode *res, *var;

	s_TimeLimit = (int)(s_Timeout /* in miliseconds*/ * (float)(CLOCKS_PER_SEC) / 1000 ) + clock();
	s_KeysLimit = ddMin( (int)manager->keys + s_KeysAllowedIncrease, s_KeysAbsoluteLimit );

	/* If the variable is not currently in the manager, f cannot
	   ** depend on it.
	 */
	if ( x >= manager->size )
		return ( Cudd_Not( DD_ONE( manager ) ) );
	var = manager->vars[x];

	do
	{
		manager->reordered = 0;
		res = extraBddBooleanDiffRecur( manager, Cudd_Regular( f ), var );
	}
	while ( manager->reordered == 1 );

	return ( res );

}								/* end of Extra_bddBooleanDiff */


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

  Synopsis    [The alternative implementation of irredundant sum-of-products.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddMinimal]

******************************************************************************/
DdNode* Extra_zddIsopCoverAltTimed( 
  DdManager * dd,     /* the DD manager */
  DdNode * bFuncOn,    /* the on-set */
  DdNode * bFuncOnDc)  /* the on-set + dc-set */
{
    DdNode	*res;

	s_TimeLimit = (int)(s_Timeout /* in miliseconds*/ * (float)(CLOCKS_PER_SEC) / 1000 ) + clock();
	s_KeysLimit = ddMin( (int)dd->keys + s_KeysAllowedIncrease, s_KeysAbsoluteLimit );

    do {
		dd->reordered = 0;
		res = extraZddIsopCoverAltTimed(dd, bFuncOn, bFuncOnDc);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddIsopCoverAlt */

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

  Synopsis    [ISOP computation with the limit on the number of backtracks.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddMinimal]

******************************************************************************/
DdNode * Extra_zddIsopCoverAltLimited( 
  DdManager * dd,      /* the DD manager */
  DdNode * bFuncOn,    /* the on-set */
  DdNode * bFuncOnDc,  /* the on-set + dc-set */
  int nBTracks )       /* the number of backtracks */
{
    DdNode * res;
    int nBTracksInit = nBTracks;

    do {
		dd->reordered = 0;
		res = extraZddIsopCoverAltLimited(dd, bFuncOn, bFuncOnDc, &nBTracks);
    } while (dd->reordered == 1);

//if ( nBTracksInit-nBTracks > 500 )
//printf( "The cover = %5d.", Cudd_zddCount( dd, res ) );
//printf( "    Performed backtracks = %5d.\n", nBTracksInit-nBTracks );

    return(res);

} /* end of Extra_zddIsopCoverAlt */


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

  Synopsis    [Computes the vector compose with the timeout.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_bddVectorCompose( DdManager * dd, DdNode * f, DdNode ** vector )
{
	DdNode *res;
	int deepest;
	int i;
	long clk = clock();

//	s_TimeLimit = (int)(s_Timeout /* in secs */       * (float)(CLOCKS_PER_SEC) ) + clock();
	s_TimeLimit = (int)(s_Timeout /* in miliseconds*/ * (float)(CLOCKS_PER_SEC) / 1000 ) + clock();
	s_KeysLimit = ddMin( (int)dd->keys + s_KeysAllowedIncrease, s_KeysAbsoluteLimit );

	do
	{
		dd->reordered = 0;

		// get unique signature
		s_Signature++;

		// set the counter of the referenced DDs to 0
		s_nRefDDs = 0;

		/* Find deepest real substitution. */
		for ( deepest = dd->size - 1; deepest >= 0; deepest-- )
		{
			i = dd->invperm[deepest];
			if ( vector[i] != dd->vars[i] )
				break;
		}

		/* Recursively solve the problem. */
		res = extraBddVectorCompose_rec( dd, f, vector, deepest );
		if ( res != NULL )
			cuddRef( res );

		/* Dispose of local cache. */
		// undo the DDs that were referenced for storing in the cache
		Extra_RefListRecursiveDeref(dd);
	}
	while ( dd->reordered == 1 );

//	printf( "VCtime = %.2f sec.\n", (float)(clock()-clk)/(float)(CLOCKS_PER_SEC) );

	if ( res != NULL )
		cuddDeref( res );
	return ( res );
}


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

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

  Synopsis [Implements the recursive step of Cudd_bddAnd.]

  Description [Implements the recursive step of Cudd_bddAnd by taking
  the conjunction of two BDDs.  Returns a pointer to the result is
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddAnd]

******************************************************************************/
DdNode * extraBddAndRecur( DdManager * manager, DdNode * f, DdNode * g )
{
	DdNode *F, *fv, *fnv, *G, *gv, *gnv;
	DdNode *one, *r, *t, *e;
	unsigned int topf, topg, index;

	// quit because of timeout or spaceout
	if ( s_Timeout && clock() > s_TimeLimit )
	{
//		printf( "t" );
		return NULL;
	}
	if ( s_KeysAllowedIncrease && (int)manager->keys > s_KeysLimit )
	{
//		printf( "s" );
		return NULL;
	}

	statLine( manager );
	one = DD_ONE( manager );

	/* Terminal cases. */
	F = Cudd_Regular( f );
	G = Cudd_Regular( g );
	if ( F == G )
	{
		if ( f == g )
			return ( f );
		else
			return ( Cudd_Not( one ) );
	}
	if ( F == one )
	{
		if ( f == one )
			return ( g );
		else
			return ( f );
	}
	if ( G == one )
	{
		if ( g == one )
			return ( f );
		else
			return ( g );
	}

	/* At this point f and g are not constant. */
	if ( f > g )
	{							/* Try to increase cache efficiency. */
		DdNode *tmp = f;
		f = g;
		g = tmp;
		F = Cudd_Regular( f );
		G = Cudd_Regular( g );
	}

	/* Check cache. */
	if ( F->ref != 1 || G->ref != 1 )
	{
		r = cuddCacheLookup2( manager, Cudd_bddAnd, f, g );
		if ( r != NULL )
			return ( r );
	}

	/* Here we can skip the use of cuddI, because the operands are known
	   ** to be non-constant.
	 */
	topf = manager->perm[F->index];
	topg = manager->perm[G->index];

	/* Compute cofactors. */
	if ( topf <= topg )
	{
		index = F->index;
		fv = cuddT( F );
		fnv = cuddE( F );
		if ( Cudd_IsComplement( f ) )
		{
			fv = Cudd_Not( fv );
			fnv = Cudd_Not( fnv );
		}
	}
	else
	{
		index = G->index;
		fv = fnv = f;
	}

	if ( topg <= topf )
	{
		gv = cuddT( G );
		gnv = cuddE( G );
		if ( Cudd_IsComplement( g ) )
		{
			gv = Cudd_Not( gv );
			gnv = Cudd_Not( gnv );
		}
	}
	else
	{
		gv = gnv = g;
	}

	t = extraBddAndRecur( manager, fv, gv );
	if ( t == NULL )
		return ( NULL );
	cuddRef( t );

	e = extraBddAndRecur( manager, fnv, gnv );
	if ( e == NULL )
	{
		Cudd_IterDerefBdd( manager, t );
		return ( NULL );
	}
	cuddRef( e );

	if ( t == e )
	{
		r = t;
	}
	else
	{
		if ( Cudd_IsComplement( t ) )
		{
			r = cuddUniqueInter( manager, ( int ) index, Cudd_Not( t ),
								 Cudd_Not( e ) );
			if ( r == NULL )
			{
				Cudd_IterDerefBdd( manager, t );
				Cudd_IterDerefBdd( manager, e );
				return ( NULL );
			}
			r = Cudd_Not( r );
		}
		else
		{
			r = cuddUniqueInter( manager, ( int ) index, t, e );
			if ( r == NULL )
			{
				Cudd_IterDerefBdd( manager, t );
				Cudd_IterDerefBdd( manager, e );
				return ( NULL );
			}
		}
	}
	cuddDeref( e );
	cuddDeref( t );
	if ( F->ref != 1 || G->ref != 1 )
		cuddCacheInsert2( manager, Cudd_bddAnd, f, g, r );
	return ( r );

}								/* end of extraBddAndRecur */

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

  Synopsis    [Performs the recursive steps of Cudd_bddBoleanDiff.]

  Description [Performs the recursive steps of Cudd_bddBoleanDiff.
  Returns the BDD obtained by XORing the cofactors of f with respect to
  var if successful; NULL otherwise. Exploits the fact that dF/dx =
  dF'/dx.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode * extraBddBooleanDiffRecur( DdManager * manager, DdNode * f, DdNode * var )