abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaTim.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [giaTim.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis [Procedures with hierarchy/timing 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: giaTim.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 "misc/tim/tim.h"
24 #include "proof/cec/cec.h"
25 #include "proof/fra/fra.h"
26 
27 ABC_NAMESPACE_IMPL_START
28 
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 ////////////////////////////////////////////////////////////////////////
35 /// FUNCTION DEFINITIONS ///
36 ////////////////////////////////////////////////////////////////////////
37 
38 /**Function*************************************************************
39 
40  Synopsis [Returns the number of boxes in the AIG with boxes.]
41 
42  Description []
43 
44  SideEffects []
45 
46  SeeAlso []
47 
48 ***********************************************************************/
49 int Gia_ManBoxNum( Gia_Man_t * p )
50 {
51  return p->pManTime ? Tim_ManBoxNum((Tim_Man_t *)p->pManTime) : 0;
52 }
53 int Gia_ManRegBoxNum( Gia_Man_t * p )
54 {
55  return p->vRegClasses ? Vec_IntSize(p->vRegClasses) : 0;
56 }
57 int Gia_ManNonRegBoxNum( Gia_Man_t * p )
58 {
59  return Gia_ManBoxNum(p) - Gia_ManRegBoxNum(p);
60 }
61 int Gia_ManBoxCiNum( Gia_Man_t * p )
62 {
63  return p->pManTime ? Gia_ManCiNum(p) - Tim_ManPiNum((Tim_Man_t *)p->pManTime) : 0;
64 }
65 int Gia_ManBoxCoNum( Gia_Man_t * p )
66 {
67  return p->pManTime ? Gia_ManCoNum(p) - Tim_ManPoNum((Tim_Man_t *)p->pManTime) : 0;
68 }
69 int Gia_ManClockDomainNum( Gia_Man_t * p )
70 {
71  int i, nDoms, Count = 0;
72  if ( p->vRegClasses == NULL )
73  return 0;
74  nDoms = Vec_IntFindMax(p->vRegClasses);
75  assert( Vec_IntCountEntry(p->vRegClasses, 0) == 0 );
76  for ( i = 1; i <= nDoms; i++ )
77  if ( Vec_IntCountEntry(p->vRegClasses, i) > 0 )
78  Count++;
79  return Count;
80 }
81 
82 /**Function*************************************************************
83 
84  Synopsis [Returns one if this is a seq AIG with non-trivial boxes.]
85 
86  Description []
87 
88  SideEffects []
89 
90  SeeAlso []
91 
92 ***********************************************************************/
93 int Gia_ManIsSeqWithBoxes( Gia_Man_t * p )
94 {
95  return (Gia_ManRegNum(p) > 0 && Gia_ManBoxNum(p) > 0);
96 }
97 
98 /**Function*************************************************************
99 
100  Synopsis [Makes sure the manager is normalized.]
101 
102  Description []
103 
104  SideEffects []
105 
106  SeeAlso []
107 
108 ***********************************************************************/
109 int Gia_ManIsNormalized( Gia_Man_t * p )
110 {
111  int i, nOffset;
112  nOffset = 1;
113  for ( i = 0; i < Gia_ManCiNum(p); i++ )
114  if ( !Gia_ObjIsCi( Gia_ManObj(p, nOffset+i) ) )
115  return 0;
116  nOffset = 1 + Gia_ManCiNum(p) + Gia_ManAndNum(p);
117  for ( i = 0; i < Gia_ManCoNum(p); i++ )
118  if ( !Gia_ObjIsCo( Gia_ManObj(p, nOffset+i) ) )
119  return 0;
120  return 1;
121 }
122 
123 /**Function*************************************************************
124 
125  Synopsis [Duplicates AIG in the DFS order while putting CIs first.]
126 
127  Description []
128 
129  SideEffects []
130 
131  SeeAlso []
132 
133 ***********************************************************************/
134 Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
135 {
136  Gia_Man_t * pNew;
137  Gia_Obj_t * pObj;
138  int i;
139  Gia_ManFillValue( p );
140  pNew = Gia_ManStart( Gia_ManObjNum(p) );
141  pNew->pName = Abc_UtilStrsav( p->pName );
142  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
143  Gia_ManConst0(p)->Value = 0;
144  if ( !Gia_ManIsSeqWithBoxes(p) )
145  {
146  Gia_ManForEachCi( p, pObj, i )
147  pObj->Value = Gia_ManAppendCi(pNew);
148  }
149  else
150  {
151  // current CI order: PIs + FOs + NewCIs
152  // desired reorder: PIs + NewCIs + FOs
153  int nCIs = Tim_ManPiNum( (Tim_Man_t *)p->pManTime );
154  int nAll = Tim_ManCiNum( (Tim_Man_t *)p->pManTime );
155  int nPis = nCIs - Gia_ManRegNum(p);
156  assert( nAll == Gia_ManCiNum(p) );
157  assert( nPis > 0 );
158  // copy PIs first
159  for ( i = 0; i < nPis; i++ )
160  Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
161  // copy new CIs second
162  for ( i = nCIs; i < nAll; i++ )
163  Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
164  // copy flops last
165  for ( i = nCIs - Gia_ManRegNum(p); i < nCIs; i++ )
166  Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
167  printf( "Warning: Shuffled CI order to be correct sequential AIG.\n" );
168  }
169  Gia_ManForEachAnd( p, pObj, i )
170  if ( Gia_ObjIsBuf(pObj) )
171  pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
172  else
173  pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
174  Gia_ManForEachCo( p, pObj, i )
175  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
176  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
177  pNew->nConstrs = p->nConstrs;
178  assert( Gia_ManIsNormalized(pNew) );
179  Gia_ManDupRemapEquiv( pNew, p );
180  return pNew;
181 }
182 
183 /**Function*************************************************************
184 
185  Synopsis [Reorders flops for sequential AIGs with boxes.]
186 
187  Description []
188 
189  SideEffects []
190 
191  SeeAlso []
192 
193 ***********************************************************************/
194 Gia_Man_t * Gia_ManDupUnshuffleInputs( Gia_Man_t * p )
195 {
196  Gia_Man_t * pNew;
197  Gia_Obj_t * pObj;
198  int i, nCIs, nAll, nPis;
199  // sanity checks
200  assert( Gia_ManIsNormalized(p) );
201  assert( Gia_ManIsSeqWithBoxes(p) );
202  Gia_ManFillValue( p );
203  pNew = Gia_ManStart( Gia_ManObjNum(p) );
204  pNew->pName = Abc_UtilStrsav( p->pName );
205  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
206  Gia_ManConst0(p)->Value = 0;
207  // change input order
208  // desired reorder: PIs + NewCIs + FOs
209  // current CI order: PIs + FOs + NewCIs
210  nCIs = Tim_ManPiNum( (Tim_Man_t *)p->pManTime );
211  nAll = Tim_ManCiNum( (Tim_Man_t *)p->pManTime );
212  nPis = nCIs - Gia_ManRegNum(p);
213  assert( nAll == Gia_ManCiNum(p) );
214  assert( nPis > 0 );
215  // copy PIs first
216  for ( i = 0; i < nPis; i++ )
217  Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
218  // copy flops second
219  for ( i = nAll - Gia_ManRegNum(p); i < nAll; i++ )
220  Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
221  // copy new CIs last
222  for ( i = nPis; i < nAll - Gia_ManRegNum(p); i++ )
223  Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
224  printf( "Warning: Unshuffled CI order to be correct AIG with boxes.\n" );
225  // other things
226  Gia_ManForEachAnd( p, pObj, i )
227  pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
228  Gia_ManForEachCo( p, pObj, i )
229  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
230  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
231  pNew->nConstrs = p->nConstrs;
232  assert( Gia_ManIsNormalized(pNew) );
233  Gia_ManDupRemapEquiv( pNew, p );
234  return pNew;
235 }
236 
237 
238 /**Function*************************************************************
239 
240  Synopsis [Find the ordering of AIG objects.]
241 
242  Description []
243 
244  SideEffects []
245 
246  SeeAlso []
247 
248 ***********************************************************************/
249 int Gia_ManOrderWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
250 {
251  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
252  return 0;
253  Gia_ObjSetTravIdCurrent(p, pObj);
254  if ( Gia_ObjIsCi(pObj) )
255  {
256  p->iData2 = Gia_ObjCioId(pObj);
257  return 1;
258  }
259  assert( Gia_ObjIsAnd(pObj) );
260  if ( Gia_ObjIsBuf(pObj) )
261  {
262  if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ) )
263  return 1;
264  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
265  return 0;
266  }
267  if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
268  if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)), vNodes ) )
269  return 1;
270  if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ) )
271  return 1;
272  if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin1(pObj), vNodes ) )
273  return 1;
274  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
275  return 0;
276 }
277 Vec_Int_t * Gia_ManOrderWithBoxes( Gia_Man_t * p )
278 {
279  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
280  Vec_Int_t * vNodes;
281  Gia_Obj_t * pObj;
282  int i, k, curCi, curCo;
283  assert( pManTime != NULL );
284  assert( Gia_ManIsNormalized( p ) );
285  // start trav IDs
286  Gia_ManIncrementTravId( p );
287  // start the array
288  vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
289  // include constant
290  Vec_IntPush( vNodes, 0 );
291  Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
292  // include primary inputs
293  for ( i = 0; i < Tim_ManPiNum(pManTime); i++ )
294  {
295  pObj = Gia_ManCi( p, i );
296  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
297  Gia_ObjSetTravIdCurrent( p, pObj );
298  assert( Gia_ObjId(p, pObj) == i+1 );
299  }
300  // for each box, include box nodes
301  curCi = Tim_ManPiNum(pManTime);
302  curCo = 0;
303  for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
304  {
305  // add internal nodes
306  for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
307  {
308  pObj = Gia_ManCo( p, curCo + k );
309  if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ) )
310  {
311  int iCiNum = p->iData2;
312  int iBoxNum = Tim_ManBoxFindFromCiNum( pManTime, iCiNum );
313  printf( "The command has to terminate. Boxes are not in a topological order.\n" );
314  printf( "The following information may help debugging (numbers are 0-based):\n" );
315  printf( "Input %d of BoxA %d (1stCI = %d; 1stCO = %d) has TFI with CI %d,\n",
316  k, i, Tim_ManBoxOutputFirst(pManTime, i), Tim_ManBoxInputFirst(pManTime, i), iCiNum );
317  printf( "which corresponds to output %d of BoxB %d (1stCI = %d; 1stCO = %d).\n",
318  iCiNum - Tim_ManBoxOutputFirst(pManTime, iBoxNum), iBoxNum,
319  Tim_ManBoxOutputFirst(pManTime, iBoxNum), Tim_ManBoxInputFirst(pManTime, iBoxNum) );
320  printf( "In a correct topological order, BoxB should precede BoxA.\n" );
321  Vec_IntFree( vNodes );
322  p->iData2 = 0;
323  return NULL;
324  }
325  }
326  // add POs corresponding to box inputs
327  for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
328  {
329  pObj = Gia_ManCo( p, curCo + k );
330  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
331  }
332  curCo += Tim_ManBoxInputNum(pManTime, i);
333  // add PIs corresponding to box outputs
334  for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
335  {
336  pObj = Gia_ManCi( p, curCi + k );
337  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
338  Gia_ObjSetTravIdCurrent( p, pObj );
339  }
340  curCi += Tim_ManBoxOutputNum(pManTime, i);
341  }
342  // add remaining nodes
343  for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
344  {
345  pObj = Gia_ManCo( p, i );
346  Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes );
347  }
348  // add POs
349  for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
350  {
351  pObj = Gia_ManCo( p, i );
352  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
353  }
354  curCo += Tim_ManPoNum(pManTime);
355  // verify counts
356  assert( curCi == Gia_ManCiNum(p) );
357  assert( curCo == Gia_ManCoNum(p) );
358  assert( Vec_IntSize(vNodes) == Gia_ManObjNum(p) );
359  return vNodes;
360 }
361 
362 /**Function*************************************************************
363 
364  Synopsis [Duplicates AIG according to the timing manager.]
365 
366  Description []
367 
368  SideEffects []
369 
370  SeeAlso []
371 
372 ***********************************************************************/
373 Gia_Man_t * Gia_ManDupUnnormalize( Gia_Man_t * p )
374 {
375  Vec_Int_t * vNodes;
376  Gia_Man_t * pNew;
377  Gia_Obj_t * pObj;
378  int i;
379  assert( !Gia_ManBufNum(p) );
380  vNodes = Gia_ManOrderWithBoxes( p );
381  if ( vNodes == NULL )
382  return NULL;
383  Gia_ManFillValue( p );
384  pNew = Gia_ManStart( Gia_ManObjNum(p) );
385  pNew->pName = Abc_UtilStrsav( p->pName );
386  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
387  if ( Gia_ManHasChoices(p) )
388  pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) );
389  Gia_ManForEachObjVec( vNodes, p, pObj, i )
390  {
391  if ( Gia_ObjIsBuf(pObj) )
392  pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
393  else if ( Gia_ObjIsAnd(pObj) )
394  {
395  pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
396  if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
397  pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))->Value);
398  }
399  else if ( Gia_ObjIsCi(pObj) )
400  pObj->Value = Gia_ManAppendCi( pNew );
401  else if ( Gia_ObjIsCo(pObj) )
402  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
403  else if ( Gia_ObjIsConst0(pObj) )
404  pObj->Value = 0;
405  else assert( 0 );
406  }
407  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
408  Vec_IntFree( vNodes );
409  return pNew;
410 }
411 
412 
413 /**Function*************************************************************
414 
415  Synopsis [Remaps the AIG from the old manager into the new manager.]
416 
417  Description []
418 
419  SideEffects []
420 
421  SeeAlso []
422 
423 ***********************************************************************/
424 void Gia_ManCleanupRemap( Gia_Man_t * p, Gia_Man_t * pGia )
425 {
426  Gia_Obj_t * pObj, * pObjGia;
427  int i, iPrev;
428  Gia_ManForEachObj1( p, pObj, i )
429  {
430  iPrev = Gia_ObjValue(pObj);
431  if ( iPrev == ~0 )
432  continue;
433  pObjGia = Gia_ManObj( pGia, Abc_Lit2Var(iPrev) );
434  if ( pObjGia->Value == ~0 )
435  Gia_ObjSetValue( pObj, pObjGia->Value );
436  else
437  Gia_ObjSetValue( pObj, Abc_LitNotCond(pObjGia->Value, Abc_LitIsCompl(iPrev)) );
438  }
439 }
440 
441 /**Function*************************************************************
442 
443  Synopsis [Computes level with boxes.]
444 
445  Description []
446 
447  SideEffects []
448 
449  SeeAlso []
450 
451 ***********************************************************************/
452 int Gia_ManLevelWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
453 {
454  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
455  return 0;
456  Gia_ObjSetTravIdCurrent(p, pObj);
457  if ( Gia_ObjIsCi(pObj) )
458  return 1;
459  assert( Gia_ObjIsAnd(pObj) );
460  if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
461  Gia_ManLevelWithBoxes_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)) );
462  if ( Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ) )
463  return 1;
464  if ( Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin1(pObj) ) )
465  return 1;
466  Gia_ObjSetAndLevel( p, pObj );
467  return 0;
468 }
469 int Gia_ManLevelWithBoxes( Gia_Man_t * p )
470 {
471  int nAnd2Delay = p->nAnd2Delay ? p->nAnd2Delay : 1;
472  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
473  Gia_Obj_t * pObj, * pObjIn;
474  int i, k, j, curCi, curCo, LevelMax;
475  assert( Gia_ManRegNum(p) == 0 );
476  assert( Gia_ManBufNum(p) == 0 );
477  // copy const and real PIs
478  Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
479  Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 );
480  Gia_ManIncrementTravId( p );
481  Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
482  for ( i = 0; i < Tim_ManPiNum(pManTime); i++ )
483  {
484  pObj = Gia_ManCi( p, i );
485  Gia_ObjSetLevel( p, pObj, Tim_ManGetCiArrival(pManTime, i) / nAnd2Delay );
486  Gia_ObjSetTravIdCurrent( p, pObj );
487  }
488  // create logic for each box
489  curCi = Tim_ManPiNum(pManTime);
490  curCo = 0;
491  for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
492  {
493  int nBoxInputs = Tim_ManBoxInputNum( pManTime, i );
494  int nBoxOutputs = Tim_ManBoxOutputNum( pManTime, i );
495  float * pDelayTable = Tim_ManBoxDelayTable( pManTime, i );
496  // compute level for TFI of box inputs
497  for ( k = 0; k < nBoxInputs; k++ )
498  {
499  pObj = Gia_ManCo( p, curCo + k );
500  if ( Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ) )
501  {
502  printf( "Boxes are not in a topological order. Switching to level computation without boxes.\n" );
503  return Gia_ManLevelNum( p );
504  }
505  // set box input level
506  Gia_ObjSetCoLevel( p, pObj );
507  }
508  // compute level for box outputs
509  for ( k = 0; k < nBoxOutputs; k++ )
510  {
511  pObj = Gia_ManCi( p, curCi + k );
512  Gia_ObjSetTravIdCurrent( p, pObj );
513  // evaluate delay of this output
514  LevelMax = 0;
515  assert( nBoxInputs == (int)pDelayTable[1] );
516  for ( j = 0; j < nBoxInputs && (pObjIn = Gia_ManCo(p, curCo + j)); j++ )
517  if ( (int)pDelayTable[3+k*nBoxInputs+j] != -ABC_INFINITY )
518  LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + ((int)pDelayTable[3+k*nBoxInputs+j] / nAnd2Delay) );
519  // set box output level
520  Gia_ObjSetLevel( p, pObj, LevelMax );
521  }
522  curCo += nBoxInputs;
523  curCi += nBoxOutputs;
524  }
525  // add remaining nodes
526  p->nLevels = 0;
527  for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
528  {
529  pObj = Gia_ManCo( p, i );
530  Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) );
531  Gia_ObjSetCoLevel( p, pObj );
532  p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
533  }
534  curCo += Tim_ManPoNum(pManTime);
535  // verify counts
536  assert( curCi == Gia_ManCiNum(p) );
537  assert( curCo == Gia_ManCoNum(p) );
538 // printf( "Max level is %d.\n", p->nLevels );
539  return p->nLevels;
540 }
541 
542 /**Function*************************************************************
543 
544  Synopsis [Computes level with boxes.]
545 
546  Description []
547 
548  SideEffects []
549 
550  SeeAlso []
551 
552 ***********************************************************************/
553 int Gia_ManLutLevelWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
554 {
555  int iObj, k, iFan, Level = 0;
556  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
557  return 0;
558  Gia_ObjSetTravIdCurrent(p, pObj);
559  if ( Gia_ObjIsCi(pObj) )
560  return 1;
561  assert( Gia_ObjIsAnd(pObj) );
562  iObj = Gia_ObjId( p, pObj );
563  Gia_LutForEachFanin( p, iObj, iFan, k )
564  {
565  if ( Gia_ManLutLevelWithBoxes_rec( p, Gia_ManObj(p, iFan) ) )
566  return 1;
567  Level = Abc_MaxInt( Level, Gia_ObjLevelId(p, iFan) );
568  }
569  Gia_ObjSetLevelId( p, iObj, Level + 1 );
570  return 0;
571 }
572 int Gia_ManLutLevelWithBoxes( Gia_Man_t * p )
573 {
574 // int nAnd2Delay = p->nAnd2Delay ? p->nAnd2Delay : 1;
575  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
576  Gia_Obj_t * pObj, * pObjIn;
577  int i, k, j, curCi, curCo, LevelMax;
578  assert( Gia_ManRegNum(p) == 0 );
579  // copy const and real PIs
580  Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
581  Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 );
582  Gia_ManIncrementTravId( p );
583  Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
584  for ( i = 0; i < Tim_ManPiNum(pManTime); i++ )
585  {
586  pObj = Gia_ManCi( p, i );
587 // Gia_ObjSetLevel( p, pObj, Tim_ManGetCiArrival(pManTime, i) / nAnd2Delay );
588  Gia_ObjSetLevel( p, pObj, 0 );
589  Gia_ObjSetTravIdCurrent( p, pObj );
590  }
591  // create logic for each box
592  curCi = Tim_ManPiNum(pManTime);
593  curCo = 0;
594  for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
595  {
596  int nBoxInputs = Tim_ManBoxInputNum( pManTime, i );
597  int nBoxOutputs = Tim_ManBoxOutputNum( pManTime, i );
598  float * pDelayTable = Tim_ManBoxDelayTable( pManTime, i );
599  // compute level for TFI of box inputs
600  for ( k = 0; k < nBoxInputs; k++ )
601  {
602  pObj = Gia_ManCo( p, curCo + k );
603  if ( Gia_ManLutLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ) )
604  {
605  printf( "Boxes are not in a topological order. Switching to level computation without boxes.\n" );
606  return Gia_ManLevelNum( p );
607  }
608  // set box input level
609  Gia_ObjSetCoLevel( p, pObj );
610  }
611  // compute level for box outputs
612  for ( k = 0; k < nBoxOutputs; k++ )
613  {
614  pObj = Gia_ManCi( p, curCi + k );
615  Gia_ObjSetTravIdCurrent( p, pObj );
616  // evaluate delay of this output
617  LevelMax = 0;
618  assert( nBoxInputs == (int)pDelayTable[1] );
619  for ( j = 0; j < nBoxInputs && (pObjIn = Gia_ManCo(p, curCo + j)); j++ )
620  if ( (int)pDelayTable[3+k*nBoxInputs+j] != -ABC_INFINITY )
621 // LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + ((int)pDelayTable[3+k*nBoxInputs+j] / nAnd2Delay) );
622  LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + 1 );
623  // set box output level
624  Gia_ObjSetLevel( p, pObj, LevelMax );
625  }
626  curCo += nBoxInputs;
627  curCi += nBoxOutputs;
628  }
629  // add remaining nodes
630  p->nLevels = 0;
631  for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
632  {
633  pObj = Gia_ManCo( p, i );
634  Gia_ManLutLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) );
635  Gia_ObjSetCoLevel( p, pObj );
636  p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
637  }
638  curCo += Tim_ManPoNum(pManTime);
639  // verify counts
640  assert( curCi == Gia_ManCiNum(p) );
641  assert( curCo == Gia_ManCoNum(p) );
642 // printf( "Max level is %d.\n", p->nLevels );
643  return p->nLevels;
644 }
645 
646 /**Function*************************************************************
647 
648  Synopsis [Update hierarchy/timing manager.]
649 
650  Description []
651 
652  SideEffects []
653 
654  SeeAlso []
655 
656 ***********************************************************************/
657 void * Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres )
658 {
659  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
660  assert( pManTime != NULL );
661  assert( Vec_IntSize(vBoxPres) == Tim_ManBoxNum(pManTime) );
662  return Tim_ManTrim( pManTime, vBoxPres );
663 }
664 void * Gia_ManUpdateTimMan2( Gia_Man_t * p, Vec_Int_t * vBoxesLeft, int nTermsDiff )
665 {
666  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
667  assert( pManTime != NULL );
668  assert( Vec_IntSize(vBoxesLeft) <= Tim_ManBoxNum(pManTime) );
669  return Tim_ManReduce( pManTime, vBoxesLeft, nTermsDiff );
670 }
671 
672 /**Function*************************************************************
673 
674  Synopsis [Update AIG of the holes.]
675 
676  Description []
677 
678  SideEffects []
679 
680  SeeAlso []
681 
682 ***********************************************************************/
683 Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * p, Vec_Int_t * vBoxPres )
684 {
685  Gia_Man_t * pNew;
686  Tim_Man_t * pManTime = (Tim_Man_t *)pTime;
687  Vec_Int_t * vOutPres = Vec_IntAlloc( 100 );
688  int i, k, curPo = 0;
689  assert( Vec_IntSize(vBoxPres) == Tim_ManBoxNum(pManTime) );
690  assert( Gia_ManCoNum(p) == Tim_ManCiNum(pManTime) - Tim_ManPiNum(pManTime) );
691  for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
692  {
693  for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
694  Vec_IntPush( vOutPres, Vec_IntEntry(vBoxPres, i) );
695  curPo += Tim_ManBoxOutputNum(pManTime, i);
696  }
697  assert( curPo == Gia_ManCoNum(p) );
698  pNew = Gia_ManDupOutputVec( p, vOutPres );
699  Vec_IntFree( vOutPres );
700  return pNew;
701 }
702 Gia_Man_t * Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * p, Vec_Int_t * vBoxesLeft )
703 {
704  Gia_Man_t * pNew;
705  Tim_Man_t * pManTime = (Tim_Man_t *)pTime;
706  int nRealPis = Tim_ManPiNum(pManTime);
707  Vec_Int_t * vOutsLeft = Vec_IntAlloc( 100 );
708  int i, k, iBox, iOutFirst;
709  assert( Vec_IntSize(vBoxesLeft) <= Tim_ManBoxNum(pManTime) );
710  assert( Gia_ManCoNum(p) == Tim_ManCiNum(pManTime) - nRealPis );
711  Vec_IntForEachEntry( vBoxesLeft, iBox, i )
712  {
713  iOutFirst = Tim_ManBoxOutputFirst(pManTime, iBox) - nRealPis;
714  for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, iBox); k++ )
715  Vec_IntPush( vOutsLeft, iOutFirst + k );
716  }
717  pNew = Gia_ManDupSelectedOutputs( p, vOutsLeft );
718  Vec_IntFree( vOutsLeft );
719  return pNew;
720 }
721 
722 /**Function*************************************************************
723 
724  Synopsis [Computes AIG with boxes.]
725 
726  Description []
727 
728  SideEffects []
729 
730  SeeAlso []
731 
732 ***********************************************************************/
733 void Gia_ManDupCollapse_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew )
734 {
735  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
736  return;
737  Gia_ObjSetTravIdCurrent(p, pObj);
738  assert( Gia_ObjIsAnd(pObj) );
739  if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
740  Gia_ManDupCollapse_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)), pNew );
741  Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
742  Gia_ManDupCollapse_rec( p, Gia_ObjFanin1(pObj), pNew );
743 // assert( !~pObj->Value );
744  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
745  if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
746  pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))->Value);
747 }
748 Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres, int fSeq )
749 {
750  // this procedure assumes that sequential AIG with boxes is unshuffled to have valid boxes
751  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
752  Gia_Man_t * pNew, * pTemp;
753  Gia_Obj_t * pObj, * pObjBox;
754  int i, k, curCi, curCo;
755  assert( !fSeq || p->vRegClasses );
756  //assert( Gia_ManRegNum(p) == 0 );
757  assert( Gia_ManCiNum(p) == Tim_ManPiNum(pManTime) + Gia_ManCoNum(pBoxes) );
758  pNew = Gia_ManStart( Gia_ManObjNum(p) );
759  pNew->pName = Abc_UtilStrsav( p->pName );
760  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
761  if ( Gia_ManHasChoices(p) )
762  pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) );
763  Gia_ManHashAlloc( pNew );
764  // copy const and real PIs
765  Gia_ManFillValue( p );
766  Gia_ManConst0(p)->Value = 0;
767  Gia_ManIncrementTravId( p );
768  Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
769  for ( i = 0; i < Tim_ManPiNum(pManTime); i++ )
770  {
771  pObj = Gia_ManCi( p, i );
772  pObj->Value = Gia_ManAppendCi(pNew);
773  Gia_ObjSetTravIdCurrent( p, pObj );
774  }
775  // create logic for each box
776  curCi = Tim_ManPiNum(pManTime);
777  curCo = 0;
778  for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
779  {
780  // clean boxes
781  Gia_ManIncrementTravId( pBoxes );
782  Gia_ObjSetTravIdCurrent( pBoxes, Gia_ManConst0(pBoxes) );
783  Gia_ManConst0(pBoxes)->Value = 0;
784  // add internal nodes
785  if ( Tim_ManBoxIsBlack(pManTime, i) )
786  {
787  int fSkip = (vBoxPres != NULL && !Vec_IntEntry(vBoxPres, i));
788  for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
789  {
790  pObj = Gia_ManCo( p, curCo + k );
791  Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
792  pObj->Value = fSkip ? -1 : Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
793  }
794  for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
795  {
796  pObj = Gia_ManCi( p, curCi + k );
797  pObj->Value = fSkip ? 0 : Gia_ManAppendCi(pNew);
798  Gia_ObjSetTravIdCurrent( p, pObj );
799  }
800  }
801  else
802  {
803  for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
804  {
805  // build logic
806  pObj = Gia_ManCo( p, curCo + k );
807  Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
808  // transfer to the PI
809  pObjBox = Gia_ManCi( pBoxes, k );
810  pObjBox->Value = Gia_ObjFanin0Copy(pObj);
811  Gia_ObjSetTravIdCurrent( pBoxes, pObjBox );
812  }
813  for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
814  {
815  // build logic
816  pObjBox = Gia_ManCo( pBoxes, curCi - Tim_ManPiNum(pManTime) + k );
817  Gia_ManDupCollapse_rec( pBoxes, Gia_ObjFanin0(pObjBox), pNew );
818  // transfer to the PI
819  pObj = Gia_ManCi( p, curCi + k );
820  pObj->Value = Gia_ObjFanin0Copy(pObjBox);
821  Gia_ObjSetTravIdCurrent( p, pObj );
822  }
823  }
824  curCo += Tim_ManBoxInputNum(pManTime, i);
825  curCi += Tim_ManBoxOutputNum(pManTime, i);
826  }
827  // add remaining nodes
828  for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
829  {
830  pObj = Gia_ManCo( p, i );
831  Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
832  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
833  }
834  curCo += Tim_ManPoNum(pManTime);
835  // verify counts
836  assert( curCi == Gia_ManCiNum(p) );
837  assert( curCo == Gia_ManCoNum(p) );
838  Gia_ManSetRegNum( pNew, (fSeq && p->vRegClasses) ? Vec_IntSize(p->vRegClasses) : Gia_ManRegNum(p) );
839  Gia_ManHashStop( pNew );
840  pNew = Gia_ManCleanup( pTemp = pNew );
841  Gia_ManCleanupRemap( p, pTemp );
842  Gia_ManStop( pTemp );
843  assert( Tim_ManPoNum(pManTime) == Gia_ManCoNum(pNew) );
844  assert( Tim_ManPiNum(pManTime) == Gia_ManCiNum(pNew) );
845  return pNew;
846 }
847 
848 /**Function*************************************************************
849 
850  Synopsis [Verify XAIG against its spec.]
851 
852  Description []
853 
854  SideEffects []
855 
856  SeeAlso []
857 
858 ***********************************************************************/
859 int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fVerbose, char * pFileSpec )
860 {
861  int Status = -1;
862  Gia_Man_t * pSpec, * pGia0, * pGia1, * pMiter;
863  Vec_Int_t * vBoxPres = NULL;
864  if ( pFileSpec == NULL && pGia->pSpec == NULL )
865  {
866  printf( "Spec file is not given. Use standard flow.\n" );
867  return Status;
868  }
869  if ( Gia_ManBoxNum(pGia) && pGia->pAigExtra == NULL )
870  {
871  printf( "Design has no box logic. Use standard flow.\n" );
872  return Status;
873  }
874  // read original AIG
875  pSpec = Gia_AigerRead( pFileSpec ? pFileSpec : pGia->pSpec, 0, 0 );
876  if ( Gia_ManBoxNum(pSpec) && pSpec->pAigExtra == NULL )
877  {
878  Gia_ManStop( pSpec );
879  printf( "Spec has no box logic. Use standard flow.\n" );
880  return Status;
881  }
882  // prepare miter
883  if ( pGia->pManTime == NULL && pSpec->pManTime == NULL )
884  {
885  pGia0 = Gia_ManDup( pSpec );
886  pGia1 = Gia_ManDup( pGia );
887  }
888  else
889  {
890  // if timing managers have different number of black boxes,
891  // it is possible that some of the boxes are swept away
892  if ( pSpec->pManTime && Tim_ManBlackBoxNum((Tim_Man_t *)pSpec->pManTime) > 0 && Gia_ManBoxNum(pGia) > 0 )
893  {
894  // specification cannot have fewer boxes than implementation
895  if ( Gia_ManBoxNum(pSpec) < Gia_ManBoxNum(pGia) )
896  {
897  printf( "Spec has less boxes than the design. Cannot proceed.\n" );
898  return Status;
899  }
900  // to align the boxes, find what boxes of pSpec are dropped in pGia
901  if ( Gia_ManBoxNum(pSpec) > Gia_ManBoxNum(pGia) )
902  {
903  vBoxPres = Tim_ManAlignTwo( (Tim_Man_t *)pSpec->pManTime, (Tim_Man_t *)pGia->pManTime );
904  if ( vBoxPres == NULL )
905  {
906  printf( "Boxes of spec and design cannot be aligned. Cannot proceed.\n" );
907  return Status;
908  }
909  }
910  }
911  // collapse two designs
912  if ( Gia_ManBoxNum(pSpec) > 0 )
913  pGia0 = Gia_ManDupCollapse( pSpec, pSpec->pAigExtra, vBoxPres, fSeq );
914  else
915  pGia0 = Gia_ManDup( pSpec );
916  if ( Gia_ManBoxNum(pGia) > 0 )
917  pGia1 = Gia_ManDupCollapse( pGia, pGia->pAigExtra, NULL, fSeq );
918  else
919  pGia1 = Gia_ManDup( pGia );
920  Vec_IntFreeP( &vBoxPres );
921  }
922  // compute the miter
923  if ( fSeq )
924  {
925  pMiter = Gia_ManMiter( pGia0, pGia1, 0, 0, 1, 0, fVerbose );
926  if ( pMiter )
927  {
928  Aig_Man_t * pMan;
929  Fra_Sec_t SecPar, * pSecPar = &SecPar;
930  Fra_SecSetDefaultParams( pSecPar );
931  pSecPar->fRetimeFirst = 0;
932  pSecPar->nBTLimit = nBTLimit;
933  pSecPar->TimeLimit = nTimeLim;
934  pSecPar->fVerbose = fVerbose;
935  pMan = Gia_ManToAig( pMiter, 0 );
936  Gia_ManStop( pMiter );
937  Status = Fra_FraigSec( pMan, pSecPar, NULL );
938  Aig_ManStop( pMan );
939  }
940  }
941  else
942  {
943  pMiter = Gia_ManMiter( pGia0, pGia1, 0, 1, 0, 0, fVerbose );
944  if ( pMiter )
945  {
946  Cec_ParCec_t ParsCec, * pPars = &ParsCec;
947  Cec_ManCecSetDefaultParams( pPars );
948  pPars->nBTLimit = nBTLimit;
949  pPars->TimeLimit = nTimeLim;
950  pPars->fVerbose = fVerbose;
951  Status = Cec_ManVerify( pMiter, pPars );
952  if ( pPars->iOutFail >= 0 )
953  Abc_Print( 1, "Verification failed for at least one output (%d).\n", pPars->iOutFail );
954  Gia_ManStop( pMiter );
955  }
956  }
957  Gia_ManStop( pGia0 );
958  Gia_ManStop( pGia1 );
959  Gia_ManStop( pSpec );
960  return Status;
961 }
962 
963 ////////////////////////////////////////////////////////////////////////
964 /// END OF FILE ///
965 ////////////////////////////////////////////////////////////////////////
966 
967 
968 ABC_NAMESPACE_IMPL_END
969 
Tim_ManBoxOutputFirst
int Tim_ManBoxOutputFirst(Tim_Man_t *p, int iBox)
Definition: timBox.c:154
Gia_ObjLevelId
static int Gia_ObjLevelId(Gia_Man_t *p, int Id)
Definition: gia.h:500
Gia_ManAppendAnd
static int Gia_ManAppendAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:592
Tim_ManCoNum
int Tim_ManCoNum(Tim_Man_t *p)
Definition: timMan.c:684
Gia_ManDupCollapse_rec
void Gia_ManDupCollapse_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Gia_Man_t *pNew)
Definition: giaTim.c:733
Gia_ManOrderWithBoxes
Vec_Int_t * Gia_ManOrderWithBoxes(Gia_Man_t *p)
Definition: giaTim.c:277
Gia_ObjSetLevelId
static void Gia_ObjSetLevelId(Gia_Man_t *p, int Id, int l)
Definition: gia.h:502
Gia_ManBoxCiNum
int Gia_ManBoxCiNum(Gia_Man_t *p)
Definition: giaTim.c:61
Gia_ObjSiblObj
static Gia_Obj_t * Gia_ObjSiblObj(Gia_Man_t *p, int Id)
Definition: gia.h:894
Gia_ManDupNormalize
Gia_Man_t * Gia_ManDupNormalize(Gia_Man_t *p)
Definition: giaTim.c:134
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
Fra_Sec_t_::TimeLimit
int TimeLimit
Definition: fra.h:141
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManBoxNum
ABC_NAMESPACE_IMPL_START int Gia_ManBoxNum(Gia_Man_t *p)
DECLARATIONS ///.
Definition: giaTim.c:49
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_Man_t_::pAigExtra
Gia_Man_t * pAigExtra
Definition: gia.h:149
Gia_AigerRead
Gia_Man_t * Gia_AigerRead(char *pFileName, int fSkipStrash, int fCheck)
Definition: giaAiger.c:821
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Gia_ManLutLevelWithBoxes_rec
int Gia_ManLutLevelWithBoxes_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaTim.c:553
Gia_ObjSetValue
static void Gia_ObjSetValue(Gia_Obj_t *pObj, int i)
Definition: gia.h:414
Gia_ManCi
static Gia_Obj_t * Gia_ManCi(Gia_Man_t *p, int v)
Definition: gia.h:403
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fra_Sec_t_
Definition: fra.h:114
Cec_ParCec_t_::nBTLimit
int nBTLimit
Definition: cec.h:120
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_IntCountEntry
static int Vec_IntCountEntry(Vec_Int_t *p, int Entry)
Definition: vecInt.h:1156
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Gia_Man_t_::vRegClasses
Vec_Int_t * vRegClasses
Definition: gia.h:144
Gia_ObjIsTravIdCurrent
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
Gia_ManNonRegBoxNum
int Gia_ManNonRegBoxNum(Gia_Man_t *p)
Definition: giaTim.c:57
Gia_Man_t_::pSibls
int * pSibls
Definition: gia.h:123
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Gia_ObjIsConst0
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
Gia_ManUpdateTimMan
void * Gia_ManUpdateTimMan(Gia_Man_t *p, Vec_Int_t *vBoxPres)
Definition: giaTim.c:657
Gia_ObjValue
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
Fra_SecSetDefaultParams
void Fra_SecSetDefaultParams(Fra_Sec_t *p)
DECLARATIONS ///.
Definition: fraSec.c:51
Gia_ManUpdateExtraAig2
Gia_Man_t * Gia_ManUpdateExtraAig2(void *pTime, Gia_Man_t *p, Vec_Int_t *vBoxesLeft)
Definition: giaTim.c:702
Gia_ObjIsBuf
static int Gia_ObjIsBuf(Gia_Obj_t *pObj)
Definition: gia.h:427
Tim_ManBoxOutputNum
int Tim_ManBoxOutputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:202
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
Gia_ManIsNormalized
int Gia_ManIsNormalized(Gia_Man_t *p)
Definition: giaTim.c:109
Gia_Man_t_::nLevels
int nLevels
Definition: gia.h:116
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Gia_ManDupUnshuffleInputs
Gia_Man_t * Gia_ManDupUnshuffleInputs(Gia_Man_t *p)
Definition: giaTim.c:194
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Tim_ManReduce
Tim_Man_t * Tim_ManReduce(Tim_Man_t *p, Vec_Int_t *vBoxesLeft, int nTermsDiff)
Definition: timMan.c:251
Gia_ManCleanupRemap
void Gia_ManCleanupRemap(Gia_Man_t *p, Gia_Man_t *pGia)
Definition: giaTim.c:424
Gia_Obj_t_
Definition: gia.h:75
Gia_ManDupOutputVec
Gia_Man_t * Gia_ManDupOutputVec(Gia_Man_t *p, Vec_Int_t *vOutPres)
Definition: giaDup.c:232
Gia_ManHasChoices
static int Gia_ManHasChoices(Gia_Man_t *p)
Definition: gia.h:397
Tim_ManPiNum
int Tim_ManPiNum(Tim_Man_t *p)
Definition: timMan.c:688
Fra_Sec_t_::fVerbose
int fVerbose
Definition: fra.h:139
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Gia_ManOrderWithBoxes_rec
int Gia_ManOrderWithBoxes_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes)
Definition: giaTim.c:249
Gia_ManIsSeqWithBoxes
int Gia_ManIsSeqWithBoxes(Gia_Man_t *p)
Definition: giaTim.c:93
Tim_ManBoxFindFromCiNum
int Tim_ManBoxFindFromCiNum(Tim_Man_t *p, int iCiNum)
Definition: timBox.c:306
Gia_ObjLevel
static int Gia_ObjLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:501
Gia_ObjSibl
static int Gia_ObjSibl(Gia_Man_t *p, int Id)
Definition: gia.h:893
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Gia_Man_t_::iData2
int iData2
Definition: gia.h:172
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_Man_t_::nConstrs
int nConstrs
Definition: gia.h:117
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Gia_ManAppendBuf
static int Gia_ManAppendBuf(Gia_Man_t *p, int iLit)
Definition: gia.h:694
Gia_ObjSetAndLevel
static void Gia_ObjSetAndLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:506
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Vec_IntFindMax
static int Vec_IntFindMax(Vec_Int_t *p)
Definition: vecInt.h:996
Gia_ObjSetTravIdCurrent
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Tim_ManCiNum
int Tim_ManCiNum(Tim_Man_t *p)
Definition: timMan.c:680
Cec_ManCecSetDefaultParams
void Cec_ManCecSetDefaultParams(Cec_ParCec_t *p)
Definition: cecCore.c:157
Gia_Man_t_::pSpec
char * pSpec
Definition: gia.h:98
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Gia_ManToAig
Aig_Man_t * Gia_ManToAig(Gia_Man_t *p, int fChoices)
Definition: giaAig.c:277
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ManRegBoxNum
int Gia_ManRegBoxNum(Gia_Man_t *p)
Definition: giaTim.c:53
Gia_Man_t_::pManTime
void * pManTime
Definition: gia.h:165
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Gia_ManCleanLevels
void Gia_ManCleanLevels(Gia_Man_t *p, int Size)
Definition: giaUtil.c:470
Gia_ManBoxCoNum
int Gia_ManBoxCoNum(Gia_Man_t *p)
Definition: giaTim.c:65
Tim_ManTrim
Tim_Man_t * Tim_ManTrim(Tim_Man_t *p, Vec_Int_t *vBoxPres)
Definition: timMan.c:163
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
Tim_ManBoxNum
int Tim_ManBoxNum(Tim_Man_t *p)
Definition: timMan.c:702
Cec_ParCec_t_::TimeLimit
int TimeLimit
Definition: cec.h:121
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Cec_ParCec_t_
Definition: cec.h:118
Tim_ManBoxInputNum
int Tim_ManBoxInputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:186
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Gia_Man_t_::nAnd2Delay
int nAnd2Delay
Definition: gia.h:173
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
Fra_FraigSec
int Fra_FraigSec(Aig_Man_t *p, Fra_Sec_t *pParSec, Aig_Man_t **ppResult)
Definition: fraSec.c:95
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Fra_Sec_t_::nBTLimit
int nBTLimit
Definition: fra.h:119
Cec_ParCec_t_::iOutFail
int iOutFail
Definition: cec.h:128
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Tim_ManBoxIsBlack
int Tim_ManBoxIsBlack(Tim_Man_t *p, int iBox)
Definition: timBox.c:257
Gia_ManDupUnnormalize
Gia_Man_t * Gia_ManDupUnnormalize(Gia_Man_t *p)
Definition: giaTim.c:373
Gia_ManCo
static Gia_Obj_t * Gia_ManCo(Gia_Man_t *p, int v)
Definition: gia.h:404
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Tim_ManBlackBoxNum
int Tim_ManBlackBoxNum(Tim_Man_t *p)
Definition: timMan.c:706
Gia_ObjSetCoLevel
static void Gia_ObjSetCoLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:504
Gia_ManLevelWithBoxes
int Gia_ManLevelWithBoxes(Gia_Man_t *p)
Definition: giaTim.c:469
Gia_Man_t_
Definition: gia.h:95
Gia_ManBufNum
static int Gia_ManBufNum(Gia_Man_t *p)
Definition: gia.h:392
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gia_ManUpdateExtraAig
Gia_Man_t * Gia_ManUpdateExtraAig(void *pTime, Gia_Man_t *p, Vec_Int_t *vBoxPres)
Definition: giaTim.c:683
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Cec_ManVerify
int Cec_ManVerify(Gia_Man_t *p, Cec_ParCec_t *pPars)
MACRO DEFINITIONS ///.
Definition: cecCec.c:308
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Cec_ParCec_t_::fVerbose
int fVerbose
Definition: cec.h:127
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Gia_ManLutLevelWithBoxes
int Gia_ManLutLevelWithBoxes(Gia_Man_t *p)
Definition: giaTim.c:572
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManUpdateTimMan2
void * Gia_ManUpdateTimMan2(Gia_Man_t *p, Vec_Int_t *vBoxesLeft, int nTermsDiff)
Definition: giaTim.c:664
Gia_ManLevelNum
int Gia_ManLevelNum(Gia_Man_t *p)
Definition: giaUtil.c:505
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Tim_Man_t
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
Gia_ManDupCollapse
Gia_Man_t * Gia_ManDupCollapse(Gia_Man_t *p, Gia_Man_t *pBoxes, Vec_Int_t *vBoxPres, int fSeq)
Definition: giaTim.c:748
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
Gia_ManDupSelectedOutputs
Gia_Man_t * Gia_ManDupSelectedOutputs(Gia_Man_t *p, Vec_Int_t *vOutsLeft)
Definition: giaDup.c:266
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Tim_ManBoxInputFirst
int Tim_ManBoxInputFirst(Tim_Man_t *p, int iBox)
Definition: timBox.c:122
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Fra_Sec_t_::fRetimeFirst
int fRetimeFirst
Definition: fra.h:127
Tim_ManGetCiArrival
float Tim_ManGetCiArrival(Tim_Man_t *p, int iCi)
Definition: timTime.c:174
Tim_ManAlignTwo
Vec_Int_t * Tim_ManAlignTwo(Tim_Man_t *pSpec, Tim_Man_t *pImpl)
Definition: timMan.c:344
Gia_LutForEachFanin
#define Gia_LutForEachFanin(p, i, iFan, k)
Definition: gia.h:970
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_ManLevelWithBoxes_rec
int Gia_ManLevelWithBoxes_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaTim.c:452
Gia_ManVerifyWithBoxes
int Gia_ManVerifyWithBoxes(Gia_Man_t *pGia, int nBTLimit, int nTimeLim, int fSeq, int fVerbose, char *pFileSpec)
Definition: giaTim.c:859
Tim_ManPoNum
int Tim_ManPoNum(Tim_Man_t *p)
Definition: timMan.c:694
Gia_ManMiter
Gia_Man_t * Gia_ManMiter(Gia_Man_t *pAig0, Gia_Man_t *pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose)
Definition: giaDup.c:2128
Gia_ObjCioId
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_ManClockDomainNum
int Gia_ManClockDomainNum(Gia_Man_t *p)
Definition: giaTim.c:69
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Gia_ManDupRemapEquiv
void Gia_ManDupRemapEquiv(Gia_Man_t *pNew, Gia_Man_t *p)
DECLARATIONS ///.
Definition: giaDup.c:46
Gia_ObjSetLevel
static void Gia_ObjSetLevel(Gia_Man_t *p, Gia_Obj_t *pObj, int l)
Definition: gia.h:503
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Tim_ManBoxDelayTable
float * Tim_ManBoxDelayTable(Tim_Man_t *p, int iBox)
Definition: timBox.c:234