abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bmcUnroll.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [bmcUnroll.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT-based bounded model checking.]
8 
9  Synopsis [Unrolling 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: bmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "bmc.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 ////////////////////////////////////////////////////////////////////////
26 /// DECLARATIONS ///
27 ////////////////////////////////////////////////////////////////////////
28 
29 #define UNR_DIFF_NULL 0x7FFF
30 
31 typedef struct Unr_Obj_t_ Unr_Obj_t; // 24 bytes + (RankMax-1) * 4 bytes
32 struct Unr_Obj_t_
33 {
34  unsigned hFan0; // address of the fanin
35  unsigned hFan1; // address of the fanin
36  unsigned fCompl0 : 1; // complemented bit
37  unsigned fCompl1 : 1; // complemented bit
38  unsigned uRDiff0 : 15; // rank diff of the fanin
39  unsigned uRDiff1 : 15; // rank diff of the fanin
40  unsigned fItIsPi : 1; // remember attributes
41  unsigned fItIsPo : 1; // remember attributes
42  unsigned RankMax : 15; // max rank diff between node and its fanout
43  unsigned RankCur : 15; // cur rank of the node
44  unsigned OrigId; // original object ID
45  unsigned Res[1]; // RankMax entries
46 };
47 
48 struct Unr_Man_t_
49 {
50  // input data
51  Gia_Man_t * pGia; // the user's AIG manager
52  Gia_Man_t * pFrames; // unrolled manager
53  int nObjs; // the number of objects
54  // intermediate data
55  Vec_Int_t * vOrder; // ordering of GIA objects
56  Vec_Int_t * vOrderLim; // beginning of each time frame
57  Vec_Int_t * vTents; // tents of GIA objects
58  Vec_Int_t * vRanks; // ranks of GIA objects
59  // unrolling data
60  int * pObjs; // storage for unroling objects
61  int * pEnd; // end of storage
62  Vec_Int_t * vObjLim; // handle of the first object in each frame
63  Vec_Int_t * vCiMap; // mapping of GIA CIs into unrolling objects
64  Vec_Int_t * vCoMap; // mapping of GIA POs into unrolling objects
65  Vec_Int_t * vPiLits; // storage for PI literals
66 };
67 
68 static inline Unr_Obj_t * Unr_ManObj( Unr_Man_t * p, int h ) { assert( h >= 0 && h < p->pEnd - p->pObjs ); return (Unr_Obj_t *)(p->pObjs + h); }
69 static inline int Unr_ObjSizeInt( int Rank ) { return 0xFFFFFFFE & (sizeof(Unr_Obj_t) / sizeof(int) + Rank); }
70 static inline int Unr_ObjSize( Unr_Obj_t * pObj ) { return Unr_ObjSizeInt(pObj->RankMax); }
71 
72 static inline int Unr_ManFanin0Value( Unr_Man_t * p, Unr_Obj_t * pObj )
73 {
74  Unr_Obj_t * pFanin = Unr_ManObj( p, pObj->hFan0 );
75  int Index = (pFanin->RankCur + pFanin->RankMax - pObj->uRDiff0) % pFanin->RankMax;
76  assert( pFanin->RankCur < pFanin->RankMax );
77  assert( pObj->uRDiff0 < pFanin->RankMax );
78  return Abc_LitNotCond( pFanin->Res[Index], pObj->fCompl0 );
79 }
80 static inline int Unr_ManFanin1Value( Unr_Man_t * p, Unr_Obj_t * pObj )
81 {
82  Unr_Obj_t * pFanin = Unr_ManObj( p, pObj->hFan1 );
83  int Index = (pFanin->RankCur + pFanin->RankMax - pObj->uRDiff1) % pFanin->RankMax;
84  assert( pFanin->RankCur < pFanin->RankMax );
85  assert( pObj->uRDiff1 < pFanin->RankMax );
86  return Abc_LitNotCond( pFanin->Res[Index], pObj->fCompl1 );
87 }
88 static inline int Unr_ManObjReadValue( Unr_Obj_t * pObj )
89 {
90  assert( pObj->RankCur >= 0 && pObj->RankCur < pObj->RankMax );
91  return pObj->Res[ pObj->RankCur ];
92 }
93 static inline void Unr_ManObjSetValue( Unr_Obj_t * pObj, int Value )
94 {
95  assert( Value >= 0 );
96  pObj->RankCur = (UNR_DIFF_NULL & (pObj->RankCur + 1)) % pObj->RankMax;
97  pObj->Res[ pObj->RankCur ] = Value;
98 }
99 
100 ////////////////////////////////////////////////////////////////////////
101 /// FUNCTION DEFINITIONS ///
102 ////////////////////////////////////////////////////////////////////////
103 
104 /**Function*************************************************************
105 
106  Synopsis []
107 
108  Description []
109 
110  SideEffects []
111 
112  SeeAlso []
113 
114 ***********************************************************************/
115 static inline void Vec_IntWriteMaxEntry( Vec_Int_t * p, int i, int Entry )
116 {
117  assert( i >= 0 && i < p->nSize );
118  p->pArray[i] = Abc_MaxInt( p->pArray[i], Entry );
119 }
120 
121 /**Function*************************************************************
122 
123  Synopsis []
124 
125  Description []
126 
127  SideEffects []
128 
129  SeeAlso []
130 
131 ***********************************************************************/
132 void Unr_ManProfileRanks( Vec_Int_t * vRanks )
133 {
134  int RankMax = Vec_IntFindMax( vRanks );
135  Vec_Int_t * vCounts = Vec_IntStart( RankMax+1 );
136  int i, Rank, Count, nExtras = 0;
137  Vec_IntForEachEntry( vRanks, Rank, i )
138  Vec_IntAddToEntry( vCounts, Rank, 1 );
139  Vec_IntForEachEntry( vCounts, Count, i )
140  {
141  if ( Count == 0 )
142  continue;
143  printf( "%2d : %8d (%6.2f %%)\n", i, Count, 100.0 * Count / Vec_IntSize(vRanks) );
144  nExtras += Count * i;
145  }
146  printf( "Extra space = %d (%6.2f %%) ", nExtras, 100.0 * nExtras / Vec_IntSize(vRanks) );
147  Vec_IntFree( vCounts );
148 }
149 
150 /**Function*************************************************************
151 
152  Synopsis []
153 
154  Description []
155 
156  SideEffects []
157 
158  SeeAlso []
159 
160 ***********************************************************************/
161 void Unr_ManSetup_rec( Unr_Man_t * p, int iObj, int iTent, Vec_Int_t * vRoots )
162 {
163  Gia_Obj_t * pObj;
164  int iFanin;
165  if ( Vec_IntEntry(p->vTents, iObj) >= 0 )
166  return;
167  Vec_IntWriteEntry(p->vTents, iObj, iTent);
168  pObj = Gia_ManObj( p->pGia, iObj );
169  if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) )
170  {
171  Unr_ManSetup_rec( p, (iFanin = Gia_ObjFaninId0(pObj, iObj)), iTent, vRoots );
172  Vec_IntWriteMaxEntry( p->vRanks, iFanin, Abc_MaxInt(0, iTent - Vec_IntEntry(p->vTents, iFanin) - 1) );
173  }
174  if ( Gia_ObjIsAnd(pObj) )
175  {
176  Unr_ManSetup_rec( p, (iFanin = Gia_ObjFaninId1(pObj, iObj)), iTent, vRoots );
177  Vec_IntWriteMaxEntry( p->vRanks, iFanin, Abc_MaxInt(0, iTent - Vec_IntEntry(p->vTents, iFanin) - 1) );
178  }
179  else if ( Gia_ObjIsRo(p->pGia, pObj) )
180  {
181  Vec_IntPush( vRoots, (iFanin = Gia_ObjId(p->pGia, Gia_ObjRoToRi(p->pGia, pObj))) );
182  Vec_IntWriteMaxEntry( p->vRanks, iFanin, 0 );
183  }
184  Vec_IntPush( p->vOrder, iObj );
185 }
186 void Unr_ManSetup( Unr_Man_t * p, int fVerbose )
187 {
188  Vec_Int_t * vRoots, * vRoots2, * vMap;
189  Unr_Obj_t * pUnrObj;
190  Gia_Obj_t * pObj;
191  int i, k, t, iObj, nInts, * pInts;
192  abctime clk = Abc_Clock();
193  // create zero rank
194  assert( Vec_IntSize(p->vOrder) == 0 );
195  Vec_IntPush( p->vOrder, 0 );
196  Vec_IntPush( p->vOrderLim, Vec_IntSize(p->vOrder) );
197  Vec_IntWriteEntry( p->vTents, 0, 0 );
198  Vec_IntWriteEntry( p->vRanks, 0, 0 );
199  // start from the POs
200  vRoots = Vec_IntAlloc( 100 );
201  vRoots2 = Vec_IntAlloc( 100 );
202  Gia_ManForEachPo( p->pGia, pObj, i )
203  Unr_ManSetup_rec( p, Gia_ObjId(p->pGia, pObj), 0, vRoots );
204  // collect tents
205  while ( Vec_IntSize(vRoots) > 0 )
206  {
207  Vec_IntPush( p->vOrderLim, Vec_IntSize(p->vOrder) );
208  Vec_IntClear( vRoots2 );
209  Vec_IntForEachEntry( vRoots, iObj, i )
210  Unr_ManSetup_rec( p, iObj, Vec_IntSize(p->vOrderLim)-1, vRoots2 );
211  ABC_SWAP( Vec_Int_t *, vRoots, vRoots2 );
212  }
213  Vec_IntPush( p->vOrderLim, Vec_IntSize(p->vOrder) );
214  Vec_IntFree( vRoots );
215  Vec_IntFree( vRoots2 );
216  // allocate memory
217  nInts = 0;
218  Vec_IntForEachEntry( p->vOrder, iObj, i )
219  nInts += Unr_ObjSizeInt( Vec_IntEntry(p->vRanks, iObj) + 1 );
220  p->pObjs = pInts = ABC_CALLOC( int, nInts );
221  p->pEnd = p->pObjs + nInts;
222  // create const0 node
223  pUnrObj = Unr_ManObj( p, pInts - p->pObjs );
224  pUnrObj->RankMax = Vec_IntEntry(p->vRanks, 0) + 1;
225  pUnrObj->uRDiff0 = pUnrObj->uRDiff1 = UNR_DIFF_NULL;
226  pUnrObj->Res[0] = 0; // const0
227  // map the objects
228  vMap = Vec_IntStartFull( p->nObjs );
229  Vec_IntWriteEntry( vMap, 0, pInts - p->pObjs );
230  pInts += Unr_ObjSize(pUnrObj);
231  // mark up the entries
232  assert( Vec_IntSize(p->vObjLim) == 0 );
233  for ( t = Vec_IntSize(p->vOrderLim) - 2; t >= 0; t-- )
234  {
235  int Beg = Vec_IntEntry(p->vOrderLim, t);
236  int End = Vec_IntEntry(p->vOrderLim, t+1);
237  Vec_IntPush( p->vObjLim, pInts - p->pObjs );
238  Vec_IntForEachEntryStartStop( p->vOrder, iObj, i, Beg, End )
239  {
240  pObj = Gia_ManObj( p->pGia, iObj );
241  pUnrObj = Unr_ManObj( p, pInts - p->pObjs );
242  pUnrObj->uRDiff0 = pUnrObj->uRDiff1 = UNR_DIFF_NULL;
243  if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) )
244  pUnrObj->uRDiff0 = Abc_MaxInt(0, Vec_IntEntry(p->vTents, iObj) - Vec_IntEntry(p->vTents, Gia_ObjFaninId0(pObj, iObj)) - 1);
245  if ( Gia_ObjIsAnd(pObj) )
246  pUnrObj->uRDiff1 = Abc_MaxInt(0, Vec_IntEntry(p->vTents, iObj) - Vec_IntEntry(p->vTents, Gia_ObjFaninId1(pObj, iObj)) - 1);
247  else if ( Gia_ObjIsRo(p->pGia, pObj) )
248  pUnrObj->uRDiff0 = 0;
249  pUnrObj->RankMax = Vec_IntEntry(p->vRanks, iObj) + 1;
250  pUnrObj->RankCur = UNR_DIFF_NULL;
251  pUnrObj->OrigId = iObj;
252  for ( k = 0; k < (int)pUnrObj->RankMax; k++ )
253  pUnrObj->Res[k] = -1;
254  assert( ((pInts - p->pObjs) & 1) == 0 ); // align for 64-bits
255  Vec_IntWriteEntry( vMap, iObj, pInts - p->pObjs );
256  pInts += Unr_ObjSize( pUnrObj );
257  }
258  }
259  assert( pInts - p->pObjs == nInts );
260  // label the objects
261  Gia_ManForEachObj( p->pGia, pObj, i )
262  {
263  if ( Vec_IntEntry(vMap, i) == -1 )
264  continue;
265  pUnrObj = Unr_ManObj( p, Vec_IntEntry(vMap, i) );
266  if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) )
267  {
268  pUnrObj->hFan0 = Vec_IntEntry( vMap, Gia_ObjFaninId0(pObj, i) );
269  pUnrObj->fCompl0 = Gia_ObjFaninC0(pObj);
270  pUnrObj->fItIsPo = Gia_ObjIsPo(p->pGia, pObj);
271  }
272  if ( Gia_ObjIsAnd(pObj) )
273  {
274  pUnrObj->hFan1 = Vec_IntEntry( vMap, Gia_ObjFaninId1(pObj, i) );
275  pUnrObj->fCompl1 = Gia_ObjFaninC1(pObj);
276  }
277  else if ( Gia_ObjIsRo(p->pGia, pObj) )
278  {
279  pUnrObj->hFan0 = Vec_IntEntry( vMap, Gia_ObjId(p->pGia, Gia_ObjRoToRi(p->pGia, pObj)) );
280  pUnrObj->fCompl0 = 0;
281  }
282  else if ( Gia_ObjIsPi(p->pGia, pObj) )
283  {
284  pUnrObj->hFan0 = Gia_ObjCioId(pObj); // remember CIO id
285  pUnrObj->hFan1 = Vec_IntEntry(p->vTents, i); // remember tent
286  pUnrObj->fItIsPi = 1;
287  }
288  }
289  // store CI/PO objects;
290  Gia_ManForEachCi( p->pGia, pObj, i )
291  Vec_IntPush( p->vCiMap, Vec_IntEntry(vMap, Gia_ObjId(p->pGia, pObj)) );
292  Gia_ManForEachCo( p->pGia, pObj, i )
293  Vec_IntPush( p->vCoMap, Vec_IntEntry(vMap, Gia_ObjId(p->pGia, pObj)) );
294  Vec_IntFreeP( &vMap );
295  // print stats
296  if ( fVerbose )
297  {
298  Unr_ManProfileRanks( p->vRanks );
299  printf( "Memory usage = %6.2f MB ", 4.0 * nInts / (1<<20) );
300  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
301  }
302  Vec_IntFreeP( &p->vOrder );
303  Vec_IntFreeP( &p->vOrderLim );
304  Vec_IntFreeP( &p->vRanks );
305  Vec_IntFreeP( &p->vTents );
306 }
307 
308 
309 
310 /**Function*************************************************************
311 
312  Synopsis []
313 
314  Description []
315 
316  SideEffects []
317 
318  SeeAlso []
319 
320 ***********************************************************************/
321 Unr_Man_t * Unr_ManAlloc( Gia_Man_t * pGia )
322 {
323  Unr_Man_t * p;
324  p = ABC_CALLOC( Unr_Man_t, 1 );
325  p->pGia = pGia;
326  p->nObjs = Gia_ManObjNum(pGia);
327  p->vOrder = Vec_IntAlloc( p->nObjs );
328  p->vOrderLim = Vec_IntAlloc( 100 );
329  p->vTents = Vec_IntStartFull( p->nObjs );
330  p->vRanks = Vec_IntStart( p->nObjs );
331  p->vObjLim = Vec_IntAlloc( 100 );
332  p->vCiMap = Vec_IntAlloc( Gia_ManCiNum(pGia) );
333  p->vCoMap = Vec_IntAlloc( Gia_ManCoNum(pGia) );
334  p->vPiLits = Vec_IntAlloc( 10000 );
335  p->pFrames = Gia_ManStart( 10000 );
336  p->pFrames->pName = Abc_UtilStrsav( pGia->pName );
337  Gia_ManHashStart( p->pFrames );
338  return p;
339 }
340 void Unr_ManFree( Unr_Man_t * p )
341 {
342  Gia_ManStop( p->pFrames );
343  // intermediate data
344  Vec_IntFreeP( &p->vOrder );
345  Vec_IntFreeP( &p->vOrderLim );
346  Vec_IntFreeP( &p->vTents );
347  Vec_IntFreeP( &p->vRanks );
348  // unrolling data
349  Vec_IntFreeP( &p->vObjLim );
350  Vec_IntFreeP( &p->vCiMap );
351  Vec_IntFreeP( &p->vCoMap );
352  Vec_IntFreeP( &p->vPiLits );
353  ABC_FREE( p->pObjs );
354  ABC_FREE( p );
355 }
356 
357 /**Function*************************************************************
358 
359  Synopsis [Perform smart unrolling.]
360 
361  Description []
362 
363  SideEffects []
364 
365  SeeAlso []
366 
367 ***********************************************************************/
368 Unr_Man_t * Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose )
369 {
370  int i, iHandle;
371  Unr_Man_t * p;
372  p = Unr_ManAlloc( pGia );
373  Unr_ManSetup( p, fVerbose );
374  for ( i = 0; i < Gia_ManRegNum(p->pGia); i++ )
375  if ( (iHandle = Vec_IntEntry(p->vCoMap, Gia_ManPoNum(p->pGia) + i)) != -1 )
376  Unr_ManObjSetValue( Unr_ManObj(p, iHandle), 0 );
377  return p;
378 }
379 Gia_Man_t * Unr_ManUnrollFrame( Unr_Man_t * p, int f )
380 {
381  int i, iLit, iLit0, iLit1, hStart;
382  for ( i = 0; i < Gia_ManPiNum(p->pGia); i++ )
383  Vec_IntPush( p->vPiLits, Gia_ManAppendCi(p->pFrames) );
384  hStart = Vec_IntEntry( p->vObjLim, Abc_MaxInt(0, Vec_IntSize(p->vObjLim)-1-f) );
385  while ( p->pObjs + hStart < p->pEnd )
386  {
387  Unr_Obj_t * pUnrObj = Unr_ManObj( p, hStart );
388  if ( pUnrObj->uRDiff0 != UNR_DIFF_NULL && pUnrObj->uRDiff1 != UNR_DIFF_NULL ) // AND node
389  {
390  iLit0 = Unr_ManFanin0Value( p, pUnrObj );
391  iLit1 = Unr_ManFanin1Value( p, pUnrObj );
392  iLit = Gia_ManHashAnd( p->pFrames, iLit0, iLit1 );
393  Unr_ManObjSetValue( pUnrObj, iLit );
394  }
395  else if ( pUnrObj->uRDiff0 != UNR_DIFF_NULL && pUnrObj->uRDiff1 == UNR_DIFF_NULL ) // PO/RI/RO
396  {
397  iLit = Unr_ManFanin0Value( p, pUnrObj );
398  Unr_ManObjSetValue( pUnrObj, iLit );
399  if ( pUnrObj->fItIsPo )
400  Gia_ManAppendCo( p->pFrames, iLit );
401  }
402  else // PI (pUnrObj->hFan0 is CioId; pUnrObj->hFan1 is tent)
403  {
404  assert( pUnrObj->fItIsPi && f >= (int)pUnrObj->hFan1 );
405  iLit = Vec_IntEntry( p->vPiLits, Gia_ManPiNum(p->pGia) * (f - pUnrObj->hFan1) + pUnrObj->hFan0 );
406  Unr_ManObjSetValue( pUnrObj, iLit );
407  }
408  hStart += Unr_ObjSize( pUnrObj );
409  }
410  assert( p->pObjs + hStart == p->pEnd );
411  assert( Gia_ManPoNum(p->pFrames) == (f + 1) * Gia_ManPoNum(p->pGia) );
412  return p->pFrames;
413 }
414 Gia_Man_t * Unr_ManUnroll( Gia_Man_t * pGia, int nFrames )
415 {
416  Unr_Man_t * p;
417  Gia_Man_t * pFrames;
418  int f;
419  p = Unr_ManUnrollStart( pGia, 1 );
420  for ( f = 0; f < nFrames; f++ )
421  Unr_ManUnrollFrame( p, f );
422  pFrames = Gia_ManCleanup( p->pFrames );
423  Unr_ManFree( p );
424  return pFrames;
425 }
426 
427 /**Function*************************************************************
428 
429  Synopsis [Perform naive unrolling.]
430 
431  Description []
432 
433  SideEffects []
434 
435  SeeAlso []
436 
437 ***********************************************************************/
438 Gia_Man_t * Unr_ManUnrollSimple( Gia_Man_t * pGia, int nFrames )
439 {
440  Gia_Man_t * pFrames;
441  Gia_Obj_t * pObj, * pObjRi;
442  int f, i;
443  pFrames = Gia_ManStart( 10000 );
444  pFrames->pName = Abc_UtilStrsav( pGia->pName );
445  Gia_ManHashAlloc( pFrames );
446  Gia_ManConst0(pGia)->Value = 0;
447  Gia_ManForEachRi( pGia, pObj, i )
448  pObj->Value = 0;
449  for ( f = 0; f < nFrames; f++ )
450  {
451  Gia_ManForEachPi( pGia, pObj, i )
452  pObj->Value = Gia_ManAppendCi(pFrames);
453  Gia_ManForEachRiRo( pGia, pObjRi, pObj, i )
454  pObj->Value = pObjRi->Value;
455  Gia_ManForEachAnd( pGia, pObj, i )
456  pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
457  Gia_ManForEachCo( pGia, pObj, i )
458  pObj->Value = Gia_ObjFanin0Copy(pObj);
459  Gia_ManForEachPo( pGia, pObj, i )
460  Gia_ManAppendCo( pFrames, pObj->Value );
461  }
462  Gia_ManHashStop( pFrames );
463  Gia_ManSetRegNum( pFrames, 0 );
464  pFrames = Gia_ManCleanup( pGia = pFrames );
465  Gia_ManStop( pGia );
466  return pFrames;
467 }
468 
469 /**Function*************************************************************
470 
471  Synopsis [Perform evaluation.]
472 
473  Description []
474 
475  SideEffects []
476 
477  SeeAlso []
478 
479 ***********************************************************************/
480 void Unr_ManTest( Gia_Man_t * pGia, int nFrames )
481 {
482  Gia_Man_t * pFrames0, * pFrames1;
483  abctime clk = Abc_Clock();
484  pFrames0 = Unr_ManUnroll( pGia, nFrames );
485  Abc_PrintTime( 1, "Unroll ", Abc_Clock() - clk );
486  clk = Abc_Clock();
487  pFrames1 = Unr_ManUnrollSimple( pGia, nFrames );
488  Abc_PrintTime( 1, "UnrollS", Abc_Clock() - clk );
489 
490 Gia_ManPrintStats( pFrames0, NULL );
491 Gia_ManPrintStats( pFrames1, NULL );
492 Gia_AigerWrite( pFrames0, "frames0.aig", 0, 0 );
493 Gia_AigerWrite( pFrames1, "frames1.aig", 0, 0 );
494 
495  Gia_ManStop( pFrames0 );
496  Gia_ManStop( pFrames1 );
497 }
498 
499 ////////////////////////////////////////////////////////////////////////
500 /// END OF FILE ///
501 ////////////////////////////////////////////////////////////////////////
502 
503 
504 ABC_NAMESPACE_IMPL_END
505 
Unr_Obj_t_::hFan0
unsigned hFan0
Definition: bmcUnroll.c:34
Unr_Man_t
typedefABC_NAMESPACE_HEADER_START struct Unr_Man_t_ Unr_Man_t
INCLUDES ///.
Definition: bmc.h:43
Unr_ManUnrollSimple
Gia_Man_t * Unr_ManUnrollSimple(Gia_Man_t *pGia, int nFrames)
Definition: bmcUnroll.c:438
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Unr_Man_t_::vOrderLim
Vec_Int_t * vOrderLim
Definition: bmcUnroll.c:56
Unr_Man_t_::pGia
Gia_Man_t * pGia
Definition: bmcUnroll.c:51
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Unr_ManUnrollStart
Unr_Man_t * Unr_ManUnrollStart(Gia_Man_t *pGia, int fVerbose)
Definition: bmcUnroll.c:368
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition: giaMan.c:389
Unr_ManUnrollFrame
Gia_Man_t * Unr_ManUnrollFrame(Unr_Man_t *p, int f)
Definition: bmcUnroll.c:379
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
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
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
UNR_DIFF_NULL
#define UNR_DIFF_NULL
DECLARATIONS ///.
Definition: bmcUnroll.c:29
Unr_ManProfileRanks
void Unr_ManProfileRanks(Vec_Int_t *vRanks)
Definition: bmcUnroll.c:132
Unr_Man_t_::vCiMap
Vec_Int_t * vCiMap
Definition: bmcUnroll.c:63
Unr_Obj_t_::fItIsPo
unsigned fItIsPo
Definition: bmcUnroll.c:41
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Unr_Man_t_::pEnd
int * pEnd
Definition: bmcUnroll.c:61
Unr_ManFree
void Unr_ManFree(Unr_Man_t *p)
Definition: bmcUnroll.c:340
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
Unr_ManObj
static Unr_Obj_t * Unr_ManObj(Unr_Man_t *p, int h)
Definition: bmcUnroll.c:68
Unr_ManSetup
void Unr_ManSetup(Unr_Man_t *p, int fVerbose)
Definition: bmcUnroll.c:186
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Gia_Man_t_::nObjs
int nObjs
Definition: gia.h:101
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Gia_Obj_t_
Definition: gia.h:75
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition: abc_global.h:218
Unr_ObjSize
static int Unr_ObjSize(Unr_Obj_t *pObj)
Definition: bmcUnroll.c:70
Unr_Obj_t_
Definition: bmcUnroll.c:32
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Unr_Man_t_::pFrames
Gia_Man_t * pFrames
Definition: bmcUnroll.c:52
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
Unr_Man_t_::nObjs
int nObjs
Definition: bmcUnroll.c:53
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Vec_IntAddToEntry
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
Unr_Obj_t_::hFan1
unsigned hFan1
Definition: bmcUnroll.c:35
Gia_ObjIsRo
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
Unr_Obj_t
struct Unr_Obj_t_ Unr_Obj_t
Definition: bmcUnroll.c:31
Gia_ObjRoToRi
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Vec_IntFindMax
static int Vec_IntFindMax(Vec_Int_t *p)
Definition: vecInt.h:996
Unr_ManFanin1Value
static int Unr_ManFanin1Value(Unr_Man_t *p, Unr_Obj_t *pObj)
Definition: bmcUnroll.c:80
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Gia_ManHashStart
void Gia_ManHashStart(Gia_Man_t *p)
Definition: giaHash.c:117
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Unr_Obj_t_::fItIsPi
unsigned fItIsPi
Definition: bmcUnroll.c:40
Unr_Obj_t_::fCompl0
unsigned fCompl0
Definition: bmcUnroll.c:36
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Unr_Obj_t_::fCompl1
unsigned fCompl1
Definition: bmcUnroll.c:37
Unr_Man_t_::vObjLim
Vec_Int_t * vObjLim
Definition: bmcUnroll.c:62
Unr_ManObjSetValue
static void Unr_ManObjSetValue(Unr_Obj_t *pObj, int Value)
Definition: bmcUnroll.c:93
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Unr_Man_t_::vRanks
Vec_Int_t * vRanks
Definition: bmcUnroll.c:58
Unr_Man_t_::vPiLits
Vec_Int_t * vPiLits
Definition: bmcUnroll.c:65
Unr_ManSetup_rec
void Unr_ManSetup_rec(Unr_Man_t *p, int iObj, int iTent, Vec_Int_t *vRoots)
Definition: bmcUnroll.c:161
Unr_ManUnroll
Gia_Man_t * Unr_ManUnroll(Gia_Man_t *pGia, int nFrames)
Definition: bmcUnroll.c:414
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact)
Definition: giaAiger.c:1024
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Unr_ManFanin0Value
static int Unr_ManFanin0Value(Unr_Man_t *p, Unr_Obj_t *pObj)
Definition: bmcUnroll.c:72
Unr_Man_t_
Definition: bmcUnroll.c:48
Unr_Man_t_::vOrder
Vec_Int_t * vOrder
Definition: bmcUnroll.c:55
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Unr_Man_t_::vTents
Vec_Int_t * vTents
Definition: bmcUnroll.c:57
Unr_Man_t_::vCoMap
Vec_Int_t * vCoMap
Definition: bmcUnroll.c:64
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Unr_ObjSizeInt
static int Unr_ObjSizeInt(int Rank)
Definition: bmcUnroll.c:69
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Unr_Man_t_::pObjs
int * pObjs
Definition: bmcUnroll.c:60
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Vec_IntWriteMaxEntry
static void Vec_IntWriteMaxEntry(Vec_Int_t *p, int i, int Entry)
FUNCTION DEFINITIONS ///.
Definition: bmcUnroll.c:115
Gia_Man_t_
Definition: gia.h:95
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Unr_Obj_t_::RankCur
unsigned RankCur
Definition: bmcUnroll.c:43
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Gia_ObjIsPo
static int Gia_ObjIsPo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:442
Unr_ManTest
void Unr_ManTest(Gia_Man_t *pGia, int nFrames)
Definition: bmcUnroll.c:480
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntForEachEntryStartStop
#define Vec_IntForEachEntryStartStop(vVec, Entry, i, Start, Stop)
Definition: vecInt.h:60
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Unr_Obj_t_::Res
unsigned Res[1]
Definition: bmcUnroll.c:45
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
Unr_ManAlloc
Unr_Man_t * Unr_ManAlloc(Gia_Man_t *pGia)
Definition: bmcUnroll.c:321
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Unr_ManObjReadValue
static int Unr_ManObjReadValue(Unr_Obj_t *pObj)
Definition: bmcUnroll.c:88
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
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_ObjFaninId1
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
Unr_Obj_t_::RankMax
unsigned RankMax
Definition: bmcUnroll.c:42
Unr_Obj_t_::uRDiff1
unsigned uRDiff1
Definition: bmcUnroll.c:39
Unr_Obj_t_::OrigId
unsigned OrigId
Definition: bmcUnroll.c:44
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_ObjCioId
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
Gia_ObjIsPi
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Unr_Obj_t_::uRDiff0
unsigned uRDiff0
Definition: bmcUnroll.c:38