ntkiglobal.c

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

    int i, v;
    ppMdds = ALLOC( DdNode **, nOuts );
    for ( i = 0; i < nOuts; i++ )
    {
        ppMdds[i] = ALLOC( DdNode *, pValues[i] );
        for ( v = 0; v < pValues[i]; v++ )
        {
            ppMdds[i][v] = Cudd_bddOr( dd, ppMdds1[i][v], ppMdds2[i][v] );  Cudd_Ref( ppMdds[i][v] );
        }
    }
    return ppMdds;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode *** Ntk_NetworkGlobalMddConvertExdc( DdManager * dd, int * pValues, int nOuts, DdNode *** ppMddsExdc )
{
    DdNode *** ppMdds;
    int * pValuesExdc;
    int i, v;
    ppMdds = ALLOC( DdNode **, nOuts );
    for ( i = 0; i < nOuts; i++ )
    {
        ppMdds[i] = ALLOC( DdNode *, pValues[i] );
        for ( v = 0; v < pValues[i]; v++ )
        {
            ppMdds[i][v] = ppMddsExdc[i][1];  Cudd_Ref( ppMdds[i][v] );
        }
    }

    pValuesExdc = ALLOC( int, nOuts );
    for ( i = 0; i < nOuts; i++ )
        pValuesExdc[i] = 2;
    Ntk_NetworkGlobalMddDeref( dd, pValuesExdc, nOuts, ppMddsExdc );
    FREE( pValuesExdc );

    return ppMdds;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ntk_NetworkGlobalMddMinimize( DdManager * dd, int * pValues, int nOuts, DdNode *** ppMdds1, DdNode *** ppMdds2 )
{
    DdNode * bTemp;
    int i, v;
    for ( i = 0; i < nOuts; i++ )
        for ( v = 0; v < pValues[i]; v++ )
        {
            ppMdds1[i][v] = Cudd_bddRestrict( dd, bTemp = ppMdds1[i][v], Cudd_Not(ppMdds2[i][v]) );  Cudd_Ref( ppMdds1[i][v] );
            Cudd_RecursiveDeref( dd, bTemp );
        }
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ntk_NetworkGlobalMddDeref( DdManager * dd, int * pValues, int nOuts, DdNode *** ppMdds )
{
    int i, v;
    for ( i = 0; i < nOuts; i++ )
    {
        for ( v = 0; v < pValues[i]; v++ )
            Cudd_RecursiveDeref( dd, ppMdds[i][v] );
        FREE( ppMdds[i] );
    }
    FREE( ppMdds );
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
bool Ntk_NetworkGlobalMddCheckEquality( DdManager * dd, int * pValues, int nOuts, DdNode *** ppMdds1, DdNode *** ppMdds2 )
{
    int i, v;
    for ( i = 0; i < nOuts; i++ )
        for ( v = 0; v < pValues[i]; v++ )
            if ( ppMdds1[i][v] != ppMdds2[i][v] )
                return 0;
    return 1;
}

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

  Synopsis    []

  Description [Teturns 1 if ppMdds1 is contained in ppMdds2.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
bool Ntk_NetworkGlobalMddCheckContainment( DdManager * dd, int * pValues, int nOuts, DdNode *** ppMdds1, DdNode *** ppMdds2 )
{
    int i, v;
    for ( i = 0; i < nOuts; i++ )
        for ( v = 0; v < pValues[i]; v++ )
            if ( !Cudd_bddLeq( dd, ppMdds1[i][v], ppMdds2[i][v] ) )
                return 0;
    return 1;
}

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

  Synopsis    []

  Description [Returns 1 if ppMdds are non-deterministic.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
bool Ntk_NetworkGlobalMddCheckND( DdManager * dd, int * pValues, int nOuts, DdNode *** ppMdds )
{
    int i, v, w;
    for ( i = 0; i < nOuts; i++ )
        for ( v = 0;   v < pValues[i]; v++ )
        for ( w = v+1; w < pValues[i]; w++ )
            if ( !Cudd_bddLeq( dd, ppMdds[i][v], Cudd_Not(ppMdds[i][w]) ) ) // they intersect
                return 1;
    return 0;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Ntk_NetworkGlobalMddErrorTrace( DdManager * dd, int * pValues, int nOuts, DdNode *** ppMdds1, DdNode *** ppMdds2, int * Out, int * Value )
{
    DdNode * bRes;
    int i, v;
    for ( i = 0; i < nOuts; i++ )
        for ( v = 0; v < pValues[i]; v++ )
            if ( !Cudd_bddLeq( dd, ppMdds1[i][v], ppMdds2[i][v] ) )
            {
                bRes = Cudd_bddAnd( dd, ppMdds1[i][v], Cudd_Not(ppMdds2[i][v]) );
                *Out = i;
                *Value = v;
                return bRes;
            }
    return NULL;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ntk_NetworkGlobalMddPrintErrorTrace( FILE * pFile, DdManager * dd, Vmx_VarMap_t * pVmx, DdNode * bTrace, int Out, char * pNameOut, int nValue, char * psLeavesByName[] )
{
    Vm_VarMap_t * pVm;
    char * sCube;
    int *  pValues;
    int *  pZddVarsLog;  
    int *  pZddVarsPos;  
    int    nVarsIn, nValuesNum;
    int i, v, Index;

    pVm        = Vmx_VarMapReadVm( pVmx );
    nVarsIn    = Vm_VarMapReadVarsInNum( pVm );
    nValuesNum = Vm_VarMapReadValuesNum( pVm );
    pValues    = Vm_VarMapReadValuesArray( pVm );

    pZddVarsLog = ALLOC( int, nValuesNum );  // logarithmic encoding goes here
    pZddVarsPos = ALLOC( int, nValuesNum );  // positional encoding goes here

    // get the cube
    sCube = ALLOC( char, dd->size );
    Cudd_bddPickOneCube( dd, bTrace, sCube );
    // translate the cube into the log-encoded cube
    for ( i = 0; i < dd->size; i++ )
        pZddVarsLog[i] = sCube[i];
    FREE( sCube );

    // decode the cube
    Vmx_VarMapDecode( pVmx, pZddVarsLog, pZddVarsPos );

    // write out the decoded cube
    fprintf( pFile, "po \"%s\": (", pNameOut );
    Index = 0;
    for ( i = 0; i < nVarsIn; i++ )
    {
        for ( v = 0; v < pValues[i]; v++ )
            if ( pZddVarsPos[Index + v] )
            {
                fprintf( pFile, "%d ", v );
                break;
            }
        Index += pValues[i];
    }
    fprintf( pFile, "-> %d)", nValue );

    FREE( pZddVarsLog );
    FREE( pZddVarsPos );
}

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

  Synopsis    [Returns the extended variable map for the construction of global MDD.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vmx_VarMap_t * Ntk_NetworkGlobalGetVmx( Ntk_Network_t * pNet, char ** psLeavesByName )
{
    Vmx_VarMap_t * pVmx;
    Vm_VarMap_t * pVm;
    Ntk_Node_t * pNodeCi;
    int * pValues;
    int nVars, i;

    // create the global variable map
    nVars = Ntk_NetworkReadCiNum( pNet );
    pValues = ALLOC( int, nVars );
    if ( psLeavesByName )
    {
        for ( i = 0; i < nVars; i++ )
        {
            pNodeCi = Ntk_NetworkFindNodeByName( pNet, psLeavesByName[i] );
            assert( pNodeCi );
            pValues[i] = pNodeCi->nValues;
        }
    }
    else
    {
        i = 0;
        Ntk_NetworkForEachCi( pNet, pNodeCi )
            pValues[i++] = pNodeCi->nValues;
    }
    pVm = Vm_VarMapLookup( Fnc_ManagerReadManVm(pNet->pMan), nVars, 0, pValues );
    pVmx = Vmx_VarMapLookup( Fnc_ManagerReadManVmx(pNet->pMan), pVm, -1, NULL );
    FREE( pValues );
    return pVmx;
}

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

  Synopsis    [Collects the output values.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int * Ntk_NetworkGlobalGetOutputValues( Ntk_Network_t * pNet )
{
    Ntk_Node_t * pNode;
    int * pValuesOut;
    int iOutput;

    pValuesOut = ALLOC( int, Ntk_NetworkReadCoNum(pNet) );
    iOutput = 0;
    Ntk_NetworkForEachCo( pNet, pNode )
        pValuesOut[iOutput++] = pNode->nValues;

    return pValuesOut;
}

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

  Synopsis    [Collects the output names.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
char ** Ntk_NetworkGlobalGetOutputs( Ntk_Network_t * pNet )
{
    char ** psRoots;
    Ntk_Node_t * pNode;
    int i;
    // put the nodes in the support into the hash table
    psRoots    = ALLOC( char *, Ntk_NetworkReadCoNum(pNet) );
    i = 0;
    Ntk_NetworkForEachCo( pNet, pNode )
        psRoots[i++]= pNode->pName;
    assert( i == Ntk_NetworkReadCoNum(pNet) ); 
    return psRoots;
}


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

  Synopsis    [Collects the output names.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
char ** Ntk_NetworkGlobalGetOutputsAndValues( Ntk_Network_t * pNet, int ** ppValues )
{
    char ** psLeaves;
    int * pValuesOut;
    Ntk_Node_t * pNode;
    int i;
    // put the nodes in the support into the hash table
    psLeaves    = ALLOC( char *, Ntk_NetworkReadCoNum(pNet) );
    pValuesOut = ALLOC( int, Ntk_NetworkReadCoNum(pNet) );
    i = 0;
    Ntk_NetworkForEachCo( pNet, pNode )
    {
        psLeaves[i]     = pNode->pName;
        pValuesOut[i++] = pNode->nValues;
    }
    assert( i == Ntk_NetworkReadCoNum(pNet) ); 
    *ppValues = pValuesOut;
    return psLeaves;
}


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

  Synopsis    [Copies the array of BDD with or without referencing them.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ntk_NodeGlobalMddCopy( DdNode * pDestin[], DdNode * pSource[], int nValues, bool fRef )
{
    int i;
    for ( i = 0; i < nValues; i++ )
    {
        assert( pSource[i] ); // the fanin global MDDs should be available
        pDestin[i] = pSource[i];
        if ( fRef )
            Cudd_Ref( pDestin[i] );
    }
}

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

  Synopsis    [Copies the array of BDD with or without referencing them.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ntk_NodeGlobalMddDeref( DdManager * dd, DdNode * pFuncs[], int nValues )
{
    int i;
    for ( i = 0; i < nValues; i++ )
        Cudd_RecursiveDeref( dd, pFuncs[i] );
}

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

  Synopsis    [Copies the array of BDD with or without referencing them.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ntk_NodeGlobalMddSetZero( DdManager * dd, DdNode * pFuncs[], int nValues )
{
    int i;
    for ( i = 0; i < nValues; i++ )
    {
        pFuncs[i] = b0;  Cudd_Ref( pFuncs[i] );
    }
}

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

  Synopsis    [Copies the array of BDD with or without referencing them.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
bool Ntk_NodeGlobalMddCheckND( DdManager * dd, DdNode * pFuncs[], int nValues )
{
    int i, k;
    for ( i = 0; i < nValues; i++ )
        for ( k = i+1; k < nValues; k++ )
            if ( !Cudd_bddLeq( dd, pFuncs[i], Cudd_Not(pFuncs[k]) ) ) // they intersect
                return 1;
    return 0;
}

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