simpodc.c

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

    }
    
    /* MDD manager for the local space */
    pMvrFunc = Ntk_NodeGetFuncMvr(pNode);
    mgLoc = Mvr_RelationReadDd(pMvrFunc);
    
    /* obtain the MDD array for the isets */
    pVm     = Mvr_RelationReadVm( pMvrFunc );
    pVmx    = Mvr_RelationReadVmx( pMvrFunc );
    bRel    = Mvr_RelationReadRel( pMvrFunc );
    bCube   = Vmx_VarMapCharCube( mgLoc, pVmx, nInputs );
    Cudd_Ref( bCube );
    nValues = Vm_VarMapReadValuesOutNum( pVm );
    
    /* issue to study:
       MODC formulea (ICCAD'00) works only for deterministic MV functions;
       need to remove the non-det part from MODC;
       (\exist f) (\forany y) R(x,y,f)
    */
    
    bNondet = NULL;
    if ( Mvr_RelationIsND( pMvrFunc ) ) {
        
        bNondet = Cudd_ReadLogicZero( mgLoc );
        Cudd_Ref( bNondet );
        
        pbIsets = ALLOC( DdNode *, nValues );
        Mvr_RelationCofactorsDerive( pMvrFunc, pbIsets, nInputs, nValues );
        
        /* initialize the sum to be 0-set */
        bSum = pbIsets[0];
        Cudd_Ref( bSum );
        
        /* accumulate the overlapping sets */
        for ( i = 1; i < nValues; i++ ) {
            
            /* intersect with the sum */
            bQuan = Cudd_bddAnd( mgLoc, bSum, pbIsets[i] );
            Cudd_Ref( bQuan );
            
            /* include the overlap into the nondet part */
            bTemp = Cudd_bddOr( mgLoc, bNondet, bQuan );
            Cudd_Ref( bTemp );
            Cudd_RecursiveDeref( mgLoc, bQuan );
            Cudd_RecursiveDeref( mgLoc, bNondet );
            bNondet = bTemp;
            
            /* include iset[i] into the sum */
            if ( i != (nValues - 1) ) {
                bTemp = Cudd_bddOr( mgLoc, bSum, pbIsets[i] );
                Cudd_Ref( bTemp );
                Cudd_RecursiveDeref( mgLoc, bSum );
                bSum = bTemp;
            }
        }
        Cudd_RecursiveDeref( mgLoc, bSum );
        Mvr_RelationCofactorsDeref( pMvrFunc, pbIsets, nInputs, nValues );
        FREE( pbIsets );
        
        /* remove the part that is truly don't cares */
        bQuan = Mvr_RelationQuantifyUniv( pMvrFunc, bRel, nInputs );
        Cudd_Ref( bQuan );
        
        bTemp = Cudd_bddAnd( mgLoc, bNondet, Cudd_Not( bQuan ) );
        Cudd_Ref( bTemp );
        Cudd_RecursiveDeref( mgLoc, bQuan );
        Cudd_RecursiveDeref( mgLoc, bNondet );
        bNondet = bTemp;
    }
    
    /* compute MSPF for each fanin */
    Ntk_NodeForEachFaninWithIndex( pNode, pPin, pFanin, iFanin ) {
        
        if ( Ntk_NodeIsCi( pFanin ) )
            continue;
        
        bQuan = Mvr_RelationQuantifyUniv( pMvrFunc, bRel, iFanin );
        Cudd_Ref( bQuan );
        
        bMspf = Cudd_bddExistAbstract( mgLoc, bQuan, bCube );
        Cudd_Ref( bMspf );
        Cudd_RecursiveDeref( mgLoc, bQuan );
        
        if ( bNondet ) {
            bMspf = SimpCleanNondet( mgLoc, pNode, pMvrFunc, iFanin, bMspf, bNondet );
        }
        
        pSimp->lMspf[iFanin] = bMspf;
    }
    
    Cudd_RecursiveDeref( mgLoc, bCube );
    
    /* deallocate memory of MDD isets */
    if ( bNondet ) {
       Cudd_RecursiveDeref( mgLoc, bNondet );
    }
    return;
}


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

  Synopsis    [Filter out variables that are not in the hash table list.]
  
  Description [Given a MDD, which represents a don't care set. Assume all
  variables in the support are already CI's. All variables not in the TFI set
  are exitentially quantified out.]

  SideEffects [the original MDD F is freed afterwards]

  SeeAlso     []

