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

Adding new feature to "lutexact".

This commit is contained in:
Alan Mishchenko 2025-05-01 21:08:46 -07:00
parent 391a767c16
commit 1c2b935a77
3 changed files with 82 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -10548,7 +10548,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, "INKTFMSYiaocgvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "INKTFMSYiaocfgvh" ) ) != EOF )
{
switch ( c )
{
@ -10646,6 +10646,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
pPars->fLutCascade ^= 1;
break;
case 'f':
pPars->fLutInFixed ^= 1;
break;
case 'g':
pPars->fGlucose ^= 1;
break;
@ -10701,7 +10704,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: lutexact [-INKTFMS <num>] [-Y string] [-iaocgvh] <hex>\n" );
Abc_Print( -2, "usage: lutexact [-INKTFMS <num>] [-Y string] [-iaocfgvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of I-input function using N K-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 K-input nodes [default = %d]\n", pPars->nNodes );
@ -10715,6 +10718,7 @@ usage:
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-f : toggle fixing LUT inputs in cascade mapping [default = %s]\n", pPars->fLutInFixed ? "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" );

1
src/sat/bmc/bmc.h
View File

@ -64,6 +64,7 @@ struct Bmc_EsPar_t_
int fQuadrEnc;
int fUniqFans;
int fLutCascade;
int fLutInFixed;
int RuntimeLim;
int nRandFuncs;
int nMintNum;

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

@ -1009,6 +1009,7 @@ struct Exa3_Man_t_
int VarMarks[MAJ_NOBJS][6][MAJ_NOBJS]; // variable marks
int VarVals[MAJ_NOBJS]; // values of the first nVars variables
Vec_Wec_t * vOutLits; // output vars
Vec_Wec_t * vInVars; // input vars
bmcg_sat_solver * pSat; // SAT solver
int nUsed[2];
};
@ -1040,6 +1041,54 @@ static inline int Exa3_ManIsUsed3( Exa3_Man_t * p, int m, int n, int i, int
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wec_t * Exa3_ChooseInputVars_int( int nVars, int nLuts, int nLutSize )
{
Vec_Wec_t * p = Vec_WecStart( nLuts );
Vec_Int_t * vLevel; int i;
Vec_WecForEachLevel( p, vLevel, i ) {
do {
int iVar = (Abc_Random(0) ^ Abc_Random(0) ^ Abc_Random(0)) % nVars;
Vec_IntPushUniqueOrder( vLevel, iVar );
}
while ( Vec_IntSize(vLevel) < nLutSize-(int)(i>0) );
}
return p;
}
Vec_Int_t * Exa3_CountInputVars( int nVars, Vec_Wec_t * p )
{
Vec_Int_t * vLevel; int i, k, Obj;
Vec_Int_t * vCounts = Vec_IntStart( nVars );
Vec_WecForEachLevel( p, vLevel, i )
Vec_IntForEachEntry( vLevel, Obj, k )
Vec_IntAddToEntry( vCounts, Obj, 1 );
return vCounts;
}
Vec_Wec_t * Exa3_ChooseInputVars( int nVars, int nLuts, int nLutSize )
{
for ( int i = 0; i < 1000; i++ ) {
Vec_Wec_t * p = Exa3_ChooseInputVars_int( nVars, nLuts, nLutSize );
Vec_Int_t * q = Exa3_CountInputVars( nVars, p );
int RetValue = Vec_IntFind( q, 0 );
Vec_IntFree( q );
if ( RetValue == -1 )
return p;
Vec_WecFree( p );
}
assert( 0 );
return NULL;
}
/**Function*************************************************************
Synopsis []
@ -1102,6 +1151,19 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
}
}
printf( "The number of parameter variables = %d.\n", p->iVar );
if ( p->pPars->fLutCascade && p->pPars->fLutInFixed ) {
p->vInVars = Exa3_ChooseInputVars( p->nVars, p->nNodes, p->nLutSize );
if ( 1 ) {
Vec_Int_t * vLevel; int i, Var;
printf( "Using fixed input assignment:\n" );
Vec_WecForEachLevelReverse( p->vInVars, vLevel, i ) {
printf( "%02d : ", p->nVars+i );
Vec_IntForEachEntry( vLevel, Var, k )
printf( "%c ", 'a'+Var );
printf( "\n" );
}
}
}
return p->iVar;
// printout
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
@ -1148,6 +1210,7 @@ static void Exa3_ManFree( Exa3_Man_t * p )
Vec_BitFreeP( &p->vUsed2 );
Vec_BitFreeP( &p->vUsed3 );
Vec_WecFree( p->vOutLits );
Vec_WecFreeP( &p->vInVars );
ABC_FREE( p );
}
@ -1396,6 +1459,18 @@ static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
if ( !bmcg_sat_solver_addclause( p->pSat, Vec_IntArray(vArray), Vec_IntSize(vArray) ) )
return 0;
}
if ( p->vInVars ) {
Vec_Int_t * vLevel; int Var;
Vec_WecForEachLevel( p->vInVars, vLevel, i )
{
assert( Vec_IntSize(vLevel) > 0 );
Vec_IntForEachEntry( vLevel, Var, k ) {
pLits[0] = Abc_Var2Lit( p->VarMarks[p->nVars+i][p->nLutSize-1-k][Var], 0 ); assert(pLits[0]);
if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 1 ) )
return 0;
}
}
}
return 1;
}
static int Exa3_ManAddCnf( Exa3_Man_t * p, int iMint )