diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-28 14:52:51 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-28 14:52:51 -0800 |
| commit | 6119f7068aea9f844ebe9b9dc6126d2883c4fecb (patch) | |
| tree | 5a8defd9c507338643341c8c9d1cfd639e42c3eb /src/base | |
| parent | 39839c3feb11fd6dcf112267f22d94777ab29062 (diff) | |
| download | abc-6119f7068aea9f844ebe9b9dc6126d2883c4fecb.tar.gz abc-6119f7068aea9f844ebe9b9dc6126d2883c4fecb.tar.bz2 abc-6119f7068aea9f844ebe9b9dc6126d2883c4fecb.zip | |
Cumulative update to BDD-based reachability, speeding up &reachm and other changes.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9890dbcf..c055c3ad 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27937,7 +27937,7 @@ usage: Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax ); Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); - Abc_Print( -2, "\t-r : enable dynamic BDD variable reordering [default = %s]\n", pPars->fReorder? "yes": "no" ); + Abc_Print( -2, "\t-r : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" ); Abc_Print( -2, "\t-b : perform backward reachability analysis [default = %s]\n", pPars->fBackward? "yes": "no" ); Abc_Print( -2, "\t-y : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" ); Abc_Print( -2, "\t-z : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" ); @@ -28069,7 +28069,7 @@ usage: Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax ); Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); - Abc_Print( -2, "\t-r : enable dynamic BDD variable reordering [default = %s]\n", pPars->fReorder? "yes": "no" ); + Abc_Print( -2, "\t-r : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" ); Abc_Print( -2, "\t-y : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" ); Abc_Print( -2, "\t-z : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" ); Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); |