fnccvr.c

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

                    break;
                }
            }

        // create the covers
        pCovers = ALLOC( Mvc_Cover_t *, nOutputValues );
        for ( i = 0; i < nOutputValues; i++ )
            if ( i != iCoverMax )
                pCovers[i] = Fnc_FunctionDeriveSopFromMdd( pManMvc, pMvr, pbIsets[i], pbIsets[i], pVm->nVarsIn );
            else
                pCovers[i] = NULL;
        // start the Cvr object using these covers
        pCvr = Cvr_CoverCreate( pVm, pCovers );
        FREE( pnCubesInIsets );
    }

    Mvr_RelationCofactorsDeref( pMvr, pbIsets, pVm->nVarsIn, nOutputValues );
    FREE( pbIsets );
    return pCvr;
}


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

  Synopsis    [Derives a single Mvc from one i-set of the relation.]

  Description [Takes the relation manager and the relation. Derives
  one MDD (i-set) of the relation as a positionally encoded Mvc
  using the MV variable map of the relation.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Mvc_Cover_t * Fnc_FunctionDeriveSopFromMdd( Mvc_Manager_t * pManMvc, Mvr_Relation_t * pMvr, DdNode * bMddOn, DdNode * bMddOnDc, int nVarsUsed )
{
    DdManager * dd = pMvr->pMan->pDdLoc;
    DdNode * zIsopLog;
    Mvc_Cover_t * Cover;
    // compute the binary ISOP
    zIsopLog = Extra_zddIsopCoverAlt( dd, bMddOn, bMddOnDc );   Cudd_Ref( zIsopLog );  
    // derive the SOP representation
    Cover = Fnc_FunctionDeriveSopFromZdd( pManMvc, pMvr, zIsopLog, nVarsUsed );
    Cudd_RecursiveDerefZdd( dd, zIsopLog );
    // the resulting cover may be not SCC-free
    return Cover;
}

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

  Synopsis    [Derives a single Mvc from one i-set of the relation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Mvc_Cover_t * Fnc_FunctionDeriveSopFromMddLimited( Mvc_Manager_t * pManMvc, Mvr_Relation_t * pMvr, DdNode * bMddOn, DdNode * bMddOnDc, int nVarsUsed )
{
    DdManager * dd = pMvr->pMan->pDdLoc;
    DdNode * zIsopLog;
    Mvc_Cover_t * Cover;
    // compute the binary ISOP
    zIsopLog = Extra_zddIsopCoverAltLimited( dd, bMddOn, bMddOnDc, 1000 );   
    if ( zIsopLog == NULL )
        return NULL;
    Cudd_Ref( zIsopLog );  
    // derive the SOP representation
    Cover = Fnc_FunctionDeriveSopFromZdd( pManMvc, pMvr, zIsopLog, nVarsUsed );
    Cudd_RecursiveDerefZdd( dd, zIsopLog );
    // the resulting cover may be not SCC-free
    return Cover;
}

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

  Synopsis    [Derives a single Mvc from one i-set of the relation using Espresso.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Mvc_Cover_t * Fnc_FunctionDeriveSopFromMddEspresso( Mvc_Manager_t * pManMvc, Mvr_Relation_t * pMvr, DdNode * bOn, DdNode * bOnDc, int nVarsUsed )
{
    DdManager * dd = pMvr->pMan->pDdLoc;
    Vm_VarMap_t * pVm = pMvr->pVmx->pVm;
    Mvc_Cover_t * pMvcOn, * pMvcDc;
    Mvc_Cover_t * pCover;
    DdNode * bDc, * zCover;

    // get the on-set as an ISOP
    zCover = Extra_zddIsopCoverAltLimited( dd, bOn, bOn, 1000 );
    if ( zCover == NULL )
        return NULL;
    Cudd_Ref( zCover );

    // cube out if the cover is too large
    if ( Cudd_zddCount(dd, zCover) > 500 )
    {
        Cudd_RecursiveDerefZdd( dd, zCover );
        return NULL;
    }
    pMvcOn = Fnc_FunctionDeriveSopFromZdd( pManMvc, pMvr, zCover, nVarsUsed );
    Cudd_RecursiveDerefZdd( dd, zCover );

    // get the dc-set as an ISOP
    bDc = Cudd_bddAnd( dd, bOnDc, Cudd_Not(bOn) );  Cudd_Ref( bDc );
    zCover = Extra_zddIsopCoverAltLimited( dd, bDc, bDc, 1000 );
    if ( zCover == NULL )
    {
        Cudd_RecursiveDeref( dd, bDc );
        Mvc_CoverFree( pMvcOn );
        return NULL;
    }
    Cudd_Ref( zCover );
    Cudd_RecursiveDeref( dd, bDc );

    // cube out if the cover is too large
    if ( Cudd_zddCount(dd, zCover) > 500 )
    {
        Cudd_RecursiveDerefZdd( dd, zCover );
        Mvc_CoverFree( pMvcOn );
        return NULL;
    }
    pMvcDc = Fnc_FunctionDeriveSopFromZdd( pManMvc, pMvr, zCover, nVarsUsed );
    Cudd_RecursiveDerefZdd( dd, zCover );

    // call Espresso
//    pCover = Cvr_IsetEspresso( pVm, pMvcOn, pMvcDc, 2, 1, 0 ); // SNOCOMP
    pCover = Cvr_IsetEspresso( pVm, pMvcOn, pMvcDc, 0, 1, 0 ); // ESPRESSO

    // remove temporary covers
    Mvc_CoverFree( pMvcOn );
    Mvc_CoverFree( pMvcDc );
    return pCover;
}

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

  Synopsis    [Derives a single Mvc_Cover_t * from one MDD (i-set) of the relation.]

  Description [Takes the relation manager and the relation. Derives
  one MDD (i-set) of the relation as a positionally encoded Mvc_Cover_t *
  using the MV variable map of the relation.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Mvc_Cover_t * Fnc_FunctionDeriveSopFromZdd( Mvc_Manager_t * pManMvc, Mvr_Relation_t * pMvr, DdNode * zIsop, int nVarsUsed )
{
    DdManager * dd = pMvr->pMan->pDdLoc;
    DdNode * zIsopLog, * zCubeLog, * zTemp;
    Vmx_VarMap_t * pVmx = pMvr->pVmx;
    Vm_VarMap_t * pVm = pVmx->pVm;
    int *  pZddVarsLog = pVmx->pMan->pArray;  // logarithmic encoding goes here
    int *  pZddVarsPos = pVm->pMan->pArray1;   // positional encoding goes here
    Mvc_Cover_t * pCover;
    Mvc_Cube_t * pCube;
    int nCubeBits, i;

    // start the cover in positional notation
    nCubeBits = pVm->pValuesFirst[nVarsUsed];
    pCover    = Mvc_CoverAlloc( pManMvc, nCubeBits );

    // translate the binary ISOP from the logarithmic into the positional notation
    zIsopLog = zIsop;      Cudd_Ref( zIsopLog );
    while ( zIsopLog != z0 )
    {
        // get a cube
        zCubeLog = Extra_zddSelectOneCube( dd, zIsopLog );         Cudd_Ref( zCubeLog );
        // subtract the cube from the cover
        zIsopLog = Cudd_zddDiff( dd, zTemp = zIsopLog, zCubeLog ); Cudd_Ref( zIsopLog );
        Cudd_RecursiveDerefZdd( dd, zTemp );

        // translate the cube into the array
        for ( i = 0; i < pVmx->nBits; i++ )
            pZddVarsLog[i] = 2;
        for ( zTemp = zCubeLog; zTemp != z1; zTemp = cuddT(zTemp) )
        {
            assert( zTemp->index < 2 * pVmx->nBits );
            if ( zTemp->index % 2 == 0 )
                pZddVarsLog[ zTemp->index / 2 ] = 1;
            else
                pZddVarsLog[ zTemp->index / 2 ] = 0;
        }
        Cudd_RecursiveDerefZdd( dd, zCubeLog );

        // convert logarithmic notation to positional notation
        Vmx_VarMapDecode( pVmx, pZddVarsLog, pZddVarsPos );

        // create the cube in the positional notation and add it to the cover
        pCube = Mvc_CubeAlloc( pCover );
        Mvc_CubeBitFill( pCube );
        for ( i = 0; i < nCubeBits; i++ )
            if ( pZddVarsPos[i] == 0 )
                Mvc_CubeBitRemove( pCube, i );
        // add the cube to the cover
        Mvc_CoverAddCubeTail( pCover, pCube );
    }
    Cudd_RecursiveDerefZdd( dd, zIsopLog );
    // make sure the cover is SCC-free
    Mvc_CoverContain( pCover );
    return pCover;
}


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

  Synopsis    [Derive MV ISOP in pos notation using the MDD and the variable map.]

  Description [Takes the variable map (pMap) and the MDD represented using
  this variable map (bMdd). Computes the binary ISOP for the binary encoded
  MDD and then translates it into the MV SOP and represents it using ZDD.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Fnc_FunctionDeriveZddFromMdd( Mvr_Relation_t * pMvr, DdNode * bMddOn, DdNode * bMddOnDc )
{
    Vmx_VarMap_t * pVmx = pMvr->pVmx;
    Vm_VarMap_t * pVm = pVmx->pVm;
    DdManager * dd = pMvr->pMan->pDdLoc;
    DdNode * zIsopLog, * zIsopPos, * zCubeLog, * zCubePos, * zTemp;
    int *  pZddVarsLog = pMvr->pVmx->pMan->pArray;  // logarithmic encoding goes here
    int *  pZddVarsPos = pMvr->pVmx->pVm->pMan->pArray1;   // positional encoding goes here
    int nValuesTotal, i;

    // get the parameters
    nValuesTotal = Vm_VarMapReadValuesNum( pVm );

    // compute the binary ISOP
    zIsopLog = Extra_zddIsopCover( dd, bMddOn, bMddOnDc );   Cudd_Ref( zIsopLog );  
    // start the cover in positional notation
    zIsopPos = z0;  Cudd_Ref( zIsopPos );

    // translate the ISOP from the logarithmic into the positional notation
    while ( zIsopLog != z0 )
    {
        // get a cube
        zCubeLog = Extra_zddSelectOneCube( dd, zIsopLog );         Cudd_Ref( zCubeLog );
        // subtract the cube from the cover
        zIsopLog = Cudd_zddDiff( dd, zTemp = zIsopLog, zCubeLog ); Cudd_Ref( zIsopLog );
        Cudd_RecursiveDerefZdd( dd, zTemp );

        // translate the cube into the array
        for ( i = 0; i < pVmx->nBits; i++ )
            pZddVarsLog[i] = 2;
        for ( zTemp = zCubeLog; zTemp != z1; zTemp = cuddT(zTemp) )
        {
            assert( zTemp->index < 2 * pVmx->nBits );
            if ( zTemp->index % 2 == 0 )
                pZddVarsLog[ zTemp->index / 2 ] = 1;
            else
                pZddVarsLog[ zTemp->index / 2 ] = 0;
        }
        Cudd_RecursiveDerefZdd( dd, zCubeLog );

        // convert logarithmic notation to positional notation
        Vmx_VarMapDecode( pVmx, pZddVarsLog, pZddVarsPos );

        // create the cube in the positional notation and add it to the cover
        zCubePos = Extra_zddCombination( dd, pZddVarsPos, nValuesTotal ); Cudd_Ref( zCubePos );
        zIsopPos = Cudd_zddUnion( dd, zTemp = zIsopPos, zCubePos );            Cudd_Ref( zIsopPos );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zCubePos );
    }
    Cudd_RecursiveDerefZdd( dd, zIsopLog );

    // ensure single-cube containment
    zIsopPos = Extra_zddMaximal( dd, zTemp = zIsopPos ); Cudd_Ref( zIsopPos );
    Cudd_RecursiveDerefZdd( dd, zTemp );

    Cudd_Deref( zIsopPos );
    return zIsopPos;
}


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