abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cecClass.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [cecClass.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Combinational equivalence checking.]
8 
9  Synopsis [Equivalence class refinement.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: cecClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "cecInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 static inline unsigned * Cec_ObjSim( Cec_ManSim_t * p, int Id ) { return p->pMems + p->pSimInfo[Id] + 1; }
31 static inline void Cec_ObjSetSim( Cec_ManSim_t * p, int Id, int n ) { p->pSimInfo[Id] = n; }
32 
33 static inline float Cec_MemUsage( Cec_ManSim_t * p ) { return 1.0*p->nMemsMax*(p->pPars->nWords+1)/(1<<20); }
34 
35 ////////////////////////////////////////////////////////////////////////
36 /// FUNCTION DEFINITIONS ///
37 ////////////////////////////////////////////////////////////////////////
38 
39 /**Function*************************************************************
40 
41  Synopsis [Compares simulation info of one node with constant 0.]
42 
43  Description []
44 
45  SideEffects []
46 
47  SeeAlso []
48 
49 ***********************************************************************/
50 int Cec_ManSimCompareConst( unsigned * p, int nWords )
51 {
52  int w;
53  if ( p[0] & 1 )
54  {
55  for ( w = 0; w < nWords; w++ )
56  if ( p[w] != ~0 )
57  return 0;
58  return 1;
59  }
60  else
61  {
62  for ( w = 0; w < nWords; w++ )
63  if ( p[w] != 0 )
64  return 0;
65  return 1;
66  }
67 }
68 
69 /**Function*************************************************************
70 
71  Synopsis [Compares simulation info of two nodes.]
72 
73  Description []
74 
75  SideEffects []
76 
77  SeeAlso []
78 
79 ***********************************************************************/
80 int Cec_ManSimCompareEqual( unsigned * p0, unsigned * p1, int nWords )
81 {
82  int w;
83  if ( (p0[0] & 1) == (p1[0] & 1) )
84  {
85  for ( w = 0; w < nWords; w++ )
86  if ( p0[w] != p1[w] )
87  return 0;
88  return 1;
89  }
90  else
91  {
92  for ( w = 0; w < nWords; w++ )
93  if ( p0[w] != ~p1[w] )
94  return 0;
95  return 1;
96  }
97 }
98 
99 /**Function*************************************************************
100 
101  Synopsis [Returns the number of the first non-equal bit.]
102 
103  Description []
104 
105  SideEffects []
106 
107  SeeAlso []
108 
109 ***********************************************************************/
110 int Cec_ManSimCompareConstFirstBit( unsigned * p, int nWords )
111 {
112  int w;
113  if ( p[0] & 1 )
114  {
115  for ( w = 0; w < nWords; w++ )
116  if ( p[w] != ~0 )
117  return 32*w + Gia_WordFindFirstBit( ~p[w] );
118  return -1;
119  }
120  else
121  {
122  for ( w = 0; w < nWords; w++ )
123  if ( p[w] != 0 )
124  return 32*w + Gia_WordFindFirstBit( p[w] );
125  return -1;
126  }
127 }
128 
129 /**Function*************************************************************
130 
131  Synopsis [Compares simulation info of two nodes.]
132 
133  Description []
134 
135  SideEffects []
136 
137  SeeAlso []
138 
139 ***********************************************************************/
140 int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords )
141 {
142  int w;
143  if ( (p0[0] & 1) == (p1[0] & 1) )
144  {
145  for ( w = 0; w < nWords; w++ )
146  if ( p0[w] != p1[w] )
147  return 32*w + Gia_WordFindFirstBit( p0[w] ^ p1[w] );
148  return -1;
149  }
150  else
151  {
152  for ( w = 0; w < nWords; w++ )
153  if ( p0[w] != ~p1[w] )
154  return 32*w + Gia_WordFindFirstBit( p0[w] ^ ~p1[w] );
155  return -1;
156  }
157 }
158 
159 /**Function*************************************************************
160 
161  Synopsis [Returns the number of the first non-equal bit.]
162 
163  Description []
164 
165  SideEffects []
166 
167  SeeAlso []
168 
169 ***********************************************************************/
170 void Cec_ManSimCompareConstScore( unsigned * p, int nWords, int * pScores )
171 {
172  int w, b;
173  if ( p[0] & 1 )
174  {
175  for ( w = 0; w < nWords; w++ )
176  if ( p[w] != ~0 )
177  for ( b = 0; b < 32; b++ )
178  if ( ((~p[w]) >> b ) & 1 )
179  pScores[32*w + b]++;
180  }
181  else
182  {
183  for ( w = 0; w < nWords; w++ )
184  if ( p[w] != 0 )
185  for ( b = 0; b < 32; b++ )
186  if ( ((p[w]) >> b ) & 1 )
187  pScores[32*w + b]++;
188  }
189 }
190 
191 /**Function*************************************************************
192 
193  Synopsis [Compares simulation info of two nodes.]
194 
195  Description []
196 
197  SideEffects []
198 
199  SeeAlso []
200 
201 ***********************************************************************/
202 void Cec_ManSimCompareEqualScore( unsigned * p0, unsigned * p1, int nWords, int * pScores )
203 {
204  int w, b;
205  if ( (p0[0] & 1) == (p1[0] & 1) )
206  {
207  for ( w = 0; w < nWords; w++ )
208  if ( p0[w] != p1[w] )
209  for ( b = 0; b < 32; b++ )
210  if ( ((p0[w] ^ p1[w]) >> b ) & 1 )
211  pScores[32*w + b]++;
212  }
213  else
214  {
215  for ( w = 0; w < nWords; w++ )
216  if ( p0[w] != ~p1[w] )
217  for ( b = 0; b < 32; b++ )
218  if ( ((p0[w] ^ ~p1[w]) >> b ) & 1 )
219  pScores[32*w + b]++;
220  }
221 }
222 
223 /**Function*************************************************************
224 
225  Synopsis [Creates equivalence class.]
226 
227  Description []
228 
229  SideEffects []
230 
231  SeeAlso []
232 
233 ***********************************************************************/
234 void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
235 {
236  int Repr = GIA_VOID, EntPrev = -1, Ent, i;
237  assert( Vec_IntSize(vClass) > 0 );
238  Vec_IntForEachEntry( vClass, Ent, i )
239  {
240  if ( i == 0 )
241  {
242  Repr = Ent;
243  Gia_ObjSetRepr( p, Ent, GIA_VOID );
244  EntPrev = Ent;
245  }
246  else
247  {
248  assert( Repr < Ent );
249  Gia_ObjSetRepr( p, Ent, Repr );
250  Gia_ObjSetNext( p, EntPrev, Ent );
251  EntPrev = Ent;
252  }
253  }
254  Gia_ObjSetNext( p, EntPrev, 0 );
255 }
256 
257 /**Function*************************************************************
258 
259  Synopsis [Refines one equivalence class.]
260 
261  Description []
262 
263  SideEffects []
264 
265  SeeAlso []
266 
267 ***********************************************************************/
268 int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
269 {
270  unsigned * pSim0, * pSim1;
271  int Ent;
272  Vec_IntClear( p->vClassOld );
273  Vec_IntClear( p->vClassNew );
274  Vec_IntPush( p->vClassOld, i );
275  pSim0 = Cec_ObjSim(p, i);
276  Gia_ClassForEachObj1( p->pAig, i, Ent )
277  {
278  pSim1 = Cec_ObjSim(p, Ent);
279  if ( Cec_ManSimCompareEqual( pSim0, pSim1, p->nWords ) )
280  Vec_IntPush( p->vClassOld, Ent );
281  else
282  {
283  Vec_IntPush( p->vClassNew, Ent );
284  if ( p->pBestState )
285  Cec_ManSimCompareEqualScore( pSim0, pSim1, p->nWords, p->pScores );
286  }
287  }
288  if ( Vec_IntSize( p->vClassNew ) == 0 )
289  return 0;
290  Cec_ManSimClassCreate( p->pAig, p->vClassOld );
291  Cec_ManSimClassCreate( p->pAig, p->vClassNew );
292  if ( Vec_IntSize(p->vClassNew) > 1 )
293  return 1 + Cec_ManSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
294  return 1;
295 }
296 
297 /**Function*************************************************************
298 
299  Synopsis [Refines one equivalence class.]
300 
301  Description []
302 
303  SideEffects []
304 
305  SeeAlso []
306 
307 ***********************************************************************/
308 int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i )
309 {
310  int iRepr, Ent;
311  if ( Gia_ObjIsConst(p->pAig, i) )
312  {
313  Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
314  return 1;
315  }
316  if ( !Gia_ObjIsClass(p->pAig, i) )
317  return 0;
318  assert( Gia_ObjIsClass(p->pAig, i) );
319  iRepr = Gia_ObjRepr( p->pAig, i );
320  if ( iRepr == GIA_VOID )
321  iRepr = i;
322  // collect nodes
323  Vec_IntClear( p->vClassOld );
324  Vec_IntClear( p->vClassNew );
325  Gia_ClassForEachObj( p->pAig, iRepr, Ent )
326  {
327  if ( Ent == i )
328  Vec_IntPush( p->vClassNew, Ent );
329  else
330  Vec_IntPush( p->vClassOld, Ent );
331  }
332  assert( Vec_IntSize( p->vClassNew ) == 1 );
333  Cec_ManSimClassCreate( p->pAig, p->vClassOld );
334  Cec_ManSimClassCreate( p->pAig, p->vClassNew );
335  assert( !Gia_ObjIsClass(p->pAig, i) );
336  return 1;
337 }
338 
339 /**Function*************************************************************
340 
341  Synopsis [Computes hash key of the simuation info.]
342 
343  Description []
344 
345  SideEffects []
346 
347  SeeAlso []
348 
349 ***********************************************************************/
350 int Cec_ManSimHashKey( unsigned * pSim, int nWords, int nTableSize )
351 {
352  static int s_Primes[16] = {
353  1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
354  4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
355  unsigned uHash = 0;
356  int i;
357  if ( pSim[0] & 1 )
358  for ( i = 0; i < nWords; i++ )
359  uHash ^= ~pSim[i] * s_Primes[i & 0xf];
360  else
361  for ( i = 0; i < nWords; i++ )
362  uHash ^= pSim[i] * s_Primes[i & 0xf];
363  return (int)(uHash % nTableSize);
364 
365 }
366 
367 /**Function*************************************************************
368 
369  Synopsis [Resets pointers to the simulation memory.]
370 
371  Description []
372 
373  SideEffects []
374 
375  SeeAlso []
376 
377 ***********************************************************************/
378 void Cec_ManSimMemRelink( Cec_ManSim_t * p )
379 {
380  unsigned * pPlace, Ent;
381  pPlace = (unsigned *)&p->MemFree;
382  for ( Ent = p->nMems * (p->nWords + 1);
383  Ent + p->nWords + 1 < (unsigned)p->nWordsAlloc;
384  Ent += p->nWords + 1 )
385  {
386  *pPlace = Ent;
387  pPlace = p->pMems + Ent;
388  }
389  *pPlace = 0;
390  p->nWordsOld = p->nWords;
391 }
392 
393 /**Function*************************************************************
394 
395  Synopsis [References simulation info.]
396 
397  Description []
398 
399  SideEffects []
400 
401  SeeAlso []
402 
403 ***********************************************************************/
404 unsigned * Cec_ManSimSimRef( Cec_ManSim_t * p, int i )
405 {
406  unsigned * pSim;
407  assert( p->pSimInfo[i] == 0 );
408  if ( p->MemFree == 0 )
409  {
410  if ( p->nWordsAlloc == 0 )
411  {
412  assert( p->pMems == NULL );
413  p->nWordsAlloc = (1<<17); // -> 1Mb
414  p->nMems = 1;
415  }
416  p->nWordsAlloc *= 2;
417  p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc );
418  Cec_ManSimMemRelink( p );
419  }
420  p->pSimInfo[i] = p->MemFree;
421  pSim = p->pMems + p->MemFree;
422  p->MemFree = pSim[0];
423  pSim[0] = Gia_ObjValue( Gia_ManObj(p->pAig, i) );
424  p->nMems++;
425  if ( p->nMemsMax < p->nMems )
426  p->nMemsMax = p->nMems;
427  return pSim;
428 }
429 
430 /**Function*************************************************************
431 
432  Synopsis [Dereferences simulaton info.]
433 
434  Description []
435 
436  SideEffects []
437 
438  SeeAlso []
439 
440 ***********************************************************************/
441 unsigned * Cec_ManSimSimDeref( Cec_ManSim_t * p, int i )
442 {
443  unsigned * pSim;
444  assert( p->pSimInfo[i] > 0 );
445  pSim = p->pMems + p->pSimInfo[i];
446  if ( --pSim[0] == 0 )
447  {
448  pSim[0] = p->MemFree;
449  p->MemFree = p->pSimInfo[i];
450  p->pSimInfo[i] = 0;
451  p->nMems--;
452  }
453  return pSim;
454 }
455 
456 /**Function*************************************************************
457 
458  Synopsis [Refines nodes belonging to candidate constant class.]
459 
460  Description []
461 
462  SideEffects []
463 
464  SeeAlso []
465 
466 ***********************************************************************/
467 void Cec_ManSimProcessRefined( Cec_ManSim_t * p, Vec_Int_t * vRefined )
468 {
469  unsigned * pSim;
470  int * pTable, nTableSize, i, k, Key;
471  if ( Vec_IntSize(vRefined) == 0 )
472  return;
473  nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
474  pTable = ABC_CALLOC( int, nTableSize );
475  Vec_IntForEachEntry( vRefined, i, k )
476  {
477  pSim = Cec_ObjSim( p, i );
478  assert( !Cec_ManSimCompareConst( pSim, p->nWords ) );
479  Key = Cec_ManSimHashKey( 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  Vec_IntForEachEntry( vRefined, i, k )
497  {
498  if ( Gia_ObjIsHead( p->pAig, i ) )
499  Cec_ManSimClassRefineOne( p, i );
500  }
501  Vec_IntForEachEntry( vRefined, i, k )
502  Cec_ManSimSimDeref( p, i );
503  ABC_FREE( pTable );
504 }
505 
506 
507 /**Function*************************************************************
508 
509  Synopsis [Saves the input pattern with the given number.]
510 
511  Description []
512 
513  SideEffects []
514 
515  SeeAlso []
516 
517 ***********************************************************************/
518 void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
519 {
520  unsigned * pInfo;
521  int i;
522  assert( p->pCexComb == NULL );
523  assert( iPat >= 0 && iPat < 32 * p->nWords );
524  p->pCexComb = (Abc_Cex_t *)ABC_CALLOC( char,
525  sizeof(Abc_Cex_t) + sizeof(unsigned) * Abc_BitWordNum(Gia_ManCiNum(p->pAig)) );
526  p->pCexComb->iPo = p->iOut;
527  p->pCexComb->nPis = Gia_ManCiNum(p->pAig);
528  p->pCexComb->nBits = Gia_ManCiNum(p->pAig);
529  for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
530  {
531  pInfo = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, i );
532  if ( Abc_InfoHasBit( pInfo, iPat ) )
533  Abc_InfoSetBit( p->pCexComb->pData, i );
534  }
535 }
536 
537 /**Function*************************************************************
538 
539  Synopsis [Find the best pattern using the scores.]
540 
541  Description []
542 
543  SideEffects []
544 
545  SeeAlso []
546 
547 ***********************************************************************/
548 void Cec_ManSimFindBestPattern( Cec_ManSim_t * p )
549 {
550  unsigned * pInfo;
551  int i, ScoreBest = 0, iPatBest = 1; // set the first pattern
552  // find the best pattern
553  for ( i = 0; i < 32 * p->nWords; i++ )
554  if ( ScoreBest < p->pScores[i] )
555  {
556  ScoreBest = p->pScores[i];
557  iPatBest = i;
558  }
559  // compare this with the available patterns - and save
560  if ( p->pBestState->iPo <= ScoreBest )
561  {
562  assert( p->pBestState->nRegs == Gia_ManRegNum(p->pAig) );
563  for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
564  {
565  pInfo = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
566  if ( Abc_InfoHasBit(p->pBestState->pData, i) != Abc_InfoHasBit(pInfo, iPatBest) )
567  Abc_InfoXorBit( p->pBestState->pData, i );
568  }
569  p->pBestState->iPo = ScoreBest;
570  }
571 }
572 
573 /**Function*************************************************************
574 
575  Synopsis [Returns 1 if computation should stop.]
576 
577  Description []
578 
579  SideEffects []
580 
581  SeeAlso []
582 
583 ***********************************************************************/
584 int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
585 {
586  unsigned * pInfo, * pInfo2;
587  int i;
588  if ( !p->pPars->fCheckMiter )
589  return 0;
590  assert( p->vCoSimInfo != NULL );
591  // compare outputs with 0
592  if ( p->pPars->fDualOut )
593  {
594  assert( (Gia_ManPoNum(p->pAig) & 1) == 0 );
595  for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
596  {
597  pInfo = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, i );
598  pInfo2 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, ++i );
599  if ( !Cec_ManSimCompareEqual( pInfo, pInfo2, p->nWords ) )
600  {
601  if ( p->iOut == -1 )
602  {
603  p->iOut = i/2;
604  Cec_ManSimSavePattern( p, Cec_ManSimCompareEqualFirstBit(pInfo, pInfo2, p->nWords) );
605  }
606  if ( p->pCexes == NULL )
607  p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig)/2 );
608  if ( p->pCexes[i/2] == NULL )
609  {
610  p->nOuts++;
611  p->pCexes[i/2] = (void *)1;
612  }
613  }
614  }
615  }
616  else
617  {
618  for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
619  {
620  pInfo = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, i );
621  if ( !Cec_ManSimCompareConst( pInfo, p->nWords ) )
622  {
623  if ( p->iOut == -1 )
624  {
625  p->iOut = i;
626  Cec_ManSimSavePattern( p, Cec_ManSimCompareConstFirstBit(pInfo, p->nWords) );
627  }
628  if ( p->pCexes == NULL )
629  p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig) );
630  if ( p->pCexes[i] == NULL )
631  {
632  p->nOuts++;
633  p->pCexes[i] = (void *)1;
634  }
635  }
636  }
637  }
638  return p->pCexes != NULL;
639 }
640 
641 /**Function*************************************************************
642 
643  Synopsis [Simulates one round.]
644 
645  Description [Returns the number of PO entry if failed; 0 otherwise.]
646 
647  SideEffects []
648 
649  SeeAlso []
650 
651 ***********************************************************************/
652 int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos )
653 {
654  Gia_Obj_t * pObj;
655  unsigned * pRes0, * pRes1, * pRes;
656  int i, k, w, Ent, iCiId = 0, iCoId = 0;
657  // prepare internal storage
658  if ( p->nWordsOld != p->nWords )
659  Cec_ManSimMemRelink( p );
660  p->nMemsMax = 0;
661  // allocate score counters
662  ABC_FREE( p->pScores );
663  if ( p->pBestState )
664  p->pScores = ABC_CALLOC( int, 32 * p->nWords );
665  // simulate nodes
666  Vec_IntClear( p->vRefinedC );
667  if ( Gia_ObjValue(Gia_ManConst0(p->pAig)) )
668  {
669  pRes = Cec_ManSimSimRef( p, 0 );
670  for ( w = 1; w <= p->nWords; w++ )
671  pRes[w] = 0;
672  }
673  Gia_ManForEachObj1( p->pAig, pObj, i )
674  {
675  if ( Gia_ObjIsCi(pObj) )
676  {
677  if ( Gia_ObjValue(pObj) == 0 )
678  {
679  iCiId++;
680  continue;
681  }
682  pRes = Cec_ManSimSimRef( p, i );
683  if ( vInfoCis )
684  {
685  pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, iCiId++ );
686  for ( w = 1; w <= p->nWords; w++ )
687  pRes[w] = pRes0[w-1];
688  }
689  else
690  {
691  for ( w = 1; w <= p->nWords; w++ )
692  pRes[w] = Gia_ManRandom( 0 );
693  }
694  // make sure the first pattern is always zero
695  pRes[1] ^= (pRes[1] & 1);
696  goto references;
697  }
698  if ( Gia_ObjIsCo(pObj) ) // co always has non-zero 1st fanin and zero 2nd fanin
699  {
700  pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
701  if ( vInfoCos )
702  {
703  pRes = (unsigned *)Vec_PtrEntry( vInfoCos, iCoId++ );
704  if ( Gia_ObjFaninC0(pObj) )
705  for ( w = 1; w <= p->nWords; w++ )
706  pRes[w-1] = ~pRes0[w];
707  else
708  for ( w = 1; w <= p->nWords; w++ )
709  pRes[w-1] = pRes0[w];
710  }
711  continue;
712  }
713  assert( Gia_ObjValue(pObj) );
714  pRes = Cec_ManSimSimRef( p, i );
715  pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
716  pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) );
717 
718 // Abc_Print( 1, "%d,%d ", Gia_ObjValue( Gia_ObjFanin0(pObj) ), Gia_ObjValue( Gia_ObjFanin1(pObj) ) );
719 
720  if ( Gia_ObjFaninC0(pObj) )
721  {
722  if ( Gia_ObjFaninC1(pObj) )
723  for ( w = 1; w <= p->nWords; w++ )
724  pRes[w] = ~(pRes0[w] | pRes1[w]);
725  else
726  for ( w = 1; w <= p->nWords; w++ )
727  pRes[w] = ~pRes0[w] & pRes1[w];
728  }
729  else
730  {
731  if ( Gia_ObjFaninC1(pObj) )
732  for ( w = 1; w <= p->nWords; w++ )
733  pRes[w] = pRes0[w] & ~pRes1[w];
734  else
735  for ( w = 1; w <= p->nWords; w++ )
736  pRes[w] = pRes0[w] & pRes1[w];
737  }
738 
739 references:
740  // if this node is candidate constant, collect it
741  if ( Gia_ObjIsConst(p->pAig, i) && !Cec_ManSimCompareConst(pRes + 1, p->nWords) )
742  {
743  pRes[0]++;
744  Vec_IntPush( p->vRefinedC, i );
745  if ( p->pBestState )
746  Cec_ManSimCompareConstScore( pRes + 1, p->nWords, p->pScores );
747  }
748  // if the node belongs to a class, save it
749  if ( Gia_ObjIsClass(p->pAig, i) )
750  pRes[0]++;
751  // if this is the last node of the class, process it
752  if ( Gia_ObjIsTail(p->pAig, i) )
753  {
754  Vec_IntClear( p->vClassTemp );
755  Gia_ClassForEachObj( p->pAig, Gia_ObjRepr(p->pAig, i), Ent )
756  Vec_IntPush( p->vClassTemp, Ent );
757  Cec_ManSimClassRefineOne( p, Gia_ObjRepr(p->pAig, i) );
758  Vec_IntForEachEntry( p->vClassTemp, Ent, k )
759  Cec_ManSimSimDeref( p, Ent );
760  }
761  }
762 
763  if ( p->pPars->fConstCorr )
764  {
765  Vec_IntForEachEntry( p->vRefinedC, i, k )
766  {
767  Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
768  Cec_ManSimSimDeref( p, i );
769  }
770  Vec_IntClear( p->vRefinedC );
771  }
772 
773  if ( Vec_IntSize(p->vRefinedC) > 0 )
774  Cec_ManSimProcessRefined( p, p->vRefinedC );
775  assert( vInfoCis == NULL || iCiId == Gia_ManCiNum(p->pAig) );
776  assert( vInfoCos == NULL || iCoId == Gia_ManCoNum(p->pAig) );
777  assert( p->nMems == 1 );
778  if ( p->nMems != 1 )
779  Abc_Print( 1, "Cec_ManSimSimulateRound(): Memory management error!\n" );
780  if ( p->pPars->fVeryVerbose )
781  Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
782  if ( p->pBestState )
783  Cec_ManSimFindBestPattern( p );
784 /*
785  if ( p->nMems > 1 ) {
786  for ( i = 1; i < p->nObjs; i++ )
787  if ( p->pSims[i] ) {
788  int x = 0;
789  }
790  }
791 */
792  return Cec_ManSimAnalyzeOutputs( p );
793 }
794 
795 
796 
797 /**Function*************************************************************
798 
799  Synopsis [Creates simulation info for this round.]
800 
801  Description []
802 
803  SideEffects []
804 
805  SeeAlso []
806 
807 ***********************************************************************/
808 void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos )
809 {
810  unsigned * pRes0, * pRes1;
811  int i, w;
812  if ( p->pPars->fSeqSimulate && Gia_ManRegNum(p->pAig) > 0 )
813  {
814  assert( vInfoCis && vInfoCos );
815  for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
816  {
817  pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, i );
818  for ( w = 0; w < p->nWords; w++ )
819  pRes0[w] = Gia_ManRandom( 0 );
820  }
821  for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
822  {
823  pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, Gia_ManPiNum(p->pAig) + i );
824  pRes1 = (unsigned *)Vec_PtrEntry( vInfoCos, Gia_ManPoNum(p->pAig) + i );
825  for ( w = 0; w < p->nWords; w++ )
826  pRes0[w] = pRes1[w];
827  }
828  }
829  else
830  {
831  for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
832  {
833  pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, i );
834  for ( w = 0; w < p->nWords; w++ )
835  pRes0[w] = Gia_ManRandom( 0 );
836  }
837  }
838 }
839 
840 /**Function*************************************************************
841 
842  Synopsis [Returns 1 if the bug is found.]
843 
844  Description []
845 
846  SideEffects []
847 
848  SeeAlso []
849 
850 ***********************************************************************/
851 int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax )
852 {
853  Gia_Obj_t * pObj;
854  int i;
855  assert( p->pAig->pReprs == NULL );
856  // allocate representation
857  p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) );
858  p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
859  // create references
860  Gia_ManCreateValueRefs( p->pAig );
861  // set starting representative of internal nodes to be constant 0
862  if ( p->pPars->fLatchCorr )
863  Gia_ManForEachObj( p->pAig, pObj, i )
864  Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
865  else if ( LevelMax == -1 )
866  Gia_ManForEachObj( p->pAig, pObj, i )
867  Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
868  else
869  {
870  Gia_ManLevelNum( p->pAig );
871  Gia_ManForEachObj( p->pAig, pObj, i )
872  Gia_ObjSetRepr( p->pAig, i, (Gia_ObjIsAnd(pObj) && Gia_ObjLevel(p->pAig,pObj) <= LevelMax) ? 0 : GIA_VOID );
873  Vec_IntFreeP( &p->pAig->vLevels );
874  }
875  // if sequential simulation, set starting representative of ROs to be constant 0
876  if ( p->pPars->fSeqSimulate )
877  Gia_ManForEachRo( p->pAig, pObj, i )
878  if ( pObj->Value )
879  Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
880  // perform simulation
881  p->nWords = 1;
882  do {
883  if ( p->pPars->fVerbose )
884  Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
885  for ( i = 0; i < 4; i++ )
886  {
887  Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
888  if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
889  return 1;
890  }
891  p->nWords = 2 * p->nWords + 1;
892  }
893  while ( p->nWords <= p->pPars->nWords );
894  return 0;
895 }
896 
897 /**Function*************************************************************
898 
899  Synopsis [Returns 1 if the bug is found.]
900 
901  Description []
902 
903  SideEffects []
904 
905  SeeAlso []
906 
907 ***********************************************************************/
908 int Cec_ManSimClassesRefine( Cec_ManSim_t * p )
909 {
910  int i;
911  Gia_ManCreateValueRefs( p->pAig );
912  p->nWords = p->pPars->nWords;
913  for ( i = 0; i < p->pPars->nRounds; i++ )
914  {
915  if ( (i % (p->pPars->nRounds / 5)) == 0 && p->pPars->fVerbose )
916  Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
917  Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
918  if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
919  return 1;
920  }
921  if ( p->pPars->fVerbose )
922  Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
923  return 0;
924 }
925 ////////////////////////////////////////////////////////////////////////
926 /// END OF FILE ///
927 ////////////////////////////////////////////////////////////////////////
928 
929 
930 ABC_NAMESPACE_IMPL_END
931 
Cec_ManSim_t_::pCexComb
Abc_Cex_t * pCexComb
Definition: cecInt.h:133
Cec_ParSim_t_::fVerbose
int fVerbose
Definition: cec.h:73
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
Cec_ManSimClassesPrepare
int Cec_ManSimClassesPrepare(Cec_ManSim_t *p, int LevelMax)
Definition: cecClass.c:851
Cec_ParSim_t_::fVeryVerbose
int fVeryVerbose
Definition: cec.h:72
Gia_ObjIsClass
static int Gia_ObjIsClass(Gia_Man_t *p, int Id)
Definition: gia.h:919
Cec_ManSimCompareEqualScore
void Cec_ManSimCompareEqualScore(unsigned *p0, unsigned *p1, int nWords, int *pScores)
Definition: cecClass.c:202
Cec_ManSimSimRef
unsigned * Cec_ManSimSimRef(Cec_ManSim_t *p, int i)
Definition: cecClass.c:404
Cec_ParSim_t_::fLatchCorr
int fLatchCorr
Definition: cec.h:70
Cec_ManSim_t_::pScores
int * pScores
Definition: cecInt.h:136
Gia_Man_t_::pNexts
int * pNexts
Definition: gia.h:122
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
Cec_ManSimSimDeref
unsigned * Cec_ManSimSimDeref(Cec_ManSim_t *p, int i)
Definition: cecClass.c:441
Cec_ParSim_t_::fSeqSimulate
int fSeqSimulate
Definition: cec.h:69
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Cec_ManSimCreateInfo
void Cec_ManSimCreateInfo(Cec_ManSim_t *p, Vec_Ptr_t *vInfoCis, Vec_Ptr_t *vInfoCos)
Definition: cecClass.c:808
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
Cec_ManSimMemRelink
void Cec_ManSimMemRelink(Cec_ManSim_t *p)
Definition: cecClass.c:378
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
Abc_InfoXorBit
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
Cec_ManSimSimulateRound
int Cec_ManSimSimulateRound(Cec_ManSim_t *p, Vec_Ptr_t *vInfoCis, Vec_Ptr_t *vInfoCos)
Definition: cecClass.c:652
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
Cec_ManSim_t_
Definition: cecInt.h:112
Gia_ObjIsHead
static int Gia_ObjIsHead(Gia_Man_t *p, int Id)
Definition: gia.h:916
Cec_ManSim_t_::pAig
Gia_Man_t * pAig
Definition: cecInt.h:115
Cec_ManSim_t_::nMems
int nMems
Definition: cecInt.h:122
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
for
for(p=first;p->value< newval;p=p->next)
Gia_Obj_t_
Definition: gia.h:75
Cec_ParSim_t_::fCheckMiter
int fCheckMiter
Definition: cec.h:67
Gia_ManEquivPrintClasses
void Gia_ManEquivPrintClasses(Gia_Man_t *p, int fVerbose, float Mem)
Definition: giaEquiv.c:304
Gia_ManRandom
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
Cec_ObjSetSim
static void Cec_ObjSetSim(Cec_ManSim_t *p, int Id, int n)
Definition: cecClass.c:31
Gia_ObjSetRepr
static void Gia_ObjSetRepr(Gia_Man_t *p, int Id, int Num)
Definition: gia.h:888
Gia_ManCreateValueRefs
void Gia_ManCreateValueRefs(Gia_Man_t *p)
Definition: giaUtil.c:687
s_Primes
static int s_Primes[MAX_PRIMES]
Definition: fxuPair.c:30
Gia_ObjLevel
static int Gia_ObjLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:501
Cec_ManSimClassRefineOne
int Cec_ManSimClassRefineOne(Cec_ManSim_t *p, int i)
Definition: cecClass.c:268
Cec_ParSim_t_::fConstCorr
int fConstCorr
Definition: cec.h:71
Cec_ManSimCompareConstFirstBit
int Cec_ManSimCompareConstFirstBit(unsigned *p, int nWords)
Definition: cecClass.c:110
Cec_ManSim_t_::nWords
int nWords
Definition: cecInt.h:117
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
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
Cec_ManSim_t_::MemFree
int MemFree
Definition: cecInt.h:124
Cec_ManSim_t_::vCiSimInfo
Vec_Ptr_t * vCiSimInfo
Definition: cecInt.h:127
Gia_ClassForEachObj1
#define Gia_ClassForEachObj1(p, i, iObj)
Definition: gia.h:933
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
Cec_ManSimFindBestPattern
void Cec_ManSimFindBestPattern(Cec_ManSim_t *p)
Definition: cecClass.c:548
Cec_ManSim_t_::pCexes
void ** pCexes
Definition: cecInt.h:130
Cec_ManSim_t_::nMemsMax
int nMemsMax
Definition: cecInt.h:123
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Cec_ManSim_t_::nWordsOld
int nWordsOld
Definition: cecInt.h:125
Cec_ManSim_t_::vClassNew
Vec_Int_t * vClassNew
Definition: cecInt.h:139
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Cec_ManSim_t_::nWordsAlloc
int nWordsAlloc
Definition: cecInt.h:121
Cec_ManSimClassCreate
void Cec_ManSimClassCreate(Gia_Man_t *p, Vec_Int_t *vClass)
Definition: cecClass.c:234
Gia_ClassForEachObj
#define Gia_ClassForEachObj(p, i, iObj)
Definition: gia.h:931
Cec_ManSimAnalyzeOutputs
int Cec_ManSimAnalyzeOutputs(Cec_ManSim_t *p)
Definition: cecClass.c:584
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
Gia_ObjNext
static int Gia_ObjNext(Gia_Man_t *p, int Id)
Definition: gia.h:912
Cec_ManSimSavePattern
void Cec_ManSimSavePattern(Cec_ManSim_t *p, int iPat)
Definition: cecClass.c:518
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
Cec_ManSimHashKey
int Cec_ManSimHashKey(unsigned *pSim, int nWords, int nTableSize)
Definition: cecClass.c:350
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
Cec_ManSimCompareConst
int Cec_ManSimCompareConst(unsigned *p, int nWords)
FUNCTION DEFINITIONS ///.
Definition: cecClass.c:50
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Cec_ObjSim
static ABC_NAMESPACE_IMPL_START unsigned * Cec_ObjSim(Cec_ManSim_t *p, int Id)
DECLARATIONS ///.
Definition: cecClass.c:30
Cec_ManSimClassesRefine
int Cec_ManSimClassesRefine(Cec_ManSim_t *p)
Definition: cecClass.c:908
Gia_ObjIsTail
static int Gia_ObjIsTail(Gia_Man_t *p, int Id)
Definition: gia.h:918
Cec_ManSim_t_::pSimInfo
int * pSimInfo
Definition: cecInt.h:119
GIA_VOID
#define GIA_VOID
Definition: gia.h:45
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Cec_MemUsage
static float Cec_MemUsage(Cec_ManSim_t *p)
Definition: cecClass.c:33
Cec_ManSimCompareConstScore
void Cec_ManSimCompareConstScore(unsigned *p, int nWords, int *pScores)
Definition: cecClass.c:170
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Cec_ManSimCompareEqualFirstBit
int Cec_ManSimCompareEqualFirstBit(unsigned *p0, unsigned *p1, int nWords)
Definition: cecClass.c:140
Gia_Man_t_
Definition: gia.h:95
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Cec_ManSim_t_::pPars
Cec_ParSim_t * pPars
Definition: cecInt.h:116
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Cec_ManSim_t_::iOut
int iOut
Definition: cecInt.h:131
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Cec_ManSim_t_::vCoSimInfo
Vec_Ptr_t * vCoSimInfo
Definition: cecInt.h:128
Cec_ParSim_t_::fDualOut
int fDualOut
Definition: cec.h:66
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_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition: gia.h:121
Cec_ManSim_t_::vRefinedC
Vec_Int_t * vRefinedC
Definition: cecInt.h:141
assert
#define assert(ex)
Definition: util_old.h:213
Cec_ParSim_t_::nRounds
int nRounds
Definition: cec.h:63
Gia_ManLevelNum
int Gia_ManLevelNum(Gia_Man_t *p)
Definition: giaUtil.c:505
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_Man_t_::vLevels
Vec_Int_t * vLevels
Definition: gia.h:115
Cec_ManSimCompareEqual
int Cec_ManSimCompareEqual(unsigned *p0, unsigned *p1, int nWords)
Definition: cecClass.c:80
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
Cec_ManSim_t_::pBestState
Abc_Cex_t * pBestState
Definition: cecInt.h:134
Cec_ParSim_t_::nWords
int nWords
Definition: cec.h:61
Gia_Rpr_t_
Definition: gia.h:56
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Cec_ManSim_t_::vClassTemp
Vec_Int_t * vClassTemp
Definition: cecInt.h:140
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
Cec_ManSim_t_::nOuts
int nOuts
Definition: cecInt.h:132
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
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
Cec_ManSim_t_::pMems
unsigned * pMems
Definition: cecInt.h:120
Cec_ManSimClassRemoveOne
int Cec_ManSimClassRemoveOne(Cec_ManSim_t *p, int i)
Definition: cecClass.c:308
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
Cec_ManSimProcessRefined
void Cec_ManSimProcessRefined(Cec_ManSim_t *p, Vec_Int_t *vRefined)
Definition: cecClass.c:467
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Cec_ManSim_t_::vClassOld
Vec_Int_t * vClassOld
Definition: cecInt.h:138
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387