luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Updates for the new BMC engine.

This commit is contained in:
Alan Mishchenko 2013-09-05 16:10:50 -07:00
parent 61126bfba4
commit 92c7c6f7e5
1 changed files with 9 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/sat/bmc/bmcBmcAnd.c
View File

@ -75,7 +75,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
Gia_Man_t * pFrames;
abctime clk = Abc_Clock();
int nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
int i, f, iStart, status = -1, Counter = 0;
int i, f, iStart, status = -1;//, Counter = 0;
p = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose );
for ( f = 0; f < nFramesMax; f++ )
{
@ -89,7 +89,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
if ( pPars->fVerbose )
{
printf( "Frame %4d : PI =%9d. AIG =%9d. Trivally UNSAT. Mem =%6.1f Mb ",
printf( "Frame %4d : PI =%9d. AIG =%9d. Trivally UNSAT. Mem =%7.1f Mb ",
f, Gia_ManPiNum(pFrames), Gia_ManAndNum(pFrames), Gia_ManMemory(pFrames) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
@ -97,13 +97,19 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
}
if ( pPars->fVerbose )
{
printf( "Frame %4d : PI =%9d. AIG =%9d. And =%9d. Mem =%6.1f Mb ",
printf( "Frame %4d : PI =%9d. AIG =%9d. And =%9d. Mem =%7.1f Mb ",
f, Gia_ManPiNum(pFrames), Gia_ManAndNum(pFrames), Gia_ManCountUnmarked(pFrames, iStart), Gia_ManMemory(pFrames) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
// if ( ++Counter == 10 )
// break;
}
// dump unfolded frames
pFrames = Gia_ManCleanup( pFrames );
Gia_AigerWrite( pFrames, "frames.aig", 0, 0 );
printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
Gia_ManStop( pFrames );
// cleanup
Unr_ManFree( p );
return status;
}