cvrfunc.c

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

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int
Cvr_CoverCountLiterals( Vm_VarMap_t * pVm, Mvc_Cover_t * pCover )
{
    Mvc_Cube_t * pCube;
    int nVarsIn, nValuesIn;
    int * pValues, iValues;
    bool fDontCare;
    int Counter;
    int i, v;

    // get the var map parameters
    nVarsIn   = Vm_VarMapReadVarsInNum( pVm );
    nValuesIn = Vm_VarMapReadValuesInNum( pVm );
    pValues   = Vm_VarMapReadValuesArray( pVm );

    // go through the cubes and count literals
    Counter = 0;
    Mvc_CoverForEachCube( pCover, pCube ) 
    {
        iValues = 0;
        for ( i = 0; i < nVarsIn; i++ )
        {
            // check it is true that the value set is a don't-care 
            fDontCare = 1;
            for ( v = 0; v < pValues[i]; v++ )
                if ( !Mvc_CubeBitValue( pCube, iValues + v ) ) 
                {
                    fDontCare = 0;
                    break;
                }
            if ( !fDontCare )
                Counter++;
            // add to the total number of values
            iValues += pValues[i];
        }
        assert( iValues == nValuesIn );
    }
    return Counter;
}

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

  Synopsis    [Counts the number of values in all MV literals.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int
Cvr_CoverCountLiteralValues( Vm_VarMap_t * pVm, Mvc_Cover_t * pCover )
{
    Mvc_Cube_t * pCube;
    int   nVarsIn, nValuesIn;
    int * pValues, iValues;
    int   nLitValues, Counter, i, v;

    // get the var map parameters
    nVarsIn   = Vm_VarMapReadVarsInNum( pVm );
    nValuesIn = Vm_VarMapReadValuesInNum( pVm );
    pValues   = Vm_VarMapReadValuesArray( pVm );

    // go through the cubes and count literals
    nLitValues = 0;
    Mvc_CoverForEachCube( pCover, pCube ) 
    {
        iValues = 0;
        for ( i = 0; i < nVarsIn; i++ )
        {
            // count the number of literal values in this cube
            Counter = 0;
            for ( v = 0; v < pValues[i]; v++ )
                if ( Mvc_CubeBitValue( pCube, iValues + v ) ) 
                {
                    Counter++;
                }
            // if not full-set then add the #values in this literal
            if ( Counter != pValues[i] )
                nLitValues += Counter;
            // add to the total number of values
            iValues += pValues[i];
        }
        assert( iValues == nValuesIn );
    }
    return nLitValues;
}

/**Function*************************************************************
  Synopsis    [Boolean OR of two binary covers]
  Description []
  SideEffects []
  SeeAlso     []
***********************************************************************/
Cvr_Cover_t *
Cvr_CoverOr  ( Cvr_Cover_t *pCvr1, Cvr_Cover_t *pCvr2 )
{
    bool fMvc1, fMvc2;
    Mvc_Cover_t **pIsets, *pMvc1, *pMvc2;
    Cvr_Cover_t *pCvrNew;
    
    if ( pCvr1==NULL || pCvr2==NULL) return NULL;
    
    if ( Vm_VarMapReadValuesOutNum(pCvr1->pVm) != 2 ||
         Vm_VarMapReadValuesOutNum(pCvr2->pVm) != 2 ) {
        return NULL;
    }
    
    /* derive onsets of the two covers */
    pIsets = ALLOC( Mvc_Cover_t *, 2 );
    fMvc1 = fMvc2 = 0;
    if ( pCvr1->ppCovers[1] ) {
        pMvc1 = pCvr1->ppCovers[1];
    } else {
        pMvc1 = Cvr_CoverComplement( pCvr1->pVm, pCvr1->ppCovers[0] );
        fMvc1 = 1;
    }
    if ( pCvr2->ppCovers[1] ) {
        pMvc2 = pCvr2->ppCovers[1];
    } else {
        pMvc2 = Cvr_CoverComplement( pCvr2->pVm, pCvr2->ppCovers[0] );
        fMvc2 = 1;
    }
    
    /* perform the disjunction */
    pIsets[1] = Mvc_CoverBooleanOr( pMvc1, pMvc2 );
    pIsets[0] = NULL;
    if ( fMvc1 ) Mvc_CoverFree( pMvc1 );
    if ( fMvc2 ) Mvc_CoverFree( pMvc2 );
    
    /* create the new cover */
    pCvrNew = Cvr_CoverCreate( pCvr1->pVm, pIsets );
    
    return pCvrNew;
}



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

  Synopsis    [Derive the collapsed cover.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Cvr_Cover_t * Cvr_CoverCreateCollapsed( Cvr_Cover_t * pCvrN, Cvr_Cover_t * pCvrF, 
        Vm_VarMap_t * pVmNew, int * pTransMapNInv, int * pTransMapF )
{
    Mvc_Data_t * pData;
    Cvr_Cover_t * pCvrNshift, * pCvrFshift, * pCvrNew;
    Mvc_Cover_t ** ppIsets, ** ppCofsN;
    Mvc_Cover_t * pIsetRes, * pMvcTemp;
    Vm_VarMap_t * pVmNewF;
    int * pTransMapN;
    int DefValueFinit, DefValueF, VarFofN, nVarsIn;
    int nValuesF, DefValueN, nValuesN;
    int v, i;

    // get parameters
    nValuesN  = Vm_VarMapReadValuesOutNum(pCvrN->pVm);
    nValuesF  = Vm_VarMapReadValuesOutNum(pCvrF->pVm);
    DefValueN = Cvr_CoverReadDefault(pCvrN);
    DefValueF = Cvr_CoverReadDefault(pCvrF);
    VarFofN   = pTransMapF[ Vm_VarMapReadVarsInNum(pCvrF->pVm) ];
    nVarsIn   = Vm_VarMapReadVarsInNum(pVmNew);

    // inverse pTransMapNInv
    pTransMapN = ALLOC( int, nVarsIn );
    for ( i = 0; i < nVarsIn; i++ )
        if ( pTransMapNInv[i] >= 0 )
            pTransMapN[pTransMapNInv[i]] = i;

    // create the shifted var map for F
    if ( nValuesN != nValuesF )
        pVmNewF = Vm_VarMapCreateOneDiff( pVmNew, nVarsIn, nValuesF );
    else
        pVmNewF = pVmNew;

    // expand the cover of the node to match the new map
    pCvrNshift = Cvr_CoverCreateAdjusted( pCvrN, pVmNew,  pTransMapN ); 
    // remap the cover of the fanin (pFanin) to match the new map
    pCvrFshift = Cvr_CoverCreateAdjusted( pCvrF, pVmNewF, pTransMapF ); 
    FREE( pTransMapN );


    // get any cover of pCvrFshift
    pMvcTemp = (DefValueF != 0)? pCvrFshift->ppCovers[0]: pCvrFshift->ppCovers[1];
    // get the MV data for the new man
    pData = Mvc_CoverDataAlloc( pVmNew, pMvcTemp );

    // if the cover of node N has literals, which include the def value of F, 
    // we need the def value cover of F explicitly
    DefValueFinit = DefValueF;
    if ( Cvr_CoverCountLitsWithValue(pData, pCvrNshift, VarFofN, DefValueF) )
    {
        if ( DefValueF >= 0 )
        {
            Cvr_CoverComputeDefault( pCvrFshift );
            DefValueF = -1;
        }
    }

    // if the default value is used in one of the covers, and one of them is ND
    // we need to get rid of the default value and have all i-sets present
    if ( (DefValueF >= 0 || DefValueN >= 0) && Cvr_CoverIsND(pData, pCvrFshift) )
    {
        if ( DefValueN >= 0 )
        {
            Cvr_CoverComputeDefault( pCvrNshift );
            DefValueN = -1;
        }
        if ( DefValueF >= 0 )
        {
            Cvr_CoverComputeDefault( pCvrFshift );
            DefValueF = -1;
        }
    }

    // start the resulting i-sets
    ppIsets = ALLOC( Mvc_Cover_t *, nValuesN );
    // for each value of N, compose the covers
    for ( v = 0; v < nValuesN; v++ )
    {
        if ( pCvrNshift->ppCovers[v] == NULL )
        {
            ppIsets[v] = NULL;
            continue;
        }
        // cofactor the corresponding i-set of N w.r.t the fanin var
        // and compute the cubes that do not depend on this var (ppCofsN[nValuesF])
        ppCofsN = Mvc_CoverCofactors( pData, pCvrNshift->ppCovers[v], VarFofN );

        // convolve the cofactors
        pIsetRes = Mvc_CoverClone( pCvrNshift->ppCovers[v] );
        for ( i = 0; i < nValuesF; i++ )
        {
            if ( Mvc_CoverReadCubeNum(ppCofsN[i]) > 0 )
            {
                // there are cubes, there should be the corresponding i-set of F-shifted
                assert( pCvrFshift->ppCovers[i] );
                // multiply
                Mvc_CoverIntersectCubes( pData, ppCofsN[i], pCvrFshift->ppCovers[i] );
                // add the cubes
                Mvc_CoverAppendCubes( pIsetRes, ppCofsN[i] );
            }
            Mvc_CoverFree( ppCofsN[i] );
        }
        // add the cubes that do not depend on this var
        Mvc_CoverAppendCubes( pIsetRes, ppCofsN[nValuesF] );
        Mvc_CoverFree( ppCofsN[nValuesF] );
        FREE( ppCofsN );
        // compress the cover
        Mvc_CoverContain( pIsetRes );
        Mvc_CoverDist1Merge( pData, pIsetRes );
        // set the cover
        ppIsets[v] = pIsetRes;
    }

    // create the new Cover
    pCvrNew = Cvr_CoverCreate( pVmNew, ppIsets );

    // free storage
    Mvc_CoverDataFree( pData, pMvcTemp );
    Cvr_CoverFree( pCvrNshift );
    Cvr_CoverFree( pCvrFshift );

    // remove the default value of F
//    if ( DefValueFinit >= 0 && DefValueF < 0 )
//        Cvr_CoverSetDefault( pCvrF, DefValueFinit );

    return pCvrNew;
}

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

  Synopsis    [Returns the cover with the appended variables.]

  Description [The original cover is expanded by adding some variables.
  These variables are the additional variables in pVmNew, compared to
  pCvr->pVm. The resulting cover is the same as the original one, except
  that it contains the additional variables present as full literals
  in every cube.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Cvr_Cover_t * Cvr_CoverCreateExpanded( Cvr_Cover_t * pCvr, Vm_VarMap_t * pVmNew )
{
    Mvc_Cover_t ** ppIsets;
    int  iVal, nVal;
    
    nVal = Vm_VarMapReadValuesOutNum(pCvr->pVm);
    ppIsets = ALLOC( Mvc_Cover_t *, nVal );
    for ( iVal = 0; iVal < nVal; ++iVal ) 
    {
        if ( pCvr->ppCovers[iVal] == NULL ) 
        {
            ppIsets[iVal] = NULL;
            continue;
        }
        ppIsets[iVal] = Mvc_CoverCreateExpanded( pCvr->ppCovers[iVal], pVmNew );
    }
    return Cvr_CoverCreate( pVmNew, ppIsets );
}



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

  Synopsis    [Checks if the given Cvr is non-deterministic.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
bool Cvr_CoverIsND( Mvc_Data_t * pData, Cvr_Cover_t * pCvr )
{
    int i, k, nValues;
    nValues = Vm_VarMapReadValuesOutNum(pCvr->pVm);
    for ( i = 0; i < nValues; i++ )
        for ( k = i + 1; k < nValues; k++ )
            if ( pCvr->ppCovers[i] && pCvr->ppCovers[k] )
                if ( Mvc_CoverIsIntersecting( pData, pCvr->ppCovers[i], pCvr->ppCovers[k] ) )
                    return 1;
    return 0;
}

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

  Synopsis    [Count the cubes with non-trivial literals with the given value.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cvr_CoverCountLitsWithValue( Mvc_Data_t * pData, Cvr_Cover_t * pCvr, int iVar, int iValue )
{
    int v, Counter, nValuesOut;
    Counter = 0;
    nValuesOut = Vm_VarMapReadValues( pCvr->pVm, Vm_VarMapReadVarsInNum(pCvr->pVm) );
    for ( v = 0; v < nValuesOut; v++ )
        if ( pCvr->ppCovers[v] )
            Counter += Mvr_CoverCountLitsWithValue( pData, pCvr->ppCovers[v], iVar, iValue );
    return Counter;
}