diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-09-30 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-09-30 08:01:00 -0700 |
commit | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (patch) | |
tree | de3ffe87c3e17950351e3b7d97fa18318bd5ea9a /src/base/abci/abcBmc.c | |
parent | 7d7e60f2dc84393cd4c5db22d2eaf7b1fb1a79b2 (diff) | |
download | abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.gz abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.bz2 abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.zip |
Version abc70930
Diffstat (limited to 'src/base/abci/abcBmc.c')
-rw-r--r-- | src/base/abci/abcBmc.c | 115 |
1 files changed, 0 insertions, 115 deletions
diff --git a/src/base/abci/abcBmc.c b/src/base/abci/abcBmc.c deleted file mode 100644 index af6d237b..00000000 --- a/src/base/abci/abcBmc.c +++ /dev/null @@ -1,115 +0,0 @@ -/**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 /// -//////////////////////////////////////////////////////////////////////// - - |