abc70930: src/base/abc/abcBlifMv.c Source File

00001 
00021 #include "abc.h"
00022 
00026  
00030 
00042 void Abc_NtkStartMvVars( Abc_Ntk_t * pNtk ) 
00043 {
00044     Vec_Att_t * pAttMan;
00045     assert( Abc_NtkMvVar(pNtk) == NULL );
00046     pAttMan = Vec_AttAlloc( 0, Abc_NtkObjNumMax(pNtk) + 1, Extra_MmFlexStart(), Extra_MmFlexStop, NULL, NULL );
00047     Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_MVVAR, pAttMan );
00048 //printf( "allocing attr\n" );
00049 }
00050 
00062 void Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk ) 
00063 { 
00064     void * pUserMan;
00065     pUserMan = Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, 0 ); 
00066     Extra_MmFlexStop( pUserMan );
00067 }
00068 
00080 void Abc_NtkSetMvVarValues( Abc_Obj_t * pObj, int nValues )
00081 {
00082     Extra_MmFlex_t * pFlex;
00083     struct temp 
00084     { 
00085         int nValues; 
00086         char ** pNames; 
00087     } * pVarStruct;
00088     assert( nValues > 1 );
00089     // skip binary signals
00090     if ( nValues == 2 )
00091         return;
00092     // skip already assigned signals
00093     if ( Abc_ObjMvVar(pObj) != NULL )
00094         return;
00095     // create the structure
00096     pFlex = Abc_NtkMvVarMan( pObj->pNtk );
00097     pVarStruct = (void *)Extra_MmFlexEntryFetch( pFlex, sizeof(struct temp) );
00098     pVarStruct->nValues = nValues;
00099     pVarStruct->pNames = NULL;
00100     Abc_ObjSetMvVar( pObj, pVarStruct );
00101 }
00102 
00114 static inline int Abc_StringGetNumber( char ** ppStr )
00115 {
00116     char * pStr = *ppStr;
00117     int Number = 0;
00118     assert( *pStr >= '0' && *pStr <= '9' );
00119     for ( ; *pStr >= '0' && *pStr <= '9'; pStr++ )
00120         Number = 10 * Number + *pStr - '0';
00121     *ppStr = pStr;
00122     return Number;
00123 }
00124 
00136 int Abc_NodeStrashBlifMv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
00137 {
00138     char * pSop;
00139     Abc_Obj_t ** pValues, ** pValuesF, ** pValuesF2;
00140     Abc_Obj_t * pTemp, * pTemp2, * pFanin, * pFanin2, * pNet;
00141     int k, v, Def, DefIndex, Index, nValues, nValuesF, nValuesF2;
00142 
00143     // start the output values
00144     assert( Abc_ObjIsNode(pObj) );
00145     pNet = Abc_ObjFanout0(pObj);
00146     nValues = Abc_ObjMvVarNum(pNet);
00147     pValues = ALLOC( Abc_Obj_t *, nValues );
00148     for ( k = 0; k < nValues; k++ )
00149         pValues[k] = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
00150 
00151     // get the BLIF-MV formula
00152     pSop = pObj->pData;
00153     // skip the value line
00154 //    while ( *pSop++ != '\n' );
00155 
00156     // handle the constant
00157     if ( Abc_ObjFaninNum(pObj) == 0 )
00158     {
00159         // skip the default if present
00160         if ( *pSop == 'd' )
00161             while ( *pSop++ != '\n' );
00162         // skip space if present
00163         if ( *pSop == ' ' )
00164             pSop++;
00165         Index = Abc_StringGetNumber( &pSop );
00166         assert( Index < nValues );
00167         pValues[Index] = Abc_AigConst1(pNtkNew);
00168         // save the values in the fanout net
00169         pNet->pCopy = (Abc_Obj_t *)pValues;
00170         return 1;
00171     }
00172 
00173     // parse the default line
00174     Def = DefIndex = -1;
00175     if ( *pSop == 'd' )
00176     {
00177         pSop++;
00178         if ( *pSop == '=' )
00179         {
00180             pSop++;
00181             DefIndex = Abc_StringGetNumber( &pSop );
00182             assert( DefIndex < Abc_ObjFaninNum(pObj) );
00183         }
00184         else if ( *pSop == '-' )
00185         {
00186             pSop++;
00187             Def = 0;
00188         }
00189         else
00190         {
00191             Def = Abc_StringGetNumber( &pSop );
00192             assert( Def < nValues );
00193         }
00194         assert( *pSop == '\n' );
00195         pSop++;
00196     }
00197 
00198     // convert the values
00199     while ( *pSop )
00200     {
00201         // extract the values for each cube
00202         pTemp = Abc_AigConst1(pNtkNew); 
00203         Abc_ObjForEachFanin( pObj, pFanin, k )
00204         {
00205             if ( *pSop == '-' )
00206             {
00207                 pSop += 2;
00208                 continue;
00209             }
00210             if ( *pSop == '!' )
00211             {
00212                 printf( "Abc_NodeStrashBlifMv(): Cannot handle complement in the MV function of node %s.\n", Abc_ObjName(Abc_ObjFanout0(pObj)) );
00213                 return 0;
00214             }
00215             if ( *pSop == '{' )
00216             {
00217                 printf( "Abc_NodeStrashBlifMv(): Cannot handle braces in the MV function of node %s.\n", Abc_ObjName(Abc_ObjFanout0(pObj)) );
00218                 return 0;
00219             }
00220             // get the value set
00221             nValuesF = Abc_ObjMvVarNum(pFanin);
00222             pValuesF = (Abc_Obj_t **)pFanin->pCopy;
00223             if ( *pSop == '(' )
00224             {
00225                 pSop++;
00226                 pTemp2 = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
00227                 while ( *pSop != ')' )
00228                 {
00229                     Index = Abc_StringGetNumber( &pSop );
00230                     assert( Index < nValuesF );
00231                     pTemp2 = Abc_AigOr( pNtkNew->pManFunc, pTemp2, pValuesF[Index] );
00232                     assert( *pSop == ')' || *pSop == ',' );
00233                     if ( *pSop == ',' )
00234                         pSop++;
00235                 }
00236                 assert( *pSop == ')' );
00237                 pSop++;
00238             }
00239             else if ( *pSop == '=' )
00240             {
00241                 pSop++;
00242                 // get the fanin index
00243                 Index = Abc_StringGetNumber( &pSop );
00244                 assert( Index < Abc_ObjFaninNum(pObj) );
00245                 assert( Index != k );
00246                 // get the fanin
00247                 pFanin2 = Abc_ObjFanin( pObj, Index );
00248                 nValuesF2 = Abc_ObjMvVarNum(pFanin2);
00249                 pValuesF2 = (Abc_Obj_t **)pFanin2->pCopy;
00250                 // create the sum of products of values
00251                 assert( nValuesF == nValuesF2 );
00252                 pTemp2 = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
00253                 for ( v = 0; v < nValues; v++ )
00254                     pTemp2 = Abc_AigOr( pNtkNew->pManFunc, pTemp2, Abc_AigAnd(pNtkNew->pManFunc, pValuesF[v], pValuesF2[v]) );
00255             }
00256             else
00257             {
00258                 Index = Abc_StringGetNumber( &pSop );
00259                 assert( Index < nValuesF );
00260                 pTemp2 = pValuesF[Index];
00261             }
00262             // compute the compute
00263             pTemp = Abc_AigAnd( pNtkNew->pManFunc, pTemp, pTemp2 );
00264             // advance the reading point
00265             assert( *pSop == ' ' );
00266             pSop++;
00267         }
00268         // check if the output value is an equal construct
00269         if ( *pSop == '=' )
00270         {
00271             pSop++;
00272             // get the output value
00273             Index = Abc_StringGetNumber( &pSop );
00274             assert( Index < Abc_ObjFaninNum(pObj) );
00275             // add values of the given fanin with the given cube
00276             pFanin = Abc_ObjFanin( pObj, Index );
00277             nValuesF = Abc_ObjMvVarNum(pFanin);
00278             pValuesF = (Abc_Obj_t **)pFanin->pCopy;
00279             assert( nValuesF == nValues ); // should be guaranteed by the parser
00280             for ( k = 0; k < nValuesF; k++ )
00281                 pValues[k] = Abc_AigOr( pNtkNew->pManFunc, pValues[k], Abc_AigAnd(pNtkNew->pManFunc, pTemp, pValuesF[k]) );
00282         }
00283         else
00284         {
00285             // get the output value
00286             Index = Abc_StringGetNumber( &pSop );
00287             assert( Index < nValues );
00288             pValues[Index] = Abc_AigOr( pNtkNew->pManFunc, pValues[Index], pTemp );
00289         }
00290         // advance the reading point
00291         assert( *pSop == '\n' );
00292         pSop++;
00293     }
00294 
00295     // compute the default value
00296     if ( Def >= 0 || DefIndex >= 0 )
00297     {
00298         pTemp = Abc_AigConst1(pNtkNew);
00299         for ( k = 0; k < nValues; k++ )
00300         {
00301             if ( k == Def )
00302                 continue;
00303             pTemp = Abc_AigAnd( pNtkNew->pManFunc, pTemp, Abc_ObjNot(pValues[k]) );
00304         }
00305 
00306         // assign the default value
00307         if ( Def >= 0 )
00308             pValues[Def] = pTemp;
00309         else
00310         {
00311             assert( DefIndex >= 0 );
00312             // add values of the given fanin with the given cube
00313             pFanin = Abc_ObjFanin( pObj, DefIndex );
00314             nValuesF = Abc_ObjMvVarNum(pFanin);
00315             pValuesF = (Abc_Obj_t **)pFanin->pCopy;
00316             assert( nValuesF == nValues ); // should be guaranteed by the parser
00317             for ( k = 0; k < nValuesF; k++ )
00318                 pValues[k] = Abc_AigOr( pNtkNew->pManFunc, pValues[k], Abc_AigAnd(pNtkNew->pManFunc, pTemp, pValuesF[k]) );
00319         }
00320 
00321     }
00322 
00323     // save the values in the fanout net
00324     pNet->pCopy = (Abc_Obj_t *)pValues;
00325     return 1;
00326 }
00327 
00339 static inline void Abc_NtkConvertAssignName( Abc_Obj_t * pObj, Abc_Obj_t * pNet, int Index )
00340 {
00341     char Suffix[16];
00342     assert( Abc_ObjIsTerm(pObj) );
00343     assert( Abc_ObjIsNet(pNet) );
00344     sprintf( Suffix, "[%d]", Index );
00345     Abc_ObjAssignName( pObj, Abc_ObjName(pNet), Suffix );
00346 }
00347 
00359 Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
00360 {
00361     int fUsePositional = 0;
00362     Vec_Ptr_t * vNodes;
00363     Abc_Obj_t ** pBits;
00364     Abc_Obj_t ** pValues;
00365     Abc_Ntk_t * pNtkNew;
00366     Abc_Obj_t * pObj, * pTemp, * pBit, * pNet;
00367     int i, k, v, nValues, nValuesMax, nBits;
00368 
00369     assert( Abc_NtkIsNetlist(pNtk) );
00370     assert( Abc_NtkHasBlifMv(pNtk) );
00371     assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
00372     assert( Abc_NtkBlackboxNum(pNtk) == 0 );
00373 
00374     // get the largest number of values
00375     nValuesMax = 2;
00376     Abc_NtkForEachNet( pNtk, pObj, i )
00377     {
00378         nValues = Abc_ObjMvVarNum(pObj);
00379         if ( nValuesMax < nValues )
00380             nValuesMax = nValues;
00381     }
00382     nBits = Extra_Base2Log( nValuesMax );
00383     pBits = ALLOC( Abc_Obj_t *, nBits );
00384 
00385     // clean the node copy fields
00386     Abc_NtkCleanCopy( pNtk );
00387     // collect the nodes
00388     vNodes = Abc_NtkDfs( pNtk, 0 );
00389 
00390     // start the network
00391     pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
00392     // duplicate the name and the spec
00393     pNtkNew->pName = Extra_UtilStrsav( pNtk->pName );
00394 //    pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pName );
00395 
00396     // encode the CI nets
00397     Abc_NtkIncrementTravId( pNtk );
00398     if ( fUsePositional )
00399     {
00400         Abc_NtkForEachCi( pNtk, pObj, i )
00401         {
00402             pNet = Abc_ObjFanout0(pObj);
00403             nValues = Abc_ObjMvVarNum(pNet);
00404             pValues = ALLOC( Abc_Obj_t *, nValues );
00405             // create PIs for the values
00406             for ( v = 0; v < nValues; v++ )
00407             {
00408                 pValues[v] = Abc_NtkCreatePi( pNtkNew );
00409                 Abc_NtkConvertAssignName( pValues[v], pNet, v );
00410             }
00411             // save the values in the fanout net
00412             pNet->pCopy = (Abc_Obj_t *)pValues;
00413             // mark the net
00414             Abc_NodeSetTravIdCurrent( pNet );
00415         }
00416     }
00417     else
00418     {
00419         Abc_NtkForEachCi( pNtk, pObj, i )
00420         {
00421             pNet = Abc_ObjFanout0(pObj);
00422             nValues = Abc_ObjMvVarNum(pNet);
00423             pValues = ALLOC( Abc_Obj_t *, nValues );
00424             // create PIs for the encoding bits
00425             nBits = Extra_Base2Log( nValues );
00426             for ( k = 0; k < nBits; k++ )
00427             {
00428                 pBits[k] = Abc_NtkCreatePi( pNtkNew );
00429                 Abc_NtkConvertAssignName( pBits[k], pNet, k );
00430             }
00431             // encode the values
00432             for ( v = 0; v < nValues; v++ )
00433             {
00434                 pValues[v] = Abc_AigConst1(pNtkNew);
00435                 for ( k = 0; k < nBits; k++ )
00436                 {
00437                     pBit = Abc_ObjNotCond( pBits[k], (v&(1<<k)) == 0 );
00438                     pValues[v] = Abc_AigAnd( pNtkNew->pManFunc, pValues[v], pBit );
00439                 }
00440             }
00441             // save the values in the fanout net
00442             pNet->pCopy = (Abc_Obj_t *)pValues;
00443             // mark the net
00444             Abc_NodeSetTravIdCurrent( pNet );
00445         }
00446     }
00447 
00448     // process nodes in the topological order
00449     Vec_PtrForEachEntry( vNodes, pObj, i )
00450         if ( !Abc_NodeStrashBlifMv( pNtkNew, pObj ) )
00451         {
00452             Abc_NtkDelete( pNtkNew );
00453             return NULL;
00454         }
00455     Vec_PtrFree( vNodes );
00456 
00457     // encode the CO nets
00458     if ( fUsePositional )
00459     {
00460         Abc_NtkForEachCo( pNtk, pObj, i )
00461         {
00462             pNet = Abc_ObjFanin0(pObj);
00463             // skip marked nets
00464             if ( Abc_NodeIsTravIdCurrent(pNet) )
00465                 continue;
00466             Abc_NodeSetTravIdCurrent( pNet );
00467             nValues = Abc_ObjMvVarNum(pNet);
00468             pValues = (Abc_Obj_t **)pNet->pCopy;
00469             for ( v = 0; v < nValues; v++ )
00470             {
00471                 pTemp = Abc_NtkCreatePo( pNtkNew );
00472                 Abc_ObjAddFanin( pTemp, pValues[v] );
00473                 Abc_NtkConvertAssignName( pTemp, pNet, v );
00474             }
00475         }
00476     }
00477     else
00478     {
00479         Abc_NtkForEachCo( pNtk, pObj, i )
00480         {
00481             pNet = Abc_ObjFanin0(pObj);
00482             // skip marked nets
00483             if ( Abc_NodeIsTravIdCurrent(pNet) )
00484                 continue;
00485             Abc_NodeSetTravIdCurrent( pNet );
00486             nValues = Abc_ObjMvVarNum(pNet);
00487             pValues = (Abc_Obj_t **)pNet->pCopy;
00488             nBits = Extra_Base2Log( nValues );
00489             for ( k = 0; k < nBits; k++ )
00490             {
00491                 pBit = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
00492                 for ( v = 0; v < nValues; v++ )
00493                     if ( v & (1<<k) )
00494                         pBit = Abc_AigOr( pNtkNew->pManFunc, pBit, pValues[v] );
00495                 pTemp = Abc_NtkCreatePo( pNtkNew );
00496                 Abc_ObjAddFanin( pTemp, pBit );
00497                 Abc_NtkConvertAssignName( pTemp, pNet, k );
00498             }
00499         }
00500     }
00501 
00502     // cleanup
00503     free( pBits );
00504     Abc_NtkForEachObj( pNtk, pObj, i )
00505         if ( pObj->pCopy )
00506             free( pObj->pCopy );
00507 
00508     // remove dangling nodes
00509     i = Abc_AigCleanup(pNtkNew->pManFunc);
00510 //    printf( "Cleanup removed %d nodes.\n", i );
00511 //    Abc_NtkReassignIds( pNtkNew );
00512 
00513     // check integrity
00514     if ( !Abc_NtkCheck( pNtkNew ) )
00515     {
00516         fprintf( stdout, "Abc_NtkStrashBlifMv(): Network check has failed.\n" );
00517         Abc_NtkDelete( pNtkNew );
00518         return NULL;
00519     }
00520     return pNtkNew;
00521 }
00522 
00534 Abc_Ntk_t * Abc_NtkSkeletonBlifMv( Abc_Ntk_t * pNtk )
00535 {
00536     int fUsePositional = 0;
00537     Abc_Ntk_t * pNtkNew;
00538     Abc_Obj_t * pObj, * pNet, * pNetNew, * pNodeNew, * pTermNew, * pBoxNew;
00539     int i, k, v, nValues, nBits;
00540 
00541     assert( Abc_NtkIsNetlist(pNtk) );
00542     assert( Abc_NtkHasBlifMv(pNtk) );
00543     assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
00544     assert( Abc_NtkBlackboxNum(pNtk) == 0 );
00545 
00546     // clean the node copy fields
00547     Abc_NtkCleanCopy( pNtk );
00548 
00549     // start the network
00550     pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
00551     // duplicate the name and the spec
00552     pNtkNew->pName = Extra_UtilStrsav( pNtk->pName );
00553     pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pName );
00554     // create the internal box (it is important to put it first!)
00555     pBoxNew = Abc_NtkCreateWhitebox( pNtkNew );
00556     // create PIs and their nets
00557     Abc_NtkForEachPi( pNtk, pObj, i )
00558     {
00559         Abc_NtkDupObj( pNtkNew, pObj, 0 );
00560         pNet = Abc_ObjFanout0(pObj);
00561         Abc_NtkDupObj( pNtkNew, pNet, 1 );
00562         Abc_ObjAddFanin( pNet->pCopy, pObj->pCopy );
00563     }
00564     // create POs and their nets
00565     Abc_NtkForEachPo( pNtk, pObj, i )
00566     {
00567         Abc_NtkDupObj( pNtkNew, pObj, 0 );
00568         pNet = Abc_ObjFanin0(pObj);
00569         if ( pNet->pCopy == NULL )
00570             Abc_NtkDupObj( pNtkNew, pNet, 1 );
00571         Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy );
00572     }
00573     // create latches
00574     Abc_NtkForEachLatch( pNtk, pObj, i )
00575     {
00576         Abc_NtkDupBox( pNtkNew, pObj, 0 );
00577         // latch outputs
00578         pNet = Abc_ObjFanout0(Abc_ObjFanout0(pObj));
00579         assert( pNet->pCopy == NULL );
00580         Abc_NtkDupObj( pNtkNew, pNet, 1 );
00581         Abc_ObjAddFanin( pNet->pCopy, Abc_ObjFanout0(pObj)->pCopy );
00582         // latch inputs
00583         pNet = Abc_ObjFanin0(Abc_ObjFanin0(pObj));
00584         if ( pNet->pCopy == NULL )
00585             Abc_NtkDupObj( pNtkNew, pNet, 1 );
00586         Abc_ObjAddFanin( Abc_ObjFanin0(pObj)->pCopy, pNet->pCopy );
00587     }
00588 
00589     // encode the CI nets
00590     Abc_NtkIncrementTravId( pNtk );
00591     if ( fUsePositional )
00592     {
00593         Abc_NtkForEachCi( pNtk, pObj, i )
00594         {
00595             pNet = Abc_ObjFanout0(pObj);
00596             nValues = Abc_ObjMvVarNum(pNet);
00597             for ( v = 0; v < nValues; v++ )
00598             {
00599                 pNodeNew = Abc_NtkCreateNode( pNtkNew );
00600                 pNodeNew->pData = Abc_SopEncoderPos( pNtkNew->pManFunc, v, nValues );
00601                 pNetNew = Abc_NtkCreateNet( pNtkNew );
00602                 pTermNew = Abc_NtkCreateBi( pNtkNew );
00603                 Abc_ObjAddFanin( pNodeNew, pNet->pCopy );
00604                 Abc_ObjAddFanin( pNetNew, pNodeNew );
00605                 Abc_ObjAddFanin( pTermNew, pNetNew );
00606                 Abc_ObjAddFanin( pBoxNew, pTermNew );
00607             }
00608             // mark the net
00609             Abc_NodeSetTravIdCurrent( pNet );
00610         }
00611     }
00612     else
00613     {
00614         Abc_NtkForEachCi( pNtk, pObj, i )
00615         {
00616             pNet = Abc_ObjFanout0(pObj);
00617             nValues = Abc_ObjMvVarNum(pNet);
00618             nBits = Extra_Base2Log( nValues );
00619             for ( k = 0; k < nBits; k++ )
00620             {
00621                 pNodeNew = Abc_NtkCreateNode( pNtkNew );
00622                 pNodeNew->pData = Abc_SopEncoderLog( pNtkNew->pManFunc, k, nValues );
00623                 pNetNew = Abc_NtkCreateNet( pNtkNew );
00624                 pTermNew = Abc_NtkCreateBi( pNtkNew );
00625                 Abc_ObjAddFanin( pNodeNew, pNet->pCopy );
00626                 Abc_ObjAddFanin( pNetNew, pNodeNew );
00627                 Abc_ObjAddFanin( pTermNew, pNetNew );
00628                 Abc_ObjAddFanin( pBoxNew, pTermNew );
00629             }
00630             // mark the net
00631             Abc_NodeSetTravIdCurrent( pNet );
00632         }
00633     }
00634 
00635     // encode the CO nets
00636     if ( fUsePositional )
00637     {
00638         Abc_NtkForEachCo( pNtk, pObj, i )
00639         {
00640             pNet = Abc_ObjFanin0(pObj);
00641             // skip marked nets
00642             if ( Abc_NodeIsTravIdCurrent(pNet) )
00643                 continue;
00644             Abc_NodeSetTravIdCurrent( pNet );
00645             nValues = Abc_ObjMvVarNum(pNet);
00646             pNodeNew = Abc_NtkCreateNode( pNtkNew );
00647             pNodeNew->pData = Abc_SopDecoderPos( pNtkNew->pManFunc, nValues );
00648             for ( v = 0; v < nValues; v++ )
00649             {
00650                 pTermNew = Abc_NtkCreateBo( pNtkNew );
00651                 pNetNew = Abc_NtkCreateNet( pNtkNew );
00652                 Abc_ObjAddFanin( pTermNew, pBoxNew );
00653                 Abc_ObjAddFanin( pNetNew, pTermNew );
00654                 Abc_ObjAddFanin( pNodeNew, pNetNew );
00655             }
00656             Abc_ObjAddFanin( pNet->pCopy, pNodeNew );
00657         }
00658     }
00659     else
00660     {
00661         Abc_NtkForEachCo( pNtk, pObj, i )
00662         {
00663             pNet = Abc_ObjFanin0(pObj);
00664             // skip marked nets
00665             if ( Abc_NodeIsTravIdCurrent(pNet) )
00666                 continue;
00667             Abc_NodeSetTravIdCurrent( pNet );
00668             nValues = Abc_ObjMvVarNum(pNet);
00669             nBits = Extra_Base2Log( nValues );
00670             pNodeNew = Abc_NtkCreateNode( pNtkNew );
00671             pNodeNew->pData = Abc_SopDecoderLog( pNtkNew->pManFunc, nValues );
00672             for ( k = 0; k < nBits; k++ )
00673             {
00674                 pTermNew = Abc_NtkCreateBo( pNtkNew );
00675                 pNetNew = Abc_NtkCreateNet( pNtkNew );
00676                 Abc_ObjAddFanin( pTermNew, pBoxNew );
00677                 Abc_ObjAddFanin( pNetNew, pTermNew );
00678                 Abc_ObjAddFanin( pNodeNew, pNetNew );
00679             }
00680             Abc_ObjAddFanin( pNet->pCopy, pNodeNew );
00681         }
00682     }
00683 
00684     // if it is a BLIF-MV netlist transfer the values of all nets
00685     if ( Abc_NtkHasBlifMv(pNtk) && Abc_NtkMvVar(pNtk) )
00686     {
00687         if ( Abc_NtkMvVar( pNtkNew ) == NULL )
00688             Abc_NtkStartMvVars( pNtkNew );
00689         Abc_NtkForEachNet( pNtk, pObj, i )
00690             if ( pObj->pCopy )
00691                 Abc_NtkSetMvVarValues( pObj->pCopy, Abc_ObjMvVarNum(pObj) );
00692     }
00693 
00694     // check integrity
00695     if ( !Abc_NtkCheck( pNtkNew ) )
00696     {
00697         fprintf( stdout, "Abc_NtkSkeletonBlifMv(): Network check has failed.\n" );
00698         Abc_NtkDelete( pNtkNew );
00699         return NULL;
00700     }
00701     return pNtkNew;
00702 }
00703 
00719 Abc_Ntk_t * Abc_NtkInsertBlifMv( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtkLogic )
00720 {
00721     Abc_Ntk_t * pNtkSkel, * pNtkNew;
00722     Abc_Obj_t * pBox;
00723 
00724     assert( Abc_NtkIsNetlist(pNtkBase) );
00725     assert( Abc_NtkHasBlifMv(pNtkBase) );
00726     assert( Abc_NtkWhiteboxNum(pNtkBase) == 0 );
00727     assert( Abc_NtkBlackboxNum(pNtkBase) == 0 );
00728 
00729     assert( Abc_NtkIsNetlist(pNtkLogic) );
00730     assert( Abc_NtkHasBlifMv(pNtkLogic) );
00731     assert( Abc_NtkWhiteboxNum(pNtkLogic) == 0 );
00732     assert( Abc_NtkBlackboxNum(pNtkLogic) == 0 );
00733 
00734     // extract the skeleton of the old network
00735     pNtkSkel = Abc_NtkSkeletonBlifMv( pNtkBase );
00736 
00737     // set the implementation of the box to be the same as the processed network
00738     assert( Abc_NtkWhiteboxNum(pNtkSkel) == 1 );
00739     pBox = Abc_NtkBox( pNtkSkel, 0 );
00740     assert( Abc_ObjIsWhitebox(pBox) );
00741     assert( pBox->pData == NULL );
00742     assert( Abc_ObjFaninNum(pBox) == Abc_NtkPiNum(pNtkLogic) );
00743     assert( Abc_ObjFanoutNum(pBox) == Abc_NtkPoNum(pNtkLogic) );
00744     pBox->pData = pNtkLogic;
00745 
00746     // flatten the hierarchy to insert the processed network
00747     pNtkNew = Abc_NtkFlattenLogicHierarchy( pNtkSkel );
00748     pBox->pData = NULL;
00749     Abc_NtkDelete( pNtkSkel );
00750     return pNtkNew;    
00751 }
00752 
00764 int Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk )
00765 {
00766     Extra_MmFlex_t * pMmFlex;
00767     Abc_Obj_t * pNode;
00768     Vec_Str_t * vCube;
00769     char * pSop0, * pSop1, * pBlifMv, * pCube, * pCur;
00770     int Value, nCubes, nSize, i, k;
00771 
00772     assert( Abc_NtkIsNetlist(pNtk) );
00773     if ( !Abc_NtkToBdd(pNtk) )
00774     {
00775         printf( "Converting logic functions to BDDs has failed.\n" );
00776         return 0;
00777     }
00778 
00779     pMmFlex = Extra_MmFlexStart();
00780     vCube   = Vec_StrAlloc( 100 );
00781     Abc_NtkForEachNode( pNtk, pNode, i )
00782     {
00783         // convert BDD into cubes for on-set and off-set
00784         Abc_NodeBddToCnf( pNode, pMmFlex, vCube, 0, &pSop0, &pSop1 );
00785         // allocate room for the MV-SOP
00786         nCubes = Abc_SopGetCubeNum(pSop0) + Abc_SopGetCubeNum(pSop1);
00787         nSize = nCubes*(2*Abc_ObjFaninNum(pNode) + 2)+1;
00788         pBlifMv = Extra_MmFlexEntryFetch( pMmFlex, nSize );
00789         // add the cubes
00790         pCur = pBlifMv;
00791         Abc_SopForEachCube( pSop0, Abc_ObjFaninNum(pNode), pCube )
00792         {
00793             Abc_CubeForEachVar( pCube, Value, k )
00794             {
00795                 *pCur++ = Value;
00796                 *pCur++ = ' ';
00797             }
00798             *pCur++ = '0';
00799             *pCur++ = '\n';
00800         }
00801         Abc_SopForEachCube( pSop1, Abc_ObjFaninNum(pNode), pCube )
00802         {
00803             Abc_CubeForEachVar( pCube, Value, k )
00804             {
00805                 *pCur++ = Value;
00806                 *pCur++ = ' ';
00807             }
00808             *pCur++ = '1';
00809             *pCur++ = '\n';
00810         }
00811         *pCur++ = 0;
00812         assert( pCur - pBlifMv == nSize );
00813         // update the node representation
00814         Cudd_RecursiveDeref( pNtk->pManFunc, pNode->pData );
00815         pNode->pData = pBlifMv;
00816     }
00817 
00818     // update the functionality type
00819     pNtk->ntkFunc = ABC_FUNC_BLIFMV;
00820     Cudd_Quit( pNtk->pManFunc );
00821     pNtk->pManFunc = pMmFlex;
00822 
00823     Vec_StrFree( vCube );
00824     return 1;
00825 }
00826 
00838 char * Abc_NodeConvertSopToMvSop( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 )
00839 {
00840     char * pMvSop, * pCur;
00841     unsigned uCube;
00842     int nCubes, nSize, Value, i, k;
00843     // consider the case of the constant node
00844     if ( Vec_IntSize(vSop0) == 0 || Vec_IntSize(vSop1) == 0 )
00845     {
00846         // (temporary) create a tautology cube
00847         pMvSop = ALLOC( char, nVars + 3 );
00848         for ( k = 0; k < nVars; k++ )
00849             pMvSop[k] = '-';
00850         pMvSop[nVars] = '0' + (int)(Vec_IntSize(vSop1) > 0);
00851         pMvSop[nVars+1] = '\n';
00852         pMvSop[nVars+2] = 0;
00853         return pMvSop;
00854     }
00855     // find the total number of cubes
00856     nCubes = Vec_IntSize(vSop0) + Vec_IntSize(vSop1);
00857     // find the size of the MVSOP represented as a C-string
00858     // (each cube has nVars variables + one output literal + end-of-line,
00859     // and the string is zero-terminated)
00860     nSize = nCubes * (nVars + 2) + 1; 
00861     // allocate memory
00862     pMvSop = pCur = ALLOC( char, nSize );
00863     // fill in the negative polarity cubes
00864     Vec_IntForEachEntry( vSop0, uCube, i )
00865     {
00866         for ( k = 0; k < nVars; k++ )
00867         {
00868             Value = (uCube >> (2*k)) & 3;
00869             if ( Value == 1 )
00870                 *pCur++ = '0';
00871             else if ( Value == 2 )
00872                 *pCur++ = '1';
00873             else if ( Value == 0 )
00874                 *pCur++ = '-';
00875             else
00876                 assert( 0 );
00877         }
00878         *pCur++ = '0';
00879         *pCur++ = '\n';
00880     }
00881     // fill in the positive polarity cubes
00882     Vec_IntForEachEntry( vSop1, uCube, i )
00883     {
00884         for ( k = 0; k < nVars; k++ )
00885         {
00886             Value = (uCube >> (2*k)) & 3;
00887             if ( Value == 1 )
00888                 *pCur++ = '0';
00889             else if ( Value == 2 )
00890                 *pCur++ = '1';
00891             else if ( Value == 0 )
00892                 *pCur++ = '-';
00893             else
00894                 assert( 0 );
00895         }
00896         *pCur++ = '1';
00897         *pCur++ = '\n';
00898     }
00899     *pCur++ = 0;
00900     assert( pCur - pMvSop == nSize );
00901     return pMvSop;
00902 }
00903 
00904 
00921 int Abc_NodeEvalMvCostInternal( int nVars, int * pVarValues, char * pMvSop ) 
00922 {
00923     // for now, return the number of cubes in the MV-SOP
00924     int Counter = 0;
00925     while ( *pMvSop ) Counter += (*pMvSop++ == '\n');
00926     return Counter;
00927 }
00928 
00929 
00945 int Abc_NodeEvalMvCost( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 ) 
00946 {
00947     char * pMvSop;
00948     int * pVarValues;
00949     int i, RetValue;
00950     // collect the input and output values (currently, they are binary)
00951     pVarValues = ALLOC( int, nVars + 1 );
00952     for ( i = 0; i <= nVars; i++ )
00953         pVarValues[i] = 2;
00954     // prepare MV-SOP for evaluation
00955     pMvSop = Abc_NodeConvertSopToMvSop( nVars, vSop0, vSop1 );
00956     // have a look at the MV-SOP:
00957 //    printf( "%s\n", pMvSop );
00958     // get the result of internal cost evaluation
00959     RetValue = Abc_NodeEvalMvCostInternal( nVars, pVarValues, pMvSop );
00960     // cleanup
00961     free( pVarValues );
00962     free( pMvSop );
00963     return RetValue;
00964 }
00965 
00969 
00970