summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2018-01-19 14:03:24 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2018-01-19 14:03:24 -0800
commit6274498e0131d650f039c49ee0ed3d3afa6bf766 (patch)
treee21f4bc2d526bc787064ae6d5b1c670e210b0625 /src/base
parentc2b6e03c6100c351533a5e2b4bd0daab4e8a7b06 (diff)
downloadabc-6274498e0131d650f039c49ee0ed3d3afa6bf766.tar.gz
abc-6274498e0131d650f039c49ee0ed3d3afa6bf766.tar.bz2
abc-6274498e0131d650f039c49ee0ed3d3afa6bf766.zip
Updates to exact synthesis commands.
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abc.c30
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" );