00001
00021 #include "aig.h"
00022
00026
00027 #define TSI_MAX_ROUNDS 1000
00028
00029 #define AIG_XVS0 1
00030 #define AIG_XVS1 2
00031 #define AIG_XVSX 3
00032
00033 static inline void Aig_ObjSetXsim( Aig_Obj_t * pObj, int Value ) { pObj->nCuts = Value; }
00034 static inline int Aig_ObjGetXsim( Aig_Obj_t * pObj ) { return pObj->nCuts; }
00035 static inline int Aig_XsimInv( int Value )
00036 {
00037 if ( Value == AIG_XVS0 )
00038 return AIG_XVS1;
00039 if ( Value == AIG_XVS1 )
00040 return AIG_XVS0;
00041 assert( Value == AIG_XVSX );
00042 return AIG_XVSX;
00043 }
00044 static inline int Aig_XsimAnd( int Value0, int Value1 )
00045 {
00046 if ( Value0 == AIG_XVS0 || Value1 == AIG_XVS0 )
00047 return AIG_XVS0;
00048 if ( Value0 == AIG_XVSX || Value1 == AIG_XVSX )
00049 return AIG_XVSX;
00050 assert( Value0 == AIG_XVS1 && Value1 == AIG_XVS1 );
00051 return AIG_XVS1;
00052 }
00053 static inline int Aig_XsimRand2()
00054 {
00055 return (rand() & 1) ? AIG_XVS1 : AIG_XVS0;
00056 }
00057 static inline int Aig_XsimRand3()
00058 {
00059 int RetValue;
00060 do {
00061 RetValue = rand() & 3;
00062 } while ( RetValue == 0 );
00063 return RetValue;
00064 }
00065 static inline int Aig_ObjGetXsimFanin0( Aig_Obj_t * pObj )
00066 {
00067 int RetValue;
00068 RetValue = Aig_ObjGetXsim(Aig_ObjFanin0(pObj));
00069 return Aig_ObjFaninC0(pObj)? Aig_XsimInv(RetValue) : RetValue;
00070 }
00071 static inline int Aig_ObjGetXsimFanin1( Aig_Obj_t * pObj )
00072 {
00073 int RetValue;
00074 RetValue = Aig_ObjGetXsim(Aig_ObjFanin1(pObj));
00075 return Aig_ObjFaninC1(pObj)? Aig_XsimInv(RetValue) : RetValue;
00076 }
00077 static inline void Aig_XsimPrint( FILE * pFile, int Value )
00078 {
00079 if ( Value == AIG_XVS0 )
00080 {
00081 fprintf( pFile, "0" );
00082 return;
00083 }
00084 if ( Value == AIG_XVS1 )
00085 {
00086 fprintf( pFile, "1" );
00087 return;
00088 }
00089 assert( Value == AIG_XVSX );
00090 fprintf( pFile, "x" );
00091 }
00092
00093
00094 typedef struct Aig_Tsi_t_ Aig_Tsi_t;
00095 struct Aig_Tsi_t_
00096 {
00097 Aig_Man_t * pAig;
00098
00099 int nWords;
00100 Vec_Ptr_t * vStates;
00101 Aig_MmFixed_t * pMem;
00102
00103 unsigned ** pBins;
00104 int nBins;
00105 };
00106
00107 static inline unsigned * Aig_TsiNext( unsigned * pState, int nWords ) { return *((unsigned **)(pState + nWords)); }
00108 static inline void Aig_TsiSetNext( unsigned * pState, int nWords, unsigned * pNext ) { *((unsigned **)(pState + nWords)) = pNext; }
00109
00113
00125 Aig_Tsi_t * Aig_TsiStart( Aig_Man_t * pAig )
00126 {
00127 Aig_Tsi_t * p;
00128 p = (Aig_Tsi_t *)malloc( sizeof(Aig_Tsi_t) );
00129 memset( p, 0, sizeof(Aig_Tsi_t) );
00130 p->pAig = pAig;
00131 p->nWords = Aig_BitWordNum( 2*Aig_ManRegNum(pAig) );
00132 p->vStates = Vec_PtrAlloc( 1000 );
00133 p->pMem = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 );
00134 p->nBins = Aig_PrimeCudd(TSI_MAX_ROUNDS/2);
00135 p->pBins = ALLOC( unsigned *, p->nBins );
00136 memset( p->pBins, 0, sizeof(unsigned *) * p->nBins );
00137 return p;
00138 }
00139
00151 void Aig_TsiStop( Aig_Tsi_t * p )
00152 {
00153 Aig_MmFixedStop( p->pMem, 0 );
00154 Vec_PtrFree( p->vStates );
00155 free( p->pBins );
00156 free( p );
00157 }
00158
00170 int Aig_TsiStateHash( unsigned * pState, int nWords, int nTableSize )
00171 {
00172 static int s_FPrimes[128] = {
00173 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
00174 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
00175 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
00176 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
00177 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
00178 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
00179 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
00180 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
00181 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
00182 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
00183 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
00184 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
00185 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
00186 };
00187 unsigned uHash;
00188 int i;
00189 uHash = 0;
00190 for ( i = 0; i < nWords; i++ )
00191 uHash ^= pState[i] * s_FPrimes[i & 0x7F];
00192 return uHash % nTableSize;
00193 }
00194
00206 int Aig_TsiStateLookup( Aig_Tsi_t * p, unsigned * pState, int nWords )
00207 {
00208 unsigned * pEntry;
00209 int Hash;
00210 Hash = Aig_TsiStateHash( pState, nWords, p->nBins );
00211 for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Aig_TsiNext(pEntry, nWords) )
00212 if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
00213 return 1;
00214 return 0;
00215 }
00216
00228 void Aig_TsiStateInsert( Aig_Tsi_t * p, unsigned * pState, int nWords )
00229 {
00230 int Hash = Aig_TsiStateHash( pState, nWords, p->nBins );
00231 assert( !Aig_TsiStateLookup( p, pState, nWords ) );
00232 Aig_TsiSetNext( pState, nWords, p->pBins[Hash] );
00233 p->pBins[Hash] = pState;
00234 }
00235
00247 unsigned * Aig_TsiStateNew( Aig_Tsi_t * p )
00248 {
00249 unsigned * pState;
00250 pState = (unsigned *)Aig_MmFixedEntryFetch( p->pMem );
00251 memset( pState, 0, sizeof(unsigned) * p->nWords );
00252 Vec_PtrPush( p->vStates, pState );
00253 return pState;
00254 }
00255
00267 void Aig_TsiStatePrint( Aig_Tsi_t * p, unsigned * pState )
00268 {
00269 int i, Value, nZeros = 0, nOnes = 0, nDcs = 0;
00270 for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
00271 {
00272 Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
00273 if ( Value == 1 )
00274 printf( "0" ), nZeros++;
00275 else if ( Value == 2 )
00276 printf( "1" ), nOnes++;
00277 else if ( Value == 3 )
00278 printf( "x" ), nDcs++;
00279 else
00280 assert( 0 );
00281 }
00282 printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs );
00283 }
00284
00285
00298 Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
00299 {
00300 Aig_Tsi_t * pTsi;
00301 Vec_Ptr_t * vMap;
00302 Aig_Obj_t * pObj, * pObjLi, * pObjLo;
00303 unsigned * pState, * pPrev;
00304 int i, k, f, fConstants, Value, nCounter;
00305
00306 pTsi = Aig_TsiStart( p );
00307
00308 Aig_ObjSetXsim( Aig_ManConst1(p), AIG_XVS1 );
00309 Aig_ManForEachPiSeq( p, pObj, i )
00310 Aig_ObjSetXsim( pObj, AIG_XVSX );
00311 Aig_ManForEachLoSeq( p, pObj, i )
00312 Aig_ObjSetXsim( pObj, AIG_XVS0 );
00313
00314 for ( f = 0; f < TSI_MAX_ROUNDS; f++ )
00315 {
00316
00317 pState = Aig_TsiStateNew( pTsi );
00318 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
00319 {
00320 Value = Aig_ObjGetXsim(pObjLo);
00321 if ( Value & 1 )
00322 Aig_InfoSetBit( pState, 2 * i );
00323 if ( Value & 2 )
00324 Aig_InfoSetBit( pState, 2 * i + 1 );
00325 }
00326
00327
00328 if ( Aig_TsiStateLookup( pTsi, pState, pTsi->nWords ) )
00329 break;
00330
00331 Aig_TsiStateInsert( pTsi, pState, pTsi->nWords );
00332
00333 Aig_ManForEachNode( p, pObj, i )
00334 Aig_ObjSetXsim( pObj, Aig_XsimAnd(Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj)) );
00335
00336 Aig_ManForEachLiSeq( p, pObj, i )
00337 Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) );
00338 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
00339 Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) );
00340 }
00341 if ( f == TSI_MAX_ROUNDS )
00342 {
00343 printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations (not a bug).\n", TSI_MAX_ROUNDS );
00344 Aig_TsiStop( pTsi );
00345 return NULL;
00346 }
00347
00348 pState = Vec_PtrEntry( pTsi->vStates, 0 );
00349 Vec_PtrForEachEntry( pTsi->vStates, pPrev, i )
00350 {
00351 for ( k = 0; k < pTsi->nWords; k++ )
00352 pState[k] |= pPrev[k];
00353 }
00354
00355 fConstants = 0;
00356 if ( 2*Aig_ManRegNum(p) == 32*pTsi->nWords )
00357 {
00358 for ( i = 0; i < pTsi->nWords; i++ )
00359 if ( pState[i] != ~0 )
00360 fConstants = 1;
00361 }
00362 else
00363 {
00364 for ( i = 0; i < pTsi->nWords - 1; i++ )
00365 if ( pState[i] != ~0 )
00366 fConstants = 1;
00367 if ( pState[i] != Aig_InfoMask( 2*Aig_ManRegNum(p) - 32*(pTsi->nWords-1) ) )
00368 fConstants = 1;
00369 }
00370 if ( fConstants == 0 )
00371 {
00372 Aig_TsiStop( pTsi );
00373 return NULL;
00374 }
00375
00376
00377 vMap = Vec_PtrAlloc( Aig_ManPiNum(p) );
00378 Aig_ManForEachPiSeq( p, pObj, i )
00379 Vec_PtrPush( vMap, pObj );
00380
00381 nCounter = 0;
00382 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
00383 {
00384 Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
00385 nCounter += (Value == 1 || Value == 2);
00386 if ( Value == 1 )
00387 Vec_PtrPush( vMap, Aig_ManConst0(p) );
00388 else if ( Value == 2 )
00389 Vec_PtrPush( vMap, Aig_ManConst1(p) );
00390 else if ( Value == 3 )
00391 Vec_PtrPush( vMap, pObjLo );
00392 else
00393 assert( 0 );
00394
00395 }
00396
00397 Aig_TsiStop( pTsi );
00398 if ( fVerbose )
00399 printf( "Detected %d constants after %d iterations of ternary simulation.\n", nCounter, f );
00400 return vMap;
00401 }
00402
00414 Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose )
00415 {
00416 Aig_Man_t * pTemp;
00417 Vec_Ptr_t * vMap;
00418 while ( (vMap = Aig_ManTernarySimulate( p, fVerbose )) )
00419 {
00420 if ( fVerbose )
00421 printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
00422 p = Aig_ManRemap( pTemp = p, vMap );
00423 Aig_ManStop( pTemp );
00424 Vec_PtrFree( vMap );
00425 Aig_ManSeqCleanup( p );
00426 if ( fVerbose )
00427 printf( "REnd = %5d. NEnd = %6d. \n", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
00428 }
00429 return p;
00430 }
00431
00435
00436