abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaSweep.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [giaSweep.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis [Sweeping of GIA manager.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: giaSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 #include "giaAig.h"
23 #include "proof/dch/dch.h"
24 #include "misc/tim/tim.h"
25 #include "proof/cec/cec.h"
26 
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 /**Function*************************************************************
38 
39  Synopsis [Mark GIA nodes that feed into POs.]
40 
41  Description [Returns the array of classes of remaining registers.]
42 
43  SideEffects []
44 
45  SeeAlso []
46 
47 ***********************************************************************/
49 {
50  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
51  int i, iBox, nBoxIns, nBoxOuts, iShift, nRealCis;
52  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
53  return;
54  Gia_ObjSetTravIdCurrent(p, pObj);
55  if ( Gia_ObjIsAnd(pObj) )
56  {
59  return;
60  }
61  assert( Gia_ObjIsCi(pObj) );
62  nRealCis = Tim_ManPiNum(pManTime);
63  if ( Gia_ObjCioId(pObj) < nRealCis )
64  {
65  int nRegs = Gia_ManRegBoxNum(p);
66  int iFlop = Gia_ObjCioId(pObj) - (nRealCis - nRegs);
67  assert( iFlop >= 0 && iFlop < nRegs );
68  pObj = Gia_ManCo( p, Gia_ManPoNum(p) - nRegs + iFlop );
69  Vec_IntPush( vRoots, Gia_ObjId(p, pObj) );
70  return;
71  }
72  // get the box
73  iBox = Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) );
74  nBoxIns = Tim_ManBoxInputNum(pManTime, iBox);
75  nBoxOuts = Tim_ManBoxOutputNum(pManTime, iBox);
76  // mark all outputs
77  iShift = Tim_ManBoxOutputFirst(pManTime, iBox);
78  for ( i = 0; i < nBoxOuts; i++ )
79  Gia_ObjSetTravIdCurrent(p, Gia_ManCi(p, iShift + i));
80  // traverse from inputs
81  iShift = Tim_ManBoxInputFirst(pManTime, iBox);
82  for ( i = 0; i < nBoxIns; i++ )
83  Gia_ObjSetTravIdCurrent(p, Gia_ManCo(p, iShift + i));
84  for ( i = 0; i < nBoxIns; i++ )
85  Gia_ManMarkSeqGiaWithBoxes_rec( p, Gia_ObjFanin0(Gia_ManCo(p, iShift + i)), vRoots );
86 }
88 {
89  // CI order: real PIs + flop outputs + box outputs
90  // CO order: box inputs + real POs + flop inputs
91  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
92  Vec_Int_t * vRoots;
93  Gia_Obj_t * pObj;
94  int nRealCis = Tim_ManPiNum(pManTime);
95  int nRealCos = Tim_ManPoNum(pManTime);
96  int i, nRegs = fSeq ? Gia_ManRegBoxNum(p) : 0;
97  assert( Gia_ManRegNum(p) == 0 );
98  assert( Gia_ManBoxNum(p) > 0 );
99  // mark the terminals
102  for ( i = 0; i < nRealCis - nRegs; i++ )
104  // collect flops reachable from the POs
105  vRoots = Vec_IntAlloc( Gia_ManRegBoxNum(p) );
106  for ( i = Gia_ManPoNum(p) - nRealCos; i < Gia_ManPoNum(p) - nRegs; i++ )
107  {
110  }
111  // collect flops reachable from roots
112  if ( fSeq )
113  {
114  Gia_ManForEachObjVec( vRoots, p, pObj, i )
115  {
116  assert( Gia_ObjIsCo(pObj) );
117  Gia_ObjSetTravIdCurrent( p, pObj );
118  Gia_ManMarkSeqGiaWithBoxes_rec( p, Gia_ObjFanin0(pObj), vRoots );
119  }
120  //printf( "Explored %d flops\n", Vec_IntSize(vRoots) );
121  }
122  Vec_IntFree( vRoots );
123 }
125 {
126  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
127  Gia_Man_t * pNew;
128  Gia_Obj_t * pObj;
129  Vec_Int_t * vBoxesLeft;
130  int curCi, curCo, nBoxIns, nBoxOuts;
131  int i, k, iShift, nMarked;
132  assert( Gia_ManBoxNum(p) > 0 );
133  // mark useful boxes
134  Gia_ManMarkSeqGiaWithBoxes( p, fSeq );
135  // duplicate marked entries
136  pNew = Gia_ManStart( Gia_ManObjNum(p) );
137  pNew->pName = Abc_UtilStrsav( p->pName );
138  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
139  Gia_ManConst0(p)->Value = 0;
140  Gia_ManForEachObj1( p, pObj, i )
141  {
142  if ( !Gia_ObjIsTravIdCurrent(p, pObj) )
143  continue;
144  if ( Gia_ObjIsCi(pObj) )
145  pObj->Value = Gia_ManAppendCi(pNew);
146  else if ( Gia_ObjIsAnd(pObj) )
147  pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
148  else if ( Gia_ObjIsCo(pObj) )
149  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
150  else assert( 0 );
151  }
152  assert( !Gia_ManHasDangling(pNew) );
153  // collect remaining flops
154  if ( fSeq )
155  {
156  pNew->vRegClasses = Vec_IntAlloc( Gia_ManRegBoxNum(p) );
157  iShift = Gia_ManPoNum(p) - Gia_ManRegBoxNum(p);
158  for ( i = 0; i < Gia_ManRegBoxNum(p); i++ )
159  if ( Gia_ObjIsTravIdCurrent(p, Gia_ManCo(p, iShift + i)) )
160  Vec_IntPush( pNew->vRegClasses, Vec_IntEntry(p->vRegClasses, i) );
161  }
162  else if ( p->vRegClasses )
163  pNew->vRegClasses = Vec_IntDup( p->vRegClasses );
164  // collect remaining boxes
165  vBoxesLeft = Vec_IntAlloc( Gia_ManBoxNum(p) );
166  curCi = Tim_ManPiNum(pManTime);
167  curCo = 0;
168  for ( i = 0; i < Gia_ManBoxNum(p); i++ )
169  {
170  nBoxIns = Tim_ManBoxInputNum(pManTime, i);
171  nBoxOuts = Tim_ManBoxOutputNum(pManTime, i);
172  nMarked = 0;
173  for ( k = 0; k < nBoxIns; k++ )
174  nMarked += Gia_ObjIsTravIdCurrent( p, Gia_ManCo(p, curCo + k) );
175  for ( k = 0; k < nBoxOuts; k++ )
176  nMarked += Gia_ObjIsTravIdCurrent( p, Gia_ManCi(p, curCi + k) );
177  curCo += nBoxIns;
178  curCi += nBoxOuts;
179  // check presence
180  assert( nMarked == 0 || nMarked == nBoxIns + nBoxOuts );
181  if ( nMarked )
182  Vec_IntPush( vBoxesLeft, i );
183  }
184  curCo += Tim_ManPoNum(pManTime);
185  assert( curCi == Gia_ManCiNum(p) );
186  assert( curCo == Gia_ManCoNum(p) );
187  // update timing manager
188  pNew->pManTime = Gia_ManUpdateTimMan2( p, vBoxesLeft, Gia_ManRegBoxNum(p) - Gia_ManRegBoxNum(pNew) );
189  // update extra STG
190  assert( p->pAigExtra != NULL );
191  assert( pNew->pAigExtra == NULL );
192  pNew->pAigExtra = Gia_ManUpdateExtraAig2( p->pManTime, p->pAigExtra, vBoxesLeft );
193  assert( Gia_ManCiNum(pNew) == Tim_ManPiNum(pNew->pManTime) + Gia_ManCoNum(pNew->pAigExtra) );
194  Vec_IntFree( vBoxesLeft );
195  return pNew;
196 }
197 
198 /**Function*************************************************************
199 
200  Synopsis [Mark GIA nodes that feed into POs.]
201 
202  Description []
203 
204  SideEffects []
205 
206  SeeAlso []
207 
208 ***********************************************************************/
210 {
211  for ( assert( Gia_ObjIsCi(pObj) ); Gia_ObjIsCi(pObj); pObj-- )
212  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
213  return 1;
214  return 0;
215 }
217 {
218  for ( assert( Gia_ObjIsCi(pObj) ); Gia_ObjIsCi(pObj); pObj-- )
219  if ( fMark )
220  Gia_ObjSetTravIdCurrent( p, pObj );
221  return pObj;
222 }
224 {
225  for ( assert( Gia_ObjIsCo(pObj) ); Gia_ObjIsCo(pObj); pObj-- )
226  if ( fMark )
227  {
228  Gia_ObjSetTravIdCurrent( p, pObj );
230  }
231  return pObj;
232 }
234 {
235  for ( assert( Gia_ObjIsAnd(pObj) ); Gia_ObjIsAnd(pObj); pObj-- )
236  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
237  {
240  }
241  return pObj;
242 }
244 {
245  Vec_Int_t * vBoxPres;
246  Gia_Man_t * pNew;
247  Gia_Obj_t * pObj;
248  int i, fLabelPos;
249  assert( p->pManTime != NULL );
250  // start marks
253  vBoxPres = Vec_IntAlloc( 1000 );
254  // mark primary outputs
255  fLabelPos = 1;
256  pObj = Gia_ManObj( p, Gia_ManObjNum(p) - 1 );
257  assert( Gia_ObjIsCo(pObj) );
258  while ( Gia_ObjIsCo(pObj) )
259  {
260  pObj = Gia_ManFraigMarkCos( p, pObj, fLabelPos );
261  if ( Gia_ObjIsAnd(pObj) )
262  pObj = Gia_ManFraigMarkAnd( p, pObj );
263  assert( Gia_ObjIsCi(pObj) );
264  fLabelPos = Gia_ManFraigCheckCis(p, pObj);
265  pObj = Gia_ManFraigMarkCis( p, pObj, fLabelPos );
266  Vec_IntPush( vBoxPres, fLabelPos );
267  }
268  Vec_IntPop( vBoxPres );
269  Vec_IntReverseOrder( vBoxPres );
270  assert( Gia_ObjIsConst0(pObj) );
271  // mark primary inputs
272  Gia_ManForEachObj1( p, pObj, i )
273  if ( Gia_ObjIsCi(pObj) )
274  Gia_ObjSetTravIdCurrent( p, pObj );
275  else
276  break;
277  // duplicate marked entries
278  pNew = Gia_ManStart( Gia_ManObjNum(p) );
279  pNew->pName = Abc_UtilStrsav( p->pName );
280  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
281  Gia_ManConst0(p)->Value = 0;
282  Gia_ManForEachObj1( p, pObj, i )
283  {
284  if ( !Gia_ObjIsTravIdCurrent(p, pObj) )
285  continue;
286  if ( Gia_ObjIsCi(pObj) )
287  pObj->Value = Gia_ManAppendCi(pNew);
288  else if ( Gia_ObjIsAnd(pObj) )
289  pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
290  else if ( Gia_ObjIsCo(pObj) )
291  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
292  else assert( 0 );
293  }
294  // update timing manager
295  pNew->pManTime = Gia_ManUpdateTimMan( p, vBoxPres );
296  // update extra STG
297  assert( p->pAigExtra != NULL );
298  assert( pNew->pAigExtra == NULL );
299  pNew->pAigExtra = Gia_ManUpdateExtraAig( p->pManTime, p->pAigExtra, vBoxPres );
300  Vec_IntFree( vBoxPres );
301 // assert( Gia_ManPiNum(pNew) == Tim_ManCiNum(pNew->pManTime) );
302 // assert( Gia_ManPoNum(pNew) == Tim_ManCoNum(pNew->pManTime) );
303 // assert( Gia_ManPiNum(pNew) == Tim_ManPiNum(pNew->pManTime) + Gia_ManPoNum(pNew->pAigExtra) );
304  return pNew;
305 }
306 
307 /**Function*************************************************************
308 
309  Synopsis [Duplicates the AIG in the DFS order.]
310 
311  Description []
312 
313  SideEffects []
314 
315  SeeAlso []
316 
317 ***********************************************************************/
318 int Gia_ObjFanin0CopyRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int * pReprs )
319 {
320  int fanId = Gia_ObjFaninId0p( p, pObj );
321  if ( pReprs[fanId] == -1 )
322  return Gia_ObjFanin0Copy( pObj );
323  assert( Abc_Lit2Var(pReprs[fanId]) < Gia_ObjId(p, pObj) );
324  return Abc_LitNotCond( Gia_ObjValue(Gia_ManObj(p, Abc_Lit2Var(pReprs[fanId]))), Gia_ObjFaninC0(pObj) ^ Abc_LitIsCompl(pReprs[fanId]) );
325 }
326 int Gia_ObjFanin1CopyRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int * pReprs )
327 {
328  int fanId = Gia_ObjFaninId1p( p, pObj );
329  if ( pReprs[fanId] == -1 )
330  return Gia_ObjFanin1Copy( pObj );
331  assert( Abc_Lit2Var(pReprs[fanId]) < Gia_ObjId(p, pObj) );
332  return Abc_LitNotCond( Gia_ObjValue(Gia_ManObj(p, Abc_Lit2Var(pReprs[fanId]))), Gia_ObjFaninC1(pObj) ^ Abc_LitIsCompl(pReprs[fanId]) );
333 }
335 {
336  Gia_Man_t * pNew;
337  Gia_Obj_t * pObj;
338  int i;
339  assert( pReprs != NULL );
340  assert( Gia_ManRegNum(p) == 0 );
341  pNew = Gia_ManStart( Gia_ManObjNum(p) );
342  pNew->pName = Abc_UtilStrsav( p->pName );
343  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
344  Gia_ManFillValue( p );
345  Gia_ManHashAlloc( pNew );
346  Gia_ManForEachObj( p, pObj, i )
347  {
348  if ( Gia_ObjIsAnd(pObj) )
349  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyRepr(p, pObj, pReprs), Gia_ObjFanin1CopyRepr(p, pObj, pReprs) );
350  else if ( Gia_ObjIsCi(pObj) )
351  pObj->Value = Gia_ManAppendCi( pNew );
352  else if ( Gia_ObjIsCo(pObj) )
353  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0CopyRepr(p, pObj, pReprs) );
354  else if ( Gia_ObjIsConst0(pObj) )
355  pObj->Value = 0;
356  else assert( 0 );
357  }
358  Gia_ManHashStop( pNew );
359  return pNew;
360 }
361 
362 /**Function*************************************************************
363 
364  Synopsis [Compute the set of CIs representing carry-outs of boxes.]
365 
366  Description []
367 
368  SideEffects []
369 
370  SeeAlso []
371 
372 ***********************************************************************/
374 {
375  Gia_Obj_t * pObj;
376  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
377  int i, iLast, iBox, nBoxes = Tim_ManBoxNum( pManTime );
378  Vec_Int_t * vCarryOuts = Vec_IntAlloc( nBoxes );
379  for ( i = 0; i < nBoxes; i++ )
380  {
381  iLast = Tim_ManBoxInputLast( pManTime, i );
382  pObj = Gia_ObjFanin0( Gia_ManCo(p, iLast) );
383  if ( !Gia_ObjIsCi(pObj) )
384  continue;
385  iBox = Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) );
386  if ( iBox == -1 )
387  continue;
388  assert( Gia_ObjIsCi(pObj) );
389  if ( Gia_ObjCioId(pObj) == Tim_ManBoxOutputLast(pManTime, iBox) )
390  Vec_IntPush( vCarryOuts, Gia_ObjId(p, pObj) );
391  }
392  return vCarryOuts;
393 }
394 
395 /**Function*************************************************************
396 
397  Synopsis [Checks integriting of complex flops and carry-chains.]
398 
399  Description []
400 
401  SideEffects []
402 
403  SeeAlso []
404 
405 ***********************************************************************/
407 {
408  Gia_Obj_t * pObj;
409  Vec_Int_t * vCarryOuts;
410  int i, nCountReg = 0, nCountCarry = 0;
411  if ( p->pManTime == NULL )
412  return;
413  Gia_ManCreateRefs( p );
414  for ( i = Gia_ManPoNum(p) - Gia_ManRegBoxNum(p); i < Gia_ManPoNum(p); i++ )
415  {
416  pObj = Gia_ObjFanin0( Gia_ManPo(p, i) );
417  assert( Gia_ObjIsCi(pObj) );
418  if ( Gia_ObjRefNum(p, pObj) > 1 )
419  nCountReg++;
420  }
421  vCarryOuts = Gia_ManComputeCarryOuts( p );
422  Gia_ManForEachObjVec( vCarryOuts, p, pObj, i )
423  if ( Gia_ObjRefNum(p, pObj) > 1 )
424  nCountCarry++;
425  Vec_IntFree( vCarryOuts );
426  if ( nCountReg || nCountCarry )
427  printf( "Warning: AIG with boxes has internal fanout in %d complex flops and %d carries.\n", nCountReg, nCountCarry );
428  ABC_FREE( p->pRefs );
429 }
430 
431 /**Function*************************************************************
432 
433  Synopsis [Computes representatives in terms of the original objects.]
434 
435  Description []
436 
437  SideEffects []
438 
439  SeeAlso []
440 
441 ***********************************************************************/
442 int * Gia_ManFraigSelectReprs( Gia_Man_t * p, Gia_Man_t * pClp, int fVerbose )
443 {
444  Gia_Obj_t * pObj;
445  Vec_Int_t * vCarryOuts;
446  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
447  int * pReprs = ABC_FALLOC( int, Gia_ManObjNum(p) );
448  int * pClp2Gia = ABC_FALLOC( int, Gia_ManObjNum(pClp) );
449  int i, iLitClp, iLitClp2, iReprClp, fCompl;
450  int nConsts = 0, nReprs = 0;
451  assert( pManTime != NULL );
452  // count the number of equivalent objects
453  Gia_ManForEachObj1( pClp, pObj, i )
454  {
455  if ( Gia_ObjIsCo(pObj) )
456  continue;
457  if ( i == Gia_ObjReprSelf(pClp, i) )
458  continue;
459  if ( Gia_ObjReprSelf(pClp, i) == 0 )
460  nConsts++;
461  else
462  nReprs++;
463  }
464  if ( fVerbose )
465  printf( "Computed %d const objects and %d other objects.\n", nConsts, nReprs );
466  nConsts = nReprs = 0;
467 
468  // mark flop input boxes
469  Gia_ManCleanMark0( p );
470  for ( i = Gia_ManPoNum(p) - Gia_ManRegBoxNum(p); i < Gia_ManPoNum(p); i++ )
471  {
472  pObj = Gia_ObjFanin0( Gia_ManPo(p, i) );
473  assert( Gia_ObjIsCi(pObj) );
474  pObj->fMark0 = 1;
475  }
476  // mark connects between last box inputs and first box outputs
477  vCarryOuts = Gia_ManComputeCarryOuts( p );
478  Gia_ManForEachObjVec( vCarryOuts, p, pObj, i )
479  pObj->fMark0 = 1;
480  if ( fVerbose )
481  printf( "Fixed %d flop inputs and %d box/box connections (out of %d non-flop boxes).\n",
482  Gia_ManRegBoxNum(p), Vec_IntSize(vCarryOuts), Gia_ManNonRegBoxNum(p) );
483  Vec_IntFree( vCarryOuts );
484 
485  // compute representatives
486  pClp2Gia[0] = 0;
487  Gia_ManSetPhase( pClp );
488  Gia_ManForEachObj1( p, pObj, i )
489  {
490  if ( Gia_ObjIsCo(pObj) )
491  continue;
492  if ( Gia_ObjIsCi(pObj) && pObj->fMark0 ) // skip CI pointed by CO
493  continue;
494  assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
495  iLitClp = Gia_ObjValue(pObj);
496  if ( iLitClp == -1 )
497  continue;
498  iReprClp = Gia_ObjReprSelf( pClp, Abc_Lit2Var(iLitClp) );
499  if ( pClp2Gia[iReprClp] == -1 )
500  pClp2Gia[iReprClp] = i;
501  else
502  {
503  iLitClp2 = Gia_ObjValue( Gia_ManObj(p, pClp2Gia[iReprClp]) );
504  assert( Gia_ObjReprSelf(pClp, Abc_Lit2Var(iLitClp)) == Gia_ObjReprSelf(pClp, Abc_Lit2Var(iLitClp2)) );
505  fCompl = Abc_LitIsCompl(iLitClp) ^ Abc_LitIsCompl(iLitClp2);
506  fCompl ^= Gia_ManObj(pClp, Abc_Lit2Var(iLitClp))->fPhase;
507  fCompl ^= Gia_ManObj(pClp, Abc_Lit2Var(iLitClp2))->fPhase;
508  pReprs[i] = Abc_Var2Lit( pClp2Gia[iReprClp], fCompl );
509  assert( Abc_Lit2Var(pReprs[i]) < i );
510  if ( pClp2Gia[iReprClp] == 0 )
511  nConsts++;
512  else
513  nReprs++;
514  }
515  }
516  ABC_FREE( pClp2Gia );
517  Gia_ManForEachCi( p, pObj, i )
518  pObj->fMark0 = 0;
519  if ( fVerbose )
520  printf( "Found %d const objects and %d other objects.\n", nConsts, nReprs );
521  return pReprs;
522 }
523 
524 /**Function*************************************************************
525 
526  Synopsis []
527 
528  Description []
529 
530  SideEffects []
531 
532  SeeAlso []
533 
534 ***********************************************************************/
535 void Gia_ManFraigSweepPerform( Gia_Man_t * p, void * pPars )
536 {
537  Aig_Man_t * pNew;
538  pNew = Gia_ManToAigSimple( p );
539  assert( Gia_ManObjNum(p) == Aig_ManObjNum(pNew) );
540  Dch_ComputeEquivalences( pNew, (Dch_Pars_t *)pPars );
541  Gia_ManReprFromAigRepr( pNew, p );
542  Aig_ManStop( pNew );
543 }
544 
545 /**Function*************************************************************
546 
547  Synopsis []
548 
549  Description []
550 
551  SideEffects []
552 
553  SeeAlso []
554 
555 ***********************************************************************/
557 {
558  Gia_Man_t * pNew;
559  assert( p->pManTime == NULL || Gia_ManBoxNum(p) == 0 );
560  Gia_ManFraigSweepPerform( p, pPars );
561  pNew = Gia_ManEquivReduce( p, 1, 0, 0, 0 );
562  if ( pNew == NULL )
563  pNew = Gia_ManDup(p);
564  Gia_ManTransferTiming( pNew, p );
565  return pNew;
566 }
567 
568 /**Function*************************************************************
569 
570  Synopsis [Computes equivalences for one clock domain.]
571 
572  Description []
573 
574  SideEffects []
575 
576  SeeAlso []
577 
578 ***********************************************************************/
579 void Gia_ManSweepComputeOneDomainEquivs( Gia_Man_t * p, Vec_Int_t * vRegClasses, int iDom, void * pParsS, int fConst, int fEquiv, int fVerbose )
580 {
581  Gia_Man_t * pNew;
582  Gia_Obj_t * pObj;
583  Vec_Int_t * vPerm;
584  int i, Class, nFlops;
585  int nDoms = Vec_IntFindMax(vRegClasses);
586  assert( iDom >= 1 && iDom <= nDoms );
587  assert( p->pManTime == NULL );
588  assert( Gia_ManRegNum(p) > 0 );
589  // create required flop permutation
590  vPerm = Vec_IntAlloc( Gia_ManRegNum(p) );
591  Vec_IntForEachEntry( vRegClasses, Class, i )
592  if ( Class != iDom )
593  Vec_IntPush( vPerm, i );
594  nFlops = Vec_IntSize( vPerm );
595  Vec_IntForEachEntry( vRegClasses, Class, i )
596  if ( Class == iDom )
597  Vec_IntPush( vPerm, i );
598  nFlops = Vec_IntSize(vPerm) - nFlops;
599  assert( Vec_IntSize(vPerm) == Gia_ManRegNum(p) );
600  // derive new AIG
601  pNew = Gia_ManDupPermFlop( p, vPerm );
602  assert( Gia_ManObjNum(pNew) == Gia_ManObjNum(p) );
603  Vec_IntFree( vPerm );
604  // perform computation of equivalences
605  pNew->nRegs = nFlops;
606  if ( pParsS )
607  Cec_ManLSCorrespondenceClasses( pNew, (Cec_ParCor_t *)pParsS );
608  else
609  Gia_ManSeqCleanupClasses( pNew, fConst, fEquiv, fVerbose );
610  pNew->nRegs = Gia_ManRegNum(p);
611  // make new point to old
612  Gia_ManForEachObj( p, pObj, i )
613  {
614  assert( !Abc_LitIsCompl(pObj->Value) );
615  Gia_ManObj(pNew, Abc_Lit2Var(pObj->Value))->Value = Abc_Var2Lit(i, 0);
616  }
617  // transfer
618  Gia_ManDupRemapEquiv( p, pNew );
619  Gia_ManStop( pNew );
620 }
621 Gia_Man_t * Gia_ManSweepWithBoxesAndDomains( Gia_Man_t * p, void * pParsS, int fConst, int fEquiv, int fVerbose )
622 {
623  Gia_Man_t * pClp, * pNew, * pTemp;
624  int nDoms = Vec_IntFindMax(p->vRegClasses);
625  int * pReprs, iDom;
626  assert( Gia_ManRegNum(p) == 0 );
627  assert( p->pAigExtra != NULL );
628  assert( nDoms > 1 );
629  // order AIG objects
630  pNew = Gia_ManDupUnnormalize( p );
631  if ( pNew == NULL )
632  return NULL;
633  Gia_ManTransferTiming( pNew, p );
634  // iterate over domains
635  for ( iDom = 1; iDom <= nDoms; iDom++ )
636  {
637  int nFlops = Vec_IntCountEntry(pNew->vRegClasses, iDom);
638  if ( nFlops < 2 )
639  continue;
640  // find global equivalences
641  pClp = Gia_ManDupCollapse( pNew, pNew->pAigExtra, NULL, 1 );
642  // compute equivalences
643  Gia_ManSweepComputeOneDomainEquivs( pClp, pNew->vRegClasses, iDom, pParsS, fConst, fEquiv, fVerbose );
644  // transfer equivalences
645  pReprs = Gia_ManFraigSelectReprs( pNew, pClp, fVerbose );
646  Gia_ManStop( pClp );
647  // reduce AIG
648  Gia_ManTransferTiming( p, pNew );
649  pNew = Gia_ManFraigReduceGia( pTemp = pNew, pReprs );
650  Gia_ManTransferTiming( pNew, p );
651  Gia_ManStop( pTemp );
652  ABC_FREE( pReprs );
653  // derive new AIG
654  pNew = Gia_ManDupWithBoxes( pTemp = pNew, 1 );
655  Gia_ManStop( pTemp );
656  // report
657  if ( fVerbose )
658  {
659  printf( "Domain %2d : %5d -> %5d : ", iDom, nFlops, Vec_IntCountEntry(pNew->vRegClasses, iDom) );
660  Gia_ManPrintStats( pNew, NULL );
661  }
662  }
663  // normalize the result
664  pNew = Gia_ManDupNormalize( pTemp = pNew );
665  Gia_ManTransferTiming( pNew, pTemp );
666  Gia_ManStop( pTemp );
667  // check integrity
668  //Gia_ManCheckIntegrityWithBoxes( pNew );
669  return pNew;
670 }
671 
672 /**Function*************************************************************
673 
674  Synopsis [Reduces root model with scorr.]
675 
676  Description []
677 
678  SideEffects []
679 
680  SeeAlso []
681 
682 ***********************************************************************/
683 Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS, int fConst, int fEquiv, int fVerbose )
684 {
685  Gia_Man_t * pClp, * pNew, * pTemp;
686  int * pReprs;
687  assert( Gia_ManRegNum(p) == 0 );
688  assert( p->pAigExtra != NULL );
689  // consider seq synthesis with multiple clock domains
690  if ( pParsC == NULL && Gia_ManClockDomainNum(p) > 1 )
691  return Gia_ManSweepWithBoxesAndDomains( p, pParsS, fConst, fEquiv, fVerbose );
692  // order AIG objects
693  pNew = Gia_ManDupUnnormalize( p );
694  if ( pNew == NULL )
695  return NULL;
696  Gia_ManTransferTiming( pNew, p );
697  // find global equivalences
698  pClp = Gia_ManDupCollapse( pNew, pNew->pAigExtra, NULL, pParsC ? 0 : 1 );
699  // compute equivalences
700  if ( pParsC )
701  Gia_ManFraigSweepPerform( pClp, pParsC );
702  else if ( pParsS )
703  Cec_ManLSCorrespondenceClasses( pClp, (Cec_ParCor_t *)pParsS );
704  else
705  Gia_ManSeqCleanupClasses( pClp, fConst, fEquiv, fVerbose );
706  // transfer equivalences
707  pReprs = Gia_ManFraigSelectReprs( pNew, pClp, fVerbose );
708  Gia_ManStop( pClp );
709  // reduce AIG
710  Gia_ManTransferTiming( p, pNew );
711  pNew = Gia_ManFraigReduceGia( pTemp = pNew, pReprs );
712  Gia_ManTransferTiming( pNew, p );
713  Gia_ManStop( pTemp );
714  ABC_FREE( pReprs );
715  // derive new AIG
716  pNew = Gia_ManDupWithBoxes( pTemp = pNew, pParsC ? 0 : 1 );
717  Gia_ManStop( pTemp );
718  // normalize the result
719  pNew = Gia_ManDupNormalize( pTemp = pNew );
720  Gia_ManTransferTiming( pNew, pTemp );
721  Gia_ManStop( pTemp );
722  // check integrity
723  //Gia_ManCheckIntegrityWithBoxes( pNew );
724  return pNew;
725 }
726 
727 ////////////////////////////////////////////////////////////////////////
728 /// END OF FILE ///
729 ////////////////////////////////////////////////////////////////////////
730 
731 
733 
int Tim_ManBoxOutputFirst(Tim_Man_t *p, int iBox)
Definition: timBox.c:154
int Tim_ManBoxForCi(Tim_Man_t *p, int iCo)
Definition: timBox.c:86
static int Gia_ManAppendAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:592
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition: giaUtil.c:715
Gia_Man_t * Gia_ManDupUnnormalize(Gia_Man_t *p)
Definition: giaTim.c:373
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Gia_Man_t * Gia_ManUpdateExtraAig(void *pTime, Gia_Man_t *pAig, Vec_Int_t *vBoxPres)
Definition: giaTim.c:683
static Vec_Int_t * Vec_IntDup(Vec_Int_t *pVec)
Definition: vecInt.h:214
void Gia_ManReprFromAigRepr(Aig_Man_t *pAig, Gia_Man_t *pGia)
Definition: giaAig.c:487
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition: giaMan.c:389
Gia_Man_t * pAigExtra
Definition: gia.h:149
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Gia_Obj_t * Gia_ManCi(Gia_Man_t *p, int v)
Definition: gia.h:403
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
int Gia_ManRegBoxNum(Gia_Man_t *p)
Definition: giaTim.c:53
static int Vec_IntCountEntry(Vec_Int_t *p, int Entry)
Definition: vecInt.h:1156
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Vec_Int_t * vRegClasses
Definition: gia.h:144
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
static int Aig_ManObjNum(Aig_Man_t *p)
Definition: aig.h:258
Gia_Man_t * Gia_ManFraigSweepSimple(Gia_Man_t *p, void *pPars)
Definition: giaSweep.c:556
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
Gia_Man_t * Gia_ManDupPermFlop(Gia_Man_t *p, Vec_Int_t *vFfPerm)
Definition: giaDup.c:663
int Tim_ManBoxOutputLast(Tim_Man_t *p, int iBox)
Definition: timBox.c:170
void Gia_ManSweepComputeOneDomainEquivs(Gia_Man_t *p, Vec_Int_t *vRegClasses, int iDom, void *pParsS, int fConst, int fEquiv, int fVerbose)
Definition: giaSweep.c:579
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
static int Gia_ObjFaninId1p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:464
Gia_Obj_t * Gia_ManFraigMarkCis(Gia_Man_t *p, Gia_Obj_t *pObj, int fMark)
Definition: giaSweep.c:216
static int Gia_ObjRefNum(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:521
int Tim_ManBoxOutputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:202
Gia_Man_t * Gia_ManSweepWithBoxes(Gia_Man_t *p, void *pParsC, void *pParsS, int fConst, int fEquiv, int fVerbose)
Definition: giaSweep.c:683
typedefABC_NAMESPACE_HEADER_START struct Dch_Pars_t_ Dch_Pars_t
INCLUDES ///.
Definition: dch.h:43
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
static void Vec_IntReverseOrder(Vec_Int_t *p)
Definition: vecInt.h:1042
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
int * pRefs
Definition: gia.h:114
Definition: gia.h:75
int * Gia_ManFraigSelectReprs(Gia_Man_t *p, Gia_Man_t *pClp, int fVerbose)
Definition: giaSweep.c:442
int Gia_ManHasDangling(Gia_Man_t *p)
Definition: giaUtil.c:1155
int Tim_ManPiNum(Tim_Man_t *p)
Definition: timMan.c:688
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Gia_Man_t * Gia_ManEquivReduce(Gia_Man_t *p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose)
Definition: giaEquiv.c:417
Gia_Man_t * Gia_ManUpdateExtraAig2(void *pTime, Gia_Man_t *pAig, Vec_Int_t *vBoxesLeft)
Definition: giaTim.c:702
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
static Gia_Obj_t * Gia_ManPi(Gia_Man_t *p, int v)
Definition: gia.h:405
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
char * pName
Definition: gia.h:97
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
void Gia_ManMarkSeqGiaWithBoxes(Gia_Man_t *p, int fSeq)
Definition: giaSweep.c:87
int Gia_ManBoxNum(Gia_Man_t *p)
DECLARATIONS ///.
Definition: giaTim.c:49
void Gia_ManCheckIntegrityWithBoxes(Gia_Man_t *p)
Definition: giaSweep.c:406
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Gia_Man_t * Gia_ManDupNormalize(Gia_Man_t *p)
Definition: giaTim.c:134
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static int Gia_ObjReprSelf(Gia_Man_t *p, int Id)
Definition: gia.h:892
static int Vec_IntFindMax(Vec_Int_t *p)
Definition: vecInt.h:996
Gia_Obj_t * Gia_ManFraigMarkCos(Gia_Man_t *p, Gia_Obj_t *pObj, int fMark)
Definition: giaSweep.c:223
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
int Tim_ManBoxInputLast(Tim_Man_t *p, int iBox)
Definition: timBox.c:138
Gia_Man_t * Gia_ManFraigReduceGia(Gia_Man_t *p, int *pReprs)
Definition: giaSweep.c:334
if(last==0)
Definition: sparse_int.h:34
char * pSpec
Definition: gia.h:98
static int Vec_IntPop(Vec_Int_t *p)
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gia_Obj_t * Gia_ManFraigMarkAnd(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaSweep.c:233
void Gia_ManSeqCleanupClasses(Gia_Man_t *p, int fConst, int fEquiv, int fVerbose)
Definition: giaAig.c:603
Vec_Int_t * Gia_ManComputeCarryOuts(Gia_Man_t *p)
Definition: giaSweep.c:373
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
void * pManTime
Definition: gia.h:165
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
void Gia_ManFraigSweepPerform(Gia_Man_t *p, void *pPars)
Definition: giaSweep.c:535
int Tim_ManBoxNum(Tim_Man_t *p)
Definition: timMan.c:702
void Gia_ManTransferTiming(Gia_Man_t *p, Gia_Man_t *pGia)
Definition: giaIf.c:1912
int Cec_ManLSCorrespondenceClasses(Gia_Man_t *pAig, Cec_ParCor_t *pPars)
Definition: cecCorr.c:909
int Tim_ManBoxInputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:186
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
int Gia_ManNonRegBoxNum(Gia_Man_t *p)
Definition: giaTim.c:57
Gia_Man_t * Gia_ManDupCollapse(Gia_Man_t *p, Gia_Man_t *pBoxes, Vec_Int_t *vBoxPres, int fSeq)
Definition: giaTim.c:748
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
unsigned fPhase
Definition: gia.h:85
static Gia_Obj_t * Gia_ManCo(Gia_Man_t *p, int v)
Definition: gia.h:404
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
int nRegs
Definition: gia.h:99
unsigned fMark0
Definition: gia.h:79
void * Gia_ManUpdateTimMan2(Gia_Man_t *p, Vec_Int_t *vBoxesLeft, int nTermsDiff)
Definition: giaTim.c:664
#define ABC_FREE(obj)
Definition: abc_global.h:232
int Gia_ManFraigCheckCis(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaSweep.c:209
Definition: gia.h:95
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
ABC_NAMESPACE_IMPL_START void Gia_ManMarkSeqGiaWithBoxes_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vRoots)
DECLARATIONS ///.
Definition: giaSweep.c:48
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
Gia_Man_t * Gia_ManFraigCreateGia(Gia_Man_t *p)
Definition: giaSweep.c:243
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
int Gia_ObjFanin0CopyRepr(Gia_Man_t *p, Gia_Obj_t *pObj, int *pReprs)
Definition: giaSweep.c:318
#define assert(ex)
Definition: util_old.h:213
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
unsigned Value
Definition: gia.h:87
void Dch_ComputeEquivalences(Aig_Man_t *pAig, Dch_Pars_t *pPars)
Definition: dchCore.c:134
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
Gia_Man_t * Gia_ManSweepWithBoxesAndDomains(Gia_Man_t *p, void *pParsS, int fConst, int fEquiv, int fVerbose)
Definition: giaSweep.c:621
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
int Tim_ManBoxInputFirst(Tim_Man_t *p, int iBox)
Definition: timBox.c:122
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_Man_t * Gia_ManDupWithBoxes(Gia_Man_t *p, int fSeq)
Definition: giaSweep.c:124
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void * Gia_ManUpdateTimMan(Gia_Man_t *p, Vec_Int_t *vBoxPres)
Definition: giaTim.c:657
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
int Tim_ManPoNum(Tim_Man_t *p)
Definition: timMan.c:694
int Gia_ObjFanin1CopyRepr(Gia_Man_t *p, Gia_Obj_t *pObj, int *pReprs)
Definition: giaSweep.c:326
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
int Gia_ManClockDomainNum(Gia_Man_t *p)
Definition: giaTim.c:69
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
#define ABC_FALLOC(type, num)
Definition: abc_global.h:231
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
void Gia_ManDupRemapEquiv(Gia_Man_t *pNew, Gia_Man_t *p)
DECLARATIONS ///.
Definition: giaDup.c:46
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387