fmimage.c

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

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

  FileName    [fmImage.c]

  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]

  Synopsis    [The binary image computation by output splitting.]

  Author      [MVSIS Group]
  
  Affiliation [UC Berkeley]

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

  Revision    [$Id: fmImage.c,v 1.5 2003/05/27 23:15:33 alanmi Exp $]

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


#include "extra.h"
#include "array.h"
#include <time.h>

////////////////////////////////////////////////////////////////////////
///                       DATA STRUCTURES                            ///
////////////////////////////////////////////////////////////////////////

//#define PRB(dd,f)    printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")

// this structure stores the information about one transition function
typedef struct partinfo_ 
{
    int       BddSize;   // the number of BDD nodes
	DdNode *  bPart;     // the BDD of this partition
	DdNode *  bSupp;     // the support of this partition
	DdNode *  bVar;      // the variable to be used in the image
} partinfo;


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

// these are needed to implement timeout
static int s_Timeout   = 0;
static int s_TimeLimit = 0; 

static DdNode *   fmImage_rec( DdManager * dd, array_t * pParts, int nBddSize );
static partinfo * fmImagePartInfoAllocate();
static void       fmImagePartInfoDeallocate( DdManager * dd, partinfo * p );
static int        fmImagePartCompareBddSize( partinfo ** ppPart1, partinfo ** ppPart2 );
static void       fmImagePartInfoArrayFree( DdManager * dd, array_t * pParts );
static DdNode *   fmImageSmallSize( DdManager * dd, array_t * pParts, int nBddSize );
static array_t *  fmImageDisjointSupport( DdManager * dd, array_t * pParts );


