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

Exact synthesis using NAND-gates.

This commit is contained in:
Alan Mishchenko 2024-03-24 00:10:08 +09:00
parent 783a5404a2
commit b0d2ff1c63
4 changed files with 205 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/base/abc/abc.h
View File

@ -841,7 +841,7 @@ extern ABC_DLL void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t
extern ABC_DLL void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
extern ABC_DLL void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
extern ABC_DLL void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
extern ABC_DLL void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes, int fVerbose );
extern ABC_DLL void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes, int fOutputs, int fVerbose );
extern ABC_DLL void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
extern ABC_DLL void Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll );
extern ABC_DLL void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj );

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

@ -2022,14 +2022,16 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fListNodes;
int fProfile;
int fOutputs;
int fVerbose;
// set defaults
fListNodes = 0;
fProfile = 1;
fOutputs = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "npvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "npovh" ) ) != EOF )
{
switch ( c )
{
@ -2039,6 +2041,9 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'p':
fProfile ^= 1;
break;
case 'o':
fOutputs ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -2079,14 +2084,15 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// process all COs
Abc_NtkPrintLevel( stdout, pNtk, fProfile, fListNodes, fVerbose );
Abc_NtkPrintLevel( stdout, pNtk, fProfile, fListNodes, fOutputs, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: print_level [-npvh] <node>\n" );
Abc_Print( -2, "usage: print_level [-npovh] <node>\n" );
Abc_Print( -2, "\t prints information about node level and cone size\n" );
Abc_Print( -2, "\t-n : toggles printing nodes by levels [default = %s]\n", fListNodes? "yes": "no" );
Abc_Print( -2, "\t-p : toggles printing level profile [default = %s]\n", fProfile? "yes": "no" );
Abc_Print( -2, "\t-o : toggles printing output levels [default = %s]\n", fOutputs? "yes": "no" );
Abc_Print( -2, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\tnode : (optional) one node to consider\n");
@ -9310,11 +9316,12 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars );
extern void Exa_ManExactSynthesis5( Bmc_EsPar_t * pPars );
extern void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName );
int c, fKissat = 0, fKissat2 = 0;
extern void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize );
int c, fKissat = 0, fKissat2 = 0, fUseNands = 0, GateSize = 0;
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "INTadconugklvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "INTGabdconugklvh" ) ) != EOF )
{
switch ( c )
{
@ -9351,9 +9358,23 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->RuntimeLim < 0 )
goto usage;
break;
case 'G':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
goto usage;
}
GateSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( GateSize < 0 )
goto usage;
break;
case 'a':
pPars->fOnlyAnd ^= 1;
break;
case 'b':
fUseNands ^= 1;
break;
case 'd':
pPars->fDynConstr ^= 1;
break;
@ -9401,7 +9422,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Truth table should be given on the command line.\n" );
return 1;
}
if ( (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) )
if ( pPars->nVars >= 2 && (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) )
{
Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (pPars->nVars-2)), strlen(pPars->pTtStr) );
return 1;
@ -9416,7 +9437,9 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Function should not have more than 10 inputs.\n" );
return 1;
}
if ( fKissat )
if ( fUseNands )
Exa_ManExactSynthesis7( pPars, GateSize );
else if ( fKissat )
Exa_ManExactSynthesis4( pPars );
else if ( fKissat2 )
Exa_ManExactSynthesis5( pPars );
@ -9427,12 +9450,14 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: twoexact [-INT <num>] [-adconugklvh] <hex>\n" );
Abc_Print( -2, "usage: twoexact [-INTG <num>] [-abdconugklvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" );
Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
Abc_Print( -2, "\t-N <num> : the number of two-input nodes [default = %d]\n", pPars->nNodes );
Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim );
Abc_Print( -2, "\t-G <num> : the largest allowed gate size (NANDs only) [default = %d]\n", GateSize );
Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
Abc_Print( -2, "\t-b : toggle using only NAND-gates [default = %s]\n", fUseNands ? "yes" : "no" );
Abc_Print( -2, "\t-d : toggle using dynamic constraint addition [default = %s]\n", pPars->fDynConstr ? "yes" : "no" );
Abc_Print( -2, "\t-c : toggle dumping CNF into a file [default = %s]\n", pPars->fDumpCnf ? "yes" : "no" );
Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" );

