abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraLcr.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [fraLcorr.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [New FRAIG package.]
8 
9  Synopsis [Latch correspondence computation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 30, 2007.]
16 
17  Revision [$Id: fraLcorr.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "fra.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 typedef struct Fra_Lcr_t_ Fra_Lcr_t;
31 struct Fra_Lcr_t_
32 {
33  // original AIG
34  Aig_Man_t * pAig;
35  // equivalence class representation
36  Fra_Cla_t * pCla;
37  // partitioning information
38  Vec_Ptr_t * vParts; // output partitions
39  int * pInToOutPart; // mapping of PI num into PO partition num
40  int * pInToOutNum; // mapping of PI num into the num of this PO in the partition
41  // AIGs for the partitions
42  Vec_Ptr_t * vFraigs;
43  // other variables
44  int fRefining;
45  // parameters
46  int nFramesP;
47  int fVerbose;
48  // statistics
49  int nIters;
50  int nLitsBeg;
51  int nLitsEnd;
52  int nNodesBeg;
53  int nNodesEnd;
54  int nRegsBeg;
55  int nRegsEnd;
56  // runtime
57  abctime timeSim;
58  abctime timePart;
59  abctime timeTrav;
60  abctime timeFraig;
61  abctime timeUpdate;
62  abctime timeTotal;
63 };
64 
65 ////////////////////////////////////////////////////////////////////////
66 /// FUNCTION DEFINITIONS ///
67 ////////////////////////////////////////////////////////////////////////
68 
69 /**Function*************************************************************
70 
71  Synopsis [Allocates the retiming manager.]
72 
73  Description []
74 
75  SideEffects []
76 
77  SeeAlso []
78 
79 ***********************************************************************/
80 Fra_Lcr_t * Lcr_ManAlloc( Aig_Man_t * pAig )
81 {
82  Fra_Lcr_t * p;
83  p = ABC_ALLOC( Fra_Lcr_t, 1 );
84  memset( p, 0, sizeof(Fra_Lcr_t) );
85  p->pAig = pAig;
86  p->pInToOutPart = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
87  memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManCiNum(pAig) );
88  p->pInToOutNum = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
89  memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManCiNum(pAig) );
90  p->vFraigs = Vec_PtrAlloc( 1000 );
91  return p;
92 }
93 
94 /**Function*************************************************************
95 
96  Synopsis [Prints stats for the fraiging manager.]
97 
98  Description []
99 
100  SideEffects []
101 
102  SeeAlso []
103 
104 ***********************************************************************/
105 void Lcr_ManPrint( Fra_Lcr_t * p )
106 {
107  printf( "Iterations = %d. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n",
108  p->nIters, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
109  printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
110  p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg,
111  p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
112  ABC_PRT( "AIG simulation ", p->timeSim );
113  ABC_PRT( "AIG partitioning", p->timePart );
114  ABC_PRT( "AIG rebuiding ", p->timeTrav );
115  ABC_PRT( "FRAIGing ", p->timeFraig );
116  ABC_PRT( "AIG updating ", p->timeUpdate );
117  ABC_PRT( "TOTAL RUNTIME ", p->timeTotal );
118 }
119 
120 /**Function*************************************************************
121 
122  Synopsis [Deallocates the retiming manager.]
123 
124  Description []
125 
126  SideEffects []
127 
128  SeeAlso []
129 
130 ***********************************************************************/
131 void Lcr_ManFree( Fra_Lcr_t * p )
132 {
133  Aig_Obj_t * pObj;
134  int i;
135  if ( p->fVerbose )
136  Lcr_ManPrint( p );
137  Aig_ManForEachCi( p->pAig, pObj, i )
138  pObj->pNext = NULL;
139  Vec_PtrFree( p->vFraigs );
140  if ( p->pCla ) Fra_ClassesStop( p->pCla );
141  if ( p->vParts ) Vec_VecFree( (Vec_Vec_t *)p->vParts );
142  ABC_FREE( p->pInToOutPart );
143  ABC_FREE( p->pInToOutNum );
144  ABC_FREE( p );
145 }
146 
147 /**Function*************************************************************
148 
149  Synopsis [Prepare the AIG for class computation.]
150 
151  Description []
152 
153  SideEffects []
154 
155  SeeAlso []
156 
157 ***********************************************************************/
158 Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig )
159 {
160  Fra_Man_t * p;
161  Aig_Obj_t * pObj;
162  int i;
163  p = ABC_ALLOC( Fra_Man_t, 1 );
164  memset( p, 0, sizeof(Fra_Man_t) );
165 // Aig_ManForEachCi( pAig, pObj, i )
166  Aig_ManForEachObj( pAig, pObj, i )
167  pObj->pData = p;
168  return p;
169 }
170 
171 /**Function*************************************************************
172 
173  Synopsis [Prepare the AIG for class computation.]
174 
175  Description []
176 
177  SideEffects []
178 
179  SeeAlso []
180 
181 ***********************************************************************/
182 void Fra_LcrAigPrepareTwo( Aig_Man_t * pAig, Fra_Man_t * p )
183 {
184  Aig_Obj_t * pObj;
185  int i;
186  Aig_ManForEachCi( pAig, pObj, i )
187  pObj->pData = p;
188 }
189 
190 /**Function*************************************************************
191 
192  Synopsis [Compares two nodes for equivalence after partitioned fraiging.]
193 
194  Description []
195 
196  SideEffects []
197 
198  SeeAlso []
199 
200 ***********************************************************************/
201 int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
202 {
203  Fra_Man_t * pTemp = (Fra_Man_t *)pObj0->pData;
204  Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
205  Aig_Man_t * pFraig;
206  Aig_Obj_t * pOut0, * pOut1;
207  int nPart0, nPart1;
208  assert( Aig_ObjIsCi(pObj0) );
209  assert( Aig_ObjIsCi(pObj1) );
210  // find the partition to which these nodes belong
211  nPart0 = pLcr->pInToOutPart[(long)pObj0->pNext];
212  nPart1 = pLcr->pInToOutPart[(long)pObj1->pNext];
213  // if this is the result of refinement of the class created const-1 nodes
214  // the nodes may end up in different partions - we assume them equivalent
215  if ( nPart0 != nPart1 )
216  {
217  assert( 0 );
218  return 1;
219  }
220  assert( nPart0 == nPart1 );
221  pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart0 );
222  // get the fraig outputs
223  pOut0 = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj0->pNext] );
224  pOut1 = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj1->pNext] );
225  return Aig_ObjFanin0(pOut0) == Aig_ObjFanin0(pOut1);
226 }
227 
228 /**Function*************************************************************
229 
230  Synopsis [Compares the node with a constant after partioned fraiging.]
231 
232  Description []
233 
234  SideEffects []
235 
236  SeeAlso []
237 
238 ***********************************************************************/
239 int Fra_LcrNodeIsConst( Aig_Obj_t * pObj )
240 {
241  Fra_Man_t * pTemp = (Fra_Man_t *)pObj->pData;
242  Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
243  Aig_Man_t * pFraig;
244  Aig_Obj_t * pOut;
245  int nPart;
246  assert( Aig_ObjIsCi(pObj) );
247  // find the partition to which these nodes belong
248  nPart = pLcr->pInToOutPart[(long)pObj->pNext];
249  pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart );
250  // get the fraig outputs
251  pOut = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj->pNext] );
252  return Aig_ObjFanin0(pOut) == Aig_ManConst1(pFraig);
253 }
254 
255 /**Function*************************************************************
256 
257  Synopsis [Duplicates the AIG manager recursively.]
258 
259  Description []
260 
261  SideEffects []
262 
263  SeeAlso []
264 
265 ***********************************************************************/
266 Aig_Obj_t * Fra_LcrManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
267 {
268  Aig_Obj_t * pObjNew;
269  if ( pObj->pData )
270  return (Aig_Obj_t *)pObj->pData;
271  Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
272  if ( Aig_ObjIsBuf(pObj) )
273  return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
274  Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
275  pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
276  return (Aig_Obj_t *)(pObj->pData = pObjNew);
277 }
278 
279 /**Function*************************************************************
280 
281  Synopsis [Give the AIG and classes, reduces AIG for partitioning.]
282 
283  Description [Ignores registers that are not in the classes.
284  Places candidate equivalent classes of registers into single outputs
285  (for ease of partitioning). The resulting combinational AIG contains
286  outputs in the same order as equivalence classes of registers,
287  followed by constant-1 registers. Preserves the set of all inputs.
288  Complemented attributes of the outputs do not matter because we need
289  then only for collecting the structural info.]
290 
291  SideEffects []
292 
293  SeeAlso []
294 
295 ***********************************************************************/
296 Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
297 {
298  Aig_Man_t * pNew;
299  Aig_Obj_t * pObj, * pObjPo, * pObjNew, ** ppClass, * pMiter;
300  int i, c, Offset;
301  // remember the numbers of the inputs of the original AIG
302  Aig_ManForEachCi( pLcr->pAig, pObj, i )
303  {
304  pObj->pData = pLcr;
305  pObj->pNext = (Aig_Obj_t *)(long)i;
306  }
307  // compute the LO/LI offset
308  Offset = Aig_ManCoNum(pLcr->pAig) - Aig_ManCiNum(pLcr->pAig);
309  // create the PIs
310  Aig_ManCleanData( pLcr->pAig );
311  pNew = Aig_ManStartFrom( pLcr->pAig );
312  // go over the equivalence classes
313  Vec_PtrForEachEntry( Aig_Obj_t **, pLcr->pCla->vClasses, ppClass, i )
314  {
315  pMiter = Aig_ManConst0(pNew);
316  for ( c = 0; ppClass[c]; c++ )
317  {
318  assert( Aig_ObjIsCi(ppClass[c]) );
319  pObjPo = Aig_ManCo( pLcr->pAig, Offset+(long)ppClass[c]->pNext );
320  pObjNew = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
321  pMiter = Aig_Exor( pNew, pMiter, pObjNew );
322  }
323  Aig_ObjCreateCo( pNew, pMiter );
324  }
325  // go over the constant candidates
326  Vec_PtrForEachEntry( Aig_Obj_t *, pLcr->pCla->vClasses1, pObj, i )
327  {
328  assert( Aig_ObjIsCi(pObj) );
329  pObjPo = Aig_ManCo( pLcr->pAig, Offset+(long)pObj->pNext );
330  pMiter = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
331  Aig_ObjCreateCo( pNew, pMiter );
332  }
333  return pNew;
334 }
335 
336 /**Function*************************************************************
337 
338  Synopsis [Remaps partitions into the inputs of original AIG.]
339 
340  Description []
341 
342  SideEffects []
343 
344  SeeAlso []
345 
346 ***********************************************************************/
347 void Fra_LcrRemapPartitions( Vec_Ptr_t * vParts, Fra_Cla_t * pCla, int * pInToOutPart, int * pInToOutNum )
348 {
349  Vec_Int_t * vOne, * vOneNew;
350  Aig_Obj_t ** ppClass, * pObjPi;
351  int Out, Offset, i, k, c;
352  // compute the LO/LI offset
353  Offset = Aig_ManCoNum(pCla->pAig) - Aig_ManCiNum(pCla->pAig);
354  Vec_PtrForEachEntry( Vec_Int_t *, vParts, vOne, i )
355  {
356  vOneNew = Vec_IntAlloc( Vec_IntSize(vOne) );
357  Vec_IntForEachEntry( vOne, Out, k )
358  {
359  if ( Out < Vec_PtrSize(pCla->vClasses) )
360  {
361  ppClass = (Aig_Obj_t **)Vec_PtrEntry( pCla->vClasses, Out );
362  for ( c = 0; ppClass[c]; c++ )
363  {
364  pInToOutPart[(long)ppClass[c]->pNext] = i;
365  pInToOutNum[(long)ppClass[c]->pNext] = Vec_IntSize(vOneNew);
366  Vec_IntPush( vOneNew, Offset+(long)ppClass[c]->pNext );
367  }
368  }
369  else
370  {
371  pObjPi = (Aig_Obj_t *)Vec_PtrEntry( pCla->vClasses1, Out - Vec_PtrSize(pCla->vClasses) );
372  pInToOutPart[(long)pObjPi->pNext] = i;
373  pInToOutNum[(long)pObjPi->pNext] = Vec_IntSize(vOneNew);
374  Vec_IntPush( vOneNew, Offset+(long)pObjPi->pNext );
375  }
376  }
377  // replace the class
378  Vec_PtrWriteEntry( vParts, i, vOneNew );
379  Vec_IntFree( vOne );
380  }
381 }
382 
383 /**Function*************************************************************
384 
385  Synopsis [Creates AIG of one partition with speculative reduction.]
386 
387  Description []
388 
389  SideEffects []
390 
391  SeeAlso []
392 
393 ***********************************************************************/
394 Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
395 {
396  assert( !Aig_IsComplement(pObj) );
397  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
398  return (Aig_Obj_t *)pObj->pData;
399  Aig_ObjSetTravIdCurrent(p, pObj);
400  if ( Aig_ObjIsCi(pObj) )
401  {
402 // Aig_Obj_t * pRepr = Fra_ClassObjRepr(pObj);
403  Aig_Obj_t * pRepr = pCla->pMemRepr[pObj->Id];
404  if ( pRepr == NULL )
405  pObj->pData = Aig_ObjCreateCi( pNew );
406  else
407  {
408  pObj->pData = Fra_LcrCreatePart_rec( pCla, pNew, p, pRepr );
409  pObj->pData = Aig_NotCond( (Aig_Obj_t *)pObj->pData, pRepr->fPhase ^ pObj->fPhase );
410  }
411  return (Aig_Obj_t *)pObj->pData;
412  }
413  Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin0(pObj) );
414  Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin1(pObj) );
415  return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
416 }
417 
418 /**Function*************************************************************
419 
420  Synopsis [Creates AIG of one partition with speculative reduction.]
421 
422  Description []
423 
424  SideEffects []
425 
426  SeeAlso []
427 
428 ***********************************************************************/
429 Aig_Man_t * Fra_LcrCreatePart( Fra_Lcr_t * p, Vec_Int_t * vPart )
430 {
431  Aig_Man_t * pNew;
432  Aig_Obj_t * pObj, * pObjNew;
433  int Out, i;
434  // create new AIG for this partition
435  pNew = Aig_ManStartFrom( p->pAig );
436  Aig_ManIncrementTravId( p->pAig );
437  Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
438  Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
439  Vec_IntForEachEntry( vPart, Out, i )
440  {
441  pObj = Aig_ManCo( p->pAig, Out );
442  if ( pObj->fMarkA )
443  {
444  pObjNew = Fra_LcrCreatePart_rec( p->pCla, pNew, p->pAig, Aig_ObjFanin0(pObj) );
445  pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
446  }
447  else
448  pObjNew = Aig_ManConst1( pNew );
449  Aig_ObjCreateCo( pNew, pObjNew );
450  }
451  return pNew;
452 }
453 
454 /**Function*************************************************************
455 
456  Synopsis [Marks the nodes belonging to the equivalence classes.]
457 
458  Description []
459 
460  SideEffects []
461 
462  SeeAlso []
463 
464 ***********************************************************************/
465 void Fra_ClassNodesMark( Fra_Lcr_t * p )
466 {
467  Aig_Obj_t * pObj, ** ppClass;
468  int i, c, Offset;
469  // compute the LO/LI offset
470  Offset = Aig_ManCoNum(p->pCla->pAig) - Aig_ManCiNum(p->pCla->pAig);
471  // mark the nodes remaining in the classes
472  Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i )
473  {
474  pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)pObj->pNext );
475  pObj->fMarkA = 1;
476  }
477  Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i )
478  {
479  for ( c = 0; ppClass[c]; c++ )
480  {
481  pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext );
482  pObj->fMarkA = 1;
483  }
484  }
485 }
486 
487 /**Function*************************************************************
488 
489  Synopsis [Unmarks the nodes belonging to the equivalence classes.]
490 
491  Description []
492 
493  SideEffects []
494 
495  SeeAlso []
496 
497 ***********************************************************************/
498 void Fra_ClassNodesUnmark( Fra_Lcr_t * p )
499 {
500  Aig_Obj_t * pObj, ** ppClass;
501  int i, c, Offset;
502  // compute the LO/LI offset
503  Offset = Aig_ManCoNum(p->pCla->pAig) - Aig_ManCiNum(p->pCla->pAig);
504  // mark the nodes remaining in the classes
505  Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i )
506  {
507  pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)pObj->pNext );
508  pObj->fMarkA = 0;
509  }
510  Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i )
511  {
512  for ( c = 0; ppClass[c]; c++ )
513  {
514  pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext );
515  pObj->fMarkA = 0;
516  }
517  }
518 }
519 
520 /**Function*************************************************************
521 
522  Synopsis [Performs choicing of the AIG.]
523 
524  Description []
525 
526  SideEffects []
527 
528  SeeAlso []
529 
530 ***********************************************************************/
531 Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit )
532 {
533  int nPartSize = 200;
534  int fReprSelect = 0;
535  Fra_Lcr_t * p;
536  Fra_Sml_t * pSml;
537  Fra_Man_t * pTemp;
538  Aig_Man_t * pAigPart, * pAigTemp, * pAigNew = NULL;
539  Vec_Int_t * vPart;
540  int i, nIter;
541  abctime timeSim, clk2, clk3, clk = Abc_Clock();
542  abctime TimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
543  if ( Aig_ManNodeNum(pAig) == 0 )
544  {
545  if ( pnIter ) *pnIter = 0;
546  // Ntl_ManFinalize() requires the following to satisfy an assertion.
547  Aig_ManReprStart(pAig,Aig_ManObjNumMax(pAig));
548  return Aig_ManDupOrdered(pAig);
549  }
550  assert( Aig_ManRegNum(pAig) > 0 );
551 
552  // simulate the AIG
553 clk2 = Abc_Clock();
554 if ( fVerbose )
555 printf( "Simulating AIG with %d nodes for %d cycles ... ", Aig_ManNodeNum(pAig), nFramesP + 32 );
556  pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1, 1 );
557 if ( fVerbose )
558 {
559 ABC_PRT( "Time", Abc_Clock() - clk2 );
560 }
561 timeSim = Abc_Clock() - clk2;
562 
563  // check if simulation discovered non-constant-0 POs
564  if ( fProve && pSml->fNonConstOut )
565  {
566  pAig->pSeqModel = Fra_SmlGetCounterExample( pSml );
567  Fra_SmlStop( pSml );
568  return NULL;
569  }
570 
571  // start the manager
572  p = Lcr_ManAlloc( pAig );
573  p->nFramesP = nFramesP;
574  p->fVerbose = fVerbose;
575  p->timeSim += timeSim;
576 
577  pTemp = Fra_LcrAigPrepare( pAig );
578  pTemp->pBmc = (Fra_Bmc_t *)p;
579  pTemp->pSml = pSml;
580 
581  // get preliminary info about equivalence classes
582  pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
583  Fra_ClassesPrepare( p->pCla, 1, 0 );
584  p->pCla->pFuncNodeIsConst = Fra_LcrNodeIsConst;
585  p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual;
586  Fra_SmlStop( pTemp->pSml );
587 
588  // partition the AIG for latch correspondence computation
589 clk2 = Abc_Clock();
590 if ( fVerbose )
591 printf( "Partitioning AIG ... " );
592  pAigPart = Fra_LcrDeriveAigForPartitioning( p );
593  p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
594  Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
595  Aig_ManStop( pAigPart );
596 if ( fVerbose )
597 {
598 ABC_PRT( "Time", Abc_Clock() - clk2 );
599 p->timePart += Abc_Clock() - clk2;
600 }
601 
602  // get the initial stats
603  p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
604  p->nNodesBeg = Aig_ManNodeNum(p->pAig);
605  p->nRegsBeg = Aig_ManRegNum(p->pAig);
606 
607  // perforn interative reduction of the partitions
608  p->fRefining = 1;
609  for ( nIter = 0; p->fRefining; nIter++ )
610  {
611  p->fRefining = 0;
612  clk3 = Abc_Clock();
613  // derive AIGs for each partition
614  Fra_ClassNodesMark( p );
615  Vec_PtrClear( p->vFraigs );
616  Vec_PtrForEachEntry( Vec_Int_t *, p->vParts, vPart, i )
617  {
618  if ( TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
619  {
620  Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i )
621  Aig_ManStop( pAigPart );
622  Aig_ManCleanMarkA( pAig );
623  Aig_ManCleanMarkB( pAig );
624  printf( "Fra_FraigLatchCorrespondence(): Runtime limit exceeded.\n" );
625  goto finish;
626  }
627 clk2 = Abc_Clock();
628  pAigPart = Fra_LcrCreatePart( p, vPart );
629 p->timeTrav += Abc_Clock() - clk2;
630 clk2 = Abc_Clock();
631  pAigTemp = Fra_FraigEquivence( pAigPart, nConfMax, 0 );
632 p->timeFraig += Abc_Clock() - clk2;
633  Vec_PtrPush( p->vFraigs, pAigTemp );
634 /*
635  {
636  char Name[1000];
637  sprintf( Name, "part%04d.blif", i );
638  Aig_ManDumpBlif( pAigPart, Name, NULL, NULL );
639  }
640 printf( "Finished part %4d (out of %4d). ", i, Vec_PtrSize(p->vParts) );
641 ABC_PRT( "Time", Abc_Clock() - clk3 );
642 */
643 
644  Aig_ManStop( pAigPart );
645  }
646  Fra_ClassNodesUnmark( p );
647  // report the intermediate results
648  if ( fVerbose )
649  {
650  printf( "%3d : Const = %6d. Class = %6d. L = %6d. Part = %3d. ",
651  nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
652  Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) );
653  ABC_PRT( "T", Abc_Clock() - clk3 );
654  }
655  // refine the classes
656  Fra_LcrAigPrepareTwo( p->pAig, pTemp );
657  if ( Fra_ClassesRefine( p->pCla ) )
658  p->fRefining = 1;
659  if ( Fra_ClassesRefine1( p->pCla, 0, NULL ) )
660  p->fRefining = 1;
661  // clean the fraigs
662  Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i )
663  Aig_ManStop( pAigPart );
664 
665  // repartition if needed
666  if ( 1 )
667  {
668 clk2 = Abc_Clock();
669  Vec_VecFree( (Vec_Vec_t *)p->vParts );
670  pAigPart = Fra_LcrDeriveAigForPartitioning( p );
671  p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
672  Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
673  Aig_ManStop( pAigPart );
674 p->timePart += Abc_Clock() - clk2;
675  }
676  }
677  p->nIters = nIter;
678 
679  // move the classes into representatives and reduce AIG
680 clk2 = Abc_Clock();
681 // Fra_ClassesPrint( p->pCla, 1 );
682  if ( fReprSelect )
683  Fra_ClassesSelectRepr( p->pCla );
684  Fra_ClassesCopyReprs( p->pCla, NULL );
685  pAigNew = Aig_ManDupRepr( p->pAig, 0 );
686  Aig_ManSeqCleanup( pAigNew );
687 // Aig_ManCountMergeRegs( pAigNew );
688 p->timeUpdate += Abc_Clock() - clk2;
689 p->timeTotal = Abc_Clock() - clk;
690  // get the final stats
691  p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
692  p->nNodesEnd = Aig_ManNodeNum(pAigNew);
693  p->nRegsEnd = Aig_ManRegNum(pAigNew);
694 finish:
695  ABC_FREE( pTemp );
696  Lcr_ManFree( p );
697  if ( pnIter ) *pnIter = nIter;
698  return pAigNew;
699 }
700 
701 
702 ////////////////////////////////////////////////////////////////////////
703 /// END OF FILE ///
704 ////////////////////////////////////////////////////////////////////////
705 
706 
707 ABC_NAMESPACE_IMPL_END
708 
memset
char * memset()
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Fra_Lcr_t
typedefABC_NAMESPACE_IMPL_START struct Fra_Lcr_t_ Fra_Lcr_t
DECLARATIONS ///.
Definition: fraLcr.c:30
Fra_Sml_t_::fNonConstOut
int fNonConstOut
Definition: fra.h:179
Fra_ClassesRefine1
int Fra_ClassesRefine1(Fra_Cla_t *p, int fRefineNewClass, int *pSkipped)
Definition: fraClass.c:527
Fra_Lcr_t_::vFraigs
Vec_Ptr_t * vFraigs
Definition: fraLcr.c:42
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Fra_LcrCreatePart
Aig_Man_t * Fra_LcrCreatePart(Fra_Lcr_t *p, Vec_Int_t *vPart)
Definition: fraLcr.c:429
Fra_Cla_t_
Definition: fra.h:150
Aig_ObjType
static Aig_Type_t Aig_ObjType(Aig_Obj_t *pObj)
Definition: aig.h:272
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
Aig_ManPartitionSmart
Vec_Ptr_t * Aig_ManPartitionSmart(Aig_Man_t *p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t **pvPartSupps)
Definition: aigPart.c:686
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
Fra_SmlSimulateSeq
Fra_Sml_t * Fra_SmlSimulateSeq(Aig_Man_t *pAig, int nPref, int nFrames, int nWords, int fCheckMiter)
Definition: fraSim.c:1021
Aig_ManSeqCleanup
int Aig_ManSeqCleanup(Aig_Man_t *p)
Definition: aigScl.c:158
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Fra_ClassesStart
Fra_Cla_t * Fra_ClassesStart(Aig_Man_t *pAig)
FUNCTION DEFINITIONS ///.
Definition: fraClass.c:60
Fra_Man_t_::pCla
Fra_Cla_t * pCla
Definition: fra.h:198
Fra_Lcr_t_::timeTrav
abctime timeTrav
Definition: fraLcr.c:59
Fra_FraigEquivence
Aig_Man_t * Fra_FraigEquivence(Aig_Man_t *pManAig, int nConfMax, int fProve)
Definition: fraCore.c:468
Fra_Cla_t_::vClasses
Vec_Ptr_t * vClasses
Definition: fra.h:154
Fra_ClassesCountLits
int Fra_ClassesCountLits(Fra_Cla_t *p)
Definition: fraClass.c:164
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Aig_Exor
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:220
Fra_Man_t_::pSml
Fra_Sml_t * pSml
Definition: fra.h:200
Aig_ManDupOrdered
Aig_Man_t * Aig_ManDupOrdered(Aig_Man_t *p)
Definition: aigDup.c:277
Fra_Cla_t_::pMemRepr
Aig_Obj_t ** pMemRepr
Definition: fra.h:153
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManCleanMarkB
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition: aigUtil.c:167
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Fra_Lcr_t_::nNodesBeg
int nNodesBeg
Definition: fraLcr.c:52
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition: aig.h:79
Aig_ManConst0
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Fra_LcrAigPrepareTwo
void Fra_LcrAigPrepareTwo(Aig_Man_t *pAig, Fra_Man_t *p)
Definition: fraLcr.c:182
Fra_Lcr_t_::timeFraig
abctime timeFraig
Definition: fraLcr.c:60
Fra_Lcr_t_::fRefining
int fRefining
Definition: fraLcr.c:44
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
Vec_VecFree
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Fra_Bmc_t_
DECLARATIONS ///.
Definition: fraBmc.c:31
Aig_Oper
Aig_Obj_t * Aig_Oper(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1, Aig_Type_t Type)
Definition: aigOper.c:83
Fra_Lcr_t_::pCla
Fra_Cla_t * pCla
Definition: fraLcr.c:36
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
Fra_LcrManDup_rec
Aig_Obj_t * Fra_LcrManDup_rec(Aig_Man_t *pNew, Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: fraLcr.c:266
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Fra_Man_t_::pBmc
Fra_Bmc_t * pBmc
Definition: fra.h:202
Fra_Lcr_t_::nRegsEnd
int nRegsEnd
Definition: fraLcr.c:55
Fra_ClassNodesMark
void Fra_ClassNodesMark(Fra_Lcr_t *p)
Definition: fraLcr.c:465
Fra_Lcr_t_::pAig
Aig_Man_t * pAig
Definition: fraLcr.c:34
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Fra_ClassesPrepare
void Fra_ClassesPrepare(Fra_Cla_t *p, int fLatchCorr, int nMaxLevs)
Definition: fraClass.c:276
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Fra_SmlGetCounterExample
Abc_Cex_t * Fra_SmlGetCounterExample(Fra_Sml_t *p)
Definition: fraSim.c:1043
Aig_ObjIsBuf
static int Aig_ObjIsBuf(Aig_Obj_t *pObj)
Definition: aig.h:277
Fra_Sml_t_
Definition: fra.h:171
Fra_Lcr_t_::nIters
int nIters
Definition: fraLcr.c:49
Lcr_ManFree
void Lcr_ManFree(Fra_Lcr_t *p)
Definition: fraLcr.c:131
Aig_ManReprStart
void Aig_ManReprStart(Aig_Man_t *p, int nIdMax)
DECLARATIONS ///.
Definition: aigRepr.c:45
Fra_Lcr_t_::nFramesP
int nFramesP
Definition: fraLcr.c:46
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Fra_Lcr_t_::nLitsEnd
int nLitsEnd
Definition: fraLcr.c:51
Fra_LcrNodeIsConst
int Fra_LcrNodeIsConst(Aig_Obj_t *pObj)
Definition: fraLcr.c:239
Fra_LcrAigPrepare
Fra_Man_t * Fra_LcrAigPrepare(Aig_Man_t *pAig)
Definition: fraLcr.c:158
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_ObjChild1Copy
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Fra_Lcr_t_::nNodesEnd
int nNodesEnd
Definition: fraLcr.c:53
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Aig_Obj_t_::pNext
Aig_Obj_t * pNext
Definition: aig.h:72
Aig_ObjChild0Copy
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
Fra_ClassesStop
void Fra_ClassesStop(Fra_Cla_t *p)
Definition: fraClass.c:90
Aig_ManStartFrom
Aig_Man_t * Aig_ManStartFrom(Aig_Man_t *p)
Definition: aigMan.c:92
Aig_ManDupRepr
Aig_Man_t * Aig_ManDupRepr(Aig_Man_t *p, int fOrdered)
Definition: aigRepr.c:267
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
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
Fra_LcrNodesAreEqual
int Fra_LcrNodesAreEqual(Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition: fraLcr.c:201
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
Fra_Cla_t_::vClasses1
Vec_Ptr_t * vClasses1
Definition: fra.h:155
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Fra_Lcr_t_::nLitsBeg
int nLitsBeg
Definition: fraLcr.c:50
Fra_Lcr_t_::vParts
Vec_Ptr_t * vParts
Definition: fraLcr.c:38
Fra_Cla_t_::pAig
Aig_Man_t * pAig
Definition: fra.h:152
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Fra_ClassesSelectRepr
void Fra_ClassesSelectRepr(Fra_Cla_t *p)
Definition: fraClass.c:706
Fra_LcrDeriveAigForPartitioning
Aig_Man_t * Fra_LcrDeriveAigForPartitioning(Fra_Lcr_t *pLcr)
Definition: fraLcr.c:296
Fra_Lcr_t_::fVerbose
int fVerbose
Definition: fraLcr.c:47
Fra_ClassNodesUnmark
void Fra_ClassNodesUnmark(Fra_Lcr_t *p)
Definition: fraLcr.c:498
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
Fra_Lcr_t_::pInToOutPart
int * pInToOutPart
Definition: fraLcr.c:39
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Fra_ClassesRefine
int Fra_ClassesRefine(Fra_Cla_t *p)
Definition: fraClass.c:493
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Fra_ClassesCopyReprs
void Fra_ClassesCopyReprs(Fra_Cla_t *p, Vec_Ptr_t *vFailed)
Definition: fraClass.c:114
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition: aigUtil.c:148
Fra_Man_t_
Definition: fra.h:186
Fra_Lcr_t_::timeUpdate
abctime timeUpdate
Definition: fraLcr.c:61
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Fra_Lcr_t_::pInToOutNum
int * pInToOutNum
Definition: fraLcr.c:40
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Fra_Lcr_t_
Definition: fraLcr.c:31
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
Lcr_ManPrint
void Lcr_ManPrint(Fra_Lcr_t *p)
Definition: fraLcr.c:105
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Lcr_ManAlloc
Fra_Lcr_t * Lcr_ManAlloc(Aig_Man_t *pAig)
FUNCTION DEFINITIONS ///.
Definition: fraLcr.c:80
Fra_FraigLatchCorrespondence
Aig_Man_t * Fra_FraigLatchCorrespondence(Aig_Man_t *pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int *pnIter, float TimeLimit)
Definition: fraLcr.c:531
Fra_Lcr_t_::timePart
abctime timePart
Definition: fraLcr.c:58
Fra_Lcr_t_::nRegsBeg
int nRegsBeg
Definition: fraLcr.c:54
Fra_LcrCreatePart_rec
Aig_Obj_t * Fra_LcrCreatePart_rec(Fra_Cla_t *pCla, Aig_Man_t *pNew, Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: fraLcr.c:394
Fra_Lcr_t_::timeSim
abctime timeSim
Definition: fraLcr.c:57
Fra_Lcr_t_::timeTotal
abctime timeTotal
Definition: fraLcr.c:62
Fra_SmlStop
void Fra_SmlStop(Fra_Sml_t *p)
Definition: fraSim.c:839
Fra_LcrRemapPartitions
void Fra_LcrRemapPartitions(Vec_Ptr_t *vParts, Fra_Cla_t *pCla, int *pInToOutPart, int *pInToOutNum)
Definition: fraLcr.c:347
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223