abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaEra.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [giaEra.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis [Explicit reachability analysis.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: giaEra.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 #include "misc/mem/mem.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 // explicit state representation
32 typedef struct Gia_ObjEra_t_ Gia_ObjEra_t;
33 struct Gia_ObjEra_t_
34 {
35  int Num; // ID of this state
36  int Cond; // input condition
37  int iPrev; // previous state
38  int iNext; // next state in the hash table
39  unsigned pData[0]; // state bits
40 };
41 
42 // explicit state reachability
43 typedef struct Gia_ManEra_t_ Gia_ManEra_t;
44 struct Gia_ManEra_t_
45 {
46  Gia_Man_t * pAig; // user's AIG manager
47  int nWordsSim; // 2^(PInum)
48  int nWordsDat; // Abc_BitWordNum
49  unsigned * pDataSim; // simulation data
50  Mem_Fixed_t * pMemory; // memory manager
51  Vec_Ptr_t * vStates; // reached states
52  Gia_ObjEra_t * pStateNew; // temporary state
53  int iCurState; // the current state
54  Vec_Int_t * vBugTrace; // the sequence of transitions
55  Vec_Int_t * vStgDump; // STG written into a file
56  // hash table for states
57  int nBins;
58  unsigned * pBins;
59 };
60 
61 static inline unsigned * Gia_ManEraData( Gia_ManEra_t * p, int i ) { return p->pDataSim + i * p->nWordsSim; }
62 static inline Gia_ObjEra_t * Gia_ManEraState( Gia_ManEra_t * p, int i ) { return (Gia_ObjEra_t *)Vec_PtrEntry(p->vStates, i); }
63 
64 ////////////////////////////////////////////////////////////////////////
65 /// FUNCTION DEFINITIONS ///
66 ////////////////////////////////////////////////////////////////////////
67 
68 /**Function*************************************************************
69 
70  Synopsis [Creates reachability manager.]
71 
72  Description []
73 
74  SideEffects []
75 
76  SeeAlso []
77 
78 ***********************************************************************/
79 Gia_ManEra_t * Gia_ManEraCreate( Gia_Man_t * pAig )
80 {
81  Vec_Ptr_t * vTruths;
82  Gia_ManEra_t * p;
83  unsigned * pTruth, * pSimInfo;
84  int i;
85  p = ABC_CALLOC( Gia_ManEra_t, 1 );
86  p->pAig = pAig;
87  p->nWordsSim = Abc_TruthWordNum( Gia_ManPiNum(pAig) );
88  p->nWordsDat = Abc_BitWordNum( Gia_ManRegNum(pAig) );
89  p->pDataSim = ABC_ALLOC( unsigned, p->nWordsSim*Gia_ManObjNum(pAig) );
90  p->pMemory = Mem_FixedStart( sizeof(Gia_ObjEra_t) + sizeof(unsigned) * p->nWordsDat );
91  p->vStates = Vec_PtrAlloc( 100000 );
92  p->nBins = Abc_PrimeCudd( 100000 );
93  p->pBins = ABC_CALLOC( unsigned, p->nBins );
94  Vec_PtrPush( p->vStates, NULL );
95  // assign primary input values
96  vTruths = Vec_PtrAllocTruthTables( Gia_ManPiNum(pAig) );
97  Vec_PtrForEachEntry( unsigned *, vTruths, pTruth, i )
98  {
99  pSimInfo = Gia_ManEraData( p, Gia_ObjId(pAig, Gia_ManPi(pAig, i)) );
100  memcpy( pSimInfo, pTruth, sizeof(unsigned) * p->nWordsSim );
101  }
102  Vec_PtrFree( vTruths );
103  // assign constant zero node
104  pSimInfo = Gia_ManEraData( p, 0 );
105  memset( pSimInfo, 0, sizeof(unsigned) * p->nWordsSim );
106  p->vStgDump = Vec_IntAlloc( 1000 );
107  return p;
108 }
109 
110 /**Function*************************************************************
111 
112  Synopsis [Deletes reachability manager.]
113 
114  Description []
115 
116  SideEffects []
117 
118  SeeAlso []
119 
120 ***********************************************************************/
121 void Gia_ManEraFree( Gia_ManEra_t * p )
122 {
123  Mem_FixedStop( p->pMemory, 0 );
124  Vec_IntFree( p->vStgDump );
125  Vec_PtrFree( p->vStates );
126  if ( p->vBugTrace ) Vec_IntFree( p->vBugTrace );
127  ABC_FREE( p->pDataSim );
128  ABC_FREE( p->pBins );
129  ABC_FREE( p );
130 }
131 
132 /**Function*************************************************************
133 
134  Synopsis [Creates new state.]
135 
136  Description []
137 
138  SideEffects []
139 
140  SeeAlso []
141 
142 ***********************************************************************/
143 Gia_ObjEra_t * Gia_ManEraCreateState( Gia_ManEra_t * p )
144 {
145  Gia_ObjEra_t * pNew;
146  pNew = (Gia_ObjEra_t *)Mem_FixedEntryFetch( p->pMemory );
147  pNew->Num = Vec_PtrSize( p->vStates );
148  pNew->iPrev = 0;
149  Vec_PtrPush( p->vStates, pNew );
150  return pNew;
151 }
152 
153 
154 /**Function*************************************************************
155 
156  Synopsis [Computes hash value of the node using its simulation info.]
157 
158  Description []
159 
160  SideEffects []
161 
162  SeeAlso []
163 
164 ***********************************************************************/
165 int Gia_ManEraStateHash( unsigned * pState, int nWordsSim, int nTableSize )
166 {
167  static int s_FPrimes[128] = {
168  1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
169  1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
170  2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
171  2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
172  3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
173  3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
174  4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
175  4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
176  5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
177  6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
178  6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
179  7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
180  8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
181  };
182  unsigned uHash;
183  int i;
184  uHash = 0;
185  for ( i = 0; i < nWordsSim; i++ )
186  uHash ^= pState[i] * s_FPrimes[i & 0x7F];
187  return uHash % nTableSize;
188 }
189 
190 /**Function*************************************************************
191 
192  Synopsis [Returns the place of this state in the table or NULL if it exists.]
193 
194  Description []
195 
196  SideEffects []
197 
198  SeeAlso []
199 
200 ***********************************************************************/
201 static inline unsigned * Gia_ManEraHashFind( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int * pStateNum )
202 {
203  Gia_ObjEra_t * pThis;
204  unsigned * pPlace = p->pBins + Gia_ManEraStateHash( pState->pData, p->nWordsDat, p->nBins );
205  for ( pThis = (*pPlace)? Gia_ManEraState(p, *pPlace) : NULL; pThis;
206  pPlace = (unsigned *)&pThis->iNext, pThis = (*pPlace)? Gia_ManEraState(p, *pPlace) : NULL )
207  if ( !memcmp( pState->pData, pThis->pData, sizeof(unsigned) * p->nWordsDat ) )
208  {
209  if ( pStateNum )
210  *pStateNum = pThis->Num;
211  return NULL;
212  }
213  if ( pStateNum )
214  *pStateNum = -1;
215  return pPlace;
216 }
217 
218 /**Function*************************************************************
219 
220  Synopsis [Resizes the hash table.]
221 
222  Description []
223 
224  SideEffects []
225 
226  SeeAlso []
227 
228 ***********************************************************************/
229 void Gia_ManEraHashResize( Gia_ManEra_t * p )
230 {
231  Gia_ObjEra_t * pThis;
232  unsigned * pBinsOld, * piPlace;
233  int nBinsOld, iNext, Counter, i;
234  assert( p->pBins != NULL );
235  // replace the table
236  pBinsOld = p->pBins;
237  nBinsOld = p->nBins;
238  p->nBins = Abc_PrimeCudd( 3 * p->nBins );
239  p->pBins = ABC_CALLOC( unsigned, p->nBins );
240  // rehash the entries from the old table
241  Counter = 0;
242  for ( i = 0; i < nBinsOld; i++ )
243  for ( pThis = (pBinsOld[i]? Gia_ManEraState(p, pBinsOld[i]) : NULL),
244  iNext = (pThis? pThis->iNext : 0);
245  pThis; pThis = (iNext? Gia_ManEraState(p, iNext) : NULL),
246  iNext = (pThis? pThis->iNext : 0) )
247  {
248  assert( pThis->Num );
249  pThis->iNext = 0;
250  piPlace = Gia_ManEraHashFind( p, pThis, NULL );
251  assert( *piPlace == 0 ); // should not be there
252  *piPlace = pThis->Num;
253  Counter++;
254  }
255  assert( Counter == Vec_PtrSize( p->vStates ) - 1 );
256  ABC_FREE( pBinsOld );
257 }
258 
259 /**Function*************************************************************
260 
261  Synopsis [Initialize register output to the given state.]
262 
263  Description []
264 
265  SideEffects []
266 
267  SeeAlso []
268 
269 ***********************************************************************/
270 void Gia_ManInsertState( Gia_ManEra_t * p, Gia_ObjEra_t * pState )
271 {
272  Gia_Obj_t * pObj;
273  unsigned * pSimInfo;
274  int i;
275  Gia_ManForEachRo( p->pAig, pObj, i )
276  {
277  pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) );
278  if ( Abc_InfoHasBit(pState->pData, i) )
279  memset( pSimInfo, 0xff, sizeof(unsigned) * p->nWordsSim );
280  else
281  memset( pSimInfo, 0, sizeof(unsigned) * p->nWordsSim );
282  }
283 }
284 
285 /**Function*************************************************************
286 
287  Synopsis [Returns -1 if outputs are not asserted.]
288 
289  Description []
290 
291  SideEffects []
292 
293  SeeAlso []
294 
295 ***********************************************************************/
296 static inline int Gia_ManOutputAsserted( Gia_ManEra_t * p, Gia_Obj_t * pObj )
297 {
298  unsigned * pInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) );
299  int w;
300  for ( w = 0; w < p->nWordsSim; w++ )
301  if ( pInfo[w] )
302  return 32*w + Gia_WordFindFirstBit( pInfo[w] );
303  return -1;
304 }
305 
306 /**Function*************************************************************
307 
308  Synopsis []
309 
310  Description []
311 
312  SideEffects []
313 
314  SeeAlso []
315 
316 ***********************************************************************/
317 static inline void Gia_ManSimulateCo( Gia_ManEra_t * p, Gia_Obj_t * pObj )
318 {
319  int Id = Gia_ObjId(p->pAig, pObj);
320  unsigned * pInfo = Gia_ManEraData( p, Id );
321  unsigned * pInfo0 = Gia_ManEraData( p, Gia_ObjFaninId0(pObj, Id) );
322  int w;
323  if ( Gia_ObjFaninC0(pObj) )
324  for ( w = p->nWordsSim-1; w >= 0; w-- )
325  pInfo[w] = ~pInfo0[w];
326  else
327  for ( w = p->nWordsSim-1; w >= 0; w-- )
328  pInfo[w] = pInfo0[w];
329 }
330 
331 /**Function*************************************************************
332 
333  Synopsis []
334 
335  Description []
336 
337  SideEffects []
338 
339  SeeAlso []
340 
341 ***********************************************************************/
342 static inline void Gia_ManSimulateNode( Gia_ManEra_t * p, Gia_Obj_t * pObj )
343 {
344  int Id = Gia_ObjId(p->pAig, pObj);
345  unsigned * pInfo = Gia_ManEraData( p, Id );
346  unsigned * pInfo0 = Gia_ManEraData( p, Gia_ObjFaninId0(pObj, Id) );
347  unsigned * pInfo1 = Gia_ManEraData( p, Gia_ObjFaninId1(pObj, Id) );
348  int w;
349  if ( Gia_ObjFaninC0(pObj) )
350  {
351  if ( Gia_ObjFaninC1(pObj) )
352  for ( w = p->nWordsSim-1; w >= 0; w-- )
353  pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
354  else
355  for ( w = p->nWordsSim-1; w >= 0; w-- )
356  pInfo[w] = ~pInfo0[w] & pInfo1[w];
357  }
358  else
359  {
360  if ( Gia_ObjFaninC1(pObj) )
361  for ( w = p->nWordsSim-1; w >= 0; w-- )
362  pInfo[w] = pInfo0[w] & ~pInfo1[w];
363  else
364  for ( w = p->nWordsSim-1; w >= 0; w-- )
365  pInfo[w] = pInfo0[w] & pInfo1[w];
366  }
367 }
368 
369 /**Function*************************************************************
370 
371  Synopsis [Performs one iteration of reachability analysis.]
372 
373  Description []
374 
375  SideEffects []
376 
377  SeeAlso []
378 
379 ***********************************************************************/
380 void Gia_ManPerformOneIter( Gia_ManEra_t * p )
381 {
382  Gia_Obj_t * pObj;
383  int i;
384  Gia_ManForEachObj1( p->pAig, pObj, i )
385  {
386  if ( Gia_ObjIsAnd(pObj) )
387  Gia_ManSimulateNode( p, pObj );
388  else if ( Gia_ObjIsCo(pObj) )
389  Gia_ManSimulateCo( p, pObj );
390  }
391 }
392 
393 /**Function*************************************************************
394 
395  Synopsis [Performs one iteration of reachability analysis.]
396 
397  Description []
398 
399  SideEffects []
400 
401  SeeAlso []
402 
403 ***********************************************************************/
404 Vec_Int_t * Gia_ManCollectBugTrace( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int iCond )
405 {
406  Vec_Int_t * vTrace;
407  vTrace = Vec_IntAlloc( 10 );
408  Vec_IntPush( vTrace, iCond );
409  for ( ; pState; pState = pState->iPrev ? Gia_ManEraState(p, pState->iPrev) : NULL )
410  Vec_IntPush( vTrace, pState->Cond );
411  Vec_IntReverseOrder( vTrace );
412  return vTrace;
413 }
414 
415 /**Function*************************************************************
416 
417  Synopsis [Counts the depth of state transitions leading ot this state.]
418 
419  Description []
420 
421  SideEffects []
422 
423  SeeAlso []
424 
425 ***********************************************************************/
426 int Gia_ManCountDepth( Gia_ManEra_t * p )
427 {
428  Gia_ObjEra_t * pState;
429  int Counter = 0;
430  pState = (Gia_ObjEra_t *)Vec_PtrEntryLast( p->vStates );
431  if ( pState->iPrev == 0 && Vec_PtrSize(p->vStates) > 3 )
432  pState = (Gia_ObjEra_t *)Vec_PtrEntry( p->vStates, Vec_PtrSize(p->vStates) - 2 );
433  for ( ; pState; pState = pState->iPrev ? Gia_ManEraState(p, pState->iPrev) : NULL )
434  Counter++;
435  return Counter;
436 }
437 
438 /**Function*************************************************************
439 
440  Synopsis [Analized reached states.]
441 
442  Description []
443 
444  SideEffects []
445 
446  SeeAlso []
447 
448 ***********************************************************************/
449 int Gia_ManAnalyzeResult( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int fMiter, int fStgDump )
450 {
451  Gia_Obj_t * pObj;
452  unsigned * pSimInfo, * piPlace, uOutput = 0;
453  int i, k, iCond, nMints, iNextState;
454  // check if the miter is asserted
455  if ( fMiter )
456  {
457  Gia_ManForEachPo( p->pAig, pObj, i )
458  {
459  iCond = Gia_ManOutputAsserted( p, pObj );
460  if ( iCond >= 0 )
461  {
462  p->vBugTrace = Gia_ManCollectBugTrace( p, pState, iCond );
463  return 1;
464  }
465  }
466  }
467  // collect reached states
468  nMints = (1 << Gia_ManPiNum(p->pAig));
469  for ( k = 0; k < nMints; k++ )
470  {
471  if ( p->pStateNew == NULL )
472  p->pStateNew = Gia_ManEraCreateState( p );
473  p->pStateNew->pData[p->nWordsDat-1] = 0;
474  Gia_ManForEachRi( p->pAig, pObj, i )
475  {
476  pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) );
477  if ( Abc_InfoHasBit(p->pStateNew->pData, i) != Abc_InfoHasBit(pSimInfo, k) )
478  Abc_InfoXorBit( p->pStateNew->pData, i );
479  }
480  if ( fStgDump )
481  {
482  uOutput = 0;
483  Gia_ManForEachPo( p->pAig, pObj, i )
484  {
485  pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) );
486  if ( Abc_InfoHasBit(pSimInfo, k) && i < 32 )
487  Abc_InfoXorBit( &uOutput, i );
488  }
489  }
490  piPlace = Gia_ManEraHashFind( p, p->pStateNew, &iNextState );
491  if ( fStgDump ) Vec_IntPush( p->vStgDump, k );
492  if ( fStgDump ) Vec_IntPush( p->vStgDump, pState->Num );
493  if ( piPlace == NULL )
494  {
495  if ( fStgDump ) Vec_IntPush( p->vStgDump, iNextState );
496  if ( fStgDump ) Vec_IntPush( p->vStgDump, uOutput );
497  continue;
498  }
499  if ( fStgDump ) Vec_IntPush( p->vStgDump, p->pStateNew->Num );
500  if ( fStgDump ) Vec_IntPush( p->vStgDump, uOutput );
501 //printf( "Inserting %d ", Vec_PtrSize(p->vStates) );
502 //Extra_PrintBinary( stdout, p->pStateNew->pData, Gia_ManRegNum(p->pAig) ); printf( "\n" );
503  assert( *piPlace == 0 );
504  *piPlace = p->pStateNew->Num;
505  p->pStateNew->Cond = k;
506  p->pStateNew->iPrev = pState->Num;
507  p->pStateNew->iNext = 0;
508  p->pStateNew = NULL;
509  // expand hash table if needed
510  if ( Vec_PtrSize(p->vStates) > 2 * p->nBins )
511  Gia_ManEraHashResize( p );
512  }
513  return 0;
514 }
515 
516 /**Function*************************************************************
517 
518  Synopsis [Resizes the hash table.]
519 
520  Description []
521 
522  SideEffects []
523 
524  SeeAlso []
525 
526 ***********************************************************************/
527 int Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fDumpFile, int fVerbose )
528 {
529  Gia_ManEra_t * p;
530  Gia_ObjEra_t * pState;
531  int Hash;
532  abctime clk = Abc_Clock();
533  int RetValue = 1;
534  assert( Gia_ManPiNum(pAig) <= 12 );
535  assert( Gia_ManRegNum(pAig) > 0 );
536  p = Gia_ManEraCreate( pAig );
537  // create init state
538  pState = Gia_ManEraCreateState( p );
539  pState->Cond = 0;
540  pState->iPrev = 0;
541  pState->iNext = 0;
542  memset( pState->pData, 0, sizeof(unsigned) * p->nWordsDat );
543  Hash = Gia_ManEraStateHash(pState->pData, p->nWordsDat, p->nBins);
544  p->pBins[ Hash ] = pState->Num;
545  // process reachable states
546  while ( p->iCurState < Vec_PtrSize( p->vStates ) - 1 )
547  {
548  if ( Vec_PtrSize(p->vStates) >= nStatesMax )
549  {
550  printf( "Reached the limit on states traversed (%d). ", nStatesMax );
551  RetValue = -1;
552  break;
553  }
554  pState = Gia_ManEraState( p, ++p->iCurState );
555  if ( p->iCurState > 1 && pState->iPrev == 0 )
556  continue;
557 //printf( "Extracting %d ", p->iCurState );
558 //Extra_PrintBinary( stdout, p->pStateNew->pData, Gia_ManRegNum(p->pAig) ); printf( "\n" );
559  Gia_ManInsertState( p, pState );
560  Gia_ManPerformOneIter( p );
561  if ( Gia_ManAnalyzeResult( p, pState, fMiter, fDumpFile ) && fMiter )
562  {
563  RetValue = 0;
564  printf( "Miter failed in state %d after %d transitions. ",
565  p->iCurState, Vec_IntSize(p->vBugTrace)-1 );
566  break;
567  }
568  if ( fVerbose && p->iCurState % 5000 == 0 )
569  {
570  printf( "States =%10d. Reached =%10d. R = %5.3f. Depth =%6d. Mem =%9.2f MB. ",
571  p->iCurState, Vec_PtrSize(p->vStates), 1.0*p->iCurState/Vec_PtrSize(p->vStates), Gia_ManCountDepth(p),
572  (1.0/(1<<20))*(1.0*Vec_PtrSize(p->vStates)*(sizeof(Gia_ObjEra_t) + sizeof(unsigned) * p->nWordsDat) +
573  1.0*p->nBins*sizeof(unsigned) + 1.0*p->vStates->nCap * sizeof(void*)) );
574  ABC_PRT( "Time", Abc_Clock() - clk );
575  }
576  }
577  printf( "Reachability analysis traversed %d states with depth %d. ", p->iCurState-1, Gia_ManCountDepth(p) );
578  ABC_PRT( "Time", Abc_Clock() - clk );
579  if ( fDumpFile )
580  {
581  char * pFileName = "test.stg";
582  FILE * pFile = fopen( pFileName, "wb" );
583  if ( pFile == NULL )
584  printf( "Cannot open file \"%s\" for writing.\n", pFileName );
585  else
586  {
587  Gia_ManStgPrint( pFile, p->vStgDump, Gia_ManPiNum(pAig), Gia_ManPoNum(pAig), p->iCurState-1 );
588  fclose( pFile );
589  printf( "Extracted STG was written into file \"%s\".\n", pFileName );
590  }
591  }
592  Gia_ManEraFree( p );
593  return RetValue;
594 }
595 
596 ////////////////////////////////////////////////////////////////////////
597 /// END OF FILE ///
598 ////////////////////////////////////////////////////////////////////////
599 
600 
601 ABC_NAMESPACE_IMPL_END
602 
memset
char * memset()
Gia_ManSimulateCo
static void Gia_ManSimulateCo(Gia_ManEra_t *p, Gia_Obj_t *pObj)
Definition: giaEra.c:317
Gia_ManEra_t_::pStateNew
Gia_ObjEra_t * pStateNew
Definition: giaEra.c:52
Gia_ManCountDepth
int Gia_ManCountDepth(Gia_ManEra_t *p)
Definition: giaEra.c:426
Gia_ManEraHashFind
static unsigned * Gia_ManEraHashFind(Gia_ManEra_t *p, Gia_ObjEra_t *pState, int *pStateNum)
Definition: giaEra.c:201
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Gia_ManEra_t_::nWordsSim
int nWordsSim
Definition: giaEra.c:47
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Gia_ManEra_t_::pBins
unsigned * pBins
Definition: giaEra.c:58
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ManEraFree
void Gia_ManEraFree(Gia_ManEra_t *p)
Definition: giaEra.c:121
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Gia_ManStgPrint
void Gia_ManStgPrint(FILE *pFile, Vec_Int_t *vLines, int nIns, int nOuts, int nStates)
Definition: giaStg.c:407
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Gia_ManEra_t_::pMemory
Mem_Fixed_t * pMemory
Definition: giaEra.c:50
Gia_ObjEra_t_
Definition: giaEra.c:33
Abc_InfoXorBit
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
Gia_ManEra_t_::vBugTrace
Vec_Int_t * vBugTrace
Definition: giaEra.c:54
Gia_ManEra_t_::nBins
int nBins
Definition: giaEra.c:57
Gia_ManEraCreate
Gia_ManEra_t * Gia_ManEraCreate(Gia_Man_t *pAig)
FUNCTION DEFINITIONS ///.
Definition: giaEra.c:79
Gia_ObjEra_t_::Num
int Num
Definition: giaEra.c:35
Gia_ManCollectBugTrace
Vec_Int_t * Gia_ManCollectBugTrace(Gia_ManEra_t *p, Gia_ObjEra_t *pState, int iCond)
Definition: giaEra.c:404
Gia_ManEra_t_::nWordsDat
int nWordsDat
Definition: giaEra.c:48
Gia_ManOutputAsserted
static int Gia_ManOutputAsserted(Gia_ManEra_t *p, Gia_Obj_t *pObj)
Definition: giaEra.c:296
Gia_ManAnalyzeResult
int Gia_ManAnalyzeResult(Gia_ManEra_t *p, Gia_ObjEra_t *pState, int fMiter, int fStgDump)
Definition: giaEra.c:449
Gia_WordFindFirstBit
static int Gia_WordFindFirstBit(unsigned uWord)
Definition: gia.h:321
Gia_ManSimulateNode
static void Gia_ManSimulateNode(Gia_ManEra_t *p, Gia_Obj_t *pObj)
Definition: giaEra.c:342
memcpy
char * memcpy()
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Mem_FixedStop
void Mem_FixedStop(Mem_Fixed_t *p, int fVerbose)
Definition: mem.c:139
Abc_TruthWordNum
static int Abc_TruthWordNum(int nVars)
Definition: abc_global.h:256
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Gia_ObjEra_t_::Cond
int Cond
Definition: giaEra.c:36
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Vec_IntReverseOrder
static void Vec_IntReverseOrder(Vec_Int_t *p)
Definition: vecInt.h:1042
Gia_ManCollectReachable
int Gia_ManCollectReachable(Gia_Man_t *pAig, int nStatesMax, int fMiter, int fDumpFile, int fVerbose)
Definition: giaEra.c:527
Gia_Obj_t_
Definition: gia.h:75
Vec_PtrAllocTruthTables
static Vec_Ptr_t * Vec_PtrAllocTruthTables(int nVars)
Definition: vecPtr.h:1065
Mem_FixedStart
Mem_Fixed_t * Mem_FixedStart(int nEntrySize)
FUNCTION DEFINITIONS ///.
Definition: mem.c:100
Gia_ManEraData
static unsigned * Gia_ManEraData(Gia_ManEra_t *p, int i)
Definition: giaEra.c:61
Gia_ManPi
static Gia_Obj_t * Gia_ManPi(Gia_Man_t *p, int v)
Definition: gia.h:405
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Vec_PtrEntryLast
static void * Vec_PtrEntryLast(Vec_Ptr_t *p)
Definition: vecPtr.h:413
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
memcmp
int memcmp()
Gia_ManEra_t_::vStgDump
Vec_Int_t * vStgDump
Definition: giaEra.c:55
Gia_ObjEra_t
typedefABC_NAMESPACE_IMPL_START struct Gia_ObjEra_t_ Gia_ObjEra_t
DECLARATIONS ///.
Definition: giaEra.c:32
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Mem_Fixed_t
typedefABC_NAMESPACE_HEADER_START struct Mem_Fixed_t_ Mem_Fixed_t
DECLARATIONS ///.
Definition: mem.h:33
Gia_ManEraStateHash
int Gia_ManEraStateHash(unsigned *pState, int nWordsSim, int nTableSize)
Definition: giaEra.c:165
Gia_ManInsertState
void Gia_ManInsertState(Gia_ManEra_t *p, Gia_ObjEra_t *pState)
Definition: giaEra.c:270
Gia_ObjEra_t_::pData
unsigned pData[0]
Definition: giaEra.c:39
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Gia_ObjEra_t_::iPrev
int iPrev
Definition: giaEra.c:37
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Gia_ObjEra_t_::iNext
int iNext
Definition: giaEra.c:38
Gia_ManPerformOneIter
void Gia_ManPerformOneIter(Gia_ManEra_t *p)
Definition: giaEra.c:380
Gia_ManEra_t_::pDataSim
unsigned * pDataSim
Definition: giaEra.c:49
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
Gia_ManEraHashResize
void Gia_ManEraHashResize(Gia_ManEra_t *p)
Definition: giaEra.c:229
Gia_ManEra_t_::vStates
Vec_Ptr_t * vStates
Definition: giaEra.c:51
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Gia_ManEra_t_::iCurState
int iCurState
Definition: giaEra.c:53
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Gia_ManEra_t_::pAig
Gia_Man_t * pAig
Definition: giaEra.c:46
Gia_ManEra_t_
Definition: giaEra.c:44
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ManEraState
static Gia_ObjEra_t * Gia_ManEraState(Gia_ManEra_t *p, int i)
Definition: giaEra.c:62
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Gia_ObjFaninId1
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
Mem_FixedEntryFetch
char * Mem_FixedEntryFetch(Mem_Fixed_t *p)
Definition: mem.c:168
Gia_ManEraCreateState
Gia_ObjEra_t * Gia_ManEraCreateState(Gia_ManEra_t *p)
Definition: giaEra.c:143
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387