abc/src/proof/acec/acecFadds.c
// computes AIG delay information when boxes are used
computes AIG delay information when boxes are used
computes AIG delay information when boxes are used
int Gia_ManFindAnnotatedDelay( Gia_Man_t * p, int DelayC, int * pnBoxes, int fIgnoreBoxDelays )
{
    Gia_Obj_t * pObj;
    int nRealPis = Gia_ManBoxNum(p) ? Tim_ManPiNum((Tim_Man_t *)p->pManTime) : Gia_ManCiNum(p);
    int * pDelays = Vec_IntArray(p->vLevels);
    int i, k, iBox, iBoxOutId, Delay, Delay0, Delay1, DelayMax = 0, nBoxes = 0;
    Vec_IntFill( p->vLevels, Gia_ManObjNum(p), 0 );
    Gia_ManForEachObj1( p, pObj, i )
    {
        if ( Gia_ObjIsCi(pObj) )
        {
            if ( fIgnoreBoxDelays )
                continue;
            iBoxOutId = Gia_ObjCioId(pObj) - nRealPis;
            if ( iBoxOutId < 0 )
                continue;
            iBox = iBoxOutId / 2;
            assert( iBox < Gia_ManBoxNum(p) );
            Delay = 0;
            for ( k = 0; k < 3; k++ )
            {
                int Id = Gia_ObjId( p, Gia_ManCo(p, iBox*3+k) );
                assert( Id < i );
                Delay = Abc_MaxInt( Delay, pDelays[Id] );
            }
            if ( iBoxOutId & 1 ) 
                Delay += DelayC;
            else 
                Delay += 100;
            pDelays[i] = Delay;
            continue;
        }
        if ( Gia_ObjIsCo(pObj) )
        {
            pDelays[i] = pDelays[Gia_ObjFaninId0(pObj, i)];
            DelayMax = Abc_MaxInt( DelayMax, pDelays[i] );
            continue;
        }
        assert( !pObj->fMark0 || !pObj->fMark1 );
        Delay0 = pDelays[Gia_ObjFaninId0(pObj, i)];
        Delay1 = pDelays[Gia_ObjFaninId1(pObj, i)];
        if ( pObj->fMark0 )
        {
            Delay = Abc_MaxInt( Delay0 + DelayC, Delay1 + 100 );
            nBoxes++;
        }
        else if ( pObj->fMark1 )
        {
            Delay = Abc_MaxInt( Delay1 + DelayC, Delay0 + 100 );
            nBoxes++;
        }
        else
            Delay = Abc_MaxInt( Delay0 + 100, Delay1 + 100 );
        pDelays[i] = Delay;
    }
    if ( pnBoxes )
        *pnBoxes = nBoxes;
    return DelayMax;
}
int Gia_ManFindAnnotatedDelay ( Gia_Man_t * p , int DelayC , int * pnBoxes , int fIgnoreBoxDelays ) { Gia_Obj_t * pObj ; int nRealPis = Gia_ManBoxNum ( p ) ? Tim_ManPiNum ( ( Tim_Man_t * ) p -> pManTime ) : Gia_ManCiNum ( p ) ; int * pDelays = Vec_IntArray ( p -> vLevels ) ; int i , k , iBox , iBoxOutId , Delay , Delay0 , Delay1 , DelayMax = 0 , nBoxes = 0 ; Vec_IntFill ( p -> vLevels , Gia_ManObjNum ( p ) , 0 ) ; Gia_ManForEachObj1 ( p , pObj , i ) { if ( Gia_ObjIsCi ( pObj ) ) { if ( fIgnoreBoxDelays ) continue ; iBoxOutId = Gia_ObjCioId ( pObj ) - nRealPis ; if ( iBoxOutId < 0 ) continue ; iBox = iBoxOutId / 2 ; assert ( iBox < Gia_ManBoxNum ( p ) ) ; Delay = 0 ; for ( k = 0 ; k < 3 ; k ++ ) { int Id = Gia_ObjId ( p , Gia_ManCo ( p , iBox * 3 + k ) ) ; assert ( Id < i ) ; Delay = Abc_MaxInt ( Delay , pDelays [ Id ] ) ; } if ( iBoxOutId & 1 ) Delay += DelayC ; else Delay += 100 ; pDelays [ i ] = Delay ; continue ; } if ( Gia_ObjIsCo ( pObj ) ) { pDelays [ i ] = pDelays [ Gia_ObjFaninId0 ( pObj , i ) ] ; DelayMax = Abc_MaxInt ( DelayMax , pDelays [ i ] ) ; continue ; } assert ( ! pObj -> fMark0 || ! pObj -> fMark1 ) ; Delay0 = pDelays [ Gia_ObjFaninId0 ( pObj , i ) ] ; Delay1 = pDelays [ Gia_ObjFaninId1 ( pObj , i ) ] ; if ( pObj -> fMark0 ) { Delay = Abc_MaxInt ( Delay0 + DelayC , Delay1 + 100 ) ; nBoxes ++ ; } else if ( pObj -> fMark1 ) { Delay = Abc_MaxInt ( Delay1 + DelayC , Delay0 + 100 ) ; nBoxes ++ ; } else Delay = Abc_MaxInt ( Delay0 + 100 , Delay1 + 100 ) ; pDelays [ i ] = Delay ; } if ( pnBoxes ) * pnBoxes = nBoxes ; return DelayMax ; }
computes AIG delay information when boxes are used
computes AIG delay information when boxes are used
// check if it is real PI // if it is a box output, find box number // check find the maximum delay of the box inputs // consider outputs // carry output // sum output