Skip to content

A
abc
Commit 7d7ce3ec by Alan Mishchenko
Options

New exact synthesis command 'allexact'.

parent c3dccf30
Showing with 242 additions and 15 deletions
abclib.dsp
......@@ -2031,6 +2031,10 @@ SOURCE=.\src\sat\bmc\bmcMaj2.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcMaj3.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcMaxi.c
# End Source File
# Begin Source File
......
src/base/abci/abc.c
......@@ -152,6 +152,7 @@ static int Abc_CommandBmsPs ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandMajExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTwoExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLutExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAllExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -821,6 +822,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Exact synthesis", "majexact", Abc_CommandMajExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "twoexact", Abc_CommandTwoExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "lutexact", Abc_CommandLutExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "allexact", Abc_CommandAllExact, 0 );
Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 );
Cmd_CommandAdd( pAbc, "Various", "comb", Abc_CommandComb, 1 );
......@@ -8385,7 +8387,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: lutexact [-INK <num>] [-aogvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\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 );
......@@ -8409,6 +8411,173 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Zyx_ManExactSynthesis( Bmc_EsPar_t * pPars );
int c;
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MINKaoegvh" ) ) != EOF )
{
switch ( c )
{
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
pPars->nMajSupp = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nMajSupp < 0 )
goto usage;
break;
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
pPars->nVars = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nVars < 0 )
goto usage;
break;
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
pPars->nNodes = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nNodes < 0 )
goto usage;
break;
case 'K':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLutSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLutSize < 0 )
goto usage;
break;
case 'a':
pPars->fOnlyAnd ^= 1;
break;
case 'o':
pPars->fOrderNodes ^= 1;
break;
case 'e':
pPars->fGenAll ^= 1;
break;
case 'g':
pPars->fGlucose ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pPars->nMajSupp > 0 )
{
if ( pPars->nMajSupp != 5 && pPars->nMajSupp != 7 && pPars->nMajSupp != 9 )
{
Abc_Print( -1, "Currently only support majority with 5, 7 or 9 inputs.\n" );
return 1;
}
pPars->nVars = pPars->nMajSupp;
pPars->nLutSize = 3;
pPars->fMajority = 1;
if ( pPars->nNodes == 0 )
{
if ( pPars->nMajSupp == 5 )
pPars->nNodes = 4;
if ( pPars->nMajSupp == 7 )
pPars->nNodes = 7;
if ( pPars->nMajSupp == 9 )
pPars->nNodes = 10;
}
}
else
{
if ( pPars->nVars == 0 )
{
Abc_Print( -1, "The number of variables (-I num) needs to be specified on the command line.\n" );
return 1;
}
if ( pPars->nNodes == 0 )
{
Abc_Print( -1, "The number of nodes (-N num) needs to be specified on the command line.\n" );
return 1;
}
if ( argc == globalUtilOptind + 1 )
pPars->pTtStr = argv[globalUtilOptind];
if ( pPars->pTtStr == NULL )
{
Abc_Print( -1, "Truth table should be given on the command line.\n" );
return 1;
}
if ( (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) )
{
Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (pPars->nVars-2)), strlen(pPars->pTtStr) );
return 1;
}
}
if ( pPars->nVars > pPars->nNodes * (pPars->nLutSize - 1) + 1 )
{
Abc_Print( -1, "Function with %d variales cannot be implemented with %d %d-input LUTs.\n", pPars->nVars, pPars->nNodes, pPars->nLutSize );
return 1;
}
if ( pPars->nVars > 10 )
{
Abc_Print( -1, "Function should not have more than 10 inputs.\n" );
return 1;
}
if ( pPars->nLutSize > 6 )
{
Abc_Print( -1, "Node size should not be more than 6 inputs.\n" );
return 1;
}
Zyx_ManExactSynthesis( pPars );
return 0;
usage:
Abc_Print( -2, "usage: allexact [-MIKN <num>] [-aoevh] <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-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->fGenAll ? "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" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
Abc_Print( -2, "\t-h : print the command usage\n" );
Abc_Print( -2, "\t<hex> : truth table in hex notation\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pNtkRes;
src/sat/bmc/bmc.h
......@@ -50,8 +50,13 @@ struct Bmc_EsPar_t_
int nVars;
int nNodes;
int nLutSize;
int fGlucose;
int nMajSupp;
int fMajority;
int fEnumSols;
int fOnlyAnd;
int fGlucose;
int fOrderNodes;
int fGenAll;
int fFewerVars;
int fVerbose;
char * pTtStr;
......@@ -59,13 +64,19 @@ struct Bmc_EsPar_t_
static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )
{
pPars->nVars = 5; // when first GC happens (4096) (degree of 2)
pPars->nNodes = 4; // when each next GC happens (5)
pPars->nLutSize = 3; // log difference compared to unique table
pPars->fGlucose = 0; // minimum gain when reodering is not performed
pPars->fOnlyAnd = 0; // minimum gain when reodering is not performed
pPars->fFewerVars = 0; // minimum gain when reodering is not performed
pPars->fVerbose = 1; // verbose output
memset( pPars, 0, sizeof(Bmc_EsPar_t) );
pPars->nVars = 0;
pPars->nNodes = 0;
pPars->nLutSize = 2;
pPars->nMajSupp = 0;
pPars->fMajority = 0;
pPars->fEnumSols = 0;
pPars->fOnlyAnd = 0;
pPars->fGlucose = 0;
pPars->fOrderNodes = 0;
pPars->fGenAll = 0;
pPars->fFewerVars = 0;
pPars->fVerbose = 1;
}
......
src/sat/bmc/bmcMaj.c
......@@ -184,6 +184,7 @@ static inline int Maj_ManFindFanin( Maj_Man_t * p, int i, int k )
}
static inline int Maj_ManEval( Maj_Man_t * p )
{
int fUseMiddle = 1;
static int Flag = 0;
int i, k, iMint; word * pFanins[3];
for ( i = p->nVars + 2; i < p->nObjs; i++ )
......@@ -192,10 +193,27 @@ static inline int Maj_ManEval( Maj_Man_t * p )
pFanins[k] = Maj_ManTruth( p, Maj_ManFindFanin(p, i, k) );
Abc_TtMaj( Maj_ManTruth(p, i), pFanins[0], pFanins[1], pFanins[2], p->nWords );
}
if ( Flag && p->nVars >= 6 )
iMint = Abc_TtFindLastDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
if ( fUseMiddle )
{
iMint = -1;
for ( i = 0; i < (1 << p->nVars); i++ )
{
int nOnes = Abc_TtBitCount16(i);
if ( nOnes < p->nVars/2 || nOnes > p->nVars/2+1 )
continue;
if ( Abc_TtGetBit(Maj_ManTruth(p, p->nObjs), i) == Abc_TtGetBit(Maj_ManTruth(p, p->nObjs-1), i) )
continue;
iMint = i;
break;
}
}
else
iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
{
if ( Flag && p->nVars >= 6 )
iMint = Abc_TtFindLastDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
else
iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
}
//Flag ^= 1;
assert( iMint < (1 << p->nVars) );
return iMint;
......
src/sat/bmc/bmcMaj2.c
......@@ -280,6 +280,7 @@ static inline int Maj_ManFindFanin( Maj_Man_t * p, int i, int k )
}
static inline int Maj_ManEval( Maj_Man_t * p )
{
int fUseMiddle = 1;
static int Flag = 0;
int i, k, iMint; word * pFanins[3];
for ( i = p->nVars + 2; i < p->nObjs; i++ )
......@@ -288,10 +289,27 @@ static inline int Maj_ManEval( Maj_Man_t * p )
pFanins[k] = Maj_ManTruth( p, Maj_ManFindFanin(p, i, k) );
Abc_TtMaj( Maj_ManTruth(p, i), pFanins[0], pFanins[1], pFanins[2], p->nWords );
}
if ( Flag && p->nVars >= 6 )
iMint = Abc_TtFindLastDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
if ( fUseMiddle )
{
iMint = -1;
for ( i = 0; i < (1 << p->nVars); i++ )
{
int nOnes = Abc_TtBitCount16(i);
if ( nOnes < p->nVars/2 || nOnes > p->nVars/2+1 )
continue;
if ( Abc_TtGetBit(Maj_ManTruth(p, p->nObjs), i) == Abc_TtGetBit(Maj_ManTruth(p, p->nObjs-1), i) )
continue;
iMint = i;
break;
}
}
else
iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
{
if ( Flag && p->nVars >= 6 )
iMint = Abc_TtFindLastDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
else
iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
}
//Flag ^= 1;
assert( iMint < (1 << p->nVars) );
return iMint;
......
src/sat/bmc/module.make
......@@ -24,6 +24,7 @@ SRC += src/sat/bmc/bmcBCore.c \
src/sat/bmc/bmcLoad.c \
src/sat/bmc/bmcMaj.c \
src/sat/bmc/bmcMaj2.c \
src/sat/bmc/bmcMaj3.c \
src/sat/bmc/bmcMaxi.c \
src/sat/bmc/bmcMesh.c \
src/sat/bmc/bmcMesh2.c \
......
src/sat/glucose/Glucose.cpp
......@@ -253,6 +253,12 @@ bool Solver::addClause_(vec<Lit>& ps)
else if (value(ps[i]) != l_False && ps[i] != p)
ps[j++] = p = ps[i];
ps.shrink(i - j);
if ( 0 ) {
for ( int i = 0; i < ps.size(); i++ )
printf( "%s%d ", (toInt(ps[i]) & 1) ? "-":"", toInt(ps[i]) >> 1 );
printf( "\n" );
}
if (flag && (certifiedUNSAT)) {
for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment