extrazddsubsup.c

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

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

  FileName    [extraZddSubSup.c]

  PackageName [extra]

  Synopsis    [SubSet, SupSet, NotSubSet, NotSupSet used to solve problems 
  arising in two-level SOP minimization. See O. Coudert, "Two-Level Logic 
  Minimization:An Overview", Integration. Vol. 17, No. 2, pp. 97-140, Oct 1994.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

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

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


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


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


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

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


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

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

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


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

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

  Synopsis    [Computes subsets in X that are contained in some of the subsets of Y.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddNotSubSet, Extra_zddSupSet, Extra_zddNotSupSet]

******************************************************************************/
DdNode	*
Extra_zddSubSet(
  DdManager * dd,
  DdNode * X,
  DdNode * Y)
{
    DdNode	*res;
    int		autoDynZ;

    autoDynZ = dd->autoDynZ;
    dd->autoDynZ = 0;

    do {
	dd->reordered = 0;
	res = extraZddSubSet(dd, X, Y);
    } while (dd->reordered == 1);
    dd->autoDynZ = autoDynZ;
    return(res);

} /* end of Extra_zddSubSet */


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

  Synopsis    [Computes subsets in X that contain some of the subsets of Y.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddSubSet, Extra_zddNotSubSet, Extra_zddNotSupSet]

******************************************************************************/
DdNode	*
Extra_zddSupSet(
  DdManager * dd,
  DdNode * X,
  DdNode * Y)
{
    DdNode	*res;
    int		autoDynZ;

    autoDynZ = dd->autoDynZ;
    dd->autoDynZ = 0;

    do {
	dd->reordered = 0;
	res = extraZddSupSet(dd, X, Y);
    } while (dd->reordered == 1);
    dd->autoDynZ = autoDynZ;
    return(res);

} /* end of Extra_zddSupSet */

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

  Synopsis    [Computes subsets in X that are not contained in any of the subsets of Y.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddSubSet, Extra_zddSupSet, Extra_zddNotSupSet]

******************************************************************************/
DdNode	*
Extra_zddNotSubSet(
  DdManager * dd,
  DdNode * X,
  DdNode * Y)
{
    DdNode	*res;
    int		autoDynZ;

    autoDynZ = dd->autoDynZ;
    dd->autoDynZ = 0;

    do {
	dd->reordered = 0;
	res = extraZddNotSubSet(dd, X, Y);
    } while (dd->reordered == 1);
    dd->autoDynZ = autoDynZ;
    return(res);

} /* end of Extra_zddNotSubSet */


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

  Synopsis    [Computes subsets in X that do not contain any of the subsets of Y.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddSubSet, Extra_zddSupSet, Extra_zddNotSubSet]

******************************************************************************/
DdNode	*
Extra_zddNotSupSet(
  DdManager * dd,
  DdNode * X,
  DdNode * Y)
{
    DdNode	*res;
    int		autoDynZ;

    autoDynZ = dd->autoDynZ;
    dd->autoDynZ = 0;

    do {
	dd->reordered = 0;
	res = extraZddNotSupSet(dd, X, Y);
    } while (dd->reordered == 1);
    dd->autoDynZ = autoDynZ;
    return(res);

} /* end of Extra_zddNotSupSet */



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

  Synopsis    [Computes the maximal of subsets in X not contained in any of the subsets of Y.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddSubSet, Extra_zddSupSet, Extra_zddSubSet, Extra_zddNotSupSet]

******************************************************************************/
DdNode	*
Extra_zddMaxNotSupSet(
  DdManager * dd,
  DdNode * X,
  DdNode * Y)
{
    DdNode	*res;
    int		autoDynZ;

    autoDynZ = dd->autoDynZ;
    dd->autoDynZ = 0;

    do {
	dd->reordered = 0;
	res = extraZddMaxNotSupSet(dd, X, Y);
    } while (dd->reordered == 1);
    dd->autoDynZ = autoDynZ;
    return(res);

} /* end of Extra_zddMaxNotSupSet */


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

  Synopsis    [Returns 1 if ZDD contains the empty combination; 0 otherwise.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int 
Extra_zddEmptyBelongs(
  DdManager *dd, 
  DdNode* zS )
{
	while ( zS->index != CUDD_MAXINDEX )
		zS = cuddE( zS );
	return (int)( zS == z1 );

} /* end of Extra_zddEmptyBelongs */


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

  Synopsis    [Returns 1 if the set is empty or consists of one subset only.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int 
Extra_zddIsOneSubset(
  DdManager * dd, 
  DdNode * zS )
{
	while ( zS->index != CUDD_MAXINDEX )
	{
		assert( cuddT(zS) != z0 );
		if ( cuddE(zS) != z0 )
			return 0;
		zS = cuddT( zS );
	}
	return (int)( zS == z1 );

} /* end of Extra_zddEmptyBelongs */


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

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

  Synopsis [Performs the recursive step of Extra_zddSubSet.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode* extraZddSubSet( DdManager *dd, DdNode *X, DdNode *Y )
{	
	DdNode *zRes;
    statLine(dd); 
	/* any comb is a subset of itself */
	if ( X == Y ) 
		return X;
	/* if X is empty, the result is empty */
	if ( X == z0 ) 
		return z0;
	/* combs in X are notsubsets of non-existant combs in Y */
	if ( Y == z0 ) 
		return z0;
	/* the empty comb is contained in all combs of Y */
	if ( X == z1 ) 
		return z1;
	/* only {()} is the subset of {()} */
	if ( Y == z1 ) /* check whether the empty combination is present in X */ 
		return ( Extra_zddEmptyBelongs( dd, X )? z1: z0 );

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddSubSet, X, Y);
    if (zRes)
    	return(zRes);
	else
	{
		DdNode *zRes0, *zRes1, *zTemp;
		int TopLevelX = dd->permZ[ X->index ];
		int TopLevelY = dd->permZ[ Y->index ];

		if ( TopLevelX < TopLevelY )
		{
			/* compute combs of X without var that are notsubsets of combs with Y */
			zRes = extraZddSubSet( dd, cuddE( X ), Y );
			if ( zRes == NULL )  return NULL;
		}
		else if ( TopLevelX == TopLevelY )
		{
			/* merge combs of Y with and without var */
			zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
			if ( zTemp == NULL )
				return NULL;
			cuddRef( zTemp );

			/* compute combs of X without var that are notsubsets of combs is Temp */
			zRes0 = extraZddSubSet( dd, cuddE( X ), zTemp );
			if ( zRes0 == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zTemp );
				return NULL;
			}
			cuddRef( zRes0 );
			Cudd_RecursiveDerefZdd( dd, zTemp );

			/* combs of X with var that are notsubsets of combs in Y with var */
			zRes1 = extraZddSubSet( dd, cuddT( X ), cuddT( Y ) );
			if ( zRes1 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				return NULL;
			}
			cuddRef( zRes1 );

			/* compose Res0 and Res1 with the given ZDD variable */
			zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
			if ( zRes == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes1 );
				return NULL;
			}
			cuddDeref( zRes0 );
			cuddDeref( zRes1 );
		}
		else /* if ( TopLevelX > TopLevelY ) */
		{
			/* merge combs of Y with and without var */
			zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
			if ( zTemp == NULL )  return NULL;
			cuddRef( zTemp );

			/* compute combs that are notsubsets of Temp */
			zRes = extraZddSubSet( dd, X, zTemp );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zTemp );
				return NULL;
			}
			cuddRef( zRes );
			Cudd_RecursiveDerefZdd( dd, zTemp );
			cuddDeref( zRes );
		}

		/* insert the result into cache */
	    cuddCacheInsert2(dd, extraZddSubSet, X, Y, zRes);
		return zRes;
	}
} /* end of extraZddSubSet */


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

  Synopsis [Performs the recursive step of Extra_zddSupSet.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode* extraZddSupSet( DdManager *dd, DdNode *X, DdNode *Y )
{	
	DdNode *zRes;
    statLine(dd); 
	/* any comb is a superset of itself */
	if ( X == Y ) 
		return X;
	/* no comb in X is superset of non-existing combs */
	if ( Y == z0 ) 
		return z0;	
	/* any comb in X is the superset of the empty comb */
	if ( Extra_zddEmptyBelongs( dd, Y ) ) 
		return X;
	/* if X is empty, the result is empty */
	if ( X == z0 ) 
		return z0;
	/* if X is the empty comb (and Y does not contain it!), return empty */
	if ( X == z1 ) 
		return z0;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddSupSet, X, Y);
    if (zRes)
    	return(zRes);
	else
	{
		DdNode *zRes0, *zRes1, *zTemp;
		int TopLevelX = dd->permZ[ X->index ];
		int TopLevelY = dd->permZ[ Y->index ];

		if ( TopLevelX < TopLevelY )
		{
			/* combinations of X without label that are supersets of combinations with Y */
			zRes0 = extraZddSupSet( dd, cuddE( X ), Y );
			if ( zRes0 == NULL )  return NULL;
			cuddRef( zRes0 );

			/* combinations of X with label that are supersets of combinations with Y */
			zRes1 = extraZddSupSet( dd, cuddT( X ), Y );
			if ( zRes1 == NULL )  
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				return NULL;
			}
			cuddRef( zRes1 );

			/* compose Res0 and Res1 with the given ZDD variable */
			zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes1 );
				return NULL;
			}