luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Extending "lutexact -k" to work with larger functions.

This commit is contained in:
Alan Mishchenko 2025-11-30 19:51:05 -08:00
parent c4b2b5c180
commit 5e58e34f6c
3 changed files with 41 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
src/base/abci/abc.c
View File

@ -10768,7 +10768,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, "NMKTFUSYPiaorfgckdsmvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NMKTFUSYPiaorfgckdsmpvh" ) ) != EOF )
{
switch ( c )
{
@ -10896,6 +10896,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
pPars->fMinNodes ^= 1;
break;
case 'p':
pPars->fUsePerm ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -10945,15 +10948,31 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
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 > 12 )
if ( pPars->fKissat )
{
Abc_Print( -1, "Function should not have more than 12 inputs.\n" );
return 1;
if ( pPars->nVars > 14 )
{
Abc_Print( -1, "Function should not have more than 14 inputs.\n" );
return 1;
}
if ( pPars->nLutSize > 8 )
{
Abc_Print( -1, "Node size should not be more than 8 inputs.\n" );
return 1;
}
}
if ( pPars->nLutSize > 6 )
else
{
Abc_Print( -1, "Node size should not be more than 6 inputs.\n" );
return 1;
if ( pPars->nVars > 12 )
{
Abc_Print( -1, "Function should not have more than 12 inputs.\n" );
return 1;
}
if ( pPars->nLutSize > 6 )
{
Abc_Print( -1, "Node size should not be more than 6 inputs.\n" );
return 1;
}
}
if ( pPars->nRandFuncs ) {
pPars->fGlucose = 1;
@ -10972,7 +10991,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: lutexact [-NMKTFUS <num>] [-Y string] [-P string] [-iaorfgckdsmvh] <hex>\n" );
Abc_Print( -2, "usage: lutexact [-NMKTFUS <num>] [-Y string] [-P string] [-iaorfgckdsmpvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" );
Abc_Print( -2, "\t-N <num> : the number of input variables [default = %d]\n", pPars->nVars );
Abc_Print( -2, "\t-M <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes );
@ -10994,6 +11013,7 @@ usage:
Abc_Print( -2, "\t-d : toggle dumping decomposed networks into BLIF files [default = %s]\n", pPars->fDumpBlif ? "yes" : "no" );
Abc_Print( -2, "\t-s : toggle silent computation (no messages, except when a solution is found) [default = %s]\n", pPars->fSilent ? "yes" : "no" );
Abc_Print( -2, "\t-m : toggle minimum-node solution possibly smaller than \"-M <num>\" [default = %s]\n", pPars->fMinNodes ? "yes" : "no" );
Abc_Print( -2, "\t-p : toggle use specialized permutation when minimizing nodes [default = %s]\n", pPars->fUsePerm ? "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" );

1
src/sat/bmc/bmc.h
View File

@ -68,6 +68,7 @@ struct Bmc_EsPar_t_
int fLutCascade;
int fLutInFixed;
int fMinNodes;
int fUsePerm;
int RuntimeLim;
int nRandFuncs;
int nMintNum;

19
src/sat/bmc/bmcMaj8.c
View File

@ -47,6 +47,7 @@ ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
#define MAJ_NOBJS 64 // Const0 + Const1 + nVars + nNodes
#define MAJ_MAX_LUT 8
typedef struct Exa8_Man_t_ Exa8_Man_t;
struct Exa8_Man_t_
@ -63,7 +64,7 @@ struct Exa8_Man_t_
Vec_Wrd_t * vInfo; // nVars + nNodes + 1
Vec_Bit_t * vUsed2; // bit masks
Vec_Bit_t * vUsed3; // bit masks
int VarMarks[MAJ_NOBJS][6][MAJ_NOBJS]; // variable marks
int VarMarks[MAJ_NOBJS][MAJ_MAX_LUT][MAJ_NOBJS]; // variable marks
int VarVals[MAJ_NOBJS]; // values of the first nVars variables
Vec_Wec_t * vOutLits; // output vars
Vec_Wec_t * vInVars; // input vars
@ -214,6 +215,7 @@ static int Exa8_ManMarkup( Exa8_Man_t * p )
{
int i, k, j;
assert( p->nObjs <= MAJ_NOBJS );
assert( p->nLutSize <= MAJ_MAX_LUT );
// assign functionality variables
p->iVar = 1 + p->LutMask * p->nNodes;
// assign connectivity variables
@ -347,7 +349,7 @@ static inline int Exa8_ManFindFanin( Exa8_Man_t * p, int i, int k )
static inline int Exa8_ManEval( Exa8_Man_t * p )
{
static int Flag = 0;
int i, k, j, iMint; word * pFanins[6];
int i, k, j, iMint; word * pFanins[MAJ_MAX_LUT];
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iVarStart = 1 + p->LutMask*(i - p->nVars);
@ -678,7 +680,11 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
abctime clkTotal = Abc_Clock();
Exa8_Man_t * p;
int fCompl = 0;
word pTruth[64];
assert( pPars->nVars <= 14 );
assert( pPars->nLutSize <= 8 );
int nTruthWords = Abc_TtWordNum( pPars->nVars );
word * pTruth = ABC_CALLOC( word, nTruthWords );
assert( pTruth );
if ( pPars->pSymStr ) {
word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars );
pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
@ -689,8 +695,6 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
if ( pPars->pTtStr )
Abc_TtReadHex( pTruth, pPars->pTtStr );
else assert( 0 );
assert( pPars->nVars <= 12 );
assert( pPars->nLutSize <= 6 );
if ( pPars->fUseIncr && !pPars->fSilent )
printf( "Warning: Ignoring incremental option when using Kissat.\n" );
pPars->fUseIncr = 0;
@ -758,6 +762,7 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
if ( pPars->pSymStr )
ABC_FREE( pPars->pTtStr );
Exa8_ManFree( p );
ABC_FREE( pTruth );
return Res;
}
@ -770,7 +775,7 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars )
for ( int n = nNodeMin; n <= nNodeMax; n++ ) {
printf( "\nTrying M = %d:\n", n );
pPars->nNodes = n;
if ( fGenPerm ) {
if ( !pPars->fUsePerm && fGenPerm ) {
Vec_Str_t * vStr = Vec_StrAlloc( 100 );
for ( int v = 0; v < pPars->nLutSize; v++ )
Vec_StrPush( vStr, 'a'+v );
@ -790,7 +795,7 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars )
pPars->pPermStr = Vec_StrReleaseArray(vStr);
Vec_StrFree( vStr );
}
if ( 0 && fGenPerm ) {
else if ( pPars->fUsePerm && fGenPerm ) {
Vec_Str_t * vStr = Vec_StrAlloc( 100 );
for ( int v = 0; v < pPars->nLutSize; v++ )
Vec_StrPush( vStr, 'a'+v );