giaTim.c 34.4 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
/**CFile****************************************************************

  FileName    [giaTim.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Scalable AIG package.]

  Synopsis    [Procedures with hierarchy/timing manager.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: giaTim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "gia.h"
22
#include "giaAig.h"
23 24
#include "misc/tim/tim.h"
#include "proof/cec/cec.h"
25
#include "proof/fra/fra.h"
26 27 28 29 30 31 32 33 34 35 36 37 38 39

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

40 41 42 43 44 45 46 47 48 49 50 51 52
  Synopsis    [Returns the number of boxes in the AIG with boxes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManBoxNum( Gia_Man_t * p )
{
    return p->pManTime ? Tim_ManBoxNum((Tim_Man_t *)p->pManTime) : 0;
}
53 54 55 56
int Gia_ManRegBoxNum( Gia_Man_t * p )
{
    return p->vRegClasses ? Vec_IntSize(p->vRegClasses) : 0;
}
57 58 59 60
int Gia_ManNonRegBoxNum( Gia_Man_t * p )
{
    return Gia_ManBoxNum(p) - Gia_ManRegBoxNum(p);
}
61 62 63 64
int Gia_ManBlackBoxNum( Gia_Man_t * p )
{
    return Tim_ManBlackBoxNum((Tim_Man_t *)p->pManTime);
}
65 66 67 68 69 70 71 72
int Gia_ManBoxCiNum( Gia_Man_t * p )
{
    return p->pManTime ? Gia_ManCiNum(p) - Tim_ManPiNum((Tim_Man_t *)p->pManTime) : 0;
}
int Gia_ManBoxCoNum( Gia_Man_t * p )
{
    return p->pManTime ? Gia_ManCoNum(p) - Tim_ManPoNum((Tim_Man_t *)p->pManTime) : 0;
}
73 74 75 76 77 78 79 80 81 82 83 84
int Gia_ManClockDomainNum( Gia_Man_t * p )
{
    int i, nDoms, Count = 0;
    if ( p->vRegClasses == NULL )
        return 0;
    nDoms = Vec_IntFindMax(p->vRegClasses);
    assert( Vec_IntCountEntry(p->vRegClasses, 0) == 0 );
    for ( i = 1; i <= nDoms; i++ )
        if ( Vec_IntCountEntry(p->vRegClasses, i) > 0 )
            Count++;
    return Count;    
}
85 86 87

/**Function*************************************************************

88 89 90 91 92 93 94 95 96 97 98
  Synopsis    [Returns one if this is a seq AIG with non-trivial boxes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManIsSeqWithBoxes( Gia_Man_t * p )
{
99
    return (Gia_ManRegNum(p) > 0 && Gia_ManBoxNum(p) > 0);
100 101 102 103
}

/**Function*************************************************************

104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
  Synopsis    [Makes sure the manager is normalized.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManIsNormalized( Gia_Man_t * p )  
{
    int i, nOffset;
    nOffset = 1;
    for ( i = 0; i < Gia_ManCiNum(p); i++ )
        if ( !Gia_ObjIsCi( Gia_ManObj(p, nOffset+i) ) )
            return 0;
    nOffset = 1 + Gia_ManCiNum(p) + Gia_ManAndNum(p);
    for ( i = 0; i < Gia_ManCoNum(p); i++ )
        if ( !Gia_ObjIsCo( Gia_ManObj(p, nOffset+i) ) )
            return 0;
    return 1;
}

/**Function*************************************************************

129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147
  Synopsis    [Duplicates AIG in the DFS order while putting CIs first.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
{
    Gia_Man_t * pNew;
    Gia_Obj_t * pObj;
    int i;
    Gia_ManFillValue( p );
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    Gia_ManConst0(p)->Value = 0;
148
    if ( !Gia_ManIsSeqWithBoxes(p) )
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
    {
        Gia_ManForEachCi( p, pObj, i )
            pObj->Value = Gia_ManAppendCi(pNew);
    }
    else
    {
        // current CI order:  PIs + FOs + NewCIs
        // desired reorder:   PIs + NewCIs + FOs
        int nCIs = Tim_ManPiNum( (Tim_Man_t *)p->pManTime );
        int nAll = Tim_ManCiNum( (Tim_Man_t *)p->pManTime );
        int nPis = nCIs - Gia_ManRegNum(p);
        assert( nAll == Gia_ManCiNum(p) );
        assert( nPis > 0 );
        // copy PIs first
        for ( i = 0; i < nPis; i++ )
            Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
       // copy new CIs second
        for ( i = nCIs; i < nAll; i++ )
            Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
        // copy flops last
        for ( i = nCIs - Gia_ManRegNum(p); i < nCIs; i++ )
            Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
171
        printf( "Warning: Shuffled CI order to be correct sequential AIG.\n" );
172
    }
173
    Gia_ManForEachAnd( p, pObj, i )
174 175 176 177
        if ( Gia_ObjIsBuf(pObj) )
            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
        else 
            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
178 179 180
    Gia_ManForEachCo( p, pObj, i )
        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
181
    pNew->nConstrs = p->nConstrs;
182 183 184 185 186 187 188
    assert( Gia_ManIsNormalized(pNew) );
    Gia_ManDupRemapEquiv( pNew, p );
    return pNew;
}

/**Function*************************************************************

189 190 191 192 193 194 195 196 197
  Synopsis    [Reorders flops for sequential AIGs with boxes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
198
Gia_Man_t * Gia_ManDupUnshuffleInputs( Gia_Man_t * p )
199 200 201 202 203 204
{
    Gia_Man_t * pNew;
    Gia_Obj_t * pObj;
    int i, nCIs, nAll, nPis;
    // sanity checks
    assert( Gia_ManIsNormalized(p) );
205
    assert( Gia_ManIsSeqWithBoxes(p) );
206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227
    Gia_ManFillValue( p );
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    Gia_ManConst0(p)->Value = 0;
    // change input order
    // desired reorder:   PIs + NewCIs + FOs
    // current CI order:  PIs + FOs + NewCIs
    nCIs = Tim_ManPiNum( (Tim_Man_t *)p->pManTime );
    nAll = Tim_ManCiNum( (Tim_Man_t *)p->pManTime );
    nPis = nCIs - Gia_ManRegNum(p);
    assert( nAll == Gia_ManCiNum(p) );
    assert( nPis > 0 );
    // copy PIs first
    for ( i = 0; i < nPis; i++ )
        Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
    // copy flops second
    for ( i = nAll - Gia_ManRegNum(p); i < nAll; i++ )
        Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
    // copy new CIs last
    for ( i = nPis; i < nAll - Gia_ManRegNum(p); i++ )
        Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
228
    printf( "Warning: Unshuffled CI order to be correct AIG with boxes.\n" );
229 230 231 232 233 234 235 236 237 238 239 240 241 242 243
    // other things
    Gia_ManForEachAnd( p, pObj, i )
        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
    Gia_ManForEachCo( p, pObj, i )
        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
    pNew->nConstrs = p->nConstrs;
    assert( Gia_ManIsNormalized(pNew) );
    Gia_ManDupRemapEquiv( pNew, p );
    return pNew;
}


/**Function*************************************************************

244 245 246 247 248 249 250 251 252
  Synopsis    [Find the ordering of AIG objects.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
253
int Gia_ManOrderWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
254 255
{
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
256
        return 0;
257
    Gia_ObjSetTravIdCurrent(p, pObj);
258 259
    if ( Gia_ObjIsCi(pObj) )
    {
260
        p->iData2 = Gia_ObjCioId(pObj);
261 262
        return 1;
    }
263
    assert( Gia_ObjIsAnd(pObj) );
264 265 266 267 268 269 270
    if ( Gia_ObjIsBuf(pObj) )
    {
        if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ) )
            return 1;
        Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
        return 0;
    }
271
    if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
272
        if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)), vNodes ) )
273
            return 1;
274
    if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ) )
275
        return 1;
276
    if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin1(pObj), vNodes ) )
277
        return 1;
278
    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
279
    return 0;
280
}
281
Vec_Int_t * Gia_ManOrderWithBoxes( Gia_Man_t * p )
282
{
Alan Mishchenko committed
283
    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
284 285 286
    Vec_Int_t * vNodes;
    Gia_Obj_t * pObj;
    int i, k, curCi, curCo;
Alan Mishchenko committed
287
    assert( pManTime != NULL );
288
    assert( Gia_ManIsNormalized( p ) );
289 290 291 292 293 294 295 296
    // start trav IDs
    Gia_ManIncrementTravId( p );
    // start the array
    vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
    // include constant
    Vec_IntPush( vNodes, 0 );
    Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
    // include primary inputs
Alan Mishchenko committed
297
    for ( i = 0; i < Tim_ManPiNum(pManTime); i++ )
298
    {
299
        pObj = Gia_ManCi( p, i );
300 301 302 303 304
        Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
        Gia_ObjSetTravIdCurrent( p, pObj );
        assert( Gia_ObjId(p, pObj) == i+1 );
    }
    // for each box, include box nodes
Alan Mishchenko committed
305
    curCi = Tim_ManPiNum(pManTime);
306
    curCo = 0;
Alan Mishchenko committed
307
    for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
308 309
    {
        // add internal nodes
Alan Mishchenko committed
310
        for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
311
        {
312
            pObj = Gia_ManCo( p, curCo + k );
313
            if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ) )
314
            {
315
                int iCiNum  = p->iData2;
Alan Mishchenko committed
316
                int iBoxNum = Tim_ManBoxFindFromCiNum( pManTime, iCiNum );
317
                printf( "The command has to terminate. Boxes are not in a topological order.\n" );
318 319
                printf( "The following information may help debugging (numbers are 0-based):\n" );
                printf( "Input %d of BoxA %d (1stCI = %d; 1stCO = %d) has TFI with CI %d,\n", 
Alan Mishchenko committed
320
                    k, i, Tim_ManBoxOutputFirst(pManTime, i), Tim_ManBoxInputFirst(pManTime, i), iCiNum );
321
                printf( "which corresponds to output %d of BoxB %d (1stCI = %d; 1stCO = %d).\n", 
Alan Mishchenko committed
322 323
                    iCiNum - Tim_ManBoxOutputFirst(pManTime, iBoxNum), iBoxNum, 
                    Tim_ManBoxOutputFirst(pManTime, iBoxNum), Tim_ManBoxInputFirst(pManTime, iBoxNum) );
324
                printf( "In a correct topological order, BoxB should precede BoxA.\n" );
325
                Vec_IntFree( vNodes );
326
                p->iData2 = 0;
327 328
                return NULL;
            }
329 330
        }
        // add POs corresponding to box inputs
Alan Mishchenko committed
331
        for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
332
        {
333
            pObj = Gia_ManCo( p, curCo + k );
334 335
            Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
        }
Alan Mishchenko committed
336
        curCo += Tim_ManBoxInputNum(pManTime, i);
337
        // add PIs corresponding to box outputs
Alan Mishchenko committed
338
        for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
339
        {
340
            pObj = Gia_ManCi( p, curCi + k );
341 342 343
            Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
            Gia_ObjSetTravIdCurrent( p, pObj );
        }
Alan Mishchenko committed
344
        curCi += Tim_ManBoxOutputNum(pManTime, i);
345 346
    }
    // add remaining nodes
Alan Mishchenko committed
347
    for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
348
    {
349
        pObj = Gia_ManCo( p, i );
350
        Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes );
351 352
    }
    // add POs
Alan Mishchenko committed
353
    for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
354
    {
355
        pObj = Gia_ManCo( p, i );
356 357
        Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
    }
Alan Mishchenko committed
358
    curCo += Tim_ManPoNum(pManTime);
359
    // verify counts
360 361
    assert( curCi == Gia_ManCiNum(p) );
    assert( curCo == Gia_ManCoNum(p) );
362 363 364 365 366 367 368 369 370 371 372 373 374 375 376
    assert( Vec_IntSize(vNodes) == Gia_ManObjNum(p) );
    return vNodes;
}

/**Function*************************************************************

  Synopsis    [Duplicates AIG according to the timing manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
377
Gia_Man_t * Gia_ManDupUnnormalize( Gia_Man_t * p )
378 379 380 381 382
{
    Vec_Int_t * vNodes;
    Gia_Man_t * pNew;
    Gia_Obj_t * pObj;
    int i;
383
    assert( !Gia_ManBufNum(p) );
384
    vNodes = Gia_ManOrderWithBoxes( p );
385 386
    if ( vNodes == NULL )
        return NULL;
387 388 389 390
    Gia_ManFillValue( p );
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
391
    if ( Gia_ManHasChoices(p) )
392
        pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) );
393 394
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
    {
395 396 397
        if ( Gia_ObjIsBuf(pObj) )
            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
        else if ( Gia_ObjIsAnd(pObj) )
398
        {
399
            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
400 401 402
            if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
                pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))->Value);        
        }
403 404 405 406 407 408 409 410 411
        else if ( Gia_ObjIsCi(pObj) )
            pObj->Value = Gia_ManAppendCi( pNew );
        else if ( Gia_ObjIsCo(pObj) )
            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
        else if ( Gia_ObjIsConst0(pObj) )
            pObj->Value = 0;
        else assert( 0 );
    }
    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
412
    Vec_IntFree( vNodes );
413 414 415 416 417 418
    return pNew;
}


/**Function*************************************************************

419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446
  Synopsis    [Remaps the AIG from the old manager into the new manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManCleanupRemap( Gia_Man_t * p, Gia_Man_t * pGia )
{
    Gia_Obj_t * pObj, * pObjGia;
    int i, iPrev;
    Gia_ManForEachObj1( p, pObj, i )
    {
        iPrev = Gia_ObjValue(pObj);
        if ( iPrev == ~0 )
            continue;
        pObjGia = Gia_ManObj( pGia, Abc_Lit2Var(iPrev) );
        if ( pObjGia->Value == ~0 )
            Gia_ObjSetValue( pObj, pObjGia->Value ); 
        else
            Gia_ObjSetValue( pObj, Abc_LitNotCond(pObjGia->Value, Abc_LitIsCompl(iPrev)) );
    }
}

/**Function*************************************************************

447
  Synopsis    [Computes level with boxes.]
448 449 450 451 452 453 454 455

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
456
int Gia_ManLevelWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
457 458
{
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
459
        return 0;
460
    Gia_ObjSetTravIdCurrent(p, pObj);
461 462
    if ( Gia_ObjIsCi(pObj) )
        return 1;
463
    assert( Gia_ObjIsAnd(pObj) );
464 465
    if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
        Gia_ManLevelWithBoxes_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)) );
466 467 468 469
    if ( Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ) )
        return 1;
    if ( Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin1(pObj) ) )
        return 1;
470
    Gia_ObjSetAndLevel( p, pObj );
471
    return 0;
472 473 474
}
int Gia_ManLevelWithBoxes( Gia_Man_t * p )
{
475
    int nAnd2Delay = p->nAnd2Delay ? p->nAnd2Delay : 1;
Alan Mishchenko committed
476
    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
477 478
    Gia_Obj_t * pObj, * pObjIn;
    int i, k, j, curCi, curCo, LevelMax;
479
    assert( Gia_ManRegNum(p) == 0 );
480
    assert( Gia_ManBufNum(p) == 0 );
481 482 483 484 485
    // copy const and real PIs
    Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
    Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 );
    Gia_ManIncrementTravId( p );
    Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
Alan Mishchenko committed
486
    for ( i = 0; i < Tim_ManPiNum(pManTime); i++ )
487
    {
488
        pObj = Gia_ManCi( p, i );
Alan Mishchenko committed
489
        Gia_ObjSetLevel( p, pObj, Tim_ManGetCiArrival(pManTime, i) / nAnd2Delay );
490 491 492
        Gia_ObjSetTravIdCurrent( p, pObj );
    }
    // create logic for each box
Alan Mishchenko committed
493
    curCi = Tim_ManPiNum(pManTime);
494
    curCo = 0;
Alan Mishchenko committed
495
    for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
496
    {
Alan Mishchenko committed
497 498 499
        int nBoxInputs  = Tim_ManBoxInputNum( pManTime, i );
        int nBoxOutputs = Tim_ManBoxOutputNum( pManTime, i );
        float * pDelayTable = Tim_ManBoxDelayTable( pManTime, i );
500 501
        // compute level for TFI of box inputs
        for ( k = 0; k < nBoxInputs; k++ )
502
        {
503
            pObj = Gia_ManCo( p, curCo + k );
504 505 506 507 508
            if ( Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ) )
            {
                printf( "Boxes are not in a topological order. Switching to level computation without boxes.\n" );
                return Gia_ManLevelNum( p );
            }
509
            // set box input level
510 511
            Gia_ObjSetCoLevel( p, pObj );
        }
512 513
        // compute level for box outputs
        for ( k = 0; k < nBoxOutputs; k++ )
514
        {
515
            pObj = Gia_ManCi( p, curCi + k );
516
            Gia_ObjSetTravIdCurrent( p, pObj );
517 518 519
            // evaluate delay of this output
            LevelMax = 0;
            assert( nBoxInputs == (int)pDelayTable[1] );
520
            for ( j = 0; j < nBoxInputs && (pObjIn = Gia_ManCo(p, curCo + j)); j++ )
521 522 523 524
                if ( (int)pDelayTable[3+k*nBoxInputs+j] != -ABC_INFINITY )
                    LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + ((int)pDelayTable[3+k*nBoxInputs+j] / nAnd2Delay) );
            // set box output level
            Gia_ObjSetLevel( p, pObj, LevelMax );
525
        }
526 527
        curCo += nBoxInputs;
        curCi += nBoxOutputs;
528 529 530
    }
    // add remaining nodes
    p->nLevels = 0;
Alan Mishchenko committed
531
    for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
532
    {
533
        pObj = Gia_ManCo( p, i );
534 535 536 537
        Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) );
        Gia_ObjSetCoLevel( p, pObj );
        p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
    }
538 539
    curCo += Tim_ManPoNum(pManTime);
    // verify counts
540 541
    assert( curCi == Gia_ManCiNum(p) );
    assert( curCo == Gia_ManCoNum(p) );
542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589
//    printf( "Max level is %d.\n", p->nLevels );
    return p->nLevels;
}

/**Function*************************************************************

  Synopsis    [Computes level with boxes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManLutLevelWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
    int iObj, k, iFan, Level = 0;
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return 0;
    Gia_ObjSetTravIdCurrent(p, pObj);
    if ( Gia_ObjIsCi(pObj) )
        return 1;
    assert( Gia_ObjIsAnd(pObj) );
    iObj = Gia_ObjId( p, pObj );
    Gia_LutForEachFanin( p, iObj, iFan, k )
    {
        if ( Gia_ManLutLevelWithBoxes_rec( p, Gia_ManObj(p, iFan) ) )
            return 1;
        Level = Abc_MaxInt( Level, Gia_ObjLevelId(p, iFan) );
    }
    Gia_ObjSetLevelId( p, iObj, Level + 1 );
    return 0;
}
int Gia_ManLutLevelWithBoxes( Gia_Man_t * p )
{
//    int nAnd2Delay = p->nAnd2Delay ? p->nAnd2Delay : 1;
    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
    Gia_Obj_t * pObj, * pObjIn;
    int i, k, j, curCi, curCo, LevelMax;
    assert( Gia_ManRegNum(p) == 0 );
    // copy const and real PIs
    Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
    Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 );
    Gia_ManIncrementTravId( p );
    Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
    for ( i = 0; i < Tim_ManPiNum(pManTime); i++ )
    {
590
        pObj = Gia_ManCi( p, i );
591 592 593 594 595 596 597 598 599 600 601 602 603 604 605
//        Gia_ObjSetLevel( p, pObj, Tim_ManGetCiArrival(pManTime, i) / nAnd2Delay );
        Gia_ObjSetLevel( p, pObj, 0 );
        Gia_ObjSetTravIdCurrent( p, pObj );
    }
    // create logic for each box
    curCi = Tim_ManPiNum(pManTime);
    curCo = 0;
    for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
    {
        int nBoxInputs  = Tim_ManBoxInputNum( pManTime, i );
        int nBoxOutputs = Tim_ManBoxOutputNum( pManTime, i );
        float * pDelayTable = Tim_ManBoxDelayTable( pManTime, i );
        // compute level for TFI of box inputs
        for ( k = 0; k < nBoxInputs; k++ )
        {
606
            pObj = Gia_ManCo( p, curCo + k );
607 608 609 610 611 612 613 614 615 616 617
            if ( Gia_ManLutLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ) )
            {
                printf( "Boxes are not in a topological order. Switching to level computation without boxes.\n" );
                return Gia_ManLevelNum( p );
            }
            // set box input level
            Gia_ObjSetCoLevel( p, pObj );
        }
        // compute level for box outputs
        for ( k = 0; k < nBoxOutputs; k++ )
        {
618
            pObj = Gia_ManCi( p, curCi + k );
619 620 621 622
            Gia_ObjSetTravIdCurrent( p, pObj );
            // evaluate delay of this output
            LevelMax = 0;
            assert( nBoxInputs == (int)pDelayTable[1] );
623
            for ( j = 0; j < nBoxInputs && (pObjIn = Gia_ManCo(p, curCo + j)); j++ )
624 625 626 627 628 629 630 631 632 633 634 635 636
                if ( (int)pDelayTable[3+k*nBoxInputs+j] != -ABC_INFINITY )
//                    LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + ((int)pDelayTable[3+k*nBoxInputs+j] / nAnd2Delay) );
                    LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + 1 );
            // set box output level
            Gia_ObjSetLevel( p, pObj, LevelMax );
        }
        curCo += nBoxInputs;
        curCi += nBoxOutputs;
    }
    // add remaining nodes
    p->nLevels = 0;
    for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
    {
637
        pObj = Gia_ManCo( p, i );
638 639 640 641
        Gia_ManLutLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) );
        Gia_ObjSetCoLevel( p, pObj );
        p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
    }
Alan Mishchenko committed
642
    curCo += Tim_ManPoNum(pManTime);
643
    // verify counts
644 645
    assert( curCi == Gia_ManCiNum(p) );
    assert( curCo == Gia_ManCoNum(p) );
646 647 648 649 650 651
//    printf( "Max level is %d.\n", p->nLevels );
    return p->nLevels;
}

/**Function*************************************************************

652 653 654 655 656 657 658 659 660 661 662 663 664
  Synopsis    [Update hierarchy/timing manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void * Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres )
{
    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
    assert( pManTime != NULL );
665
    assert( Vec_IntSize(vBoxPres) == Tim_ManBoxNum(pManTime) );
666 667
    return Tim_ManTrim( pManTime, vBoxPres );
}
668
void * Gia_ManUpdateTimMan2( Gia_Man_t * p, Vec_Int_t * vBoxesLeft, int nTermsDiff )
669 670 671 672
{
    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
    assert( pManTime != NULL );
    assert( Vec_IntSize(vBoxesLeft) <= Tim_ManBoxNum(pManTime) );
673
    return Tim_ManReduce( pManTime, vBoxesLeft, nTermsDiff );
674
}
675 676 677 678 679 680 681 682 683 684 685 686 687 688

/**Function*************************************************************

  Synopsis    [Update AIG of the holes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * p, Vec_Int_t * vBoxPres )
{
689
    Gia_Man_t * pNew;
690 691 692 693 694 695 696 697 698 699 700 701
    Tim_Man_t * pManTime = (Tim_Man_t *)pTime;
    Vec_Int_t * vOutPres = Vec_IntAlloc( 100 );
    int i, k, curPo = 0;
    assert( Vec_IntSize(vBoxPres) == Tim_ManBoxNum(pManTime) );
    assert( Gia_ManCoNum(p) == Tim_ManCiNum(pManTime) - Tim_ManPiNum(pManTime) );
    for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
    {
        for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
            Vec_IntPush( vOutPres, Vec_IntEntry(vBoxPres, i) );
        curPo += Tim_ManBoxOutputNum(pManTime, i);
    }
    assert( curPo == Gia_ManCoNum(p) );
702
    pNew = Gia_ManDupOutputVec( p, vOutPres );
703 704 705
    Vec_IntFree( vOutPres );
    return pNew;
}
706 707 708 709 710
Gia_Man_t * Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * p, Vec_Int_t * vBoxesLeft )
{
    Gia_Man_t * pNew;
    Tim_Man_t * pManTime = (Tim_Man_t *)pTime;
    int nRealPis = Tim_ManPiNum(pManTime);
711
    Vec_Int_t * vOutsLeft = Vec_IntAlloc( 100 );
712
    int i, k, iBox, iOutFirst;
713
    assert( Vec_IntSize(vBoxesLeft) <= Tim_ManBoxNum(pManTime) );
714 715 716 717 718 719 720 721 722 723 724
    assert( Gia_ManCoNum(p) == Tim_ManCiNum(pManTime) - nRealPis );
    Vec_IntForEachEntry( vBoxesLeft, iBox, i )
    {
        iOutFirst = Tim_ManBoxOutputFirst(pManTime, iBox) - nRealPis;
        for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, iBox); k++ )
            Vec_IntPush( vOutsLeft, iOutFirst + k );
    }
    pNew = Gia_ManDupSelectedOutputs( p, vOutsLeft );
    Vec_IntFree( vOutsLeft );
    return pNew;
}
725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751

/**Function*************************************************************

  Synopsis    [Computes AIG with boxes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManDupCollapse_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew )
{
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return;
    Gia_ObjSetTravIdCurrent(p, pObj);
    assert( Gia_ObjIsAnd(pObj) );
    if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
        Gia_ManDupCollapse_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)), pNew );
    Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
    Gia_ManDupCollapse_rec( p, Gia_ObjFanin1(pObj), pNew );
//    assert( !~pObj->Value );
    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
    if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
        pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))->Value);        
}
752
Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres, int fSeq )
753
{
754
    // this procedure assumes that sequential AIG with boxes is unshuffled to have valid boxes
755 756 757
    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj, * pObjBox;
758
    int i, k, curCi, curCo, nBBins = 0, nBBouts = 0;
759
    assert( !fSeq || p->vRegClasses );
760
    //assert( Gia_ManRegNum(p) == 0 );
761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788
    assert( Gia_ManCiNum(p) == Tim_ManPiNum(pManTime) + Gia_ManCoNum(pBoxes) );
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    if ( Gia_ManHasChoices(p) )
        pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) );
    Gia_ManHashAlloc( pNew );
    // copy const and real PIs
    Gia_ManFillValue( p );
    Gia_ManConst0(p)->Value = 0;
    Gia_ManIncrementTravId( p );
    Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
    for ( i = 0; i < Tim_ManPiNum(pManTime); i++ )
    {
        pObj = Gia_ManCi( p, i );
        pObj->Value = Gia_ManAppendCi(pNew);
        Gia_ObjSetTravIdCurrent( p, pObj );
    }
    // create logic for each box
    curCi = Tim_ManPiNum(pManTime);
    curCo = 0;
    for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
    {
        // clean boxes
        Gia_ManIncrementTravId( pBoxes );
        Gia_ObjSetTravIdCurrent( pBoxes, Gia_ManConst0(pBoxes) );
        Gia_ManConst0(pBoxes)->Value = 0;
        // add internal nodes
789
        //printf( "%d ", Tim_ManBoxIsBlack(pManTime, i) );
790 791 792 793 794 795 796 797
        if ( Tim_ManBoxIsBlack(pManTime, i) )
        {
            int fSkip = (vBoxPres != NULL && !Vec_IntEntry(vBoxPres, i));
            for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
            {
                pObj = Gia_ManCo( p, curCo + k );
                Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
                pObj->Value = fSkip ? -1 : Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
798
                nBBouts++;
799 800 801 802 803 804
            }
            for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
            {
                pObj = Gia_ManCi( p, curCi + k );
                pObj->Value = fSkip ? 0 : Gia_ManAppendCi(pNew);
                Gia_ObjSetTravIdCurrent( p, pObj );
805
                nBBins++;
806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833
            }
        }
        else
        {
            for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
            {
                // build logic
                pObj = Gia_ManCo( p, curCo + k );
                Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
                // transfer to the PI
                pObjBox = Gia_ManCi( pBoxes, k );
                pObjBox->Value = Gia_ObjFanin0Copy(pObj);
                Gia_ObjSetTravIdCurrent( pBoxes, pObjBox );
            }
            for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
            {
                // build logic
                pObjBox = Gia_ManCo( pBoxes, curCi - Tim_ManPiNum(pManTime) + k );
                Gia_ManDupCollapse_rec( pBoxes, Gia_ObjFanin0(pObjBox), pNew );
                // transfer to the PI
                pObj = Gia_ManCi( p, curCi + k );
                pObj->Value = Gia_ObjFanin0Copy(pObjBox);
                Gia_ObjSetTravIdCurrent( p, pObj );
            }
        }
        curCo += Tim_ManBoxInputNum(pManTime, i);
        curCi += Tim_ManBoxOutputNum(pManTime, i);
    }
834
    //printf( "\n" );
835 836 837 838 839 840 841 842 843 844 845
    // add remaining nodes
    for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
    {
        pObj = Gia_ManCo( p, i );
        Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    }
    curCo += Tim_ManPoNum(pManTime);
    // verify counts
    assert( curCi == Gia_ManCiNum(p) );
    assert( curCo == Gia_ManCoNum(p) );
846
    Gia_ManSetRegNum( pNew, (fSeq && p->vRegClasses) ? Vec_IntSize(p->vRegClasses) : Gia_ManRegNum(p) );
847 848 849 850
    Gia_ManHashStop( pNew );
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManCleanupRemap( p, pTemp );
    Gia_ManStop( pTemp );
851 852
    assert( Tim_ManPoNum(pManTime) == Gia_ManCoNum(pNew) - nBBouts );
    assert( Tim_ManPiNum(pManTime) == Gia_ManCiNum(pNew) - nBBins );
853
    // implement initial state if given
854
    if ( fSeq && p->vRegInits && Vec_IntSum(p->vRegInits) )
855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874
    {
        char * pInit = ABC_ALLOC( char, Vec_IntSize(p->vRegInits) + 1 );
        Gia_Obj_t * pObj;
        int i;
        assert( Vec_IntSize(p->vRegInits) == Gia_ManRegNum(pNew) );
        Gia_ManForEachRo( pNew, pObj, i )
        {
            if ( Vec_IntEntry(p->vRegInits, i) == 0 )
                pInit[i] = '0';
            else if ( Vec_IntEntry(p->vRegInits, i) == 1 )
                pInit[i] = '1';
            else 
                pInit[i] = 'X';
        }
        pInit[i] = 0;
        pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 1 );
        pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
        Gia_ManStop( pTemp );
        ABC_FREE( pInit );
    }
875 876 877 878 879
    return pNew;
}

/**Function*************************************************************

880
  Synopsis    [Verify XAIG against its spec.]
881 882 883 884 885 886 887 888

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
889
int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fVerbose, char * pFileSpec )
890 891 892
{
    int Status   = -1;
    Gia_Man_t * pSpec, * pGia0, * pGia1, * pMiter;
893
    Vec_Int_t * vBoxPres = NULL;
894
    if ( pFileSpec == NULL && pGia->pSpec == NULL )
895 896 897 898
    {
        printf( "Spec file is not given. Use standard flow.\n" );
        return Status;
    }
899
    if ( Gia_ManBoxNum(pGia) && pGia->pAigExtra == NULL )
900 901 902 903 904
    {
        printf( "Design has no box logic. Use standard flow.\n" );
        return Status;
    }
    // read original AIG
905
    pSpec = Gia_AigerRead( pFileSpec ? pFileSpec : pGia->pSpec, 0, 0 );
906
    if ( Gia_ManBoxNum(pSpec) && pSpec->pAigExtra == NULL )
907
    {
908 909
        Gia_ManStop( pSpec );
        printf( "Spec has no box logic. Use standard flow.\n" );
910 911
        return Status;
    }
912 913
    // prepare miter
    if ( pGia->pManTime == NULL && pSpec->pManTime == NULL )
914
    {
915 916
        pGia0 = Gia_ManDup( pSpec );
        pGia1 = Gia_ManDup( pGia );
917
    }
918
    else
919
    {
920 921 922
        // if timing managers have different number of black boxes,
        // it is possible that some of the boxes are swept away
        if ( pSpec->pManTime && Tim_ManBlackBoxNum((Tim_Man_t *)pSpec->pManTime) > 0 && Gia_ManBoxNum(pGia) > 0 )
923
        {
924 925
            // specification cannot have fewer boxes than implementation
            if ( Gia_ManBoxNum(pSpec) < Gia_ManBoxNum(pGia) )
926
            {
927
                printf( "Spec has less boxes than the design. Cannot proceed.\n" );
928 929
                return Status;
            }
930 931 932 933 934 935 936 937 938 939
            // to align the boxes, find what boxes of pSpec are dropped in pGia
            if ( Gia_ManBoxNum(pSpec) > Gia_ManBoxNum(pGia) )
            {
                vBoxPres = Tim_ManAlignTwo( (Tim_Man_t *)pSpec->pManTime, (Tim_Man_t *)pGia->pManTime );
                if ( vBoxPres == NULL )
                {
                    printf( "Boxes of spec and design cannot be aligned. Cannot proceed.\n" );
                    return Status;
                }
            }
940
        }
941 942
        // collapse two designs
        if ( Gia_ManBoxNum(pSpec) > 0 )
943
            pGia0 = Gia_ManDupCollapse( pSpec, pSpec->pAigExtra, vBoxPres, fSeq );
944 945 946
        else
            pGia0 = Gia_ManDup( pSpec );
        if ( Gia_ManBoxNum(pGia) > 0 )
947
            pGia1 = Gia_ManDupCollapse( pGia,  pGia->pAigExtra,  NULL, fSeq  );
948 949 950
        else
            pGia1 = Gia_ManDup( pGia );
        Vec_IntFreeP( &vBoxPres );
951
    }
952
    // compute the miter
953 954 955 956 957 958 959 960
    if ( fSeq )
    {
        pMiter = Gia_ManMiter( pGia0, pGia1, 0, 0, 1, 0, fVerbose );
        if ( pMiter )
        {
            Aig_Man_t * pMan;
            Fra_Sec_t SecPar, * pSecPar = &SecPar;
            Fra_SecSetDefaultParams( pSecPar );
961
            pSecPar->fRetimeFirst = 0;
962 963 964 965 966 967 968 969 970 971
            pSecPar->nBTLimit  = nBTLimit;
            pSecPar->TimeLimit = nTimeLim;
            pSecPar->fVerbose  = fVerbose;
            pMan = Gia_ManToAig( pMiter, 0 );
            Gia_ManStop( pMiter );
            Status = Fra_FraigSec( pMan, pSecPar, NULL );
            Aig_ManStop( pMan );
        }
    }
    else
972
    {
973 974 975 976 977 978 979 980 981 982 983 984 985
        pMiter = Gia_ManMiter( pGia0, pGia1, 0, 1, 0, 0, fVerbose );
        if ( pMiter )
        {
            Cec_ParCec_t ParsCec, * pPars = &ParsCec;
            Cec_ManCecSetDefaultParams( pPars );
            pPars->nBTLimit  = nBTLimit;
            pPars->TimeLimit = nTimeLim;
            pPars->fVerbose  = fVerbose;
            Status = Cec_ManVerify( pMiter, pPars );
            if ( pPars->iOutFail >= 0 )
                Abc_Print( 1, "Verification failed for at least one output (%d).\n", pPars->iOutFail );
            Gia_ManStop( pMiter );
        }
986 987 988 989 990 991 992 993 994 995 996 997 998 999
    }
    Gia_ManStop( pGia0 );
    Gia_ManStop( pGia1 );
    Gia_ManStop( pSpec );
    return Status;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END