abc70930: src/aig/ivy/ivyDfs.c Source File

00001 
00021 #include "ivy.h"
00022 
00026 
00030 
00042 void Ivy_ManDfs_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
00043 {
00044     if ( Ivy_ObjIsMarkA(pObj) )
00045         return;
00046     Ivy_ObjSetMarkA(pObj);
00047     if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
00048     {
00049         if ( p->pHaig == NULL && pObj->pEquiv )
00050             Ivy_ManDfs_rec( p, Ivy_Regular(pObj->pEquiv), vNodes );
00051         return;
00052     }
00053 //printf( "visiting node %d\n", pObj->Id );
00054 /*
00055     if ( pObj->Id == 87 || pObj->Id == 90 )
00056     {
00057         int y = 0;
00058     }
00059 */
00060     assert( Ivy_ObjIsBuf(pObj) || Ivy_ObjIsAnd(pObj) || Ivy_ObjIsExor(pObj) );
00061     Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
00062     if ( !Ivy_ObjIsBuf(pObj) )
00063         Ivy_ManDfs_rec( p, Ivy_ObjFanin1(pObj), vNodes );
00064     if ( p->pHaig == NULL && pObj->pEquiv )
00065         Ivy_ManDfs_rec( p, Ivy_Regular(pObj->pEquiv), vNodes );
00066     Vec_IntPush( vNodes, pObj->Id );
00067 
00068 //printf( "adding node %d with fanins %d and %d and equiv %d (refs = %d)\n", 
00069 //       pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id, 
00070 //       pObj->pEquiv? Ivy_Regular(pObj->pEquiv)->Id: -1, Ivy_ObjRefs(pObj) );
00071 }
00072 
00084 Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p )
00085 {
00086     Vec_Int_t * vNodes;
00087     Ivy_Obj_t * pObj;
00088     int i;
00089     assert( Ivy_ManLatchNum(p) == 0 );
00090     // make sure the nodes are not marked
00091     Ivy_ManForEachObj( p, pObj, i )
00092         assert( !pObj->fMarkA && !pObj->fMarkB );
00093     // collect the nodes
00094     vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
00095     Ivy_ManForEachPo( p, pObj, i )
00096         Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
00097     // unmark the collected nodes
00098 //    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
00099 //        Ivy_ObjClearMarkA(pObj);
00100     Ivy_ManForEachObj( p, pObj, i )
00101         Ivy_ObjClearMarkA(pObj);
00102     // make sure network does not have dangling nodes
00103     assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
00104     return vNodes;
00105 }
00106 
00118 Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches )
00119 {
00120     Vec_Int_t * vNodes, * vLatches;
00121     Ivy_Obj_t * pObj;
00122     int i;
00123 //    assert( Ivy_ManLatchNum(p) > 0 );
00124     // make sure the nodes are not marked
00125     Ivy_ManForEachObj( p, pObj, i )
00126         assert( !pObj->fMarkA && !pObj->fMarkB );
00127     // collect the latches
00128     vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) );
00129     Ivy_ManForEachLatch( p, pObj, i )
00130         Vec_IntPush( vLatches, pObj->Id );
00131     // collect the nodes
00132     vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
00133     Ivy_ManForEachPo( p, pObj, i )
00134         Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
00135     Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
00136         Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
00137     // unmark the collected nodes
00138 //    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
00139 //        Ivy_ObjClearMarkA(pObj);
00140     Ivy_ManForEachObj( p, pObj, i )
00141         Ivy_ObjClearMarkA(pObj);
00142     // make sure network does not have dangling nodes
00143 //    assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
00144 
00145 // temporary!!!
00146 
00147     if ( pvLatches == NULL )
00148         Vec_IntFree( vLatches );
00149     else
00150         *pvLatches = vLatches;
00151     return vNodes;
00152 }
00153 
00165 void Ivy_ManCollectCone_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vCone )
00166 {
00167     if ( pObj->fMarkA )
00168         return;
00169     if ( Ivy_ObjIsBuf(pObj) )
00170     {
00171         Ivy_ManCollectCone_rec( Ivy_ObjFanin0(pObj), vCone );
00172         Vec_PtrPush( vCone, pObj );
00173         return;
00174     }
00175     assert( Ivy_ObjIsNode(pObj) );
00176     Ivy_ManCollectCone_rec( Ivy_ObjFanin0(pObj), vCone );
00177     Ivy_ManCollectCone_rec( Ivy_ObjFanin1(pObj), vCone );
00178     Vec_PtrPushUnique( vCone, pObj );
00179 }
00180 
00192 void Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone )
00193 {
00194     Ivy_Obj_t * pTemp;
00195     int i;
00196     assert( !Ivy_IsComplement(pObj) );
00197     assert( Ivy_ObjIsNode(pObj) );
00198     // mark the nodes
00199     Vec_PtrForEachEntry( vFront, pTemp, i )
00200         Ivy_Regular(pTemp)->fMarkA = 1;
00201     assert( pObj->fMarkA == 0 );
00202     // collect the cone
00203     Vec_PtrClear( vCone );
00204     Ivy_ManCollectCone_rec( pObj, vCone );
00205     // unmark the nodes
00206     Vec_PtrForEachEntry( vFront, pTemp, i )
00207         Ivy_Regular(pTemp)->fMarkA = 0;
00208 }
00209 
00221 Vec_Vec_t * Ivy_ManLevelize( Ivy_Man_t * p )
00222 {
00223     Vec_Vec_t * vNodes;
00224     Ivy_Obj_t * pObj;
00225     int i;
00226     vNodes = Vec_VecAlloc( 100 );
00227     Ivy_ManForEachObj( p, pObj, i )
00228     {
00229         assert( !Ivy_ObjIsBuf(pObj) );
00230         if ( Ivy_ObjIsNode(pObj) )
00231             Vec_VecPush( vNodes, pObj->Level, pObj );
00232     }
00233     return vNodes;
00234 }
00235 
00247 Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p )
00248 {
00249     Ivy_Obj_t * pObj;
00250     Vec_Int_t * vLevelsR;
00251     Vec_Vec_t * vNodes;
00252     int i, k, Level, LevelMax;
00253     assert( p->vRequired == NULL );
00254     // start the required times
00255     vLevelsR = Vec_IntStart( Ivy_ManObjIdMax(p) + 1 );
00256     // iterate through the nodes in the reverse order
00257     vNodes = Ivy_ManLevelize( p );
00258     Vec_VecForEachEntryReverseReverse( vNodes, pObj, i, k )
00259     {
00260         Level = Vec_IntEntry( vLevelsR, pObj->Id ) + 1 + Ivy_ObjIsExor(pObj);
00261         if ( Vec_IntEntry( vLevelsR, Ivy_ObjFaninId0(pObj) ) < Level )
00262             Vec_IntWriteEntry( vLevelsR, Ivy_ObjFaninId0(pObj), Level );
00263         if ( Vec_IntEntry( vLevelsR, Ivy_ObjFaninId1(pObj) ) < Level )
00264             Vec_IntWriteEntry( vLevelsR, Ivy_ObjFaninId1(pObj), Level );
00265     }
00266     Vec_VecFree( vNodes );
00267     // convert it into the required times
00268     LevelMax = Ivy_ManLevels( p );
00269 //printf( "max %5d\n",LevelMax );
00270     Ivy_ManForEachObj( p, pObj, i )
00271     {
00272         Level = Vec_IntEntry( vLevelsR, pObj->Id );
00273         Vec_IntWriteEntry( vLevelsR, pObj->Id, LevelMax - Level );
00274 //printf( "%5d : %5d %5d\n", pObj->Id, Level, LevelMax - Level );
00275     }
00276     p->vRequired = vLevelsR;
00277     return vLevelsR;
00278 }
00279 
00291 int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj )
00292 {
00293     // skip the node if it is already visited
00294     if ( Ivy_ObjIsTravIdPrevious(p, pObj) )
00295         return 1;
00296     // check if the node is part of the combinational loop
00297     if ( Ivy_ObjIsTravIdCurrent(p, pObj) )
00298     {
00299         fprintf( stdout, "Manager contains combinational loop!\n" );
00300         fprintf( stdout, "Node \"%d\" is encountered twice on the following path:\n",  Ivy_ObjId(pObj) );
00301         fprintf( stdout, " %d",  Ivy_ObjId(pObj) );
00302         return 0;
00303     }
00304     // mark this node as a node on the current path
00305     Ivy_ObjSetTravIdCurrent( p, pObj );
00306     // explore equivalent nodes if pObj is the main node
00307     if ( p->pHaig == NULL && pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
00308     {
00309         Ivy_Obj_t * pTemp;
00310         assert( !Ivy_IsComplement(pObj->pEquiv) );
00311         for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
00312         {
00313             // traverse the fanin's cone searching for the loop
00314             if ( !Ivy_ManIsAcyclic_rec(p, pTemp) )
00315             {
00316                 // return as soon as the loop is detected
00317                 fprintf( stdout, " -> (%d", Ivy_ObjId(pObj) );
00318                 for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
00319                     fprintf( stdout, " %d", Ivy_ObjId(pTemp) );
00320                 fprintf( stdout, ")" );
00321                 return 0; 
00322             }
00323         }
00324     }
00325     // quite if it is a CI node
00326     if ( Ivy_ObjIsCi(pObj) || Ivy_ObjIsConst1(pObj) )
00327     {
00328         // mark this node as a visited node
00329         Ivy_ObjSetTravIdPrevious( p, pObj );
00330         return 1;
00331     }
00332     assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
00333     // traverse the fanin's cone searching for the loop
00334     if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pObj)) )
00335     {
00336         // return as soon as the loop is detected
00337         fprintf( stdout, " -> %d", Ivy_ObjId(pObj) );
00338         return 0;
00339     }
00340     // traverse the fanin's cone searching for the loop
00341     if ( Ivy_ObjIsNode(pObj) && !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin1(pObj)) )
00342     {
00343         // return as soon as the loop is detected
00344         fprintf( stdout, " -> %d", Ivy_ObjId(pObj) );
00345         return 0;
00346     }
00347     // mark this node as a visited node
00348     Ivy_ObjSetTravIdPrevious( p, pObj );
00349     return 1;
00350 }
00351 
00370 int Ivy_ManIsAcyclic( Ivy_Man_t * p )
00371 {
00372     Ivy_Obj_t * pObj;
00373     int fAcyclic, i;
00374     // set the traversal ID for this DFS ordering
00375     Ivy_ManIncrementTravId( p );   
00376     Ivy_ManIncrementTravId( p );   
00377     // pObj->TravId == pNet->nTravIds      means "pObj is on the path"
00378     // pObj->TravId == pNet->nTravIds - 1  means "pObj is visited but is not on the path"
00379     // pObj->TravId <  pNet->nTravIds - 1  means "pObj is not visited"
00380     // traverse the network to detect cycles
00381     fAcyclic = 1;
00382     Ivy_ManForEachCo( p, pObj, i )
00383     {
00384         // traverse the output logic cone
00385         if ( fAcyclic = Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pObj)) )
00386             continue;
00387         // stop as soon as the first loop is detected
00388         fprintf( stdout, " (cone of %s \"%d\")\n", Ivy_ObjIsLatch(pObj)? "latch" : "PO", Ivy_ObjId(pObj) );
00389         break;
00390     }
00391     return fAcyclic;
00392 }
00393 
00405 int Ivy_ManSetLevels_rec( Ivy_Obj_t * pObj, int fHaig )
00406 {
00407     // quit if the node is visited
00408     if ( Ivy_ObjIsMarkA(pObj) )
00409         return pObj->Level;
00410     Ivy_ObjSetMarkA(pObj);
00411     // quit if this is a CI
00412     if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
00413         return 0;
00414     assert( Ivy_ObjIsBuf(pObj) || Ivy_ObjIsAnd(pObj) || Ivy_ObjIsExor(pObj) );
00415     // get levels of the fanins
00416     Ivy_ManSetLevels_rec( Ivy_ObjFanin0(pObj), fHaig );
00417     if ( !Ivy_ObjIsBuf(pObj) )
00418         Ivy_ManSetLevels_rec( Ivy_ObjFanin1(pObj), fHaig );
00419     // get level of the node
00420     if ( Ivy_ObjIsBuf(pObj) )
00421         pObj->Level = 1 + Ivy_ObjFanin0(pObj)->Level;
00422     else if ( Ivy_ObjIsNode(pObj) )
00423         pObj->Level = Ivy_ObjLevelNew( pObj );
00424     else assert( 0 );
00425     // get level of other choices
00426     if ( fHaig && pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
00427     {
00428         Ivy_Obj_t * pTemp;
00429         unsigned LevelMax = pObj->Level;
00430         for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
00431         {
00432             Ivy_ManSetLevels_rec( pTemp, fHaig );
00433             LevelMax = IVY_MAX( LevelMax, pTemp->Level );
00434         }
00435         // get this level
00436         pObj->Level = LevelMax;
00437         for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
00438             pTemp->Level = LevelMax;
00439     }
00440     return pObj->Level;
00441 }
00442 
00454 int Ivy_ManSetLevels( Ivy_Man_t * p, int fHaig )
00455 {
00456     Ivy_Obj_t * pObj;
00457     int i, LevelMax;
00458     // check if CIs have choices
00459     if ( fHaig )
00460     {
00461         Ivy_ManForEachCi( p, pObj, i )
00462             if ( pObj->pEquiv )
00463                 printf( "CI %d has a choice, which will not be visualized.\n", pObj->Id );
00464     }
00465     // clean the levels
00466     Ivy_ManForEachObj( p, pObj, i )
00467         pObj->Level = 0;
00468     // compute the levels
00469     LevelMax = 0;
00470     Ivy_ManForEachCo( p, pObj, i )
00471     {
00472         Ivy_ManSetLevels_rec( Ivy_ObjFanin0(pObj), fHaig );
00473         LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level );
00474     }
00475     // compute levels of nodes without fanout
00476     Ivy_ManForEachObj( p, pObj, i )
00477         if ( (Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj)) && Ivy_ObjRefs(pObj) == 0 )
00478         {
00479             Ivy_ManSetLevels_rec( pObj, fHaig );
00480             LevelMax = IVY_MAX( LevelMax, (int)pObj->Level );
00481         }
00482     // clean the marks
00483     Ivy_ManForEachObj( p, pObj, i )
00484         Ivy_ObjClearMarkA(pObj);
00485     return LevelMax;
00486 }
00487 
00488 
00492 
00493