abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
sswIslands.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [sswIslands.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Inductive prover with constraints.]
8 
9  Synopsis [Detection of islands of difference.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - September 1, 2008.]
16 
17  Revision [$Id: sswIslands.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "sswInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Creates pair of structurally equivalent nodes.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 void Ssw_CreatePair( Vec_Int_t * vPairs, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
46 {
47  pObj0->pData = pObj1;
48  pObj1->pData = pObj0;
49  Vec_IntPush( vPairs, pObj0->Id );
50  Vec_IntPush( vPairs, pObj1->Id );
51 }
52 
53 /**Function*************************************************************
54 
55  Synopsis [Establishes relationship between nodes using pairing.]
56 
57  Description []
58 
59  SideEffects []
60 
61  SeeAlso []
62 
63 ***********************************************************************/
64 void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
65 {
66  Aig_Obj_t * pObj0, * pObj1;
67  int i;
68  // create matching
69  Aig_ManCleanData( p0 );
70  Aig_ManCleanData( p1 );
71  for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
72  {
73  pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairs, i) );
74  pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairs, i+1) );
75  assert( pObj0->pData == NULL );
76  assert( pObj1->pData == NULL );
77  pObj0->pData = pObj1;
78  pObj1->pData = pObj0;
79  }
80  // make sure constants are matched
81  pObj0 = Aig_ManConst1( p0 );
82  pObj1 = Aig_ManConst1( p1 );
83  assert( pObj0->pData == pObj1 );
84  assert( pObj1->pData == pObj0 );
85  // make sure PIs are matched
86  Saig_ManForEachPi( p0, pObj0, i )
87  {
88  pObj1 = Aig_ManCi( p1, i );
89  assert( pObj0->pData == pObj1 );
90  assert( pObj1->pData == pObj0 );
91  }
92  // make sure the POs are not matched
93  Aig_ManForEachCo( p0, pObj0, i )
94  {
95  pObj1 = Aig_ManCo( p1, i );
96  assert( pObj0->pData == NULL );
97  assert( pObj1->pData == NULL );
98  }
99 
100  // check that LIs/LOs are matched in sync
101  Saig_ManForEachLo( p0, pObj0, i )
102  {
103  if ( pObj0->pData == NULL )
104  continue;
105  pObj1 = (Aig_Obj_t *)pObj0->pData;
106  if ( !Saig_ObjIsLo(p1, pObj1) )
107  Abc_Print( 1, "Mismatch between LO pairs.\n" );
108  }
109  Saig_ManForEachLo( p1, pObj1, i )
110  {
111  if ( pObj1->pData == NULL )
112  continue;
113  pObj0 = (Aig_Obj_t *)pObj1->pData;
114  if ( !Saig_ObjIsLo(p0, pObj0) )
115  Abc_Print( 1, "Mismatch between LO pairs.\n" );
116  }
117 }
118 
119 /**Function*************************************************************
120 
121  Synopsis [Establishes relationship between nodes using pairing.]
122 
123  Description []
124 
125  SideEffects []
126 
127  SeeAlso []
128 
129 ***********************************************************************/
130 void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
131 {
132  Aig_Obj_t * pNext, * pObj;
133  int i, k, iFan = -1;
134  Vec_PtrClear( vNodes );
135  Aig_ManIncrementTravId( p );
136  Aig_ManForEachObj( p, pObj, i )
137  {
138  if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
139  continue;
140  if ( pObj->pData != NULL )
141  continue;
142  if ( Saig_ObjIsLo(p, pObj) )
143  {
144  pNext = Saig_ObjLoToLi(p, pObj);
145  pNext = Aig_ObjFanin0(pNext);
146  if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) && !Aig_ObjIsConst1(pNext) )
147  {
148  Aig_ObjSetTravIdCurrent(p, pNext);
149  Vec_PtrPush( vNodes, pNext );
150  }
151  }
152  if ( Aig_ObjIsNode(pObj) )
153  {
154  pNext = Aig_ObjFanin0(pObj);
155  if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
156  {
157  Aig_ObjSetTravIdCurrent(p, pNext);
158  Vec_PtrPush( vNodes, pNext );
159  }
160  pNext = Aig_ObjFanin1(pObj);
161  if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
162  {
163  Aig_ObjSetTravIdCurrent(p, pNext);
164  Vec_PtrPush( vNodes, pNext );
165  }
166  }
167  Aig_ObjForEachFanout( p, pObj, pNext, iFan, k )
168  {
169  if ( Saig_ObjIsPo(p, pNext) )
170  continue;
171  if ( Saig_ObjIsLi(p, pNext) )
172  pNext = Saig_ObjLiToLo(p, pNext);
173  if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
174  {
175  Aig_ObjSetTravIdCurrent(p, pNext);
176  Vec_PtrPush( vNodes, pNext );
177  }
178  }
179  }
180 }
181 
182 /**Function*************************************************************
183 
184  Synopsis [Establishes relationship between nodes using pairing.]
185 
186  Description []
187 
188  SideEffects []
189 
190  SeeAlso []
191 
192 ***********************************************************************/
193 int Ssw_MatchingCountUnmached( Aig_Man_t * p )
194 {
195  Aig_Obj_t * pObj;
196  int i, Counter = 0;
197  Aig_ManForEachObj( p, pObj, i )
198  {
199  if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
200  continue;
201  if ( pObj->pData != NULL )
202  continue;
203  Counter++;
204  }
205  return Counter;
206 }
207 
208 /**Function*************************************************************
209 
210  Synopsis [Establishes relationship between nodes using pairing.]
211 
212  Description []
213 
214  SideEffects []
215 
216  SeeAlso []
217 
218 ***********************************************************************/
219 void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose )
220 {
221  Vec_Ptr_t * vNodes0, * vNodes1;
222  Aig_Obj_t * pNext0, * pNext1;
223  int d, k;
224  Aig_ManFanoutStart(p0);
225  Aig_ManFanoutStart(p1);
226  vNodes0 = Vec_PtrAlloc( 1000 );
227  vNodes1 = Vec_PtrAlloc( 1000 );
228  if ( fVerbose )
229  {
230  int nUnmached = Ssw_MatchingCountUnmached(p0);
231  Abc_Print( 1, "Extending islands by %d steps:\n", nDist );
232  Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
233  0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
234  nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
235  }
236  for ( d = 0; d < nDist; d++ )
237  {
238  Ssw_MatchingExtendOne( p0, vNodes0 );
239  Ssw_MatchingExtendOne( p1, vNodes1 );
240  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pNext0, k )
241  {
242  pNext1 = (Aig_Obj_t *)pNext0->pData;
243  if ( pNext1 == NULL )
244  continue;
245  assert( pNext1->pData == pNext0 );
246  if ( Saig_ObjIsPi(p0, pNext1) )
247  continue;
248  pNext0->pData = NULL;
249  pNext1->pData = NULL;
250  }
251  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pNext0, k )
252  {
253  pNext1 = (Aig_Obj_t *)pNext0->pData;
254  if ( pNext1 == NULL )
255  continue;
256  assert( pNext1->pData == pNext0 );
257  if ( Saig_ObjIsPi(p1, pNext1) )
258  continue;
259  pNext0->pData = NULL;
260  pNext1->pData = NULL;
261  }
262  if ( fVerbose )
263  {
264  int nUnmached = Ssw_MatchingCountUnmached(p0);
265  Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
266  d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
267  nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
268  }
269  }
270  Vec_PtrFree( vNodes0 );
271  Vec_PtrFree( vNodes1 );
272  Aig_ManFanoutStop(p0);
273  Aig_ManFanoutStop(p1);
274 }
275 
276 /**Function*************************************************************
277 
278  Synopsis [Used differences in p0 to complete p1.]
279 
280  Description []
281 
282  SideEffects []
283 
284  SeeAlso []
285 
286 ***********************************************************************/
287 void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 )
288 {
289  Vec_Ptr_t * vNewLis;
290  Aig_Obj_t * pObj0, * pObj0Li, * pObj1;
291  int i;
292  // create register outputs in p0 that are absent in p1
293  vNewLis = Vec_PtrAlloc( 100 );
294  Saig_ManForEachLiLo( p0, pObj0Li, pObj0, i )
295  {
296  if ( pObj0->pData != NULL )
297  continue;
298  pObj1 = Aig_ObjCreateCi( p1 );
299  pObj0->pData = pObj1;
300  pObj1->pData = pObj0;
301  Vec_PtrPush( vNewLis, pObj0Li );
302  }
303  // add missing nodes in the topological order
304  Aig_ManForEachNode( p0, pObj0, i )
305  {
306  if ( pObj0->pData != NULL )
307  continue;
308  pObj1 = Aig_And( p1, Aig_ObjChild0Copy(pObj0), Aig_ObjChild1Copy(pObj0) );
309  pObj0->pData = pObj1;
310  pObj1->pData = pObj0;
311  }
312  // create register outputs in p0 that are absent in p1
313  Vec_PtrForEachEntry( Aig_Obj_t *, vNewLis, pObj0Li, i )
314  Aig_ObjCreateCo( p1, Aig_ObjChild0Copy(pObj0Li) );
315  // increment the number of registers
316  Aig_ManSetRegNum( p1, Aig_ManRegNum(p1) + Vec_PtrSize(vNewLis) );
317  Vec_PtrFree( vNewLis );
318 }
319 
320 
321 /**Function*************************************************************
322 
323  Synopsis [Derives matching for all pairs.]
324 
325  Description [Modifies both AIGs.]
326 
327  SideEffects []
328 
329  SeeAlso []
330 
331 ***********************************************************************/
332 Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 )
333 {
334  Vec_Int_t * vPairsNew;
335  Aig_Obj_t * pObj0, * pObj1;
336  int i;
337  // check correctness
338  assert( Aig_ManCiNum(p0) == Aig_ManCiNum(p1) );
339  assert( Aig_ManCoNum(p0) == Aig_ManCoNum(p1) );
340  assert( Aig_ManRegNum(p0) == Aig_ManRegNum(p1) );
341  assert( Aig_ManObjNum(p0) == Aig_ManObjNum(p1) );
342  // create complete pairs
343  vPairsNew = Vec_IntAlloc( 2*Aig_ManObjNum(p0) );
344  Aig_ManForEachObj( p0, pObj0, i )
345  {
346  if ( Aig_ObjIsCo(pObj0) )
347  continue;
348  pObj1 = (Aig_Obj_t *)pObj0->pData;
349  Vec_IntPush( vPairsNew, pObj0->Id );
350  Vec_IntPush( vPairsNew, pObj1->Id );
351  }
352  return vPairsNew;
353 }
354 
355 
356 
357 
358 
359 /**Function*************************************************************
360 
361  Synopsis [Transfers the result of matching to miter.]
362 
363  Description [The array of pairs should be complete.]
364 
365  SideEffects []
366 
367  SeeAlso []
368 
369 ***********************************************************************/
370 Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairsAll )
371 {
372  Vec_Int_t * vPairsMiter;
373  Aig_Obj_t * pObj0, * pObj1;
374  int i;
375  // create matching of nodes in the miter
376  vPairsMiter = Vec_IntAlloc( 2*Aig_ManObjNum(p0) );
377  for ( i = 0; i < Vec_IntSize(vPairsAll); i += 2 )
378  {
379  pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairsAll, i) );
380  pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairsAll, i+1) );
381  assert( pObj0->pData != NULL );
382  assert( pObj1->pData != NULL );
383  if ( pObj0->pData == pObj1->pData )
384  continue;
385  if ( Aig_ObjIsNone((Aig_Obj_t *)pObj0->pData) || Aig_ObjIsNone((Aig_Obj_t *)pObj1->pData) )
386  continue;
387  // get the miter nodes
388  pObj0 = (Aig_Obj_t *)pObj0->pData;
389  pObj1 = (Aig_Obj_t *)pObj1->pData;
390  assert( !Aig_IsComplement(pObj0) );
391  assert( !Aig_IsComplement(pObj1) );
392  assert( Aig_ObjType(pObj0) == Aig_ObjType(pObj1) );
393  if ( Aig_ObjIsCo(pObj0) )
394  continue;
395  assert( Aig_ObjIsNode(pObj0) || Saig_ObjIsLo(pMiter, pObj0) );
396  assert( Aig_ObjIsNode(pObj1) || Saig_ObjIsLo(pMiter, pObj1) );
397  assert( pObj0->Id < pObj1->Id );
398  Vec_IntPush( vPairsMiter, pObj0->Id );
399  Vec_IntPush( vPairsMiter, pObj1->Id );
400  }
401  return vPairsMiter;
402 }
403 
404 
405 
406 
407 
408 /**Function*************************************************************
409 
410  Synopsis [Solves SEC using structural similarity.]
411 
412  Description [Modifies both p0 and p1 by adding extra logic.]
413 
414  SideEffects []
415 
416  SeeAlso []
417 
418 ***********************************************************************/
419 Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars )
420 {
421  Ssw_Man_t * p;
422  Vec_Int_t * vPairsAll, * vPairsMiter;
423  Aig_Man_t * pMiter, * pAigNew;
424  // derive full matching
425  Ssw_MatchingStart( p0, p1, vPairs );
426  if ( pPars->nIsleDist )
427  Ssw_MatchingExtend( p0, p1, pPars->nIsleDist, pPars->fVerbose );
428  Ssw_MatchingComplete( p0, p1 );
429  Ssw_MatchingComplete( p1, p0 );
430  vPairsAll = Ssw_MatchingPairs( p0, p1 );
431  // create miter and transfer matching
432  pMiter = Saig_ManCreateMiter( p0, p1, 0 );
433  vPairsMiter = Ssw_MatchingMiter( pMiter, p0, p1, vPairsAll );
434  Vec_IntFree( vPairsAll );
435  // start the induction manager
436  p = Ssw_ManCreate( pMiter, pPars );
437  // create equivalence classes using these IDs
438  if ( p->pPars->fPartSigCorr )
439  p->ppClasses = Ssw_ClassesPreparePairsSimple( pMiter, vPairsMiter );
440  else
441  p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
442  if ( p->pPars->fDumpSRInit )
443  {
444  if ( p->pPars->fPartSigCorr )
445  {
446  Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
447  Aig_ManDumpBlif( pSRed, "srm_part.blif", NULL, NULL );
448  Aig_ManStop( pSRed );
449  Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" );
450  }
451  else
452  Abc_Print( 1, "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" );
453  }
454  p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 );
455  Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
456  // perform refinement of classes
457  pAigNew = Ssw_SignalCorrespondenceRefine( p );
458  // cleanup
459  Ssw_ManStop( p );
460  Aig_ManStop( pMiter );
461  Vec_IntFree( vPairsMiter );
462  return pAigNew;
463 }
464 
465 /**Function*************************************************************
466 
467  Synopsis [Solves SEC with structural similarity.]
468 
469  Description [The first two arguments are pointers to the AIG managers.
470  The third argument is the array of pairs of IDs of structurally equivalent
471  nodes from the first and second managers, respectively.]
472 
473  SideEffects [The managers will be updated by adding "islands of difference".]
474 
475  SeeAlso []
476 
477 ***********************************************************************/
478 int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars )
479 {
480  Ssw_Pars_t Pars;
481  Aig_Man_t * pAigRes;
482  int RetValue;
483  abctime clk = Abc_Clock();
484  // derive parameters if not given
485  if ( pPars == NULL )
486  Ssw_ManSetDefaultParams( pPars = &Pars );
487  // reduce the AIG with pairs
488  pAigRes = Ssw_SecWithSimilaritySweep( p0, p1, vPairs, pPars );
489  // report the result of verification
490  RetValue = Ssw_MiterStatus( pAigRes, 1 );
491  if ( RetValue == 1 )
492  Abc_Print( 1, "Verification successful. " );
493  else if ( RetValue == 0 )
494  Abc_Print( 1, "Verification failed with a counter-example. " );
495  else
496  Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
497  Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) );
498  ABC_PRT( "Time", Abc_Clock() - clk );
499  Aig_ManStop( pAigRes );
500  return RetValue;
501 }
502 
503 /**Function*************************************************************
504 
505  Synopsis [Dummy procedure to detect structural similarity.]
506 
507  Description []
508 
509  SideEffects []
510 
511  SeeAlso []
512 
513 ***********************************************************************/
514 Vec_Int_t * Saig_StrSimPerformMatching_hack( Aig_Man_t * p0, Aig_Man_t * p1 )
515 {
516  Vec_Int_t * vPairs;
517  Aig_Obj_t * pObj;
518  int i;
519  // create array of pairs
520  vPairs = Vec_IntAlloc( 100 );
521  Aig_ManForEachObj( p0, pObj, i )
522  {
523  if ( !Aig_ObjIsConst1(pObj) && !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
524  continue;
525  Vec_IntPush( vPairs, i );
526  Vec_IntPush( vPairs, i );
527  }
528  return vPairs;
529 }
530 
531 /**Function*************************************************************
532 
533  Synopsis [Solves SEC with structural similarity.]
534 
535  Description []
536 
537  SideEffects []
538 
539  SeeAlso []
540 
541 ***********************************************************************/
542 int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
543 {
544  Vec_Int_t * vPairs;
545  Aig_Man_t * pPart0, * pPart1;
546  int RetValue;
547  if ( pPars->fVerbose )
548  Abc_Print( 1, "Performing sequential verification using structural similarity.\n" );
549  // consider the case when a miter is given
550  if ( p1 == NULL )
551  {
552  if ( pPars->fVerbose )
553  {
554  Aig_ManPrintStats( p0 );
555  }
556  // demiter the miter
557  if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
558  {
559  Abc_Print( 1, "Demitering has failed.\n" );
560  return -1;
561  }
562  }
563  else
564  {
565  pPart0 = Aig_ManDupSimple( p0 );
566  pPart1 = Aig_ManDupSimple( p1 );
567  }
568  if ( pPars->fVerbose )
569  {
570 // Aig_ManPrintStats( pPart0 );
571 // Aig_ManPrintStats( pPart1 );
572  if ( p1 == NULL )
573  {
574 // Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
575 // Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
576 // Abc_Print( 1, "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
577  }
578  }
579  assert( Aig_ManRegNum(pPart0) > 0 );
580  assert( Aig_ManRegNum(pPart1) > 0 );
581  assert( Saig_ManPiNum(pPart0) == Saig_ManPiNum(pPart1) );
582  assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) );
583  // derive pairs
584 // vPairs = Saig_StrSimPerformMatching_hack( pPart0, pPart1 );
585  vPairs = Saig_StrSimPerformMatching( pPart0, pPart1, 0, pPars->fVerbose, NULL );
586  RetValue = Ssw_SecWithSimilarityPairs( pPart0, pPart1, vPairs, pPars );
587  Aig_ManStop( pPart0 );
588  Aig_ManStop( pPart1 );
589  Vec_IntFree( vPairs );
590  return RetValue;
591 }
592 
593 ////////////////////////////////////////////////////////////////////////
594 /// END OF FILE ///
595 ////////////////////////////////////////////////////////////////////////
596 
597 
598 ABC_NAMESPACE_IMPL_END
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Aig_ObjForEachFanout
#define Aig_ObjForEachFanout(p, pObj, pFanout, iFan, i)
Definition: aig.h:427
Ssw_ManStop
void Ssw_ManStop(Ssw_Man_t *p)
Definition: sswMan.c:189
Ssw_CreatePair
ABC_NAMESPACE_IMPL_START void Ssw_CreatePair(Vec_Int_t *vPairs, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
DECLARATIONS ///.
Definition: sswIslands.c:45
Ssw_SmlObjHashWord
unsigned Ssw_SmlObjHashWord(Ssw_Sml_t *p, Aig_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition: sswSim.c:63
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Ssw_SecWithSimilarity
int Ssw_SecWithSimilarity(Aig_Man_t *p0, Aig_Man_t *p1, Ssw_Pars_t *pPars)
Definition: sswIslands.c:542
Aig_ObjType
static Aig_Type_t Aig_ObjType(Aig_Obj_t *pObj)
Definition: aig.h:272
Ssw_MatchingExtendOne
void Ssw_MatchingExtendOne(Aig_Man_t *p, Vec_Ptr_t *vNodes)
Definition: sswIslands.c:130
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
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
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Aig_ManObjNum
static int Aig_ManObjNum(Aig_Man_t *p)
Definition: aig.h:258
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Ssw_Pars_t
typedefABC_NAMESPACE_HEADER_START struct Ssw_Pars_t_ Ssw_Pars_t
INCLUDES ///.
Definition: ssw.h:40
Saig_StrSimPerformMatching_hack
Vec_Int_t * Saig_StrSimPerformMatching_hack(Aig_Man_t *p0, Aig_Man_t *p1)
Definition: sswIslands.c:514
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Ssw_MatchingComplete
void Ssw_MatchingComplete(Aig_Man_t *p0, Aig_Man_t *p1)
Definition: sswIslands.c:287
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Aig_ManObj
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
Saig_StrSimPerformMatching
Vec_Int_t * Saig_StrSimPerformMatching(Aig_Man_t *p0, Aig_Man_t *p1, int nDist, int fVerbose, Aig_Man_t **ppMiter)
Definition: saigStrSim.c:873
Ssw_Man_t
typedefABC_NAMESPACE_HEADER_START struct Ssw_Man_t_ Ssw_Man_t
INCLUDES ///.
Definition: sswInt.h:47
Ssw_ClassesPreparePairsSimple
Ssw_Cla_t * Ssw_ClassesPreparePairsSimple(Aig_Man_t *pMiter, Vec_Int_t *vPairs)
Definition: sswClass.c:928
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Ssw_SmlObjIsConstWord
int Ssw_SmlObjIsConstWord(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition: sswSim.c:102
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Saig_ObjIsLi
static int Saig_ObjIsLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:85
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_ManFanoutStart
void Aig_ManFanoutStart(Aig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: aigFanout.c:56
Aig_ManFanoutStop
void Aig_ManFanoutStop(Aig_Man_t *p)
Definition: aigFanout.c:89
Saig_ManDemiterSimpleDiff
int Saig_ManDemiterSimpleDiff(Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
Definition: saigMiter.c:660
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Ssw_ManCreate
Ssw_Man_t * Ssw_ManCreate(Aig_Man_t *pAig, Ssw_Pars_t *pPars)
DECLARATIONS ///.
Definition: sswMan.c:45
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Saig_ManCreateMiter
Aig_Man_t * Saig_ManCreateMiter(Aig_Man_t *p1, Aig_Man_t *p2, int Oper)
Definition: saigMiter.c:100
Ssw_ClassesPrepare
Ssw_Cla_t * Ssw_ClassesPrepare(Aig_Man_t *pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose)
Definition: sswClass.c:596
Ssw_MatchingCountUnmached
int Ssw_MatchingCountUnmached(Aig_Man_t *p)
Definition: sswIslands.c:193
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
Ssw_MatchingStart
void Ssw_MatchingStart(Aig_Man_t *p0, Aig_Man_t *p1, Vec_Int_t *vPairs)
Definition: sswIslands.c:64
Ssw_SmlObjsAreEqualWord
int Ssw_SmlObjsAreEqualWord(Ssw_Sml_t *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition: sswSim.c:124
Ssw_MatchingExtend
void Ssw_MatchingExtend(Aig_Man_t *p0, Aig_Man_t *p1, int nDist, int fVerbose)
Definition: sswIslands.c:219
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
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
Aig_ObjIsNone
static int Aig_ObjIsNone(Aig_Obj_t *pObj)
Definition: aig.h:273
Ssw_ManSetDefaultParams
void Ssw_ManSetDefaultParams(Ssw_Pars_t *p)
DECLARATIONS ///.
Definition: sswCore.c:45
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Saig_ObjIsPo
static int Saig_ObjIsPo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:83
Saig_ObjLiToLo
static Aig_Obj_t * Saig_ObjLiToLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:87
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
if
if(last==0)
Definition: sparse_int.h:34
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Ssw_MatchingPairs
Vec_Int_t * Ssw_MatchingPairs(Aig_Man_t *p0, Aig_Man_t *p1)
Definition: sswIslands.c:332
Aig_ObjChild1Copy
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Ssw_SignalCorrespondenceRefine
Aig_Man_t * Ssw_SignalCorrespondenceRefine(Ssw_Man_t *p)
Definition: sswCore.c:234
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Ssw_MatchingMiter
Vec_Int_t * Ssw_MatchingMiter(Aig_Man_t *pMiter, Aig_Man_t *p0, Aig_Man_t *p1, Vec_Int_t *vPairsAll)
Definition: sswIslands.c:370
Counter
static int Counter
Definition: extraBddMisc.c:1877
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Aig_ObjChild0Copy
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
Aig_ManDumpBlif
void Aig_ManDumpBlif(Aig_Man_t *p, char *pFileName, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vPoNames)
Definition: aigUtil.c:733
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Ssw_SecWithSimilarityPairs
int Ssw_SecWithSimilarityPairs(Aig_Man_t *p0, Aig_Man_t *p1, Vec_Int_t *vPairs, Ssw_Pars_t *pPars)
Definition: sswIslands.c:478
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Ssw_SecWithSimilaritySweep
Aig_Man_t * Ssw_SecWithSimilaritySweep(Aig_Man_t *p0, Aig_Man_t *p1, Vec_Int_t *vPairs, Ssw_Pars_t *pPars)
Definition: sswIslands.c:419
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_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Ssw_MiterStatus
int Ssw_MiterStatus(Aig_Man_t *p, int fVerbose)
DECLARATIONS ///.
Definition: sswPairs.c:45
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Ssw_SpeculativeReduction
Aig_Man_t * Ssw_SpeculativeReduction(Ssw_Man_t *p)
Definition: sswAig.c:212
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Aig_ManDupSimple
Aig_Man_t * Aig_ManDupSimple(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigDup.c:46
Ssw_SmlStart
Ssw_Sml_t * Ssw_SmlStart(Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
Definition: sswSim.c:1148
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