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

Adding BLIF dumping to "lutexact".

This commit is contained in:
Alan Mishchenko 2024-08-13 20:03:18 -07:00
parent 324ceeaa08
commit c2391686ea
2 changed files with 116 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

59
src/sat/bmc/bmcMaj.c
View File

@ -1228,6 +1228,61 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl )
{
int i, k, b, iVar;
char pFileName[1000];
sprintf( pFileName, "%s.blif", p->pPars->pTtStr );
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL ) return;
fprintf( pFile, "# Realization of given %d-input function using %d %d-input LUTs synthesized by ABC on %s\n", p->nVars, p->nNodes, p->nLutSize, Extra_TimeStamp() );
fprintf( pFile, ".model %s\n", p->pPars->pTtStr );
fprintf( pFile, ".inputs" );
for ( k = 0; k < p->nVars; k++ )
fprintf( pFile, " %c", 'a'+k );
fprintf( pFile, "\n.outputs F\n" );
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
{
fprintf( pFile, ".names" );
for ( k = 0; k < p->nLutSize; k++ )
{
iVar = Exa3_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
fprintf( pFile, " %c", 'a'+iVar );
else
fprintf( pFile, " %02d", iVar );
}
if ( i == p->nObjs - 1 )
fprintf( pFile, " F\n" );
else
fprintf( pFile, " %02d\n", i );
int iVarStart = 1 + p->LutMask*(i - p->nVars);
for ( k = 0; k < p->LutMask; k++ )
{
int Val = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+k);
if ( Val == 0 )
continue;
for ( b = 0; b < p->nLutSize; b++ )
fprintf( pFile, "%d", ((k+1) >> b) & 1 );
fprintf( pFile, " %d\n", i != p->nObjs - 1 || !fCompl );
}
}
fprintf( pFile, ".end\n\n" );
fclose( pFile );
printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
}
/**Function*************************************************************
@ -1483,8 +1538,10 @@ void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
else
printf( "The problem has no solution.\n" );
printf( "Added = %d. Tried = %d. ", p->nUsed[1], p->nUsed[0] );
Exa3_ManFree( p );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
if ( iMint == -1 )
Exa3_ManDumpBlif( p, fCompl );
Exa3_ManFree( p );
}
/**Function*************************************************************

59
src/sat/bmc/bmcMaj2.c
View File

@ -1176,6 +1176,61 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl )
{
int i, k, b, iVar;
char pFileName[1000];
sprintf( pFileName, "%s.blif", p->pPars->pTtStr );
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL ) return;
fprintf( pFile, "# Realization of given %d-input function using %d %d-input LUTs synthesized by ABC on %s\n", p->nVars, p->nNodes, p->nLutSize, Extra_TimeStamp() );
fprintf( pFile, ".model %s\n", p->pPars->pTtStr );
fprintf( pFile, ".inputs" );
for ( k = 0; k < p->nVars; k++ )
fprintf( pFile, " %c", 'a'+k );
fprintf( pFile, "\n.outputs F\n" );
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
{
fprintf( pFile, ".names" );
for ( k = 0; k < p->nLutSize; k++ )
{
iVar = Exa3_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
fprintf( pFile, " %c", 'a'+iVar );
else
fprintf( pFile, " %02d", iVar );
}
if ( i == p->nObjs - 1 )
fprintf( pFile, " F\n" );
else
fprintf( pFile, " %02d\n", i );
int iVarStart = 1 + p->LutMask*(i - p->nVars);
for ( k = 0; k < p->LutMask; k++ )
{
int Val = sat_solver_var_value(p->pSat, iVarStart+k);
if ( Val == 0 )
continue;
for ( b = 0; b < p->nLutSize; b++ )
fprintf( pFile, "%d", ((k+1) >> b) & 1 );
fprintf( pFile, " %d\n", i != p->nObjs - 1 || !fCompl );
}
}
fprintf( pFile, ".end\n\n" );
fclose( pFile );
printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
}
/**Function*************************************************************
@ -1364,8 +1419,10 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars )
}
if ( iMint == -1 )
Exa3_ManPrintSolution( p, fCompl );
Exa3_ManFree( p );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
if ( iMint == -1 )
Exa3_ManDumpBlif( p, fCompl );
Exa3_ManFree( p );
}