extraddutils.c

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

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

  FileName    [extraDdUtils.c]

  PackageName [extra]

  Synopsis    [Various BDD manipulating procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "extra.h"

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

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

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

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

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


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

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

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


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

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

  Synopsis    [Selects cubes from the cover that are completely contained in the area.]

  Description [This function is similar to Extra_zddSubSet(X,Y) which selects 
  those subsets of X that are completely contained in at least one subset of Y. 
  Extra_zddCoveredByArea() filters the cover of cubes and returns only those cubes 
  that are completely contained in the area. The cover is given as a ZDD, the 
  area is a BDD. Returns the reduced cube set on success; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Extra_zddSubSet]

******************************************************************************/
DdNode	*
Extra_zddCoveredByArea(
  DdManager * dd,
  DdNode * zC,
  DdNode * bA)
{
    DdNode	*res;

    do {
	dd->reordered = 0;
	res = extraZddCoveredByArea(dd, zC, bA);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddCoveredByArea */


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

  Synopsis    [Selects cubes from the cover that are not completely covered by other cover.]

  Description [This function is equivalent to first converting the second cover 
  into BDD, calling Extra_zddCoveredByArea(), and then subtracting from the
  first cover the result of the latter operation. However, it is more efficient.
  Returns the reduced cube set on success; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Extra_zddSubSet]

******************************************************************************/
DdNode	*
Extra_zddNotCoveredByCover(
  DdManager * dd,
  DdNode * zC,
  DdNode * zD)
{
    DdNode	*res;

    do {
	dd->reordered = 0;
	res = extraZddNotCoveredByCover(dd, zC, zD);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddNotCoveredByCover */


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

  Synopsis    [Selects cubes from the cover that are overlapping with the area.]

  Description [This function is similar to Extra_zddNotSubSet(X,Y) which selects 
  those subsets of X that are completely contained in at least one subset of Y. 
  Extra_zddOverlappingWithArea() filters the cover of cubes and returns only those 
  cubes that overlap with the area. The completely contained cubes are counted as
  overlapping. The cover is given as a ZDD, the area is a BDD. Returns the reduced 
  cube set on success; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Extra_zddSubSet]

******************************************************************************/
DdNode	*
Extra_zddOverlappingWithArea(
  DdManager * dd,
  DdNode * zC,
  DdNode * bA)
{
    DdNode	*res;

    do {
	dd->reordered = 0;
	res = extraZddOverlappingWithArea(dd, zC, bA);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddOverlappingWithArea */


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

  Synopsis    [Converts the ZDD into the BDD.]

  Description [This function is a reimplementation of Cudd_MakeBddFromZddCover 
  for the case when BDD variable and ZDD variable orders are synchronized. 
  It is the user's responsibility to ensure the synchronization. This function is
  more efficient than Cudd_MakeBddFromZddCover because it does not require
  referencing cofactors of the cover and because it used cuddUniqueInterO() 
  instead of cuddUniqueInterIVO(). Returns the bdd on success; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_MakeBddFromZddCover]

******************************************************************************/
DdNode	*
Extra_zddConvertToBdd(
  DdManager * dd,
  DdNode * zC)
{
    DdNode	*res;

    do {
	dd->reordered = 0;
	res = extraZddConvertToBdd(dd, zC);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddConvertToBdd */

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

  Synopsis    [Converts the ZDD of the positive unate function into the BDD.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_MakeBddFromZddCover Extra_zddConvertToBdd]

******************************************************************************/
DdNode	*
Extra_zddConvertToBddUnate(
  DdManager * dd,
  DdNode * zC)
{
    DdNode	*res;

    do {
	dd->reordered = 0;
	res = extraZddConvertToBddUnate(dd, zC);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddConvertToBdd */

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

  Synopsis    [Converts the ZDD for ESOP into the BDD.]

  Description [Returns the bdd on success; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_MakeBddFromZddCover Extra_zddConvertToBdd]

******************************************************************************/
DdNode	*
Extra_zddConvertEsopToBdd(
  DdManager * dd,
  DdNode * zC)
{
    DdNode	*res;

    do {
	dd->reordered = 0;
	res = extraZddConvertEsopToBdd(dd, zC);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddConvertEsopToBdd */


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

  Synopsis    [Converts ZDD into BDD while at the same time adding another BDD to it.]

  Description [This function is equivalent to first calling Extra_zddConvertToBdd()
  and then Cudd_bddOr() but is more efficient. Returns the reduced cube set on 
  success; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Extra_zddConvertToBdd]

******************************************************************************/
DdNode	*
Extra_zddConvertToBddAndAdd(
  DdManager * dd,
  DdNode * zC,
  DdNode * bA)
{
    DdNode	*res;

    do {
	dd->reordered = 0;
	res = extraZddConvertToBddAndAdd(dd, zC, bA);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddConvertToBddAndAdd */


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

  Synopsis    [Finds the area covered by only one cube from cover.]

  Description [This function computes the BDD of the area covered by only one cube
  from the give cover. Returns the reduced cube set on success; NULL otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode	*
Extra_zddSingleCoveredArea(
  DdManager * dd,
  DdNode * zC)
{
    DdNode	*res;

    do {
	dd->reordered = 0;
	res = extraZddSingleCoveredArea(dd, zC);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddSingleCoveredArea */

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

  Synopsis    [Converts the BDD cube into the ZDD cube.]

  Description [Returns the pointer to the ZDD on success; NULL otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode	*
Extra_zddConvertBddCubeIntoZddCube(
  DdManager * dd,
  DdNode * bCube)
{
    DdNode	*zCube;
	int *VarValues, i;

	/* allocate temporary storage for variable values */
	assert( dd->sizeZ == 2 * dd->size );
	VarValues = (int*) malloc( dd->sizeZ * sizeof(int) );
	if ( VarValues == NULL ) 
	{
		dd->errorCode = CUDD_MEMORY_OUT;
		return NULL;
	}
	/* clean the storage */
	for ( i = 0; i < dd->sizeZ; i++ )
		VarValues[i] = 0;
	/* get the variable values */
	while ( bCube != b1 )
	{
		assert( !Cudd_IsComplement(bCube) );
		if ( Cudd_E(bCube) == b0 ) /* positive literal */
			VarValues[2*bCube->index] = 1, bCube = Cudd_T(bCube);
		else if ( Cudd_T(bCube) == b0 ) /* negative literal */
			VarValues[2*bCube->index+1] = 1, bCube = Cudd_E(bCube);
		else
			assert(0);
		assert( bCube != b0 );
	}
	/* get the ZDD cube */
	zCube = Extra_zddCombination( dd, VarValues, dd->sizeZ );
	free(VarValues);
	return zCube;
} /* end of Extra_zddConvertBddCubeIntoZddCube */

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

  Synopsis    [Verifies whether the cover belongs to the specified range.]

  Description [Returns 1 if verification succeeds; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
Extra_zddVerifyCover(
  DdManager * dd,
  DdNode * zC,
  DdNode * bFuncOn,
  DdNode * bFuncOnDc)
{
	DdNode * bCover;
	int fVerificationOkay = 1;

	bCover = Extra_zddConvertToBdd( dd, zC );
	Cudd_Ref( bCover );

	if ( Cudd_bddIteConstant( dd, bFuncOn, bCover, dd->one ) != dd->one )
	{
		fVerificationOkay = 0;
		printf(" - Verification not okey: Solution does not cover the on-set\n");
	}
	if ( Cudd_bddIteConstant( dd, bCover, bFuncOnDc, dd->one ) != dd->one )
	{
		fVerificationOkay = 0;
		printf(" - Verification not okey: Solution overlaps with the off-set\n");
	}
	if ( fVerificationOkay )
		printf(" +\n");

	Cudd_RecursiveDeref( dd, bCover );
	return fVerificationOkay;
} /* end of Extra_zddVerifyCover */



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

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

  Synopsis [Performs the recursive step of Extra_zddCoveredByArea.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode	*
extraZddCoveredByArea(
  DdManager * dd,
  DdNode * zC,   /* the ZDD for the cover */
  DdNode * bA)   /* the BDD for the area */
{
    DdNode	*zRes;
    statLine(dd); 

	/* if there is no area, there are no contained cubes */
	if ( bA == b0 )  return z0;
	/* if the area is the total boolean space, the cover is contained completely */
	if ( bA == b1 )  return zC;
	/* if there is nothing in the cover, nothing is contained */
	if ( zC == z0 )  return z0;
	/* if the cover is one large cube (and the area is less than the total boolean space), 
	   nothing is contained */
	if ( zC == z1 )  return z0;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddCoveredByArea, zC, bA);
    if (zRes)
		return zRes;
	else
	{
		DdNode *bA0, *bA1, *bA01;

		/* find the level in terms of the original variable levels, not ZDD variable levels */
		int levCover = dd->permZ[zC->index] >> 1;
		int levArea  = dd->perm[Cudd_Regular(bA)->index];
		/* determine whether the area is a complemented BDD */
		int fIsComp  = Cudd_IsComplement( bA );

		if ( levCover > levArea )
		{
			/* find the parts(cofactors) of the area */
			bA0 = Cudd_NotCond( Cudd_E( bA ), fIsComp );
			bA1 = Cudd_NotCond( Cudd_T( bA ), fIsComp );

			/* find the intersection of cofactors */
			bA01 = cuddBddAndRecur( dd, bA0, bA1 );
			if ( bA01 == NULL ) return NULL;
			cuddRef( bA01 );

			/* only those cubes are contained which are contained in the intersection */
			zRes = extraZddCoveredByArea( dd, zC, bA01 );
			if ( zRes == NULL ) return NULL;
			cuddRef( zRes );
			Cudd_RecursiveDeref( dd, bA01 );
			cuddDeref( zRes );
		}
		else /* if ( levCover <= levArea ) */
		{
			DdNode *zRes0, *zRes1, *zRes2, *zTemp;
			int TopZddVar;

			/* decompose the cover */
			DdNode *zC0, *zC1, *zC2;
			extraDecomposeCover(dd, zC, &zC0, &zC1, &zC2);

			if ( levCover == levArea )
			{
				/* find the parts(cofactors) of the area */
				bA0 = Cudd_NotCond( Cudd_E( bA ), fIsComp );
				bA1 = Cudd_NotCond( Cudd_T( bA ), fIsComp );

				/* find the intersection of cofactors */
				bA01 = cuddBddAndRecur( dd, bA0, bA1 );
				if ( bA01 == NULL ) return NULL;
				cuddRef( bA01 );

			}
			else /* if ( levCover < levArea ) */
			{
				/* assign the cofactors and their intersection */
				bA0 = bA1 = bA01 = bA;
				/* reference the intersection for uniformity with the above case */
				cuddRef( bA01 );
			}

			/* solve subproblems */

			/* cover without literal can only be contained in the intersection */
			zRes2 = extraZddCoveredByArea( dd, zC2, bA01 );
			if ( zRes2 == NULL )
			{
				Cudd_RecursiveDeref( dd, bA01 );
				return NULL;
			}
			cuddRef( zRes2 );
			Cudd_RecursiveDeref( dd, bA01 );

			/* cover with negative literal can only be contained in bA0 */
			zRes0 = extraZddCoveredByArea( dd, zC0, bA0 );
			if ( zRes0 == NULL )
			{
				Cudd_RecursiveDerefZdd(dd, zRes2);
				return NULL;
			}
			cuddRef( zRes0 );

			/* cover with positive literal can only be contained in bA1 */
			zRes1 = extraZddCoveredByArea( dd, zC1, bA1 );
			if ( zRes1 == NULL )
			{
				Cudd_RecursiveDerefZdd(dd, zRes0);
				Cudd_RecursiveDerefZdd(dd, zRes2);
				return NULL;
			}
			cuddRef( zRes1 );

			/* --------------- compose the result ------------------ */
			/* the index of the positive ZDD variable in zC */
			TopZddVar = (zC->index >> 1) << 1;

			/* compose with-neg-var and without-var using the neg ZDD var */
			zTemp = cuddZddGetNode(dd, TopZddVar + 1, zRes0, zRes2 );
			if ( zTemp == NULL ) 
			{
				Cudd_RecursiveDerefZdd(dd, zRes0);
				Cudd_RecursiveDerefZdd(dd, zRes1);
				Cudd_RecursiveDerefZdd(dd, zRes2);
				return NULL;
			}
			cuddRef( zTemp );
			cuddDeref( zRes0 );
			cuddDeref( zRes2 );

			/* compose with-pos-var and previous result using the pos ZDD var */
			zRes = cuddZddGetNode(dd, TopZddVar, zRes1, zTemp );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd(dd, zRes1);
				Cudd_RecursiveDerefZdd(dd, zTemp);
				return NULL;
			}
			cuddDeref( zRes1 );
			cuddDeref( zTemp );
		}

		/* insert the result into cache and return */
		cuddCacheInsert2(dd, extraZddCoveredByArea, zC, bA, zRes);
		return zRes;
	}
} /* end of extraZddCoveredByArea */