abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
saigPhase.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [saigPhase.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Sequential AIG package.]
8 
9  Synopsis [Automated phase abstraction.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: saigPhase.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "saig.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 /*
27  The algorithm is described in the paper: Per Bjesse and Jim Kukula,
28  "Automatic Phase Abstraction for Formal Verification", ICCAD 2005
29  http://www.iccad.com/data2/iccad/iccad_05acceptedpapers.nsf/9cfb1ebaaf59043587256a6a00031f78/1701ecf34b149e958725702f00708828?OpenDocument
30 */
31 
32 // the maximum number of cycles of termiry simulation
33 #define TSIM_MAX_ROUNDS 10000
34 #define TSIM_ONE_SERIES 3000
35 
36 #define SAIG_XVS0 1
37 #define SAIG_XVS1 2
38 #define SAIG_XVSX 3
39 
40 static inline int Saig_XsimConvertValue( int v ) { return v == 0? SAIG_XVS0 : (v == 1? SAIG_XVS1 : (v == 2? SAIG_XVSX : -1)); }
41 
42 static inline void Saig_ObjSetXsim( Aig_Obj_t * pObj, int Value ) { pObj->nCuts = Value; }
43 static inline int Saig_ObjGetXsim( Aig_Obj_t * pObj ) { return pObj->nCuts; }
44 static inline int Saig_XsimInv( int Value )
45 {
46  if ( Value == SAIG_XVS0 )
47  return SAIG_XVS1;
48  if ( Value == SAIG_XVS1 )
49  return SAIG_XVS0;
50  assert( Value == SAIG_XVSX );
51  return SAIG_XVSX;
52 }
53 static inline int Saig_XsimAnd( int Value0, int Value1 )
54 {
55  if ( Value0 == SAIG_XVS0 || Value1 == SAIG_XVS0 )
56  return SAIG_XVS0;
57  if ( Value0 == SAIG_XVSX || Value1 == SAIG_XVSX )
58  return SAIG_XVSX;
59  assert( Value0 == SAIG_XVS1 && Value1 == SAIG_XVS1 );
60  return SAIG_XVS1;
61 }
62 static inline int Saig_XsimRand2()
63 {
64  return (Aig_ManRandom(0) & 1) ? SAIG_XVS1 : SAIG_XVS0;
65 }
66 static inline int Saig_XsimRand3()
67 {
68  int RetValue;
69  do {
70  RetValue = Aig_ManRandom(0) & 3;
71  } while ( RetValue == 0 );
72  return RetValue;
73 }
74 static inline int Saig_ObjGetXsimFanin0( Aig_Obj_t * pObj )
75 {
76  int RetValue;
77  RetValue = Saig_ObjGetXsim(Aig_ObjFanin0(pObj));
78  return Aig_ObjFaninC0(pObj)? Saig_XsimInv(RetValue) : RetValue;
79 }
80 static inline int Saig_ObjGetXsimFanin1( Aig_Obj_t * pObj )
81 {
82  int RetValue;
83  RetValue = Saig_ObjGetXsim(Aig_ObjFanin1(pObj));
84  return Aig_ObjFaninC1(pObj)? Saig_XsimInv(RetValue) : RetValue;
85 }
86 static inline void Saig_XsimPrint( FILE * pFile, int Value )
87 {
88  if ( Value == SAIG_XVS0 )
89  {
90  fprintf( pFile, "0" );
91  return;
92  }
93  if ( Value == SAIG_XVS1 )
94  {
95  fprintf( pFile, "1" );
96  return;
97  }
98  assert( Value == SAIG_XVSX );
99  fprintf( pFile, "x" );
100 }
101 
102 // simulation manager
103 typedef struct Saig_Tsim_t_ Saig_Tsim_t;
104 struct Saig_Tsim_t_
105 {
106  Aig_Man_t * pAig; // the original AIG manager
107  int nWords; // the number of words in the states
108  // ternary state representation
109  Vec_Ptr_t * vStates; // the collection of ternary states
110  Aig_MmFixed_t * pMem; // memory for ternary states
111  int nPrefix; // prefix of the ternary state space
112  int nCycle; // cycle of the ternary state space
113  int nNonXRegs; // the number of candidate registers
114  Vec_Int_t * vNonXRegs; // the candidate registers
115  // hash table for terminary states
116  unsigned ** pBins;
117  int nBins;
118 };
119 
120 static inline unsigned * Saig_TsiNext( unsigned * pState, int nWords ) { return *((unsigned **)(pState + nWords)); }
121 static inline void Saig_TsiSetNext( unsigned * pState, int nWords, unsigned * pNext ) { *((unsigned **)(pState + nWords)) = pNext; }
122 
123 ////////////////////////////////////////////////////////////////////////
124 /// DECLARATIONS ///
125 ////////////////////////////////////////////////////////////////////////
126 
127 ////////////////////////////////////////////////////////////////////////
128 /// FUNCTION DEFINITIONS ///
129 ////////////////////////////////////////////////////////////////////////
130 
131 /**Function*************************************************************
132 
133  Synopsis [Allocates simulation manager.]
134 
135  Description []
136 
137  SideEffects []
138 
139  SeeAlso []
140 
141 ***********************************************************************/
142 Saig_Tsim_t * Saig_TsiStart( Aig_Man_t * pAig )
143 {
144  Saig_Tsim_t * p;
145  p = (Saig_Tsim_t *)ABC_ALLOC( char, sizeof(Saig_Tsim_t) );
146  memset( p, 0, sizeof(Saig_Tsim_t) );
147  p->pAig = pAig;
148  p->nWords = Abc_BitWordNum( 2*Aig_ManRegNum(pAig) );
149  p->vStates = Vec_PtrAlloc( 1000 );
150  p->pMem = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 );
151  p->nBins = Abc_PrimeCudd(TSIM_MAX_ROUNDS/2);
152  p->pBins = ABC_ALLOC( unsigned *, p->nBins );
153  memset( p->pBins, 0, sizeof(unsigned *) * p->nBins );
154  return p;
155 }
156 
157 /**Function*************************************************************
158 
159  Synopsis [Deallocates simulation manager.]
160 
161  Description []
162 
163  SideEffects []
164 
165  SeeAlso []
166 
167 ***********************************************************************/
168 void Saig_TsiStop( Saig_Tsim_t * p )
169 {
170  if ( p->vNonXRegs )
171  Vec_IntFree( p->vNonXRegs );
172  Aig_MmFixedStop( p->pMem, 0 );
173  Vec_PtrFree( p->vStates );
174  ABC_FREE( p->pBins );
175  ABC_FREE( p );
176 }
177 
178 /**Function*************************************************************
179 
180  Synopsis [Computes hash value of the node using its simulation info.]
181 
182  Description []
183 
184  SideEffects []
185 
186  SeeAlso []
187 
188 ***********************************************************************/
189 int Saig_TsiStateHash( unsigned * pState, int nWords, int nTableSize )
190 {
191  static int s_FPrimes[128] = {
192  1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
193  1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
194  2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
195  2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
196  3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
197  3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
198  4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
199  4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
200  5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
201  6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
202  6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
203  7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
204  8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
205  };
206  unsigned uHash;
207  int i;
208  uHash = 0;
209  for ( i = 0; i < nWords; i++ )
210  uHash ^= pState[i] * s_FPrimes[i & 0x7F];
211  return uHash % nTableSize;
212 }
213 
214 /**Function*************************************************************
215 
216  Synopsis [Count non-X-valued registers in the simulation data.]
217 
218  Description []
219 
220  SideEffects []
221 
222  SeeAlso []
223 
224 ***********************************************************************/
225 int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nPref )
226 {
227  unsigned * pState;
228  int nRegs = p->pAig->nRegs;
229  int Value, i, k;
230  assert( p->vNonXRegs == NULL );
231  p->vNonXRegs = Vec_IntAlloc( 10 );
232  for ( i = 0; i < nRegs; i++ )
233  {
234  Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, k, nPref )
235  {
236  Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
237  assert( Value != 0 );
238  if ( Value == SAIG_XVSX )
239  break;
240  }
241  if ( k == Vec_PtrSize(p->vStates) )
242  Vec_IntPush( p->vNonXRegs, i );
243  }
244  return Vec_IntSize(p->vNonXRegs);
245 }
246 
247 /**Function*************************************************************
248 
249  Synopsis [Computes flops that are stuck-at constant.]
250 
251  Description []
252 
253  SideEffects []
254 
255  SeeAlso []
256 
257 ***********************************************************************/
258 Vec_Int_t * Saig_TsiComputeTransient( Saig_Tsim_t * p, int nPref )
259 {
260  Vec_Int_t * vCounters;
261  unsigned * pState;
262  int ValueThis = -1, ValuePrev = -1, StepPrev = -1;
263  int i, k, nRegs = p->pAig->nRegs;
264  vCounters = Vec_IntStart( nPref );
265  for ( i = 0; i < nRegs; i++ )
266  {
267  Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k )
268  {
269  ValueThis = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
270 //printf( "%s", (ValueThis == 1)? "0" : ((ValueThis == 2)? "1" : "x") );
271  assert( ValueThis != 0 );
272  if ( ValuePrev != ValueThis )
273  {
274  ValuePrev = ValueThis;
275  StepPrev = k;
276  }
277  }
278 //printf( "\n" );
279  if ( ValueThis == SAIG_XVSX )
280  continue;
281  if ( StepPrev >= nPref )
282  continue;
283  Vec_IntAddToEntry( vCounters, StepPrev, 1 );
284  }
285  Vec_IntForEachEntry( vCounters, ValueThis, i )
286  {
287  if ( ValueThis == 0 )
288  continue;
289 // printf( "%3d : %3d\n", i, ValueThis );
290  }
291  return vCounters;
292 }
293 
294 /**Function*************************************************************
295 
296  Synopsis [Count non-X-valued registers in the simulation data.]
297 
298  Description []
299 
300  SideEffects []
301 
302  SeeAlso []
303 
304 ***********************************************************************/
305 void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix, int nLoop )
306 {
307  unsigned * pState;
308  int nRegs = p->pAig->nRegs;
309  int Value, i, k, Counter = 0;
310  printf( "Ternary traces for each flop:\n" );
311  printf( " : " );
312  for ( i = 0; i < Vec_PtrSize(p->vStates) - nLoop - 1; i++ )
313  printf( "%d", i%10 );
314  printf( " " );
315  for ( i = 0; i < nLoop; i++ )
316  printf( "%d", i%10 );
317  printf( "\n" );
318  for ( i = 0; i < nRegs; i++ )
319  {
320 /*
321  Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k )
322  {
323  Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
324  if ( Value == SAIG_XVSX )
325  break;
326  }
327  if ( k == Vec_PtrSize(p->vStates) )
328  Counter++;
329  else
330  continue;
331 */
332 
333  // print trace
334 // printf( "%5d : %5d %5d ", Counter, i, Saig_ManLo(p->pAig, i)->Id );
335  printf( "%5d : ", Counter++ );
336  Vec_PtrForEachEntryStop( unsigned *, p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 )
337  {
338  Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
339  if ( Value == SAIG_XVS0 )
340  printf( "0" );
341  else if ( Value == SAIG_XVS1 )
342  printf( "1" );
343  else if ( Value == SAIG_XVSX )
344  printf( "x" );
345  else
346  assert( 0 );
347  if ( k == nPrefix - 1 )
348  printf( " " );
349  }
350  printf( "\n" );
351  }
352 }
353 
354 /**Function*************************************************************
355 
356  Synopsis [Returns the number of the state.]
357 
358  Description []
359 
360  SideEffects []
361 
362  SeeAlso []
363 
364 ***********************************************************************/
365 int Saig_TsiComputePrefix( Saig_Tsim_t * p, unsigned * pState, int nWords )
366 {
367  unsigned * pEntry, * pPrev;
368  int Hash, i;
369  Hash = Saig_TsiStateHash( pState, nWords, p->nBins );
370  for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Saig_TsiNext(pEntry, nWords) )
371  if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
372  {
373  Vec_PtrForEachEntry( unsigned *, p->vStates, pPrev, i )
374  {
375  if ( pPrev == pEntry )
376  return i;
377  }
378  assert( 0 );
379  return -1;
380  }
381  return -1;
382 }
383 
384 /**Function*************************************************************
385 
386  Synopsis [Checks if the value exists in the table.]
387 
388  Description []
389 
390  SideEffects []
391 
392  SeeAlso []
393 
394 ***********************************************************************/
395 int Saig_TsiStateLookup( Saig_Tsim_t * p, unsigned * pState, int nWords )
396 {
397  unsigned * pEntry;
398  int Hash;
399  Hash = Saig_TsiStateHash( pState, nWords, p->nBins );
400  for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Saig_TsiNext(pEntry, nWords) )
401  if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
402  return 1;
403  return 0;
404 }
405 
406 /**Function*************************************************************
407 
408  Synopsis [Inserts value into the table.]
409 
410  Description []
411 
412  SideEffects []
413 
414  SeeAlso []
415 
416 ***********************************************************************/
417 void Saig_TsiStateInsert( Saig_Tsim_t * p, unsigned * pState, int nWords )
418 {
419  int Hash = Saig_TsiStateHash( pState, nWords, p->nBins );
420  assert( !Saig_TsiStateLookup( p, pState, nWords ) );
421  Saig_TsiSetNext( pState, nWords, p->pBins[Hash] );
422  p->pBins[Hash] = pState;
423 }
424 
425 /**Function*************************************************************
426 
427  Synopsis [Inserts value into the table.]
428 
429  Description []
430 
431  SideEffects []
432 
433  SeeAlso []
434 
435 ***********************************************************************/
436 unsigned * Saig_TsiStateNew( Saig_Tsim_t * p )
437 {
438  unsigned * pState;
439  pState = (unsigned *)Aig_MmFixedEntryFetch( p->pMem );
440  memset( pState, 0, sizeof(unsigned) * p->nWords );
441  Vec_PtrPush( p->vStates, pState );
442  return pState;
443 }
444 
445 /**Function*************************************************************
446 
447  Synopsis [Inserts value into the table.]
448 
449  Description []
450 
451  SideEffects []
452 
453  SeeAlso []
454 
455 ***********************************************************************/
456 void Saig_TsiStatePrint( Saig_Tsim_t * p, unsigned * pState )
457 {
458  int i, Value, nZeros = 0, nOnes = 0, nDcs = 0;
459  for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
460  {
461  Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
462  if ( Value == SAIG_XVS0 )
463  printf( "0" ), nZeros++;
464  else if ( Value == SAIG_XVS1 )
465  printf( "1" ), nOnes++;
466  else if ( Value == SAIG_XVSX )
467  printf( "x" ), nDcs++;
468  else
469  assert( 0 );
470  }
471  printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs );
472 }
473 
474 /**Function*************************************************************
475 
476  Synopsis [Count constant values in the state.]
477 
478  Description []
479 
480  SideEffects []
481 
482  SeeAlso []
483 
484 ***********************************************************************/
485 int Saig_TsiStateCount( Saig_Tsim_t * p, unsigned * pState )
486 {
487  Aig_Obj_t * pObjLi, * pObjLo;
488  int i, Value, nCounter = 0;
489  Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
490  {
491  Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
492  nCounter += (Value == SAIG_XVS0 || Value == SAIG_XVS1);
493  }
494  return nCounter;
495 }
496 
497 /**Function*************************************************************
498 
499  Synopsis [Count constant values in the state.]
500 
501  Description []
502 
503  SideEffects []
504 
505  SeeAlso []
506 
507 ***********************************************************************/
508 void Saig_TsiStateOrAll( Saig_Tsim_t * pTsi, unsigned * pState )
509 {
510  unsigned * pPrev;
511  int i, k;
512  Vec_PtrForEachEntry( unsigned *, pTsi->vStates, pPrev, i )
513  {
514  for ( k = 0; k < pTsi->nWords; k++ )
515  pState[k] |= pPrev[k];
516  }
517 }
518 
519 /**Function*************************************************************
520 
521  Synopsis [Cycles the circuit to create a new initial state.]
522 
523  Description [Simulates the circuit with random input for the given
524  number of timeframes to get a better initial state.]
525 
526  SideEffects []
527 
528  SeeAlso []
529 
530 ***********************************************************************/
531 Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits, int fVerbose )
532 {
533  Saig_Tsim_t * pTsi;
534  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
535  unsigned * pState;
536  int i, f, Value, nCounter;
537  // allocate the simulation manager
538  pTsi = Saig_TsiStart( p );
539  // initialize the values
540  Saig_ObjSetXsim( Aig_ManConst1(p), SAIG_XVS1 );
541  Saig_ManForEachPi( p, pObj, i )
542  Saig_ObjSetXsim( pObj, SAIG_XVSX );
543  if ( vInits )
544  {
545  Saig_ManForEachLo( p, pObj, i )
546  Saig_ObjSetXsim( pObj, Saig_XsimConvertValue(Vec_IntEntry(vInits, i)) );
547  }
548  else
549  {
550  Saig_ManForEachLo( p, pObj, i )
551  Saig_ObjSetXsim( pObj, SAIG_XVS0 );
552  }
553  // simulate for the given number of timeframes
554  for ( f = 0; f < TSIM_MAX_ROUNDS; f++ )
555  {
556  // collect this state
557  pState = Saig_TsiStateNew( pTsi );
558  Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
559  {
560  Value = Saig_ObjGetXsim(pObjLo);
561  if ( Value & 1 )
562  Abc_InfoSetBit( pState, 2 * i );
563  if ( Value & 2 )
564  Abc_InfoSetBit( pState, 2 * i + 1 );
565  }
566 // printf( "%d ", Saig_TsiStateCount(pTsi, pState) );
567 // Saig_TsiStatePrint( pTsi, pState );
568  // check if this state exists
569  if ( Saig_TsiStateLookup( pTsi, pState, pTsi->nWords ) )
570  {
571  if ( fVerbose )
572  printf( "Ternary simulation converged after %d iterations.\n", f );
573  return pTsi;
574  }
575  // insert this state
576  Saig_TsiStateInsert( pTsi, pState, pTsi->nWords );
577  // simulate internal nodes
578  Aig_ManForEachNode( p, pObj, i )
579  Saig_ObjSetXsim( pObj, Saig_XsimAnd(Saig_ObjGetXsimFanin0(pObj), Saig_ObjGetXsimFanin1(pObj)) );
580  // transfer the latch values
581  Saig_ManForEachLi( p, pObj, i )
582  Saig_ObjSetXsim( pObj, Saig_ObjGetXsimFanin0(pObj) );
583  nCounter = 0;
584  Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
585  {
586  if ( f < TSIM_ONE_SERIES )
587  Saig_ObjSetXsim( pObjLo, Saig_ObjGetXsim(pObjLi) );
588  else
589  {
590  if ( Saig_ObjGetXsim(pObjLi) != Saig_ObjGetXsim(pObjLo) )
591  Saig_ObjSetXsim( pObjLo, SAIG_XVSX );
592  }
593  nCounter += (Saig_ObjGetXsim(pObjLo) == SAIG_XVS0);
594  }
595  }
596  printf( "Saig_ManReachableTernary(): Did not reach a fixed point after %d iterations (not a bug).\n", TSIM_MAX_ROUNDS );
597  Saig_TsiStop( pTsi );
598  return NULL;
599 }
600 
601 /**Function*************************************************************
602 
603  Synopsis [Analize initial value of the selected register.]
604 
605  Description []
606 
607  SideEffects []
608 
609  SeeAlso []
610 
611 ***********************************************************************/
612 void Saig_ManAnalizeControl( Aig_Man_t * p, int Reg )
613 {
614  Aig_Obj_t * pObj, * pReg, * pCtrl, * pAnd;
615  int i;
616  pReg = Saig_ManLo( p, Reg );
617  pCtrl = Saig_ManLo( p, Saig_ManRegNum(p)-1 );
618  assert( pReg->Id < pCtrl->Id );
619  // find a node pointing to both
620  pAnd = NULL;
621  Aig_ManForEachNode( p, pObj, i )
622  {
623  if ( Aig_ObjFanin0(pObj) == pReg && Aig_ObjFanin1(pObj) == pCtrl )
624  {
625  pAnd = pObj;
626  break;
627  }
628  }
629  if ( pAnd == NULL )
630  {
631  printf( "Register is not found.\n" );
632  return;
633  }
634  printf( "Clock-like register: \n" );
635  Aig_ObjPrint( p, pReg );
636  printf( "\n" );
637  printf( "Control register: \n" );
638  Aig_ObjPrint( p, pCtrl );
639  printf( "\n" );
640  printf( "Their fanout: \n" );
641  Aig_ObjPrint( p, pAnd );
642  printf( "\n" );
643 
644  // find the fanouts of pAnd
645  printf( "Fanouts of the fanout: \n" );
646  Aig_ManForEachObj( p, pObj, i )
647  if ( Aig_ObjFanin0(pObj) == pAnd || Aig_ObjFanin1(pObj) == pAnd )
648  {
649  Aig_ObjPrint( p, pObj );
650  printf( "\n" );
651  }
652  printf( "\n" );
653 }
654 
655 /**Function*************************************************************
656 
657  Synopsis [Finds the registers to phase-abstract.]
658 
659  Description []
660 
661  SideEffects []
662 
663  SeeAlso []
664 
665 ***********************************************************************/
666 int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVerbose )
667 {
668  int Values[257] = {0};
669  unsigned * pState;
670  int r, i, k, Reg, Value;
671  int nTests = pTsi->nPrefix + 2 * pTsi->nCycle;
672  assert( nFrames <= 256 );
673  r = 0;
674  Vec_IntForEachEntry( pTsi->vNonXRegs, Reg, i )
675  {
676  for ( k = 0; k < nTests; k++ )
677  {
678  if ( k < pTsi->nPrefix + pTsi->nCycle )
679  pState = (unsigned *)Vec_PtrEntry( pTsi->vStates, k );
680  else
681  pState = (unsigned *)Vec_PtrEntry( pTsi->vStates, k - pTsi->nCycle );
682  Value = (Abc_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * Reg );
683  assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 );
684  if ( k < nFrames || (fIgnore && k == nFrames) )
685  Values[k % nFrames] = Value;
686  else if ( Values[k % nFrames] != Value )
687  break;
688  }
689  if ( k < nTests )
690  continue;
691  // skip stuck at
692  if ( fIgnore )
693  {
694  for ( k = 1; k < nFrames; k++ )
695  if ( Values[k] != Values[0] )
696  break;
697  if ( k == nFrames )
698  continue;
699  }
700  // report useful register
701  Vec_IntWriteEntry( pTsi->vNonXRegs, r++, Reg );
702  if ( fVerbose )
703  {
704  printf( "Register %5d has generator: [", Reg );
705  for ( k = 0; k < nFrames; k++ )
706  Saig_XsimPrint( stdout, Values[k] );
707  printf( "]\n" );
708 
709  if ( fVerbose )
710  Saig_ManAnalizeControl( pTsi->pAig, Reg );
711  }
712  }
713  Vec_IntShrink( pTsi->vNonXRegs, r );
714  if ( fVerbose )
715  printf( "Found %3d useful registers.\n", Vec_IntSize(pTsi->vNonXRegs) );
716  return Vec_IntSize(pTsi->vNonXRegs);
717 }
718 
719 
720 /**Function*************************************************************
721 
722  Synopsis [Mapping of AIG nodes into frames nodes.]
723 
724  Description []
725 
726  SideEffects []
727 
728  SeeAlso []
729 
730 ***********************************************************************/
731 static inline Aig_Obj_t * Saig_ObjFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return pObjMap[nFs*pObj->Id + i]; }
732 static inline void Saig_ObjSetFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { pObjMap[nFs*pObj->Id + i] = pNode; }
733 
734 static inline Aig_Obj_t * Saig_ObjChild0Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin0(pObj)? Aig_NotCond(Saig_ObjFrames(pObjMap,nFs,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
735 static inline Aig_Obj_t * Saig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin1(pObj)? Aig_NotCond(Saig_ObjFrames(pObjMap,nFs,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
736 
737 /**Function*************************************************************
738 
739  Synopsis [Performs phase abstraction by unrolling the circuit.]
740 
741  Description []
742 
743  SideEffects []
744 
745  SeeAlso []
746 
747 ***********************************************************************/
748 Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVerbose )
749 {
750  Aig_Man_t * pFrames, * pAig = pTsi->pAig;
751  Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
752  Aig_Obj_t ** pObjMap;
753  unsigned * pState;
754  int i, f, Reg, Value;
755 
756  assert( Vec_IntSize(pTsi->vNonXRegs) > 0 );
757 
758  // create mapping for the frames nodes
759  pObjMap = ABC_ALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
760  memset( pObjMap, 0, sizeof(Aig_Obj_t *) * nFrames * Aig_ManObjNumMax(pAig) );
761 
762  // start the fraig package
763  pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
764  pFrames->pName = Abc_UtilStrsav( pAig->pName );
765  pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
766  // map constant nodes
767  for ( f = 0; f < nFrames; f++ )
768  Saig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
769  // create PI nodes for the frames
770  for ( f = 0; f < nFrames; f++ )
771  Aig_ManForEachPiSeq( pAig, pObj, i )
772  Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) );
773  // create the latches
774  Aig_ManForEachLoSeq( pAig, pObj, i )
775  Saig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) );
776 
777  // add timeframes
778  for ( f = 0; f < nFrames; f++ )
779  {
780  // replace abstracted registers by constants
781  Vec_IntForEachEntry( pTsi->vNonXRegs, Reg, i )
782  {
783  pObj = Saig_ManLo( pAig, Reg );
784  pState = (unsigned *)Vec_PtrEntry( pTsi->vStates, f );
785  Value = (Abc_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * Reg );
786  assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 );
787  pObjNew = (Value == SAIG_XVS1)? Aig_ManConst1(pFrames) : Aig_ManConst0(pFrames);
788  Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
789  }
790  // add internal nodes of this frame
791  Aig_ManForEachNode( pAig, pObj, i )
792  {
793  pObjNew = Aig_And( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Saig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
794  Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
795  }
796  // set the latch inputs and copy them into the latch outputs of the next frame
797  Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
798  {
799  pObjNew = Saig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
800  if ( f < nFrames - 1 )
801  Saig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
802  }
803  }
804  for ( f = 0; f < nFrames; f++ )
805  {
806  Aig_ManForEachPoSeq( pAig, pObj, i )
807  {
808  pObjNew = Aig_ObjCreateCo( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,f) );
809  Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
810  }
811  }
812  pFrames->nRegs = pAig->nRegs;
813  pFrames->nTruePis = Aig_ManCiNum(pFrames) - Aig_ManRegNum(pFrames);
814  pFrames->nTruePos = Aig_ManCoNum(pFrames) - Aig_ManRegNum(pFrames);
815  Aig_ManForEachLiSeq( pAig, pObj, i )
816  {
817  pObjNew = Aig_ObjCreateCo( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,nFrames-1) );
818  Saig_ObjSetFrames( pObjMap, nFrames, pObj, nFrames-1, pObjNew );
819  }
820 //Aig_ManPrintStats( pFrames );
821  Aig_ManSeqCleanup( pFrames );
822 //Aig_ManPrintStats( pFrames );
823 // Aig_ManCiCleanup( pFrames );
824 //Aig_ManPrintStats( pFrames );
825  ABC_FREE( pObjMap );
826  return pFrames;
827 }
828 
829 
830 /**Function*************************************************************
831 
832  Synopsis [Performs automated phase abstraction.]
833 
834  Description [Takes the AIG manager and the array of initial states.]
835 
836  SideEffects []
837 
838  SeeAlso []
839 
840 ***********************************************************************/
841 int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits )
842 {
843  Saig_Tsim_t * pTsi;
844  int nFrames, nPrefix;
845  assert( Saig_ManRegNum(p) );
846  assert( Saig_ManPiNum(p) );
847  assert( Saig_ManPoNum(p) );
848  // perform terminary simulation
849  pTsi = Saig_ManReachableTernary( p, vInits, 0 );
850  if ( pTsi == NULL )
851  return 1;
852  // derive information
853  nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
854  nFrames = Vec_PtrSize(pTsi->vStates) - 1 - nPrefix;
855  Saig_TsiStop( pTsi );
856  // potentially, may need to reduce nFrames if nPrefix is less than nFrames
857  return nFrames;
858 }
859 
860 /**Function*************************************************************
861 
862  Synopsis [Performs automated phase abstraction.]
863 
864  Description [Takes the AIG manager and the array of initial states.]
865 
866  SideEffects []
867 
868  SeeAlso []
869 
870 ***********************************************************************/
871 int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose, Vec_Int_t ** pvTrans )
872 {
873  Saig_Tsim_t * pTsi;
874  int nFrames, nPrefix, nNonXRegs;
875  assert( Saig_ManRegNum(p) );
876  assert( Saig_ManPiNum(p) );
877  assert( Saig_ManPoNum(p) );
878  // perform terminary simulation
879  pTsi = Saig_ManReachableTernary( p, NULL, 0 );
880  if ( pTsi == NULL )
881  return 0;
882  // derive information
883  nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
884  nFrames = Vec_PtrSize(pTsi->vStates) - 1 - nPrefix;
885  nNonXRegs = Saig_TsiCountNonXValuedRegisters( pTsi, nPrefix );
886 
887  if ( pvTrans )
888  *pvTrans = Saig_TsiComputeTransient( pTsi, nPrefix );
889 
890  // print statistics
891  if ( fVerbose )
892  printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n", nPrefix, nFrames, p->nRegs, nNonXRegs );
893  if ( fVeryVerbose )
894  Saig_TsiPrintTraces( pTsi, pTsi->nWords, nPrefix, nFrames );
895  Saig_TsiStop( pTsi );
896  // potentially, may need to reduce nFrames if nPrefix is less than nFrames
897  return nPrefix;
898 }
899 
900 /**Function*************************************************************
901 
902  Synopsis [Performs automated phase abstraction.]
903 
904  Description [Takes the AIG manager and the array of initial states.]
905 
906  SideEffects []
907 
908  SeeAlso []
909 
910 ***********************************************************************/
911 Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose )
912 {
913  Aig_Man_t * pNew = NULL;
914  Saig_Tsim_t * pTsi;
915  assert( Saig_ManRegNum(p) );
916  assert( Saig_ManPiNum(p) );
917  assert( Saig_ManPoNum(p) );
918  // perform terminary simulation
919  pTsi = Saig_ManReachableTernary( p, vInits, fVerbose );
920  if ( pTsi == NULL )
921  return NULL;
922  // derive information
923  pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
924  pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
925  pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, Abc_MinInt(pTsi->nPrefix,nPref));
926  // print statistics
927  if ( fVerbose )
928  {
929  printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n",
930  pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
931  if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 )
932  Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle );
933  }
934  if ( fPrint )
935  printf( "Print-out finished. Phase assignment is not performed.\n" );
936  else if ( nFrames < 2 )
937  printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
938  else if ( nFrames > 256 )
939  printf( "The number of frames is more than 256. Phase assignment is not performed.\n" );
940  else if ( pTsi->nCycle == 1 )
941  printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
942  else if ( pTsi->nCycle % nFrames != 0 )
943  printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames );
944  else if ( pTsi->nNonXRegs == 0 )
945  printf( "All registers have X-valued states. Phase abstraction cannot be done.\n" );
946  else if ( !Saig_ManFindRegisters( pTsi, nFrames, fIgnore, fVerbose ) )
947  printf( "There is no registers to abstract with %d frames.\n", nFrames );
948  else
949  pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
950  Saig_TsiStop( pTsi );
951  return pNew;
952 }
953 
954 /**Function*************************************************************
955 
956  Synopsis [Performs automated phase abstraction.]
957 
958  Description [Takes the AIG manager and the array of initial states.]
959 
960  SideEffects []
961 
962  SeeAlso []
963 
964 ***********************************************************************/
965 Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
966 {
967  Aig_Man_t * pNew = NULL;
968  Saig_Tsim_t * pTsi;
969  int fPrint = 0;
970  int nFrames;
971  assert( Saig_ManRegNum(p) );
972  assert( Saig_ManPiNum(p) );
973  assert( Saig_ManPoNum(p) );
974  // perform terminary simulation
975  pTsi = Saig_ManReachableTernary( p, NULL, fVerbose );
976  if ( pTsi == NULL )
977  return NULL;
978  // derive information
979  pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
980  pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
981  pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, 0);
982  // print statistics
983  if ( fVerbose )
984  {
985  printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n",
986  pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
987  if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 )
988  Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle );
989  }
990  nFrames = pTsi->nCycle;
991  if ( fPrint )
992  {
993  printf( "Print-out finished. Phase assignment is not performed.\n" );
994  }
995  else if ( nFrames < 2 )
996  {
997 // printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
998  }
999  else if ( nFrames > 256 )
1000  {
1001 // printf( "The number of frames is more than 256. Phase assignment is not performed.\n" );
1002  }
1003  else if ( pTsi->nCycle == 1 )
1004  {
1005 // printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
1006  }
1007  else if ( pTsi->nCycle % nFrames != 0 )
1008  {
1009 // printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames );
1010  }
1011  else if ( pTsi->nNonXRegs == 0 )
1012  {
1013 // printf( "All registers have X-valued states. Phase abstraction cannot be done.\n" );
1014  }
1015  else if ( !Saig_ManFindRegisters( pTsi, nFrames, 0, fVerbose ) )
1016  {
1017 // printf( "There is no registers to abstract with %d frames.\n", nFrames );
1018  }
1019  else
1020  pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
1021  Saig_TsiStop( pTsi );
1022  if ( pNew == NULL )
1023  pNew = Aig_ManDupSimple( p );
1024  if ( Aig_ManCiNum(pNew) == Aig_ManRegNum(pNew) )
1025  {
1026  Aig_ManStop( pNew);
1027  pNew = Aig_ManDupSimple( p );
1028  }
1029  return pNew;
1030 }
1031 
1032 
1033 /**Function*************************************************************
1034 
1035  Synopsis [Derives CEX for the original AIG from CEX of the unrolled AIG.]
1036 
1037  Description [The number of PIs of the given CEX should divide by the number
1038  of PIs of the original AIG without a remainder.]
1039 
1040  SideEffects []
1041 
1042  SeeAlso []
1043 
1044 ***********************************************************************/
1045 Abc_Cex_t * Saig_PhaseTranslateCex( Aig_Man_t * p, Abc_Cex_t * pCex )
1046 {
1047  Abc_Cex_t * pNew;
1048  int i, k, iFrame, nFrames;
1049  // make sure the PI count of the AIG is a multiple of the PI count of the CEX
1050  // if this is not true, the CEX is not derived as the result of unrolling of pAig
1051  // or the unrolled CEX went through transformations that change the PI count
1052  if ( pCex->nPis % Saig_ManPiNum(p) != 0 )
1053  {
1054  printf( "The PI count in the AIG and in the CEX do not match.\n" );
1055  return NULL;
1056  }
1057  // get the number of unrolled frames
1058  nFrames = pCex->nPis / Saig_ManPiNum(p);
1059  // get the frame where it fails
1060  iFrame = pCex->iFrame * nFrames + pCex->iPo / Saig_ManPoNum(p);
1061  // start a new CEX (assigns: p->nRegs, p->nPis, p->nBits)
1062  pNew = Abc_CexAlloc( Saig_ManRegNum(p), Saig_ManPiNum(p), iFrame+1 );
1063  assert( pNew->nBits == pNew->nPis * (iFrame + 1) + pNew->nRegs );
1064  // now assign the failed frame and the failed PO (p->iFrame and p->iPo)
1065  pNew->iFrame = iFrame;
1066  pNew->iPo = pCex->iPo % Saig_ManPoNum(p);
1067  // copy the bit data
1068  for ( i = pCex->nRegs, k = pNew->nRegs; k < pNew->nBits; k++, i++ )
1069  if ( Abc_InfoHasBit( pCex->pData, i ) )
1070  Abc_InfoSetBit( pNew->pData, k );
1071  assert( i <= pCex->nBits );
1072  return pNew;
1073 }
1074 
1075 ////////////////////////////////////////////////////////////////////////
1076 /// END OF FILE ///
1077 ////////////////////////////////////////////////////////////////////////
1078 
1079 
1080 ABC_NAMESPACE_IMPL_END
1081 
memset
char * memset()
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Saig_XsimRand2
static int Saig_XsimRand2()
Definition: saigPhase.c:62
Saig_Tsim_t_::pAig
Aig_Man_t * pAig
Definition: saigPhase.c:106
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
Saig_TsiStateHash
int Saig_TsiStateHash(unsigned *pState, int nWords, int nTableSize)
Definition: saigPhase.c:189
Saig_TsiNext
static unsigned * Saig_TsiNext(unsigned *pState, int nWords)
Definition: saigPhase.c:120
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition: vecPtr.h:57
Saig_TsiSetNext
static void Saig_TsiSetNext(unsigned *pState, int nWords, unsigned *pNext)
Definition: saigPhase.c:121
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Saig_TsiCountNonXValuedRegisters
int Saig_TsiCountNonXValuedRegisters(Saig_Tsim_t *p, int nPref)
Definition: saigPhase.c:225
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Saig_ManPhasePrefixLength
int Saig_ManPhasePrefixLength(Aig_Man_t *p, int fVerbose, int fVeryVerbose, Vec_Int_t **pvTrans)
Definition: saigPhase.c:871
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
Aig_ManSeqCleanup
int Aig_ManSeqCleanup(Aig_Man_t *p)
Definition: aigScl.c:158
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Saig_ManLo
static Aig_Obj_t * Saig_ManLo(Aig_Man_t *p, int i)
Definition: saig.h:79
Saig_Tsim_t_::nWords
int nWords
Definition: saigPhase.c:107
Aig_MmFixedStop
void Aig_MmFixedStop(Aig_MmFixed_t *p, int fVerbose)
Definition: aigMem.c:132
Saig_ObjSetFrames
static void Saig_ObjSetFrames(Aig_Obj_t **pObjMap, int nFs, Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
Definition: saigPhase.c:732
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Saig_TsiStateLookup
int Saig_TsiStateLookup(Saig_Tsim_t *p, unsigned *pState, int nWords)
Definition: saigPhase.c:395
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_ManConst0
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
Saig_TsiStateInsert
void Saig_TsiStateInsert(Saig_Tsim_t *p, unsigned *pState, int nWords)
Definition: saigPhase.c:417
Saig_PhaseTranslateCex
Abc_Cex_t * Saig_PhaseTranslateCex(Aig_Man_t *p, Abc_Cex_t *pCex)
Definition: saigPhase.c:1045
Saig_ObjChild0Frames
static Aig_Obj_t * Saig_ObjChild0Frames(Aig_Obj_t **pObjMap, int nFs, Aig_Obj_t *pObj, int i)
Definition: saigPhase.c:734
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Aig_MmFixedStart
Aig_MmFixed_t * Aig_MmFixedStart(int nEntrySize, int nEntriesMax)
FUNCTION DEFINITIONS ///.
Definition: aigMem.c:96
Saig_TsiStateOrAll
void Saig_TsiStateOrAll(Saig_Tsim_t *pTsi, unsigned *pState)
Definition: saigPhase.c:508
nWords
int nWords
Definition: abcNpn.c:127
Saig_Tsim_t_::vNonXRegs
Vec_Int_t * vNonXRegs
Definition: saigPhase.c:114
Saig_XsimAnd
static int Saig_XsimAnd(int Value0, int Value1)
Definition: saigPhase.c:53
Saig_TsiStart
Saig_Tsim_t * Saig_TsiStart(Aig_Man_t *pAig)
DECLARATIONS ///.
Definition: saigPhase.c:142
Saig_Tsim_t_::nPrefix
int nPrefix
Definition: saigPhase.c:111
Aig_MmFixed_t_
DECLARATIONS ///.
Definition: aigMem.c:30
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_ObjPrint
void Aig_ObjPrint(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aigObj.c:316
SAIG_XVS1
#define SAIG_XVS1
Definition: saigPhase.c:37
Saig_ManPhaseFrameNum
int Saig_ManPhaseFrameNum(Aig_Man_t *p, Vec_Int_t *vInits)
Definition: saigPhase.c:841
Saig_ManPhaseAbstract
Aig_Man_t * Saig_ManPhaseAbstract(Aig_Man_t *p, Vec_Int_t *vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose)
Definition: saigPhase.c:911
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Saig_ManPerformAbstraction
Aig_Man_t * Saig_ManPerformAbstraction(Saig_Tsim_t *pTsi, int nFrames, int fVerbose)
Definition: saigPhase.c:748
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Saig_TsiComputePrefix
int Saig_TsiComputePrefix(Saig_Tsim_t *p, unsigned *pState, int nWords)
Definition: saigPhase.c:365
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
SAIG_XVSX
#define SAIG_XVSX
Definition: saigPhase.c:38
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Saig_TsiComputeTransient
Vec_Int_t * Saig_TsiComputeTransient(Saig_Tsim_t *p, int nPref)
Definition: saigPhase.c:258
Vec_IntAddToEntry
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
Aig_ManForEachLiLoSeq
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition: aig.h:450
Saig_TsiPrintTraces
void Saig_TsiPrintTraces(Saig_Tsim_t *p, int nWords, int nPrefix, int nLoop)
Definition: saigPhase.c:305
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Saig_TsiStateCount
int Saig_TsiStateCount(Saig_Tsim_t *p, unsigned *pState)
Definition: saigPhase.c:485
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
memcmp
int memcmp()
Saig_ObjGetXsimFanin1
static int Saig_ObjGetXsimFanin1(Aig_Obj_t *pObj)
Definition: saigPhase.c:80
SAIG_XVS0
#define SAIG_XVS0
Definition: saigPhase.c:36
Aig_MmFixedEntryFetch
char * Aig_MmFixedEntryFetch(Aig_MmFixed_t *p)
Definition: aigMem.c:161
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Counter
static int Counter
Definition: extraBddMisc.c:1877
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Saig_TsiStateNew
unsigned * Saig_TsiStateNew(Saig_Tsim_t *p)
Definition: saigPhase.c:436
Saig_ObjGetXsimFanin0
static int Saig_ObjGetXsimFanin0(Aig_Obj_t *pObj)
Definition: saigPhase.c:74
Saig_XsimInv
static int Saig_XsimInv(int Value)
Definition: saigPhase.c:44
Saig_ObjSetXsim
static void Saig_ObjSetXsim(Aig_Obj_t *pObj, int Value)
Definition: saigPhase.c:42
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Saig_ManRegNum
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Saig_ManReachableTernary
Saig_Tsim_t * Saig_ManReachableTernary(Aig_Man_t *p, Vec_Int_t *vInits, int fVerbose)
Definition: saigPhase.c:531
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
TSIM_ONE_SERIES
#define TSIM_ONE_SERIES
Definition: saigPhase.c:34
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Saig_XsimRand3
static int Saig_XsimRand3()
Definition: saigPhase.c:66
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_PtrForEachEntryStop
#define Vec_PtrForEachEntryStop(Type, vVec, pEntry, i, Stop)
Definition: vecPtr.h:59
Saig_Tsim_t_::pMem
Aig_MmFixed_t * pMem
Definition: saigPhase.c:110
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Saig_Tsim_t_::nNonXRegs
int nNonXRegs
Definition: saigPhase.c:113
Saig_TsiStatePrint
void Saig_TsiStatePrint(Saig_Tsim_t *p, unsigned *pState)
Definition: saigPhase.c:456
Saig_Tsim_t_::pBins
unsigned ** pBins
Definition: saigPhase.c:116
Aig_ManForEachLoSeq
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
Saig_ObjGetXsim
static int Saig_ObjGetXsim(Aig_Obj_t *pObj)
Definition: saigPhase.c:43
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Saig_ObjChild1Frames
static Aig_Obj_t * Saig_ObjChild1Frames(Aig_Obj_t **pObjMap, int nFs, Aig_Obj_t *pObj, int i)
Definition: saigPhase.c:735
Saig_ObjFrames
static Aig_Obj_t * Saig_ObjFrames(Aig_Obj_t **pObjMap, int nFs, Aig_Obj_t *pObj, int i)
Definition: saigPhase.c:731
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ManForEachLiSeq
#define Aig_ManForEachLiSeq(p, pObj, i)
Definition: aig.h:447
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Saig_Tsim_t_::vStates
Vec_Ptr_t * vStates
Definition: saigPhase.c:109
Saig_TsiStop
void Saig_TsiStop(Saig_Tsim_t *p)
Definition: saigPhase.c:168
Saig_Tsim_t_::nBins
int nBins
Definition: saigPhase.c:117
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
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
Aig_ManForEachPoSeq
#define Aig_ManForEachPoSeq(p, pObj, i)
Definition: aig.h:444
Saig_XsimPrint
static void Saig_XsimPrint(FILE *pFile, int Value)
Definition: saigPhase.c:86
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Aig_ManDupSimple
Aig_Man_t * Aig_ManDupSimple(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigDup.c:46
Aig_Obj_t_::nCuts
unsigned nCuts
Definition: aig.h:83
Saig_XsimConvertValue
static int Saig_XsimConvertValue(int v)
Definition: saigPhase.c:40
Saig_Tsim_t_
Definition: saigPhase.c:104
Aig_ManForEachPiSeq
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition: aig.h:438
TSIM_MAX_ROUNDS
#define TSIM_MAX_ROUNDS
Definition: saigPhase.c:33
Saig_ManPhaseAbstractAuto
Aig_Man_t * Saig_ManPhaseAbstractAuto(Aig_Man_t *p, int fVerbose)
Definition: saigPhase.c:965
Saig_ManFindRegisters
int Saig_ManFindRegisters(Saig_Tsim_t *pTsi, int nFrames, int fIgnore, int fVerbose)
Definition: saigPhase.c:666
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Saig_ManAnalizeControl
void Saig_ManAnalizeControl(Aig_Man_t *p, int Reg)
Definition: saigPhase.c:612
Saig_Tsim_t_::nCycle
int nCycle
Definition: saigPhase.c:112
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91