The-OpenROAD-Project/abc
1
0
Fork 0
mirror of https://github.com/The-OpenROAD-Project/abc.git synced 2026-03-12 11:26:17 +08:00
Code Issues Actions Packages Projects Releases Wiki Activity

Updated to "lutexact".

Browse Source
This commit is contained in:
Alan Mishchenko
2025-11-20 13:35:47 -08:00
parent 6490bd7da3
commit 51c5ff3b81
3 changed files with 47 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -10757,6 +10757,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Exa7_ManExactSynthesis( Bmc_EsPar_t * pPars );
extern int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars );
extern int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars );
extern int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars );
extern void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars );
extern void Exa3_ManExactSynthesisRand( Bmc_EsPar_t * pPars );
@@ -10765,7 +10766,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, "NMKTFUSYPiaorfgckdsvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NMKTFUSYPiaorfgckdsmvh" ) ) != EOF )
{
switch ( c )
{
@@ -10890,6 +10891,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
pPars->fSilent ^= 1;
break;
case 'm':
pPars->fMinNodes ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -10966,7 +10970,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] [-iaorfgckdsvh] <hex>\n" );
Abc_Print( -2, "usage: lutexact [-NMKTFUS <num>] [-Y string] [-P string] [-iaorfgckdsmvh] <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 );
@@ -10987,6 +10991,7 @@ usage:
Abc_Print( -2, "\t-k : toggle using Kissat 4.0.2 by Armin Biere [default = %s]\n", pPars->fKissat ? "yes" : "no" );
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-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

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

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

@@ -670,6 +670,9 @@ static int Exa8_ManAddCnf( Exa8_Man_t * p, int iMint )
int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
{
extern int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars );
if ( pPars->fMinNodes )
return Exa8_ManExactSynthesisIter( pPars );
int status = KISSAT_UNDEC;
int Res = 0;
abctime clkTotal = Abc_Clock();
@@ -744,6 +747,7 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
}
else
{
Res = 0;
if ( pPars->RuntimeLim )
printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
}
@@ -757,6 +761,41 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
return Res;
}
int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars )
{
pPars->fMinNodes = 0;
int nNodeMin = (pPars->nVars-2)/(pPars->nLutSize-1) + 1;
int nNodeMax = pPars->nNodes, Result = 0;
int fGenPerm = pPars->pPermStr == NULL;
for ( int n = nNodeMin; n <= nNodeMax; n++ ) {
printf( "\nTrying M = %d:\n", n );
pPars->nNodes = n;
if ( fGenPerm ) {
Vec_Str_t * vStr = Vec_StrAlloc( 100 );
for ( int v = 0; v < pPars->nLutSize; v++ )
Vec_StrPush( vStr, 'a'+v );
int nDupVars = Abc_MaxInt(0, (pPars->nLutSize-1) - (pPars->nVars-pPars->nLutSize));
Vec_StrPush( vStr, '_' );
for ( int v = 0; v < nDupVars; v++ )
Vec_StrPush( vStr, 'a'+v );
for ( int v = 0; v < pPars->nLutSize-1-nDupVars; v++ )
Vec_StrPush( vStr, '*' );
for ( int m = 2; m < pPars->nNodes; m++ ) {
Vec_StrPush( vStr, '_' );
for ( int v = 0; v < pPars->nLutSize-1; v++ )
Vec_StrPush( vStr, '*' );
}
Vec_StrPush( vStr, '\0' );
ABC_FREE( pPars->pPermStr );
pPars->pPermStr = Vec_StrReleaseArray(vStr);
Vec_StrFree( vStr );
}
Result = Exa8_ManExactSynthesis(pPars);
if ( Result != 2 )
break;
}
return Result;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///