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
Unr_ManObj(Unr_Man_t * p,int h)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); }
Unr_ObjSizeInt(int Rank)69 static inline int Unr_ObjSizeInt( int Rank ) { return 0xFFFFFFFE & (sizeof(Unr_Obj_t) / sizeof(int) + Rank); }
Unr_ObjSize(Unr_Obj_t * pObj)70 static inline int Unr_ObjSize( Unr_Obj_t * pObj ) { return Unr_ObjSizeInt(pObj->RankMax); }
71
Unr_ManFanin0Value(Unr_Man_t * p,Unr_Obj_t * pObj)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 }
Unr_ManFanin1Value(Unr_Man_t * p,Unr_Obj_t * pObj)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 }
Unr_ManObjReadValue(Unr_Obj_t * pObj)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 }
Unr_ManObjSetValue(Unr_Obj_t * pObj,int Value)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 ***********************************************************************/
Vec_IntWriteMaxEntry(Vec_Int_t * p,int i,int Entry)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 ***********************************************************************/
Unr_ManProfileRanks(Vec_Int_t * vRanks)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 ***********************************************************************/
Unr_ManSetup_rec(Unr_Man_t * p,int iObj,int iTent,Vec_Int_t * vRoots)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 }
Unr_ManSetup(Unr_Man_t * p,int fVerbose)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 ***********************************************************************/
Unr_ManAlloc(Gia_Man_t * pGia)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 }
Unr_ManFree(Unr_Man_t * p)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 ***********************************************************************/
Unr_ManUnrollStart(Gia_Man_t * pGia,int fVerbose)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 }
Unr_ManUnrollFrame(Unr_Man_t * p,int f)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 }
Unr_ManUnroll(Gia_Man_t * pGia,int nFrames)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 ***********************************************************************/
Unr_ManUnrollSimple(Gia_Man_t * pGia,int nFrames)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 ***********************************************************************/
Unr_ManTest(Gia_Man_t * pGia,int nFrames)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, 0 );
493 Gia_AigerWrite( pFrames1, "frames1.aig", 0, 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
506