src/aig/ivy/ivyDfs.c File Reference

#include "ivy.h"
Include dependency graph for ivyDfs.c:

Go to the source code of this file.

Functions

void Ivy_ManDfs_rec (Ivy_Man_t *p, Ivy_Obj_t *pObj, Vec_Int_t *vNodes)
Vec_Int_t * Ivy_ManDfs (Ivy_Man_t *p)
Vec_Int_t * Ivy_ManDfsSeq (Ivy_Man_t *p, Vec_Int_t **pvLatches)
void Ivy_ManCollectCone_rec (Ivy_Obj_t *pObj, Vec_Ptr_t *vCone)
void Ivy_ManCollectCone (Ivy_Obj_t *pObj, Vec_Ptr_t *vFront, Vec_Ptr_t *vCone)
Vec_Vec_t * Ivy_ManLevelize (Ivy_Man_t *p)
Vec_Int_t * Ivy_ManRequiredLevels (Ivy_Man_t *p)
int Ivy_ManIsAcyclic_rec (Ivy_Man_t *p, Ivy_Obj_t *pObj)
int Ivy_ManIsAcyclic (Ivy_Man_t *p)
int Ivy_ManSetLevels_rec (Ivy_Obj_t *pObj, int fHaig)
int Ivy_ManSetLevels (Ivy_Man_t *p, int fHaig)

Function Documentation

void Ivy_ManCollectCone ( Ivy_Obj_t *  pObj,
Vec_Ptr_t *  vFront,
Vec_Ptr_t *  vCone 
)

Function*************************************************************

Synopsis [Collects nodes in the cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 192 of file ivyDfs.c.

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 }

void Ivy_ManCollectCone_rec ( Ivy_Obj_t *  pObj,
Vec_Ptr_t *  vCone 
)

Function*************************************************************

Synopsis [Collects nodes in the cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 165 of file ivyDfs.c.

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 }

Vec_Int_t* Ivy_ManDfs ( Ivy_Man_t *  p  ) 

Function*************************************************************

Synopsis [Collects AND/EXOR nodes in the DFS order from CIs to COs.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file ivyDfs.c.

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 }

void Ivy_ManDfs_rec ( Ivy_Man_t *  p,
Ivy_Obj_t *  pObj,
Vec_Int_t *  vNodes 
)

CFile****************************************************************

FileName [ivyDfs.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [DFS collection procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id
ivyDfs.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Collects nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file ivyDfs.c.

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 }

Vec_Int_t* Ivy_ManDfsSeq ( Ivy_Man_t *  p,
Vec_Int_t **  pvLatches 
)

Function*************************************************************

Synopsis [Collects AND/EXOR nodes in the DFS order from CIs to COs.]

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file ivyDfs.c.

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 }

int Ivy_ManIsAcyclic ( Ivy_Man_t *  p  ) 

Function*************************************************************

Synopsis [Detects combinational loops.]

Description [This procedure is based on the idea suggested by Donald Chai. As we traverse the network and visit the nodes, we need to distinquish three types of nodes: (1) those that are visited for the first time, (2) those that have been visited in this traversal but are currently not on the traversal path, (3) those that have been visited and are currently on the travesal path. When the node of type (3) is encountered, it means that there is a combinational loop. To mark the three types of nodes, two new values of the traversal IDs are used.]

SideEffects []

SeeAlso []

Definition at line 370 of file ivyDfs.c.

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 }

int Ivy_ManIsAcyclic_rec ( Ivy_Man_t *  p,
Ivy_Obj_t *  pObj 
)

Function*************************************************************

Synopsis [Recursively detects combinational loops.]

Description []

SideEffects []

SeeAlso []

Definition at line 291 of file ivyDfs.c.

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 }

Vec_Vec_t* Ivy_ManLevelize ( Ivy_Man_t *  p  ) 

Function*************************************************************

Synopsis [Returns the nodes by level.]

Description []

SideEffects []

SeeAlso []

Definition at line 221 of file ivyDfs.c.

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 }

Vec_Int_t* Ivy_ManRequiredLevels ( Ivy_Man_t *  p  ) 

Function*************************************************************

Synopsis [Computes required levels for each node.]

Description [Assumes topological ordering of the nodes.]

SideEffects []

SeeAlso []

Definition at line 247 of file ivyDfs.c.

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 }

int Ivy_ManSetLevels ( Ivy_Man_t *  p,
int  fHaig 
)

Function*************************************************************

Synopsis [Sets the levels of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 454 of file ivyDfs.c.

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 }

int Ivy_ManSetLevels_rec ( Ivy_Obj_t *  pObj,
int  fHaig 
)

Function*************************************************************

Synopsis [Sets the levels of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 405 of file ivyDfs.c.

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 }

Generated on Tue Jan 5 12:18:23 2010 for abc70930 by  doxygen 1.6.1