diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 426f90fd5..c4cdfa202 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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 ); @@ -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 ); @@ -39179,7 +39179,7 @@ usage: /**Function************************************************************* - Synopsis [Abc_CommandAbc9SimGen] + Synopsis [Abc_CommandAbc9AdvGenSim] Description [This function calls SimGen tool] @@ -39189,7 +39189,7 @@ usage: ***********************************************************************/ -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 ); @@ -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 ) { @@ -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; @@ -39287,13 +39296,14 @@ int Abc_CommandAbc9SimGen( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &fraigSimGen [-EOSsivV ] [-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 ] [-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 ); diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index 4db2df726..3ef5454e1 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -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 }; //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 1a27162ee..2e25ff249 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -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************************************************************* @@ -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"); @@ -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 @@ -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 /*