abc70930: src/base/abci/abcFraig.c Source File

00001 
00021 #include "abc.h"
00022 #include "fraig.h"
00023 #include "main.h"
00024 
00028 
00029 extern Abc_Ntk_t *    Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
00030 static Abc_Ntk_t *    Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
00031 static Abc_Obj_t *    Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig );
00032 static void           Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs );
00033 extern Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc );
00034 static void           Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
00035 
00036 static int            Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk );
00037 static void           Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
00038 static Abc_Obj_t *    Abc_NodeFraigTrust( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode );
00039  
00043 
00055 Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc )
00056 {
00057     Fraig_Params_t * pPars = pParams;
00058     Abc_Ntk_t * pNtkNew;
00059     Fraig_Man_t * pMan; 
00060     // check if EXDC is present
00061     if ( fExdc && pNtk->pExdc == NULL )
00062         fExdc = 0, printf( "Warning: Networks has no EXDC.\n" );
00063     // perform fraiging
00064     pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes, fExdc ); 
00065     // add algebraic choices
00066 //    if ( pPars->fChoicing )
00067 //        Fraig_ManAddChoices( pMan, 0, 6 );
00068     // prove the miter if asked to
00069     if ( pPars->fTryProve )
00070         Fraig_ManProveMiter( pMan );
00071     // reconstruct FRAIG in the new network
00072     if ( fExdc ) 
00073         pNtkNew = Abc_NtkFromFraig2( pMan, pNtk );
00074     else
00075         pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
00076     Fraig_ManFree( pMan );
00077     if ( pNtk->pExdc )
00078         pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
00079     // make sure that everything is okay
00080     if ( !Abc_NtkCheck( pNtkNew ) )
00081     {
00082         printf( "Abc_NtkFraig: The network check has failed.\n" );
00083         Abc_NtkDelete( pNtkNew );
00084         return NULL;
00085     }
00086     return pNtkNew;
00087 }
00088 
00100 void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc )
00101 {
00102     int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
00103     Fraig_Man_t * pMan;
00104     ProgressBar * pProgress;
00105     Vec_Ptr_t * vNodes;
00106     Abc_Obj_t * pNode;
00107     int i;
00108 
00109     assert( Abc_NtkIsStrash(pNtk) );
00110 
00111     // create the FRAIG manager
00112     pMan = Fraig_ManCreate( pParams );
00113 
00114     // map the constant node
00115     Abc_NtkCleanCopy( pNtk );
00116     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
00117     // create PIs and remember them in the old nodes
00118     Abc_NtkForEachCi( pNtk, pNode, i )
00119         pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
00120  
00121     // perform strashing
00122     vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
00123     if ( !fInternal )
00124         pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
00125     Vec_PtrForEachEntry( vNodes, pNode, i )
00126     {
00127         if ( Abc_ObjFaninNum(pNode) == 0 )
00128             continue;
00129         if ( !fInternal )
00130             Extra_ProgressBarUpdate( pProgress, i, NULL );
00131         pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
00132                 Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
00133                 Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
00134     }
00135     if ( !fInternal )
00136         Extra_ProgressBarStop( pProgress );
00137     Vec_PtrFree( vNodes );
00138 
00139     // use EXDC to change the mapping of nodes into FRAIG nodes
00140     if ( fExdc )
00141         Abc_NtkFraigRemapUsingExdc( pMan, pNtk );
00142 
00143     // set the primary outputs
00144     Abc_NtkForEachCo( pNtk, pNode, i )
00145         Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
00146     return pMan;
00147 }
00148 
00161 Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc )
00162 {
00163     Abc_Ntk_t * pNtkStrash;
00164     Abc_Obj_t * pObj;
00165     Fraig_Node_t * gResult;
00166     char ** ppNames;
00167     int i, k;
00168     // strash the EXDC network
00169     pNtkStrash = Abc_NtkStrash( pNtkExdc, 0, 0, 0 );
00170     Abc_NtkCleanCopy( pNtkStrash );
00171     Abc_AigConst1(pNtkStrash)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
00172     // set the mapping of the PI nodes
00173     ppNames = Abc_NtkCollectCioNames( pNtkMain, 0 );
00174     Abc_NtkForEachCi( pNtkStrash, pObj, i )
00175     {
00176         for ( k = 0; k < Abc_NtkCiNum(pNtkMain); k++ )
00177             if ( strcmp( Abc_ObjName(pObj), ppNames[k] ) == 0 )
00178             {
00179                 pObj->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, k);
00180                 break;
00181             }
00182         assert( pObj->pCopy != NULL );
00183     }
00184     free( ppNames );
00185     // build FRAIG for each node
00186     Abc_AigForEachAnd( pNtkStrash, pObj, i )
00187         pObj->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
00188                 Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ),
00189                 Fraig_NotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) ) );
00190     // get the EXDC to be returned
00191     pObj = Abc_NtkPo( pNtkStrash, 0 );
00192     gResult = Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
00193     Abc_NtkDelete( pNtkStrash );
00194     return gResult;
00195 }
00196 
00197 
00209 void Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
00210 {
00211     Fraig_Node_t * gNodeNew, * gNodeExdc;
00212     stmm_table * tTable;
00213     stmm_generator * gen;
00214     Abc_Obj_t * pNode, * pNodeBest;
00215     Abc_Obj_t * pClass, ** ppSlot;
00216     Vec_Ptr_t * vNexts;
00217     int i;
00218 
00219     // get the global don't-cares
00220     assert( pNtk->pExdc );
00221     gNodeExdc = Abc_NtkToFraigExdc( pMan, pNtk, pNtk->pExdc );
00222 
00223     // save the next pointers
00224     vNexts = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
00225     Abc_NtkForEachNode( pNtk, pNode, i )
00226         Vec_PtrWriteEntry( vNexts, pNode->Id, pNode->pNext );
00227 
00228     // find the classes of AIG nodes which have FRAIG nodes assigned
00229     Abc_NtkCleanNext( pNtk );
00230     tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
00231     Abc_NtkForEachNode( pNtk, pNode, i )
00232         if ( pNode->pCopy )
00233         {
00234             gNodeNew = Fraig_NodeAnd( pMan, (Fraig_Node_t *)pNode->pCopy, Fraig_Not(gNodeExdc) );
00235             if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(gNodeNew), (char ***)&ppSlot ) )
00236                 *ppSlot = NULL;
00237             pNode->pNext = *ppSlot;
00238             *ppSlot = pNode;
00239         }
00240 
00241     // for reach non-trival class, find the node with minimum level, and replace other nodes by it
00242     Abc_AigSetNodePhases( pNtk );
00243     stmm_foreach_item( tTable, gen, (char **)&gNodeNew, (char **)&pClass )
00244     {
00245         if ( pClass->pNext == NULL )
00246             continue;
00247         // find the node with minimum level
00248         pNodeBest = pClass;
00249         for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext )
00250             if ( pNodeBest->Level > pNode->Level )
00251                  pNodeBest = pNode;
00252         // remap the class nodes
00253         for ( pNode = pClass; pNode; pNode = pNode->pNext )
00254             pNode->pCopy = Abc_ObjNotCond( pNodeBest->pCopy, pNode->fPhase ^ pNodeBest->fPhase );
00255     }
00256     stmm_free_table( tTable );
00257 
00258     // restore the next pointers
00259     Abc_NtkCleanNext( pNtk );
00260     Abc_NtkForEachNode( pNtk, pNode, i )
00261         pNode->pNext = Vec_PtrEntry( vNexts, pNode->Id );
00262     Vec_PtrFree( vNexts );
00263 }
00264 
00276 Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
00277 {
00278     ProgressBar * pProgress;
00279     Abc_Ntk_t * pNtkNew;
00280     Abc_Obj_t * pNode, * pNodeNew;
00281     int i;
00282     // create the new network
00283     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
00284     // make the mapper point to the new network
00285     Abc_NtkForEachCi( pNtk, pNode, i )
00286         Fraig_NodeSetData1( Fraig_ManReadIthVar(pMan, i), (Fraig_Node_t *)pNode->pCopy );
00287     // set the constant node
00288     Fraig_NodeSetData1( Fraig_ManReadConst1(pMan), (Fraig_Node_t *)Abc_AigConst1(pNtkNew) );
00289     // process the nodes in topological order
00290     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
00291     Abc_NtkForEachCo( pNtk, pNode, i )
00292     {
00293         Extra_ProgressBarUpdate( pProgress, i, NULL );
00294         pNodeNew = Abc_NodeFromFraig_rec( pNtkNew, Fraig_ManReadOutputs(pMan)[i] );
00295         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
00296     }
00297     Extra_ProgressBarStop( pProgress );
00298     Abc_NtkReassignIds( pNtkNew );
00299     return pNtkNew;
00300 }
00301 
00313 Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig )
00314 {
00315     Abc_Obj_t * pRes, * pRes0, * pRes1, * pResMin, * pResCur;
00316     Fraig_Node_t * pNodeTemp, * pNodeFraigR = Fraig_Regular(pNodeFraig);
00317     void ** ppTail;
00318     // check if the node was already considered
00319     if ( pRes = (Abc_Obj_t *)Fraig_NodeReadData1(pNodeFraigR) )
00320         return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) );
00321     // solve the children
00322     pRes0 = Abc_NodeFromFraig_rec( pNtkNew, Fraig_NodeReadOne(pNodeFraigR) );
00323     pRes1 = Abc_NodeFromFraig_rec( pNtkNew, Fraig_NodeReadTwo(pNodeFraigR) );
00324     // derive the new node
00325     pRes = Abc_AigAnd( pNtkNew->pManFunc, pRes0, pRes1 );
00326     pRes->fPhase = Fraig_NodeReadSimInv( pNodeFraigR );
00327     // if the node has an equivalence class, find its representative
00328     if ( Fraig_NodeReadRepr(pNodeFraigR) == NULL && Fraig_NodeReadNextE(pNodeFraigR) != NULL )
00329     {
00330         // go through the FRAIG nodes belonging to this equivalence class
00331         // and find the representative node (the node with the smallest level)
00332         pResMin = pRes;
00333         for ( pNodeTemp = Fraig_NodeReadNextE(pNodeFraigR); pNodeTemp; pNodeTemp = Fraig_NodeReadNextE(pNodeTemp) )
00334         {
00335             assert( Fraig_NodeReadData1(pNodeTemp) == NULL );
00336             pResCur = Abc_NodeFromFraig_rec( pNtkNew, pNodeTemp );
00337             if ( pResMin->Level > pResCur->Level )
00338                 pResMin = pResCur;
00339         }
00340         // link the nodes in such a way that representative goes first
00341         ppTail = &pResMin->pData;
00342         if ( pRes != pResMin )
00343         {
00344             *ppTail = pRes;
00345             ppTail = &pRes->pData;
00346         }
00347         for ( pNodeTemp = Fraig_NodeReadNextE(pNodeFraigR); pNodeTemp; pNodeTemp = Fraig_NodeReadNextE(pNodeTemp) )
00348         {
00349             pResCur = (Abc_Obj_t *)Fraig_NodeReadData1(pNodeTemp);
00350             assert( pResCur );
00351             if ( pResMin == pResCur )
00352                 continue;
00353             *ppTail = pResCur;
00354             ppTail = &pResCur->pData;
00355         }
00356         assert( *ppTail == NULL );
00357 
00358         // update the phase of the node
00359         pRes = Abc_ObjNotCond( pResMin, (pRes->fPhase ^ pResMin->fPhase) );
00360     }
00361     Fraig_NodeSetData1( pNodeFraigR, (Fraig_Node_t *)pRes );
00362     return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) );
00363 }
00364 
00376 Abc_Ntk_t * Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
00377 {
00378     ProgressBar * pProgress;
00379     stmm_table * tTable;
00380     Vec_Ptr_t * vNodeReprs;
00381     Abc_Ntk_t * pNtkNew;
00382     Abc_Obj_t * pNode, * pRepr, ** ppSlot;
00383     int i;
00384 
00385     // map the nodes into their lowest level representives
00386     tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
00387     pNode = Abc_AigConst1(pNtk);
00388     if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
00389         *ppSlot = pNode;
00390     Abc_NtkForEachCi( pNtk, pNode, i )
00391         if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
00392             *ppSlot = pNode;
00393     Abc_NtkForEachNode( pNtk, pNode, i )
00394         if ( pNode->pCopy )
00395         {
00396             if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
00397                 *ppSlot = pNode;
00398             else if ( (*ppSlot)->Level > pNode->Level )
00399                 *ppSlot = pNode;
00400         }
00401     // save representatives for each node
00402     vNodeReprs = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
00403     Abc_NtkForEachNode( pNtk, pNode, i )
00404         if ( pNode->pCopy )
00405         {           
00406             if ( !stmm_lookup( tTable, (char *)Fraig_Regular(pNode->pCopy), (char **)&pRepr ) )
00407                 assert( 0 );
00408             if ( pNode != pRepr )
00409                 Vec_PtrWriteEntry( vNodeReprs, pNode->Id, pRepr );
00410         }
00411     stmm_free_table( tTable );
00412 
00413     // create the new network
00414     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
00415 
00416     // perform strashing
00417     Abc_AigSetNodePhases( pNtk );
00418     Abc_NtkIncrementTravId( pNtk );
00419     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
00420     Abc_NtkForEachCo( pNtk, pNode, i )
00421     {
00422         Extra_ProgressBarUpdate( pProgress, i, NULL );
00423         Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs );
00424     }
00425     Extra_ProgressBarStop( pProgress );
00426     Vec_PtrFree( vNodeReprs );
00427 
00428     // finalize the network
00429     Abc_NtkFinalize( pNtk, pNtkNew );
00430     return pNtkNew;
00431 }
00432 
00433 
00445 void Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs )
00446 {
00447     Abc_Obj_t * pRepr;
00448     // skip the PIs and constants
00449     if ( Abc_ObjFaninNum(pNode) < 2 )
00450         return;
00451     // if this node is already visited, skip
00452     if ( Abc_NodeIsTravIdCurrent( pNode ) )
00453         return;
00454     // mark the node as visited
00455     Abc_NodeSetTravIdCurrent( pNode );
00456     assert( Abc_ObjIsNode( pNode ) );
00457     // get the node's representative
00458     if ( pRepr = Vec_PtrEntry(vNodeReprs, pNode->Id) )
00459     {
00460         Abc_NtkFromFraig2_rec( pNtkNew, pRepr, vNodeReprs );
00461         pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pRepr->fPhase ^ pNode->fPhase );
00462         return;
00463     }
00464     Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs );
00465     Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin1(pNode), vNodeReprs );
00466     pNode->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
00467 }
00468 
00469 
00470 
00482 Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
00483 {
00484     Abc_Ntk_t * pNtkNew;
00485 
00486     if ( !Abc_NtkIsSopLogic(pNtk) )
00487     {
00488         printf( "Abc_NtkFraigTrust: Trust mode works for netlists and logic SOP networks.\n" );
00489         return NULL;
00490     }
00491 
00492     if ( !Abc_NtkFraigTrustCheck(pNtk) )
00493     {
00494         printf( "Abc_NtkFraigTrust: The network does not look like an AIG with choice nodes.\n" );
00495         return NULL;
00496     }
00497     
00498     // perform strashing
00499     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
00500     Abc_NtkFraigTrustOne( pNtk, pNtkNew );
00501     Abc_NtkFinalize( pNtk, pNtkNew );
00502     Abc_NtkReassignIds( pNtkNew );
00503 
00504     // print a warning about choice nodes
00505     printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) );
00506 
00507     // make sure that everything is okay
00508     if ( !Abc_NtkCheck( pNtkNew ) )
00509     {
00510         printf( "Abc_NtkFraigTrust: The network check has failed.\n" );
00511         Abc_NtkDelete( pNtkNew );
00512         return NULL;
00513     }
00514     return pNtkNew;
00515 }
00516 
00528 int Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk )
00529 {
00530     Abc_Obj_t * pNode;
00531     int i, nFanins;
00532     Abc_NtkForEachNode( pNtk, pNode, i )
00533     {
00534         nFanins = Abc_ObjFaninNum(pNode);
00535         if ( nFanins < 2 )
00536             continue;
00537         if ( nFanins == 2 && Abc_SopIsAndType(pNode->pData) )
00538             continue;
00539         if ( !Abc_SopIsOrType(pNode->pData) )
00540             return 0;
00541     }
00542     return 1;
00543 }
00544 
00556 void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
00557 {
00558     ProgressBar * pProgress;
00559     Vec_Ptr_t * vNodes;
00560     Abc_Obj_t * pNode, * pNodeNew, * pObj;
00561     int i;
00562 
00563     // perform strashing
00564     vNodes = Abc_NtkDfs( pNtk, 0 );
00565     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
00566     Vec_PtrForEachEntry( vNodes, pNode, i )
00567     {
00568         Extra_ProgressBarUpdate( pProgress, i, NULL );
00569         // get the node
00570         assert( Abc_ObjIsNode(pNode) );
00571          // strash the node
00572         pNodeNew = Abc_NodeFraigTrust( pNtkNew, pNode );
00573         // get the old object
00574         if ( Abc_NtkIsNetlist(pNtk) )
00575             pObj = Abc_ObjFanout0( pNode ); // the fanout net 
00576         else 
00577             pObj = pNode; // the node itself
00578         // make sure the node is not yet strashed
00579         assert( pObj->pCopy == NULL );
00580         // mark the old object with the new AIG node
00581         pObj->pCopy = pNodeNew;
00582     }
00583     Vec_PtrFree( vNodes );
00584     Extra_ProgressBarStop( pProgress );
00585 }
00586 
00598 Abc_Obj_t * Abc_NodeFraigTrust( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
00599 {
00600     Abc_Obj_t * pSum, * pFanin;
00601     void ** ppTail;
00602     int i, nFanins, fCompl;
00603 
00604     assert( Abc_ObjIsNode(pNode) );
00605     // get the number of node's fanins
00606     nFanins = Abc_ObjFaninNum( pNode );
00607     assert( nFanins == Abc_SopGetVarNum(pNode->pData) );
00608     // check if it is a constant
00609     if ( nFanins == 0 )
00610         return Abc_ObjNotCond( Abc_AigConst1(pNtkNew), Abc_SopIsConst0(pNode->pData) );
00611     if ( nFanins == 1 )
00612         return Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_SopIsInv(pNode->pData) );
00613     if ( nFanins == 2 && Abc_SopIsAndType(pNode->pData) )
00614         return Abc_AigAnd( pNtkNew->pManFunc, 
00615             Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, !Abc_SopGetIthCareLit(pNode->pData,0) ),
00616             Abc_ObjNotCond( Abc_ObjFanin1(pNode)->pCopy, !Abc_SopGetIthCareLit(pNode->pData,1) )  );
00617     assert( Abc_SopIsOrType(pNode->pData) );
00618     fCompl = Abc_SopGetIthCareLit(pNode->pData,0);
00619     // get the root of the choice node (the first fanin)
00620     pSum = Abc_ObjFanin0(pNode)->pCopy;
00621     // connect other fanins
00622     ppTail = &pSum->pData;
00623     Abc_ObjForEachFanin( pNode, pFanin, i )
00624     {
00625         if ( i == 0 )
00626             continue;
00627         *ppTail = pFanin->pCopy;
00628         ppTail = &pFanin->pCopy->pData;
00629         // set the complemented bit of this cut
00630         if ( fCompl ^ Abc_SopGetIthCareLit(pNode->pData, i) )
00631             pFanin->pCopy->fPhase = 1;
00632     }
00633     assert( *ppTail == NULL );
00634     return pSum;
00635 }
00636 
00637 
00638 
00639 
00651 int Abc_NtkFraigStore( Abc_Ntk_t * pNtkAdd )
00652 {
00653     Vec_Ptr_t * vStore;
00654     Abc_Ntk_t * pNtk;
00655     // create the network to be stored
00656     pNtk = Abc_NtkStrash( pNtkAdd, 0, 0, 0 );
00657     if ( pNtk == NULL )
00658     {
00659         printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );
00660         return 0;
00661     }
00662     // get the network currently stored
00663     vStore = Abc_FrameReadStore();
00664     if ( Vec_PtrSize(vStore) > 0 )
00665     {
00666         // check that the networks have the same PIs
00667         // reorder PIs of pNtk2 according to pNtk1
00668         if ( !Abc_NtkCompareSignals( pNtk, Vec_PtrEntry(vStore, 0), 1, 1 ) )
00669         {
00670             printf( "Trying to store the network with different primary inputs.\n" );
00671             printf( "The previously stored networks are deleted and this one is added.\n" );
00672             Abc_NtkFraigStoreClean();
00673         }
00674     }
00675     Vec_PtrPush( vStore, pNtk );
00676 //    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) );
00677     return 1;
00678 }
00679 
00691 Abc_Ntk_t * Abc_NtkFraigRestore()
00692 {
00693     extern Abc_Ntk_t * Abc_NtkFraigPartitioned( Vec_Ptr_t * vStore, void * pParams );
00694     Fraig_Params_t Params;
00695     Vec_Ptr_t * vStore;
00696     Abc_Ntk_t * pNtk, * pFraig;
00697     int nWords1, nWords2, nWordsMin;
00698     int clk = clock();
00699 
00700     // get the stored network
00701     vStore = Abc_FrameReadStore();
00702     if ( Vec_PtrSize(vStore) == 0 )
00703     {
00704         printf( "There are no network currently in storage.\n" );
00705         return NULL;
00706     }
00707 //    printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) );
00708     pNtk = Vec_PtrEntry( vStore, 0 );
00709 
00710     // swap the first and last network
00711     // this should lead to the primary choice being "better" because of synthesis
00712     pNtk = Vec_PtrPop( vStore );
00713     Vec_PtrPush( vStore, Vec_PtrEntry(vStore,0) );
00714     Vec_PtrWriteEntry( vStore, 0, pNtk );
00715 
00716     // to determine the number of simulation patterns
00717     // use the following strategy
00718     // at least 64 words (32 words random and 32 words dynamic)
00719     // no more than 256M for one circuit (128M + 128M)
00720     nWords1 = 32;
00721     nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk));
00722     nWordsMin = ABC_MIN( nWords1, nWords2 );
00723 
00724     // set parameters for fraiging
00725     Fraig_ParamsSetDefault( &Params );
00726     Params.nPatsRand  = nWordsMin * 32;    // the number of words of random simulation info
00727     Params.nPatsDyna  = nWordsMin * 32;    // the number of words of dynamic simulation info
00728     Params.nBTLimit   = 1000;              // the max number of backtracks to perform
00729     Params.fFuncRed   =    1;              // performs only one level hashing
00730     Params.fFeedBack  =    1;              // enables solver feedback
00731     Params.fDist1Pats =    1;              // enables distance-1 patterns
00732     Params.fDoSparse  =    1;              // performs equiv tests for sparse functions 
00733     Params.fChoicing  =    1;              // enables recording structural choices
00734     Params.fTryProve  =    0;              // tries to solve the final miter
00735     Params.fVerbose   =    0;              // the verbosiness flag
00736 
00737     // perform partitioned computation of structural choices
00738     pFraig = Abc_NtkFraigPartitioned( vStore, &Params );
00739     Abc_NtkFraigStoreClean();
00740 //PRT( "Total choicing time", clock() - clk );
00741     return pFraig;
00742 }
00743 
00755 void Abc_NtkFraigStoreClean()
00756 {
00757     Vec_Ptr_t * vStore;
00758     Abc_Ntk_t * pNtk;
00759     int i;
00760     vStore = Abc_FrameReadStore();
00761     Vec_PtrForEachEntry( vStore, pNtk, i )
00762         Abc_NtkDelete( pNtk );
00763     Vec_PtrClear( vStore );
00764 }
00765 
00777 void Abc_NtkFraigStoreCheck( Abc_Ntk_t * pFraig )
00778 {
00779     Abc_Obj_t * pNode0, * pNode1;
00780     int nPoOrig, nPoFinal, nStored; 
00781     int i, k;
00782     // check that the PO functions are correct
00783     nPoFinal = Abc_NtkPoNum(pFraig);
00784     nStored  = Abc_FrameReadStoreSize();
00785     assert( nPoFinal % nStored == 0 );
00786     nPoOrig  = nPoFinal / nStored;
00787     for ( i = 0; i < nPoOrig; i++ )
00788     {
00789         pNode0 = Abc_ObjFanin0( Abc_NtkPo(pFraig, i) ); 
00790         for ( k = 1; k < nStored; k++ )
00791         {
00792             pNode1 = Abc_ObjFanin0( Abc_NtkPo(pFraig, k*nPoOrig+i) ); 
00793             if ( pNode0 != pNode1 )
00794                 printf( "Verification for PO #%d of network #%d has failed. The PO function is not used.\n", i+1, k+1 );
00795         }
00796     }
00797 }
00798 
00802 
00803