From 81fcf8494ead2d2ba18fffab0cb8e54bacf30052 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 12 Aug 2024 16:26:55 -0700 Subject: [PATCH] Updating "lutexact" to support single-rail LUT cascade. --- src/base/abci/abc.c | 8 +++-- src/sat/bmc/bmc.h | 4 ++- src/sat/bmc/bmcMaj.c | 75 +++++++++++++++++++++++++++++++++++++++++++ src/sat/bmc/bmcMaj2.c | 17 ++++++++++ 4 files changed, 101 insertions(+), 3 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 346a1ae923..2c84a9da6f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -9804,7 +9804,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INKTiaogvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INKTiaocgvh" ) ) != EOF ) { switch ( c ) { @@ -9861,6 +9861,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'o': pPars->fFewerVars ^= 1; break; + case 'c': + pPars->fLutCascade ^= 1; + break; case 'g': pPars->fGlucose ^= 1; break; @@ -9907,7 +9910,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutexact [-INKT ] [-iaogvh] \n" ); + Abc_Print( -2, "usage: lutexact [-INKT ] [-iaocgvh] \n" ); Abc_Print( -2, "\t exact synthesis of I-input function using N K-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 K-input nodes [default = %d]\n", pPars->nNodes ); @@ -9916,6 +9919,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "\t-i : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" ); Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" ); + Abc_Print( -2, "\t-c : toggle synthesizing a single-rail cascade [default = %s]\n", pPars->fLutCascade ? "yes" : "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" ); Abc_Print( -2, "\t-h : print the command usage\n" ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 3435635985..795296e6ff 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -62,6 +62,7 @@ struct Bmc_EsPar_t_ int fFewerVars; int fQuadrEnc; int fUniqFans; + int fLutCascade; int RuntimeLim; int fVerbose; char * pTtStr; @@ -84,7 +85,8 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars ) pPars->fEnumSols = 0; pPars->fFewerVars = 0; pPars->fQuadrEnc = 0; - pPars->fUniqFans = 0; + pPars->fUniqFans = 0; + pPars->fLutCascade = 0; pPars->RuntimeLim = 0; pPars->fVerbose = 1; } diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index 5e9c1310ce..06bf93ce4c 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -24,6 +24,8 @@ #include "sat/glucose/AbcGlucose.h" #include "aig/miniaig/miniaig.h" #include "base/io/ioResub.h" +#include "base/main/main.h" +#include "base/cmd/cmd.h" ABC_NAMESPACE_IMPL_START @@ -1045,6 +1047,23 @@ static int Exa3_ManMarkup( Exa3_Man_t * p ) // assign connectivity variables for ( i = p->nVars; i < p->nObjs; i++ ) { + if ( p->pPars->fLutCascade ) + { + if ( i > p->nVars ) + { + Vec_WecPush( p->vOutLits, i-1, Abc_Var2Lit(p->iVar, 0) ); + p->VarMarks[i][0][i-1] = p->iVar++; + } + for ( k = (int)(i > p->nVars); k < p->nLutSize; k++ ) + { + for ( j = 0; j < p->nVars - k + (int)(i > p->nVars); j++ ) + { + Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); + p->VarMarks[i][k][j] = p->iVar++; + } + } + continue; + } for ( k = 0; k < p->nLutSize; k++ ) { if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 ) @@ -3916,6 +3935,62 @@ void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize ) Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Exa_NpnCascadeTest() +{ + char Buffer[100]; + char Command[1000]; int i; + FILE * pFile = fopen( "npn3.txt", "r" ); + for ( i = 0; i < 14; i++ ) +// FILE * pFile = fopen( "npn4.txt", "r" ); +// for ( i = 0; i < 222; i++ ) +// FILE * pFile = fopen( "npn5.txt", "r" ); +// for ( i = 0; i < 616126; i++ ) + { + int Value = fscanf( pFile, "%s", Buffer ); + assert( Value == 1 ); + if ( i == 0 ) continue; + if ( Buffer[strlen(Buffer)-1] == '\n' ) + Buffer[strlen(Buffer)-1] = '\0'; + if ( Buffer[strlen(Buffer)-1] == '\r' ) + Buffer[strlen(Buffer)-1] = '\0'; + sprintf( Command, "lutexact -I 3 -N 2 -K 2 -gvc %s", Buffer+2 ); + printf( "\nNPN class %6d : Command \"%s\":\n", i, Command ); + if ( Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) ) + { + fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); + return; + } + } + fclose( pFile ); +} +void Exa_NpnCascadeTest6() +{ + char Command[1000]; int i; + Abc_Random(1); + for ( i = 0; i < 10000; i++ ) + { + word Truth = Abc_RandomW(0); + sprintf( Command, "lutexact -I 6 -N 2 -K 5 -gvc %016lx", Truth ); + printf( "\nIter %4d : Command \"%s\":\n", i, Command ); + if ( Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) ) + { + fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); + return; + } + } +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c index 32bbc102f4..3025b8a0b6 100644 --- a/src/sat/bmc/bmcMaj2.c +++ b/src/sat/bmc/bmcMaj2.c @@ -944,6 +944,23 @@ static int Exa3_ManMarkup( Exa3_Man_t * p ) // assign connectivity variables for ( i = p->nVars; i < p->nObjs; i++ ) { + if ( p->pPars->fLutCascade ) + { + if ( i > p->nVars ) + { + Vec_WecPush( p->vOutLits, i-1, Abc_Var2Lit(p->iVar, 0) ); + p->VarMarks[i][0][i-1] = p->iVar++; + } + for ( k = (int)(i > p->nVars); k < p->nLutSize; k++ ) + { + for ( j = 0; j < p->nVars - k + (int)(i > p->nVars); j++ ) + { + Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); + p->VarMarks[i][k][j] = p->iVar++; + } + } + continue; + } for ( k = 0; k < p->nLutSize; k++ ) { if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 )