diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-21 15:09:51 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-21 15:09:51 -0800 |
| commit | 75ee395f916f44fd564deb89b64a2c7e4db081bc (patch) | |
| tree | 523ccee9241dbdf8ee6f171ede366363fc357305 /src/base | |
| parent | ab75993d28e766062dbcfe5c8009e80d74d74121 (diff) | |
| download | abc-75ee395f916f44fd564deb89b64a2c7e4db081bc.tar.gz abc-75ee395f916f44fd564deb89b64a2c7e4db081bc.tar.bz2 abc-75ee395f916f44fd564deb89b64a2c7e4db081bc.zip | |
Implemented additional filtering of equivalences (&srm -sf).
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index eba34d62..1b9d8ab9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -25941,22 +25941,26 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) char pFileName[10], pFileName2[10]; Gia_Man_t * pTemp, * pAux; int c, fVerbose = 0; - int fSpeculate = 1; int fSynthesis = 0; + int fSpeculate = 1; + int fSkipSome = 0; int fDualOut = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "dsrvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "drsfvh" ) ) != EOF ) { switch ( c ) { case 'd': fDualOut ^= 1; break; + case 'r': + fSynthesis ^= 1; + break; case 's': fSpeculate ^= 1; break; - case 'r': - fSynthesis ^= 1; + case 'f': + fSkipSome ^= 1; break; case 'v': fVerbose ^= 1; @@ -25974,7 +25978,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) } sprintf( pFileName, "gsrm%s.aig", fSpeculate? "" : "s" ); sprintf( pFileName2, "gsyn%s.aig", fSpeculate? "" : "s" ); - pTemp = Gia_ManSpecReduce( pAbc->pGia, fDualOut, fSynthesis, fSpeculate, fVerbose ); + pTemp = Gia_ManSpecReduce( pAbc->pGia, fDualOut, fSynthesis, fSpeculate, fSkipSome, fVerbose ); if ( pTemp ) { if ( fSpeculate ) @@ -26004,11 +26008,12 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &srm [-dsrvh]\n" ); + Abc_Print( -2, "usage: &srm [-drsfvh]\n" ); Abc_Print( -2, "\t writes speculatively reduced model into file \"%s\"\n", pFileName ); Abc_Print( -2, "\t-d : toggle creating dual output miter [default = %s]\n", fDualOut? "yes": "no" ); - Abc_Print( -2, "\t-s : toggle using speculation at the internal nodes [default = %s]\n", fSpeculate? "yes": "no" ); Abc_Print( -2, "\t-r : toggle writing reduced network for synthesis [default = %s]\n", fSynthesis? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle using speculation at the internal nodes [default = %s]\n", fSpeculate? "yes": "no" ); + Abc_Print( -2, "\t-f : toggle filtering to remove redundant equivalences [default = %s]\n", fSkipSome? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -26127,7 +26132,7 @@ usage: Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t<miter.aig> : file with the external miter to read\n"); Abc_Print( -2, "\t \n" ); - Abc_Print( -2, "\t The external miter should be generated by &srm -m\n" ); + Abc_Print( -2, "\t The external miter should be generated by &srm -s\n" ); Abc_Print( -2, "\t and (partially) solved by any verification engine(s).\n" ); Abc_Print( -2, "\t The external miter should have as many POs as\n" ); Abc_Print( -2, "\t the number of POs in the current AIG plus\n" ); |