abc70930: src/aig/aig/aigSeq.c Source File

00001 
00021 #include "aig.h"
00022 
00026 
00030 
00042 void Aig_ManSeqStrashConvert( Aig_Man_t * p, int nLatches, int * pInits )
00043 {
00044     Aig_Obj_t * pObjLi, * pObjLo, * pLatch;
00045     int i;
00046     assert( Vec_PtrSize( p->vBufs ) == 0 );
00047     // collect the POs to be converted into latches
00048     for ( i = 0; i < nLatches; i++ )
00049     {
00050         // get the corresponding PI/PO pair
00051         pObjLi = Aig_ManPo( p, Aig_ManPoNum(p) - nLatches + i );
00052         pObjLo = Aig_ManPi( p, Aig_ManPiNum(p) - nLatches + i );
00053         // create latch
00054         pLatch = Aig_Latch( p, Aig_ObjChild0(pObjLi), pInits? pInits[i] : 0 );
00055         // recycle the old PO object
00056         Aig_ObjDisconnect( p, pObjLi );
00057         Vec_PtrWriteEntry( p->vObjs, pObjLi->Id, NULL );
00058         Aig_ManRecycleMemory( p, pObjLi );
00059         // convert the corresponding PI to be a buffer and connect it to the latch
00060         pObjLo->Type = AIG_OBJ_BUF;
00061         Aig_ObjConnect( p, pObjLo, pLatch, NULL );
00062         // save the buffer
00063 //        Vec_PtrPush( p->vBufs, pObjLo );
00064     }
00065     // shrink the arrays
00066     Vec_PtrShrink( p->vPis, Aig_ManPiNum(p) - nLatches );
00067     Vec_PtrShrink( p->vPos, Aig_ManPoNum(p) - nLatches );
00068     // update the counters of different objects
00069     p->nObjs[AIG_OBJ_PI]  -= nLatches;
00070     p->nObjs[AIG_OBJ_PO]  -= nLatches;
00071     p->nObjs[AIG_OBJ_BUF] += nLatches;
00072 }
00073 
00085 void Aig_ManDfsSeq_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
00086 {
00087     assert( !Aig_IsComplement(pObj) );
00088     if ( pObj == NULL )
00089         return;
00090     if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
00091         return;
00092     Aig_ObjSetTravIdCurrent( p, pObj );
00093     if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
00094         return;
00095     Aig_ManDfsSeq_rec( p, Aig_ObjFanin0(pObj), vNodes );
00096     Aig_ManDfsSeq_rec( p, Aig_ObjFanin1(pObj), vNodes );
00097 //    if ( (Aig_ObjFanin0(pObj) == NULL || Aig_ObjIsBuf(Aig_ObjFanin0(pObj))) &&
00098 //         (Aig_ObjFanin1(pObj) == NULL || Aig_ObjIsBuf(Aig_ObjFanin1(pObj))) )
00099         Vec_PtrPush( vNodes, pObj );
00100 }
00101 
00113 Vec_Ptr_t * Aig_ManDfsSeq( Aig_Man_t * p )
00114 {
00115     Vec_Ptr_t * vNodes;
00116     Aig_Obj_t * pObj;
00117     int i;
00118     Aig_ManIncrementTravId( p );
00119     vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
00120     Aig_ManForEachPo( p, pObj, i )
00121         Aig_ManDfsSeq_rec( p, Aig_ObjFanin0(pObj), vNodes );
00122     return vNodes;
00123 }
00124 
00136 void Aig_ManDfsUnreach_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
00137 {
00138     assert( !Aig_IsComplement(pObj) );
00139     if ( pObj == NULL )
00140         return;
00141     if ( Aig_ObjIsTravIdPrevious(p, pObj) || Aig_ObjIsTravIdCurrent(p, pObj) )
00142         return;
00143     Aig_ObjSetTravIdPrevious( p, pObj ); // assume unknown
00144     Aig_ManDfsUnreach_rec( p, Aig_ObjFanin0(pObj), vNodes );
00145     Aig_ManDfsUnreach_rec( p, Aig_ObjFanin1(pObj), vNodes );
00146     if ( Aig_ObjIsTravIdPrevious(p, Aig_ObjFanin0(pObj)) && 
00147         (Aig_ObjFanin1(pObj) == NULL || Aig_ObjIsTravIdPrevious(p, Aig_ObjFanin1(pObj))) )
00148         Vec_PtrPush( vNodes, pObj );
00149     else
00150         Aig_ObjSetTravIdCurrent( p, pObj );
00151 }
00152 
00164 Vec_Ptr_t * Aig_ManDfsUnreach( Aig_Man_t * p )
00165 {
00166     Vec_Ptr_t * vNodes;
00167     Aig_Obj_t * pObj, * pFanin;
00168     int i, k;//, RetValue;
00169     // collect unreachable nodes
00170     Aig_ManIncrementTravId( p ); 
00171     Aig_ManIncrementTravId( p ); 
00172     // mark the constant and PIs
00173     Aig_ObjSetTravIdPrevious( p, Aig_ManConst1(p) );
00174     Aig_ManForEachPi( p, pObj, i )
00175         Aig_ObjSetTravIdCurrent( p, pObj );
00176     // curr marks visited nodes reachable from PIs
00177     // prev marks visited nodes unreachable or unknown
00178 
00179     // collect the unreachable nodes
00180     vNodes = Vec_PtrAlloc( 32 );
00181     Aig_ManForEachPo( p, pObj, i )
00182         Aig_ManDfsUnreach_rec( p, Aig_ObjFanin0(pObj), vNodes );
00183 
00184     // refine resulting nodes
00185     do 
00186     {
00187         k = 0;
00188         Vec_PtrForEachEntry( vNodes, pObj, i )
00189         {
00190             assert( Aig_ObjIsTravIdPrevious(p, pObj) );
00191             if ( Aig_ObjIsLatch(pObj) || Aig_ObjIsBuf(pObj) )
00192             {
00193                 pFanin = Aig_ObjFanin0(pObj);
00194                 assert( Aig_ObjIsTravIdPrevious(p, pFanin) || Aig_ObjIsTravIdCurrent(p, pFanin) );
00195                 if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
00196                 {
00197                     Aig_ObjSetTravIdCurrent( p, pObj );
00198                     continue;
00199                 }
00200             }
00201             else // AND gate
00202             {
00203                 assert( Aig_ObjIsNode(pObj) );
00204                 pFanin = Aig_ObjFanin0(pObj);
00205                 assert( Aig_ObjIsTravIdPrevious(p, pFanin) || Aig_ObjIsTravIdCurrent(p, pFanin) );
00206                 if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
00207                 {
00208                     Aig_ObjSetTravIdCurrent( p, pObj );
00209                     continue;
00210                 }
00211                 pFanin = Aig_ObjFanin1(pObj);
00212                 assert( Aig_ObjIsTravIdPrevious(p, pFanin) || Aig_ObjIsTravIdCurrent(p, pFanin) );
00213                 if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
00214                 {
00215                     Aig_ObjSetTravIdCurrent( p, pObj );
00216                     continue;
00217                 }
00218             }
00219             // write it back
00220             Vec_PtrWriteEntry( vNodes, k++, pObj );
00221         }
00222         Vec_PtrShrink( vNodes, k );
00223     } 
00224     while ( k < i );
00225 
00226 //    if ( Vec_PtrSize(vNodes) > 0 )
00227 //        printf( "Found %d unreachable.\n", Vec_PtrSize(vNodes) ); 
00228     return vNodes;
00229 
00230 /*
00231     // the resulting array contains all unreachable nodes except const 1
00232     if ( Vec_PtrSize(vNodes) == 0 )
00233     {
00234         Vec_PtrFree( vNodes );
00235         return 0;
00236     }
00237     RetValue = Vec_PtrSize(vNodes);
00238 
00239     // mark these nodes
00240     Aig_ManIncrementTravId( p ); 
00241     Vec_PtrForEachEntry( vNodes, pObj, i )
00242         Aig_ObjSetTravIdCurrent( p, pObj );
00243     Vec_PtrFree( vNodes );
00244     return RetValue;
00245 */
00246 }
00247 
00248 
00260 int Aig_ManRemoveUnmarked( Aig_Man_t * p )
00261 {
00262     Vec_Ptr_t * vNodes;
00263     Aig_Obj_t * pObj;
00264     int i, RetValue;
00265     // collect unmarked nodes
00266     vNodes = Vec_PtrAlloc( 100 );
00267     Aig_ManForEachObj( p, pObj, i )
00268     {
00269         if ( Aig_ObjIsTerm(pObj) )
00270             continue;
00271         if ( Aig_ObjIsTravIdCurrent(p, pObj) )
00272             continue;
00273 //Aig_ObjPrintVerbose( pObj, 0 );
00274         Aig_ObjDisconnect( p, pObj );
00275         Vec_PtrPush( vNodes, pObj );
00276     }
00277     if ( Vec_PtrSize(vNodes) == 0 )
00278     {
00279         Vec_PtrFree( vNodes );
00280         return 0;
00281     }
00282     // remove the dangling objects
00283     RetValue = Vec_PtrSize(vNodes);
00284     Vec_PtrForEachEntry( vNodes, pObj, i )
00285         Aig_ObjDelete( p, pObj );
00286 //    printf( "Removed %d dangling.\n", Vec_PtrSize(vNodes) ); 
00287     Vec_PtrFree( vNodes );
00288     return RetValue;
00289 }
00290 
00302 int Aig_ManSeqRehashOne( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach )
00303 {
00304     Aig_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1;
00305     int i, RetValue = 0, Counter = 0;//, Counter2 = 0;
00306 
00307     // mark the unreachable nodes
00308     Aig_ManIncrementTravId( p );
00309     Vec_PtrForEachEntry( vUnreach, pObj, i )
00310         Aig_ObjSetTravIdCurrent(p, pObj);
00311 /*
00312     // count the number of unreachable object connections
00313     // that is the number of unreachable objects connected to main objects
00314     Aig_ManForEachObj( p, pObj, i )
00315     {
00316         if ( Aig_ObjIsTravIdCurrent(p, pObj) )
00317             continue;
00318 
00319         pFanin0 = Aig_ObjFanin0(pObj);
00320         if ( pFanin0 == NULL )
00321             continue;
00322         if ( Aig_ObjIsTravIdCurrent(p, pFanin0) )
00323             pFanin0->fMarkA = 1;
00324 
00325         pFanin1 = Aig_ObjFanin1(pObj);
00326         if ( pFanin1 == NULL )
00327             continue;
00328         if ( Aig_ObjIsTravIdCurrent(p, pFanin1) )
00329             pFanin1->fMarkA = 1;
00330     }
00331 
00332     // count the objects
00333     Aig_ManForEachObj( p, pObj, i )
00334         Counter2 += pObj->fMarkA, pObj->fMarkA = 0;
00335     printf( "Connections = %d.\n", Counter2 );
00336 */
00337 
00338     // go through the nodes while skipping unreachable
00339     Vec_PtrForEachEntry( vNodes, pObj, i )
00340     {
00341         // skip nodes unreachable from the PIs
00342         if ( Aig_ObjIsTravIdCurrent(p, pObj) )
00343             continue;
00344         // process the node
00345         if ( Aig_ObjIsPo(pObj) )
00346         {
00347             if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) )
00348                 continue;
00349             pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
00350             Aig_ObjPatchFanin0( p, pObj, pFanin0 );
00351             continue;
00352         }
00353         if ( Aig_ObjIsLatch(pObj) )
00354         {
00355             if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) )
00356                 continue;
00357             pObjNew = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
00358             pObjNew = Aig_Latch( p, pObjNew, 0 );
00359             Aig_ObjReplace( p, pObj, pObjNew, 1, 0 );
00360             RetValue = 1;
00361             Counter++;
00362             continue;
00363         }
00364         if ( Aig_ObjIsNode(pObj) )
00365         {
00366             if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) && !Aig_ObjIsBuf(Aig_ObjFanin1(pObj)) )
00367                 continue;
00368             pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
00369             pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
00370             pObjNew = Aig_And( p, pFanin0, pFanin1 );
00371             Aig_ObjReplace( p, pObj, pObjNew, 1, 0 );
00372             RetValue = 1;
00373             Counter++;
00374             continue;
00375         }
00376     }
00377 //    printf( "Rehashings = %d.\n", Counter++ );
00378     return RetValue;
00379 }
00380 
00392 void Aig_ManRemoveBuffers( Aig_Man_t * p )
00393 {
00394     Aig_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1;
00395     int i;
00396     if ( Aig_ManBufNum(p) == 0 )
00397         return;
00398     Aig_ManForEachObj( p, pObj, i )
00399     {
00400         if ( Aig_ObjIsPo(pObj) )
00401         {
00402             if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) )
00403                 continue;
00404             pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
00405             Aig_ObjPatchFanin0( p, pObj, pFanin0 );
00406         }
00407         else if ( Aig_ObjIsLatch(pObj) )
00408         {
00409             if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) )
00410                 continue;
00411             pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
00412             pObjNew = Aig_Latch( p, pFanin0, 0 );
00413             Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
00414         }
00415         else if ( Aig_ObjIsAnd(pObj) )
00416         {
00417             if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) && !Aig_ObjIsBuf(Aig_ObjFanin1(pObj)) )
00418                 continue;
00419             pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
00420             pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
00421             pObjNew = Aig_And( p, pFanin0, pFanin1 );
00422             Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
00423         }
00424     }
00425     assert( Aig_ManBufNum(p) == 0 );
00426 }
00427 
00439 int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits )
00440 {
00441     Vec_Ptr_t * vNodes, * vUnreach;
00442 //    Aig_Obj_t * pObj, * pFanin;
00443 //    int i;
00444     int Iter, RetValue = 1;
00445 
00446     // create latches out of the additional PI/PO pairs
00447     Aig_ManSeqStrashConvert( p, nLatches, pInits );
00448 
00449     // iteratively rehash the network
00450     for ( Iter = 0; RetValue; Iter++ )
00451     {
00452 //        Aig_ManPrintStats( p );
00453 /*
00454         Aig_ManForEachObj( p, pObj, i )
00455         {
00456             assert( pObj->Type > 0 );
00457             pFanin = Aig_ObjFanin0(pObj);
00458             assert( pFanin == NULL || pFanin->Type > 0 );
00459             pFanin = Aig_ObjFanin1(pObj);
00460             assert( pFanin == NULL || pFanin->Type > 0 );
00461         }
00462 */
00463         // mark nodes unreachable from the PIs
00464         vUnreach = Aig_ManDfsUnreach( p );
00465         if ( Iter == 0 && Vec_PtrSize(vUnreach) > 0 )
00466             printf( "Unreachable objects = %d.\n", Vec_PtrSize(vUnreach) );
00467         // collect nodes reachable from the POs
00468         vNodes = Aig_ManDfsSeq( p );
00469         // remove nodes unreachable from the POs
00470         if ( Iter == 0 )
00471             Aig_ManRemoveUnmarked( p );
00472         // continue rehashing as long as there are changes
00473         RetValue = Aig_ManSeqRehashOne( p, vNodes, vUnreach );
00474         Vec_PtrFree( vNodes );
00475         Vec_PtrFree( vUnreach );
00476     }
00477 
00478     // perform the final cleanup
00479     Aig_ManIncrementTravId( p );
00480     vNodes = Aig_ManDfsSeq( p );
00481     Aig_ManRemoveUnmarked( p );
00482     Vec_PtrFree( vNodes );
00483     // remove buffers if they are left
00484 //    Aig_ManRemoveBuffers( p );
00485 
00486     // clean up
00487     if ( !Aig_ManCheck( p ) )
00488     {
00489         printf( "Aig_ManSeqStrash: The network check has failed.\n" );
00490         return 0;
00491     }
00492     return 1;
00493 
00494 }
00495 
00496 
00497 
00501 
00502