From b0d2ff1c63106626246adea908511a8c94c4a280 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 24 Mar 2024 00:10:08 +0900 Subject: [PATCH] Exact synthesis using NAND-gates. --- src/base/abc/abc.h | 2 +- src/base/abci/abc.c | 41 ++++++++-- src/base/abci/abcPrint.c | 12 ++- src/sat/bmc/bmcMaj.c | 162 ++++++++++++++++++++++++++++++++++++++- 4 files changed, 205 insertions(+), 12 deletions(-) diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 5cf7a0f59..58131f185 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -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 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b9535f423..66af8713a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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] \n" ); + Abc_Print( -2, "usage: print_level [-npovh] \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 ] [-adconugklvh] \n" ); + Abc_Print( -2, "usage: twoexact [-INTG ] [-abdconugklvh] \n" ); Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" ); Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N : the number of two-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); + Abc_Print( -2, "\t-G : 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" ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index e90159d2a..636665249 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -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; diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index d3a3ac18d..40ecd4a5e 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -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