src/base/abci/abcBmc.c

Go to the documentation of this file.

#include "abc.h"
#include "ivy.h"


extern Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc );

static void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig, Vec_Ptr_t * vMapping, int nFrames );


void Abc_NtkBmc( Abc_Ntk_t * pNtk, int nFrames, int fInit, int fVerbose )
{
    Ivy_FraigParams_t Params, * pParams = &Params; 
    Ivy_Man_t * pMan, * pFrames, * pFraig;
    Vec_Ptr_t * vMapping;
    // convert to IVY manager
    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
    // generate timeframes
    pFrames = Ivy_ManFrames( pMan, Abc_NtkLatchNum(pNtk), nFrames, fInit, &vMapping );
    // fraig the timeframes
    Ivy_FraigParamsDefault( pParams );
    pParams->nBTLimitNode = ABC_INFINITY;
    pParams->fVerbose = 0;
    pParams->fProve = 0;
    pFraig = Ivy_FraigPerform( pFrames, pParams );
printf( "Frames have %6d nodes.  ", Ivy_ManNodeNum(pFrames) );
printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) );
    // report the classes
//    if ( fVerbose )
//        Abc_NtkBmcReport( pMan, pFrames, pFraig, vMapping, nFrames );
    // free stuff
    Vec_PtrFree( vMapping );
    Ivy_ManStop( pFraig );
    Ivy_ManStop( pFrames );
    Ivy_ManStop( pMan );
}
 
void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig, Vec_Ptr_t * vMapping, int nFrames )
{
    Ivy_Obj_t * pFirst1, * pFirst2, * pFirst3;
    int i, f, nIdMax, Prev2, Prev3;
    nIdMax = Ivy_ManObjIdMax(pMan);
    // check what is the number of nodes in each frame
    Prev2 = Prev3 = 0;
    for ( f = 0; f < nFrames; f++ )
    {
        Ivy_ManForEachNode( pMan, pFirst1, i )
        {
            pFirst2 = Ivy_Regular( Vec_PtrEntry(vMapping, f * nIdMax + pFirst1->Id) );
            if ( Ivy_ObjIsConst1(pFirst2) || pFirst2->Type == 0 )
                continue;
            pFirst3 = Ivy_Regular( pFirst2->pEquiv );
            if ( Ivy_ObjIsConst1(pFirst3) || pFirst3->Type == 0 )
                continue;
            break;
        }
        if ( f )
            printf( "Frame %3d :  Strash = %5d  Fraig = %5d\n", f, pFirst2->Id - Prev2, pFirst3->Id - Prev3 );
        Prev2 = pFirst2->Id;
        Prev3 = pFirst3->Id;   
    }
}

---