ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
aigTsim.c
Go to the documentation of this file.
1
20
21#include "aig.h"
22#include "aig/saig/saig.h"
23
25
26
30
31#define TSI_MAX_ROUNDS 1000
32#define TSI_ONE_SERIES 300
33
34#define AIG_XVS0 1
35#define AIG_XVS1 2
36#define AIG_XVSX 3
37
38static inline void Aig_ObjSetXsim( Aig_Obj_t * pObj, int Value ) { pObj->nCuts = Value; }
39static inline int Aig_ObjGetXsim( Aig_Obj_t * pObj ) { return pObj->nCuts; }
40static inline int Aig_XsimInv( int Value )
41{
42 if ( Value == AIG_XVS0 )
43 return AIG_XVS1;
44 if ( Value == AIG_XVS1 )
45 return AIG_XVS0;
46 assert( Value == AIG_XVSX );
47 return AIG_XVSX;
48}
49static inline int Aig_XsimAnd( int Value0, int Value1 )
50{
51 if ( Value0 == AIG_XVS0 || Value1 == AIG_XVS0 )
52 return AIG_XVS0;
53 if ( Value0 == AIG_XVSX || Value1 == AIG_XVSX )
54 return AIG_XVSX;
55 assert( Value0 == AIG_XVS1 && Value1 == AIG_XVS1 );
56 return AIG_XVS1;
57}
58static inline int Aig_XsimRand2()
59{
60 return (Aig_ManRandom(0) & 1) ? AIG_XVS1 : AIG_XVS0;
61}
62static inline int Aig_XsimRand3()
63{
64 int RetValue;
65 do {
66 RetValue = Aig_ManRandom(0) & 3;
67 } while ( RetValue == 0 );
68 return RetValue;
69}
70static inline int Aig_ObjGetXsimFanin0( Aig_Obj_t * pObj )
71{
72 int RetValue;
73 RetValue = Aig_ObjGetXsim(Aig_ObjFanin0(pObj));
74 return Aig_ObjFaninC0(pObj)? Aig_XsimInv(RetValue) : RetValue;
75}
76static inline int Aig_ObjGetXsimFanin1( Aig_Obj_t * pObj )
77{
78 int RetValue;
79 RetValue = Aig_ObjGetXsim(Aig_ObjFanin1(pObj));
80 return Aig_ObjFaninC1(pObj)? Aig_XsimInv(RetValue) : RetValue;
81}
82static inline void Aig_XsimPrint( FILE * pFile, int Value )
83{
84 if ( Value == AIG_XVS0 )
85 {
86 fprintf( pFile, "0" );
87 return;
88 }
89 if ( Value == AIG_XVS1 )
90 {
91 fprintf( pFile, "1" );
92 return;
93 }
94 assert( Value == AIG_XVSX );
95 fprintf( pFile, "x" );
96}
97
98// simulation manager
99typedef struct Aig_Tsi_t_ Aig_Tsi_t;
101{
102 Aig_Man_t * pAig; // the original AIG manager
103 // ternary state representation
104 int nWords; // the number of words in the states
105 Vec_Ptr_t * vStates; // the collection of ternary states
106 Aig_MmFixed_t * pMem; // memory for ternary states
107 // hash table for terminary states
108 unsigned ** pBins;
109 int nBins;
110};
111
112static inline unsigned * Aig_TsiNext( unsigned * pState, int nWords ) { return *((unsigned **)(pState + nWords)); }
113static inline void Aig_TsiSetNext( unsigned * pState, int nWords, unsigned * pNext ) { *((unsigned **)(pState + nWords)) = pNext; }
114
118
131{
132 Aig_Tsi_t * p;
133 p = ABC_ALLOC( Aig_Tsi_t, 1 );
134 memset( p, 0, sizeof(Aig_Tsi_t) );
135 p->pAig = pAig;
136 p->nWords = Abc_BitWordNum( 2*Aig_ManRegNum(pAig) );
137 p->vStates = Vec_PtrAlloc( 1000 );
138 p->pMem = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 );
139 p->nBins = Abc_PrimeCudd(TSI_MAX_ROUNDS/2);
140 p->pBins = ABC_ALLOC( unsigned *, p->nBins );
141 memset( p->pBins, 0, sizeof(unsigned *) * p->nBins );
142 return p;
143}
144
157{
158 Aig_MmFixedStop( p->pMem, 0 );
159 Vec_PtrFree( p->vStates );
160 ABC_FREE( p->pBins );
161 ABC_FREE( p );
162}
163
175int Aig_TsiStateHash( unsigned * pState, int nWords, int nTableSize )
176{
177 static int s_FPrimes[128] = {
178 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
179 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
180 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
181 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
182 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
183 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
184 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
185 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
186 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
187 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
188 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
189 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
190 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
191 };
192 unsigned uHash;
193 int i;
194 uHash = 0;
195 for ( i = 0; i < nWords; i++ )
196 uHash ^= pState[i] * s_FPrimes[i & 0x7F];
197 return uHash % nTableSize;
198}
199
211int Aig_TsiStateLookup( Aig_Tsi_t * p, unsigned * pState, int nWords )
212{
213 unsigned * pEntry;
214 int Hash;
215 Hash = Aig_TsiStateHash( pState, nWords, p->nBins );
216 for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Aig_TsiNext(pEntry, nWords) )
217 if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
218 return 1;
219 return 0;
220}
221
233void Aig_TsiStateInsert( Aig_Tsi_t * p, unsigned * pState, int nWords )
234{
235 int Hash = Aig_TsiStateHash( pState, nWords, p->nBins );
236 assert( !Aig_TsiStateLookup( p, pState, nWords ) );
237 Aig_TsiSetNext( pState, nWords, p->pBins[Hash] );
238 p->pBins[Hash] = pState;
239}
240
253{
254 unsigned * pState;
255 pState = (unsigned *)Aig_MmFixedEntryFetch( p->pMem );
256 memset( pState, 0, sizeof(unsigned) * p->nWords );
257 Vec_PtrPush( p->vStates, pState );
258 return pState;
259}
260
272void Aig_TsiStatePrint( Aig_Tsi_t * p, unsigned * pState )
273{
274 int i, Value, nZeros = 0, nOnes = 0, nDcs = 0;
275 for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
276 {
277 Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
278 if ( Value == 1 )
279 printf( "0" ), nZeros++;
280 else if ( Value == 2 )
281 printf( "1" ), nOnes++;
282 else if ( Value == 3 )
283 printf( "x" ), nDcs++;
284 else
285 assert( 0 );
286 }
287 printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs );
288}
289
301int Aig_TsiStateCount( Aig_Tsi_t * p, unsigned * pState )
302{
303 Aig_Obj_t * pObjLi, * pObjLo;
304 int i, Value, nCounter = 0;
305 Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
306 {
307 Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
308 nCounter += (Value == 1 || Value == 2);
309 }
310 return nCounter;
311}
312
324void Aig_TsiStateOrAll( Aig_Tsi_t * pTsi, unsigned * pState )
325{
326 unsigned * pPrev;
327 int i, k;
328 Vec_PtrForEachEntry( unsigned *, pTsi->vStates, pPrev, i )
329 {
330 for ( k = 0; k < pTsi->nWords; k++ )
331 pState[k] |= pPrev[k];
332 }
333}
334
335
348Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose, int fVeryVerbose )
349{
350 Aig_Tsi_t * pTsi;
351 Vec_Ptr_t * vMap;
352 Aig_Obj_t * pObj, * pObjLi, * pObjLo;
353 unsigned * pState;//, * pPrev;
354 int i, f, fConstants, Value, nCounter, nRetired;
355 // allocate the simulation manager
356 pTsi = Aig_TsiStart( p );
357 // initialize the values
358 Aig_ObjSetXsim( Aig_ManConst1(p), AIG_XVS1 );
359 Aig_ManForEachPiSeq( p, pObj, i )
360 Aig_ObjSetXsim( pObj, AIG_XVSX );
361 Aig_ManForEachLoSeq( p, pObj, i )
362 Aig_ObjSetXsim( pObj, AIG_XVS0 );
363 // simulate for the given number of timeframes
364 for ( f = 0; f < TSI_MAX_ROUNDS; f++ )
365 {
366 // collect this state
367 pState = Aig_TsiStateNew( pTsi );
368 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
369 {
370 Value = Aig_ObjGetXsim(pObjLo);
371 if ( Value & 1 )
372 Abc_InfoSetBit( pState, 2 * i );
373 if ( Value & 2 )
374 Abc_InfoSetBit( pState, 2 * i + 1 );
375 }
376
377// printf( "%d ", Aig_TsiStateCount(pTsi, pState) );
378if ( fVeryVerbose )
379{
380printf( "%3d : ", f );
381Aig_TsiStatePrint( pTsi, pState );
382}
383 // check if this state exists
384 if ( Aig_TsiStateLookup( pTsi, pState, pTsi->nWords ) )
385 break;
386// nCounter = 0;
387// Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
388// nCounter += (Aig_ObjGetXsim(pObjLo) == AIG_XVS0);
389//printf( "%d -> ", nCounter );
390 // insert this state
391 Aig_TsiStateInsert( pTsi, pState, pTsi->nWords );
392 // simulate internal nodes
393 Aig_ManForEachNode( p, pObj, i )
394 {
395 Aig_ObjSetXsim( pObj, Aig_XsimAnd(Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj)) );
396// printf( "%d %d Id = %2d. Value = %d.\n",
397// Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj),
398// i, Aig_XsimAnd(Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj)) );
399 }
400 // transfer the latch values
401 Aig_ManForEachLiSeq( p, pObj, i )
402 Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) );
403 nCounter = 0;
404 nRetired = 0;
405 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
406 {
407 if ( f < TSI_ONE_SERIES )
408 Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) );
409 else
410 {
411 if ( Aig_ObjGetXsim(pObjLi) != Aig_ObjGetXsim(pObjLo) )
412 {
413 Aig_ObjSetXsim( pObjLo, AIG_XVSX );
414 nRetired++;
415 }
416 }
417 nCounter += (Aig_ObjGetXsim(pObjLo) == AIG_XVS0);
418 }
419// if ( nRetired )
420// printf( "Retired %d registers.\n", nRetired );
421
422// if ( f && (f % 1000 == 0) )
423// printf( "%d \n", f );
424//printf( "%d ", nCounter );
425 }
426//printf( "\n" );
427 if ( f == TSI_MAX_ROUNDS )
428 {
429 printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations (not a bug).\n", TSI_MAX_ROUNDS );
430 Aig_TsiStop( pTsi );
431 return NULL;
432 }
433 // OR all the states
434 pState = (unsigned *)Vec_PtrEntry( pTsi->vStates, 0 );
435 Aig_TsiStateOrAll( pTsi, pState );
436 // check if there are constants
437 fConstants = 0;
438 if ( 2*Aig_ManRegNum(p) == 32*pTsi->nWords )
439 {
440 for ( i = 0; i < pTsi->nWords; i++ )
441 if ( pState[i] != ~0 )
442 fConstants = 1;
443 }
444 else
445 {
446 for ( i = 0; i < pTsi->nWords - 1; i++ )
447 if ( pState[i] != ~0 )
448 fConstants = 1;
449 if ( pState[i] != Abc_InfoMask( 2*Aig_ManRegNum(p) - 32*(pTsi->nWords-1) ) )
450 fConstants = 1;
451 }
452 if ( fConstants == 0 )
453 {
454 if ( fVerbose )
455 printf( "Detected 0 constants after %d iterations of ternary simulation.\n", f );
456 Aig_TsiStop( pTsi );
457 return NULL;
458 }
459
460 // start mapping by adding the true PIs
461 vMap = Vec_PtrAlloc( Aig_ManCiNum(p) );
462 Aig_ManForEachPiSeq( p, pObj, i )
463 Vec_PtrPush( vMap, pObj );
464 // find constant registers
465 nCounter = 0;
466 Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
467 {
468 Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
469 nCounter += (Value == 1 || Value == 2);
470 if ( Value == 1 )
471 Vec_PtrPush( vMap, Aig_ManConst0(p) );
472 else if ( Value == 2 )
473 Vec_PtrPush( vMap, Aig_ManConst1(p) );
474 else if ( Value == 3 )
475 Vec_PtrPush( vMap, pObjLo );
476 else
477 assert( 0 );
478// Aig_XsimPrint( stdout, Value );
479 }
480// printf( "\n" );
481 Aig_TsiStop( pTsi );
482 if ( fVerbose )
483 printf( "Detected %d constants after %d iterations of ternary simulation.\n", nCounter, f );
484 return vMap;
485}
486
498Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose )
499{
500 Aig_Man_t * pTemp;
501 Vec_Ptr_t * vMap;
502 while ( Aig_ManRegNum(p) > 0 )
503 {
504 if ( fUseMvSweep )
505 vMap = Saig_MvManSimulate( p, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
506 else
507 vMap = Aig_ManTernarySimulate( p, fVerbose, fVeryVerbose );
508 if ( vMap == NULL )
509 break;
510 p = Aig_ManRemap( pTemp = p, vMap );
511 Vec_PtrFree( vMap );
513 if ( fVerbose )
514 Aig_ManReportImprovement( pTemp, p );
515 Aig_ManStop( pTemp );
516 }
517 return p;
518}
519
523
524
526
int nWords
Definition abcNpn.c:127
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
struct Aig_Tsi_t_ Aig_Tsi_t
Definition aigTsim.c:99
#define AIG_XVS1
Definition aigTsim.c:35
Aig_Man_t * Aig_ManConstReduce(Aig_Man_t *p, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose)
Definition aigTsim.c:498
void Aig_TsiStop(Aig_Tsi_t *p)
Definition aigTsim.c:156
int Aig_TsiStateHash(unsigned *pState, int nWords, int nTableSize)
Definition aigTsim.c:175
#define AIG_XVSX
Definition aigTsim.c:36
int Aig_TsiStateCount(Aig_Tsi_t *p, unsigned *pState)
Definition aigTsim.c:301
Aig_Tsi_t * Aig_TsiStart(Aig_Man_t *pAig)
FUNCTION DEFINITIONS ///.
Definition aigTsim.c:130
int Aig_TsiStateLookup(Aig_Tsi_t *p, unsigned *pState, int nWords)
Definition aigTsim.c:211
void Aig_TsiStateOrAll(Aig_Tsi_t *pTsi, unsigned *pState)
Definition aigTsim.c:324
#define TSI_ONE_SERIES
Definition aigTsim.c:32
#define AIG_XVS0
Definition aigTsim.c:34
void Aig_TsiStatePrint(Aig_Tsi_t *p, unsigned *pState)
Definition aigTsim.c:272
#define TSI_MAX_ROUNDS
DECLARATIONS ///.
Definition aigTsim.c:31
Vec_Ptr_t * Aig_ManTernarySimulate(Aig_Man_t *p, int fVerbose, int fVeryVerbose)
Definition aigTsim.c:348
unsigned * Aig_TsiStateNew(Aig_Tsi_t *p)
Definition aigTsim.c:252
void Aig_TsiStateInsert(Aig_Tsi_t *p, unsigned *pState, int nWords)
Definition aigTsim.c:233
int Aig_ManSeqCleanup(Aig_Man_t *p)
Definition aigScl.c:158
char * Aig_MmFixedEntryFetch(Aig_MmFixed_t *p)
Definition aigMem.c:161
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
#define Aig_ManForEachLiSeq(p, pObj, i)
Definition aig.h:447
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
void Aig_ManReportImprovement(Aig_Man_t *p, Aig_Man_t *pNew)
Definition aigMan.c:415
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_Man_t * Aig_ManRemap(Aig_Man_t *p, Vec_Ptr_t *vMap)
DECLARATIONS ///.
Definition aigScl.c:46
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition aig.h:438
Aig_MmFixed_t * Aig_MmFixedStart(int nEntrySize, int nEntriesMax)
FUNCTION DEFINITIONS ///.
Definition aigMem.c:96
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition aig.h:441
struct Aig_MmFixed_t_ Aig_MmFixed_t
Definition aig.h:52
void Aig_MmFixedStop(Aig_MmFixed_t *p, int fVerbose)
Definition aigMem.c:132
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition aig.h:450
unsigned Aig_ManRandom(int fReset)
Definition aigUtil.c:1170
Cube * p
Definition exorList.c:222
Vec_Ptr_t * Saig_MvManSimulate(Aig_Man_t *pAig, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose)
Definition saigSimMv.c:879
unsigned nCuts
Definition aig.h:83
int nWords
Definition aigTsim.c:104
int nBins
Definition aigTsim.c:109
Aig_MmFixed_t * pMem
Definition aigTsim.c:106
Vec_Ptr_t * vStates
Definition aigTsim.c:105
Aig_Man_t * pAig
Definition aigTsim.c:102
unsigned ** pBins
Definition aigTsim.c:108
#define assert(ex)
Definition util_old.h:213
char * memset()
int memcmp()
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55