******************************************************************************/
DdNode *
SimpFilterGlobal(
    Simp_Info_t *pInfo,
    DdNode       *bFunc,
    st_table     *stNodes)
{
    int iSeq, *pSup, nVars;
    char          *dummy;
    Ntk_Node_t    *pStick;
    DdManager     *mg;
    DdNode        *bTemp, *bResult, *bCube;
    
    mg    = pInfo->ddmg;
    if ( bFunc == Cudd_ReadOne( mg ) ||
         bFunc == Cudd_ReadLogicZero( mg ) ) {
        return bFunc;
    }
    
    /* access information */
    pStick = NULL;
    nVars = Cudd_ReadSize( mg );
    pSup  = Cudd_SupportIndex( mg, bFunc );
    bCube = Cudd_ReadOne( mg );
    Cudd_Ref( bCube );
    
    for ( iSeq = 0; iSeq < nVars; ++iSeq ) {
        
        if ( pSup[iSeq] > 0 ) {
            
            /* new test if it is in stNodes as well */
            if ( pStick == pInfo->ppNodes[iSeq] ||
                 !st_lookup(stNodes, (char *)pInfo->ppNodes[iSeq], &dummy)) {
                
                /* accumulate the variables in a cube */
                bTemp = Cudd_bddAnd( mg, bCube, Cudd_bddIthVar(mg, iSeq) );
                Cudd_Ref( bTemp );
                Cudd_RecursiveDeref( mg, bCube );
                bCube  = bTemp;
                
                pStick = pInfo->ppNodes[iSeq];
            }
        }
    }
    
    bResult = Cudd_bddUnivAbstract( mg, bFunc, bCube );
    Cudd_Ref( bResult );
    Cudd_RecursiveDeref( mg, bFunc );
    Cudd_RecursiveDeref( mg, bCube );
    
    FREE(pSup);
    return bResult;
}


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

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

  Synopsis    [Makes the MSPF compatible with a previous visited edge.]
  
  Description [Makes the MSPF compatible with a previous visited edge. Given
  the current CODC of a node, and another previously visited node, compute its
  compatible subset. Assume both are in the global MDD manager space.]

  SideEffects [The original codc set is freed after wards.]

  SeeAlso     []

******************************************************************************/
bool
SimpComputeCspf(
    Simp_Info_t    * pInfo,
    DdNode        ** pbMspf,   /* boolean difference in local DD domain   */
    DdNode        ** pbCodc,   /* current CODC in global DD domain        */
    Mvr_Relation_t * pMvrFout, /* fanout relation where pMspf was derived */
    DdManager      * mgLoc,    /* local DD manager for pMspf              */
    Ntk_Node_t     * pNode,    /* current node being worked on            */
    Ntk_Node_t     * pOther,   /* neighbor node being compatiblized       */
    int              iOther )
{
    DdNode         *bQuan, *bTemp, *bOthDc;
    DdNode         *bCodc, *bMspf;
    DdManager      *mg;
    Simp_Node_t    *pSimpThi, *pSimpOth;
    
    /* global MDD manager */
    mg = pInfo->ddmg;
    bCodc = *pbCodc;
    bMspf = *pbMspf;
    
    /* retrieve the computed codc from the other node */
    pSimpThi = Simp_DaemonGetNodeData( pNode );
    pSimpOth = Simp_DaemonGetNodeData( pOther );
    bOthDc   = pSimpOth->pCodc;
    if ( bOthDc==NIL(DdNode) || bOthDc == Cudd_ReadLogicZero(mg) ) {
        return FALSE;
    }
    
    if (pInfo->verbose) {
        printf("Compatability: %s(%d) ", Ntk_NodeGetNamePrintable(pOther),
               Cudd_DagSize(bOthDc) );
        printf("<- %s(%d)\n", Ntk_NodeGetNamePrintable(pNode),
               bCodc?Cudd_DagSize(bCodc):0 );
    }
    
    /* compute (ANYx)CODC - universal quantification (in the local domain) */
    if ( bMspf && bMspf != Cudd_ReadLogicZero( mgLoc ) ) {
        
        bQuan = Mvr_RelationQuantifyUniv( pMvrFout, bMspf, iOther );
        Cudd_Ref( bQuan );
        Cudd_RecursiveDeref( mgLoc, bMspf );
        *pbMspf = bQuan;
    }
    
    /* compute Care(x) * CODC: (in the global domain ok) */
    if ( bCodc && bCodc != Cudd_ReadLogicZero( mg ) ) {
        
        bTemp = Cudd_bddAnd( mg, Cudd_Not(bOthDc), bCodc ); Cudd_Ref( bTemp );
        Cudd_RecursiveDeref( mg, bCodc );
        *pbCodc = bTemp;
    }
    
    return TRUE;
}

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

  Synopsis    [Remove non-deterministic parts from MODC]
  
  Description [Remove non-deterministic parts from MODC, using equation :
  ( \forall x \not{NonDet()} \cdot MSPF )]
  
  SideEffects []
  SeeAlso     []

******************************************************************************/
DdNode *
SimpCleanNondet(
    DdManager      *mg,
    Ntk_Node_t     *pNode,
    Mvr_Relation_t *pMvrFunc,
    int             iFanin,
    DdNode         *bMspf,
    DdNode         *bNondet)
{
    DdNode *bTemp, *bQuan;
    
    if ( bMspf == NIL(DdNode) ) return NIL(DdNode);
    
    bQuan = Mvr_RelationQuantifyUniv( pMvrFunc, Cudd_Not(bNondet), iFanin );
    Cudd_Ref( bQuan );
    
    bTemp = Cudd_bddAnd( mg, bMspf, bQuan);
    Cudd_Ref( bTemp );
    
    Cudd_RecursiveDeref( mg, bMspf );
    Cudd_RecursiveDeref( mg, bQuan );
    
    return bTemp;
}


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

  Synopsis    [Adjust the MSPF with the fanout's CODC]
  
  Description [Compute MSPF that is independent of the fanout's
  implementation, using formulea: (MSPF + \exist x_i CODC) given by
  Brayton, ICCAD'01.]

  SideEffects []
  SeeAlso     []

******************************************************************************/
DdNode *
SimpAdjustMspf( DdManager * ddmg, DdNode * pMspf, DdNode * pCodcFout )
{
    DdNode *pMspfNew;
    
    /* since we are in the global space already,
       thus don't need to quantify out x_i
    */
    pMspfNew = Cudd_bddOr( ddmg, pMspf, pCodcFout );
    Cudd_Ref( pMspfNew );
    
    return pMspfNew;
}