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