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

00001 
00021 #include "aig.h"
00022 
00026 
00030 
00043 Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
00044 {
00045     Aig_Man_t * pNew;
00046     Aig_Obj_t * pObj, * pObjMapped;
00047     int i;
00048     // create the new manager
00049     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
00050     pNew->pName = Aig_UtilStrsav( p->pName );
00051     pNew->nRegs = p->nRegs;
00052     pNew->nAsserts = p->nAsserts;
00053     if ( p->vFlopNums )
00054         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
00055     // create the PIs
00056     Aig_ManCleanData( p );
00057     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
00058     Aig_ManForEachPi( p, pObj, i )
00059         pObj->pData = Aig_ObjCreatePi(pNew);
00060     // implement the mapping
00061     Aig_ManForEachPi( p, pObj, i )
00062     {
00063         pObjMapped = Vec_PtrEntry( vMap, i );
00064         pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) );
00065     }
00066     // duplicate internal nodes
00067     Aig_ManForEachObj( p, pObj, i )
00068         if ( Aig_ObjIsBuf(pObj) )
00069             pObj->pData = Aig_ObjChild0Copy(pObj);
00070         else if ( Aig_ObjIsNode(pObj) )
00071             pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
00072     // add the POs
00073     Aig_ManForEachPo( p, pObj, i )
00074         Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
00075     assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) );
00076     // check the resulting network
00077     if ( !Aig_ManCheck(pNew) )
00078         printf( "Aig_ManDup(): The check has failed.\n" );
00079     return pNew;
00080 }
00081 
00093 void Aig_ManSeqCleanup_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
00094 {
00095     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
00096         return;
00097     Aig_ObjSetTravIdCurrent(p, pObj);
00098     // collect latch input corresponding to unmarked PI (latch output)
00099     if ( Aig_ObjIsPi(pObj) )
00100     {
00101         Vec_PtrPush( vNodes, pObj->pNext );
00102         return;
00103     }
00104     if ( Aig_ObjIsPo(pObj) )
00105     {
00106         Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
00107         return;
00108     }
00109     assert( Aig_ObjIsNode(pObj) );
00110     Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
00111     Aig_ManSeqCleanup_rec( p, Aig_ObjFanin1(pObj), vNodes );
00112 }
00113 
00125 int Aig_ManSeqCleanup( Aig_Man_t * p )
00126 {
00127     Vec_Ptr_t * vNodes, * vCis, * vCos;
00128     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
00129     int i, nTruePis, nTruePos;
00130     assert( Aig_ManBufNum(p) == 0 );
00131 
00132     // mark the PIs
00133     Aig_ManIncrementTravId( p );
00134     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
00135     Aig_ManForEachPiSeq( p, pObj, i )
00136         Aig_ObjSetTravIdCurrent( p, pObj );
00137 
00138     // prepare to collect nodes reachable from POs
00139     vNodes = Vec_PtrAlloc( 100 );
00140     Aig_ManForEachPoSeq( p, pObj, i )
00141         Vec_PtrPush( vNodes, pObj );
00142 
00143     // remember latch inputs in latch outputs
00144     Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
00145         pObjLo->pNext = pObjLi;
00146     // mark the nodes reachable from these nodes
00147     Vec_PtrForEachEntry( vNodes, pObj, i )
00148         Aig_ManSeqCleanup_rec( p, pObj, vNodes );
00149     assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) );
00150     // clean latch output pointers
00151     Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
00152         pObjLo->pNext = NULL;
00153 
00154     // if some latches are removed, update PIs/POs
00155     if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) )
00156     {
00157         if ( p->vFlopNums )
00158         {
00159             int nTruePos = Aig_ManPoNum(p)-Aig_ManRegNum(p);
00160             // remember numbers of flops in the flops
00161             Aig_ManForEachLiSeq( p, pObj, i )
00162                 pObj->pNext = (Aig_Obj_t *)(long)Vec_IntEntry( p->vFlopNums, i - nTruePos );
00163             // reset the flop numbers
00164             Vec_PtrForEachEntryStart( vNodes, pObj, i, nTruePos )
00165                 Vec_IntWriteEntry( p->vFlopNums, i - nTruePos, (int)(long)pObj->pNext );
00166             Vec_IntShrink( p->vFlopNums, Vec_PtrSize(vNodes) - nTruePos );
00167             // clean the next pointer
00168             Aig_ManForEachLiSeq( p, pObj, i )
00169                 pObj->pNext = NULL;
00170         }
00171         // collect new CIs/COs
00172         vCis = Vec_PtrAlloc( Aig_ManPiNum(p) );
00173         Aig_ManForEachPi( p, pObj, i )
00174             if ( Aig_ObjIsTravIdCurrent(p, pObj) )
00175                 Vec_PtrPush( vCis, pObj );
00176             else
00177             {
00178                 Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
00179 //                Aig_ManRecycleMemory( p, pObj );
00180             }
00181         vCos = Vec_PtrAlloc( Aig_ManPoNum(p) );
00182         Aig_ManForEachPo( p, pObj, i )
00183             if ( Aig_ObjIsTravIdCurrent(p, pObj) )
00184                 Vec_PtrPush( vCos, pObj );
00185             else
00186             {
00187                 Aig_ObjDisconnect( p, pObj );
00188                 Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
00189 //                Aig_ManRecycleMemory( p, pObj );
00190             }
00191         // remember the number of true PIs/POs
00192         nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
00193         nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
00194         // set the new number of registers
00195         p->nRegs -= Aig_ManPoNum(p) - Vec_PtrSize(vNodes);
00196         // create new PIs/POs
00197         assert( Vec_PtrSize(vCis) == nTruePis + p->nRegs );
00198         assert( Vec_PtrSize(vCos) == nTruePos + p->nRegs );
00199         Vec_PtrFree( p->vPis );    p->vPis = vCis;
00200         Vec_PtrFree( p->vPos );    p->vPos = vCos;
00201         p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
00202         p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
00203                 
00204     }
00205     Vec_PtrFree( vNodes );
00206     // remove dangling nodes
00207     return Aig_ManCleanup( p );
00208 }
00209 
00221 int Aig_ManCountMergeRegs( Aig_Man_t * p )
00222 {
00223     Aig_Obj_t * pObj, * pFanin;
00224     int i, Counter = 0, Const0 = 0, Const1 = 0;
00225     Aig_ManIncrementTravId( p );
00226     Aig_ManForEachLiSeq( p, pObj, i )
00227     {
00228         pFanin = Aig_ObjFanin0(pObj);
00229         if ( Aig_ObjIsConst1(pFanin) )
00230         {
00231             if ( Aig_ObjFaninC0(pObj) )
00232                 Const0++;
00233             else
00234                 Const1++;
00235         }
00236         if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
00237             continue;
00238         Aig_ObjSetTravIdCurrent(p, pFanin);
00239         Counter++;
00240     }
00241     printf( "Regs = %d. Fanins = %d. Const0 = %d. Const1 = %d.\n", 
00242         Aig_ManRegNum(p), Counter, Const0, Const1 );
00243     return 0;
00244 }
00245 
00246 
00258 int Aig_ManReduceLachesCount( Aig_Man_t * p )
00259 {
00260     Aig_Obj_t * pObj, * pFanin;
00261     int i, Counter = 0, Diffs = 0;
00262     assert( Aig_ManRegNum(p) > 0 );
00263     Aig_ManForEachObj( p, pObj, i )
00264         assert( !pObj->fMarkA && !pObj->fMarkB );
00265     Aig_ManForEachLiSeq( p, pObj, i )
00266     {
00267         pFanin = Aig_ObjFanin0(pObj);
00268         if ( Aig_ObjFaninC0(pObj) )
00269         {
00270             if ( pFanin->fMarkB )
00271                 Counter++;
00272             else
00273                 pFanin->fMarkB = 1;
00274         }
00275         else
00276         {
00277             if ( pFanin->fMarkA )
00278                 Counter++;
00279             else
00280                 pFanin->fMarkA = 1;
00281         }
00282     }
00283     // count fanins that have both attributes
00284     Aig_ManForEachLiSeq( p, pObj, i )
00285     {
00286         pFanin = Aig_ObjFanin0(pObj);
00287         Diffs += pFanin->fMarkA && pFanin->fMarkB;
00288         pFanin->fMarkA = pFanin->fMarkB = 0;
00289     }
00290 //    printf( "Diffs = %d.\n", Diffs );
00291     return Counter;
00292 }
00293 
00305 Vec_Ptr_t * Aig_ManReduceLachesOnce( Aig_Man_t * p )
00306 {
00307     Vec_Ptr_t * vMap;
00308     Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pFanin;
00309     int * pMapping, i;
00310     // start mapping by adding the true PIs
00311     vMap = Vec_PtrAlloc( Aig_ManPiNum(p) );
00312     Aig_ManForEachPiSeq( p, pObj, i )
00313         Vec_PtrPush( vMap, pObj );
00314     // create mapping of fanin nodes into the corresponding latch outputs
00315     pMapping = ALLOC( int, 2 * Aig_ManObjNumMax(p) );
00316     Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
00317     {
00318         pFanin = Aig_ObjFanin0(pObjLi);
00319         if ( Aig_ObjFaninC0(pObjLi) )
00320         {
00321             if ( pFanin->fMarkB )
00322             {
00323                 Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id + 1]) );
00324             }
00325             else
00326             {
00327                 pFanin->fMarkB = 1;
00328                 pMapping[2*pFanin->Id + 1] = i;
00329                 Vec_PtrPush( vMap, pObjLo );
00330             }
00331         }
00332         else
00333         {
00334             if ( pFanin->fMarkA )
00335             {
00336                 Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id]) );
00337             }
00338             else
00339             {
00340                 pFanin->fMarkA = 1;
00341                 pMapping[2*pFanin->Id] = i;
00342                 Vec_PtrPush( vMap, pObjLo );
00343             }
00344         }
00345     }
00346     free( pMapping );
00347     Aig_ManForEachLiSeq( p, pObj, i )
00348     {
00349         pFanin = Aig_ObjFanin0(pObj);
00350         pFanin->fMarkA = pFanin->fMarkB = 0;
00351     }
00352     return vMap;
00353 }
00354 
00366 Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
00367 {
00368     Aig_Man_t * pTemp;
00369     Vec_Ptr_t * vMap;
00370     int nSaved, nCur;
00371     for ( nSaved = 0; (nCur = Aig_ManReduceLachesCount(p)); nSaved += nCur )
00372     {
00373         if ( fVerbose )
00374         {
00375         printf( "Saved = %5d.   ", nCur );
00376         printf( "RBeg = %5d. NBeg = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
00377         }
00378         vMap = Aig_ManReduceLachesOnce( p );
00379         p = Aig_ManRemap( pTemp = p, vMap );
00380         Aig_ManStop( pTemp );
00381         Vec_PtrFree( vMap );
00382         Aig_ManSeqCleanup( p );
00383         if ( fVerbose )
00384         {
00385         printf( "REnd = %5d. NEnd = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
00386         printf( "\n" );
00387         }
00388         if ( p->nRegs == 0 )
00389             break;
00390     }
00391     return p;
00392 }
00393 
00394 
00398 
00399