extraaddmisc.c

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

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

  Synopsis [ADD restrict according.]

  Description [ADD restrict according to Coudert and Madre's algorithm
  (ICCAD90) applicable to true ADDs (and not only to 0/1 ADDs as in CUDD). 
  Another important difference is that this procedure takes the don't-care set,
  and not the care set as the standard restrict.
  Returns the restricted ADD if successful; otherwise NULL.  If application of 
  restrict results in an ADD larger than the input ADD, the input ADD is returned.]

  SideEffects [None]

  SeeAlso     [Cudd_addConstrain Cudd_addRestrict]

******************************************************************************/
DdNode * Extra_addRestrictAdd( DdManager * dd, DdNode * f, DdNode * d )
{
	DdNode *supp_f, *supp_d;
	DdNode *res, *commonSupport;
	int intersection;
	int sizeF, sizeRes;

	/* Check if supports intersect. */
	supp_f = Cudd_Support( dd, f );
	if ( supp_f == NULL )
	{
		return ( NULL );
	}
	cuddRef( supp_f );
	supp_d = Cudd_Support( dd, d );
	if ( supp_d == NULL )
	{
		Cudd_RecursiveDeref( dd, supp_f );
		return ( NULL );
	}
	cuddRef( supp_d );
	commonSupport = Cudd_bddLiteralSetIntersection( dd, supp_f, supp_d );
	if ( commonSupport == NULL )
	{
		Cudd_RecursiveDeref( dd, supp_f );
		Cudd_RecursiveDeref( dd, supp_d );
		return ( NULL );
	}
	cuddRef( commonSupport );
	Cudd_RecursiveDeref( dd, supp_f );
	Cudd_RecursiveDeref( dd, supp_d );
	intersection = (commonSupport != DD_ONE(dd));
	Cudd_RecursiveDeref( dd, commonSupport );

	if ( intersection )
	{
		do
		{
			dd->reordered = 0;
			res = extraAddRestrictAdd( dd, f, d );
		}
		while ( dd->reordered == 1 );
		sizeF   = Cudd_DagSize( f );
		sizeRes = Cudd_DagSize( res );
		if ( sizeF <= sizeRes )
		{
			cuddRef( res );
			Cudd_RecursiveDeref( dd, res );
			return ( f );
		}
		else
		{
			return ( res );
		}
	}
	else
	{
		return ( f );
	}

}								/* end of Extra_addRestrictAdd */

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

  Synopsis    [The intersection of paths leading to each terminal, except terminal 0.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_addApply]

******************************************************************************/
DdNode * Extra_addForeachTerminalAnd( DdManager * dd, DdNode ** f, DdNode ** g )
{
	if ( cuddIsConstant( *f ) && cuddIsConstant( *g ) )
	{
		if ( *f == *g )
			return *f;
		else
			return dd->zero;
	}
	return NULL;
}								/* end of Extra_addForeachTerminalAnd */

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

  Synopsis    [The union of paths leading to each terminal, except terminal 0.]

  Description [The same path in two ADDs cannot lead to different terminals 
  unless one of the terminals is 0.]

  SideEffects [None]

  SeeAlso     [Cudd_addApply]

******************************************************************************/
DdNode * Extra_addForeachTerminalOr( DdManager * dd, DdNode ** f, DdNode ** g )
{
	if ( cuddIsConstant( *f ) && cuddIsConstant( *g ) )
	{
		if ( *f == *g )
			return *f;
		if ( *f == dd->zero )
			return *g;
		if ( *g == dd->zero )
			return *f;
		assert( 0 );
	}
	return NULL;
}								/* end of Extra_addForeachTerminalOr */

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

  Synopsis    [The union of paths leading to each terminal, except terminal 0.]

  Description [It is known that g is the subset of f.]

  SideEffects [None]

  SeeAlso     [Cudd_addApply]

