Skip to content

A
abc
Commit 26c0e937 by Alan Mishchenko
Options

Updates for the new BMC engine.

parent 0e256dc2
Showing with 5 additions and 1 deletions
src/sat/bmc/bmcBmcAnd.c
...@@ -717,11 +717,15 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ...@@ -717,11 +717,15 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{ {
Bmc_Mna_t * p; Bmc_Mna_t * p;
int nFramesMax, f, i=0, Lit, status, RetValue = -2; int nFramesMax, f, i=0, Lit, status, RetValue = -2;
abctime clk = Abc_Clock();
p = Bmc_MnaAlloc(); p = Bmc_MnaAlloc();
p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose ); p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose );
nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia); nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
if ( pPars->fVerbose ) if ( pPars->fVerbose )
printf( "Performed unfolding for %d frames.\n", nFramesMax ); {
printf( "Performed unfolding for %d frames. ", nFramesMax );
Abc_PrintTime( 1, "Unfolding time", Abc_Clock() - clk );
}
if ( pPars->fVerbose ) if ( pPars->fVerbose )
Gia_ManPrintStats( p->pFrames, NULL ); Gia_ManPrintStats( p->pFrames, NULL );
for ( f = 0; f < nFramesMax; f++ ) for ( f = 0; f < nFramesMax; f++ )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment