diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
commit | 4812c90424dfc40d26725244723887a2d16ddfd9 (patch) | |
tree | b32ace96e7e2d84d586e09ba605463b6f49c3271 /src/base/abci/abcBmc.c | |
parent | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (diff) | |
download | abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.gz abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.bz2 abc-4812c90424dfc40d26725244723887a2d16ddfd9.zip |
Version abc71001
Diffstat (limited to 'src/base/abci/abcBmc.c')
-rw-r--r-- | src/base/abci/abcBmc.c | 115 |
1 files changed, 115 insertions, 0 deletions
diff --git a/src/base/abci/abcBmc.c b/src/base/abci/abcBmc.c new file mode 100644 index 00000000..af6d237b --- /dev/null +++ b/src/base/abci/abcBmc.c @@ -0,0 +1,115 @@ +/**CFile**************************************************************** + + FileName [abcBmc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Performs bounded model check.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +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 ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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; + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |