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

Supporting random seed in "lutexact".

This commit is contained in:
Alan Mishchenko 2025-04-30 12:10:22 -07:00
parent 59bb4de39f
commit 6a031620fe
3 changed files with 32 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
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, "INKTSFMiaocgvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "INKTFMSYiaocgvh" ) ) != EOF )
{
switch ( c )
{
@ -10596,15 +10596,6 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->RuntimeLim < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->pSymStr = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
@ -10623,6 +10614,26 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nMintNum = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->Seed = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->Seed < 0 )
goto usage;
break;
case 'Y':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-Y\" should be followed by a string.\n" );
goto usage;
}
pPars->pSymStr = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'i':
pPars->fUseIncr ^= 1;
break;
@ -10690,7 +10701,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: lutexact [-INKTFM <num>] [-S string] [-iaocgvh] <hex>\n" );
Abc_Print( -2, "usage: lutexact [-INKTFMS <num>] [-Y string] [-iaocgvh] <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 );
@ -10698,7 +10709,8 @@ usage:
Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim );
Abc_Print( -2, "\t-F <num> : the number of random functions to try [default = unused]\n" );
Abc_Print( -2, "\t-M <num> : the number of positive minterms in the random function [default = unused]\n" );
Abc_Print( -2, "\t-S <str> : charasteristic string of a symmetric function [default = %d]\n", pPars->pSymStr );
Abc_Print( -2, "\t-S <num> : the random seed for random function generation with -F <num> [default = %d]\n", pPars->Seed );
Abc_Print( -2, "\t-Y <str> : charasteristic string of a symmetric function [default = %d]\n", pPars->pSymStr );
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" );

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

@ -67,6 +67,7 @@ struct Bmc_EsPar_t_
int RuntimeLim;
int nRandFuncs;
int nMintNum;
int Seed;
int fVerbose;
char * pTtStr;
char * pSymStr;

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

@ -1580,18 +1580,19 @@ int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
void Exa3_ManExactSynthesisRand( Bmc_EsPar_t * pPars )
{
int i, k, nDecs = 0, nWords = Abc_TtWordNum(pPars->nVars);
word * pFun = ABC_ALLOC( word, nWords );
Abc_Random(1);
printf( "\n" );
word * pFun = ABC_ALLOC( word, nWords );
unsigned Rand0 = Abc_Random(1);
for ( i = 0; i < pPars->Seed; i++ )
Rand0 = Abc_Random(0);
for ( i = 0; i < pPars->nRandFuncs; i++ ) {
if ( pPars->nMintNum == 0 )
for ( k = 0; k < nWords; k++ )
pFun[k] = Abc_RandomW(0);
pFun[k] = Rand0 ^ Abc_RandomW(0);
else {
Abc_TtClear( pFun, nWords );
for ( k = 0; k < pPars->nMintNum; k++ ) {
int iMint = 0;
do iMint = Abc_Random(0) % (1 << pPars->nVars);
do iMint = (Rand0 ^ Abc_Random(0)) % (1 << pPars->nVars);
while ( Abc_TtGetBit(pFun, iMint) );
Abc_TtSetBit( pFun, iMint );
}
@ -1607,7 +1608,7 @@ void Exa3_ManExactSynthesisRand( Bmc_EsPar_t * pPars )
nDecs += Exa3_ManExactSynthesis( pPars );
ABC_FREE( pPars->pTtStr );
}
printf( "Decomposable are %d (out of %d) functions (%.2f %%).\n", nDecs, pPars->nRandFuncs, 100.0*nDecs/pPars->nRandFuncs );
printf( "\nDecomposable are %d (out of %d) functions (%.2f %%).\n", nDecs, pPars->nRandFuncs, 100.0*nDecs/pPars->nRandFuncs );
ABC_FREE( pFun );
}