fmimagemv.c

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

			printf( "\n" );
		}
	}

	// allocate the place for the set
	pSet = ALLOC( char, array_n(pParts) );
	pAll = ALLOC( char, array_n(pParts) );
	memset( pAll, 0, sizeof(char) * array_n(pParts) );

	// isolate strongly connected components
	nCompsTotal = 0;
	while ( nCompsTotal < array_n(pParts) )
	{
		// find the next comp
		nComps = 0;
		for ( i = 0; i < array_n(pParts); i++ )
			if ( pAll[i] == 0 )
			{
				// add this comp
				pAll[i]        = 1;
				pSet[nComps++] = i;
				nCompsTotal++;
				break;
			}
		// add all the related comps
		for ( c = 0; c < nComps; c++ )
			for ( k = 0; k < array_n(pParts); k++ )
				if ( pAll[k] == 0 && pMatrix[pSet[c]][k] )
				{
					pAll[k]        = 1;
					pSet[nComps++] = k;
					nCompsTotal++;
				}
		// add this set of components to the result
		if ( nComps < array_n(pParts) )
		{
			if ( pArray == NULL )
				pArray = array_alloc( array_t *, 5 );
			// create the new set of partitions
			pPartNew = array_alloc( Fm_ImagePartInfo_t *, 10 );
			for ( i = 0; i < nComps; i++ )
			{
				p1 = array_fetch( Fm_ImagePartInfo_t *, pParts, pSet[i] );
				array_insert_last( Fm_ImagePartInfo_t *, pPartNew, p1 );
			}
			// insert the new set
			array_insert_last( array_t *, pArray, pPartNew );
		}
	}
	assert( nCompsTotal == array_n(pParts) );
	free( pMatrix[0] );
	free( pMatrix );
	free( pSet );
	free( pAll );

	if ( fPrintPartitions && pArray )
	{
		Fm_ImagePartInfo_t * p;
		array_t * pComp;
		int i, k;

		printf( "The total number of components = %d.\n", array_n(pParts) );
		for ( i = 0; i < array_n(pArray); i++ )
		{
			pComp = array_fetch( array_t *, pArray, i );
			printf( "The number of components = %d.\n", array_n(pComp) );
			for ( k = 0; k < array_n(pComp); k++ )
			{
				p = array_fetch( Fm_ImagePartInfo_t *, pComp, k );
//				PRB( dd, p->bSupp );
			}
		}
		i = 0;
	}

	return pArray;
}


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

  Synopsis    [Solves small problems using monolithic transition relation.]

  Description [Returns NULL if the problem is larger than the given size. 
  Otherwise, returns the solution.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * fmImageMvSmallSize( DdManager * dd, array_t * pParts, DdNode * bCubeIn, int nBddSize )
{
	DdNode * bTransRel, * bComp, * bTemp, * bImage;
	Fm_ImagePartInfo_t * pCur;
	int i, nNodes;

	assert( array_n(pParts) > 1 );

	nNodes = 0;
	for ( i = 0; i < array_n(pParts); i++ )
	{
		pCur    = array_fetch( Fm_ImagePartInfo_t *, pParts, i );
		nNodes += pCur->BddSize;
		if ( nNodes >= nBddSize )
			return NULL;
	}

	// build the transition relation mapping X space into P space using bPFuncs
	bTransRel = b1;  Cudd_Ref( b1 );
	for ( i = 0; i < array_n(pParts); i++ )
	{
		if ( s_Timeout && clock() > s_TimeLimit )
		{
			Cudd_RecursiveDeref( dd, bTransRel );
			return NULL;
		}

		// get the partition
		pCur = array_fetch( Fm_ImagePartInfo_t *, pParts, i );
		// get the component
//		bComp = Cudd_bddXnor( dd, pCur->bPart, pCur->bVar );	Cudd_Ref( bComp );
        bComp = fmImageMvPartConvolve( dd, pCur->pbFuncs, pCur->pbCodes, pCur->nValues );  Cudd_Ref( bComp );
		// multiply this component with the transitive relation
		bTransRel = Cudd_bddAnd( dd, bTemp = bTransRel, bComp );  Cudd_Ref( bTransRel );
		Cudd_RecursiveDeref( dd, bTemp );
		Cudd_RecursiveDeref( dd, bComp );
	}

	bImage = Cudd_bddExistAbstract( dd, bTransRel, bCubeIn );    Cudd_Ref( bImage );
	Cudd_RecursiveDeref( dd, bTransRel );
	Cudd_Deref( bImage );
	return bImage;
}




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

  Synopsis    [Allocates the data structure to store one partition.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Fm_ImagePartInfo_t * fmImageMvPartAllocate( DdNode * bSupp, DdNode ** pbFuncs, DdNode ** pbCodes, int nValues )
{
    Fm_ImagePartInfo_t * p;
    int i;
    p = ALLOC( Fm_ImagePartInfo_t, 1 );
    p->nValues = nValues;
    p->pbFuncs = ALLOC( DdNode *, nValues );
    p->pbCodes = ALLOC( DdNode *, nValues );
    p->bSupp = bSupp;   Cudd_Ref( bSupp );
    for ( i = 0; i < nValues; i++ )
    {
        p->pbFuncs[i] = pbFuncs[i];   Cudd_Ref( pbFuncs[i] );
        p->pbCodes[i] = pbCodes[i];   Cudd_Ref( pbCodes[i] );
    }
    p->BddSize = Cudd_SharingSize( pbFuncs, nValues );
	return p;
}

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

  Synopsis    [Creates the partition corresponding to one MV var.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Fm_ImagePartInfo_t * fmImageMvPartCreate( DdManager * dd, DdNode * bCare, DdNode * pbFuncs[], 
    DdNode * pbCodes[], int nValues, Vmx_VarMap_t * pVmxGlo, DdNode ** pbImagePart, bool fUseAnd )
{
    DdNode * pbConstrs[32];
    DdNode * bSupp;
    Fm_ImagePartInfo_t * pPart;

    // constrain the functions corresponding to this var
//	bConstr = Cudd_bddConstrain( dd, pbFuncs[i], bCareSet ); Cudd_Ref( bConstr );
    fmImageMvPartConstrain( dd, bCare, pbFuncs, nValues, pbConstrs, fUseAnd );
    // compute the support of the partition
    bSupp = fmImageMvPartSupport( dd, pbConstrs, nValues, pVmxGlo ); Cudd_Ref( bSupp );
    // decide whether this is a trivial case
	if ( bSupp == b1 ) // this MV partition is a constant after constraining
	{
//		bImage = Cudd_bddAnd( dd, bTemp = bImage, Cudd_NotCond(pbVars[i], (bConstr == b0)) );  Cudd_Ref( bImage );
        *pbImagePart = fmImageMvPartConvolve( dd, pbConstrs, pbCodes, nValues );  Cudd_Ref( *pbImagePart );
        pPart = NULL;
    }
	else
	{
		pPart = fmImageMvPartAllocate( bSupp, pbConstrs, pbCodes, nValues );
        *pbImagePart = NULL;
	}
    // deref the support
    Cudd_RecursiveDeref( dd, bSupp );
    // dereference the computed constrain
    fmImageMvPartDeref( dd, pbConstrs, nValues );
    return pPart;
}



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

  Synopsis    [Frees the data structure.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void fmImageMvPartFree( DdManager * dd, Fm_ImagePartInfo_t * p )
{
    int i;
    for ( i = 0; i < p->nValues; i++ )
    {
	    Cudd_RecursiveDeref( dd, p->pbFuncs[i] );
	    Cudd_RecursiveDeref( dd, p->pbCodes[i] );
    }
	Cudd_RecursiveDeref( dd, p->bSupp );
	free( p->pbFuncs );
	free( p->pbCodes );
	free( p );
}

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

  Synopsis    [Compares two nodes by the number of their fanins.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int fmImageMvPartCompareBddSize( Fm_ImagePartInfo_t ** ppPart1, Fm_ImagePartInfo_t ** ppPart2 )
{
    if ( (*ppPart1)->BddSize < (*ppPart2)->BddSize )
        return  1;
    if ( (*ppPart1)->BddSize > (*ppPart2)->BddSize )
        return -1;
    return 0;
}

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

  Synopsis    [Dereferences a set of functions]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void fmImageMvPartDeref( DdManager * dd, DdNode ** pbFuncs, int nFuncs )
{
    int i;
    for ( i = 0; i < nFuncs; i++ )
        Cudd_RecursiveDeref( dd, pbFuncs[i] );
}

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

  Synopsis    [Constrains the functions of one partition with the care set.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void fmImageMvPartConstrain( DdManager * dd, DdNode * bCare,
        DdNode ** pbFuncs, int nFuncs, DdNode * pbConstrs[], bool fUseAnd )
{
    int i;
    for ( i = 0; i < nFuncs; i++ )
    {
//        if ( fUseAnd )
//            pbConstrs[i] = Cudd_bddAnd( dd, pbFuncs[i], bCare ); 
//        else
            pbConstrs[i] = Cudd_bddConstrain( dd, pbFuncs[i], bCare ); 
        Cudd_Ref( pbConstrs[i] );
    }
}

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

  Synopsis    [Computes the MV support of the set of functions.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * fmImageMvPartSupport( DdManager * dd, DdNode ** pbFuncs, int nFuncs, Vmx_VarMap_t * pVmxGlo )
{
    DdNode * bTemp, * bComp, * bSupp;
    int i;

    bSupp = b1;   Cudd_Ref( bSupp );
    for ( i = 0; i < nFuncs; i++ )
    {
        bComp = Mvr_RelationSupportCube( dd, pbFuncs[i], pVmxGlo );   Cudd_Ref( bComp );
        bSupp = Cudd_bddAnd( dd, bTemp = bSupp, bComp );              Cudd_Ref( bSupp );
        Cudd_RecursiveDeref( dd, bTemp );  
        Cudd_RecursiveDeref( dd, bComp );
    }
    Cudd_Deref( bSupp );
    return bSupp;
}

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

  Synopsis    [Convolves the array of functions.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * fmImageMvPartConvolve( DdManager * dd, DdNode ** pbFuncs, DdNode ** pbCodes, int nFuncs )
{
    DdNode * bRes, * bComp, * bTemp;
    int i;
    bRes = b0;    Cudd_Ref( bRes );
    for ( i = 0; i < nFuncs; i++ )
    {
        bComp = Cudd_bddAnd( dd, pbFuncs[i], pbCodes[i] ); Cudd_Ref( bComp );
        bRes  = Cudd_bddOr ( dd, bTemp = bRes,  bComp );   Cudd_Ref( bRes );
        Cudd_RecursiveDeref( dd, bTemp );  
        Cudd_RecursiveDeref( dd, bComp );
    }
    Cudd_Deref( bRes );
    return bRes;
}

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

  Synopsis    [Computes the image of one partition.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * fmImageMvPartImage( DdManager * dd, DdNode * bCubeIn, Fm_ImagePartInfo_t * p )
{
    DdNode * bRes, * bPart;
    bPart = fmImageMvPartConvolve( dd, p->pbFuncs, p->pbCodes, p->nValues );  Cudd_Ref( bPart );
    bRes = Cudd_bddExistAbstract( dd, bPart, bCubeIn ); Cudd_Ref( bRes );
    Cudd_RecursiveDeref( dd, bPart );
    Cudd_Deref( bRes );
    return bRes;
}

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

  Synopsis    [Frees the array of partitions.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void fmImageMvPartArrayFree( DdManager * dd, array_t * pParts )
{
	int i;
	Fm_ImagePartInfo_t * pCur;
	// free the partitions
	for ( i = 0; i < array_n(pParts); i++ )
	{
		pCur = array_fetch( Fm_ImagePartInfo_t *, pParts, i );
		fmImageMvPartFree( dd, pCur );
	}
	array_free( pParts );
}


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

  Synopsis    [Sets the timeout.]

  Description []

  SideEffects [None]

  SeeAlso     []

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


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

  Synopsis    [Resets the timeout.]

  Description []

  SideEffects [None]

  SeeAlso     []

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

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////