diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2018-01-19 14:03:24 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2018-01-19 14:03:24 -0800 |
commit | 6274498e0131d650f039c49ee0ed3d3afa6bf766 (patch) | |
tree | e21f4bc2d526bc787064ae6d5b1c670e210b0625 /src/base/abci/abc.c | |
parent | c2b6e03c6100c351533a5e2b4bd0daab4e8a7b06 (diff) | |
download | abc-6274498e0131d650f039c49ee0ed3d3afa6bf766.tar.gz abc-6274498e0131d650f039c49ee0ed3d3afa6bf766.tar.bz2 abc-6274498e0131d650f039c49ee0ed3d3afa6bf766.zip |
Updates to exact synthesis commands.
Diffstat (limited to 'src/base/abci/abc.c')
-rw-r--r-- | src/base/abci/abc.c | 30 |
1 files changed, 26 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3467008a..2259d3ff 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8299,7 +8299,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INKaogvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INKiaogvh" ) ) != EOF ) { switch ( c ) { @@ -8336,6 +8336,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nLutSize < 0 ) goto usage; break; + case 'i': + pPars->fUseIncr ^= 1; + break; case 'a': pPars->fOnlyAnd ^= 1; break; @@ -8388,11 +8391,12 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutexact [-INK <num>] [-aogvh] <hex>\n" ); + Abc_Print( -2, "usage: lutexact [-INK <num>] [-iaogvh] <hex>\n" ); Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" ); Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-K <num> : the number of node fanins [default = %d]\n", pPars->nLutSize ); + Abc_Print( -2, "\t-i : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" ); Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" ); @@ -8420,7 +8424,7 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MINKaoegvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MINKiaoegvh" ) ) != EOF ) { switch ( c ) { @@ -8468,6 +8472,9 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nLutSize < 0 ) goto usage; break; + case 'i': + pPars->fUseIncr ^= 1; + break; case 'a': pPars->fOnlyAnd ^= 1; break; @@ -8499,6 +8506,7 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nVars = pPars->nMajSupp; pPars->nLutSize = 3; pPars->fMajority = 1; + pPars->fUseIncr = 1; if ( pPars->nNodes == 0 ) { if ( pPars->nMajSupp == 5 ) @@ -8549,16 +8557,30 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Node size should not be more than 6 inputs.\n" ); return 1; } + if ( !pPars->fUseIncr ) + { + if ( pPars->fMajority ) + { + Abc_Print( -1, "Cannot synthesize majority in the non-incremental mode (use \'-i\').\n" ); + return 1; + } + if ( pPars->nLutSize > 3 ) + { + Abc_Print( -1, "Cannot synthesize LUT4 and larger in non-incremental mode (use \'-i\').\n" ); + return 1; + } + } Zyx_ManExactSynthesis( pPars ); return 0; usage: - Abc_Print( -2, "usage: allexact [-MIKN <num>] [-aoevh] <hex>\n" ); + Abc_Print( -2, "usage: allexact [-MIKN <num>] [-iaoevh] <hex>\n" ); Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" ); Abc_Print( -2, "\t-M <num> : the majority support size (overrides -I and -K) [default = %d]\n", pPars->nMajSupp ); Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-K <num> : the number of node fanins [default = %d]\n", pPars->nLutSize ); Abc_Print( -2, "\t-N <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes ); + Abc_Print( -2, "\t-i : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" ); Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); Abc_Print( -2, "\t-o : toggle using node ordering by fanins [default = %s]\n", pPars->fOrderNodes ? "yes" : "no" ); Abc_Print( -2, "\t-e : toggle enumerating all solutions [default = %s]\n", pPars->fEnumSols ? "yes" : "no" ); |