From c787e32f86597ffce2080534c1093f02e8c9f8d5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 5 Nov 2024 22:01:07 -0800 Subject: [PATCH] Adding postiive minterm count for random functions generated by "lutexact". --- src/base/abci/abc.c | 16 +++++++++++++--- src/sat/bmc/bmc.h | 1 + src/sat/bmc/bmcMaj.c | 30 ++++++++++++++++++++++-------- 3 files changed, 36 insertions(+), 11 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ec891dea8..428ba2c37 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -9803,14 +9803,14 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) ***********************************************************************/ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Exa3_ManExactSynthesis( 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 ); int c; Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INKTSRiaocgvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INKTSRMiaocgvh" ) ) != EOF ) { switch ( c ) { @@ -9876,6 +9876,15 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nRandFuncs = atoi(argv[globalUtilOptind]); globalUtilOptind++; break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by a file name.\n" ); + goto usage; + } + pPars->nMintNum = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; case 'i': pPars->fUseIncr ^= 1; break; @@ -9943,13 +9952,14 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutexact [-INKTR ] [-S string] [-iaocgvh] \n" ); + Abc_Print( -2, "usage: lutexact [-INKTRM ] [-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-R : the number of random functions to try [default = unused]\n" ); + Abc_Print( -2, "\t-M : the number of positive minterms in the random function [default = unused]\n" ); 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" ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index f39a09726..92fbb7422 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -65,6 +65,7 @@ struct Bmc_EsPar_t_ int fLutCascade; int RuntimeLim; int nRandFuncs; + int nMintNum; int fVerbose; char * pTtStr; char * pSymStr; diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index d03b1aba0..168f7fc55 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -1499,9 +1499,9 @@ void Exa3_ManPrint( Exa3_Man_t * p, int i, int iMint, abctime clk ) printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) ); Abc_PrintTime( 1, "Time", clk ); } -void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ) +int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ) { - int i, status, iMint = 1; + int i, status, Res = 0, iMint = 1; abctime clkTotal = Abc_Clock(); Exa3_Man_t * p; int fCompl = 0; word pTruth[16]; @@ -1542,7 +1542,7 @@ void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ) if ( pPars->fVerbose && status != GLUCOSE_UNDEC ) Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal ); if ( iMint == -1 ) - Exa3_ManPrintSolution( p, fCompl ); + Exa3_ManPrintSolution( p, fCompl ), Res = 1; else if ( status == GLUCOSE_UNDEC ) printf( "The problem timed out after %d sec.\n", pPars->RuntimeLim ); else @@ -1554,21 +1554,35 @@ void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ) if ( pPars->pSymStr ) ABC_FREE( pPars->pTtStr ); Exa3_ManFree( p ); + return Res; } void Exa3_ManExactSynthesisRand( Bmc_EsPar_t * pPars ) { - int i, k, nWords = Abc_TtWordNum(pPars->nVars); + int i, k, nDecs = 0, nWords = Abc_TtWordNum(pPars->nVars); word * pFun = ABC_ALLOC( word, nWords ); - Abc_RandomW(1); + Abc_Random(1); + printf( "\n" ); for ( i = 0; i < pPars->nRandFuncs; i++ ) { - for ( k = 0; k < nWords; k++ ) - pFun[k] = Abc_RandomW(0); + if ( pPars->nMintNum == 0 ) + for ( k = 0; k < nWords; k++ ) + pFun[k] = Abc_RandomW(0); + else { + Abc_TtClear( pFun, nWords ); + for ( k = 0; k < pPars->nMintNum; k++ ) { + int iMint = 0; + do iMint = Abc_Random(0) % (1 << pPars->nVars); + while ( Abc_TtGetBit(pFun, iMint) ); + Abc_TtSetBit( pFun, iMint ); + } + } pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 ); Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars ); printf( "Generated random function: %s\n", pPars->pTtStr ); - Exa3_ManExactSynthesis( pPars ); + nDecs += Exa3_ManExactSynthesis( pPars ); ABC_FREE( pPars->pTtStr ); + printf( "\n" ); } + printf( "Decomposable are %d (out of %d) functions (%.2f %%).\n", nDecs, pPars->nRandFuncs, 100.0*nDecs/pPars->nRandFuncs ); ABC_FREE( pFun ); }