******************************************************************************/
DdNode * Extra_addForeachTerminalSharp( DdManager * dd, DdNode ** f, DdNode ** g )
{
	if ( cuddIsConstant( *f ) && cuddIsConstant( *g ) )
	{
		if ( *f == *g )
			return dd->zero;
		if ( *g == dd->zero )
			return *f;
		assert( 0 );
	}
	return NULL;
}								/* end of Extra_addForeachTerminalOr */

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

  Synopsis    [Swaps the given terminal with the zero terminal.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_addSwapTerminals( DdManager * dd, DdNode * aFunc, DdNode * aTerm )
{
    DdNode * aRes;
    do {
		dd->reordered = 0;
		aRes = extraAddSwapTerminals( dd, aFunc, aTerm );
    } while (dd->reordered == 1);
    return aRes;
}

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

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

  Synopsis    [Swaps the given terminal with the zero terminal.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraAddSwapTerminals( DdManager * dd, DdNode * aFunc, DdNode * aTerm )
{
	DdNode * aRes0, * aRes1, * aRes;

	if ( cuddIsConstant( aFunc ) )
	{
		if ( aFunc == a0 )
			return aTerm;
		if ( aFunc == aTerm )
			return a0;
		return aFunc;
	}

    if ( aRes = cuddCacheLookup2(dd, extraAddSwapTerminals, aFunc, aTerm) )
    	return aRes;

	aRes0 = extraAddSwapTerminals( dd, cuddE(aFunc), aTerm );
	if ( aRes0 == NULL ) 
		return NULL;
	cuddRef( aRes0 );

	aRes1 = extraAddSwapTerminals( dd, cuddT(aFunc), aTerm );
	if ( aRes1 == NULL ) 
	{
		Cudd_RecursiveDeref( dd, aRes0 );
		return NULL;
	}
	cuddRef( aRes1 );

	if ( aRes0 == aRes1 )
		aRes = aRes1;
	else 
	{
		aRes = cuddUniqueInter( dd, aFunc->index, aRes1, aRes0 );
		if ( aRes == NULL ) 
		{
			Cudd_RecursiveDeref(dd,aRes0);
			Cudd_RecursiveDeref(dd,aRes1);
			return NULL;
		}
	}
	cuddDeref( aRes0 );
	cuddDeref( aRes1 );
		
	cuddCacheInsert2(dd, extraAddSwapTerminals, aFunc, aTerm, aRes);
	return aRes;
}


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

  Synopsis    [Performs the recursive step of Extra_addRestrictAdd.]

  Description [Performs the recursive step of Extra_addRestrictAdd.
  Returns the restricted ADD if successful; otherwise NULL.]

  SideEffects [None]

  SeeAlso     [Cudd_addRestrict]

******************************************************************************/
DdNode * extraAddRestrictAdd( DdManager * dd, DdNode * aF, DdNode * aD )
{
	DdNode * aF0, * aF1, * aD0, * aD1, * aDtot, * aRes0, * aRes1, * aRes;
	int topf, topd;

	statLine( dd );

	// if there is no don't-care, return aF
	if ( aD == dd->zero )
		return aF;
	// if they are equal, aF is a complete don't-care (can be simplified to zero)
	if ( aF == aD )
		return dd->zero;
	// here, they are not equal and don't-care is not empty

	// if they are both constants, they are *different* constants, so return aF
	if ( cuddIsConstant(aF) && cuddIsConstant(aD) )
		return aF;
	// here, at least one of them is not a constant

	// check the cache
	aRes = cuddCacheLookup2( dd, extraAddRestrictAdd, aF, aD );
	if ( aRes != NULL )
		return aRes;

	topf = cuddI( dd, aF->index );
	topd = cuddI( dd, aD->index );

	if ( topd < topf )
	{ // abstract the top variable from aD

		// find cofactors of aD
		aD0 = cuddE(aD);
		aD1 = cuddT(aD);
		// intersect the cofactor don't-cares
		aDtot = cuddAddApplyRecur( dd, Extra_addForeachTerminalAnd, aD0, aD1 );
		if ( aDtot == NULL )
			return ( NULL );
		cuddRef( aDtot );
		aRes = extraAddRestrictAdd( dd, aF, aDtot );
		if ( aRes == NULL )
		{
			Cudd_RecursiveDeref( dd, aDtot );
			return ( NULL );
		}
		cuddRef( aRes );
		Cudd_RecursiveDeref( dd, aDtot );
		cuddCacheInsert2( dd, extraAddRestrictAdd, aF, aD, aRes );
		cuddDeref( aRes );
		return aRes;
	}
	// here topf <= topc

	aF0 = cuddE(aF);
	aF1 = cuddT(aF);
	if ( topd == topf )
	{
		aD0 = cuddE(aD);
		aD1 = cuddT(aD);
	}
	else
	{
		aD0 = aD1 = aD;
	}

	aRes0 = extraAddRestrictAdd( dd, aF0, aD0 );
	if ( aRes0 == NULL )
		return NULL;
	cuddRef( aRes0 );

	aRes1 = extraAddRestrictAdd( dd, aF1, aD1 );
	if ( aRes1 == NULL )
	{
		Cudd_RecursiveDeref( dd, aRes0 );
		return NULL;
	}
	cuddRef( aRes1 );

	aRes = ( aRes0 == aRes1 ) ? aRes0 : cuddUniqueInter( dd, aF->index, aRes1, aRes0 );
	if ( aRes == NULL )
	{
		Cudd_RecursiveDeref( dd, aRes0 );
		Cudd_RecursiveDeref( dd, aRes1 );
		return ( NULL );
	}
	cuddDeref( aRes0 );
	cuddDeref( aRes1 );

	cuddCacheInsert2( dd, extraAddRestrictAdd, aF, aD, aRes );
	return aRes;

}	/* end of extraAddRestrictAdd */


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