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

Updating "lutexact" to support single-rail LUT cascade.

This commit is contained in:
Alan Mishchenko 2024-08-12 16:26:55 -07:00
parent 807f6ddacf
commit 81fcf8494e
4 changed files with 101 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -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 <num>] [-iaogvh] <hex>\n" );
Abc_Print( -2, "usage: lutexact [-INKT <num>] [-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 );
@ -9916,6 +9919,7 @@ usage:
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" );

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

@ -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;
}

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

@ -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 ///
////////////////////////////////////////////////////////////////////////

17
src/sat/bmc/bmcMaj2.c
View File

@ -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 )