abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaSim2.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [giaSim.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis [Fast sequential simulator.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: giaSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 typedef struct Gia_Sim2_t_ Gia_Sim2_t;
31 struct Gia_Sim2_t_
32 {
33  Gia_Man_t * pAig;
34  Gia_ParSim_t * pPars;
35  int nWords;
36  unsigned * pDataSim;
37  Vec_Int_t * vClassOld;
38  Vec_Int_t * vClassNew;
39 };
40 
41 static inline unsigned * Gia_Sim2Data( Gia_Sim2_t * p, int i ) { return p->pDataSim + i * p->nWords; }
42 
43 extern void Gia_ManResetRandom( Gia_ParSim_t * pPars );
44 
45 ////////////////////////////////////////////////////////////////////////
46 /// FUNCTION DEFINITIONS ///
47 ////////////////////////////////////////////////////////////////////////
48 
49 /**Function*************************************************************
50 
51  Synopsis []
52 
53  Description []
54 
55  SideEffects []
56 
57  SeeAlso []
58 
59 ***********************************************************************/
60 void Gia_Sim2Delete( Gia_Sim2_t * p )
61 {
62  Vec_IntFreeP( &p->vClassOld );
63  Vec_IntFreeP( &p->vClassNew );
64  ABC_FREE( p->pDataSim );
65  ABC_FREE( p );
66 }
67 
68 /**Function*************************************************************
69 
70  Synopsis [Creates fast simulation manager.]
71 
72  Description []
73 
74  SideEffects []
75 
76  SeeAlso []
77 
78 ***********************************************************************/
79 Gia_Sim2_t * Gia_Sim2Create( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
80 {
81  Gia_Sim2_t * p;
82  Gia_Obj_t * pObj;
83  int i;
84  p = ABC_CALLOC( Gia_Sim2_t, 1 );
85  p->pAig = pAig;
86  p->pPars = pPars;
87  p->nWords = pPars->nWords;
88  p->pDataSim = ABC_ALLOC( unsigned, p->nWords * Gia_ManObjNum(p->pAig) );
89  if ( !p->pDataSim )
90  {
91  Abc_Print( 1, "Simulator could not allocate %.2f GB for simulation info.\n",
92  4.0 * p->nWords * Gia_ManObjNum(p->pAig) / (1<<30) );
93  Gia_Sim2Delete( p );
94  return NULL;
95  }
96  p->vClassOld = Vec_IntAlloc( 100 );
97  p->vClassNew = Vec_IntAlloc( 100 );
98  if ( pPars->fVerbose )
99  Abc_Print( 1, "Memory: AIG = %7.2f MB. SimInfo = %7.2f MB.\n",
100  12.0*Gia_ManObjNum(p->pAig)/(1<<20), 4.0*p->nWords*Gia_ManObjNum(p->pAig)/(1<<20) );
101  // prepare AIG
102  Gia_ManSetPhase( pAig );
103  Gia_ManForEachObj( pAig, pObj, i )
104  pObj->Value = i;
105  return p;
106 }
107 
108 /**Function*************************************************************
109 
110  Synopsis []
111 
112  Description []
113 
114  SideEffects []
115 
116  SeeAlso []
117 
118 ***********************************************************************/
119 static inline void Gia_Sim2InfoRandom( Gia_Sim2_t * p, unsigned * pInfo )
120 {
121  int w;
122  for ( w = p->nWords-1; w >= 0; w-- )
123  pInfo[w] = Gia_ManRandom( 0 );
124 }
125 
126 /**Function*************************************************************
127 
128  Synopsis []
129 
130  Description []
131 
132  SideEffects []
133 
134  SeeAlso []
135 
136 ***********************************************************************/
137 static inline void Gia_Sim2InfoZero( Gia_Sim2_t * p, unsigned * pInfo )
138 {
139  int w;
140  for ( w = p->nWords-1; w >= 0; w-- )
141  pInfo[w] = 0;
142 }
143 
144 /**Function*************************************************************
145 
146  Synopsis []
147 
148  Description []
149 
150  SideEffects []
151 
152  SeeAlso []
153 
154 ***********************************************************************/
155 static inline void Gia_Sim2InfoOne( Gia_Sim2_t * p, unsigned * pInfo )
156 {
157  int w;
158  for ( w = p->nWords-1; w >= 0; w-- )
159  pInfo[w] = ~0;
160 }
161 
162 /**Function*************************************************************
163 
164  Synopsis []
165 
166  Description []
167 
168  SideEffects []
169 
170  SeeAlso []
171 
172 ***********************************************************************/
173 static inline void Gia_Sim2InfoCopy( Gia_Sim2_t * p, unsigned * pInfo, unsigned * pInfo0 )
174 {
175  int w;
176  for ( w = p->nWords-1; w >= 0; w-- )
177  pInfo[w] = pInfo0[w];
178 }
179 
180 /**Function*************************************************************
181 
182  Synopsis []
183 
184  Description []
185 
186  SideEffects []
187 
188  SeeAlso []
189 
190 ***********************************************************************/
191 static inline void Gia_Sim2SimulateCo( Gia_Sim2_t * p, Gia_Obj_t * pObj )
192 {
193  unsigned * pInfo = Gia_Sim2Data( p, Gia_ObjValue(pObj) );
194  unsigned * pInfo0 = Gia_Sim2Data( p, Gia_ObjFaninId0(pObj, Gia_ObjValue(pObj)) );
195  int w;
196  if ( Gia_ObjFaninC0(pObj) )
197  for ( w = p->nWords-1; w >= 0; w-- )
198  pInfo[w] = ~pInfo0[w];
199  else
200  for ( w = p->nWords-1; w >= 0; w-- )
201  pInfo[w] = pInfo0[w];
202 }
203 
204 /**Function*************************************************************
205 
206  Synopsis []
207 
208  Description []
209 
210  SideEffects []
211 
212  SeeAlso []
213 
214 ***********************************************************************/
215 static inline void Gia_Sim2SimulateNode( Gia_Sim2_t * p, Gia_Obj_t * pObj )
216 {
217  unsigned * pInfo = Gia_Sim2Data( p, Gia_ObjValue(pObj) );
218  unsigned * pInfo0 = Gia_Sim2Data( p, Gia_ObjFaninId0(pObj, Gia_ObjValue(pObj)) );
219  unsigned * pInfo1 = Gia_Sim2Data( p, Gia_ObjFaninId1(pObj, Gia_ObjValue(pObj)) );
220  int w;
221  if ( Gia_ObjFaninC0(pObj) )
222  {
223  if ( Gia_ObjFaninC1(pObj) )
224  for ( w = p->nWords-1; w >= 0; w-- )
225  pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
226  else
227  for ( w = p->nWords-1; w >= 0; w-- )
228  pInfo[w] = ~pInfo0[w] & pInfo1[w];
229  }
230  else
231  {
232  if ( Gia_ObjFaninC1(pObj) )
233  for ( w = p->nWords-1; w >= 0; w-- )
234  pInfo[w] = pInfo0[w] & ~pInfo1[w];
235  else
236  for ( w = p->nWords-1; w >= 0; w-- )
237  pInfo[w] = pInfo0[w] & pInfo1[w];
238  }
239 }
240 
241 /**Function*************************************************************
242 
243  Synopsis []
244 
245  Description []
246 
247  SideEffects []
248 
249  SeeAlso []
250 
251 ***********************************************************************/
252 static inline void Gia_Sim2InfoTransfer( Gia_Sim2_t * p )
253 {
254  Gia_Obj_t * pObjRo, * pObjRi;
255  unsigned * pInfo0, * pInfo1;
256  int i;
257  Gia_ManForEachRiRo( p->pAig, pObjRi, pObjRo, i )
258  {
259  pInfo0 = Gia_Sim2Data( p, Gia_ObjValue(pObjRo) );
260  pInfo1 = Gia_Sim2Data( p, Gia_ObjValue(pObjRi) );
261  Gia_Sim2InfoCopy( p, pInfo0, pInfo1 );
262  }
263 }
264 
265 /**Function*************************************************************
266 
267  Synopsis []
268 
269  Description []
270 
271  SideEffects []
272 
273  SeeAlso []
274 
275 ***********************************************************************/
276 static inline void Gia_Sim2SimulateRound( Gia_Sim2_t * p )
277 {
278  Gia_Obj_t * pObj;
279  int i;
280  pObj = Gia_ManConst0(p->pAig);
281  assert( Gia_ObjValue(pObj) == 0 );
282  Gia_Sim2InfoZero( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
283  Gia_ManForEachPi( p->pAig, pObj, i )
284  Gia_Sim2InfoRandom( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
285  Gia_ManForEachAnd( p->pAig, pObj, i )
286  {
287  assert( Gia_ObjValue(pObj) == i );
288  Gia_Sim2SimulateNode( p, pObj );
289  }
290  Gia_ManForEachCo( p->pAig, pObj, i )
291  Gia_Sim2SimulateCo( p, pObj );
292 }
293 
294 
295 
296 /**Function*************************************************************
297 
298  Synopsis [Compares simulation info of two nodes.]
299 
300  Description []
301 
302  SideEffects []
303 
304  SeeAlso []
305 
306 ***********************************************************************/
307 int Gia_Sim2CompareEqual( unsigned * p0, unsigned * p1, int nWords, int fCompl )
308 {
309  int w;
310  if ( !fCompl )
311  {
312  for ( w = 0; w < nWords; w++ )
313  if ( p0[w] != p1[w] )
314  return 0;
315  return 1;
316  }
317  else
318  {
319  for ( w = 0; w < nWords; w++ )
320  if ( p0[w] != ~p1[w] )
321  return 0;
322  return 1;
323  }
324 }
325 
326 /**Function*************************************************************
327 
328  Synopsis [Compares simulation info of one node.]
329 
330  Description []
331 
332  SideEffects []
333 
334  SeeAlso []
335 
336 ***********************************************************************/
337 int Gia_Sim2CompareZero( unsigned * p0, int nWords, int fCompl )
338 {
339  int w;
340  if ( !fCompl )
341  {
342  for ( w = 0; w < nWords; w++ )
343  if ( p0[w] != 0 )
344  return 0;
345  return 1;
346  }
347  else
348  {
349  for ( w = 0; w < nWords; w++ )
350  if ( p0[w] != ~0 )
351  return 0;
352  return 1;
353  }
354 }
355 
356 /**Function*************************************************************
357 
358  Synopsis [Creates equivalence class.]
359 
360  Description []
361 
362  SideEffects []
363 
364  SeeAlso []
365 
366 ***********************************************************************/
367 void Gia_Sim2ClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
368 {
369  int Repr = GIA_VOID, EntPrev = -1, Ent, i;
370  assert( Vec_IntSize(vClass) > 0 );
371  Vec_IntForEachEntry( vClass, Ent, i )
372  {
373  if ( i == 0 )
374  {
375  Repr = Ent;
376  Gia_ObjSetRepr( p, Ent, GIA_VOID );
377  EntPrev = Ent;
378  }
379  else
380  {
381  assert( Repr < Ent );
382  Gia_ObjSetRepr( p, Ent, Repr );
383  Gia_ObjSetNext( p, EntPrev, Ent );
384  EntPrev = Ent;
385  }
386  }
387  Gia_ObjSetNext( p, EntPrev, 0 );
388 }
389 
390 /**Function*************************************************************
391 
392  Synopsis [Refines one equivalence class.]
393 
394  Description []
395 
396  SideEffects []
397 
398  SeeAlso []
399 
400 ***********************************************************************/
401 int Gia_Sim2ClassRefineOne( Gia_Sim2_t * p, int i )
402 {
403  Gia_Obj_t * pObj0, * pObj1;
404  unsigned * pSim0, * pSim1;
405  int Ent;
406  Vec_IntClear( p->vClassOld );
407  Vec_IntClear( p->vClassNew );
408  Vec_IntPush( p->vClassOld, i );
409  pObj0 = Gia_ManObj( p->pAig, i );
410  pSim0 = Gia_Sim2Data( p, i );
411  Gia_ClassForEachObj1( p->pAig, i, Ent )
412  {
413  pObj1 = Gia_ManObj( p->pAig, Ent );
414  pSim1 = Gia_Sim2Data( p, Ent );
415  if ( Gia_Sim2CompareEqual( pSim0, pSim1, p->nWords, Gia_ObjPhase(pObj0) ^ Gia_ObjPhase(pObj1) ) )
416  Vec_IntPush( p->vClassOld, Ent );
417  else
418  Vec_IntPush( p->vClassNew, Ent );
419  }
420  if ( Vec_IntSize( p->vClassNew ) == 0 )
421  return 0;
422  Gia_Sim2ClassCreate( p->pAig, p->vClassOld );
423  Gia_Sim2ClassCreate( p->pAig, p->vClassNew );
424  if ( Vec_IntSize(p->vClassNew) > 1 )
425  return 1 + Gia_Sim2ClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
426  return 1;
427 }
428 
429 /**Function*************************************************************
430 
431  Synopsis [Computes hash key of the simuation info.]
432 
433  Description []
434 
435  SideEffects []
436 
437  SeeAlso []
438 
439 ***********************************************************************/
440 int Gia_Sim2HashKey( unsigned * pSim, int nWords, int nTableSize )
441 {
442  static int s_Primes[16] = {
443  1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
444  4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
445  unsigned uHash = 0;
446  int i;
447  if ( pSim[0] & 1 )
448  for ( i = 0; i < nWords; i++ )
449  uHash ^= ~pSim[i] * s_Primes[i & 0xf];
450  else
451  for ( i = 0; i < nWords; i++ )
452  uHash ^= pSim[i] * s_Primes[i & 0xf];
453  return (int)(uHash % nTableSize);
454 
455 }
456 
457 /**Function*************************************************************
458 
459  Synopsis [Refines nodes belonging to candidate constant class.]
460 
461  Description []
462 
463  SideEffects []
464 
465  SeeAlso []
466 
467 ***********************************************************************/
468 void Gia_Sim2ProcessRefined( Gia_Sim2_t * p, Vec_Int_t * vRefined )
469 {
470  unsigned * pSim;
471  int * pTable, nTableSize, i, k, Key;
472  if ( Vec_IntSize(vRefined) == 0 )
473  return;
474  nTableSize = Abc_PrimeCudd( 1000 + Vec_IntSize(vRefined) / 3 );
475  pTable = ABC_CALLOC( int, nTableSize );
476  Vec_IntForEachEntry( vRefined, i, k )
477  {
478  pSim = Gia_Sim2Data( p, i );
479  Key = Gia_Sim2HashKey( pSim, p->nWords, nTableSize );
480  if ( pTable[Key] == 0 )
481  {
482  assert( Gia_ObjRepr(p->pAig, i) == 0 );
483  assert( Gia_ObjNext(p->pAig, i) == 0 );
484  Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
485  }
486  else
487  {
488  Gia_ObjSetNext( p->pAig, pTable[Key], i );
489  Gia_ObjSetRepr( p->pAig, i, Gia_ObjRepr(p->pAig, pTable[Key]) );
490  if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID )
491  Gia_ObjSetRepr( p->pAig, i, pTable[Key] );
492  assert( Gia_ObjRepr(p->pAig, i) > 0 );
493  }
494  pTable[Key] = i;
495  }
496 /*
497  Vec_IntForEachEntry( vRefined, i, k )
498  {
499  if ( Gia_ObjIsHead( p->pAig, i ) )
500  Gia_Sim2ClassRefineOne( p, i );
501  }
502 */
503  ABC_FREE( pTable );
504 }
505 /**Function*************************************************************
506 
507  Synopsis [Refines equivalences after one simulation round.]
508 
509  Description []
510 
511  SideEffects []
512 
513  SeeAlso []
514 
515 ***********************************************************************/
516 void Gia_Sim2InfoRefineEquivs( Gia_Sim2_t * p )
517 {
518  Vec_Int_t * vRefined;
519  Gia_Obj_t * pObj;
520  unsigned * pSim;
521  int i, Count = 0;
522  // process constant candidates
523  vRefined = Vec_IntAlloc( 100 );
524  Gia_ManForEachObj1( p->pAig, pObj, i )
525  {
526  if ( !Gia_ObjIsConst(p->pAig, i) )
527  continue;
528  pSim = Gia_Sim2Data( p, i );
529 //Extra_PrintBinary( stdout, pSim, 32 * p->nWords ); printf( "\n" );
530  if ( !Gia_Sim2CompareZero( pSim, p->nWords, Gia_ObjPhase(pObj) ) )
531  {
532  Vec_IntPush( vRefined, i );
533  Count++;
534  }
535  }
536  Gia_Sim2ProcessRefined( p, vRefined );
537  Vec_IntFree( vRefined );
538  // process other classes
539  Gia_ManForEachClass( p->pAig, i )
540  Count += Gia_Sim2ClassRefineOne( p, i );
541 // if ( Count )
542 // printf( "Refined %d times.\n", Count );
543 }
544 
545 /**Function*************************************************************
546 
547  Synopsis [Returns index of the first pattern that failed.]
548 
549  Description []
550 
551  SideEffects []
552 
553  SeeAlso []
554 
555 ***********************************************************************/
556 static inline int Gia_Sim2InfoIsZero( Gia_Sim2_t * p, unsigned * pInfo )
557 {
558  int w;
559  for ( w = 0; w < p->nWords; w++ )
560  if ( pInfo[w] )
561  return 32*w + Gia_WordFindFirstBit( pInfo[w] );
562  return -1;
563 }
564 
565 /**Function*************************************************************
566 
567  Synopsis [Returns index of the PO and pattern that failed it.]
568 
569  Description []
570 
571  SideEffects []
572 
573  SeeAlso []
574 
575 ***********************************************************************/
576 static inline int Gia_Sim2CheckPos( Gia_Sim2_t * p, int * piPo, int * piPat )
577 {
578  Gia_Obj_t * pObj;
579  int i, iPat;
580  Gia_ManForEachPo( p->pAig, pObj, i )
581  {
582  iPat = Gia_Sim2InfoIsZero( p, Gia_Sim2Data( p, Gia_ObjValue(pObj) ) );
583  if ( iPat >= 0 )
584  {
585  *piPo = i;
586  *piPat = iPat;
587  return 1;
588  }
589  }
590  return 0;
591 }
592 
593 /**Function*************************************************************
594 
595  Synopsis [Returns the counter-example.]
596 
597  Description []
598 
599  SideEffects []
600 
601  SeeAlso []
602 
603 ***********************************************************************/
604 Abc_Cex_t * Gia_Sim2GenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat )
605 {
606  Abc_Cex_t * p;
607  unsigned * pData;
608  int f, i, w, Counter;
609  p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
610  p->iFrame = iFrame;
611  p->iPo = iOut;
612  // fill in the binary data
613  Counter = p->nRegs;
614  pData = ABC_ALLOC( unsigned, nWords );
615  for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
616  for ( i = 0; i < Gia_ManPiNum(pAig); i++ )
617  {
618  for ( w = nWords-1; w >= 0; w-- )
619  pData[w] = Gia_ManRandom( 0 );
620  if ( Abc_InfoHasBit( pData, iPat ) )
621  Abc_InfoSetBit( p->pData, Counter + i );
622  }
623  ABC_FREE( pData );
624  return p;
625 }
626 
627 /**Function*************************************************************
628 
629  Synopsis [Performs simulation to refine equivalence classes.]
630 
631  Description [Returns 1 if counter-example is detected.]
632 
633  SideEffects []
634 
635  SeeAlso []
636 
637 ***********************************************************************/
638 int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
639 {
640  Gia_Sim2_t * p;
641  Gia_Obj_t * pObj;
642  abctime clkTotal = Abc_Clock();
643  int i, RetValue = 0, iOut, iPat;
644  abctime nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
645  assert( pAig->pReprs && pAig->pNexts );
646  ABC_FREE( pAig->pCexSeq );
647  p = Gia_Sim2Create( pAig, pPars );
648  Gia_ManResetRandom( pPars );
649  Gia_ManForEachRo( p->pAig, pObj, i )
650  Gia_Sim2InfoZero( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
651  for ( i = 0; i < pPars->nIters; i++ )
652  {
653  Gia_Sim2SimulateRound( p );
654  if ( pPars->fVerbose )
655  {
656  Abc_Print( 1, "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
657  if ( pAig->pReprs && pAig->pNexts )
658  Abc_Print( 1, "Lits = %4d. ", Gia_ManEquivCountLitsAll(pAig) );
659  Abc_Print( 1, "Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC );
660  }
661  if ( pPars->fCheckMiter && Gia_Sim2CheckPos( p, &iOut, &iPat ) )
662  {
663  Gia_ManResetRandom( pPars );
664  pPars->iOutFail = iOut;
665  pAig->pCexSeq = Gia_Sim2GenerateCounter( pAig, i, iOut, p->nWords, iPat );
666  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", iOut, pAig->pName, i );
667  if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
668  {
669 // Abc_Print( 1, "\n" );
670  Abc_Print( 1, "\nGenerated counter-example is INVALID. " );
671 // Abc_Print( 1, "\n" );
672  }
673  else
674  {
675 // Abc_Print( 1, "\n" );
676 // if ( pPars->fVerbose )
677 // Abc_Print( 1, "\nGenerated counter-example is verified correctly. " );
678 // Abc_Print( 1, "\n" );
679  }
680  RetValue = 1;
681  break;
682  }
683  if ( pAig->pReprs && pAig->pNexts )
684  Gia_Sim2InfoRefineEquivs( p );
685  if ( Abc_Clock() > nTimeToStop )
686  {
687  i++;
688  break;
689  }
690  if ( i < pPars->nIters - 1 )
691  Gia_Sim2InfoTransfer( p );
692  }
693  Gia_Sim2Delete( p );
694  if ( pAig->pCexSeq == NULL )
695  Abc_Print( 1, "No bug detected after simulating %d frames with %d words. ", i, pPars->nWords );
696  Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
697  return RetValue;
698 }
699 
700 ////////////////////////////////////////////////////////////////////////
701 /// END OF FILE ///
702 ////////////////////////////////////////////////////////////////////////
703 
704 
705 ABC_NAMESPACE_IMPL_END
706 
Gia_Sim2SimulateRound
static void Gia_Sim2SimulateRound(Gia_Sim2_t *p)
Definition: giaSim2.c:276
Gia_Sim2InfoTransfer
static void Gia_Sim2InfoTransfer(Gia_Sim2_t *p)
Definition: giaSim2.c:252
Gia_Sim2InfoIsZero
static int Gia_Sim2InfoIsZero(Gia_Sim2_t *p, unsigned *pInfo)
Definition: giaSim2.c:556
Gia_Sim2Delete
void Gia_Sim2Delete(Gia_Sim2_t *p)
FUNCTION DEFINITIONS ///.
Definition: giaSim2.c:60
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Gia_Sim2ClassRefineOne
int Gia_Sim2ClassRefineOne(Gia_Sim2_t *p, int i)
Definition: giaSim2.c:401
Gia_ObjPhase
static int Gia_ObjPhase(Gia_Obj_t *pObj)
Definition: gia.h:415
Gia_ParSim_t_::nWords
int nWords
Definition: gia.h:241
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition: giaCex.c:44
Gia_Man_t_::pNexts
int * pNexts
Definition: gia.h:122
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Gia_Sim2InfoRefineEquivs
void Gia_Sim2InfoRefineEquivs(Gia_Sim2_t *p)
Definition: giaSim2.c:516
Gia_Sim2InfoOne
static void Gia_Sim2InfoOne(Gia_Sim2_t *p, unsigned *pInfo)
Definition: giaSim2.c:155
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
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
Gia_Sim2CompareEqual
int Gia_Sim2CompareEqual(unsigned *p0, unsigned *p1, int nWords, int fCompl)
Definition: giaSim2.c:307
Gia_WordFindFirstBit
static int Gia_WordFindFirstBit(unsigned uWord)
Definition: gia.h:321
Gia_ObjValue
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
Gia_Sim2InfoZero
static void Gia_Sim2InfoZero(Gia_Sim2_t *p, unsigned *pInfo)
Definition: giaSim2.c:137
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
nWords
int nWords
Definition: abcNpn.c:127
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Gia_Sim2Create
Gia_Sim2_t * Gia_Sim2Create(Gia_Man_t *pAig, Gia_ParSim_t *pPars)
Definition: giaSim2.c:79
Gia_Obj_t_
Definition: gia.h:75
Gia_ParSim_t_::fVerbose
int fVerbose
Definition: gia.h:246
Gia_Sim2ProcessRefined
void Gia_Sim2ProcessRefined(Gia_Sim2_t *p, Vec_Int_t *vRefined)
Definition: giaSim2.c:468
Gia_ManRandom
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
Gia_Sim2Data
static unsigned * Gia_Sim2Data(Gia_Sim2_t *p, int i)
Definition: giaSim2.c:41
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Gia_Sim2SimulateCo
static void Gia_Sim2SimulateCo(Gia_Sim2_t *p, Gia_Obj_t *pObj)
Definition: giaSim2.c:191
Gia_ObjSetRepr
static void Gia_ObjSetRepr(Gia_Man_t *p, int Id, int Num)
Definition: gia.h:888
Gia_Sim2_t_::vClassNew
Vec_Int_t * vClassNew
Definition: giaSim2.c:38
s_Primes
static int s_Primes[MAX_PRIMES]
Definition: fxuPair.c:30
Gia_Sim2CompareZero
int Gia_Sim2CompareZero(unsigned *p0, int nWords, int fCompl)
Definition: giaSim2.c:337
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_Sim2SimulateNode
static void Gia_Sim2SimulateNode(Gia_Sim2_t *p, Gia_Obj_t *pObj)
Definition: giaSim2.c:215
Gia_ParSim_t_::fCheckMiter
int fCheckMiter
Definition: gia.h:245
Gia_Sim2GenerateCounter
Abc_Cex_t * Gia_Sim2GenerateCounter(Gia_Man_t *pAig, int iFrame, int iOut, int nWords, int iPat)
Definition: giaSim2.c:604
Gia_ManEquivCountLitsAll
int Gia_ManEquivCountLitsAll(Gia_Man_t *p)
Definition: giaEquiv.c:160
Gia_ParSim_t_
Definition: gia.h:238
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_Sim2InfoRandom
static void Gia_Sim2InfoRandom(Gia_Sim2_t *p, unsigned *pInfo)
Definition: giaSim2.c:119
Gia_ObjIsConst
static int Gia_ObjIsConst(Gia_Man_t *p, int Id)
Definition: gia.h:915
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Gia_Sim2_t_
Definition: giaSim2.c:31
Gia_ClassForEachObj1
#define Gia_ClassForEachObj1(p, i, iObj)
Definition: gia.h:933
Gia_Sim2HashKey
int Gia_Sim2HashKey(unsigned *pSim, int nWords, int nTableSize)
Definition: giaSim2.c:440
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Gia_ParSim_t_::nIters
int nIters
Definition: gia.h:242
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_Sim2_t_::pDataSim
unsigned * pDataSim
Definition: giaSim2.c:36
Counter
static int Counter
Definition: extraBddMisc.c:1877
Gia_Sim2_t_::nWords
int nWords
Definition: giaSim2.c:35
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Gia_Sim2_t_::pPars
Gia_ParSim_t * pPars
Definition: giaSim2.c:34
Gia_ObjNext
static int Gia_ObjNext(Gia_Man_t *p, int Id)
Definition: gia.h:912
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Gia_ObjSetNext
static void Gia_ObjSetNext(Gia_Man_t *p, int Id, int Num)
Definition: gia.h:913
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Gia_Sim2_t
typedefABC_NAMESPACE_IMPL_START struct Gia_Sim2_t_ Gia_Sim2_t
DECLARATIONS ///.
Definition: giaSim2.c:30
GIA_VOID
#define GIA_VOID
Definition: gia.h:45
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
Gia_Sim2CheckPos
static int Gia_Sim2CheckPos(Gia_Sim2_t *p, int *piPo, int *piPat)
Definition: giaSim2.c:576
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Gia_ManResetRandom
void Gia_ManResetRandom(Gia_ParSim_t *pPars)
Definition: giaSim.c:579
Gia_ManForEachClass
#define Gia_ManForEachClass(p, i)
Definition: gia.h:927
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition: gia.h:121
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManSetPhase
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
Gia_ParSim_t_::iOutFail
int iOutFail
Definition: gia.h:247
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Gia_ManSimSimulateEquiv
int Gia_ManSimSimulateEquiv(Gia_Man_t *pAig, Gia_ParSim_t *pPars)
Definition: giaSim2.c:638
Gia_Sim2ClassCreate
void Gia_Sim2ClassCreate(Gia_Man_t *p, Vec_Int_t *vClass)
Definition: giaSim2.c:367
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_ObjFaninId1
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
Gia_Sim2_t_::vClassOld
Vec_Int_t * vClassOld
Definition: giaSim2.c:37
Gia_Sim2_t_::pAig
Gia_Man_t * pAig
Definition: giaSim2.c:33
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_ObjRepr
static int Gia_ObjRepr(Gia_Man_t *p, int Id)
Definition: gia.h:887
Gia_Sim2InfoCopy
static void Gia_Sim2InfoCopy(Gia_Sim2_t *p, unsigned *pInfo, unsigned *pInfo0)
Definition: giaSim2.c:173
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
Gia_Man_t_::pCexSeq
Abc_Cex_t * pCexSeq
Definition: gia.h:136
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Gia_ParSim_t_::TimeLimit
int TimeLimit
Definition: gia.h:244