diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-02-15 16:52:32 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-02-15 16:52:32 -0800 |
| commit | d5253839b94fcee4c8fae623591642be773ae498 (patch) | |
| tree | f50e9aa396b392acede0bba5c61b4251de02404f /src/base | |
| parent | d3c42bb96a39d2549bd428378c51e52e21c1e289 (diff) | |
| download | abc-d5253839b94fcee4c8fae623591642be773ae498.tar.gz abc-d5253839b94fcee4c8fae623591642be773ae498.tar.bz2 abc-d5253839b94fcee4c8fae623591642be773ae498.zip | |
Fixing timeout in &icheck.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 924c614d..884c1901 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -4744,18 +4744,18 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->nIndFrames <= 0 ) { Abc_Print( -1, "The number of k-inductive frames is not specified.\n" ); - return 1; + return 0; } if ( pAbc->vIndFlops == NULL ) { Abc_Print( -1, "The set of k-inductive flops is not specified.\n" ); - return 1; + return 0; } if ( Vec_IntSize(pAbc->vIndFlops) != Abc_NtkLatchNum(pNtk) ) { Abc_Print( -1, "The saved flop count (%d) does not match that of the current network (%d).\n", Vec_IntSize(pAbc->vIndFlops), Abc_NtkLatchNum(pNtk) ); - return 1; + return 0; } // modify the current network if ( !Abc_NtkMfsAfterICheck( pNtk, pAbc->nIndFrames, nFramesAdd, pAbc->vIndFlops, pPars ) ) @@ -4763,6 +4763,11 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Resynthesis has failed.\n" ); return 1; } + if ( fUseAllFfs ) + { + pAbc->nIndFrames = 0; + Vec_IntFreeP( &pAbc->vIndFlops ); + } } else { @@ -32989,7 +32994,7 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv ) pAbc->vIndFlops = Bmc_PerformISearch( pAbc->pGia, nFramesMax, nTimeOut, fReverse, fDump, fVerbose ); else Bmc_PerformICheck( pAbc->pGia, nFramesMax, nTimeOut, fEmpty, fVerbose ); - pAbc->nIndFrames = nFramesMax; + pAbc->nIndFrames = pAbc->vIndFlops ? nFramesMax : 0; return 0; usage: |