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

Improvements to "lutcasdec".

This commit is contained in:
Alan Mishchenko 2025-05-20 06:39:28 -07:00
parent c398b06740
commit 9bb736acee
3 changed files with 156 additions and 104 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -9171,12 +9171,12 @@ usage:
int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Abc_Ntk_t * Abc_NtkLutCascadeGen( int nLutSize, int nStages, int nRails, int nShared, int fVerbose );
extern Abc_Ntk_t * Abc_NtkLutCascade2( Abc_Ntk_t * pNtk, int nLutSize, int nLuts, int nRails, int nIters, int nJRatio, int Seed, int fVerbose, char * pGuide );
extern void Abc_NtkLutCascadeFile( char * pFileName, int nVarNum, int nLutSize, int nLuts, int nRails, int nIters, int nJRatio, int Seed, int fVerbose, int fVeryVerbose, int fPrintMyu );
extern Abc_Ntk_t * Abc_NtkLutCascade2( Abc_Ntk_t * pNtk, int nLutSize, int nLuts, int nRails, int nIters, int nJRatio, int nZParam, int Seed, int fVerbose, int fVeryVerbose, char * pGuide );
extern void Abc_NtkLutCascadeFile( char * pFileName, int nVarNum, int nLutSize, int nLuts, int nRails, int nIters, int nJRatio, int nZParam, int Seed, int fVerbose, int fVeryVerbose, int fPrintMyu );
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; char * pGuide = NULL, * pFileName = NULL;
int c, nVarNum = -1, nLutSize = 6, nStages = 8, nRails = 1, nShared = 2, Seed = 0, nIters = 10, nJRatio = 0, fGen = 0, fPrintMyu = 0, fVerbose = 0, fVeryVerbose = 0;
int c, nVarNum = -1, nLutSize = 6, nStages = 8, nRails = 1, nShared = 2, Seed = 0, nIters = 1, nJRatio = 0, nZParam = 0, fGen = 0, fPrintMyu = 0, fVerbose = 0, fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KMRSCIJNFgmvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "KMRSCIJZNFgmvwh" ) ) != EOF )
{
switch ( c )
{
@ -9257,6 +9257,15 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nJRatio < 0 )
goto usage;
break;
case 'Z':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-Z\" should be followed by a file name.\n" );
goto usage;
}
nZParam = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'N':
if ( globalUtilOptind >= argc )
{
@ -9302,7 +9311,7 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "The number of variables should be given on the command line using switch \"-N <num>\".\n" );
return 1;
}
Abc_NtkLutCascadeFile( pFileName, nVarNum, nLutSize, nStages, nRails, nIters, nJRatio, Seed, fVerbose, fVeryVerbose, fPrintMyu );
Abc_NtkLutCascadeFile( pFileName, nVarNum, nLutSize, nStages, nRails, nIters, nJRatio, nZParam, Seed, fVerbose, fVeryVerbose, fPrintMyu );
return 0;
}
if ( fGen )
@ -9339,7 +9348,7 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( argc == globalUtilOptind + 1 )
pGuide = argv[globalUtilOptind];
pNtkRes = Abc_NtkLutCascade2( pNtk, nLutSize, nStages, nRails, nIters, nJRatio, Seed, fVerbose, pGuide );
pNtkRes = Abc_NtkLutCascade2( pNtk, nLutSize, nStages, nRails, nIters, nJRatio, nZParam, Seed, fVerbose, fVeryVerbose, pGuide );
if ( pNtkRes == NULL )
{
Abc_Print( -1, "LUT cascade mapping failed.\n" );
@ -9349,7 +9358,7 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: lutcasdec [-KMRCSIJN <num>] [-F <file>] [-gmvwh]\n" );
Abc_Print( -2, "usage: lutcasdec [-KMRCSIJZN <num>] [-F <file>] [-gmvwh]\n" );
Abc_Print( -2, "\t decomposes the primary output functions into LUT cascades\n" );
Abc_Print( -2, "\t-K <num> : the number of LUT inputs [default = %d]\n", nLutSize );
Abc_Print( -2, "\t-M <num> : the maximum delay (the number of stages) [default = %d]\n", nStages );
@ -9358,6 +9367,7 @@ usage:
Abc_Print( -2, "\t-S <num> : the random seed for randomized bound-set selection [default = %d]\n", Seed );
Abc_Print( -2, "\t-I <num> : the number of iterations when looking for a solution [default = %d]\n", nIters );
Abc_Print( -2, "\t-J <num> : toggle using random bound-set every this many iterations [default = %d]\n", nJRatio );
Abc_Print( -2, "\t-Z <num> : the number determining how many decompositions are tried [default = %d]\n", nZParam );
Abc_Print( -2, "\t-N <num> : the number of support variables (for truth table files only) [default = unused]\n" );
Abc_Print( -2, "\t-F <file>: a text file with truth tables in hexadecimal listed one per line\n");
Abc_Print( -2, "\t-g : toggle generating random cascade with these parameters [default = %s]\n", fGen? "yes": "no" );

22
src/base/abci/abcCas.c
View File

@ -656,12 +656,18 @@ 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 nJRatio, int fVerbose, Vec_Wrd_t * vCas, int * pMyu )
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 nJRatio, int nZParam, int fVerbose, Vec_Wrd_t * vCas, int * pMyu )
{
extern word Abc_TtFindBVarsSVars( word * p, int nVars, int nRVars, int nRails, int nLutSize, int fVerbose, int * pMyu, int nJRatio );
extern word Abc_TtFindBVarsSVars2( word * p, int nVars, int nRVars, int nRails, int nLutSize, int fVerbose, int * pMyu, int nJRatio );
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, pMyu, nJRatio );
//word Guide = pGuide ? 0 : Abc_TtFindBVarsSVars( Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVars, nRails, nLutSize, fVerbose, pMyu, nJRatio );
word Guide = pGuide ? 0 : Abc_TtFindBVarsSVars2( Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVars, nRails, nLutSize, fVerbose, pMyu, nZParam );
// if ( nZParam )
// Guide = pGuide ? 0 : Abc_TtFindBVarsSVars2( Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVars, nRails, nLutSize, fVerbose, pMyu, nZParam );
// else
// Guide = pGuide ? 0 : Abc_TtFindBVarsSVars( Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVars, nRails, nLutSize, fVerbose, pMyu, nJRatio );
if ( !pGuide && !Guide ) {
if ( fVerbose )
printf( "The function is not decomposable with %d rails.\n", nRails );
@ -716,7 +722,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 nJRatio, int fVerbose, int * pnStages, int * pMyu )
word * Abc_LutCascadeDec( char * pGuide, word * pTruth, int nVarsOrig, Vec_Int_t * vVarIDs, int nRails, int nLutSize, int nStages, int nJRatio, int nZParam, 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 +730,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, nJRatio, fVerbose, vCas, i ? NULL : pMyu );
nRVars = Abc_LutCascadeDecStage( pGuide, i, vFuncs, vVarIDs, nRVars, nRails, nLutSize, nJRatio, nZParam, fVerbose, vCas, i ? NULL : pMyu );
if ( i+2 > nStages ) {
if ( fVerbose )
printf( "The length of the cascade (%d) exceeds the max allowed number of stages (%d).\n", i+2, nStages );
@ -836,7 +842,7 @@ Abc_Ntk_t * Abc_NtkLutCascade( Abc_Ntk_t * pNtk, int nLutSize, int nStages, int
Gia_ManStop( pGia );
return pNew;
}
Abc_Ntk_t * Abc_NtkLutCascade2( Abc_Ntk_t * pNtk, int nLutSize, int nStages, int nRails, int nIters, int nJRatio, int Seed, int fVerbose, char * pGuide )
Abc_Ntk_t * Abc_NtkLutCascade2( Abc_Ntk_t * pNtk, int nLutSize, int nStages, int nRails, int nIters, int nJRatio, int nZParam, int Seed, int fVerbose, int fVeryVerbose, char * pGuide )
{
extern Gia_Man_t * Abc_NtkStrashToGia( Abc_Ntk_t * pNtk );
int i, nWords = Abc_TtWordNum(Abc_NtkCiNum(pNtk));
@ -864,7 +870,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, Iter >= nIters ? 1 : 0, fVerbose, NULL, NULL );
word * pLuts = Abc_LutCascadeDec( pGuide, pTruth1, Abc_NtkCiNum(pNtk), vVarIDs, nRails, nLutSize, nStages, Iter >= nIters ? 1 : 0, nZParam, fVeryVerbose, NULL, NULL );
pNew = pLuts ? Abc_NtkLutCascadeFromLuts( pLuts, Abc_NtkCiNum(pNtk), pNtk, nLutSize, fVerbose ) : NULL;
Vec_IntFree( vVarIDs );
@ -1377,7 +1383,7 @@ Vec_Wrd_t * Abc_NtkLutCasReadTruths( char * pFileName, int nVarsOrig )
SeeAlso []
***********************************************************************/
void Abc_NtkLutCascadeFile( char * pFileName, int nVarsOrig, int nLutSize, int nStages, int nRails, int nIters, int nJRatio, int Seed, int fVerbose, int fVeryVerbose, int fPrintMyu )
void Abc_NtkLutCascadeFile( char * pFileName, int nVarsOrig, int nLutSize, int nStages, int nRails, int nIters, int nJRatio, int nZParam, int Seed, int fVerbose, int fVeryVerbose, int fPrintMyu )
{
abctime clkStart = Abc_Clock();
int i, Sum = 0, nStageCount = 0, MyuMin = 0, nTotalLuts = 0, nWords = Abc_TtWordNum(nVarsOrig);
@ -1425,7 +1431,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, (int)(Iter >= nIters), fVeryVerbose, &nStageCount, &MyuMin );
word * pLuts = Abc_LutCascadeDec( NULL, pTruth, nVarsOrig, vVarIDs, nRails, nLutSize, nStages, (int)(Iter >= nIters), nZParam, fVeryVerbose, &nStageCount, &MyuMin );
Vec_IntFree( vVarIDs );
if ( MyuMin < 50 ) MyuStats[MyuMin]++, IterReal++;
if ( pLuts == NULL ) {

214
src/misc/util/utilBSet.c
View File

@ -635,10 +635,10 @@ int Abc_BSEvalBest( Abc_BSEval_t * p, word * pIn, word * pBest, word * pBest2, i
}
if ( 0 ) {
//word pPat[MAX_PAT_WORD_SIZE];
int nRails = 1, Shared = 0;
int nRails = 1, Shared = 0, nSetSize = 0;
if ( CostThis > (1 << nRails) ) {
extern int Abc_SharedEvalBest( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, int nFVars, int MyuMin, int nRails, int fVerbose, int * pSetShared, word * pPat );
int nRailsMin = Abc_SharedEvalBest( p, pIn, nVars, nCVars, nFVars, CostThis, nRails, 0, &Shared, p->pPat );
extern int Abc_SharedEvalBest( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, int nFVars, int MyuMin, int nRails, int fVerbose, int * pSetShared, int * pSetSize, word * pPat );
int nRailsMin = Abc_SharedEvalBest( p, pIn, nVars, nCVars, nFVars, CostThis, nRails, 0, &Shared, &nSetSize, p->pPat );
printf( " RailMin = %d. Shared = %2d. ", nRailsMin, Shared );
}
}
@ -892,7 +892,7 @@ int Abc_BSEvalFindShared( int nVars, word * pISets, int nISets, int nBSWords, Ve
SeeAlso []
***********************************************************************/
int Abc_SharedEvalBest( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, int nFVars, int MyuMin, int nRails, int fVerbose, int * pSetShared, word * pPat )
int Abc_SharedEvalBest( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, int nFVars, int MyuMin, int nRails, int fVerbose, int * pSetShared, int * pnSetSize, word * pPat )
{
int nBSWords = Abc_Truth6WordNum( nVars - nFVars ), CVarMask = nCVars ? Abc_InfoMask(nCVars) << (nVars - nCVars - nFVars) : 0;
int MyuCur, Myu = Abc_TtGetCMInt( pTruth, nVars, nFVars, p->vCounts, p->vTable, p->vStore, p->vUsed, pPat );
@ -914,6 +914,7 @@ int Abc_SharedEvalBest( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars,
if ( nRailsMin > nRailsCur ) {
nRailsMin = nRailsCur;
*pSetShared = iSet;
*pnSetSize = i;
}
}
if ( nRailsMin <= nRails )
@ -921,89 +922,6 @@ int Abc_SharedEvalBest( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars,
}
return nRailsMin;
}
int Abc_DeriveLutDec( word * pTruth, int nVars, int nCVars, int nFVars, int * pPerm, int nRails, int Shared, int fVerbose, Vec_Wrd_t * vRes )
{
return 0;
}
/**Function*************************************************************
Synopsis [Decomposing truth table into a K-LUT cascade with R rails.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
word * Abc_LutCascade2( word * pFunc, int nVars, int nLutSize, int nLuts, int nRails, int nIters, int fVerbose )
{
Abc_BSEval_t * p = Abc_BSEvalAlloc();
Vec_Wrd_t * vRes = Vec_WrdStart( 1 ); word * pRes = NULL;
word * pTruth = ABC_ALLOC( word, Abc_TtWordNum(nVars) );
word * pBest = ABC_ALLOC( word, Abc_TtWordNum(nVars) );
word * pBest2 = ABC_ALLOC( word, Abc_TtWordNum(nVars) );
Abc_TtCopy( pTruth, pFunc, Abc_TtWordNum(nVars), 0 );
int i, r, nVarsCur = nVars, nOutVars = 0;
while ( nVarsCur > nLutSize )
{
int pPerm[32] = {0};
int pPerm2[32] = {0};
if ( p->nVars != nVarsCur || p->nBVars != nLutSize ) {
Vec_IntFreeP( &p->vPairs );
if ( p->nBVars != nLutSize ) {
Vec_WecFreeP( &p->vSets );
Vec_WrdFreeP( &p->vCofs );
p->vCofs = Abc_BSEvalCreateCofactorSets( nLutSize, &p->vSets );
if ( p->nBVars < nLutSize ) {
ABC_FREE( p->pPat );
p->pPat = ABC_ALLOC( word, (1 << nLutSize)*Abc_TtWordNum(nLutSize) );
}
}
p->vPairs = Abc_GenChasePairs( nVarsCur, nLutSize );
p->nVars = nVarsCur;
p->nBVars = nLutSize;
}
int MyuMin = Abc_BSEvalBest( p, pTruth, pBest, pBest2, nVarsCur, nOutVars, nVarsCur-nLutSize, fVerbose, pPerm, pPerm2, 0, 0 );
int Shared = 0, nRailsMin = Abc_Base2Log( MyuMin );
for ( r = 1; r <= nRails && nRailsMin > r; r++ ) {
int nRailsMinNew = Abc_SharedEvalBest( p, pBest, nVarsCur, nOutVars, nVarsCur-nLutSize, MyuMin, nRails, fVerbose, &Shared, p->pPat );
if ( nRailsMinNew < 100 )
nRailsMin = nRailsMinNew;
}
MyuMin = 1 << nRailsMin;
if ( nRailsMin > nRails ) {
Vec_WrdFreeP( &vRes );
break;
}
// update nVarsCur, pTruth, nOutVars, and vRes
nVarsCur = Abc_DeriveLutDec( pBest, nVarsCur, nOutVars, nVarsCur-nLutSize, pPerm, nRailsMin, Shared, fVerbose, vRes );
Abc_TtCopy( pTruth, pBest, Abc_TtWordNum(nVarsCur), 0 );
nOutVars = nRailsMin;
}
if ( vRes ) // decomposition succeeded
{
// create the last node
assert( nVarsCur <= nLutSize );
Vec_WrdAddToEntry( vRes, 0, 1 );
Vec_WrdPush( vRes, nVarsCur+4 );
Vec_WrdPush( vRes, nVarsCur );
for ( i = 0; i < nVarsCur; i++ )
Vec_WrdPush( vRes, i );
Vec_WrdPush( vRes, 0 );
Vec_WrdPush( vRes, pTruth[0] );
// extract the output array
pRes = Vec_WrdReleaseArray( vRes );
Vec_WrdFree( vRes );
}
// cleanup and return
Abc_BSEvalFree(p);
ABC_FREE( pTruth );
ABC_FREE( pBest );
ABC_FREE( pBest2 );
return pRes;
}
/**Function*************************************************************
@ -1057,9 +975,9 @@ word Abc_TtFindBVarsSVars( word * pTruth, int nVars, int nRVars, int nRails, int
printf( " Myu = %d. ", MyuMin );
}
int Shared = 0, nRailsMin = Abc_Base2Log( MyuMin );
int Shared = 0, nSetSize = 0, nRailsMin = Abc_Base2Log( MyuMin );
for ( r = 1; r <= nRails && nRailsMin > r; r++ ) {
int nRailsMinNew = Abc_SharedEvalBest( p, pBest, nVars, nRVars, nVars-nLutSize, MyuMin, r, 0, &Shared, p->pPat );
int nRailsMinNew = Abc_SharedEvalBest( p, pBest, nVars, nRVars, nVars-nLutSize, MyuMin, r, 0, &Shared, &nSetSize, p->pPat );
if ( nRailsMinNew < 100 )
nRailsMin = nRailsMinNew;
}
@ -1088,6 +1006,124 @@ word Abc_TtFindBVarsSVars( word * pTruth, int nVars, int nRVars, int nRails, int
return ((word)MyuMin << 48) | (mSVars << 24) | mBVars;
}
word Abc_BSEvalEncode( int * pPermBest, int nVars, int nLutSize, int Shared, int MyuMin, int SharedSize )
{
int v;
word mBVars = 0;
for ( v = 0; v < nLutSize; v++ )
mBVars |= (word)1 << pPermBest[nVars-nLutSize+v];
word mSVars = 0;
for ( v = 0; v < nLutSize; v++ )
if ( (Shared >> v) & 1 )
mSVars |= (word)1 << (nVars-nLutSize+v);
return ((word)MyuMin << 48) | (mSVars << 24) | mBVars;
}
word Abc_TtFindBVarsSVars2( word * pTruth, int nVars, int nCVars, int nRails, int nLutSize, int fVerbose, int * pMyu, int nMyuIncrease )
{
Abc_BSEval_t * p = Abc_BSEvalAlloc();
int nFVars = nVars-nLutSize;
int nPermVars = nVars-nCVars;
if ( p->nVars != nPermVars ) {
Vec_IntFreeP( &p->vPairs );
p->vPairs = Abc_GenChasePairs( nPermVars, nLutSize-nCVars );
p->nVars = nPermVars;
}
if ( p->nBVars != nLutSize ) {
Vec_WecFreeP( &p->vSets );
Vec_WrdFreeP( &p->vCofs );
p->vCofs = Abc_BSEvalCreateCofactorSets( nLutSize, &p->vSets );
if ( p->nBVars < nLutSize ) {
ABC_FREE( p->pPat );
p->pPat = ABC_ALLOC( word, (1 << nLutSize)*Abc_TtWordNum(nLutSize) );
}
p->nBVars = nLutSize;
}
int nWords = Abc_TtWordNum(nVars);
word * pCopy = ABC_ALLOC( word, nWords );
Abc_TtCopy( pCopy, pTruth, nWords, 0 );
word Result = 0;
int i, k, Var0, Var1, Pla2Var[32], Var2Pla[32];
for ( i = 0; i < nVars; i++ )
Pla2Var[i] = Var2Pla[i] = i;
int MyuBest = 1 << nVars;
int nSetSizeBest = nVars;
if ( pMyu ) *pMyu = 1 << nVars;
Vec_IntForEachEntryDouble( p->vPairs, Var0, Var1, i ) {
int MyuThis = Abc_TtGetCM( pCopy, nVars, nFVars, p->vCounts, p->vTable, p->vStore, p->vUsed, 0 );
if ( pMyu ) *pMyu = Abc_MinInt( *pMyu, MyuThis );
if ( fVerbose )
{
printf( "%3d : ", i/2 );
for ( k = nCVars-1; k >= 0; k-- )
printf( " %d", nVars-nCVars+k );
printf( " " );
for ( k = nPermVars-1; k >= nFVars; k-- )
printf( " %d", Pla2Var[k] );
printf( " " );
for ( k = nFVars-1; k >= 0; k-- )
printf( " %d", Pla2Var[k] );
printf( " : Myu = %3d", MyuThis );
}
if ( MyuThis <= MyuBest + nMyuIncrease ) {
int Shared = 0, nSetSize = 0;
if ( MyuThis > 2 ) {
int SharedThis = 0, nSetSizeThis = 0;
int nRailsMin = Abc_SharedEvalBest( p, pCopy, nVars, nCVars, nFVars, MyuThis, nRails, 0, &SharedThis, &nSetSizeThis, p->pPat );
if ( fVerbose )
printf( " RailsMyu = %3d. RailsMin = %3d. Shared = %2d. SetSize = %d.", Abc_Base2Log(MyuThis), nRailsMin, SharedThis, nSetSizeThis );
if ( nRailsMin <= nRails ) {
assert( Abc_Base2Log(MyuThis) >= nRailsMin );
MyuThis = 1 << nRailsMin;
Shared = SharedThis;
nSetSize = nSetSizeThis;
}
}
if ( MyuBest > MyuThis || (MyuBest == MyuThis && nSetSizeBest > nSetSize) ) {
MyuBest = MyuThis;
nSetSizeBest = nSetSize;
Result = Abc_BSEvalEncode( Pla2Var, nVars, p->nBVars, Shared, MyuBest, nSetSize );
if ( fVerbose )
printf( " <== best" );
}
}
if ( fVerbose )
printf( "\n" );
int iPlace0 = Var2Pla[Var0];
int iPlace1 = Var2Pla[Var1];
if ( iPlace0 == iPlace1 )
continue;
Abc_TtSwapVars( pCopy, nVars, iPlace0, iPlace1 );
Var2Pla[Pla2Var[iPlace0]] = iPlace1;
Var2Pla[Pla2Var[iPlace1]] = iPlace0;
Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
}
for ( i = 0; i < nPermVars; i++ )
{
int iPlace0 = i;
int iPlace1 = Var2Pla[i];
if ( iPlace0 == iPlace1 )
continue;
Abc_TtSwapVars( pCopy, nVars, iPlace0, iPlace1 );
Var2Pla[Pla2Var[iPlace0]] = iPlace1;
Var2Pla[Pla2Var[iPlace1]] = iPlace0;
Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
}
if ( !Abc_TtEqual(pCopy, pTruth, nWords) )
printf( "Internal truth table check failed.\n" );
Abc_BSEvalFree(p);
if ( MyuBest > (1 << nRails) )
return 0;
return Result;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////