abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cecCorr.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [cecCorr.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Combinational equivalence checking.]
8 
9  Synopsis [Latch/signal correspondence computation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: cecCorr.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 void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
31 
32 ////////////////////////////////////////////////////////////////////////
33 /// FUNCTION DEFINITIONS ///
34 ////////////////////////////////////////////////////////////////////////
35 
36 /**Function*************************************************************
37 
38  Synopsis [Computes the real value of the literal w/o spec reduction.]
39 
40  Description []
41 
42  SideEffects []
43 
44  SeeAlso []
45 
46 ***********************************************************************/
47 static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
48 {
49  if ( Gia_ObjIsAnd(pObj) )
50  {
51  Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f, nPrefix );
52  Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f, nPrefix );
53  return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) );
54  }
55  if ( f == 0 )
56  {
57  assert( Gia_ObjIsRo(p, pObj) );
58  return Gia_ObjCopyF(p, f, pObj);
59  }
60  assert( f && Gia_ObjIsRo(p, pObj) );
61  pObj = Gia_ObjRoToRi( p, pObj );
62  Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1, nPrefix );
63  return Gia_ObjFanin0CopyF( p, f-1, pObj );
64 }
65 
66 /**Function*************************************************************
67 
68  Synopsis [Recursively performs speculative reduction for the object.]
69 
70  Description []
71 
72  SideEffects []
73 
74  SeeAlso []
75 
76 ***********************************************************************/
77 void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
78 {
79  Gia_Obj_t * pRepr;
80  int iLitNew;
81  if ( ~Gia_ObjCopyF(p, f, pObj) )
82  return;
83  if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
84  {
85  Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f, nPrefix );
86  iLitNew = Abc_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
87  Gia_ObjSetCopyF( p, f, pObj, iLitNew );
88  return;
89  }
90  assert( Gia_ObjIsCand(pObj) );
91  iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
92  Gia_ObjSetCopyF( p, f, pObj, iLitNew );
93 }
94 
95 /**Function*************************************************************
96 
97  Synopsis [Derives SRM for signal correspondence.]
98 
99  Description []
100 
101  SideEffects []
102 
103  SeeAlso []
104 
105 ***********************************************************************/
106 Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
107 {
108  Gia_Man_t * pNew, * pTemp;
109  Gia_Obj_t * pObj, * pRepr;
110  Vec_Int_t * vXorLits;
111  int f, i, iPrev, iObj, iPrevNew, iObjNew;
112  assert( nFrames > 0 );
113  assert( Gia_ManRegNum(p) > 0 );
114  assert( p->pReprs != NULL );
115  Vec_IntFill( &p->vCopies, (nFrames+fScorr)*Gia_ManObjNum(p), -1 );
116  Gia_ManSetPhase( p );
117  pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
118  pNew->pName = Abc_UtilStrsav( p->pName );
119  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
120  Gia_ManHashAlloc( pNew );
121  Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 );
122  Gia_ManForEachRo( p, pObj, i )
123  Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) );
124  Gia_ManForEachRo( p, pObj, i )
125  if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
126  Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) );
127  for ( f = 0; f < nFrames+fScorr; f++ )
128  {
129  Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
130  Gia_ManForEachPi( p, pObj, i )
131  Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
132  }
133  *pvOutputs = Vec_IntAlloc( 1000 );
134  vXorLits = Vec_IntAlloc( 1000 );
135  if ( fRings )
136  {
137  Gia_ManForEachObj1( p, pObj, i )
138  {
139  if ( Gia_ObjIsConst( p, i ) )
140  {
141  iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
142  iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
143  if ( iObjNew != 0 )
144  {
145  Vec_IntPush( *pvOutputs, 0 );
146  Vec_IntPush( *pvOutputs, i );
147  Vec_IntPush( vXorLits, iObjNew );
148  }
149  }
150  else if ( Gia_ObjIsHead( p, i ) )
151  {
152  iPrev = i;
153  Gia_ClassForEachObj1( p, i, iObj )
154  {
155  iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
156  iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
157  iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
158  iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
159  if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
160  {
161  Vec_IntPush( *pvOutputs, iPrev );
162  Vec_IntPush( *pvOutputs, iObj );
163  Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
164  }
165  iPrev = iObj;
166  }
167  iObj = i;
168  iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
169  iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
170  iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
171  iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
172  if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
173  {
174  Vec_IntPush( *pvOutputs, iPrev );
175  Vec_IntPush( *pvOutputs, iObj );
176  Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
177  }
178  }
179  }
180  }
181  else
182  {
183  Gia_ManForEachObj1( p, pObj, i )
184  {
185  pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
186  if ( pRepr == NULL )
187  continue;
188  iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 );
189  iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
190  iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
191  if ( iPrevNew != iObjNew )
192  {
193  Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
194  Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
195  Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
196  }
197  }
198  }
199  Vec_IntForEachEntry( vXorLits, iObjNew, i )
200  Gia_ManAppendCo( pNew, iObjNew );
201  Vec_IntFree( vXorLits );
202  Gia_ManHashStop( pNew );
203  Vec_IntErase( &p->vCopies );
204 //Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
205  pNew = Gia_ManCleanup( pTemp = pNew );
206 //Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );
207  Gia_ManStop( pTemp );
208  return pNew;
209 }
210 
211 
212 /**Function*************************************************************
213 
214  Synopsis [Derives SRM for signal correspondence.]
215 
216  Description []
217 
218  SideEffects []
219 
220  SeeAlso []
221 
222 ***********************************************************************/
223 Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
224 {
225  Gia_Man_t * pNew, * pTemp;
226  Gia_Obj_t * pObj, * pRepr;
227  Vec_Int_t * vXorLits;
228  int f, i, iPrevNew, iObjNew;
229  assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
230  assert( Gia_ManRegNum(p) > 0 );
231  assert( p->pReprs != NULL );
232  Vec_IntFill( &p->vCopies, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p), -1 );
233  Gia_ManSetPhase( p );
234  pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
235  pNew->pName = Abc_UtilStrsav( p->pName );
236  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
237  Gia_ManHashAlloc( pNew );
238  Gia_ManForEachRo( p, pObj, i )
239  {
240  Gia_ManAppendCi(pNew);
241  Gia_ObjSetCopyF( p, 0, pObj, 0 );
242  }
243  for ( f = 0; f < nFrames+nPrefix+fScorr; f++ )
244  {
245  Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
246  Gia_ManForEachPi( p, pObj, i )
247  Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
248  }
249  *pvOutputs = Vec_IntAlloc( 1000 );
250  vXorLits = Vec_IntAlloc( 1000 );
251  for ( f = nPrefix; f < nFrames+nPrefix; f++ )
252  {
253  Gia_ManForEachObj1( p, pObj, i )
254  {
255  pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
256  if ( pRepr == NULL )
257  continue;
258  iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix );
259  iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
260  iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
261  if ( iPrevNew != iObjNew )
262  {
263  Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
264  Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
265  Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
266  }
267  }
268  }
269  Vec_IntForEachEntry( vXorLits, iObjNew, i )
270  Gia_ManAppendCo( pNew, iObjNew );
271  Vec_IntFree( vXorLits );
272  Gia_ManHashStop( pNew );
273  Vec_IntErase( &p->vCopies );
274 //Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
275  pNew = Gia_ManCleanup( pTemp = pNew );
276 //Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );
277  Gia_ManStop( pTemp );
278  return pNew;
279 }
280 
281 /**Function*************************************************************
282 
283  Synopsis [Initializes simulation info for lcorr/scorr counter-examples.]
284 
285  Description []
286 
287  SideEffects []
288 
289  SeeAlso []
290 
291 ***********************************************************************/
292 void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops )
293 {
294  unsigned * pInfo;
295  int k, w, nWords;
296  nWords = Vec_PtrReadWordsSimInfo( vInfo );
297  assert( nFlops <= Vec_PtrSize(vInfo) );
298  for ( k = 0; k < nFlops; k++ )
299  {
300  pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
301  for ( w = 0; w < nWords; w++ )
302  pInfo[w] = 0;
303  }
304  for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ )
305  {
306  pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
307  for ( w = 0; w < nWords; w++ )
308  pInfo[w] = Gia_ManRandom( 0 );
309  }
310 }
311 
312 /**Function*************************************************************
313 
314  Synopsis [Remaps simulation info from SRM to the original AIG.]
315 
316  Description []
317 
318  SideEffects []
319 
320  SeeAlso []
321 
322 ***********************************************************************/
323 void Gia_ManCorrRemapSimInfo( Gia_Man_t * p, Vec_Ptr_t * vInfo )
324 {
325  Gia_Obj_t * pObj, * pRepr;
326  unsigned * pInfoObj, * pInfoRepr;
327  int i, w, nWords;
328  nWords = Vec_PtrReadWordsSimInfo( vInfo );
329  Gia_ManForEachRo( p, pObj, i )
330  {
331  // skip ROs without representatives
332  pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
333  if ( pRepr == NULL || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
334  continue;
335  pInfoObj = (unsigned *)Vec_PtrEntry( vInfo, i );
336  for ( w = 0; w < nWords; w++ )
337  assert( pInfoObj[w] == 0 );
338  // skip ROs with constant representatives
339  if ( Gia_ObjIsConst0(pRepr) )
340  continue;
341  assert( Gia_ObjIsRo(p, pRepr) );
342 // Abc_Print( 1, "%d -> %d ", i, Gia_ObjId(p, pRepr) );
343  // transfer info from the representative
344  pInfoRepr = (unsigned *)Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
345  for ( w = 0; w < nWords; w++ )
346  pInfoObj[w] = pInfoRepr[w];
347  }
348 // Abc_Print( 1, "\n" );
349 }
350 
351 /**Function*************************************************************
352 
353  Synopsis [Collects information about remapping.]
354 
355  Description []
356 
357  SideEffects []
358 
359  SeeAlso []
360 
361 ***********************************************************************/
362 Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p )
363 {
364  Vec_Int_t * vPairs;
365  Gia_Obj_t * pObj, * pRepr;
366  int i;
367  vPairs = Vec_IntAlloc( 100 );
368  Gia_ManForEachRo( p, pObj, i )
369  {
370  // skip ROs without representatives
371  pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
372  if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
373 // if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
374  continue;
375  assert( Gia_ObjIsRo(p, pRepr) );
376 // Abc_Print( 1, "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) );
377  // remember the pair
378  Vec_IntPush( vPairs, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
379  Vec_IntPush( vPairs, i );
380  }
381  return vPairs;
382 }
383 
384 /**Function*************************************************************
385 
386  Synopsis [Remaps simulation info from SRM to the original AIG.]
387 
388  Description []
389 
390  SideEffects []
391 
392  SeeAlso []
393 
394 ***********************************************************************/
395 void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo )
396 {
397  unsigned * pInfoObj, * pInfoRepr;
398  int w, i, iObj, iRepr, nWords;
399  nWords = Vec_PtrReadWordsSimInfo( vInfo );
400  Vec_IntForEachEntry( vPairs, iRepr, i )
401  {
402  iObj = Vec_IntEntry( vPairs, ++i );
403  pInfoObj = (unsigned *)Vec_PtrEntry( vInfo, iObj );
404  pInfoRepr = (unsigned *)Vec_PtrEntry( vInfo, iRepr );
405  for ( w = 0; w < nWords; w++ )
406  {
407  assert( pInfoObj[w] == 0 );
408  pInfoObj[w] = pInfoRepr[w];
409  }
410  }
411 }
412 
413 /**Function*************************************************************
414 
415  Synopsis [Packs one counter-examples into the array of simulation info.]
416 
417  Description []
418 
419  SideEffects []
420 
421  SeeAlso []
422 
423 *************************************`**********************************/
424 int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
425 {
426  unsigned * pInfo, * pPres;
427  int i;
428  for ( i = 0; i < nLits; i++ )
429  {
430  pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
431  pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
432  if ( Abc_InfoHasBit( pPres, iBit ) &&
433  Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
434  return 0;
435  }
436  for ( i = 0; i < nLits; i++ )
437  {
438  pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
439  pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
440  Abc_InfoSetBit( pPres, iBit );
441  if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
442  Abc_InfoXorBit( pInfo, iBit );
443  }
444  return 1;
445 }
446 
447 /**Function*************************************************************
448 
449  Synopsis [Performs bitpacking of counter-examples.]
450 
451  Description []
452 
453  SideEffects []
454 
455  SeeAlso []
456 
457 ***********************************************************************/
458 int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
459 {
460  Vec_Int_t * vPat;
461  Vec_Ptr_t * vPres;
462  int nWords = Vec_PtrReadWordsSimInfo(vInfo);
463  int nBits = 32 * nWords;
464  int k, nSize, kMax = 0;//, iBit = 1;
465  vPat = Vec_IntAlloc( 100 );
466  vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords );
467  Vec_PtrCleanSimInfo( vPres, 0, nWords );
468  while ( iStart < Vec_IntSize(vCexStore) )
469  {
470  // skip the output number
471  iStart++;
472  // get the number of items
473  nSize = Vec_IntEntry( vCexStore, iStart++ );
474  if ( nSize <= 0 )
475  continue;
476  // extract pattern
477  Vec_IntClear( vPat );
478  for ( k = 0; k < nSize; k++ )
479  Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
480  // add pattern to storage
481  for ( k = 1; k < nBits; k++ )
482  if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
483  break;
484  kMax = Abc_MaxInt( kMax, k );
485  if ( k == nBits-1 )
486  break;
487  }
488  Vec_PtrFree( vPres );
489  Vec_IntFree( vPat );
490  return iStart;
491 }
492 
493 /**Function*************************************************************
494 
495  Synopsis [Performs bitpacking of counter-examples.]
496 
497  Description []
498 
499  SideEffects []
500 
501  SeeAlso []
502 
503 ***********************************************************************/
504 int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
505 {
506  unsigned * pInfo;
507  int nBits = 32 * Vec_PtrReadWordsSimInfo(vInfo);
508  int k, iLit, nLits, Out, iBit = 1;
509  while ( iStart < Vec_IntSize(vCexStore) )
510  {
511  // skip the output number
512 // iStart++;
513  Out = Vec_IntEntry( vCexStore, iStart++ );
514 // Abc_Print( 1, "iBit = %d. Out = %d.\n", iBit, Out );
515  // get the number of items
516  nLits = Vec_IntEntry( vCexStore, iStart++ );
517  if ( nLits <= 0 )
518  continue;
519  // add pattern to storage
520  for ( k = 0; k < nLits; k++ )
521  {
522  iLit = Vec_IntEntry( vCexStore, iStart++ );
523  pInfo = (unsigned *)Vec_PtrEntry( vInfo, Abc_Lit2Var(iLit) );
524  if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(iLit) )
525  Abc_InfoXorBit( pInfo, iBit );
526  }
527  if ( ++iBit == nBits )
528  break;
529  }
530 // Abc_Print( 1, "added %d bits\n", iBit-1 );
531  return iStart;
532 }
533 
534 /**Function*************************************************************
535 
536  Synopsis [Resimulates counter-examples derived by the SAT solver.]
537 
538  Description []
539 
540  SideEffects []
541 
542  SeeAlso []
543 
544 ***********************************************************************/
545 int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames )
546 {
547  Vec_Int_t * vPairs;
548  Vec_Ptr_t * vSimInfo;
549  int RetValue = 0, iStart = 0;
550  vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
551  Gia_ManCreateValueRefs( pSim->pAig );
552 // pSim->pPars->nWords = 63;
553  pSim->pPars->nFrames = nFrames;
554  vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
555  while ( iStart < Vec_IntSize(vCexStore) )
556  {
557  Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) );
558  iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
559 // iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
560 // Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
561  Gia_ManCorrPerformRemapping( vPairs, vSimInfo );
562  RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
563 // Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL );
564  }
565 //Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
566  assert( iStart == Vec_IntSize(vCexStore) );
567  Vec_PtrFree( vSimInfo );
568  Vec_IntFree( vPairs );
569  return RetValue;
570 }
571 
572 /**Function*************************************************************
573 
574  Synopsis [Resimulates counter-examples derived by the SAT solver.]
575 
576  Description []
577 
578  SideEffects []
579 
580  SeeAlso []
581 
582 ***********************************************************************/
583 int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore )
584 {
585  Vec_Ptr_t * vSimInfo;
586  int RetValue = 0, iStart = 0;
587  Gia_ManCreateValueRefs( pSim->pAig );
588  pSim->pPars->nFrames = 1;
589  vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords );
590  while ( iStart < Vec_IntSize(vCexStore) )
591  {
592  Cec_ManStartSimInfo( vSimInfo, 0 );
593  iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
594  RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
595  }
596  assert( iStart == Vec_IntSize(vCexStore) );
597  Vec_PtrFree( vSimInfo );
598  return RetValue;
599 }
600 
601 /**Function*************************************************************
602 
603  Synopsis [Updates equivalence classes by marking those that timed out.]
604 
605  Description [Returns 1 if all ndoes are proved.]
606 
607  SideEffects []
608 
609  SeeAlso []
610 
611 ***********************************************************************/
612 int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings )
613 {
614  int i, status, iRepr, iObj;
615  int Counter = 0;
616  assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) );
617  Vec_StrForEachEntry( vStatus, status, i )
618  {
619  iRepr = Vec_IntEntry( vOutputs, 2*i );
620  iObj = Vec_IntEntry( vOutputs, 2*i+1 );
621  if ( status == 1 )
622  continue;
623  if ( status == 0 )
624  {
625  if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
626  Counter++;
627 // if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
628 // Abc_Print( 1, "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj );
629 // if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
630 // Cec_ManSimClassRemoveOne( pSim, iObj );
631  continue;
632  }
633  if ( status == -1 )
634  {
635 // if ( !Gia_ObjFailed( p, iObj ) )
636 // Abc_Print( 1, "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" );
637 // Gia_ObjSetFailed( p, iRepr );
638 // Gia_ObjSetFailed( p, iObj );
639 // if ( fRings )
640 // Cec_ManSimClassRemoveOne( pSim, iRepr );
641  Cec_ManSimClassRemoveOne( pSim, iObj );
642  continue;
643  }
644  }
645 // if ( Counter )
646 // Abc_Print( 1, "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter );
647  return 1;
648 }
649 
650 
651 /**Function*************************************************************
652 
653  Synopsis [Duplicates the AIG in the DFS order.]
654 
655  Description []
656 
657  SideEffects []
658 
659  SeeAlso []
660 
661 ***********************************************************************/
662 void Gia_ManCorrReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
663 {
664  Gia_Obj_t * pRepr;
665  if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
666  {
667  Gia_ManCorrReduce_rec( pNew, p, pRepr );
668  pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
669  return;
670  }
671  if ( ~pObj->Value )
672  return;
673  assert( Gia_ObjIsAnd(pObj) );
674  Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
675  Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
676  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
677 }
678 
679 /**Function*************************************************************
680 
681  Synopsis [Reduces AIG using equivalence classes.]
682 
683  Description []
684 
685  SideEffects []
686 
687  SeeAlso []
688 
689 ***********************************************************************/
690 Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p )
691 {
692  Gia_Man_t * pNew;
693  Gia_Obj_t * pObj;
694  int i;
695  Gia_ManSetPhase( p );
696  pNew = Gia_ManStart( Gia_ManObjNum(p) );
697  pNew->pName = Abc_UtilStrsav( p->pName );
698  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
699  Gia_ManFillValue( p );
700  Gia_ManConst0(p)->Value = 0;
701  Gia_ManForEachCi( p, pObj, i )
702  pObj->Value = Gia_ManAppendCi(pNew);
703  Gia_ManHashAlloc( pNew );
704  Gia_ManForEachCo( p, pObj, i )
705  Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
706  Gia_ManForEachCo( p, pObj, i )
707  Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
708  Gia_ManHashStop( pNew );
709  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
710  return pNew;
711 }
712 
713 
714 /**Function*************************************************************
715 
716  Synopsis [Prints statistics during solving.]
717 
718  Description []
719 
720  SideEffects []
721 
722  SeeAlso []
723 
724 ***********************************************************************/
725 void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, abctime Time )
726 {
727  int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
728  int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
729  for ( i = 1; i < Gia_ManObjNum(p); i++ )
730  {
731  if ( Gia_ObjIsNone(p, i) )
732  CounterX++;
733  else if ( Gia_ObjIsConst(p, i) )
734  Counter0++;
735  else if ( Gia_ObjIsHead(p, i) )
736  Counter++;
737  }
738  CounterX -= Gia_ManCoNum(p);
739  nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
740  if ( iIter == -1 )
741  Abc_Print( 1, "BMC : " );
742  else
743  Abc_Print( 1, "%3d : ", iIter );
744  Abc_Print( 1, "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits );
745  if ( vStatus )
746  Vec_StrForEachEntry( vStatus, Entry, i )
747  {
748  if ( Entry == 1 )
749  nProve++;
750  else if ( Entry == 0 )
751  nDispr++;
752  else if ( Entry == -1 )
753  nFail++;
754  }
755  Abc_Print( 1, "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail );
756  Abc_Print( 1, "%c ", Gia_ObjIsConst( p, Gia_ObjFaninId0p(p, Gia_ManPo(p, 0)) ) ? '+' : '-' );
757  Abc_PrintTime( 1, "T", Time );
758 }
759 
760 /**Function*************************************************************
761 
762  Synopsis [Runs BMC for the equivalence classes.]
763 
764  Description []
765 
766  SideEffects []
767 
768  SeeAlso []
769 
770 ***********************************************************************/
771 void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPrefs )
772 {
773  Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
774  Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
775  Vec_Str_t * vStatus;
776  Vec_Int_t * vOutputs;
777  Vec_Int_t * vCexStore;
778  Cec_ManSim_t * pSim;
779  Gia_Man_t * pSrm;
780  int fChanges, RetValue;
781  // prepare simulation manager
782  Cec_ManSimSetDefaultParams( pParsSim );
783  pParsSim->nWords = pPars->nWords;
784  pParsSim->nFrames = pPars->nRounds;
785  pParsSim->fVerbose = pPars->fVerbose;
786  pParsSim->fLatchCorr = pPars->fLatchCorr;
787  pParsSim->fSeqSimulate = 1;
788  pSim = Cec_ManSimStart( pAig, pParsSim );
789  // prepare SAT solving
790  Cec_ManSatSetDefaultParams( pParsSat );
791  pParsSat->nBTLimit = pPars->nBTLimit;
792  pParsSat->fVerbose = pPars->fVerbose;
793  fChanges = 1;
794  while ( fChanges )
795  {
796  abctime clkBmc = Abc_Clock();
797  fChanges = 0;
798  pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
799  if ( Gia_ManPoNum(pSrm) == 0 )
800  {
801  Gia_ManStop( pSrm );
802  Vec_IntFree( vOutputs );
803  break;
804  }
805  pParsSat->nBTLimit *= 10;
806  if ( pPars->fUseCSat )
807  vCexStore = Tas_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
808  else
809  vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
810  // refine classes with these counter-examples
811  if ( Vec_IntSize(vCexStore) )
812  {
813  RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nPrefs );
814  Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
815  fChanges = 1;
816  }
817  if ( pPars->fVerbose )
818  Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, Abc_Clock() - clkBmc );
819  // recycle
820  Vec_IntFree( vCexStore );
821  Vec_StrFree( vStatus );
822  Gia_ManStop( pSrm );
823  Vec_IntFree( vOutputs );
824  }
825  Cec_ManSimStop( pSim );
826 }
827 
828 /**Function*************************************************************
829 
830  Synopsis []
831 
832  Description []
833 
834  SideEffects []
835 
836  SeeAlso []
837 
838 ***********************************************************************/
839 int Cec_ManLSCorrAnalyzeDependence( Gia_Man_t * p, Vec_Int_t * vEquivs, Vec_Str_t * vStatus )
840 {
841  Gia_Obj_t * pObj, * pObjRo;
842  int i, Iter, iObj, iRepr, fPrev, Total, Count0, Count1;
843  assert( Vec_StrSize(vStatus) * 2 == Vec_IntSize(vEquivs) );
844  Total = 0;
845  Gia_ManForEachObj( p, pObj, i )
846  {
847  assert( pObj->fMark1 == 0 );
848  if ( Gia_ObjHasRepr(p, i) )
849  Total++;
850  }
851  Count0 = 0;
852  for ( i = 0; i < Vec_StrSize(vStatus); i++ )
853  {
854  iRepr = Vec_IntEntry(vEquivs, 2*i);
855  iObj = Vec_IntEntry(vEquivs, 2*i+1);
856  assert( iRepr == Gia_ObjRepr(p, iObj) );
857  if ( Vec_StrEntry(vStatus, i) != 1 ) // disproved or undecided
858  {
859  Gia_ManObj(p, iObj)->fMark1 = 1;
860  Count0++;
861  }
862  }
863  for ( Iter = 0; Iter < 100; Iter++ )
864  {
865  int fChanges = 0;
866  Gia_ManForEachObj1( p, pObj, i )
867  {
868  if ( Gia_ObjIsCi(pObj) )
869  continue;
870  assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) );
871 // fPrev = pObj->fMark1;
872  if ( Gia_ObjIsAnd(pObj) )
873  pObj->fMark1 |= Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
874  else
875  pObj->fMark1 |= Gia_ObjFanin0(pObj)->fMark1;
876 // fChanges += fPrev ^ pObj->fMark1;
877  }
878  Gia_ManForEachRiRo( p, pObj, pObjRo, i )
879  {
880  fPrev = pObjRo->fMark1;
881  pObjRo->fMark1 = pObj->fMark1;
882  fChanges += fPrev ^ pObjRo->fMark1;
883  }
884  if ( fChanges == 0 )
885  break;
886  }
887  Count1 = 0;
888  Gia_ManForEachObj( p, pObj, i )
889  {
890  if ( pObj->fMark1 && Gia_ObjHasRepr(p, i) )
891  Count1++;
892  pObj->fMark1 = 0;
893  }
894  printf( "%5d -> %5d (%3d) ", Count0, Count1, Iter );
895  return 0;
896 }
897 
898 /**Function*************************************************************
899 
900  Synopsis [Internal procedure for register correspondence.]
901 
902  Description []
903 
904  SideEffects []
905 
906  SeeAlso []
907 
908 ***********************************************************************/
909 int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
910 {
911  int nIterMax = 100000;
912  int nAddFrames = 1; // additional timeframes to simulate
913  int fRunBmcFirst = 1;
914  Vec_Str_t * vStatus;
915  Vec_Int_t * vOutputs;
916  Vec_Int_t * vCexStore;
917  Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
918  Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
919  Cec_ManSim_t * pSim;
920  Gia_Man_t * pSrm;
921  int r, RetValue;
922  abctime clkTotal = Abc_Clock();
923  abctime clkSat = 0, clkSim = 0, clkSrm = 0;
924  abctime clk2, clk = Abc_Clock();
925  if ( Gia_ManRegNum(pAig) == 0 )
926  {
927  Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
928  return 0;
929  }
930  Gia_ManRandom( 1 );
931  // prepare simulation manager
932  Cec_ManSimSetDefaultParams( pParsSim );
933  pParsSim->nWords = pPars->nWords;
934  pParsSim->nFrames = pPars->nFrames;
935  pParsSim->fVerbose = pPars->fVerbose;
936  pParsSim->fLatchCorr = pPars->fLatchCorr;
937  pParsSim->fConstCorr = pPars->fConstCorr;
938  pParsSim->fSeqSimulate = 1;
939  // create equivalence classes of registers
940  pSim = Cec_ManSimStart( pAig, pParsSim );
941  if ( pAig->pReprs == NULL )
942  {
943  Cec_ManSimClassesPrepare( pSim, pPars->nLevelMax );
944  Cec_ManSimClassesRefine( pSim );
945  }
946  // prepare SAT solving
947  Cec_ManSatSetDefaultParams( pParsSat );
948  pParsSat->nBTLimit = pPars->nBTLimit;
949  pParsSat->fVerbose = pPars->fVerbose;
950  // limit the number of conflicts in the circuit-based solver
951  if ( pPars->fUseCSat )
952  pParsSat->nBTLimit = Abc_MinInt( pParsSat->nBTLimit, 1000 );
953  if ( pPars->fVerbose )
954  {
955  Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
956  Gia_ManObjNum(pAig), Gia_ManAndNum(pAig),
957  pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
958  Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk );
959  }
960  // check the base case
961  if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
962  Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
963  if ( pPars->pFunc )
964  {
965  ((int (*)(void *))pPars->pFunc)( pPars->pData );
966  ((int (*)(void *))pPars->pFunc)( pPars->pData );
967  }
968  if ( pPars->nStepsMax == 0 )
969  {
970  Abc_Print( 1, "Stopped signal correspondence after BMC.\n" );
971  Cec_ManSimStop( pSim );
972  return 1;
973  }
974  // perform refinement of equivalence classes
975  for ( r = 0; r < nIterMax; r++ )
976  {
977  if ( pPars->nStepsMax == r )
978  {
979  Cec_ManSimStop( pSim );
980  Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r );
981  return 1;
982  }
983  clk = Abc_Clock();
984  // perform speculative reduction
985  clk2 = Abc_Clock();
986  pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
987  assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) );
988  clkSrm += Abc_Clock() - clk2;
989  if ( Gia_ManCoNum(pSrm) == 0 )
990  {
991  Vec_IntFree( vOutputs );
992  Gia_ManStop( pSrm );
993  break;
994  }
995 //Gia_DumpAiger( pSrm, "corrsrm", r, 2 );
996  // found counter-examples to speculation
997  clk2 = Abc_Clock();
998  if ( pPars->fUseCSat )
999  vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
1000  else
1001  vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
1002  Gia_ManStop( pSrm );
1003  clkSat += Abc_Clock() - clk2;
1004  if ( Vec_IntSize(vCexStore) == 0 )
1005  {
1006  Vec_IntFree( vCexStore );
1007  Vec_StrFree( vStatus );
1008  Vec_IntFree( vOutputs );
1009  break;
1010  }
1011 // Cec_ManLSCorrAnalyzeDependence( pAig, vOutputs, vStatus );
1012 
1013  // refine classes with these counter-examples
1014  clk2 = Abc_Clock();
1015  RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames );
1016  Vec_IntFree( vCexStore );
1017  clkSim += Abc_Clock() - clk2;
1018  Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
1019  if ( pPars->fVerbose )
1020  Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );
1021  Vec_StrFree( vStatus );
1022  Vec_IntFree( vOutputs );
1023 //Gia_ManEquivPrintClasses( pAig, 1, 0 );
1024  if ( pPars->pFunc )
1025  ((int (*)(void *))pPars->pFunc)( pPars->pData );
1026  // quit if const is no longer there
1027  if ( pPars->fStopWhenGone && Gia_ManPoNum(pAig) == 1 && !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) ) )
1028  {
1029  printf( "Iterative refinement is stopped after iteration %d\n", r );
1030  printf( "because the property output is no longer a candidate constant.\n" );
1031  Cec_ManSimStop( pSim );
1032  return 0;
1033  }
1034  }
1035  if ( pPars->fVerbose )
1036  Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, Abc_Clock() - clk );
1037  // check the overflow
1038  if ( r == nIterMax )
1039  Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" );
1040  Cec_ManSimStop( pSim );
1041  // check the base case
1042  if ( !fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
1043  Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
1044  clkTotal = Abc_Clock() - clkTotal;
1045  // report the results
1046  if ( pPars->fVerbose )
1047  {
1048  ABC_PRTP( "Srm ", clkSrm, clkTotal );
1049  ABC_PRTP( "Sat ", clkSat, clkTotal );
1050  ABC_PRTP( "Sim ", clkSim, clkTotal );
1051  ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
1052  Abc_PrintTime( 1, "TOTAL", clkTotal );
1053  }
1054  return 1;
1055 }
1056 
1057 /**Function*************************************************************
1058 
1059  Synopsis [Computes new initial state.]
1060 
1061  Description []
1062 
1063  SideEffects []
1064 
1065  SeeAlso []
1066 
1067 ***********************************************************************/
1068 unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames )
1069 {
1070  Gia_Obj_t * pObj, * pObjRo, * pObjRi;
1071  unsigned * pInitState;
1072  int i, f;
1073  Gia_ManRandom( 1 );
1074 // Abc_Print( 1, "Simulating %d timeframes.\n", nFrames );
1075  Gia_ManForEachRo( pAig, pObj, i )
1076  pObj->fMark1 = 0;
1077  for ( f = 0; f < nFrames; f++ )
1078  {
1079  Gia_ManConst0(pAig)->fMark1 = 0;
1080  Gia_ManForEachPi( pAig, pObj, i )
1081  pObj->fMark1 = Gia_ManRandom(0) & 1;
1082  Gia_ManForEachAnd( pAig, pObj, i )
1083  pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) &
1084  (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
1085  Gia_ManForEachRi( pAig, pObj, i )
1086  pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj));
1087  Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, i )
1088  pObjRo->fMark1 = pObjRi->fMark1;
1089  }
1090  pInitState = ABC_CALLOC( unsigned, Abc_BitWordNum(Gia_ManRegNum(pAig)) );
1091  Gia_ManForEachRo( pAig, pObj, i )
1092  {
1093  if ( pObj->fMark1 )
1094  Abc_InfoSetBit( pInitState, i );
1095 // Abc_Print( 1, "%d", pObj->fMark1 );
1096  }
1097 // Abc_Print( 1, "\n" );
1098  Gia_ManCleanMark1( pAig );
1099  return pInitState;
1100 }
1101 
1102 /**Function*************************************************************
1103 
1104  Synopsis [Prints flop equivalences.]
1105 
1106  Description []
1107 
1108  SideEffects []
1109 
1110  SeeAlso []
1111 
1112 ***********************************************************************/
1113 void Cec_ManPrintFlopEquivs( Gia_Man_t * p )
1114 {
1115  Gia_Obj_t * pObj, * pRepr;
1116  int i;
1117  assert( p->vNamesIn != NULL );
1118  Gia_ManForEachRo( p, pObj, i )
1119  {
1120  if ( Gia_ObjIsConst(p, Gia_ObjId(p, pObj)) )
1121  Abc_Print( 1, "Original flop %s is proved equivalent to constant.\n", Vec_PtrEntry(p->vNamesIn, Gia_ObjCioId(pObj)) );
1122  else if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
1123  {
1124  if ( Gia_ObjIsCi(pRepr) )
1125  Abc_Print( 1, "Original flop %s is proved equivalent to flop %s.\n",
1126  Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ),
1127  Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pRepr) ) );
1128  else
1129  Abc_Print( 1, "Original flop %s is proved equivalent to internal node %d.\n",
1130  Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ), Gia_ObjId(p, pRepr) );
1131  }
1132  }
1133 }
1134 
1135 
1136 /**Function*************************************************************
1137 
1138  Synopsis [Top-level procedure for register correspondence.]
1139 
1140  Description []
1141 
1142  SideEffects []
1143 
1144  SeeAlso []
1145 
1146 ***********************************************************************/
1147 Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
1148 {
1149  Gia_Man_t * pNew, * pTemp;
1150  unsigned * pInitState;
1151  int RetValue;
1152  ABC_FREE( pAig->pReprs );
1153  ABC_FREE( pAig->pNexts );
1154  if ( pPars->nPrefix == 0 )
1155  {
1156  RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
1157  if ( RetValue == 0 )
1158  return Gia_ManDup( pAig );
1159  }
1160  else
1161  {
1162  // compute the cycles AIG
1163  pInitState = Cec_ManComputeInitState( pAig, pPars->nPrefix );
1164  pTemp = Gia_ManDupFlip( pAig, (int *)pInitState );
1165  ABC_FREE( pInitState );
1166  // compute classes of this AIG
1167  RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars );
1168  // transfer the class info
1169  pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL;
1170  pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL;
1171  // perform additional BMC
1172  pPars->fUseCSat = 0;
1173  pPars->nBTLimit = Abc_MaxInt( pPars->nBTLimit, 1000 );
1174  Cec_ManLSCorrespondenceBmc( pAig, pPars, pPars->nPrefix );
1175 /*
1176  // transfer the class info back
1177  pTemp->pReprs = pAig->pReprs; pAig->pReprs = NULL;
1178  pTemp->pNexts = pAig->pNexts; pAig->pNexts = NULL;
1179  // continue refining
1180  RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars );
1181  // transfer the class info
1182  pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL;
1183  pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL;
1184 */
1185  Gia_ManStop( pTemp );
1186  }
1187  // derive reduced AIG
1188  if ( pPars->fMakeChoices )
1189  {
1190  pNew = Gia_ManEquivToChoices( pAig, 1 );
1191 // Gia_ManHasChoices_very_old( pNew );
1192  }
1193  else
1194  {
1195 // Gia_ManEquivImprove( pAig );
1196  pNew = Gia_ManCorrReduce( pAig );
1197  pNew = Gia_ManSeqCleanup( pTemp = pNew );
1198  Gia_ManStop( pTemp );
1199  //Gia_AigerWrite( pNew, "reduced.aig", 0, 0 );
1200  }
1201  // report the results
1202  if ( pPars->fVerbose )
1203  {
1204  Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
1205  Gia_ManAndNum(pAig), Gia_ManAndNum(pNew),
1206  100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
1207  Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),
1208  100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
1209  }
1210  if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) )
1211  Abc_Print( 1, "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix );
1212  // print verbose info about equivalences
1213  if ( pPars->fVerboseFlops )
1214  {
1215  if ( pAig->vNamesIn == NULL )
1216  Abc_Print( 1, "Flop output names are not available. Use command \"&get -n\".\n" );
1217  else
1218  Cec_ManPrintFlopEquivs( pAig );
1219  }
1220  return pNew;
1221 }
1222 
1223 ////////////////////////////////////////////////////////////////////////
1224 /// END OF FILE ///
1225 ////////////////////////////////////////////////////////////////////////
1226 
1227 
1228 ABC_NAMESPACE_IMPL_END
1229 
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Gia_ObjSetCopyF
static void Gia_ObjSetCopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj, int iLit)
Definition: gia.h:486
Cec_ParCor_t_::nRounds
int nRounds
Definition: cec.h:136
Cec_ParSim_t_::fVerbose
int fVerbose
Definition: cec.h:73
Gia_ManCorrSpecReduce
Gia_Man_t * Gia_ManCorrSpecReduce(Gia_Man_t *p, int nFrames, int fScorr, Vec_Int_t **pvOutputs, int fRings)
Definition: cecCorr.c:106
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Cec_ManSimClassesPrepare
int Cec_ManSimClassesPrepare(Cec_ManSim_t *p, int LevelMax)
Definition: cecClass.c:851
Gia_ObjPhase
static int Gia_ObjPhase(Gia_Obj_t *pObj)
Definition: gia.h:415
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
Gia_ObjPhaseReal
static int Gia_ObjPhaseReal(Gia_Obj_t *pObj)
Definition: gia.h:416
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Cec_ParSim_t_::fLatchCorr
int fLatchCorr
Definition: cec.h:70
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_Man_t_::pNexts
int * pNexts
Definition: gia.h:122
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Cec_ParCor_t_::fUseCSat
int fUseCSat
Definition: cec.h:146
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Cec_ParSim_t_::fSeqSimulate
int fSeqSimulate
Definition: cec.h:69
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
Cec_ManStartSimInfo
void Cec_ManStartSimInfo(Vec_Ptr_t *vInfo, int nFlops)
Definition: cecCorr.c:292
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Cec_ParCor_t_
Definition: cec.h:133
Gia_ManHashXor
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:658
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
Gia_ObjFanin1CopyF
static int Gia_ObjFanin1CopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj)
Definition: gia.h:492
Cec_ManSatSolveMiter
Vec_Int_t * Cec_ManSatSolveMiter(Gia_Man_t *pAig, Cec_ParSat_t *pPars, Vec_Str_t **pvStatus)
Definition: cecSolve.c:1026
Gia_ManPo
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
Gia_ObjIsCand
static int Gia_ObjIsCand(Gia_Obj_t *pObj)
Definition: gia.h:429
Cec_ParCor_t_::nPrefix
int nPrefix
Definition: cec.h:138
Abc_InfoXorBit
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
Cec_ParCor_t_::pData
void * pData
Definition: cec.h:154
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Cec_ManRefinedClassPrintStats
void Cec_ManRefinedClassPrintStats(Gia_Man_t *p, Vec_Str_t *vStatus, int iIter, abctime Time)
MACRO DEFINITIONS ///.
Definition: cecCorr.c:725
Vec_StrForEachEntry
#define Vec_StrForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecStr.h:54
Gia_ObjIsConst0
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
Cec_ParCor_t_::fUseRings
int fUseRings
Definition: cec.h:144
Vec_PtrCleanSimInfo
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
Cec_ManLSCorrespondenceClasses
int Cec_ManLSCorrespondenceClasses(Gia_Man_t *pAig, Cec_ParCor_t *pPars)
Definition: cecCorr.c:909
Cec_ManSim_t_
Definition: cecInt.h:112
Cec_ParCor_t_::fConstCorr
int fConstCorr
Definition: cec.h:143
Gia_ObjIsHead
static int Gia_ObjIsHead(Gia_Man_t *p, int Id)
Definition: gia.h:916
Cec_ManSimStop
void Cec_ManSimStop(Cec_ManSim_t *p)
Definition: cecMan.c:232
Gia_ManCorrSpecReduce_rec
static ABC_NAMESPACE_IMPL_START void Gia_ManCorrSpecReduce_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, int f, int nPrefix)
DECLARATIONS ///.
Definition: cecCorr.c:77
Cec_ManSim_t_::pAig
Gia_Man_t * pAig
Definition: cecInt.h:115
Vec_IntErase
static void Vec_IntErase(Vec_Int_t *p)
Definition: vecInt.h:266
Cec_ManLoadCounterExamples2
int Cec_ManLoadCounterExamples2(Vec_Ptr_t *vInfo, Vec_Int_t *vCexStore, int iStart)
Definition: cecCorr.c:504
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
Gia_Obj_t_::fMark1
unsigned fMark1
Definition: gia.h:84
Gia_ManCorrReduce
Gia_Man_t * Gia_ManCorrReduce(Gia_Man_t *p)
Definition: cecCorr.c:690
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
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
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Gia_Obj_t_
Definition: gia.h:75
Gia_ManCleanMark1
void Gia_ManCleanMark1(Gia_Man_t *p)
Definition: giaUtil.c:272
Cec_ParCor_t_::fVerboseFlops
int fVerboseFlops
Definition: cec.h:150
Cec_ParCor_t_::fLatchCorr
int fLatchCorr
Definition: cec.h:142
Cec_ParCor_t_::fVerbose
int fVerbose
Definition: cec.h:152
Gia_ManCheckRefinements
int Gia_ManCheckRefinements(Gia_Man_t *p, Vec_Str_t *vStatus, Vec_Int_t *vOutputs, Cec_ManSim_t *pSim, int fRings)
Definition: cecCorr.c:612
Cec_ManSimStart
Cec_ManSim_t * Cec_ManSimStart(Gia_Man_t *pAig, Cec_ParSim_t *pPars)
Definition: cecMan.c:198
Cbs_ManSolveMiterNc
Vec_Int_t * Cbs_ManSolveMiterNc(Gia_Man_t *pGia, int nConfs, Vec_Str_t **pvStatus, int fVerbose)
Definition: giaCSat.c:998
Gia_ManRandom
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition: abc_global.h:223
Cec_ManSimSetDefaultParams
void Cec_ManSimSetDefaultParams(Cec_ParSim_t *p)
Definition: cecCore.c:70
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Gia_ManEquivToChoices
Gia_Man_t * Gia_ManEquivToChoices(Gia_Man_t *p, int nSnapshots)
Definition: giaEquiv.c:1629
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Gia_ManCreateValueRefs
void Gia_ManCreateValueRefs(Gia_Man_t *p)
Definition: giaUtil.c:687
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Vec_StrEntry
static char Vec_StrEntry(Vec_Str_t *p, int i)
Definition: vecStr.h:336
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_ManSeqCleanup
Gia_Man_t * Gia_ManSeqCleanup(Gia_Man_t *p)
Definition: giaScl.c:183
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Cec_ParSim_t_::fConstCorr
int fConstCorr
Definition: cec.h:71
Cec_ManLSCorrespondenceBmc
void Cec_ManLSCorrespondenceBmc(Gia_Man_t *pAig, Cec_ParCor_t *pPars, int nPrefs)
Definition: cecCorr.c:771
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Vec_StrFree
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
Gia_ObjIsRo
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
Cec_ManLoadCounterExamples
int Cec_ManLoadCounterExamples(Vec_Ptr_t *vInfo, Vec_Int_t *vCexStore, int iStart)
Definition: cecCorr.c:458
Cec_ParCor_t_::nFrames
int nFrames
Definition: cec.h:137
Gia_ObjRoToRi
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Cec_ManComputeInitState
unsigned * Cec_ManComputeInitState(Gia_Man_t *pAig, int nFrames)
Definition: cecCorr.c:1068
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_ParCor_t_::nLevelMax
int nLevelMax
Definition: cec.h:140
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Cec_ParCor_t_::fMakeChoices
int fMakeChoices
Definition: cec.h:145
Gia_Man_t_::pSpec
char * pSpec
Definition: gia.h:98
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gia_ClassForEachObj1
#define Gia_ClassForEachObj1(p, i, iObj)
Definition: gia.h:933
Cec_ManLSCorrAnalyzeDependence
int Cec_ManLSCorrAnalyzeDependence(Gia_Man_t *p, Vec_Int_t *vEquivs, Vec_Str_t *vStatus)
Definition: cecCorr.c:839
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Cec_ParCor_t_::fStopWhenGone
int fStopWhenGone
Definition: cec.h:149
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Cec_ManResimulateCounterExamplesComb
int Cec_ManResimulateCounterExamplesComb(Cec_ManSim_t *pSim, Vec_Int_t *vCexStore)
Definition: cecCorr.c:583
Gia_ManCorrPerformRemapping
void Gia_ManCorrPerformRemapping(Vec_Int_t *vPairs, Vec_Ptr_t *vInfo)
Definition: cecCorr.c:395
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
Cec_ManLoadCounterExamplesTry
int Cec_ManLoadCounterExamplesTry(Vec_Ptr_t *vInfo, Vec_Ptr_t *vPres, int iBit, int *pLits, int nLits)
Definition: cecCorr.c:424
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Cec_ParCor_t_::nWords
int nWords
Definition: cec.h:135
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
Gia_ObjReprObj
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
Cec_ManPrintFlopEquivs
void Cec_ManPrintFlopEquivs(Gia_Man_t *p)
Definition: cecCorr.c:1113
Vec_StrSize
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Cec_ParCor_t_::pFunc
void * pFunc
Definition: cec.h:155
Cec_ManSimClassesRefine
int Cec_ManSimClassesRefine(Cec_ManSim_t *p)
Definition: cecClass.c:908
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Vec_PtrReadWordsSimInfo
static int Vec_PtrReadWordsSimInfo(Vec_Ptr_t *p)
Definition: vecPtr.h:952
Gia_ObjHasSameRepr
static int Gia_ObjHasSameRepr(Gia_Man_t *p, int i, int k)
Definition: gia.h:920
Gia_ManCorrReduce_rec
void Gia_ManCorrReduce_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: cecCorr.c:662
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_Str_t_
Definition: bblif.c:47
Cec_ParSim_t_::nFrames
int nFrames
Definition: cec.h:62
Gia_ManDupFlip
Gia_Man_t * Gia_ManDupFlip(Gia_Man_t *p, int *pInitState)
Definition: giaDup.c:460
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Cec_ParCor_t_::nBTLimit
int nBTLimit
Definition: cec.h:139
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
Gia_ObjIsNone
static int Gia_ObjIsNone(Gia_Man_t *p, int Id)
Definition: gia.h:917
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Gia_ManCorrRemapSimInfo
void Gia_ManCorrRemapSimInfo(Gia_Man_t *p, Vec_Ptr_t *vInfo)
Definition: cecCorr.c:323
Gia_ObjFaninId0p
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Gia_ManCorrSpecReal
static int Gia_ManCorrSpecReal(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, int f, int nPrefix)
FUNCTION DEFINITIONS ///.
Definition: cecCorr.c:47
Gia_ObjFailed
static int Gia_ObjFailed(Gia_Man_t *p, int Id)
Definition: gia.h:900
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
Cec_ParSat_t
typedefABC_NAMESPACE_HEADER_START struct Cec_ParSat_t_ Cec_ParSat_t
INCLUDES ///.
Definition: cec.h:43
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition: gia.h:121
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManSetPhase
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
Cec_ParSim_t_
Definition: cec.h:59
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
Gia_Man_t_::vNamesIn
Vec_Ptr_t * vNamesIn
Definition: gia.h:155
Gia_ManCorrSpecReduceInit
Gia_Man_t * Gia_ManCorrSpecReduceInit(Gia_Man_t *p, int nFrames, int nPrefix, int fScorr, Vec_Int_t **pvOutputs, int fRings)
Definition: cecCorr.c:223
Cec_ParSim_t_::nWords
int nWords
Definition: cec.h:61
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Cec_ParCor_t_::nStepsMax
int nStepsMax
Definition: cec.h:141
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Cec_ManResimulateCounterExamples
int Cec_ManResimulateCounterExamples(Cec_ManSim_t *pSim, Vec_Int_t *vCexStore, int nFrames)
Definition: cecCorr.c:545
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Cec_ManSimClassRemoveOne
int Cec_ManSimClassRemoveOne(Cec_ManSim_t *p, int i)
Definition: cecClass.c:308
Gia_ObjFanin0CopyF
static int Gia_ObjFanin0CopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj)
Definition: gia.h:491
Cec_ManSatSetDefaultParams
void Cec_ManSatSetDefaultParams(Cec_ParSat_t *p)
DECLARATIONS ///.
Definition: cecCore.c:45
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_ObjCioId
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
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
Tas_ManSolveMiterNc
Vec_Int_t * Tas_ManSolveMiterNc(Gia_Man_t *pGia, int nConfs, Vec_Str_t **pvStatus, int fVerbose)
Definition: giaCTas.c:1517
Cec_ManSeqResimulate
int Cec_ManSeqResimulate(Cec_ManSim_t *p, Vec_Ptr_t *vInfo)
Definition: cecSeq.c:137
Vec_PtrAllocSimInfo
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
Cec_ManLSCorrespondence
Gia_Man_t * Cec_ManLSCorrespondence(Gia_Man_t *pAig, Cec_ParCor_t *pPars)
Definition: cecCorr.c:1147
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Gia_Man_t_::vCopies
Vec_Int_t vCopies
Definition: gia.h:138
Gia_ManCorrCreateRemapping
Vec_Int_t * Gia_ManCorrCreateRemapping(Gia_Man_t *p)
Definition: cecCorr.c:362
Gia_ObjHasRepr
static int Gia_ObjHasRepr(Gia_Man_t *p, int Id)
Definition: gia.h:891
Gia_ObjCopyF
static int Gia_ObjCopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj)
Definition: gia.h:485
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387