src/aig/aig/aigTiming.c

Go to the documentation of this file.

#include "aig.h"



static inline int Aig_ObjReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    assert( p->vLevelR );
    Vec_IntFillExtra( p->vLevelR, pObj->Id + 1, 0 );
    return Vec_IntEntry(p->vLevelR, pObj->Id);
}

static inline void Aig_ObjSetReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj, int LevelR )
{
    assert( p->vLevelR );
    Vec_IntFillExtra( p->vLevelR, pObj->Id + 1, 0 );
    Vec_IntWriteEntry( p->vLevelR, pObj->Id, LevelR );
}

void Aig_ObjClearReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    Aig_ObjSetReverseLevel( p, pObj, 0 );
}

int Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    assert( p->vLevelR );
    return p->nLevelMax + 1 - Aig_ObjReverseLevel(p, pObj);
}

int Aig_ObjReverseLevelNew( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    Aig_Obj_t * pFanout;
    int i, iFanout = -1, LevelCur, Level = 0;
    Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
    {
        LevelCur = Aig_ObjReverseLevel( p, pFanout );
        Level = AIG_MAX( Level, LevelCur );
    }
    return Level + 1;
}

void Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease )
{
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj;
    int i;
    assert( p->pFanData != NULL );
    assert( p->vLevelR == NULL );
    // remember the maximum number of direct levels
    p->nLevelMax = Aig_ManLevels(p) + nMaxLevelIncrease;
    // start the reverse levels
    p->vLevelR = Vec_IntAlloc( 0 );
    Vec_IntFill( p->vLevelR, Aig_ManObjNumMax(p), 0 );
    // compute levels in reverse topological order
    vNodes = Aig_ManDfsReverse( p );
    Vec_PtrForEachEntry( vNodes, pObj, i )
    {
        assert( pObj->fMarkA == 0 );
        Aig_ObjSetReverseLevel( p, pObj, Aig_ObjReverseLevelNew(p, pObj) );
    }
    Vec_PtrFree( vNodes );
}

void Aig_ManStopReverseLevels( Aig_Man_t * p )
{
    assert( p->vLevelR != NULL );
    Vec_IntFree( p->vLevelR );
    p->vLevelR = NULL;
    p->nLevelMax = 0;

}

void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew )
{
    Aig_Obj_t * pFanout, * pTemp;
    int iFanout = -1, LevelOld, Lev, k, m;
    assert( p->pFanData != NULL );
    assert( Aig_ObjIsNode(pObjNew) );
    // allocate level if needed
    if ( p->vLevels == NULL )
        p->vLevels = Vec_VecAlloc( Aig_ManLevels(p) + 8 );
    // check if level has changed
    LevelOld = Aig_ObjLevel(pObjNew);
    if ( LevelOld == Aig_ObjLevelNew(pObjNew) )
        return;
    // start the data structure for level update
    // we cannot fail to visit a node when using this structure because the 
    // nodes are stored by their _old_ levels, which are assumed to be correct
    Vec_VecClear( p->vLevels );
    Vec_VecPush( p->vLevels, LevelOld, pObjNew );
    pObjNew->fMarkA = 1;
    // recursively update level
    Vec_VecForEachEntryStart( p->vLevels, pTemp, Lev, k, LevelOld )
    {
        pTemp->fMarkA = 0;
        assert( Aig_ObjLevel(pTemp) == Lev );
        pTemp->Level = Aig_ObjLevelNew(pTemp);
        // if the level did not change, no need to check the fanout levels
        if ( Aig_ObjLevel(pTemp) == Lev )
            continue;
        // schedule fanout for level update
        Aig_ObjForEachFanout( p, pTemp, pFanout, iFanout, m )
        {
            if ( Aig_ObjIsNode(pFanout) && !pFanout->fMarkA )
            {
                assert( Aig_ObjLevel(pFanout) >= Lev );
                Vec_VecPush( p->vLevels, Aig_ObjLevel(pFanout), pFanout );
                pFanout->fMarkA = 1;
            }
        }
    }
}

void Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew )
{
    Aig_Obj_t * pFanin, * pTemp;
    int LevelOld, LevFanin, Lev, k;
    assert( p->vLevelR != NULL );
    assert( Aig_ObjIsNode(pObjNew) );
    // allocate level if needed
    if ( p->vLevels == NULL )
        p->vLevels = Vec_VecAlloc( Aig_ManLevels(p) + 8 );
    // check if level has changed
    LevelOld = Aig_ObjReverseLevel(p, pObjNew);
    if ( LevelOld == Aig_ObjReverseLevelNew(p, pObjNew) )
        return;
    // start the data structure for level update
    // we cannot fail to visit a node when using this structure because the 
    // nodes are stored by their _old_ levels, which are assumed to be correct
    Vec_VecClear( p->vLevels );
    Vec_VecPush( p->vLevels, LevelOld, pObjNew );
    pObjNew->fMarkA = 1;
    // recursively update level
    Vec_VecForEachEntryStart( p->vLevels, pTemp, Lev, k, LevelOld )
    {
        pTemp->fMarkA = 0;
        LevelOld = Aig_ObjReverseLevel(p, pTemp); 
        assert( LevelOld == Lev );
        Aig_ObjSetReverseLevel( p, pTemp, Aig_ObjReverseLevelNew(p, pTemp) );
        // if the level did not change, to need to check the fanout levels
        if ( Aig_ObjReverseLevel(p, pTemp) == Lev )
            continue;
        // schedule fanins for level update
        pFanin = Aig_ObjFanin0(pTemp);
        if ( Aig_ObjIsNode(pFanin) && !pFanin->fMarkA )
        {
            LevFanin = Aig_ObjReverseLevel( p, pFanin );
            assert( LevFanin >= Lev );
            Vec_VecPush( p->vLevels, LevFanin, pFanin );
            pFanin->fMarkA = 1;
        }
        pFanin = Aig_ObjFanin1(pTemp);
        if ( Aig_ObjIsNode(pFanin) && !pFanin->fMarkA )
        {
            LevFanin = Aig_ObjReverseLevel( p, pFanin );
            assert( LevFanin >= Lev );
            Vec_VecPush( p->vLevels, LevFanin, pFanin );
            pFanin->fMarkA = 1;
        }
    }
}

void Aig_ManVerifyLevel( Aig_Man_t * p )
{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    assert( p->pFanData );
    Aig_ManForEachNode( p, pObj, i )
        if ( Aig_ObjLevel(pObj) != Aig_ObjLevelNew(pObj) )
        {
            printf( "Level of node %6d should be %4d instead of %4d.\n", 
                pObj->Id, Aig_ObjLevelNew(pObj), Aig_ObjLevel(pObj) );
            Counter++;
        }
    if ( Counter )
    printf( "Levels of %d nodes are incorrect.\n", Counter );
}

void Aig_ManVerifyReverseLevel( Aig_Man_t * p )
{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    assert( p->vLevelR );
    Aig_ManForEachNode( p, pObj, i )
        if ( Aig_ObjLevel(pObj) != Aig_ObjLevelNew(pObj) )
        {
            printf( "Reverse level of node %6d should be %4d instead of %4d.\n", 
                pObj->Id, Aig_ObjReverseLevelNew(p, pObj), Aig_ObjReverseLevel(p, pObj) );
            Counter++;
        }
    if ( Counter )
    printf( "Reverse levels of %d nodes are incorrect.\n", Counter );
}

---