////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFITIONS                           ///
////////////////////////////////////////////////////////////////////////


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

  Synopsis    [Computes the image of a set of function.]

  Description [Computes the image of the care set (bCareSet) with the set 
  of functions (pbFuncs). The variables used in the image are given (pbVars). 
  The number of functions in the set is also given (nFuncs). Stops iterative 
  splitting when the shared BDD size is less than nBddSize. ]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Fm_ImageCompute( DdManager * dd, DdNode * bCareSet, DdNode ** pbFuncs, int nFuncs, 
    DdNode ** pbVars, int nBddSize )
{
	array_t * pParts;
	DdNode * bImage, * bImageProper;
	DdNode * bTemp, * bConstr;
	partinfo * pNew;
	int i;

	s_TimeLimit = (int)(s_Timeout /* in miliseconds*/ * (float)(CLOCKS_PER_SEC) / 1000 ) + clock();

	// create the array of partitions
	pParts = array_alloc( partinfo *, 10 );

	// constrain the functions
	bImage = b1;  Cudd_Ref( bImage );
	for ( i = 0; i < nFuncs; i++ )
	{
		bConstr = Cudd_bddConstrain( dd, pbFuncs[i], bCareSet ); Cudd_Ref( bConstr );
		if ( Cudd_IsConstant(bConstr) )
		{
			bImage = Cudd_bddAnd( dd, bTemp = bImage, Cudd_NotCond(pbVars[i], (bConstr == b0)) );  Cudd_Ref( bImage );
			Cudd_RecursiveDeref( dd, bTemp );
			Cudd_RecursiveDeref( dd, bConstr );
		}
		else
		{
			pNew = fmImagePartInfoAllocate();
			pNew->bPart = bConstr; // takes ref
			pNew->bSupp = Cudd_Support( dd, bConstr );   Cudd_Ref( pNew->bSupp );
			pNew->bVar  = pbVars[i];
            pNew->BddSize = Cudd_DagSize(pNew->bPart);
			array_insert_last( partinfo *, pParts, pNew );
		}
	}

    if ( array_n(pParts) > 0 )
    {
//        partinfo * p1;
//        partinfo * p2;
//        p1 = array_fetch( partinfo *, pParts, 0 );
//        p2 = array_fetch( partinfo *, pParts, 1 );

        // sort partitions by size
        array_sort( pParts, fmImagePartCompareBddSize );
	    // call the recursive image computation
	    bImageProper = fmImage_rec( dd, pParts, nBddSize );  
	    if ( bImageProper == NULL )
	    {
		    Cudd_RecursiveDeref( dd, bImage );
		    fmImagePartInfoArrayFree( dd, pParts );
		    return NULL;
	    }
	    Cudd_Ref( bImageProper );
	    // add to the image
	    bImage = Cudd_bddAnd( dd, bTemp = bImage, bImageProper );  Cudd_Ref( bImage );
	    Cudd_RecursiveDeref( dd, bTemp );
	    Cudd_RecursiveDeref( dd, bImageProper );
    }
    fmImagePartInfoArrayFree( dd, pParts );

	Cudd_Deref( bImage );
	return bImage;
}



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

  Synopsis    [Computes the image of a set of function.]

  Description [Checks the terminal case (n=0,1), Checks the special case (n=2). 
  Checks disjoint supports. Checks the total BDD node limit (nBddSize). 
  If none of these trivial cases apply, splits recursively.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * fmImage_rec( DdManager * dd, array_t * pParts, int nBddSize )
{
	DdNode * bImage, * bImage0, * bImage1, * bConstr, * bTemp;
	DdNode * bImageProper0, * bImageProper1;
	array_t * pParts0, * pParts1;
	array_t * pDisjs, * pArray;
	partinfo * pCur, * pStart, * pNew;
	int i, k;

    assert( array_n(pParts) > 0 );

	// if there is no more than 1 non-constant function, the image is ready
	if ( array_n(pParts) == 1 )
		return dd->one;

	// checking the special case of 2 non-constant functions
	if ( array_n(pParts) == 2 )
	{ 
		partinfo * p1, * p2;
		p1 = array_fetch( partinfo *, pParts, 0 );
		p2 = array_fetch( partinfo *, pParts, 1 );
		if ( p1->bPart == p2->bPart )
			return Cudd_bddXnor( dd, p1->bVar, p2->bVar );
		else if ( p1->bPart == Cudd_Not(p2->bPart) )
			return Cudd_bddXor( dd, p1->bVar, p2->bVar );
	}

	// checking for disjoint supports
	pDisjs = fmImageDisjointSupport( dd, pParts );
	if ( pDisjs != NULL ) // there are disjoint support groups
	{
		DdNode * bImageNew, * bTemp;
		bImage = b1; Cudd_Ref( bImage );
		for ( i = 0; i < array_n(pDisjs); i++ )
		{
			pArray = array_fetch( array_t *, pDisjs, i );
			bImageNew = fmImage_rec( dd, pArray, nBddSize );   
			if ( bImageNew == NULL )
			{
				Cudd_RecursiveDeref( dd, bImage );
				for ( k = i; k < array_n(pDisjs); k++ )
				{
					pArray = array_fetch( array_t *, pDisjs, k );
					array_free(pArray);
				}
				array_free( pDisjs );
				return NULL;
			}
			Cudd_Ref( bImageNew );

			bImage = Cudd_bddAnd( dd, bTemp = bImage, bImageNew );  Cudd_Ref( bImage );
			Cudd_RecursiveDeref( dd, bTemp );
			Cudd_RecursiveDeref( dd, bImageNew );
			array_free(pArray);
		}
		array_free( pDisjs );
		Cudd_Deref( bImage );
		return bImage;
	}

	// checking the BDD size
	if ( bImage = fmImageSmallSize( dd, pParts, nBddSize ) )
		return bImage;

	if ( s_Timeout && clock() > s_TimeLimit )
		return NULL;

	// the regular case - split around the first function in the array
	pParts0 = array_alloc( partinfo *, array_n(pParts) - 1 );
	pParts1 = array_alloc( partinfo *, array_n(pParts) - 1 );
	bImage0 = b1;  Cudd_Ref( bImage0 );
	bImage1 = b1;  Cudd_Ref( bImage1 );
	pStart  = array_fetch( partinfo *, pParts, 0 );
	for ( i = 1; i < array_n(pParts); i++ )
	{
		// get the current partition
		pCur = array_fetch( partinfo *, pParts, i );

		// constrain using the negative phase
		bConstr = Cudd_bddConstrain( dd, pCur->bPart, Cudd_Not(pStart->bPart) ); Cudd_Ref( bConstr );
		if ( Cudd_IsConstant(bConstr) )
		{
			bImage0 = Cudd_bddAnd( dd, bTemp = bImage0, Cudd_NotCond(pCur->bVar, (bConstr == b0)) );  Cudd_Ref( bImage0 );
			Cudd_RecursiveDeref( dd, bTemp );
			Cudd_RecursiveDeref( dd, bConstr );
		}
		else
		{
			pNew = fmImagePartInfoAllocate();
			pNew->bPart = bConstr; // takes ref
			pNew->bSupp = Cudd_Support( dd, bConstr );   Cudd_Ref( pNew->bSupp );
			pNew->bVar  = pCur->bVar;
            pNew->BddSize = Cudd_DagSize(pNew->bPart);
			array_insert_last( partinfo *, pParts0, pNew );
		}

		// constrain using the positive phase
		bConstr = Cudd_bddConstrain( dd, pCur->bPart, pStart->bPart ); Cudd_Ref( bConstr );
		if ( Cudd_IsConstant(bConstr) )
		{
			bImage1 = Cudd_bddAnd( dd, bTemp = bImage1, Cudd_NotCond(pCur->bVar, (bConstr == b0)) );  Cudd_Ref( bImage1 );
			Cudd_RecursiveDeref( dd, bTemp );
			Cudd_RecursiveDeref( dd, bConstr );
		}
		else
		{
			pNew = fmImagePartInfoAllocate();
			pNew->bPart = bConstr; // takes ref
			pNew->bSupp = Cudd_Support( dd, bConstr );   Cudd_Ref( pNew->bSupp );
			pNew->bVar  = pCur->bVar;
            pNew->BddSize = Cudd_DagSize(pNew->bPart);
			array_insert_last( partinfo *, pParts1, pNew );
		}
	}

	// call the recursive image computation
    if ( array_n(pParts0) > 0 )
    {
        // sort partitions by size
        array_sort( pParts0, fmImagePartCompareBddSize );
	    bImageProper0 = fmImage_rec( dd, pParts0, nBddSize );  
	    if ( bImageProper0 == NULL )
	    {
		    Cudd_RecursiveDeref( dd, bImage0 );
		    Cudd_RecursiveDeref( dd, bImage1 );
		    fmImagePartInfoArrayFree( dd, pParts0 );
		    fmImagePartInfoArrayFree( dd, pParts1 );
		    return NULL;
	    }
	    Cudd_Ref( bImageProper0 );
	    // add to the image
	    bImage0 = Cudd_bddAnd( dd, bTemp = bImage0, bImageProper0 );  Cudd_Ref( bImage0 );
	    Cudd_RecursiveDeref( dd, bTemp );
	    Cudd_RecursiveDeref( dd, bImageProper0 );
    }
	fmImagePartInfoArrayFree( dd, pParts0 );

    if ( array_n(pParts1) > 0 )
    {
        // sort partitions by size
        array_sort( pParts1, fmImagePartCompareBddSize );
	    // call the recursive image computation
	    bImageProper1 = fmImage_rec( dd, pParts1, nBddSize );  
	    if ( bImageProper1 == NULL )
	    {
		    Cudd_RecursiveDeref( dd, bImageProper0 );
		    Cudd_RecursiveDeref( dd, bImage0 );
		    Cudd_RecursiveDeref( dd, bImage1 );
		    fmImagePartInfoArrayFree( dd, pParts0 );
		    fmImagePartInfoArrayFree( dd, pParts1 );
		    return NULL;
	    }
	    Cudd_Ref( bImageProper1 );
	    // add to the image
	    bImage1 = Cudd_bddAnd( dd, bTemp = bImage1, bImageProper1 );  Cudd_Ref( bImage1 );
	    Cudd_RecursiveDeref( dd, bTemp );
	    Cudd_RecursiveDeref( dd, bImageProper1 );
    }
	fmImagePartInfoArrayFree( dd, pParts1 );

	// compose the resulting image
	bImage = Cudd_bddIte( dd, pStart->bVar, bImage1, bImage0 ); Cudd_Ref( bImage );
	Cudd_RecursiveDeref( dd, bImage0 );
	Cudd_RecursiveDeref( dd, bImage1 );
	Cudd_Deref( bImage );