Skip to content

Commit

Permalink
[CEC][SimGen][CLI] Changed function name and help message. Added new …
Browse files Browse the repository at this point in the history 
…option to specify file where to dump simulation vectors. Commented out too verbose information
  • Loading branch information
@Carmine50
Carmine50 committed Dec 24, 2024
1 parent 463cf6a commit 1a89f7f
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 11 deletions.
30 changes: 20 additions & 10 deletions src/base/abci/abc.c
View file
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 @@ -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-S num : the bitwidth of the simulation vectors for random simulation [default = %d]\n", pPars->bitwidthSim );
Abc_Print( -2, "\t-t num : the timeout value [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-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
1 change: 1 addition & 0 deletions src/proof/cec/cec.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -220,6 +220,7 @@ struct Cec_ParSimGen_t_
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
7 changes: 6 additions & 1 deletion src/proof/cec/cecSatG2.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -254,6 +254,7 @@ void Cec_SimGenSetParDefault( Cec_ParSimGen_t * pPars )
pPars->nImplicationSuccessChecks = 0; // the number of implication successful checks
pPars->pCECPars = (Cec_ParFra_t *) malloc(sizeof( Cec_ParFra_t )); // parameters of CEC
Cec4_ManSetParams( pPars->pCECPars );
pPars->pFileName = NULL; // file name to dump simulation vectors
}

/**Function*************************************************************
Expand Down Expand Up @@ -4380,6 +4381,7 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){

Cec_DeriveSOPs( pMapped );

/*
if (pPars->fVeryVerbose)
{
printf("**Printing LUTs information**\n");
Expand All @@ -4391,6 +4393,7 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){
printISOPLUT( pMapped, i );
}
}
*/

// compute MFFCs
Gia_ManLevelNum( pMapped); // compute levels
Expand Down Expand Up @@ -4469,7 +4472,9 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){
}
p->nSimWords = nWordsPerCi;

//Vec_WrdDumpHex( "sim_vec.out", p->vSimsPi, nWordsPerCi , 1 );
if (pPars->pFileName != NULL){
Vec_WrdDumpHex( pPars->pFileName, p->vSimsPi, nWordsPerCi , 1 );
}

// call SAT solver
/*
Expand Down

0 comments on commit 1a89f7f

Please sign in to comment.