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

Merge pull request #351 from Carmine50/master 

cec: Adding new algorithm for generating simulation vectors for SAT sweeping (SimGen)
This commit is contained in:
alanminko 2024-12-21 15:02:29 -08:00 committed by GitHub
parent 8ba3d9b91c ef8c35f95d
commit df4d847bbf
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
5 changed files with 2368 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/aig/gia/gia.h
View File

@ -249,6 +249,11 @@ struct Gia_Man_t_
int iFirstPoId;
int iFirstAndObj;
int iFirstPoObj;
Vec_Str_t * vTTISOPs; // truth tables from ISOP computation
Vec_Int_t * vTTLut; // truth tables from ISOP computation
Vec_Int_t * vMFFCsInfo; // MFFC information
Vec_Int_t * vMFFCsLuts; // MFFCs for each lut
Vec_Ptr_t * vLutsRankings; // LUTs rankings of inputs
};
@ -1843,6 +1848,8 @@ extern void Bnd_ManPrintStats();
// util
extern Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec_Bit_t* vEI_phase, Vec_Bit_t* vEO_phase );
extern int Gia_ObjCheckMffc( Gia_Man_t * p, Gia_Obj_t * pRoot, int Limit, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t * vInners );
ABC_NAMESPACE_HEADER_END

2
src/aig/gia/giaResub.c
View File

@ -68,7 +68,7 @@ int Gia_ObjCheckMffc_rec( Gia_Man_t * p,Gia_Obj_t * pObj, int Limit, Vec_Int_t *
return 0;
return 1;
}
static inline int Gia_ObjCheckMffc( Gia_Man_t * p, Gia_Obj_t * pRoot, int Limit, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t * vInners )
int Gia_ObjCheckMffc( Gia_Man_t * p, Gia_Obj_t * pRoot, int Limit, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t * vInners )
{
int RetValue, iObj, i;
Vec_IntClear( vNodes );

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

@ -477,6 +477,7 @@ static int Abc_CommandAbc9Scorr ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Choice ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatEnum ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SimGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9CFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Srm ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1276,6 +1277,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&choice", Abc_CommandAbc9Choice, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sat", Abc_CommandAbc9Sat, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&satenum", Abc_CommandAbc9SatEnum, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&fraigSimGen", Abc_CommandAbc9SimGen, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&fraig", Abc_CommandAbc9Fraig, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cfraig", Abc_CommandAbc9CFraig, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&srm", Abc_CommandAbc9Srm, 0 );
@ -39175,6 +39177,130 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis [Abc_CommandAbc9SimGen]
Description [This function calls SimGen tool]
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9SimGen( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Cec_SimGenSetParDefault( Cec_ParSimGen_t * pPars );
extern Gia_Man_t * Cec_SimGenRun( Gia_Man_t * pAig, Cec_ParSimGen_t * pPars );
Cec_ParSimGen_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
int c;
Cec_SimGenSetParDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "EOStiwvV" ) ) != EOF )
{
switch ( c )
{
case 'E':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-E\" should be followed by an integer.\n" );
goto usage;
}
pPars->expId = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->expId < 0 )
goto usage;
break;
case 'O':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
goto usage;
}
pPars->bitwidthOutgold = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->bitwidthOutgold <= 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->bitwidthSim = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->bitwidthSim <= 0 )
goto usage;
break;
case 't':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-t\" should be followed by an integer.\n" );
goto usage;
}
pPars->timeOutSim = atof(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->timeOutSim <= 0 )
goto usage;
break;
case 'i':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-i\" should be followed by an integer.\n" );
goto usage;
}
pPars->nMaxIter = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nMaxIter <= -2 )
goto usage;
break;
case 'w':
pPars->fUseWatchlist = 1;
break;
case 'v':
pPars->fVerbose = 1;
break;
case 'V':
pPars->fVeryVerbose = 1;
break;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Fraig(): There is no AIG.\n" );
return 1;
}
pTemp = Cec_SimGenRun(pAbc->pGia, pPars );
if ( pAbc->pGia->pCexSeq != NULL )
{
pAbc->Status = 0;
pAbc->nFrames = 0;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
}
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &fraigSimGen [-EOSsivV <num>] [-v] \n" );
Abc_Print( -2, "\t performs combinational SAT sweeping applying SimGen\n" );
Abc_Print( -2, "\t-E num : the experiment ID for SimGen [default = %d]\n", pPars->expId );
Abc_Print( -2, "\t-O num : the bitwidth of the output gold [default = %d]\n", pPars->bitwidthOutgold );
Abc_Print( -2, "\t-S num : the bitwidth of the simulation vectors [default = %d]\n", pPars->bitwidthSim );
Abc_Print( -2, "\t-t num : the timeout value after which Smart Simulation Pattern Generation terminates [default = %.0f]\n", pPars->timeOutSim);
Abc_Print( -2, "\t-i num : the maximum number of iterations [default = %d]\n", pPars->nMaxIter );
Abc_Print( -2, "\t-w : activates the watchlist feature [default = %d]\n", pPars->fUseWatchlist);
Abc_Print( -2, "\t-v : verbose [default = %d]\n", pPars->fVerbose );
Abc_Print( -2, "\t-V : very verbose [default = %d]\n", pPars->fVeryVerbose );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []

21
src/proof/cec/cec.h
View File

@ -201,6 +201,27 @@ struct Cec_ParSeq_t_
int fVerbose; // verbose stats
};
// CEC SimGen parameters
typedef struct Cec_ParSimGen_t_ Cec_ParSimGen_t;
struct Cec_ParSimGen_t_
{
int fVerbose; // verbose flag
int fVeryVerbose; // verbose flag
int expId; // experiment ID for SimGen
int bitwidthOutgold; // bitwidth of the output gold
int bitwidthSim; // bitwidth of the simulation vectors
int nMaxIter; // maximum number of iterations
char * outGold; // data containing outgold
float timeOutSim; // timeout for simulation
int fUseWatchlist; // use watchlist
float fImplicationTime; // time spent in implication
int nImplicationExecution; // number of times implication was executed
int nImplicationSuccess; // number of times implication was successful
int nImplicationTotalChecks; // number of times implication was checked
int nImplicationSuccessChecks; // number of times implication was successful
Cec_ParFra_t * pCECPars; // parameters of CEC
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////

2213
src/proof/cec/cecSatG2.c
View File

File diff suppressed because it is too large Load Diff