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