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

00001 
00021 #include "abc.h"
00022 #include "dec.h"
00023 #include "ivy.h"
00024 #include "fraig.h"
00025 
00029 
00030 static Abc_Ntk_t *  Abc_NtkFromIvy( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
00031 static Abc_Ntk_t *  Abc_NtkFromIvySeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig );
00032 static Ivy_Man_t *  Abc_NtkToIvy( Abc_Ntk_t * pNtkOld );
00033 
00034 static void         Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan );
00035 static Ivy_Obj_t *  Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode );
00036 static Ivy_Obj_t *  Abc_NodeStrashAigSopAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
00037 static Ivy_Obj_t *  Abc_NodeStrashAigExorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
00038 static Ivy_Obj_t *  Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
00039 extern char *       Mio_GateReadSop( void * pGate );
00040 
00041 typedef int   Abc_Edge_t;
00042 static inline Abc_Edge_t   Abc_EdgeCreate( int Id, int fCompl )                { return (Id << 1) | fCompl;             }
00043 static inline int          Abc_EdgeId( Abc_Edge_t Edge )                       { return Edge >> 1;                      }
00044 static inline int          Abc_EdgeIsComplement( Abc_Edge_t Edge )             { return Edge & 1;                       }
00045 static inline Abc_Edge_t   Abc_EdgeRegular( Abc_Edge_t Edge )                  { return (Edge >> 1) << 1;               }
00046 static inline Abc_Edge_t   Abc_EdgeNot( Abc_Edge_t Edge )                      { return Edge ^ 1;                       }
00047 static inline Abc_Edge_t   Abc_EdgeNotCond( Abc_Edge_t Edge, int fCond )       { return Edge ^ fCond;                   }
00048 static inline Abc_Edge_t   Abc_EdgeFromNode( Abc_Obj_t * pNode )               { return Abc_EdgeCreate( Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) );       }
00049 static inline Abc_Obj_t *  Abc_EdgeToNode( Abc_Ntk_t * p, Abc_Edge_t Edge )    { return Abc_ObjNotCond( Abc_NtkObj(p, Abc_EdgeId(Edge)), Abc_EdgeIsComplement(Edge) ); }
00050 
00051 static inline Abc_Obj_t *  Abc_ObjFanin0Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ); }
00052 static inline Abc_Obj_t *  Abc_ObjFanin1Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ); }
00053 
00054 static Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs );
00055 
00056 extern int timeRetime;
00057 
00061 
00073 Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
00074 {
00075     Ivy_Man_t * pMan;
00076     int fCleanup = 1;
00077 //timeRetime = clock();
00078     assert( !Abc_NtkIsNetlist(pNtk) );
00079     if ( Abc_NtkIsBddLogic(pNtk) )
00080     {
00081         if ( !Abc_NtkBddToSop(pNtk, 0) )
00082         {
00083             printf( "Abc_NtkIvyBefore(): Converting to SOPs has failed.\n" );
00084             return NULL;
00085         }
00086     }
00087     if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) )
00088     {
00089         printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
00090 //        return NULL;
00091     }
00092     // print warning about choice nodes
00093     if ( Abc_NtkGetChoiceNum( pNtk ) )
00094         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
00095     // convert to the AIG manager
00096     pMan = Abc_NtkToIvy( pNtk );
00097     if ( !Ivy_ManCheck( pMan ) )
00098     {
00099         printf( "AIG check has failed.\n" );
00100         Ivy_ManStop( pMan );
00101         return NULL;
00102     }
00103 //    Ivy_ManPrintStats( pMan );
00104     if ( fSeq )
00105     {
00106         int nLatches = Abc_NtkLatchNum(pNtk);
00107         Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, fUseDc );
00108         Ivy_ManMakeSeq( pMan, nLatches, vInit->pArray );
00109         Vec_IntFree( vInit );
00110 //        Ivy_ManPrintStats( pMan );
00111     }
00112 //timeRetime = clock() - timeRetime;
00113     return pMan;
00114 }
00115 
00127 Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq, int fHaig )
00128 {
00129     Abc_Ntk_t * pNtkAig;
00130     int nNodes, fCleanup = 1;
00131     // convert from the AIG manager
00132     if ( fSeq )
00133         pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan, fHaig );
00134     else
00135         pNtkAig = Abc_NtkFromIvy( pNtk, pMan );
00136     // report the cleanup results
00137     if ( !fHaig && fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
00138         printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
00139     // duplicate EXDC 
00140     if ( pNtk->pExdc )
00141         pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
00142     // make sure everything is okay
00143     if ( !Abc_NtkCheck( pNtkAig ) )
00144     {
00145         printf( "Abc_NtkStrash: The network check has failed.\n" );
00146         Abc_NtkDelete( pNtkAig );
00147         return NULL;
00148     }
00149     return pNtkAig;
00150 }
00151 
00163 Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk )
00164 {
00165     Abc_Ntk_t * pNtkAig;
00166     Ivy_Man_t * pMan;
00167     pMan = Abc_NtkIvyBefore( pNtk, 1, 0 );
00168     if ( pMan == NULL )
00169         return NULL;
00170     pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
00171     Ivy_ManStop( pMan );
00172     return pNtkAig;
00173 }
00174  
00186 Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int fVerbose )
00187 {
00188     Abc_Ntk_t * pNtkAig;
00189     Ivy_Man_t * pMan;
00190     int clk;
00191 //    int i;
00192 /*
00193 extern int nMoves;
00194 extern int nMovesS;
00195 extern int nClauses;
00196 extern int timeInv;
00197 
00198 nMoves = 0;
00199 nMovesS = 0;
00200 nClauses = 0;
00201 timeInv = 0;
00202 */
00203     pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
00204     if ( pMan == NULL )
00205         return NULL;
00206 //timeRetime = clock();
00207 
00208 clk = clock();
00209     Ivy_ManHaigStart( pMan, fVerbose );
00210 //    Ivy_ManRewriteSeq( pMan, 0, 0 );
00211 //    for ( i = 0; i < nIters; i++ )
00212 //        Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
00213 
00214 //printf( "%d ", Ivy_ManNodeNum(pMan) );
00215     Ivy_ManRewriteSeq( pMan, 0, 0 );
00216     Ivy_ManRewriteSeq( pMan, 0, 0 );
00217     Ivy_ManRewriteSeq( pMan, 1, 0 );
00218 //printf( "%d ", Ivy_ManNodeNum(pMan) );
00219 //printf( "%d ", Ivy_ManNodeNum(pMan->pHaig) );
00220 //PRT( " ", clock() - clk );
00221 //printf( "\n" );
00222 /*
00223     printf( "Moves = %d.  ", nMoves );
00224     printf( "MovesS = %d.  ", nMovesS );
00225     printf( "Clauses = %d.  ", nClauses );
00226     PRT( "Time", timeInv );
00227 */
00228 //    Ivy_ManRewriteSeq( pMan, 1, 0 );
00229 //printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) );
00230 //    Ivy_ManHaigPostprocess( pMan, fVerbose );
00231 //timeRetime = clock() - timeRetime;
00232 
00233     // write working AIG into the current network
00234 //    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 ); 
00235     // write HAIG into the current network
00236     pNtkAig = Abc_NtkIvyAfter( pNtk, pMan->pHaig, 1, 1 );
00237 
00238     Ivy_ManHaigStop( pMan );
00239     Ivy_ManStop( pMan );
00240     return pNtkAig;
00241 }
00242 
00254 void Abc_NtkIvyCuts( Abc_Ntk_t * pNtk, int nInputs )
00255 {
00256     extern void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs );
00257     Ivy_Man_t * pMan;
00258     pMan = Abc_NtkIvyBefore( pNtk, 1, 0 );
00259     if ( pMan == NULL )
00260         return;
00261     Ivy_CutComputeAll( pMan, nInputs );
00262     Ivy_ManStop( pMan );
00263 }
00264 
00276 Abc_Ntk_t * Abc_NtkIvyRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeroCost, int fVerbose )
00277 {
00278     Abc_Ntk_t * pNtkAig;
00279     Ivy_Man_t * pMan;
00280     pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
00281     if ( pMan == NULL )
00282         return NULL;
00283 //timeRetime = clock();
00284     Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose );
00285 //timeRetime = clock() - timeRetime;
00286     pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
00287     Ivy_ManStop( pMan );
00288     return pNtkAig;
00289 }
00290 
00302 Abc_Ntk_t * Abc_NtkIvyRewriteSeq( Abc_Ntk_t * pNtk, int fUseZeroCost, int fVerbose )
00303 {
00304     Abc_Ntk_t * pNtkAig;
00305     Ivy_Man_t * pMan;
00306     pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
00307     if ( pMan == NULL )
00308         return NULL;
00309 //timeRetime = clock();
00310     Ivy_ManRewriteSeq( pMan, fUseZeroCost, fVerbose );
00311 //timeRetime = clock() - timeRetime;
00312 //    Ivy_ManRewriteSeq( pMan, 1, 0 );
00313 //    Ivy_ManRewriteSeq( pMan, 1, 0 );
00314     pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
00315     Ivy_ManStop( pMan );
00316     return pNtkAig;
00317 }
00318 
00330 Abc_Ntk_t * Abc_NtkIvyResyn0( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
00331 {
00332     Abc_Ntk_t * pNtkAig;
00333     Ivy_Man_t * pMan, * pTemp;
00334     pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
00335     if ( pMan == NULL )
00336         return NULL;
00337     pMan = Ivy_ManResyn0( pTemp = pMan, fUpdateLevel, fVerbose );
00338     Ivy_ManStop( pTemp );
00339     pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
00340     Ivy_ManStop( pMan );
00341     return pNtkAig;
00342 }
00343 
00355 Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
00356 {
00357     Abc_Ntk_t * pNtkAig;
00358     Ivy_Man_t * pMan, * pTemp;
00359     pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
00360     if ( pMan == NULL )
00361         return NULL;
00362     pMan = Ivy_ManResyn( pTemp = pMan, fUpdateLevel, fVerbose );
00363     Ivy_ManStop( pTemp );
00364     pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
00365     Ivy_ManStop( pMan );
00366     return pNtkAig;
00367 }
00368 
00380 Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
00381 {
00382     Ivy_FraigParams_t Params, * pParams = &Params; 
00383     Abc_Ntk_t * pNtkAig;
00384     Ivy_Man_t * pMan, * pTemp;
00385     pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
00386     if ( pMan == NULL )
00387         return NULL;
00388     Ivy_FraigParamsDefault( pParams );
00389     pParams->nBTLimitMiter = nConfLimit;
00390     pParams->fVerbose = fVerbose;
00391 //    pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
00392     pMan = Ivy_FraigMiter( pTemp = pMan, pParams );
00393     Ivy_ManStop( pTemp );
00394     pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
00395     Ivy_ManStop( pMan );
00396     return pNtkAig;
00397 }
00398 
00410 void Abc_NtkTransferPointers( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig )
00411 {
00412     Abc_Obj_t * pObj;
00413     Ivy_Obj_t * pObjIvy, * pObjFraig;
00414     int i;
00415     pObj = Abc_AigConst1(pNtk);
00416     pObj->pCopy = Abc_AigConst1(pNtkAig);
00417     Abc_NtkForEachCi( pNtk, pObj, i )
00418         pObj->pCopy = Abc_NtkCi(pNtkAig, i);
00419     Abc_NtkForEachCo( pNtk, pObj, i )
00420         pObj->pCopy = Abc_NtkCo(pNtkAig, i);
00421     Abc_NtkForEachLatch( pNtk, pObj, i )
00422         pObj->pCopy = Abc_NtkBox(pNtkAig, i);
00423     Abc_NtkForEachNode( pNtk, pObj, i )
00424     {
00425         pObjIvy = (Ivy_Obj_t *)pObj->pCopy;
00426         if ( pObjIvy == NULL )
00427             continue;
00428         pObjFraig = Ivy_ObjEquiv( pObjIvy );
00429         if ( pObjFraig == NULL )
00430             continue;
00431         pObj->pCopy = Abc_EdgeToNode( pNtkAig, Ivy_Regular(pObjFraig)->TravId );
00432         pObj->pCopy = Abc_ObjNotCond( pObj->pCopy, Ivy_IsComplement(pObjFraig) );
00433     }
00434 }
00435 
00447 Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose )
00448 {
00449     Ivy_FraigParams_t Params, * pParams = &Params; 
00450     Abc_Ntk_t * pNtkAig;
00451     Ivy_Man_t * pMan, * pTemp;
00452     pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
00453     if ( pMan == NULL )
00454         return NULL;
00455     Ivy_FraigParamsDefault( pParams );
00456     pParams->nBTLimitNode = nConfLimit;
00457     pParams->fVerbose     = fVerbose;
00458     pParams->fProve       = fProve;
00459     pParams->fDoSparse    = fDoSparse;
00460     pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
00461     // transfer the pointers
00462     if ( fTransfer == 1 )
00463     {
00464         Vec_Ptr_t * vCopies;
00465         vCopies = Abc_NtkSaveCopy( pNtk );
00466         pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
00467         Abc_NtkLoadCopy( pNtk, vCopies );
00468         Vec_PtrFree( vCopies );
00469         Abc_NtkTransferPointers( pNtk, pNtkAig );
00470     }
00471     else
00472         pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
00473     Ivy_ManStop( pTemp );
00474     Ivy_ManStop( pMan );
00475     return pNtkAig;
00476 }
00477 
00489 int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
00490 {
00491     Prove_Params_t * pParams = pPars;
00492     Abc_Ntk_t * pNtk = *ppNtk, * pNtkTemp;
00493     Abc_Obj_t * pObj, * pFanin;
00494     Ivy_Man_t * pMan;
00495     int RetValue;
00496     assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
00497     // experiment with various parameters settings
00498 //    pParams->fUseBdds = 1;
00499 //    pParams->fBddReorder = 1;
00500 //    pParams->nTotalBacktrackLimit = 10000;
00501 
00502     // strash the network if it is not strashed already
00503     if ( !Abc_NtkIsStrash(pNtk) )
00504     {
00505         pNtk = Abc_NtkStrash( pNtkTemp = pNtk, 0, 1, 0 );
00506         Abc_NtkDelete( pNtkTemp );
00507     }
00508 
00509     // check the case when the 0000 simulation pattern detect the bug
00510     pObj = Abc_NtkPo(pNtk,0);
00511     pFanin = Abc_ObjFanin0(pObj);
00512     if ( Abc_ObjFanin0(pObj)->fPhase != (unsigned)Abc_ObjFaninC0(pObj) )
00513     {
00514         pNtk->pModel = ALLOC( int, Abc_NtkPiNum(pNtk) );
00515         memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkPiNum(pNtk) );
00516         return 0;
00517     }
00518 
00519     // if SAT only, solve without iteration
00520     RetValue = Abc_NtkMiterSat( pNtk, 2*(sint64)pParams->nMiteringLimitStart, (sint64)0, 0, NULL, NULL );
00521     if ( RetValue >= 0 )
00522         return RetValue;
00523 
00524     // apply AIG rewriting
00525     if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 )
00526     {
00527         pParams->fUseRewriting = 0;
00528         pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
00529         Abc_NtkDelete( pNtkTemp );
00530         Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00531         pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
00532         Abc_NtkDelete( pNtkTemp );
00533         Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00534         Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
00535     }
00536 
00537     // convert ABC network into IVY network
00538     pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
00539 
00540     // solve the CEC problem
00541     RetValue = Ivy_FraigProve( &pMan, pParams );
00542     // convert IVY network into ABC network    
00543     pNtk = Abc_NtkIvyAfter( pNtkTemp = pNtk, pMan, 0, 0 );
00544     Abc_NtkDelete( pNtkTemp );
00545     // transfer model if given
00546     pNtk->pModel = pMan->pData; pMan->pData = NULL;
00547     Ivy_ManStop( pMan );
00548 
00549     // try to prove it using brute force SAT
00550     if ( RetValue < 0 && pParams->fUseBdds )
00551     {
00552         if ( pParams->fVerbose )
00553         {
00554             printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
00555             fflush( stdout );
00556         }
00557         pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
00558         if ( pNtk )   
00559         {
00560             Abc_NtkDelete( pNtkTemp );
00561             RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero(pNtk->pManFunc)) );
00562         }
00563         else 
00564             pNtk = pNtkTemp;
00565     }
00566 
00567     // return the result
00568     *ppNtk = pNtk;
00569     return RetValue;
00570 }
00571 
00583 Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
00584 {
00585 //    Abc_Ntk_t * pNtkAig;
00586     Ivy_Man_t * pMan;//, * pTemp;
00587     int fCleanup = 1;
00588 //    int nNodes;
00589     int nLatches = Abc_NtkLatchNum(pNtk);
00590     Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, 0 );
00591 
00592     assert( !Abc_NtkIsNetlist(pNtk) );
00593     if ( Abc_NtkIsBddLogic(pNtk) )
00594     {
00595         if ( !Abc_NtkBddToSop(pNtk, 0) )
00596         {
00597             Vec_IntFree( vInit );
00598             printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" );
00599             return NULL;
00600         }
00601     }
00602     if ( Abc_NtkCountSelfFeedLatches(pNtk) )
00603     {
00604         printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
00605         return NULL;
00606     }
00607 
00608     // print warning about choice nodes
00609     if ( Abc_NtkGetChoiceNum( pNtk ) )
00610         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
00611 
00612     // convert to the AIG manager
00613     pMan = Abc_NtkToIvy( pNtk );
00614     if ( !Ivy_ManCheck( pMan ) )
00615     {
00616         Vec_IntFree( vInit );
00617         printf( "AIG check has failed.\n" );
00618         Ivy_ManStop( pMan );
00619         return NULL;
00620     }
00621 
00622 //    Ivy_MffcTest( pMan );
00623 //    Ivy_ManPrintStats( pMan );
00624 
00625 //    pMan = Ivy_ManBalance( pTemp = pMan, 1 );
00626 //    Ivy_ManStop( pTemp );
00627 
00628 //    Ivy_ManSeqRewrite( pMan, 0, 0 );
00629 //    Ivy_ManTestCutsAlg( pMan );
00630 //    Ivy_ManTestCutsBool( pMan );
00631 //    Ivy_ManRewriteAlg( pMan, 1, 1 );
00632 
00633 //    pMan = Ivy_ManResyn( pTemp = pMan, 1, 0 );
00634 //    Ivy_ManStop( pTemp );
00635 
00636 //    Ivy_ManTestCutsAll( pMan );
00637 //    Ivy_ManTestCutsTravAll( pMan );
00638 
00639 //    Ivy_ManPrintStats( pMan );
00640 
00641 //    Ivy_ManPrintStats( pMan );
00642 //    Ivy_ManRewritePre( pMan, 1, 0, 0 );
00643 //    Ivy_ManPrintStats( pMan );
00644 //    printf( "\n" );
00645 
00646 //    Ivy_ManPrintStats( pMan );
00647 //    Ivy_ManMakeSeq( pMan, nLatches, pInit );
00648 //    Ivy_ManPrintStats( pMan );
00649 
00650 //    Ivy_ManRequiredLevels( pMan );
00651 
00652 //    Ivy_FastMapPerform( pMan, 8 );
00653     Ivy_ManStop( pMan );
00654     return NULL;
00655 
00656 
00657 /*
00658     // convert from the AIG manager
00659     pNtkAig = Abc_NtkFromIvy( pNtk, pMan );
00660 //    pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan );
00661     Ivy_ManStop( pMan );
00662 
00663     // report the cleanup results
00664     if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
00665         printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
00666     // duplicate EXDC 
00667     if ( pNtk->pExdc )
00668         pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
00669     // make sure everything is okay
00670     if ( !Abc_NtkCheck( pNtkAig ) )
00671     {
00672         FREE( pInit );
00673         printf( "Abc_NtkStrash: The network check has failed.\n" );
00674         Abc_NtkDelete( pNtkAig );
00675         return NULL;
00676     }
00677 
00678     FREE( pInit );
00679     return pNtkAig;
00680 */
00681 }
00682 
00683 
00684 
00696 Abc_Ntk_t * Abc_NtkFromIvy( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
00697 {
00698     Vec_Int_t * vNodes;
00699     Abc_Ntk_t * pNtk;
00700     Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
00701     Ivy_Obj_t * pNode;
00702     int i;
00703     // perform strashing
00704     pNtk = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
00705     // transfer the pointers to the basic nodes
00706     Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_AigConst1(pNtk) );
00707     Abc_NtkForEachCi( pNtkOld, pObj, i )
00708         Ivy_ManPi(pMan, i)->TravId = Abc_EdgeFromNode( pObj->pCopy );
00709     // rebuild the AIG
00710     vNodes = Ivy_ManDfs( pMan );
00711     Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i )
00712     {
00713         // add the first fanin
00714         pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode );
00715         if ( Ivy_ObjIsBuf(pNode) )
00716         {
00717             pNode->TravId = Abc_EdgeFromNode( pFaninNew0 );
00718             continue;
00719         }
00720         // add the second fanin
00721         pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode );
00722         // create the new node
00723         if ( Ivy_ObjIsExor(pNode) )
00724             pObjNew = Abc_AigXor( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
00725         else
00726             pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
00727         pNode->TravId = Abc_EdgeFromNode( pObjNew );
00728     }
00729     // connect the PO nodes
00730     Abc_NtkForEachCo( pNtkOld, pObj, i )
00731     {
00732         pFaninNew = Abc_ObjFanin0Ivy( pNtk, Ivy_ManPo(pMan, i) );
00733         Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
00734     }
00735     Vec_IntFree( vNodes );
00736     if ( !Abc_NtkCheck( pNtk ) )
00737         fprintf( stdout, "Abc_NtkFromIvy(): Network check has failed.\n" );
00738     return pNtk;
00739 }
00740 
00752 Abc_Ntk_t * Abc_NtkFromIvySeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig )
00753 {
00754     Vec_Int_t * vNodes, * vLatches;
00755     Abc_Ntk_t * pNtk;
00756     Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
00757     Ivy_Obj_t * pNode, * pTemp;
00758     int i;
00759 //    assert( Ivy_ManLatchNum(pMan) > 0 );
00760     // perform strashing
00761     pNtk = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
00762     // transfer the pointers to the basic nodes
00763     Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_AigConst1(pNtk) );
00764     Abc_NtkForEachPi( pNtkOld, pObj, i )
00765         Ivy_ManPi(pMan, i)->TravId = Abc_EdgeFromNode( pObj->pCopy );
00766     // create latches of the new network
00767     vNodes = Ivy_ManDfsSeq( pMan, &vLatches );
00768     Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i )
00769     {
00770         pObjNew = Abc_NtkCreateLatch( pNtk );
00771         pFaninNew0 = Abc_NtkCreateBi( pNtk );
00772         pFaninNew1 = Abc_NtkCreateBo( pNtk );
00773         Abc_ObjAddFanin( pObjNew, pFaninNew0 );
00774         Abc_ObjAddFanin( pFaninNew1, pObjNew );
00775         if ( fHaig || Ivy_ObjInit(pNode) == IVY_INIT_DC )
00776             Abc_LatchSetInitDc( pObjNew );
00777         else if ( Ivy_ObjInit(pNode) == IVY_INIT_1 )
00778             Abc_LatchSetInit1( pObjNew );
00779         else if ( Ivy_ObjInit(pNode) == IVY_INIT_0 )
00780             Abc_LatchSetInit0( pObjNew );
00781         else assert( 0 );
00782         pNode->TravId = Abc_EdgeFromNode( pFaninNew1 );
00783     }
00784     Abc_NtkAddDummyBoxNames( pNtk );
00785     // rebuild the AIG
00786     Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i )
00787     {
00788         // add the first fanin
00789         pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode );
00790         if ( Ivy_ObjIsBuf(pNode) )
00791         {
00792             pNode->TravId = Abc_EdgeFromNode( pFaninNew0 );
00793             continue;
00794         }
00795         // add the second fanin
00796         pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode );
00797         // create the new node
00798         if ( Ivy_ObjIsExor(pNode) )
00799             pObjNew = Abc_AigXor( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
00800         else
00801             pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
00802         pNode->TravId = Abc_EdgeFromNode( pObjNew );
00803         // process the choice nodes
00804         if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 )
00805         {
00806             pFaninNew = Abc_EdgeToNode( pNtk, pNode->TravId );
00807 //            pFaninNew->fPhase = 0;
00808             assert( !Ivy_IsComplement(pNode->pEquiv) );
00809             for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) )
00810             {
00811                 pFaninNew1 = Abc_EdgeToNode( pNtk, pTemp->TravId );
00812 //                pFaninNew1->fPhase = Ivy_IsComplement( pTemp->pEquiv );
00813                 pFaninNew->pData = pFaninNew1;
00814                 pFaninNew = pFaninNew1;
00815             }
00816             pFaninNew->pData = NULL;
00817 //            printf( "Writing choice node %d.\n", pNode->Id );
00818         }
00819     }
00820     // connect the PO nodes
00821     Abc_NtkForEachPo( pNtkOld, pObj, i )
00822     {
00823         pFaninNew = Abc_ObjFanin0Ivy( pNtk, Ivy_ManPo(pMan, i) );
00824         Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
00825     }
00826     // connect the latches
00827     Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i )
00828     {
00829         pFaninNew = Abc_ObjFanin0Ivy( pNtk, pNode );
00830         Abc_ObjAddFanin( Abc_ObjFanin0(Abc_NtkBox(pNtk, i)), pFaninNew );
00831     }
00832     Vec_IntFree( vLatches );
00833     Vec_IntFree( vNodes );
00834     if ( !Abc_NtkCheck( pNtk ) )
00835         fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
00836     return pNtk;
00837 }
00838 
00850 Ivy_Man_t * Abc_NtkToIvy( Abc_Ntk_t * pNtkOld )
00851 {
00852     Ivy_Man_t * pMan;
00853     Abc_Obj_t * pObj;
00854     Ivy_Obj_t * pFanin;
00855     int i;
00856     // create the manager
00857     assert( Abc_NtkHasSop(pNtkOld) || Abc_NtkIsStrash(pNtkOld) );
00858     pMan = Ivy_ManStart();
00859     // create the PIs
00860     if ( Abc_NtkIsStrash(pNtkOld) )
00861         Abc_AigConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan);
00862     Abc_NtkForEachCi( pNtkOld, pObj, i )
00863         pObj->pCopy = (Abc_Obj_t *)Ivy_ObjCreatePi(pMan);
00864     // perform the conversion of the internal nodes
00865     Abc_NtkStrashPerformAig( pNtkOld, pMan );
00866     // create the POs
00867     Abc_NtkForEachCo( pNtkOld, pObj, i )
00868     {
00869         pFanin = (Ivy_Obj_t *)Abc_ObjFanin0(pObj)->pCopy;
00870         pFanin = Ivy_NotCond( pFanin, Abc_ObjFaninC0(pObj) );
00871         Ivy_ObjCreatePo( pMan, pFanin );
00872     }
00873     Ivy_ManCleanup( pMan );
00874     return pMan;
00875 }
00876 
00888 void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan )
00889 {
00890 //    ProgressBar * pProgress;
00891     Vec_Ptr_t * vNodes;
00892     Abc_Obj_t * pNode;
00893     int i;
00894     vNodes = Abc_NtkDfs( pNtk, 0 );
00895 //    pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
00896     Vec_PtrForEachEntry( vNodes, pNode, i )
00897     {
00898 //        Extra_ProgressBarUpdate( pProgress, i, NULL );
00899         pNode->pCopy = (Abc_Obj_t *)Abc_NodeStrashAig( pMan, pNode );
00900     }
00901 //    Extra_ProgressBarStop( pProgress );
00902     Vec_PtrFree( vNodes );
00903 }
00904 
00916 Ivy_Obj_t * Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode )
00917 {
00918     int fUseFactor = 1;
00919     char * pSop;
00920     Ivy_Obj_t * pFanin0, * pFanin1;
00921 
00922     assert( Abc_ObjIsNode(pNode) );
00923 
00924     // consider the case when the graph is an AIG
00925     if ( Abc_NtkIsStrash(pNode->pNtk) )
00926     {
00927         if ( Abc_AigNodeIsConst(pNode) )
00928             return Ivy_ManConst1(pMan);
00929         pFanin0 = (Ivy_Obj_t *)Abc_ObjFanin0(pNode)->pCopy;
00930         pFanin0 = Ivy_NotCond( pFanin0, Abc_ObjFaninC0(pNode) );
00931         pFanin1 = (Ivy_Obj_t *)Abc_ObjFanin1(pNode)->pCopy;
00932         pFanin1 = Ivy_NotCond( pFanin1, Abc_ObjFaninC1(pNode) );
00933         return Ivy_And( pMan, pFanin0, pFanin1 );
00934     }
00935 
00936     // get the SOP of the node
00937     if ( Abc_NtkHasMapping(pNode->pNtk) )
00938         pSop = Mio_GateReadSop(pNode->pData);
00939     else
00940         pSop = pNode->pData;
00941 
00942     // consider the constant node
00943     if ( Abc_NodeIsConst(pNode) )
00944         return Ivy_NotCond( Ivy_ManConst1(pMan), Abc_SopIsConst0(pSop) );
00945 
00946     // consider the special case of EXOR function
00947     if ( Abc_SopIsExorType(pSop) )
00948         return Abc_NodeStrashAigExorAig( pMan, pNode, pSop );
00949 
00950     // decide when to use factoring
00951     if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
00952         return Abc_NodeStrashAigFactorAig( pMan, pNode, pSop );
00953     return Abc_NodeStrashAigSopAig( pMan, pNode, pSop );
00954 }
00955 
00967 Ivy_Obj_t * Abc_NodeStrashAigSopAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop )
00968 {
00969     Abc_Obj_t * pFanin;
00970     Ivy_Obj_t * pAnd, * pSum;
00971     char * pCube;
00972     int i, nFanins;
00973 
00974     // get the number of node's fanins
00975     nFanins = Abc_ObjFaninNum( pNode );
00976     assert( nFanins == Abc_SopGetVarNum(pSop) );
00977     // go through the cubes of the node's SOP
00978     pSum = Ivy_Not( Ivy_ManConst1(pMan) );
00979     Abc_SopForEachCube( pSop, nFanins, pCube )
00980     {
00981         // create the AND of literals
00982         pAnd = Ivy_ManConst1(pMan);
00983         Abc_ObjForEachFanin( pNode, pFanin, i ) // pFanin can be a net
00984         {
00985             if ( pCube[i] == '1' )
00986                 pAnd = Ivy_And( pMan, pAnd, (Ivy_Obj_t *)pFanin->pCopy );
00987             else if ( pCube[i] == '0' )
00988                 pAnd = Ivy_And( pMan, pAnd, Ivy_Not((Ivy_Obj_t *)pFanin->pCopy) );
00989         }
00990         // add to the sum of cubes
00991         pSum = Ivy_Or( pMan, pSum, pAnd );
00992     }
00993     // decide whether to complement the result
00994     if ( Abc_SopIsComplement(pSop) )
00995         pSum = Ivy_Not(pSum);
00996     return pSum;
00997 }
00998 
01010 Ivy_Obj_t * Abc_NodeStrashAigExorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop )
01011 {
01012     Abc_Obj_t * pFanin;
01013     Ivy_Obj_t * pSum;
01014     int i, nFanins;
01015     // get the number of node's fanins
01016     nFanins = Abc_ObjFaninNum( pNode );
01017     assert( nFanins == Abc_SopGetVarNum(pSop) );
01018     // go through the cubes of the node's SOP
01019     pSum = Ivy_Not( Ivy_ManConst1(pMan) );
01020     for ( i = 0; i < nFanins; i++ )
01021     {
01022         pFanin = Abc_ObjFanin( pNode, i );
01023         pSum = Ivy_Exor( pMan, pSum, (Ivy_Obj_t *)pFanin->pCopy );
01024     }
01025     if ( Abc_SopIsComplement(pSop) )
01026         pSum = Ivy_Not(pSum);
01027     return pSum;
01028 }
01029 
01041 Ivy_Obj_t * Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pRoot, char * pSop )
01042 {
01043     Dec_Graph_t * pFForm;
01044     Dec_Node_t * pNode;
01045     Ivy_Obj_t * pAnd;
01046     int i;
01047 
01048 //    extern Ivy_Obj_t * Dec_GraphToNetworkAig( Ivy_Man_t * pMan, Dec_Graph_t * pGraph );
01049     extern Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph );
01050 
01051 //    assert( 0 );
01052 
01053     // perform factoring
01054     pFForm = Dec_Factor( pSop );
01055     // collect the fanins
01056     Dec_GraphForEachLeaf( pFForm, pNode, i )
01057         pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy;
01058     // perform strashing
01059 //    pAnd = Dec_GraphToNetworkAig( pMan, pFForm );
01060     pAnd = Dec_GraphToNetworkIvy( pMan, pFForm );
01061 //    pAnd = NULL;
01062 
01063     Dec_GraphFree( pFForm );
01064     return pAnd;
01065 }
01066 
01078 Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs )
01079 {
01080     Abc_Obj_t * pLatch;
01081     Vec_Int_t * vArray;
01082     int i;
01083     vArray = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
01084     Abc_NtkForEachLatch( pNtk, pLatch, i )
01085     {
01086         if ( fUseDcs || Abc_LatchIsInitDc(pLatch) )
01087             Vec_IntPush( vArray, IVY_INIT_DC );
01088         else if ( Abc_LatchIsInit1(pLatch) )
01089             Vec_IntPush( vArray, IVY_INIT_1 );
01090         else if ( Abc_LatchIsInit0(pLatch) )
01091             Vec_IntPush( vArray, IVY_INIT_0 );
01092         else assert( 0 );
01093     }
01094     return vArray;
01095 }
01096 
01100 
01101