mvrutils.c

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

    // extend the local manager if necessary
    if ( dd->size < pVmxNew->nBits )
    {
        for ( i = dd->size; i < pVmxNew->nBits + 10; i++ )
            Cudd_bddIthVar( dd, i );
        Cudd_zddVarsFromBddVars( dd, 2 );
    }

    // set up the permutation array
    pPermute = ALLOC( int, dd->size );
    for ( v = 0; v < nVmOld; v++ )
        if ( pVarTrans[v] != -1 )
        {
            assert( pVmOld->pValues[v] == pVmNew->pValues[pVarTrans[v]] );
            for ( b = 0; b < pVmxOld->pBits[v]; b++ )
            {
                index = pVmxOld->pBitsOrder[ pVmxOld->pBitsFirst[v] + b ];
                assert( index >= 0 && index < pVmxOld->nBits );
                pPermute[index] = pVmxNew->pBitsOrder[ pVmxNew->pBitsFirst[pVarTrans[v]] + b ];
            }
        }
    // remap the function
//  bRes = Cudd_bddPermute( dd, bFunc, pPermute ); // returns non-referenced
    bRes = Extra_Permute( pMvr->pMan->pPerm, dd, bFunc, pPermute );  
    free( pPermute );
    return bRes;
}

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

  Synopsis    [Forces the equality of the two MV variables in Mvr.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Mvr_RelationMakeVarsEqual( Mvr_Relation_t * pMvr, int iVar1, int iVar2 )
{
    DdManager * dd;
    DdNode ** pbCofs, ** pbCodes;
    DdNode * bRelCol, * bComp, * bTemp;
    int nValues, i;

    // get the DD manager
    dd = pMvr->pMan->pDdLoc;

    // get the number of values
    nValues = pMvr->pVmx->pVm->pValues[iVar1];
    assert( nValues == pMvr->pVmx->pVm->pValues[iVar2] );

    // cofactor the relation w.r.t. the first var
    pbCofs = ALLOC( DdNode *, nValues );
    Mvr_RelationCofactorsDerive( pMvr, pbCofs, iVar1, nValues );
    // get the codes w.r.t. the second var
    pbCodes = Vmx_VarMapEncodeVar( dd, pMvr->pVmx, iVar2 );

    // create the resulting relation
    bRelCol = b0;    Cudd_Ref( bRelCol );
    for ( i = 0; i < nValues; i++ )
    {
        bComp = Cudd_bddAnd( dd, pbCofs[i], pbCodes[i] );     Cudd_Ref( bComp );
        bRelCol = Cudd_bddOr( dd, bTemp = bRelCol, bComp );   Cudd_Ref( bRelCol );
        Cudd_RecursiveDeref( dd, bComp );
        Cudd_RecursiveDeref( dd, bTemp );
    }

    // deref the cofactors
    Mvr_RelationCofactorsDeref( pMvr, pbCofs, iVar1, nValues );
    FREE( pbCofs );
    // deref the codes
    Vmx_VarMapEncodeDeref( dd, pMvr->pVmx, pbCodes );

    // deref the old relation
    Cudd_RecursiveDeref( dd, pMvr->bRel );
    pMvr->nBddNodes = BDD_NODES_UNKNOWN;
    // set the new relation
    pMvr->bRel = bRelCol;  // comes referenced
}


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

  Synopsis    [Reorders the BEMDD representing the relation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
bool Mvr_RelationReorder( Mvr_Relation_t * pMvr )
{
    DdManager * dd;
    Vmx_VarMap_t * pVmx;
    Vmx_VarMap_t * pVmxNew;
    Vm_VarMap_t  * pVm;
    DdNode * bRelNew;
    int * pOrder, * pOrderInv, * pBitOrderNew;
    int i;

    if ( pMvr == NULL )
        return 0;

    // start the order array
    dd = pMvr->pMan->pDdLoc;
    pVmx = pMvr->pVmx;
    pVm = pVmx->pVm;
    pOrder = Vm_VarMapGetStorageArray1( pVm );
    for ( i = 0; i < pVmx->nBits; i++ )
        pOrder[i] = -1;

    // perform variable reordering
    bRelNew = Extra_Reorder( pMvr->pMan->pReo, dd, pMvr->bRel, pOrder );  Cudd_Ref( bRelNew );

    // invert the variable order
    pOrderInv = Vm_VarMapGetStoragePermute( pVm );
    for ( i = 0; i < pVmx->nBits; i++ )
        if ( pOrder[i] >= 0 )
            pOrderInv[ pOrder[i] ] = i;
        else
            pOrderInv[i] = i;

    // create the new bit order
    // start with the original order
    pBitOrderNew = Vm_VarMapGetStorageArray2( pVm );
    for ( i = 0; i < pVmx->nBits; i++ )
        if ( pOrderInv[i] >= 0 )
            pBitOrderNew[i] = pOrderInv[ pVmx->pBitsOrder[i] ];
        else
            pBitOrderNew[i] = pVmx->pBitsOrder[i];

    // create the new ext var map
    pVmxNew = Vmx_VarMapLookup( pVmx->pMan, pVm, pVmx->nBits, pBitOrderNew );
    if ( pVmxNew == pVmx )
    { // no change
        assert( bRelNew == pMvr->bRel );
        Cudd_RecursiveDeref( dd, bRelNew );
        return 0;
    }

    // update the variable map
    pMvr->pVmx = pVmxNew;
    // update the BDD
    Cudd_RecursiveDeref( dd, pMvr->bRel );
    pMvr->bRel = bRelNew; // takes ref
    pMvr->nBddNodes = BDD_NODES_UNKNOWN;
    return 1;
}


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

  Synopsis    [Returns the number of binary variables in the support.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Mvr_RelationSupportBinarySize( Mvr_Relation_t * pMvr )
{
    int nSuppSize;
    // get the number of nodes and the support size of the relation
    pMvr->nBddNodes = Extra_DagSizeSuppSize( pMvr->bRel, &nSuppSize );
    assert( nSuppSize <= pMvr->pVmx->nBits );
    return nSuppSize;
}

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

  Synopsis    [Check if the binary variables form a contiguous range.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
bool Mvr_RelationSupportBinaryIsRange( Mvr_Relation_t * pMvr )
{
    int * pSupport;
    int i;

    pSupport = ALLOC( int, ddMax(pMvr->pMan->pDdLoc->size, pMvr->pMan->pDdLoc->sizeZ) );
    Extra_SupportArray( pMvr->pMan->pDdLoc, pMvr->bRel, pSupport );

    for ( i = 0; i < pMvr->pVmx->nBits; i++ )
        if ( pSupport[i] == 0 )
        {
            free( pSupport );
            return 0;
        }
    free( pSupport );
    return 1;
}

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

  Synopsis    [Returns 1 if the relation's support is okay.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
bool Mvr_RelationCheckSupport( Mvr_Relation_t * pMvr )
{
    int * pSupport;
    int i;

    pSupport = ALLOC( int, ddMax(pMvr->pMan->pDdLoc->size, pMvr->pMan->pDdLoc->sizeZ) );
    Extra_SupportArray( pMvr->pMan->pDdLoc, pMvr->bRel, pSupport );

    // makes sure the support does not depend on variables 
    // below the lowest allowed variable for the given relation
    for ( i = pMvr->pVmx->nBits; i < pMvr->pMan->pDdLoc->size; i++ )
        if ( pSupport[i] )
        {
            fprintf( stdout, "Relation's support is not correct.\n" );
            free( pSupport );
            return 0;
        }
    free( pSupport );
    return 1;
}

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

  Synopsis    [Computes the support of MV relation in terms of MV variables.]

  Description [Takes an MV relation and the array where the resulting 
  support is written. Entry 1 means var is in the support. Entry 0 means
  var is not in the support. This procedure returns the total number of 
  MV variables in the support. In many ways, this procedure is similar 
  to Extra_SupportArray, except that it considers MV variables.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Mvr_RelationSupport( Mvr_Relation_t * pMvr, int * pSuppMv )
{
    Vm_VarMap_t * pVm;
    Vmx_VarMap_t * pVmx;
    int * pSuppBin;
    int nSuppMv;
    int nVars;
    int v, b;

    // compute the binary support of the relation
    pSuppBin = ALLOC( int, ddMax(pMvr->pMan->pDdLoc->size, pMvr->pMan->pDdLoc->sizeZ) );
    Extra_SupportArray( pMvr->pMan->pDdLoc, pMvr->bRel, pSuppBin );

    // find MV variables that are not in the binary support
    pVm   = pMvr->pVmx->pVm;
    pVmx  = pMvr->pVmx;
    nVars = pVm->nVarsIn + pVm->nVarsOut;
    memset( pSuppMv, 0, sizeof(int) * nVars );

    // go through the input MV variables
    nSuppMv = 0;
    for ( v = 0; v < pVm->nVarsIn; v++ )
        for ( b = 0; b < pVmx->pBits[v]; b++ ) // go though every bit of this MV variable
            if ( pSuppBin[ pVmx->pBitsOrder[ pVmx->pBitsFirst[v] + b ] ] )
            {
                pSuppMv[v] = 1;
                nSuppMv++;
                break;
            }
    free( pSuppBin );
    // the output vars are always present
    for ( v = pVm->nVarsIn; v < nVars; v++ )
    {
        pSuppMv[v] = 1;
        nSuppMv++;
    }
    return nSuppMv;
}

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

  Synopsis    [Computes the support of MV relation in terms of MV variables.]

  Description [Returns the cube composed of the binary variables selected
  in the following way. If some *input* MV variable is present in the current 
  support of the relation (bRel), the first binary variable used to encode
  this MV variable is included in the resulting cube. This function is useful 
  for image computation.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Mvr_RelationSupportCube( DdManager * dd, DdNode * bFuncs, Vmx_VarMap_t * pVmx )
{
    DdNode * bSupp, * bVar, * bTemp;
    Vm_VarMap_t * pVm;
    int * pSuppBin;
    int v, b;

    // compute the binary support of the relation
    pSuppBin = ALLOC( int, ddMax(dd->size, dd->sizeZ) );
    Extra_SupportArray( dd, bFuncs, pSuppBin );

    // find MV variables that are not in the binary support
    pVm   = pVmx->pVm;
    // start the MV support
    bSupp = b1;  Cudd_Ref( bSupp );
    // go through the input MV variables
    for ( v = 0; v < pVm->nVarsIn; v++ )
        for ( b = 0; b < pVmx->pBits[v]; b++ ) // go though every bit of this MV variable
            if ( pSuppBin[ pVmx->pBitsOrder[ pVmx->pBitsFirst[v] + b ] ] )
            {
                bVar  = dd->vars[ pVmx->pBitsOrder[ pVmx->pBitsFirst[v] ] ];
                bSupp = Cudd_bddAnd( dd, bTemp = bSupp, bVar );  Cudd_Ref( bSupp );
                Cudd_RecursiveDeref( dd, bTemp );
                break;
            }
    free( pSuppBin );
    Cudd_Deref( bSupp );
    return bSupp;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Mvr_RelationAddDontCare( Mvr_Relation_t * pMvr, Mvr_Relation_t * pMvrDc )
{
    Vm_VarMap_t * pVm;
    DdNode * pbIsets[2];
    DdNode * bTemp;
    int nOutputValues;

    pVm = pMvr->pVmx->pVm;
    nOutputValues = Vm_VarMapReadValuesOutNum( pVm );
    assert( nOutputValues == 2 );

    // cofactor w.r.t. the output variable
    Mvr_RelationCofactorsDerive( pMvrDc, pbIsets, pVm->nVarsIn, 2 );

    pMvr->bRel = Cudd_bddOr( pMvr->pMan->pDdLoc, bTemp = pMvr->bRel, pbIsets[1] );
    Cudd_Ref( pMvr->bRel );
    Cudd_RecursiveDeref( pMvr->pMan->pDdLoc, bTemp );
    pMvr->nBddNodes = BDD_NODES_UNKNOWN;

    Mvr_RelationCofactorsDeref( pMvr, pbIsets, pVm->nVarsIn, 2 );
}

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

  Synopsis    [Determinizes the relation.]

  Description [Returns 1, if determinization was applied. Returns 0
  if determinization was not necessary.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
bool Mvr_RelationDeterminize( Mvr_Relation_t * pMvr )
{
    DdManager * dd = pMvr->pMan->pDdLoc;
    Vm_VarMap_t * pVm;
    DdNode ** pbIsets, * bSum, * bTemp;
    int nOutputValues, i, k;
    bool fNonDeterminstic;

    // get the MV var map of this relation
    pVm = pMvr->pVmx->pVm;
    // get the number of output values
    nOutputValues = Vm_VarMapReadValuesOutput( pVm );

    // allocate room for cofactors
    pbIsets = ALLOC( DdNode *, nOutputValues );
    // set the i-sets w.r.t the last variable
    Mvr_RelationCofactorsDerive( pMvr, pbIsets, pVm->nVarsIn, nOutputValues );

    // check the i-sets for overlapping
    fNonDeterminstic = 0;
    for ( i = 0; i < nOutputValues; i++ )
        for ( k = i+1; k < nOutputValues; k++ )
            if ( !Cudd_bddLeq( dd, pbIsets[i], Cudd_Not(pbIsets[k]) ) ) // they intersect
            {
                fNonDeterminstic = 1;
                break;
            }

    if ( fNonDeterminstic )
    { // apply greedy determinization
        // start the sum of all i-sets by adding the first i-set
        bSum = pbIsets[0]; Cudd_Ref( bSum );
        // go through other i-sets
        for ( i = 1; i < nOutputValues; i++ )
        {
            if ( !Cudd_bddLeq( dd, pbIsets[i], Cudd_Not(bSum) ) ) 
            { // i-set number i intersects with the sum
                // sharp this i-set with the sum of other i-sets
                pbIsets[i] = Cudd_bddAnd( dd, bTemp = pbIsets[i], Cudd_Not(bSum) ); Cudd_Ref( pbIsets[i] );
                Cudd_RecursiveDeref( dd, bTemp );
            }
            // add this i-set to the sum
            bSum = Cudd_bddOr( dd, bTemp = bSum, pbIsets[i] ); Cudd_Ref( bSum );
            Cudd_RecursiveDeref( dd, bTemp );
        }
        assert( bSum == b1 );
        // complete domain should be covered
        // otherwise, the relation was not well-defined (should never happen)
        // or some other bug crept in
        Cudd_RecursiveDeref( dd, bSum );
    }

    // derive the relation from i-sets
    Mvr_RelationCofactorsDeriveRelation( pMvr, pbIsets, pVm->nVarsIn, nOutputValues );
    Mvr_RelationCofactorsDeref( pMvr, pbIsets, pVm->nVarsIn, nOutputValues );
    FREE( pbIsets );

    // in any case, the relation became deterministic
    pMvr->NonDet = MVR_DETERM;
    return fNonDeterminstic;
}

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