diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-03 12:29:15 -0800 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-03 12:29:15 -0800 |
| commit | 40d29e781387fdfbe8fec47e600d57a109fed1d9 (patch) | |
| tree | 7e917217f829f6e361a05cf48ab80e195259dedb | |
| parent | cb603c5ea16c9a4756cf26144c2ae7af9800f5b3 (diff) | |
| download | abc-40d29e781387fdfbe8fec47e600d57a109fed1d9.tar.gz abc-40d29e781387fdfbe8fec47e600d57a109fed1d9.tar.bz2 abc-40d29e781387fdfbe8fec47e600d57a109fed1d9.zip | |
only try scorr on small circuits
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 58 |
1 files changed, 31 insertions, 27 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 5a582663..79da6235 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -1124,34 +1124,38 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) if ( vClauses && pPars->fCheckCombUnsat ) { Pdr_Man_t * pPdr2; - Aig_Man_t * pAigScorr; - Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars; - int nAnds; - clk2 = Abc_Clock(); - - Ssw_ManSetDefaultParams( pScorrPars ); - pScorrPars->fStopWhenGone = 1; - pScorrPars->nFramesK = 1; - pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars ); - assert ( pAigScorr ); - nAnds = Aig_ManAndNum( pAigScorr); - Aig_ManStop( pAigScorr ); - - if ( nAnds == 0 ) - { - if ( pPars->fVerbose ) - Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk2 ); - RetValue = 1; - Gia_ManStop( pGia ); - Vec_IntFree( vPisNew ); - Aig_ManStop( pAig ); - break; - } - else if ( pPars->fVerbose ) - { - Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 ); + if ( Aig_ManAndNum( pAig ) <= 20000 ) + { + Aig_Man_t * pAigScorr; + Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars; + int nAnds; + + clk2 = Abc_Clock(); + + Ssw_ManSetDefaultParams( pScorrPars ); + pScorrPars->fStopWhenGone = 1; + pScorrPars->nFramesK = 1; + pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars ); + assert ( pAigScorr ); + nAnds = Aig_ManAndNum( pAigScorr); + Aig_ManStop( pAigScorr ); + + if ( nAnds == 0 ) + { + if ( pPars->fVerbose ) + Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk2 ); + RetValue = 1; + Gia_ManStop( pGia ); + Vec_IntFree( vPisNew ); + Aig_ManStop( pAig ); + break; + } + else if ( pPars->fVerbose ) + { + Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 ); + } } clk2 = Abc_Clock(); |