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

Upgrading "lutexact -c" to be like "lutexact -k".

This commit is contained in:
Alan Mishchenko 2025-12-24 13:37:06 -08:00
parent 3d32b8b2ad
commit bd7fb12e18
1 changed files with 144 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

148
src/sat/bmc/bmcMaj7.c
View File

@ -405,6 +405,77 @@ static void Exa7_ManPrintSolution( Exa7_Man_t * p, int fCompl )
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Vec_Wrd_t * Exa7_ManSaveTruthTables( Exa7_Man_t * p, int fCompl )
{
int i, k, nWordsNode, nMintsNode;
assert( p->nLutSize <= 8 );
nMintsNode = 1 << p->nLutSize;
nWordsNode = (p->nLutSize <= 6) ? 1 : (p->nLutSize == 7 ? 2 : 4);
Vec_Wrd_t * vTruths = Vec_WrdStart( p->nObjs * nWordsNode );
for ( i = p->nVars; i < p->nObjs; i++ )
{
word Truth[4] = {0, 0, 0, 0};
int iVarStart = 1 + p->LutMask*(i - p->nVars);
for ( k = 0; k < p->LutMask; k++ )
{
if ( cadical_solver_get_var_value(p->pSat, iVarStart + k) )
{
int bit = k + 1; // minterm index (minterm 0 is fixed to 0)
int w = bit >> 6;
int b = bit & 63;
Truth[w] |= ((word)1 << b);
}
}
// complement the output fully if needed (including minterm 0)
if ( i == p->nObjs - 1 && fCompl )
{
for ( int w = 0; w < nWordsNode; w++ )
{
word Mask;
int rem = nMintsNode - w * 64;
if ( rem <= 0 )
Mask = 0;
else if ( rem >= 64 )
Mask = ~(word)0;
else
Mask = (((word)1) << rem) - 1;
Truth[w] = (~Truth[w]) & Mask;
}
}
if ( p->nLutSize < 6 )
Truth[0] = Abc_Tt6Stretch( Truth[0], p->nLutSize );
for ( int w = 0; w < nWordsNode; w++ )
Vec_WrdWriteEntry( vTruths, i * nWordsNode + w, Truth[w] );
}
return vTruths;
}
static void Exa7_ManPrintPerm( Exa7_Man_t * p )
{
int i, k, iVar;
for ( i = p->nVars; i < p->nObjs; i++ )
{
if ( i > p->nVars )
printf( "_" );
for ( k = p->nLutSize - 1; k >= 0; k-- )
{
iVar = Exa7_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
printf( "%c", 'a'+iVar );
}
}
}
/**Function*************************************************************
Synopsis []
@ -705,6 +776,9 @@ void Exa7_ManPrint( Exa7_Man_t * p, int i, int iMint, abctime clk )
}
int Exa7_ManExactSynthesis( Bmc_EsPar_t * pPars )
{
extern int Exa7_ManExactSynthesisIter( Bmc_EsPar_t * pPars );
if ( pPars->fMinNodes )
return Exa7_ManExactSynthesisIter( pPars );
int i, status, Res = 0, iMint = 1;
abctime clkTotal = Abc_Clock();
Exa7_Man_t * p; int fCompl = 0;
@ -713,7 +787,7 @@ int Exa7_ManExactSynthesis( Bmc_EsPar_t * pPars )
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 );
if ( !pPars->fSilent ) printf( "Generated symmetric function: %s\n", pPars->pTtStr );
if ( !pPars->fSilent && pPars->nVars <= 7 ) printf( "Generated symmetric function: %s\n", pPars->pTtStr );
ABC_FREE( pFun );
}
if ( pPars->pTtStr )
@ -745,21 +819,87 @@ int Exa7_ManExactSynthesis( Bmc_EsPar_t * pPars )
if ( pPars->fVerbose && status != CADICAL_UNDEC )
Exa7_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
if ( iMint == -1 )
Exa7_ManPrintSolution( p, fCompl ), Res = 1;
{
Exa7_ManPrintSolution( p, fCompl );
printf( "The variable permutation is \"" );
Exa7_ManPrintPerm( p );
printf( "\".\n" );
if ( pPars->fDumpBlif )
Exa7_ManDumpBlif( p, fCompl );
if ( p->pPars->fGenTruths ) {
if ( p->pPars->vTruths )
Vec_WrdFreeP( &p->pPars->vTruths );
p->pPars->vTruths = Exa7_ManSaveTruthTables( p, fCompl );
}
Res = 1;
}
else if ( status == CADICAL_UNDEC )
printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
else if ( !p->pPars->fSilent )
printf( "The problem has no solution.\n" ), Res = 2;
if ( !pPars->fSilent && (p->nUsed[0] || p->nUsed[1]) ) printf( "Added = %d. Tried = %d. ", p->nUsed[1], p->nUsed[0] );
if ( !pPars->fSilent ) Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
if ( iMint == -1 && pPars->fDumpBlif )
Exa7_ManDumpBlif( p, fCompl );
if ( pPars->pSymStr )
ABC_FREE( pPars->pTtStr );
Exa7_ManFree( p );
return Res;
}
int Exa7_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++ ) {
if ( !pPars->fSilent ) printf( "\nTrying M = %d:\n", n );
pPars->nNodes = n;
if ( !pPars->fUsePerm && 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 );
}
else if ( pPars->fUsePerm && fGenPerm ) {
Vec_Str_t * vStr = Vec_StrAlloc( 100 );
for ( int v = 0; v < pPars->nLutSize; v++ )
Vec_StrPush( vStr, 'a'+v );
for ( int m = 1; m < pPars->nNodes; m++ ) {
Vec_StrPush( vStr, '_' );
if ( m & 1 )
for ( int v = 0; v < pPars->nLutSize-1; v++ )
Vec_StrPush( vStr, 'a'+(pPars->nVars-(pPars->nLutSize-1-v)) );
else
for ( int v = 0; v < pPars->nLutSize-1; v++ )
Vec_StrPush( vStr, 'a'+v );
}
Vec_StrPush( vStr, '\0' );
ABC_FREE( pPars->pPermStr );
pPars->pPermStr = Vec_StrReleaseArray(vStr);
Vec_StrFree( vStr );
}
Result = Exa7_ManExactSynthesis(pPars);
fflush( stdout );
if ( Result == 1 )
break;
}
return Result;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///