From 2e3384390a6cc4896bbaeb3453995abfafa0b9bc Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 7 Oct 2024 14:10:02 +0700 Subject: [PATCH] Updating "lutexact" to run on symmetric functions. --- src/base/abci/abc.c | 23 +++++++++++++++++++---- src/sat/bmc/bmc.h | 3 ++- src/sat/bmc/bmcMaj.c | 14 +++++++++++++- src/sat/bmc/bmcMaj2.c | 14 +++++++++++++- 4 files changed, 47 insertions(+), 7 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3c560b71e..dce8cec1f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -9810,7 +9810,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, "INKTiaocgvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INKTSiaocgvh" ) ) != EOF ) { switch ( c ) { @@ -9858,6 +9858,15 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->RuntimeLim < 0 ) goto usage; break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by a file name.\n" ); + goto usage; + } + pPars->pSymStr = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'i': pPars->fUseIncr ^= 1; break; @@ -9884,16 +9893,21 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( argc == globalUtilOptind + 1 ) pPars->pTtStr = argv[globalUtilOptind]; - if ( pPars->pTtStr == NULL ) + if ( pPars->pTtStr == NULL && pPars->pSymStr == 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) ) + if ( pPars->pTtStr && (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->pSymStr && pPars->nVars+1 != strlen(pPars->pSymStr) ) + { + Abc_Print( -1, "The char string of the %d-variable symmetric function should have %d zeros and ones (instead of %d).\n", pPars->nVars, pPars->nVars+1, strlen(pPars->pSymStr) ); + 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 ); @@ -9916,12 +9930,13 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutexact [-INKT ] [-iaocgvh] \n" ); + Abc_Print( -2, "usage: lutexact [-INKT ] [-S string] [-iaocgvh] \n" ); Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" ); Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N : the number of K-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-K : the number of node fanins [default = %d]\n", pPars->nLutSize ); Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); + Abc_Print( -2, "\t-S : charasteristic string of a symmetric function [default = %d]\n", pPars->pSymStr ); 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" ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 795296e6f..11578a56b 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -66,6 +66,7 @@ struct Bmc_EsPar_t_ int RuntimeLim; int fVerbose; char * pTtStr; + char * pSymStr; }; static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars ) @@ -88,7 +89,7 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars ) pPars->fUniqFans = 0; pPars->fLutCascade = 0; pPars->RuntimeLim = 0; - pPars->fVerbose = 1; + pPars->fVerbose = 0; } diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index b6ff80a58..f89d74ea1 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -1504,7 +1504,17 @@ void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ) int i, status, iMint = 1; abctime clkTotal = Abc_Clock(); Exa3_Man_t * p; int fCompl = 0; - word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr ); + word pTruth[16]; + 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 ); + Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars ); + printf( "Generated symmetric function: %s\n", pPars->pTtStr ); + ABC_FREE( pFun ); + } + if ( pPars->pTtStr ) + Abc_TtReadHex( pTruth, pPars->pTtStr ); + else assert( 0 ); assert( pPars->nVars <= 10 ); assert( pPars->nLutSize <= 6 ); p = Exa3_ManAlloc( pPars, pTruth ); @@ -1541,6 +1551,8 @@ void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ) Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); if ( iMint == -1 ) Exa3_ManDumpBlif( p, fCompl ); + if ( pPars->pSymStr ) + ABC_FREE( pPars->pTtStr ); Exa3_ManFree( p ); } diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c index 8becc6321..665b61611 100644 --- a/src/sat/bmc/bmcMaj2.c +++ b/src/sat/bmc/bmcMaj2.c @@ -1387,7 +1387,17 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars ) int i, status, iMint = 1; abctime clkTotal = Abc_Clock(); Exa3_Man_t * p; int fCompl = 0; - word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr ); + word pTruth[16]; + 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 ); + Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars ); + printf( "Generated symmetric function: %s\n", pPars->pTtStr ); + ABC_FREE( pFun ); + } + if ( pPars->pTtStr ) + Abc_TtReadHex( pTruth, pPars->pTtStr ); + else assert( 0 ); assert( pPars->nVars <= 10 ); assert( pPars->nLutSize <= 6 ); p = Exa3_ManAlloc( pPars, pTruth ); @@ -1422,6 +1432,8 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars ) Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); if ( iMint == -1 ) Exa3_ManDumpBlif( p, fCompl ); + if ( pPars->pSymStr ) + ABC_FREE( pPars->pTtStr ); Exa3_ManFree( p ); }