Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

cec: Modifying algorithm for generating simulation vectors for SAT sweeping (SimGen) and adding new feature to specify the simulation vector of the PIs for SAT sweeping algorithm. #353

Merged
merged 9 commits into from
Dec 24, 2024
Merged

cec: Modifying algorithm for generating simulation vectors for SAT sweeping (SimGen) and adding new feature to specify the simulation vector of the PIs for SAT sweeping algorithm. #353

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
463cf6a
[CEC][SimGen][ABC Integration] Removed SAT solver calls and saving th…
Carmine50 Dec 24, 2024
1a89f7f
[CEC][SimGen][CLI] Changed function name and help message. Added new …
Carmine50 Dec 24, 2024
0ba2b7d
[CEC][SimGen][Clean codes] Removing unused parameters.
Carmine50 Dec 24, 2024
699c8c4
[CEC][SimGen][Clean codes] Removing commented SAT calls operations.
Carmine50 Dec 24, 2024
37979db
[CEC][SimGen][Clean codes] Removing commented SAT calls operations.
Carmine50 Dec 24, 2024
7c6d1ff
[CEC][SimGen][Bugs] Fixing bugs and removing unused var.
Carmine50 Dec 24, 2024
5961231
[CEC][SimGen][Clean codes] Disabling verbose.
Carmine50 Dec 24, 2024
64e8bb0
[CEC][SimGen][Bits to Words] Changing the units of measure for random…
Carmine50 Dec 24, 2024
a74da1c
[CEC][SAT Sweeping] Added new functionality in SAT sweeping function …
Carmine50 Dec 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 23 additions & 13 deletions src/base/abci/abc.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -477,7 +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_CommandAbc9AdvGenSim ( 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 );
Expand Down Expand Up @@ -1277,7 +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", "&adv_sim_gen", Abc_CommandAbc9AdvGenSim, 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 );
Expand Down Expand Up @@ -39179,7 +39179,7 @@ int Abc_CommandAbc9SatEnum( Abc_Frame_t * pAbc, int argc, char ** argv )

/**Function*************************************************************

Synopsis [Abc_CommandAbc9SimGen]
Synopsis [Abc_CommandAbc9AdvGenSim]

Description [This function calls SimGen tool]

Expand All @@ -39189,7 +39189,7 @@ int Abc_CommandAbc9SatEnum( Abc_Frame_t * pAbc, int argc, char ** argv )

***********************************************************************/

int Abc_CommandAbc9SimGen( Abc_Frame_t * pAbc, int argc, char ** argv )
int Abc_CommandAbc9AdvGenSim( 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 );
Expand All @@ -39198,7 +39198,7 @@ int Abc_CommandAbc9SimGen( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Cec_SimGenSetParDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "EOStiwvV" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "EOStiFwvV" ) ) != EOF )
{
switch ( c )
{
Expand Down Expand Up @@ -39230,9 +39230,9 @@ int Abc_CommandAbc9SimGen( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->bitwidthSim = atoi(argv[globalUtilOptind]);
pPars->nSimWords = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->bitwidthSim <= 0 )
if ( pPars->nSimWords <= 0 )
goto usage;
break;
case 't':
Expand All @@ -39257,6 +39257,15 @@ int Abc_CommandAbc9SimGen( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nMaxIter <= -2 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by a string.\n" );
goto usage;
}
pPars->pFileName = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'w':
pPars->fUseWatchlist = 1;
break;
Expand Down Expand Up @@ -39287,13 +39296,14 @@ int Abc_CommandAbc9SimGen( Abc_Frame_t * pAbc, int argc, char ** argv )
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, "usage: &adv_sim_gen [-EOSsivV <num>] [-v] \n" );
Abc_Print( -2, "\t generates simulation patterns for combinational SAT sweeping\n" );
Abc_Print( -2, "\t-E num : the experiment ID for different techniques [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-S num : the number of words in a round for random simulation [default = %d]\n", pPars->nSimWords );
Abc_Print( -2, "\t-t num : the timeout value [default = %.0f]\n", pPars->timeOutSim);
Abc_Print( -2, "\t-i num : the number of rounds of random simulation [default = %d]\n", pPars->nMaxIter );
Abc_Print( -2, "\t-F file: the file name to dump the generated patterns [default = none]\n");
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 );
Expand Down
6 changes: 3 additions & 3 deletions src/proof/cec/cec.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -209,8 +209,8 @@ struct Cec_ParSimGen_t_
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
int nSimWords; // number of words in a round of random simulation
int nMaxIter; // maximum number of rounds of random simulation
char * outGold; // data containing outgold
float timeOutSim; // timeout for simulation
int fUseWatchlist; // use watchlist
Expand All @@ -219,7 +219,7 @@ struct Cec_ParSimGen_t_
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
char * pFileName; // file name to dump simulation vectors
};

////////////////////////////////////////////////////////////////////////
Expand Down
Loading
Loading