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

Improving verbose printout of 'sim3' when solving multiple outputs.

This commit is contained in:
Alan Mishchenko 2013-03-30 15:15:26 -07:00
parent be8125f364
commit ca7c801150
2 changed files with 17 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/base/abci/abc.c
View File

@ -17904,7 +17904,7 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
int nWords = 50; int nWords = 50;
int nBinSize = 8; int nBinSize = 8;
int nRounds = 0; int nRounds = 0;
int nRestart = 100; int nRestart = 0;
int nRandSeed = 0; int nRandSeed = 0;
int TimeOut = 0; int TimeOut = 0;
int TimeOutGap = 0; int TimeOutGap = 0;
@ -24884,7 +24884,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
nWords = 50; nWords = 50;
nBinSize = 8; nBinSize = 8;
nRounds = 0; nRounds = 0;
nRestart = 100; nRestart = 0;
nRandSeed = 0; nRandSeed = 0;
TimeOut = 0; TimeOut = 0;
TimeOutGap = 0; TimeOutGap = 0;
@ -25449,7 +25449,7 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
int nWords = 50; int nWords = 50;
int nBinSize = 8; int nBinSize = 8;
int nRounds = 0; int nRounds = 0;
int nRestart = 100; int nRestart = 0;
int nRandSeed = 0; int nRandSeed = 0;
int TimeOut = 0; int TimeOut = 0;
int fMiter = 0; int fMiter = 0;

20
src/proof/ssw/sswRarity.c
View File

@ -965,8 +965,8 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
// if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) ) // if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) )
// return 0; // return 0;
if ( fVerbose ) if ( fVerbose )
Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d restart, %d seed, and %d sec timeout.\n",
nWords, nFrames, nRounds, nRandSeed, TimeOut ); nWords, nFrames, nRounds, nRestart, nRandSeed, TimeOut );
// reset random numbers // reset random numbers
Ssw_RarManPrepareRandom( nSavedSeed ); Ssw_RarManPrepareRandom( nSavedSeed );
@ -1043,12 +1043,20 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
else else
Ssw_RarTransferPatterns( p, p->vInits ); Ssw_RarTransferPatterns( p, p->vInits );
// printout // printout
if ( fVerbose && !fSolveAll ) if ( fVerbose )
{ {
// Abc_Print( 1, "Round %3d: ", r ); if ( fSolveAll )
// Abc_PrintTime( 1, "Time", clock() - clk ); {
Abc_Print( 1, "." ); Abc_Print( 1, "Starts =%6d ", nNumRestart );
Abc_Print( 1, "Rounds =%6d ", nNumRestart * nRestart + ((r==-1)?0:r) );
Abc_Print( 1, "Frames =%6d ", (nNumRestart * nRestart + r) * nFrames );
Abc_Print( 1, "CEX =%6d (%6.2f %%) ", nSolved, 100.0*nSolved/Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
else
Abc_Print( 1, "." );
} }
} }
finish: finish:
if ( nSolved ) if ( nSolved )