12
src/base/abci/abcPrint.c
View File

@ -1228,11 +1228,19 @@ char * Abc_NodeGetPrintName( Abc_Obj_t * pObj )
}
return Abc_ObjName(nPos == 1 ? pFanout : pObj);
}
void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes, int fVerbose )
void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes, int fOutputs, int fVerbose )
{
Abc_Obj_t * pNode;
int i, k, Length;
if ( fOutputs )
{
Abc_NtkLevel(pNtk);
printf( "Outputs by level: " );
Abc_NtkForEachCo( pNtk, pNode, k )
printf( "%d=%d ", k, Abc_ObjFanin0(pNode)->Level );
printf( "\n" );
return;
}
if ( fListNodes )
{
int nLevels;

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

@ -3724,10 +3724,170 @@ void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName )
if ( pMini ) Mini_AigStop( pMini );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Exa7_AddClause( FILE * pFile, int * pLits, int nLits )
{
int i, k = 0;
for ( i = 0; i < nLits; i++ ) {
if ( pLits[i] == 1 )
return 0;
else if ( pLits[i] == 0 )
continue;
else
pLits[k++] = pLits[i];
}
nLits = k;
assert( nLits > 0 );
if ( pFile )
{
for ( i = 0; i < nLits; i++ )
fprintf( pFile, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
fprintf( pFile, "0\n" );
}
if ( 0 )
{
for ( i = 0; i < nLits; i++ )
fprintf( stdout, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i])-1 );
fprintf( stdout, "\n" );
}
return 1;
}
static inline int Exa7_AddClause4( FILE * pFile, int Lit0, int Lit1, int Lit2, int Lit3 )
{
int pLits[4] = { Lit0, Lit1, Lit2, Lit3 };
return Exa7_AddClause( pFile, pLits, 4 );
}
int Exa7_GetVar( int n, int i, int j, int m )
{
return 1 + n*n*m + n*i + j;
}
int Exa7_ManGenCnf( char * pFileName, word * pTruth, int nVars, int nNodes, int GateSize )
{
int m, n, v, k, nV = nVars + nNodes, nMints = 1 << nVars, nClas = 0;
int pVars[32] = {0}; assert( nVars + nNodes + 1 < 32 );
FILE * pFile = fopen( pFileName, "wb" );
fputs( "p cnf \n", pFile );
for ( m = 0; m < nMints; m++ )
{
for ( v = 0; v < nVars; v++ )
nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(Exa7_GetVar(nV, v, v, m), ((m >> v)&1)==0), 0, 0, 0 );
nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(Exa7_GetVar(nV, nV-1, nV-1, m), ((pTruth[0] >> m)&1)==0), 0, 0, 0 );
for ( n = nVars; n < nV; n++ )
{
int iValNode = Exa7_GetVar(nV, n, n, m);
for ( v = 0; v < n; v++ )
{
int iParVar = Exa7_GetVar(nV, v, n, 0); // v < n
int iFanVar = Exa7_GetVar(nV, n, v, m);
int iValFan = Exa7_GetVar(nV, v, v, m);
// iFanVar = ~iParVar | iValFan
nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 1), Abc_Var2Lit(iParVar, 1), Abc_Var2Lit(iValFan, 0), 0 );
nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 0), Abc_Var2Lit(iParVar, 0), 0, 0 );
nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 0), Abc_Var2Lit(iValFan, 1), 0, 0 );
// iParVar & ~iValFan => iValNode
nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iParVar, 1), Abc_Var2Lit(iValFan, 0), Abc_Var2Lit(iValNode, 0), 0 );
pVars[v] = Abc_Var2Lit(iFanVar, 1);
}
pVars[v] = Abc_Var2Lit(iValNode, 1);
// (iFanVar0 & iFanVar1 & iFanVar2) => ~iValNode
nClas += Exa7_AddClause( pFile, pVars, n+1 );
}
}
for ( n = nVars; n < nV; n++ ) {
for ( v = 0; v < n; v++ )
pVars[v] = Abc_Var2Lit(Exa7_GetVar(nV, v, n, 0), 0); // v < n
nClas += Exa7_AddClause( pFile, pVars, n );
if ( GateSize ) {
int Total = 1 << n, Limit = GateSize + 1;
for ( m = 0; m < Total; m++ )
{
if ( Abc_TtCountOnes((word)m) != Limit )
continue;
for ( k = v = 0; v < n; v++ )
if ( (m >> v) & 1 )
pVars[k++] = Abc_Var2Lit(Exa7_GetVar(nV, v, n, 0), 1);
assert( k == Limit );
nClas += Exa7_AddClause( pFile, pVars, Limit );
}
}
}
rewind( pFile );
fprintf( pFile, "p cnf %d %d", nMints * nV * nV, nClas );
fclose( pFile );
return nClas;
}
void Exa_ManDumpVerilog( Vec_Int_t * vValues, int nVars, int nNodes, int GateSize, word * pTruth )
{
FILE * pFile;
char Buffer[1000];
char FileName[1100];
int v, n, k, nV = nVars+nNodes;
Extra_PrintHexadecimalString( Buffer, (unsigned *)pTruth, nVars );
sprintf( FileName, "func%s_%d_%d.v", Buffer, GateSize, nNodes );
pFile = fopen( FileName, "wb" );
fprintf( pFile, "// Realization of the %d-input function %s using %d NAND gates:\n", nVars, Buffer, nNodes );
fprintf( pFile, "module func%s_%d_%d ( input", Buffer, GateSize, nNodes );
for ( v = 0; v < nVars; v++ )
fprintf( pFile, " %c,", 'a'+v );
fprintf( pFile, " output out );\n" );
for ( n = nVars; n < nV; n++ ) {
int nFans = 0;
for ( v = 0; v < n; v++ )
nFans += Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0));
fprintf( pFile, " wire %c = ~(", 'a'+n );
for ( k = v = 0; v < n; v++ )
if ( Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0)) )
fprintf( pFile, "%c%s", 'a'+v, ++k < nFans ? " & ":"" );
fprintf( pFile, ");\n" );
}
fprintf( pFile, " assign out = %c;\n", 'a'+nV-1 );
fprintf( pFile, "endmodule\n\n" );
fclose( pFile );
printf( "Solution was dumped into file \"%s\".\n", FileName );
}
void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize )
{
abctime clkTotal = Abc_Clock();
int v, n, nMints = 1 << pPars->nVars;
int nV = pPars->nVars + pPars->nNodes;
word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
Vec_Int_t * vValues = NULL;
char * pFileNameIn = "_temp_.cnf";
char * pFileNameOut = "_temp_out.cnf";
int nClas = Exa7_ManGenCnf( pFileNameIn, pTruth, pPars->nVars, pPars->nNodes, GateSize );
if ( pPars->fVerbose )
printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", nMints * nV * nV, nClas, pFileNameIn );
vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, pPars->RuntimeLim, pPars->fVerbose );
if ( pPars->fVerbose && vValues ) {
printf( " " );
for ( n = 0; n < nV; n++ )
printf( "%2d ", n );
printf( "\n" );
for ( n = pPars->nVars; n < nV; n++, printf("\n") ) {
printf( "%2d : ", n );
for ( v = 0; v < n; v++ )
printf( " %c ", Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0)) ? '1':'.' ); // v < n
}
}
if ( vValues )
Exa_ManDumpVerilog( vValues, pPars->nVars, pPars->nNodes, GateSize, pTruth );
Vec_IntFreeP( &vValues );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END