ntkisat.c

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

    {
        // write the internal node
        Ntk_NodeWriteClauses( pFile, pNode2, pPref2 );
        // if an internal node has only one fanout, which is a PO,
        // the PO name is used for the internal node, and in this way, 
        // the PO is written into the file

        // however, if an internal node has more than one fanout
        // it is written as an intenal node with its own name
        // in this case, if among the fanouts of the node there are POs,
        // they should be written with their names, as MV buffers
        // driven by the given internal node
        if ( Ntk_NodeReadFanoutNum( pNode2 ) > 1 )
        {
            Ntk_NodeForEachFanout( pNode2, pPin, pFanout ) 
                if ( Ntk_NodeIsCo(pFanout) )
                    Ntk_NodeWriteClausesBuffer( pFile, pNode2, pFanout, pPref2, pPref2, 1 ); 
        }
    }

    // finish off
    fprintf( pFile, ".e\n" );
    fclose( pFile );

    // remove the clauses
    Ntk_NetworkDeleteClauses( pNet1 );
    Ntk_NetworkDeleteClauses( pNet2 );
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ntk_NetworkCreateClauses( Ntk_Network_t * pNet )
{
    Ntk_Node_t * pNode;
    int nClauses;
    // for each internal node, get the set of clauses
    // the clauses are pset_families attached to the pNode->pCopy field
    nClauses = 0;
    Ntk_NetworkForEachNode( pNet, pNode )
        nClauses += Ntk_NodeGenerateClauses( pNode );
    return nClauses;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ntk_NetworkDeleteClauses( Ntk_Network_t * pNet )
{
    Ntk_Node_t * pNode;
    Ntk_NetworkForEachNode( pNet, pNode )
        Mvc_CoverFree( (Mvc_Cover_t *)pNode->pCopy );
    return 1;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ntk_NodeGenerateClauses( Ntk_Node_t * pNode )
{
    Mvr_Relation_t * pMvr;
    DdNode * bRel;
    Vm_VarMap_t * pVm;
    Mvc_Cover_t * pCover;
    int nVars;

    // get the relation
    pMvr  = Ntk_NodeReadFuncMvr( pNode );
    pVm   = Ntk_NodeReadFuncVm( pNode );
    nVars = Vm_VarMapReadVarsNum( pVm );
    bRel  = Mvr_RelationReadRel( pMvr );  // comes already referenced
    // derife the cover
    pCover = Fnc_FunctionDeriveSopFromMdd( Ntk_NodeReadManMvc(pNode), pMvr, Cudd_Not(bRel), Cudd_Not(bRel), nVars );
//Ntk_NodePrintMvr( stdout, pNode );
//Ntk_NodePrintCvrPositional( stdout, pVm, pCover, Ntk_NodeReadFaninNum(pNode) + 1 );
    // attach the cover to the node
    pNode->pCopy = (Ntk_Node_t *)pCover;
    return Mvc_CoverReadCubeNum( pCover );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ntk_NodeWriteClauses( FILE * pFile, Ntk_Node_t * pNode, char * sPrefix )
{
    Vm_VarMap_t * pVm;
    Mvc_Cover_t * Cover;
    Mvc_Cube_t * pCube;
    bool fFirstLit, fFirstValue;
    Ntk_Node_t ** pFanins;
    int nFanins;
    int i, v;
    int nVars;
    int * pValuesFirst;


    // get the fanins
    nFanins = Ntk_NodeReadFaninNum(pNode);
    pFanins = pNode->pNet->pArray1;
    Ntk_NodeReadFanins( pNode, pFanins );
    // add the output variable just in case
    pFanins[nFanins] = pNode;
    // get the cover and the variable map to use with the cover
    Cover = (Mvc_Cover_t *)pNode->pCopy;
    pVm   = Ntk_NodeReadFuncVm( pNode );
    nVars = Vm_VarMapReadVarsNum( pVm );
    pValuesFirst = Vm_VarMapReadValuesArray(pVm);
    assert( Mvc_CoverReadBitNum(Cover) == Vm_VarMapReadValuesNum(pVm) );

    // iterate through the cubes (1 cube = 1 clause)
    Mvc_CoverForEachCube( Cover, pCube )
    {
        fFirstLit = 1;
        for ( i = 0; i < nVars; i++ )
        {
            // check if this literal is full
            for ( v = pValuesFirst[i]; v < pValuesFirst[i+1]; v++ )
                if ( !Mvc_CubeBitValue( pCube,  v ) )
                    break;
            if ( v == pValuesFirst[i+1] )
                continue;

            if ( fFirstLit )
                fFirstLit = 0;
            else
                fprintf( pFile, " " );

            // print this literal
            fFirstValue = 1;
            fprintf( pFile, "%s%s{", (sPrefix? sPrefix: ""), Ntk_NodeGetNameLong(pFanins[i]) );
            for ( v = pValuesFirst[i]; v < pValuesFirst[i+1]; v++ )
                if ( !Mvc_CubeBitValue( pCube,  v ) ) // complementation is done here!
                {
                    if ( fFirstValue )
                        fFirstValue = 0;
                    else
                        fprintf( pFile, "," );
                    fprintf( pFile, "%d", v - pValuesFirst[i] );
                }
            fprintf( pFile, "}" );
        }
        fprintf( pFile, "\n" );
    }
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ntk_NodeWriteClausesBuffer( FILE * pFile, 
    Ntk_Node_t * pNode1, Ntk_Node_t * pNode2, 
    char * pPref1, char * pPref2, 
    int Phase )
{
    int v, i, nValues;
    bool fFirst;
    assert( pNode1->nValues == pNode2->nValues );

    nValues = pNode1->nValues;
    for ( v = 0; v < nValues; v++ )
    {
        fprintf( pFile, "%s%s", (pPref1? pPref1: ""), Ntk_NodeGetNameLong(pNode1) );
        fprintf( pFile, "{" );
        if ( Phase ) // write the buffer (pNode1 == pNode1)
            fprintf( pFile, "%d", v );
        else // write the complement of the buffer (pNode1 != pNode1)
        {
            fFirst = 1;
            for ( i = 0; i < nValues; i++ )
                if ( i != v )
                {
                    if ( fFirst )
                        fFirst = 0;
                    else
                        fprintf( pFile, "," );
                    fprintf( pFile, "%d", i );
                }
        }
        fprintf( pFile, "} " );

        fprintf( pFile, "%s%s", (pPref2? pPref2: ""), Ntk_NodeGetNameLong(pNode2) );
        fprintf( pFile, "{" );
        fFirst = 1;
        for ( i = 0; i < nValues; i++ )
            if ( i != v )
            {
                if ( fFirst )
                    fFirst = 0;
                else
                    fprintf( pFile, "," );
                fprintf( pFile, "%d", i );
            }
        fprintf( pFile, "}\n" );
    }
}


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