From 692b0c69081fb88102f314b835321b7a4a1fbead Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 2 May 2025 08:13:20 -0700 Subject: [PATCH] Printout of column multiplicity statistics. --- src/base/abci/abc.c | 2 +- src/base/abci/abcCas.c | 34 ++++++++++++++++++++-------------- src/misc/util/utilBSet.c | 3 ++- src/sat/bmc/bmcMaj.c | 4 ++-- 4 files changed, 25 insertions(+), 18 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c90c2f7d3..a5f22d2fc 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7771,7 +7771,7 @@ int Abc_CommandRunScript( Abc_Frame_t * pAbc, int argc, char ** argv ) strcat( pCommLine, pNumber ); strcat( pCommLine, pSpot+1 ); if ( fVerbose ) - printf( "Iteration %3d : %s\n", c, pCommLine ); + printf( "ITERATION %3d : %s\n", c, pCommLine ); if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), pCommLine) ) { Abc_Print( 1, "Something did not work out with the command \"%s\".\n", pCommLine ); goto usage; diff --git a/src/base/abci/abcCas.c b/src/base/abci/abcCas.c index a2bfea56a..861860d04 100644 --- a/src/base/abci/abcCas.c +++ b/src/base/abci/abcCas.c @@ -656,12 +656,12 @@ void Abc_LutCascadeDerive( word * p, int nVars, int nBVars, int Myu, word * pRem } // performs decomposition of one stage -static inline int Abc_LutCascadeDecStage( char * pGuide, int Iter, Vec_Wrd_t * vFuncs[3], Vec_Int_t * vVarIDs, int nRVars, int nRails, int nLutSize, int fVerbose, Vec_Wrd_t * vCas ) +static inline int Abc_LutCascadeDecStage( char * pGuide, int Iter, Vec_Wrd_t * vFuncs[3], Vec_Int_t * vVarIDs, int nRVars, int nRails, int nLutSize, int fVerbose, Vec_Wrd_t * vCas, int * pMyu ) { - extern word Abc_TtFindBVarsSVars( word * p, int nVars, int nRVars, int nRails, int nLutSize, int fVerbose ); + extern word Abc_TtFindBVarsSVars( word * p, int nVars, int nRVars, int nRails, int nLutSize, int fVerbose, int * pMyu ); assert( Vec_IntSize(vVarIDs) > nLutSize ); assert( Vec_IntSize(vVarIDs) <= 24 ); - word Guide = pGuide ? 0 : Abc_TtFindBVarsSVars( Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVars, nRails, nLutSize, fVerbose ); + word Guide = pGuide ? 0 : Abc_TtFindBVarsSVars( Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVars, nRails, nLutSize, fVerbose, pMyu ); if ( !pGuide && !Guide ) { if ( fVerbose ) printf( "The function is not decomposable with %d rails.\n", nRails ); @@ -716,7 +716,7 @@ static inline int Abc_LutCascadeDecStage( char * pGuide, int Iter, Vec_Wrd_t * v Vec_IntShrink( vVarIDs, nFVars+nSVars+nEVars ); return nEVars; } -word * Abc_LutCascadeDec( char * pGuide, word * pTruth, int nVarsOrig, Vec_Int_t * vVarIDs, int nRails, int nLutSize, int nStages, int fVerbose, int * pnStages ) +word * Abc_LutCascadeDec( char * pGuide, word * pTruth, int nVarsOrig, Vec_Int_t * vVarIDs, int nRails, int nLutSize, int nStages, int fVerbose, int * pnStages, int * pMyu ) { word * pRes = NULL; int i, nRVars = 0, nVars = Vec_IntSize(vVarIDs); Vec_Wrd_t * vFuncs[3] = { Vec_WrdStart(Abc_TtWordNum(nVars)), Vec_WrdAlloc(0), Vec_WrdAlloc(0) }; @@ -724,7 +724,7 @@ word * Abc_LutCascadeDec( char * pGuide, word * pTruth, int nVarsOrig, Vec_Int_t Vec_Wrd_t * vCas = Vec_WrdAlloc( 100 ); Vec_WrdPush( vCas, nVarsOrig ); if ( pnStages ) *pnStages = 0; for ( i = 0; Vec_IntSize(vVarIDs) > nLutSize; i++ ) { - nRVars = Abc_LutCascadeDecStage( pGuide, i, vFuncs, vVarIDs, nRVars, nRails, nLutSize, fVerbose, vCas ); + nRVars = Abc_LutCascadeDecStage( pGuide, i, vFuncs, vVarIDs, nRVars, nRails, nLutSize, fVerbose, vCas, pMyu ); if ( i+2 > nStages ) { printf( "The length of the cascade (%d) exceeds the max allowed number of stages (%d).\n", i+2, nStages ); nRVars = -1; @@ -863,7 +863,7 @@ Abc_Ntk_t * Abc_NtkLutCascade2( Abc_Ntk_t * pNtk, int nLutSize, int nStages, int printf( ".\n" ); } - word * pLuts = Abc_LutCascadeDec( pGuide, pTruth1, Abc_NtkCiNum(pNtk), vVarIDs, nRails, nLutSize, nStages, fVerbose, NULL ); + word * pLuts = Abc_LutCascadeDec( pGuide, pTruth1, Abc_NtkCiNum(pNtk), vVarIDs, nRails, nLutSize, nStages, fVerbose, NULL, NULL ); pNew = pLuts ? Abc_NtkLutCascadeFromLuts( pLuts, Abc_NtkCiNum(pNtk), pNtk, nLutSize, fVerbose ) : NULL; Vec_IntFree( vVarIDs ); @@ -1379,7 +1379,7 @@ Vec_Wrd_t * Abc_NtkLutCasReadTruths( char * pFileName, int nVarsOrig ) void Abc_NtkLutCascadeFile( char * pFileName, int nVarsOrig, int nLutSize, int nStages, int nRails, int nIters, int Seed, int fVerbose, int fVeryVerbose ) { abctime clkStart = Abc_Clock(); - int i, Sum = 0, nStageCount, nTotalLuts = 0, nWords = Abc_TtWordNum(nVarsOrig); + int i, Sum = 0, nStageCount = 0, MyuMin = 0, nTotalLuts = 0, nWords = Abc_TtWordNum(nVarsOrig); Vec_Wrd_t * vTruths = NULL; if ( strstr(pFileName, ".txt") ) vTruths = Abc_NtkLutCasReadTruths( pFileName, nVarsOrig ); @@ -1397,7 +1397,7 @@ void Abc_NtkLutCascadeFile( char * pFileName, int nVarsOrig, int nLutSize, int n printf( "Considering %d functions having %d variables from file \"%s\".\n", nFuncs, nVarsOrig, pFileName ); word * pCopy = ABC_ALLOC( word, nWords ); - int Iter = 0, LutStats[100] = {0}, StageStats[100] = {0}; + int Iter = 0, LutStats[50] = {0}, StageStats[50] = {0}, MyuStats[50] = {0}; Abc_Random(1); for ( i = 0; i < Seed; i++ ) Abc_Random(0); @@ -1409,7 +1409,7 @@ void Abc_NtkLutCascadeFile( char * pFileName, int nVarsOrig, int nLutSize, int n if ( fVeryVerbose ) printf( "\n" ); if ( fVerbose || fVeryVerbose ) - printf( "Function %3d : ", i ); + printf( "Function %4d : ", i ); if ( fVeryVerbose ) Abc_TtPrintHexRev( stdout, pTruth, nVarsOrig ), printf( "\n" ); //continue; @@ -1424,7 +1424,7 @@ void Abc_NtkLutCascadeFile( char * pFileName, int nVarsOrig, int nLutSize, int n printf( "Decomposing %d-var function into %d-rail cascade of %d-LUTs.\n", nVars, nRails, nLutSize ); } - word * pLuts = Abc_LutCascadeDec( NULL, pTruth, nVarsOrig, vVarIDs, nRails, nLutSize, nStages, fVeryVerbose, &nStageCount ); + word * pLuts = Abc_LutCascadeDec( NULL, pTruth, nVarsOrig, vVarIDs, nRails, nLutSize, nStages, fVeryVerbose, &nStageCount, &MyuMin ); Vec_IntFree( vVarIDs ); if ( pLuts == NULL ) { if ( ++Iter < nIters ) { @@ -1439,8 +1439,10 @@ void Abc_NtkLutCascadeFile( char * pFileName, int nVarsOrig, int nLutSize, int n Iter = 0; Sum++; nTotalLuts += Abc_LutCascadeCount(pLuts); - LutStats[Abc_LutCascadeCount(pLuts)]++; - StageStats[nStageCount]++; + if ( Abc_LutCascadeCount(pLuts) < 50 ) + LutStats[Abc_LutCascadeCount(pLuts)]++; + if ( nStageCount < 50) StageStats[nStageCount]++; + if ( MyuMin < 50 ) MyuStats[MyuMin]++; word * pTruth2 = Abc_LutCascadeTruth( pLuts, nVarsOrig ); if ( fVeryVerbose ) Abc_LutCascadePrint( pLuts ); @@ -1458,12 +1460,16 @@ void Abc_NtkLutCascadeFile( char * pFileName, int nVarsOrig, int nLutSize, int n } ABC_FREE( pCopy ); Vec_WrdFree( vTruths ); + printf( "Column multiplicity statistics for %d-rail LUT cascade:\n", nRails ); + for ( i = 0; i < 50; i++ ) + if ( MyuStats[i] ) + printf( " %2d Myu : Function count = %8d (%6.2f %%)\n", i, StageStats[i], 100.0*StageStats[i]/nFuncs ); printf( "Level count statistics for %d-rail LUT cascade:\n", nRails ); - for ( i = 0; i < 100; i++ ) + for ( i = 0; i < 50; i++ ) if ( StageStats[i] ) printf( " %2d level : Function count = %8d (%6.2f %%)\n", i, StageStats[i], 100.0*StageStats[i]/nFuncs ); printf( "LUT count statistics for %d-rail LUT cascade:\n", nRails ); - for ( i = 0; i < 100; i++ ) + for ( i = 0; i < 50; i++ ) if ( LutStats[i] ) printf( " %2d LUT%d : Function count = %8d (%6.2f %%)\n", i, nLutSize, LutStats[i], 100.0*LutStats[i]/nFuncs ); printf( "Non-decomp : Function count = %8d (%6.2f %%)\n", nFuncs-Sum, 100.0*(nFuncs-Sum)/Abc_MaxInt(1, nFuncs) ); diff --git a/src/misc/util/utilBSet.c b/src/misc/util/utilBSet.c index 6f4111eb9..77257b673 100644 --- a/src/misc/util/utilBSet.c +++ b/src/misc/util/utilBSet.c @@ -996,7 +996,7 @@ word * Abc_LutCascade2( word * pFunc, int nVars, int nLutSize, int nLuts, int nR SeeAlso [] ***********************************************************************/ -word Abc_TtFindBVarsSVars( word * pTruth, int nVars, int nRVars, int nRails, int nLutSize, int fVerbose ) +word Abc_TtFindBVarsSVars( word * pTruth, int nVars, int nRVars, int nRails, int nLutSize, int fVerbose, int * pMyu ) { Abc_BSEval_t * p = Abc_BSEvalAlloc(); int nPermVars = nVars-nRVars; @@ -1026,6 +1026,7 @@ word Abc_TtFindBVarsSVars( word * pTruth, int nVars, int nRVars, int nRails, int //printf("Function before: "); Abc_TtPrintHexRev( stdout, pCopy, nVars ); printf( "\n" ); int MyuMin = Abc_BSEvalBest( p, pCopy, pBest, nVars, nRVars, nVars-nLutSize, 0, pPermBest, 0 ); //printf("Function before: "); Abc_TtPrintHexRev( stdout, pCopy, nVars ); printf( "\n" ); + if ( pMyu ) *pMyu = MyuMin; if ( fVerbose ) { printf( "Best perm: " ); diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index 6e50ea981..7c62c5c3a 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -1674,7 +1674,7 @@ void Exa3_ManExactSynthesisRand( Bmc_EsPar_t * pPars ) } pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 ); Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars ); - printf( "\nIteration %d : ", i ); + printf( "\nFunction %4d : ", i ); if ( pPars->nMintNum ) printf( "Random function has %d positive minterms.", pPars->nMintNum ); printf( "\n" ); @@ -1683,7 +1683,7 @@ void Exa3_ManExactSynthesisRand( Bmc_EsPar_t * pPars ) nDecs += Exa3_ManExactSynthesis( pPars ); ABC_FREE( pPars->pTtStr ); } - printf( "\nDecomposable are %d (out of %d) functions (%.2f %%).\n", nDecs, pPars->nRandFuncs, 100.0*nDecs/pPars->nRandFuncs ); + printf( "\nDecomposable are %d (out of %d) functions (%.2f %%).\n\n", nDecs, pPars->nRandFuncs, 100.0*nDecs/pPars->nRandFuncs ); ABC_FREE( pFun ); }