diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-02-15 09:36:53 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-02-15 09:36:53 -0800 |
| commit | 2bad26634c6d2fb0d804c10dbc0d269be636c0e1 (patch) | |
| tree | a9e1e968d0214fb768557896d9dffcd1ecd2cc55 /src/sat/bmc | |
| parent | bd45eca406c88e164680657f87457cf198782583 (diff) | |
| download | abc-2bad26634c6d2fb0d804c10dbc0d269be636c0e1.tar.gz abc-2bad26634c6d2fb0d804c10dbc0d269be636c0e1.tar.bz2 abc-2bad26634c6d2fb0d804c10dbc0d269be636c0e1.zip | |
Enabling default no output in &icheck.
Diffstat (limited to 'src/sat/bmc')
| -rw-r--r-- | src/sat/bmc/bmcICheck.c | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c index f404def5..4d70096c 100644 --- a/src/sat/bmc/bmcICheck.c +++ b/src/sat/bmc/bmcICheck.c @@ -206,6 +206,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, assert( nFramesMax > 0 ); assert( Gia_ManRegNum(p) > 0 ); + if ( fVerbose ) printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n", Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) ); @@ -272,10 +273,12 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, fChanges = 1; } // report the results + if ( fVerbose ) printf( "M =%4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ", nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter), Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat), sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) ); + if ( fVerbose ) Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); // count the number of negative literals sat_solver_delete( pSat ); @@ -375,19 +378,23 @@ void Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fRe else assert( 0 ); // report the results //printf( "Round %d: ", o ); + if ( fVerbose ) printf( "I = %4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ", i, (nFramesMax+1) * Gia_ManAndNum(pMiter), Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat), sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) ); + if ( fVerbose ) ABC_PRTr( "Time", Abc_Clock() - clkStart ); fflush( stdout ); } // report the results //printf( "Round %d: ", o ); + if ( fVerbose ) printf( "M = %4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ", nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter), Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat), sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) ); + if ( fVerbose ) Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); fflush( stdout ); @@ -401,6 +408,7 @@ Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int { Vec_Int_t * vLits, * vFlops; int i, f; + if ( fVerbose ) printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n", Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) ); fflush( stdout ); |