abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
sswRarity.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [sswRarity.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Inductive prover with constraints.]
8 
9  Synopsis [Rarity-driven refinement of equivalence classes.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - September 1, 2008.]
16 
17  Revision [$Id: sswRarity.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "sswInt.h"
22 #include "aig/gia/giaAig.h"
23 #include "base/main/main.h"
24 #include "sat/bmc/bmc.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 typedef struct Ssw_RarMan_t_ Ssw_RarMan_t;
34 struct Ssw_RarMan_t_
35 {
36  // parameters
37  Ssw_RarPars_t* pPars;
38  int nGroups; // the number of flop groups
39  int nWordsReg; // the number of words in the registers
40  // internal data
41  Aig_Man_t * pAig; // AIG with equivalence classes
42  Ssw_Cla_t * ppClasses; // equivalence classes
43  Vec_Int_t * vInits; // initial state
44  // simulation data
45  word * pObjData; // simulation info for each obj
46  word * pPatData; // pattern data for each reg
47  // candidates to update
48  Vec_Ptr_t * vUpdConst; // constant 1 candidates
49  Vec_Ptr_t * vUpdClass; // class representatives
50  // rarity data
51  int * pRarity; // occur counts for patterns in groups
52  double * pPatCosts; // pattern costs
53  // best patterns
54  Vec_Int_t * vPatBests; // best patterns
55  int iFailPo; // failed primary output
56  int iFailPat; // failed pattern
57  // counter-examples
58  Vec_Ptr_t * vCexes;
59 };
60 
61 
62 static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
63 {
64  assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize );
65  assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) );
66  return p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat];
67 }
68 static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value )
69 {
70  assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize );
71  assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) );
72  p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat] = Value;
73 }
74 static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
75 {
76  assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize );
77  assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) );
78  p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat]++;
79 }
80 
81 static inline int Ssw_RarBitWordNum( int nBits ) { return (nBits>>6) + ((nBits&63) > 0); }
82 
83 static inline word * Ssw_RarObjSim( Ssw_RarMan_t * p, int Id ) { assert( Id < Aig_ManObjNumMax(p->pAig) ); return p->pObjData + p->pPars->nWords * Id; }
84 static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 64 * p->pPars->nWords ); return p->pPatData + p->nWordsReg * Id; }
85 
86 
87 ////////////////////////////////////////////////////////////////////////
88 /// FUNCTION DEFINITIONS ///
89 ////////////////////////////////////////////////////////////////////////
90 
91 /**Function*************************************************************
92 
93  Synopsis []
94 
95  Description []
96 
97  SideEffects []
98 
99  SeeAlso []
100 
101 ***********************************************************************/
102 void Ssw_RarSetDefaultParams( Ssw_RarPars_t * p )
103 {
104  memset( p, 0, sizeof(Ssw_RarPars_t) );
105  p->nFrames = 20;
106  p->nWords = 50;
107  p->nBinSize = 8;
108  p->nRounds = 0;
109  p->nRestart = 0;
110  p->nRandSeed = 0;
111  p->TimeOut = 0;
112  p->TimeOutGap = 0;
113  p->fSolveAll = 0;
114  p->fDropSatOuts = 0;
115  p->fSetLastState = 0;
116  p->fVerbose = 0;
117  p->fNotVerbose = 0;
118 }
119 
120 /**Function*************************************************************
121 
122  Synopsis [Prepares random number generator.]
123 
124  Description []
125 
126  SideEffects []
127 
128  SeeAlso []
129 
130 ***********************************************************************/
131 void Ssw_RarManPrepareRandom( int nRandSeed )
132 {
133  int i;
134  Aig_ManRandom( 1 );
135  for ( i = 0; i < nRandSeed; i++ )
136  Aig_ManRandom( 0 );
137 }
138 
139 /**Function*************************************************************
140 
141  Synopsis [Initializes random primary inputs.]
142 
143  Description []
144 
145  SideEffects []
146 
147  SeeAlso []
148 
149 ***********************************************************************/
150 void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p )
151 {
152  word * pSim;
153  Aig_Obj_t * pObj;
154  int w, i;
155  Saig_ManForEachPi( p->pAig, pObj, i )
156  {
157  pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
158  for ( w = 0; w < p->pPars->nWords; w++ )
159  pSim[w] = Aig_ManRandom64(0);
160 // pSim[0] <<= 1;
161 // pSim[0] = (pSim[0] << 2) | 2;
162  pSim[0] = (pSim[0] << 4) | ((i & 1) ? 0xA : 0xC);
163  }
164 }
165 
166 /**Function*************************************************************
167 
168  Synopsis [Derives the counter-example.]
169 
170  Description []
171 
172  SideEffects []
173 
174  SeeAlso []
175 
176 ***********************************************************************/
177 Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFinal, int fVerbose )
178 {
179  Abc_Cex_t * pCex;
180  Aig_Obj_t * pObj;
181  Vec_Int_t * vTrace;
182  word * pSim;
183  int i, r, f, iBit, iPatThis;
184  // compute the pattern sequence
185  iPatThis = iPatFinal;
186  vTrace = Vec_IntStartFull( iFrame / p->pPars->nFrames + 1 );
187  Vec_IntWriteEntry( vTrace, iFrame / p->pPars->nFrames, iPatThis );
188  for ( r = iFrame / p->pPars->nFrames - 1; r >= 0; r-- )
189  {
190  iPatThis = Vec_IntEntry( p->vPatBests, r * p->pPars->nWords + iPatThis / 64 );
191  Vec_IntWriteEntry( vTrace, r, iPatThis );
192  }
193  // create counter-example
194  pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), iFrame+1 );
195  pCex->iFrame = iFrame;
196  pCex->iPo = iPo;
197  // insert the bits
198  iBit = Aig_ManRegNum(p->pAig);
199  for ( f = 0; f <= iFrame; f++ )
200  {
201  Ssw_RarManAssingRandomPis( p );
202  iPatThis = Vec_IntEntry( vTrace, f / p->pPars->nFrames );
203  Saig_ManForEachPi( p->pAig, pObj, i )
204  {
205  pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
206  if ( Abc_InfoHasBit( (unsigned *)pSim, iPatThis ) )
207  Abc_InfoSetBit( pCex->pData, iBit );
208  iBit++;
209  }
210  }
211  Vec_IntFree( vTrace );
212  assert( iBit == pCex->nBits );
213  // verify the counter example
214  if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
215  {
216  Abc_Print( 1, "Ssw_RarDeriveCex(): Counter-example is invalid.\n" );
217 // Abc_CexFree( pCex );
218 // pCex = NULL;
219  }
220  else
221  {
222 // Abc_Print( 1, "Counter-example verification is successful.\n" );
223  }
224  return pCex;
225 }
226 
227 
228 /**Function*************************************************************
229 
230  Synopsis [Transposing 32-bit matrix.]
231 
232  Description [Borrowed from "Hacker's Delight", by Henry Warren.]
233 
234  SideEffects []
235 
236  SeeAlso []
237 
238 ***********************************************************************/
239 void transpose32( unsigned A[32] )
240 {
241  int j, k;
242  unsigned t, m = 0x0000FFFF;
243  for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) )
244  {
245  for ( k = 0; k < 32; k = (k + j + 1) & ~j )
246  {
247  t = (A[k] ^ (A[k+j] >> j)) & m;
248  A[k] = A[k] ^ t;
249  A[k+j] = A[k+j] ^ (t << j);
250  }
251  }
252 }
253 
254 /**Function*************************************************************
255 
256  Synopsis [Transposing 64-bit matrix.]
257 
258  Description []
259 
260  SideEffects []
261 
262  SeeAlso []
263 
264 ***********************************************************************/
265 void transpose64( word A[64] )
266 {
267  int j, k;
268  word t, m = 0x00000000FFFFFFFF;
269  for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) )
270  {
271  for ( k = 0; k < 64; k = (k + j + 1) & ~j )
272  {
273  t = (A[k] ^ (A[k+j] >> j)) & m;
274  A[k] = A[k] ^ t;
275  A[k+j] = A[k+j] ^ (t << j);
276  }
277  }
278 }
279 
280 /**Function*************************************************************
281 
282  Synopsis [Transposing 64-bit matrix.]
283 
284  Description []
285 
286  SideEffects []
287 
288  SeeAlso []
289 
290 ***********************************************************************/
291 void transpose64Simple( word A[64], word B[64] )
292 {
293  int i, k;
294  for ( i = 0; i < 64; i++ )
295  B[i] = 0;
296  for ( i = 0; i < 64; i++ )
297  for ( k = 0; k < 64; k++ )
298  if ( (A[i] >> k) & 1 )
299  B[k] |= ((word)1 << (63-i));
300 }
301 
302 /**Function*************************************************************
303 
304  Synopsis [Testing the transposing code.]
305 
306  Description []
307 
308  SideEffects []
309 
310  SeeAlso []
311 
312 ***********************************************************************/
313 void TransposeTest()
314 {
315  word M[64], N[64];
316  int i;
317  abctime clk;
318  Aig_ManRandom64( 1 );
319 // for ( i = 0; i < 64; i++ )
320 // M[i] = Aig_ManRandom64( 0 );
321  for ( i = 0; i < 64; i++ )
322  M[i] = i? (word)0 : ~(word)0;
323 // for ( i = 0; i < 64; i++ )
324 // Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" );
325 
326  clk = Abc_Clock();
327  for ( i = 0; i < 100001; i++ )
328  transpose64Simple( M, N );
329  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
330 
331  clk = Abc_Clock();
332  for ( i = 0; i < 100001; i++ )
333  transpose64( M );
334  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
335 
336  for ( i = 0; i < 64; i++ )
337  if ( M[i] != N[i] )
338  Abc_Print( 1, "Mismatch\n" );
339 /*
340  Abc_Print( 1, "\n" );
341  for ( i = 0; i < 64; i++ )
342  Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" );
343  Abc_Print( 1, "\n" );
344  for ( i = 0; i < 64; i++ )
345  Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), Abc_Print( 1, "\n" );
346 */
347 }
348 
349 /**Function*************************************************************
350 
351  Synopsis [Transposing pObjData[ nRegs x nWords ] -> pPatData[ nWords x nRegs ].]
352 
353  Description []
354 
355  SideEffects []
356 
357  SeeAlso []
358 
359 ***********************************************************************/
360 void Ssw_RarTranspose( Ssw_RarMan_t * p )
361 {
362  Aig_Obj_t * pObj;
363  word M[64];
364  int w, r, i;
365  for ( w = 0; w < p->pPars->nWords; w++ )
366  for ( r = 0; r < p->nWordsReg; r++ )
367  {
368  // save input
369  for ( i = 0; i < 64; i++ )
370  {
371  if ( r*64 + 63-i < Aig_ManRegNum(p->pAig) )
372  {
373  pObj = Saig_ManLi( p->pAig, r*64 + 63-i );
374  M[i] = Ssw_RarObjSim( p, Aig_ObjId(pObj) )[w];
375  }
376  else
377  M[i] = 0;
378  }
379  // transpose
380  transpose64( M );
381  // save output
382  for ( i = 0; i < 64; i++ )
383  Ssw_RarPatSim( p, w*64 + 63-i )[r] = M[i];
384  }
385 /*
386  Saig_ManForEachLi( p->pAig, pObj, i )
387  {
388  word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
389  Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->pPars->nWords ); Abc_Print( 1, "\n" );
390  }
391  Abc_Print( 1, "\n" );
392  for ( i = 0; i < p->pPars->nWords*64; i++ )
393  {
394  word * pBitData = Ssw_RarPatSim( p, i );
395  Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); Abc_Print( 1, "\n" );
396  }
397  Abc_Print( 1, "\n" );
398 */
399 }
400 
401 
402 
403 
404 /**Function*************************************************************
405 
406  Synopsis [Sets random inputs and specialied flop outputs.]
407 
408  Description []
409 
410  SideEffects []
411 
412  SeeAlso []
413 
414 ***********************************************************************/
415 void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
416 {
417  Aig_Obj_t * pObj, * pObjLi;
418  word * pSim, * pSimLi;
419  int w, i;
420  // constant
421  pObj = Aig_ManConst1( p->pAig );
422  pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
423  for ( w = 0; w < p->pPars->nWords; w++ )
424  pSim[w] = ~(word)0;
425  // primary inputs
426  Ssw_RarManAssingRandomPis( p );
427  // flop outputs
428  if ( vInit )
429  {
430  assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->pPars->nWords );
431  Saig_ManForEachLo( p->pAig, pObj, i )
432  {
433  pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
434  for ( w = 0; w < p->pPars->nWords; w++ )
435  pSim[w] = Vec_IntEntry(vInit, w * Saig_ManRegNum(p->pAig) + i) ? ~(word)0 : (word)0;
436  }
437  }
438  else
439  {
440  Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i )
441  {
442  pSimLi = Ssw_RarObjSim( p, Aig_ObjId(pObjLi) );
443  pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
444  for ( w = 0; w < p->pPars->nWords; w++ )
445  pSim[w] = pSimLi[w];
446  }
447  }
448 }
449 
450 /**Function*************************************************************
451 
452  Synopsis [Returns 1 if simulation info is composed of all zeros.]
453 
454  Description []
455 
456  SideEffects []
457 
458  SeeAlso []
459 
460 ***********************************************************************/
461 int Ssw_RarManPoIsConst0( void * pMan, Aig_Obj_t * pObj )
462 {
463  Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
464  word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
465  int w;
466  for ( w = 0; w < p->pPars->nWords; w++ )
467  if ( pSim[w] )
468  return 0;
469  return 1;
470 }
471 
472 /**Function*************************************************************
473 
474  Synopsis [Returns 1 if simulation info is composed of all zeros.]
475 
476  Description []
477 
478  SideEffects []
479 
480  SeeAlso []
481 
482 ***********************************************************************/
483 int Ssw_RarManObjIsConst( void * pMan, Aig_Obj_t * pObj )
484 {
485  Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
486  word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
487  word Flip = pObj->fPhase ? ~(word)0 : 0;
488  int w;
489  for ( w = 0; w < p->pPars->nWords; w++ )
490  if ( pSim[w] ^ Flip )
491  return 0;
492  return 1;
493 }
494 
495 /**Function*************************************************************
496 
497  Synopsis [Returns 1 if simulation infos are equal.]
498 
499  Description []
500 
501  SideEffects []
502 
503  SeeAlso []
504 
505 ***********************************************************************/
506 int Ssw_RarManObjsAreEqual( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
507 {
508  Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
509  word * pSim0 = Ssw_RarObjSim( p, pObj0->Id );
510  word * pSim1 = Ssw_RarObjSim( p, pObj1->Id );
511  word Flip = (pObj0->fPhase != pObj1->fPhase) ? ~(word)0 : 0;
512  int w;
513  for ( w = 0; w < p->pPars->nWords; w++ )
514  if ( pSim0[w] ^ pSim1[w] ^ Flip )
515  return 0;
516  return 1;
517 }
518 
519 /**Function*************************************************************
520 
521  Synopsis [Computes hash value of the node using its simulation info.]
522 
523  Description []
524 
525  SideEffects []
526 
527  SeeAlso []
528 
529 ***********************************************************************/
530 unsigned Ssw_RarManObjHashWord( void * pMan, Aig_Obj_t * pObj )
531 {
532  Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
533  static int s_SPrimes[128] = {
534  1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
535  1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
536  2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
537  2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
538  3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
539  3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
540  4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
541  4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
542  5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
543  6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
544  6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
545  7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
546  8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
547  };
548  unsigned * pSims;
549  unsigned uHash;
550  int i;
551  uHash = 0;
552  pSims = (unsigned *)Ssw_RarObjSim( p, pObj->Id );
553  for ( i = 0; i < 2 * p->pPars->nWords; i++ )
554  uHash ^= pSims[i] * s_SPrimes[i & 0x7F];
555  return uHash;
556 }
557 
558 /**Function*************************************************************
559 
560  Synopsis [Returns 1 if simulation info is composed of all zeros.]
561 
562  Description []
563 
564  SideEffects []
565 
566  SeeAlso []
567 
568 ***********************************************************************/
569 int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
570 {
571  word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
572  word Flip = 0;//pObj->fPhase ? ~(word)0 : 0; // bug fix!
573  int w, i;
574  for ( w = 0; w < p->pPars->nWords; w++ )
575  if ( pSim[w] ^ Flip )
576  {
577  for ( i = 0; i < 64; i++ )
578  if ( ((pSim[w] ^ Flip) >> i) & 1 )
579  break;
580  assert( i < 64 );
581  return w * 64 + i;
582  }
583  return -1;
584 }
585 
586 /**Function*************************************************************
587 
588  Synopsis [Check if any of the POs becomes non-constant.]
589 
590  Description []
591 
592  SideEffects []
593 
594  SeeAlso []
595 
596 ***********************************************************************/
597 int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int iFrame, abctime Time )
598 {
599  Aig_Obj_t * pObj;
600  int i;
601  p->iFailPo = -1;
602  p->iFailPat = -1;
603  Saig_ManForEachPo( p->pAig, pObj, i )
604  {
605  if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
606  break;
607  if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
608  continue;
609  if ( Ssw_RarManPoIsConst0(p, pObj) )
610  continue;
611  p->iFailPo = i;
612  p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
613  if ( !p->pPars->fSolveAll )
614  break;
615  // remember the one solved
616  p->pPars->nSolved++;
617  if ( p->vCexes == NULL )
618  p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
619  assert( Vec_PtrEntry(p->vCexes, i) == NULL );
620  Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 );
621  if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(i, NULL) )
622  return 2; // quitting due to callback
623  // print final report
624  if ( !p->pPars->fNotVerbose )
625  {
626  int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
627  Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs). ",
628  nOutDigits, p->iFailPo, iFrame,
629  nOutDigits, p->pPars->nSolved,
630  nOutDigits, Saig_ManPoNum(p->pAig) );
631  Abc_PrintTime( 1, "Time", Time );
632  }
633  }
634  if ( p->iFailPo >= 0 ) // found CEX
635  return 1;
636  else
637  return 0;
638 }
639 
640 /**Function*************************************************************
641 
642  Synopsis [Performs one round of simulation.]
643 
644  Description []
645 
646  SideEffects []
647 
648  SeeAlso []
649 
650 ***********************************************************************/
651 void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int fFirst )
652 {
653  Aig_Obj_t * pObj, * pRepr;
654  word * pSim, * pSim0, * pSim1;
655  word Flip, Flip0, Flip1;
656  int w, i;
657  // initialize
658  Ssw_RarManInitialize( p, vInit );
659  Vec_PtrClear( p->vUpdConst );
660  Vec_PtrClear( p->vUpdClass );
661  Aig_ManIncrementTravId( p->pAig );
662  // check comb inputs
663  if ( fUpdate )
664  Aig_ManForEachCi( p->pAig, pObj, i )
665  {
666  pRepr = Aig_ObjRepr(p->pAig, pObj);
667  if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
668  continue;
669  if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
670  continue;
671  // save for update
672  if ( pRepr == Aig_ManConst1(p->pAig) )
673  Vec_PtrPush( p->vUpdConst, pObj );
674  else
675  {
676  Vec_PtrPush( p->vUpdClass, pRepr );
677  Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
678  }
679  }
680  // simulate
681  Aig_ManForEachNode( p->pAig, pObj, i )
682  {
683  pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
684  pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
685  pSim1 = Ssw_RarObjSim( p, Aig_ObjFaninId1(pObj) );
686  Flip0 = Aig_ObjFaninC0(pObj) ? ~(word)0 : 0;
687  Flip1 = Aig_ObjFaninC1(pObj) ? ~(word)0 : 0;
688  for ( w = 0; w < p->pPars->nWords; w++ )
689  pSim[w] = (Flip0 ^ pSim0[w]) & (Flip1 ^ pSim1[w]);
690 
691 
692  if ( !fUpdate )
693  continue;
694  // check classes
695  pRepr = Aig_ObjRepr(p->pAig, pObj);
696  if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
697  continue;
698  if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
699  continue;
700  // save for update
701  if ( pRepr == Aig_ManConst1(p->pAig) )
702  Vec_PtrPush( p->vUpdConst, pObj );
703  else
704  {
705  Vec_PtrPush( p->vUpdClass, pRepr );
706  Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
707  }
708  }
709  // transfer to POs
710  Aig_ManForEachCo( p->pAig, pObj, i )
711  {
712  pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
713  pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
714  Flip = Aig_ObjFaninC0(pObj) ? ~(word)0 : 0;
715  for ( w = 0; w < p->pPars->nWords; w++ )
716  pSim[w] = Flip ^ pSim0[w];
717  }
718  // refine classes
719  if ( fUpdate )
720  {
721  if ( fFirst )
722  {
723  Vec_Ptr_t * vCands = Vec_PtrAlloc( 1000 );
724  Aig_ManForEachObj( p->pAig, pObj, i )
725  if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
726  Vec_PtrPush( vCands, pObj );
727  assert( Vec_PtrSize(vCands) == Ssw_ClassesCand1Num(p->ppClasses) );
728  Ssw_ClassesPrepareRehash( p->ppClasses, vCands, 0 );
729  Vec_PtrFree( vCands );
730  }
731  else
732  {
733  Ssw_ClassesRefineConst1Group( p->ppClasses, p->vUpdConst, 1 );
734  Ssw_ClassesRefineGroup( p->ppClasses, p->vUpdClass, 1 );
735  }
736  }
737 }
738 
739 
740 /**Function*************************************************************
741 
742  Synopsis []
743 
744  Description []
745 
746  SideEffects []
747 
748  SeeAlso []
749 
750 ***********************************************************************/
751 static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
752 {
753  Ssw_RarMan_t * p;
754 // if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
755 // return NULL;
756  p = ABC_CALLOC( Ssw_RarMan_t, 1 );
757  p->pAig = pAig;
758  p->pPars = pPars;
759  p->nGroups = Aig_ManRegNum(pAig) / pPars->nBinSize;
760  p->pRarity = ABC_CALLOC( int, (1 << pPars->nBinSize) * p->nGroups );
761  p->pPatCosts = ABC_CALLOC( double, p->pPars->nWords * 64 );
762  p->nWordsReg = Ssw_RarBitWordNum( Aig_ManRegNum(pAig) );
763  p->pObjData = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->pPars->nWords );
764  p->pPatData = ABC_ALLOC( word, 64 * p->pPars->nWords * p->nWordsReg );
765  p->vUpdConst = Vec_PtrAlloc( 100 );
766  p->vUpdClass = Vec_PtrAlloc( 100 );
767  p->vPatBests = Vec_IntAlloc( 100 );
768  return p;
769 }
770 
771 /**Function*************************************************************
772 
773  Synopsis []
774 
775  Description []
776 
777  SideEffects []
778 
779  SeeAlso []
780 
781 ***********************************************************************/
782 static void Ssw_RarManStop( Ssw_RarMan_t * p )
783 {
784 // Vec_PtrFreeP( &p->vCexes );
785  if ( p->vCexes )
786  {
787  assert( p->pAig->vSeqModelVec == NULL );
788  p->pAig->vSeqModelVec = p->vCexes;
789  p->vCexes = NULL;
790  }
791  if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
792  Vec_IntFreeP( &p->vInits );
793  Vec_IntFreeP( &p->vPatBests );
794  Vec_PtrFreeP( &p->vUpdConst );
795  Vec_PtrFreeP( &p->vUpdClass );
796  ABC_FREE( p->pObjData );
797  ABC_FREE( p->pPatData );
798  ABC_FREE( p->pPatCosts );
799  ABC_FREE( p->pRarity );
800  ABC_FREE( p );
801 }
802 
803 /**Function*************************************************************
804 
805  Synopsis [Select best patterns.]
806 
807  Description []
808 
809  SideEffects []
810 
811  SeeAlso []
812 
813 ***********************************************************************/
814 static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
815 {
816 // Aig_Obj_t * pObj;
817  unsigned char * pData;
818  unsigned * pPattern;
819  int i, k, Value;
820 
821  // more data from regs to pats
822  Ssw_RarTranspose( p );
823 
824  // update counters
825  for ( k = 0; k < p->pPars->nWords * 64; k++ )
826  {
827  pData = (unsigned char *)Ssw_RarPatSim( p, k );
828  for ( i = 0; i < p->nGroups; i++ )
829  Ssw_RarAddToBinPat( p, i, pData[i] );
830  }
831 
832  // for each pattern
833  for ( k = 0; k < p->pPars->nWords * 64; k++ )
834  {
835  pData = (unsigned char *)Ssw_RarPatSim( p, k );
836  // find the cost of its values
837  p->pPatCosts[k] = 0.0;
838  for ( i = 0; i < p->nGroups; i++ )
839  {
840  Value = Ssw_RarGetBinPat( p, i, pData[i] );
841  assert( Value > 0 );
842  p->pPatCosts[k] += 1.0/(Value*Value);
843  }
844  // print the result
845 //Abc_Print( 1, "%3d : %9.6f\n", k, p->pPatCosts[k] );
846  }
847 
848  // choose as many as there are words
849  Vec_IntClear( vInits );
850  for ( i = 0; i < p->pPars->nWords; i++ )
851  {
852  // select the best
853  int iPatBest = -1;
854  double iCostBest = -ABC_INFINITY;
855  for ( k = 0; k < p->pPars->nWords * 64; k++ )
856  if ( iCostBest < p->pPatCosts[k] )
857  {
858  iCostBest = p->pPatCosts[k];
859  iPatBest = k;
860  }
861  // remove from costs
862  assert( iPatBest >= 0 );
863  p->pPatCosts[iPatBest] = -ABC_INFINITY;
864  // set the flops
865  pPattern = (unsigned *)Ssw_RarPatSim( p, iPatBest );
866  for ( k = 0; k < Aig_ManRegNum(p->pAig); k++ )
867  Vec_IntPush( vInits, Abc_InfoHasBit(pPattern, k) );
868 //Abc_Print( 1, "Best pattern %5d\n", iPatBest );
869  Vec_IntPush( p->vPatBests, iPatBest );
870  }
871  assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->pPars->nWords );
872 }
873 
874 
875 /**Function*************************************************************
876 
877  Synopsis [Performs fraiging for one node.]
878 
879  Description [Returns the fraiged node.]
880 
881  SideEffects []
882 
883  SeeAlso []
884 
885 ***********************************************************************/
886 static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
887 {
888  Vec_Int_t * vInit;
889  Aig_Obj_t * pObj, * pObjLi;
890  int f, i, iBit;
891  // assign register outputs
892  Saig_ManForEachLi( pAig, pObj, i )
893  pObj->fMarkB = Abc_InfoHasBit( pCex->pData, i );
894  // simulate the timeframes
895  iBit = pCex->nRegs;
896  for ( f = 0; f <= pCex->iFrame; f++ )
897  {
898  // set the PI simulation information
899  Aig_ManConst1(pAig)->fMarkB = 1;
900  Saig_ManForEachPi( pAig, pObj, i )
901  pObj->fMarkB = Abc_InfoHasBit( pCex->pData, iBit++ );
902  Saig_ManForEachLiLo( pAig, pObjLi, pObj, i )
903  pObj->fMarkB = pObjLi->fMarkB;
904  // simulate internal nodes
905  Aig_ManForEachNode( pAig, pObj, i )
906  pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
907  & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
908  // assign the COs
909  Aig_ManForEachCo( pAig, pObj, i )
910  pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
911  }
912  assert( iBit == pCex->nBits );
913  // check that the output failed as expected -- cannot check because it is not an SRM!
914 // pObj = Aig_ManCo( pAig, pCex->iPo );
915 // if ( pObj->fMarkB != 1 )
916 // Abc_Print( 1, "The counter-example does not refine the output.\n" );
917  // record the new pattern
918  vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) );
919  Saig_ManForEachLo( pAig, pObj, i )
920  {
921 //Abc_Print( 1, "%d", pObj->fMarkB );
922  Vec_IntPush( vInit, pObj->fMarkB );
923  }
924 //Abc_Print( 1, "\n" );
925  Aig_ManCleanMarkB( pAig );
926  return vInit;
927 }
928 
929 
930 /**Function*************************************************************
931 
932  Synopsis []
933 
934  Description []
935 
936  SideEffects []
937 
938  SeeAlso []
939 
940 ***********************************************************************/
941 int Ssw_RarCheckTrivial( Aig_Man_t * pAig, int fVerbose )
942 {
943  Aig_Obj_t * pObj;
944  int i;
945  Saig_ManForEachPo( pAig, pObj, i )
946  {
947  if ( pAig->nConstrs && i >= Saig_ManPoNum(pAig) - pAig->nConstrs )
948  return 0;
949  if ( pObj->fPhase )
950  {
951  ABC_FREE( pAig->pSeqModel );
952  pAig->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), 1 );
953  pAig->pSeqModel->iPo = i;
954  if ( fVerbose )
955  Abc_Print( 1, "Output %d is trivally SAT in frame 0. \n", i );
956  return 1;
957  }
958  }
959  return 0;
960 }
961 
962 /**Function*************************************************************
963 
964  Synopsis [Perform sequential simulation.]
965 
966  Description []
967 
968  SideEffects []
969 
970  SeeAlso []
971 
972 ***********************************************************************/
973 int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
974 {
975  int fTryBmc = 0;
976  int fMiter = 1;
977  Ssw_RarMan_t * p;
978  int r, f = -1;
979  abctime clk, clkTotal = Abc_Clock();
980  abctime nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
981  abctime timeLastSolved = 0;
982  int nNumRestart = 0;
983  int nSavedSeed = pPars->nRandSeed;
984  int RetValue = -1;
985  int iFrameFail = -1;
986  assert( Aig_ManRegNum(pAig) > 0 );
987  assert( Aig_ManConstrNum(pAig) == 0 );
988  ABC_FREE( pAig->pSeqModel );
989  // consider the case of empty AIG
990 // if ( Aig_ManNodeNum(pAig) == 0 )
991 // return -1;
992  // check trivially SAT miters
993 // if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) )
994 // return 0;
995  if ( pPars->fVerbose )
996  Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d restart, %d seed, and %d sec timeout.\n",
997  pPars->nWords, pPars->nFrames, pPars->nRounds, pPars->nRestart, pPars->nRandSeed, pPars->TimeOut );
998  // reset random numbers
999  Ssw_RarManPrepareRandom( nSavedSeed );
1000 
1001  // create manager
1002  p = Ssw_RarManStart( pAig, pPars );
1003  p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * pPars->nWords );
1004 
1005  // perform simulation rounds
1006  pPars->nSolved = 0;
1007  timeLastSolved = Abc_Clock();
1008  for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
1009  {
1010  clk = Abc_Clock();
1011  if ( fTryBmc )
1012  {
1013  Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits );
1014  Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0 );
1015 // if ( pNewAig->pSeqModel != NULL )
1016 // Abc_Print( 1, "BMC has found a counter-example in frame %d.\n", iFrameFail );
1017  Aig_ManStop( pNewAig );
1018  }
1019  // simulate
1020  for ( f = 0; f < pPars->nFrames; f++ )
1021  {
1022  Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
1023  if ( fMiter )
1024  {
1025  int Status = Ssw_RarManCheckNonConstOutputs(p, r * p->pPars->nFrames + f, Abc_Clock() - clkTotal);
1026  if ( Status == 2 )
1027  {
1028  Abc_Print( 1, "Quitting due to callback on fail.\n" );
1029  goto finish;
1030  }
1031  if ( Status == 1 ) // found CEX
1032  {
1033  RetValue = 0;
1034  if ( !pPars->fSolveAll )
1035  {
1036  if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
1037  // Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
1038  Ssw_RarManPrepareRandom( nSavedSeed );
1039  if ( pPars->fVerbose )
1040  Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
1041  pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, pPars->fVerbose );
1042  // print final report
1043  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
1044  Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
1045  goto finish;
1046  }
1047  timeLastSolved = Abc_Clock();
1048  }
1049  // else - did not find a counter example
1050  }
1051  // check timeout
1052  if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
1053  {
1054  if ( !pPars->fSilent )
1055  {
1056  if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
1057  Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved );
1058  Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut );
1059  }
1060  goto finish;
1061  }
1062  if ( pPars->TimeOutGap && timeLastSolved && Abc_Clock() > timeLastSolved + pPars->TimeOutGap * CLOCKS_PER_SEC )
1063  {
1064  if ( !pPars->fSilent )
1065  {
1066  if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
1067  Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved );
1068  Abc_Print( 1, "Reached gap timeout (%d sec).\n", pPars->TimeOutGap );
1069  }
1070  goto finish;
1071  }
1072  // check if all outputs are solved by now
1073  if ( pPars->fSolveAll && p->vCexes && Vec_PtrCountZero(p->vCexes) == 0 )
1074  goto finish;
1075  }
1076  // get initialization patterns
1077  if ( pPars->nRestart && r == pPars->nRestart )
1078  {
1079  r = -1;
1080  nSavedSeed = (nSavedSeed + 1) % 1000;
1081  Ssw_RarManPrepareRandom( nSavedSeed );
1082  Vec_IntFill( p->vInits, Aig_ManRegNum(pAig) * pPars->nWords, 0 );
1083  nNumRestart++;
1084  Vec_IntClear( p->vPatBests );
1085  // clean rarity info
1086 // memset( p->pRarity, 0, sizeof(int) * (1 << nBinSize) * p->nGroups );
1087  }
1088  else
1089  Ssw_RarTransferPatterns( p, p->vInits );
1090  // printout
1091  if ( pPars->fVerbose )
1092  {
1093  if ( pPars->fSolveAll )
1094  {
1095  Abc_Print( 1, "Starts =%6d ", nNumRestart );
1096  Abc_Print( 1, "Rounds =%6d ", nNumRestart * pPars->nRestart + ((r==-1)?0:r) );
1097  Abc_Print( 1, "Frames =%6d ", (nNumRestart * pPars->nRestart + r) * pPars->nFrames );
1098  Abc_Print( 1, "CEX =%6d (%6.2f %%) ", pPars->nSolved, 100.0*pPars->nSolved/Saig_ManPoNum(p->pAig) );
1099  Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
1100  }
1101  else
1102  Abc_Print( 1, "." );
1103  }
1104 
1105  }
1106 finish:
1107  if ( pPars->fSetLastState && p->vInits )
1108  {
1109  assert( Vec_IntSize(p->vInits) % Aig_ManRegNum(pAig) == 0 );
1110  Vec_IntShrink( p->vInits, Aig_ManRegNum(pAig) );
1111  pAig->pData = p->vInits; p->vInits = NULL;
1112  }
1113  if ( pPars->nSolved )
1114  {
1115 /*
1116  if ( !pPars->fSilent )
1117  {
1118  if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
1119  Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved, Saig_ManPoNum(p->pAig) );
1120  Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
1121  }
1122 */
1123  }
1124  else if ( r == pPars->nRounds && f == pPars->nFrames )
1125  {
1126  if ( !pPars->fSilent )
1127  {
1128  if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
1129  Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
1130  Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
1131  }
1132  }
1133  // cleanup
1134  Ssw_RarManStop( p );
1135  return RetValue;
1136 }
1137 
1138 
1139 /**Function*************************************************************
1140 
1141  Synopsis [Derive random flop permutation.]
1142 
1143  Description []
1144 
1145  SideEffects []
1146 
1147  SeeAlso []
1148 
1149 ***********************************************************************/
1150 Vec_Int_t * Ssw_RarRandomPermFlop( int nFlops, int nUnused )
1151 {
1152  Vec_Int_t * vPerm;
1153  int i, k, * pArray;
1154  srand( 1 );
1155  printf( "Generating random permutation of %d flops.\n", nFlops );
1156  vPerm = Vec_IntStartNatural( nFlops );
1157  pArray = Vec_IntArray( vPerm );
1158  for ( i = 0; i < nFlops; i++ )
1159  {
1160  k = rand() % nFlops;
1161  ABC_SWAP( int, pArray[i], pArray[k] );
1162  }
1163  printf( "Randomly adding %d unused flops.\n", nUnused );
1164  for ( i = 0; i < nUnused; i++ )
1165  {
1166  k = rand() % Vec_IntSize(vPerm);
1167  Vec_IntPush( vPerm, -1 );
1168  pArray = Vec_IntArray( vPerm );
1169  ABC_SWAP( int, pArray[Vec_IntSize(vPerm)-1], pArray[k] );
1170  }
1171 // Vec_IntPrint(vPerm);
1172  return vPerm;
1173 }
1174 
1175 /**Function*************************************************************
1176 
1177  Synopsis [Perform sequential simulation.]
1178 
1179  Description []
1180 
1181  SideEffects []
1182 
1183  SeeAlso []
1184 
1185 ***********************************************************************/
1186 int Ssw_RarSimulateGia( Gia_Man_t * p, Ssw_RarPars_t * pPars )
1187 {
1188  Aig_Man_t * pAig;
1189  int RetValue;
1190  if ( pPars->fUseFfGrouping )
1191  {
1192  Vec_Int_t * vPerm = Ssw_RarRandomPermFlop( Gia_ManRegNum(p), 10 );
1193  Gia_Man_t * pTemp = Gia_ManDupPermFlopGap( p, vPerm );
1194  Vec_IntFree( vPerm );
1195  pAig = Gia_ManToAigSimple( pTemp );
1196  Gia_ManStop( pTemp );
1197  }
1198  else
1199  pAig = Gia_ManToAigSimple( p );
1200  RetValue = Ssw_RarSimulate( pAig, pPars );
1201  // save counter-example
1202  Abc_CexFree( p->pCexSeq );
1203  p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
1204  Aig_ManStop( pAig );
1205  return RetValue;
1206 }
1207 
1208 /**Function*************************************************************
1209 
1210  Synopsis [Filter equivalence classes of nodes.]
1211 
1212  Description []
1213 
1214  SideEffects []
1215 
1216  SeeAlso []
1217 
1218 ***********************************************************************/
1219 int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
1220 {
1221  Ssw_RarMan_t * p;
1222  int r, f = -1, i, k;
1223  abctime clkTotal = Abc_Clock();
1224  abctime nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
1225  int nNumRestart = 0;
1226  int nSavedSeed = pPars->nRandSeed;
1227  int RetValue = -1;
1228  assert( Aig_ManRegNum(pAig) > 0 );
1229  assert( Aig_ManConstrNum(pAig) == 0 );
1230  // consider the case of empty AIG
1231  if ( Aig_ManNodeNum(pAig) == 0 )
1232  return -1;
1233  // check trivially SAT miters
1234  if ( pPars->fMiter && Ssw_RarCheckTrivial( pAig, 1 ) )
1235  return 0;
1236  if ( pPars->fVerbose )
1237  Abc_Print( 1, "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
1238  pPars->nWords, pPars->nFrames, pPars->nRounds, pPars->nRandSeed, pPars->TimeOut );
1239  // reset random numbers
1240  Ssw_RarManPrepareRandom( nSavedSeed );
1241 
1242  // create manager
1243  p = Ssw_RarManStart( pAig, pPars );
1244  // compute starting state if needed
1245  assert( p->vInits == NULL );
1246  if ( pPars->pCex )
1247  {
1248  p->vInits = Ssw_RarFindStartingState( pAig, pPars->pCex );
1249  Abc_Print( 1, "Beginning simulation from the state derived using the counter-example.\n" );
1250  }
1251  else
1252  p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) );
1253  // duplicate the array
1254  for ( i = 1; i < pPars->nWords; i++ )
1255  for ( k = 0; k < Aig_ManRegNum(pAig); k++ )
1256  Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) );
1257  assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * pPars->nWords );
1258 
1259  // create trivial equivalence classes with all nodes being candidates for constant 1
1260  if ( pAig->pReprs == NULL )
1261  p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchOnly, 0 );
1262  else
1263  p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
1264  Ssw_ClassesSetData( p->ppClasses, p, Ssw_RarManObjHashWord, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual );
1265  // print the stats
1266  if ( pPars->fVerbose )
1267  {
1268  Abc_Print( 1, "Initial : " );
1269  Ssw_ClassesPrint( p->ppClasses, 0 );
1270  }
1271  // refine classes using BMC
1272  for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
1273  {
1274  // start filtering equivalence classes
1275  if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
1276  {
1277  Abc_Print( 1, "All equivalences are refined away.\n" );
1278  break;
1279  }
1280  // simulate
1281  for ( f = 0; f < pPars->nFrames; f++ )
1282  {
1283  Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
1284  if ( pPars->fMiter && Ssw_RarManCheckNonConstOutputs(p, -1, 0) )
1285  {
1286  if ( !pPars->fVerbose )
1287  Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
1288 // Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * pPars->nFrames, (r+1) * pPars->nFrames );
1289  if ( pPars->fVerbose )
1290  Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
1291  Ssw_RarManPrepareRandom( nSavedSeed );
1292  Abc_CexFree( pAig->pSeqModel );
1293  pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, 1 );
1294  // print final report
1295  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
1296  Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
1297  RetValue = 0;
1298  goto finish;
1299  }
1300  // check timeout
1301  if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
1302  {
1303  if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
1304  Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
1305  Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut );
1306  goto finish;
1307  }
1308  }
1309  // get initialization patterns
1310  if ( pPars->pCex == NULL && pPars->nRestart && r == pPars->nRestart )
1311  {
1312  r = -1;
1313  nSavedSeed = (nSavedSeed + 1) % 1000;
1314  Ssw_RarManPrepareRandom( nSavedSeed );
1315  Vec_IntFill( p->vInits, Aig_ManRegNum(pAig) * pPars->nWords, 0 );
1316  nNumRestart++;
1317  Vec_IntClear( p->vPatBests );
1318  // clean rarity info
1319 // memset( p->pRarity, 0, sizeof(int) * (1 << nBinSize) * p->nGroups );
1320  }
1321  else
1322  Ssw_RarTransferPatterns( p, p->vInits );
1323  // printout
1324  if ( pPars->fVerbose )
1325  {
1326  Abc_Print( 1, "Round %3d: ", r );
1327  Ssw_ClassesPrint( p->ppClasses, 0 );
1328  }
1329  else
1330  {
1331  Abc_Print( 1, "." );
1332  }
1333  }
1334 finish:
1335  // report
1336  if ( r == pPars->nRounds && f == pPars->nFrames )
1337  {
1338  if ( !pPars->fVerbose )
1339  Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
1340  Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
1341  Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
1342  }
1343  // cleanup
1344  Ssw_RarManStop( p );
1345  return RetValue;
1346 }
1347 
1348 /**Function*************************************************************
1349 
1350  Synopsis [Filter equivalence classes of nodes.]
1351 
1352  Description []
1353 
1354  SideEffects []
1355 
1356  SeeAlso []
1357 
1358 ***********************************************************************/
1359 int Ssw_RarSignalFilterGia( Gia_Man_t * p, Ssw_RarPars_t * pPars )
1360 {
1361  Aig_Man_t * pAig;
1362  int RetValue;
1363  pAig = Gia_ManToAigSimple( p );
1364  if ( p->pReprs != NULL )
1365  {
1366  Gia_ManReprToAigRepr2( pAig, p );
1367  ABC_FREE( p->pReprs );
1368  ABC_FREE( p->pNexts );
1369  }
1370  RetValue = Ssw_RarSignalFilter( pAig, pPars );
1371  Gia_ManReprFromAigRepr( pAig, p );
1372  // save counter-example
1373  Abc_CexFree( p->pCexSeq );
1374  p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
1375  Aig_ManStop( pAig );
1376  return RetValue;
1377 }
1378 
1379 
1380 ////////////////////////////////////////////////////////////////////////
1381 /// END OF FILE ///
1382 ////////////////////////////////////////////////////////////////////////
1383 
1384 
1385 ABC_NAMESPACE_IMPL_END
memset
char * memset()
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Vec_PtrStart
static Vec_Ptr_t * Vec_PtrStart(int nSize)
Definition: vecPtr.h:106
Ssw_RarFindStartingState
static Vec_Int_t * Ssw_RarFindStartingState(Aig_Man_t *pAig, Abc_Cex_t *pCex)
Definition: sswRarity.c:886
Ssw_RarManInitialize
void Ssw_RarManInitialize(Ssw_RarMan_t *p, Vec_Int_t *vInit)
Definition: sswRarity.c:415
Ssw_RarPars_t_::fSetLastState
int fSetLastState
Definition: ssw.h:101
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Ssw_ClassesRefineGroup
int Ssw_ClassesRefineGroup(Ssw_Cla_t *p, Vec_Ptr_t *vReprs, int fRecursive)
Definition: sswClass.c:1054
Ssw_ClassesClassNum
int Ssw_ClassesClassNum(Ssw_Cla_t *p)
Definition: sswClass.c:275
Aig_ObjRepr
static Aig_Obj_t * Aig_ObjRepr(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:330
Aig_ObjFaninId0
static int Aig_ObjFaninId0(Aig_Obj_t *pObj)
Definition: aig.h:304
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Ssw_RarPars_t_::nFrames
int nFrames
Definition: ssw.h:92
Aig_ManConstrNum
static int Aig_ManConstrNum(Aig_Man_t *p)
Definition: aig.h:261
Gia_ManReprFromAigRepr
void Gia_ManReprFromAigRepr(Aig_Man_t *pAig, Gia_Man_t *pGia)
Definition: giaAig.c:487
Gia_Man_t_::pNexts
int * pNexts
Definition: gia.h:122
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
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
transpose32
void transpose32(unsigned A[32])
Definition: sswRarity.c:239
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
Ssw_ClassesCand1Num
int Ssw_ClassesCand1Num(Ssw_Cla_t *p)
Definition: sswClass.c:259
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Ssw_RarSetDefaultParams
void Ssw_RarSetDefaultParams(Ssw_RarPars_t *p)
FUNCTION DEFINITIONS ///.
Definition: sswRarity.c:102
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Saig_ManVerifyCex
int Saig_ManVerifyCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:279
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition: aig.h:80
Abc_FrameIsBatchMode
ABC_DLL int Abc_FrameIsBatchMode()
Definition: mainFrame.c:92
Ssw_RarManObjHashWord
unsigned Ssw_RarManObjHashWord(void *pMan, Aig_Obj_t *pObj)
Definition: sswRarity.c:530
Ssw_RarManSimulate
void Ssw_RarManSimulate(Ssw_RarMan_t *p, Vec_Int_t *vInit, int fUpdate, int fFirst)
Definition: sswRarity.c:651
Ssw_RarManStop
static void Ssw_RarManStop(Ssw_RarMan_t *p)
Definition: sswRarity.c:782
Ssw_RarMan_t_::pAig
Aig_Man_t * pAig
Definition: sswRarity.c:41
Ssw_RarRandomPermFlop
Vec_Int_t * Ssw_RarRandomPermFlop(int nFlops, int nUnused)
Definition: sswRarity.c:1150
Ssw_RarPars_t_::TimeOutGap
int TimeOutGap
Definition: ssw.h:99
Ssw_RarObjSim
static word * Ssw_RarObjSim(Ssw_RarMan_t *p, int Id)
Definition: sswRarity.c:83
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Ssw_RarMan_t_::vUpdClass
Vec_Ptr_t * vUpdClass
Definition: sswRarity.c:49
Ssw_ClassesRefineConst1Group
int Ssw_ClassesRefineConst1Group(Ssw_Cla_t *p, Vec_Ptr_t *vRoots, int fRecursive)
Definition: sswClass.c:1074
Aig_ManCleanMarkB
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition: aigUtil.c:167
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Ssw_RarMan_t_::nGroups
int nGroups
Definition: sswRarity.c:38
Ssw_RarManObjWhichOne
int Ssw_RarManObjWhichOne(Ssw_RarMan_t *p, Aig_Obj_t *pObj)
Definition: sswRarity.c:569
Ssw_ClassesStop
void Ssw_ClassesStop(Ssw_Cla_t *p)
Definition: sswClass.c:189
Ssw_ClassesPrepareRehash
int Ssw_ClassesPrepareRehash(Ssw_Cla_t *p, Vec_Ptr_t *vCands, int fConstCorr)
Definition: sswClass.c:500
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Ssw_RarPars_t_::fSilent
int fSilent
Definition: ssw.h:104
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Saig_BmcPerform
int Saig_BmcPerform(Aig_Man_t *pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int *piFrames, int fSilent)
Definition: bmcBmc2.c:761
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Aig_ManRandom64
word Aig_ManRandom64(int fReset)
Definition: aigUtil.c:1182
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
Aig_ObjFaninId1
static int Aig_ObjFaninId1(Aig_Obj_t *pObj)
Definition: aig.h:305
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Ssw_RarMan_t_::vCexes
Vec_Ptr_t * vCexes
Definition: sswRarity.c:58
Ssw_RarManStart
static Ssw_RarMan_t * Ssw_RarManStart(Aig_Man_t *pAig, Ssw_RarPars_t *pPars)
Definition: sswRarity.c:751
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Vec_IntStartNatural
static Vec_Int_t * Vec_IntStartNatural(int nSize)
Definition: bblif.c:192
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
M
word M(word f1, word f2, int n)
Definition: kitPerm.c:240
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Ssw_RarManAssingRandomPis
void Ssw_RarManAssingRandomPis(Ssw_RarMan_t *p)
Definition: sswRarity.c:150
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition: abc_global.h:218
Ssw_RarPars_t_::fNotVerbose
int fNotVerbose
Definition: ssw.h:103
Ssw_RarTransferPatterns
static void Ssw_RarTransferPatterns(Ssw_RarMan_t *p, Vec_Int_t *vInits)
Definition: sswRarity.c:814
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Ssw_RarPars_t_::pCex
Abc_Cex_t * pCex
Definition: ssw.h:111
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Ssw_RarTranspose
void Ssw_RarTranspose(Ssw_RarMan_t *p)
Definition: sswRarity.c:360
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Gia_ManReprToAigRepr2
void Gia_ManReprToAigRepr2(Aig_Man_t *pAig, Gia_Man_t *pGia)
Definition: giaAig.c:459
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Ssw_RarMan_t_::nWordsReg
int nWordsReg
Definition: sswRarity.c:39
transpose64Simple
void transpose64Simple(word A[64], word B[64])
Definition: sswRarity.c:291
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Ssw_RarPars_t_::nSolved
int nSolved
Definition: ssw.h:110
Ssw_ClassesSetData
void Ssw_ClassesSetData(Ssw_Cla_t *p, void *pManData, unsigned(*pFuncNodeHash)(void *, Aig_Obj_t *), int(*pFuncNodeIsConst)(void *, Aig_Obj_t *), int(*pFuncNodesAreEqual)(void *, Aig_Obj_t *, Aig_Obj_t *))
Definition: sswClass.c:167
Ssw_ClassesPrint
void Ssw_ClassesPrint(Ssw_Cla_t *p, int fVeryVerbose)
Definition: sswClass.c:414
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Abc_Base10Log
static int Abc_Base10Log(unsigned n)
Definition: abc_global.h:252
Ssw_RarPars_t_::fVerbose
int fVerbose
Definition: ssw.h:102
Ssw_RarManPoIsConst0
int Ssw_RarManPoIsConst0(void *pMan, Aig_Obj_t *pObj)
Definition: sswRarity.c:461
Ssw_RarMan_t_::pObjData
word * pObjData
Definition: sswRarity.c:45
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Ssw_RarPars_t_::TimeOut
int TimeOut
Definition: ssw.h:98
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Ssw_RarMan_t_::pPars
Ssw_RarPars_t * pPars
Definition: sswRarity.c:37
Ssw_RarPars_t_::nRestart
int nRestart
Definition: ssw.h:96
Saig_ManLi
static Aig_Obj_t * Saig_ManLi(Aig_Man_t *p, int i)
Definition: saig.h:80
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Ssw_RarPars_t_::fLatchOnly
int fLatchOnly
Definition: ssw.h:108
Ssw_RarCheckTrivial
int Ssw_RarCheckTrivial(Aig_Man_t *pAig, int fVerbose)
Definition: sswRarity.c:941
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Ssw_Cla_t_
Definition: sswClass.c:36
Ssw_RarSetBinPat
static void Ssw_RarSetBinPat(Ssw_RarMan_t *p, int iBin, int iPat, int Value)
Definition: sswRarity.c:68
Saig_ManDupWithPhase
Aig_Man_t * Saig_ManDupWithPhase(Aig_Man_t *pAig, Vec_Int_t *vInit)
Definition: saigDup.c:480
Ssw_RarSimulateGia
int Ssw_RarSimulateGia(Gia_Man_t *p, Ssw_RarPars_t *pPars)
Definition: sswRarity.c:1186
Ssw_RarMan_t
typedefABC_NAMESPACE_IMPL_START struct Ssw_RarMan_t_ Ssw_RarMan_t
DECLARATIONS ///.
Definition: sswRarity.c:33
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Ssw_RarManCheckNonConstOutputs
int Ssw_RarManCheckNonConstOutputs(Ssw_RarMan_t *p, int iFrame, abctime Time)
Definition: sswRarity.c:597
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Ssw_RarManObjIsConst
int Ssw_RarManObjIsConst(void *pMan, Aig_Obj_t *pObj)
Definition: sswRarity.c:483
Vec_PtrCountZero
static int Vec_PtrCountZero(Vec_Ptr_t *p)
Definition: vecPtr.h:343
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
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Ssw_RarMan_t_::ppClasses
Ssw_Cla_t * ppClasses
Definition: sswRarity.c:42
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Ssw_ClassesPrepareFromReprs
Ssw_Cla_t * Ssw_ClassesPrepareFromReprs(Aig_Man_t *pAig)
Definition: sswClass.c:768
Ssw_RarPars_t_::nWords
int nWords
Definition: ssw.h:93
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Ssw_RarMan_t_::vInits
Vec_Int_t * vInits
Definition: sswRarity.c:43
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
Ssw_RarManObjsAreEqual
int Ssw_RarManObjsAreEqual(void *pMan, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition: sswRarity.c:506
Ssw_ClassesPrepareSimple
Ssw_Cla_t * Ssw_ClassesPrepareSimple(Aig_Man_t *pAig, int fLatchCorr, int nMaxLevs)
Definition: sswClass.c:724
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
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Ssw_RarSignalFilterGia
int Ssw_RarSignalFilterGia(Gia_Man_t *p, Ssw_RarPars_t *pPars)
Definition: sswRarity.c:1359
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
Ssw_RarMan_t_::pPatData
word * pPatData
Definition: sswRarity.c:46
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
Ssw_RarSimulate
int Ssw_RarSimulate(Aig_Man_t *pAig, Ssw_RarPars_t *pPars)
Definition: sswRarity.c:973
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
Ssw_RarMan_t_::iFailPat
int iFailPat
Definition: sswRarity.c:56
Ssw_RarPars_t_::fSolveAll
int fSolveAll
Definition: ssw.h:100
Ssw_ObjIsConst1Cand
static int Ssw_ObjIsConst1Cand(Aig_Man_t *pAig, Aig_Obj_t *pObj)
Definition: sswInt.h:172
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Vec_PtrFreeP
static void Vec_PtrFreeP(Vec_Ptr_t **p)
Definition: vecPtr.h:240
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Ssw_RarMan_t_
Definition: sswRarity.c:34
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
Ssw_RarMan_t_::pRarity
int * pRarity
Definition: sswRarity.c:51
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition: gia.h:121
assert
#define assert(ex)
Definition: util_old.h:213
Ssw_RarPatSim
static word * Ssw_RarPatSim(Ssw_RarMan_t *p, int Id)
Definition: sswRarity.c:84
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
transpose64
void transpose64(word A[64])
Definition: sswRarity.c:265
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Ssw_RarPars_t_
Definition: ssw.h:90
Ssw_RarMan_t_::pPatCosts
double * pPatCosts
Definition: sswRarity.c:52
Ssw_RarMan_t_::vUpdConst
Vec_Ptr_t * vUpdConst
Definition: sswRarity.c:48
Ssw_RarMan_t_::vPatBests
Vec_Int_t * vPatBests
Definition: sswRarity.c:54
Ssw_RarPars_t_::nRandSeed
int nRandSeed
Definition: ssw.h:97
TransposeTest
void TransposeTest()
Definition: sswRarity.c:313
Ssw_RarSignalFilter
int Ssw_RarSignalFilter(Aig_Man_t *pAig, Ssw_RarPars_t *pPars)
Definition: sswRarity.c:1219
Ssw_RarPars_t_::fMiter
int fMiter
Definition: ssw.h:106
Ssw_RarPars_t_::fUseFfGrouping
int fUseFfGrouping
Definition: ssw.h:109
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition: utilCex.c:371
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Ssw_RarPars_t_::fDropSatOuts
int fDropSatOuts
Definition: ssw.h:105
Gia_ManDupPermFlopGap
Gia_Man_t * Gia_ManDupPermFlopGap(Gia_Man_t *p, Vec_Int_t *vFfPerm)
Definition: giaDup.c:725
Ssw_RarGetBinPat
static int Ssw_RarGetBinPat(Ssw_RarMan_t *p, int iBin, int iPat)
Definition: sswRarity.c:62
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Ssw_RarDeriveCex
Abc_Cex_t * Ssw_RarDeriveCex(Ssw_RarMan_t *p, int iFrame, int iPo, int iPatFinal, int fVerbose)
Definition: sswRarity.c:177
Ssw_RarManPrepareRandom
void Ssw_RarManPrepareRandom(int nRandSeed)
Definition: sswRarity.c:131
Ssw_RarBitWordNum
static int Ssw_RarBitWordNum(int nBits)
Definition: sswRarity.c:81
Ssw_RarPars_t_::nRounds
int nRounds
Definition: ssw.h:95
Ssw_RarPars_t_::nBinSize
int nBinSize
Definition: ssw.h:94
Ssw_RarAddToBinPat
static void Ssw_RarAddToBinPat(Ssw_RarMan_t *p, int iBin, int iPat)
Definition: sswRarity.c:74
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
Ssw_RarMan_t_::iFailPo
int iFailPo
Definition: sswRarity.c:55
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