From 463cf6a7df6f6ac9da1b1b9756ece647c897d046 Mon Sep 17 00:00:00 2001 From: Carmine50 Date: Tue, 24 Dec 2024 11:06:00 +0100 Subject: [PATCH 1/9] [CEC][SimGen][ABC Integration] Removed SAT solver calls and saving the simulation vectors in an internal data structure to pass to other functions. --- src/proof/cec/cecSatG2.c | 116 +++++++++++++++++++++++++++++++++++---- 1 file changed, 104 insertions(+), 12 deletions(-) diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 33259bfe4..1a27162ee 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -2942,6 +2942,37 @@ int totalNumClasses(Gia_Man_t * p){ return numClasses; } +/**Function************************************************************* + + Synopsis [Save PI simulation values.] + + Description [] + + SideEffects [] + + SeeAlso [] + +************************************************************************/ + +void saveSimVectors( Gia_Man_t * p, Vec_Ptr_t * pValues, int bitLength, int jth_word, int kth_bit){ + + int i, Id; + int nWords = bitLength / 64; + assert(nWords == 0); // Not considering case with large outgold values + Gia_ManForEachCiId( p, Id, i ){ + Vec_Wrd_t * pValuesPi = Vec_PtrEntry( pValues, i ); + word pValuePiJWord = 0; + if(kth_bit == 0){ + Vec_WrdPush( pValuesPi, 0 ); + } else { + pValuePiJWord = Vec_WrdEntry( pValuesPi, jth_word ); + } + word * pSim = Cec4_ObjSim( p, Id ); + pValuePiJWord = (pSim[0] << kth_bit) ^ pValuePiJWord; + Vec_WrdWriteEntry( pValuesPi, jth_word, pValuePiJWord ); + } +} + /**Function************************************************************* Synopsis [Simulate the CIs with random values.] @@ -2954,10 +2985,10 @@ int totalNumClasses(Gia_Man_t * p){ ************************************************************************/ -void executeRandomSim( Gia_Man_t * p, Cec4_Man_t * pMan , int dynSim, int nMaxIter , int bitwidthSim , int verbose ){ +void executeRandomSim( Gia_Man_t * p, Cec4_Man_t * pMan , int dynSim, int nMaxIter , int bitwidthSim , Vec_Ptr_t * vSimSave, int verbose ){ clock_t start_time = clock(); - int i; + int i, j, k, Id; int numClass = 100000; int oldNumClass = 0, iMaxNumber = 200, iNumber = 0; if(dynSim){ @@ -2971,6 +3002,13 @@ void executeRandomSim( Gia_Man_t * p, Cec4_Man_t * pMan , int dynSim, int nMaxIt printf("Time elapsed: %f (classes size: %d)\n", (float)(clock() - start_time)/CLOCKS_PER_SEC, quality); numClass = totalNumClasses(p); iNumber++; + Gia_ManForEachCiId( p, Id, j ){ + Vec_Wrd_t * vSimPI = Vec_PtrEntry( vSimSave, j ); + word * pSim = Cec4_ObjSim( p, Id ); + for( k = 0; k < p->nSimWords; k++ ){ + Vec_WrdPush( vSimPI, pSim[k] ); + } + } } @@ -2982,6 +3020,13 @@ void executeRandomSim( Gia_Man_t * p, Cec4_Man_t * pMan , int dynSim, int nMaxIt Cec_RemoveNonLutNodes( p ); if (verbose) printf("Time elapsed: %f (classes size: %d)\n", (float)(clock() - start_time)/CLOCKS_PER_SEC, quality); + Gia_ManForEachCiId( p, Id, j ){ + Vec_Wrd_t * vSimPI = Vec_PtrEntry( vSimSave, j ); + word * pSim = Cec4_ObjSim( p, Id ); + for( k = 0; k < p->nSimWords; k++ ){ + Vec_WrdPush( vSimPI, pSim[k] ); + } + } } } } @@ -3893,7 +3938,7 @@ void exportSimValues( Gia_Man_t * p, char * filename ) ************************************************************************/ -int computeInputVectors(Gia_Man_t * p, Cec4_Man_t * pMan, Cec_ParSimGen_t * pPars , Vec_Int_t * vLuts , char * outGold, int outGold_bitwidth , Vec_Int_t * vLutsFaninCones , Vec_Ptr_t * vNodesWatchlist , int experimentID){ +int computeInputVectors(Gia_Man_t * p, Cec4_Man_t * pMan, Cec_ParSimGen_t * pPars , Vec_Int_t * vLuts , char * outGold, int outGold_bitwidth , Vec_Int_t * vLutsFaninCones , Vec_Ptr_t * vNodesWatchlist , Vec_Ptr_t * vSimSave ,int experimentID){ char * networkValues1s, * networkValuesNotSet; // data structure containing the values inside the network char networkValid = (char) (1 << outGold_bitwidth) - 1; // keeps track which array out of the 8 is valid @@ -4010,6 +4055,16 @@ int computeInputVectors(Gia_Man_t * p, Cec4_Man_t * pMan, Cec_ParSimGen_t * pPar if(success >= 2){ saveInputVectors(p, pMan, networkValues1s); Cec4_ManSimulate( p, pMan ); + // saving the pi simulation values in a compacted format + int jth_word = p->iData & 0xFFFF; + int kth_bit = (p->iData & 0xFFFF0000) >> 16; + if( kth_bit + outGold_bitwidth >= 64 ){ + kth_bit = 0; + jth_word += 1; + } + saveSimVectors(p, vSimSave, outGold_bitwidth, jth_word, kth_bit); + kth_bit += outGold_bitwidth; + p->iData = (kth_bit << 16) | jth_word; if( pPars->fVerbose || pPars->fVeryVerbose){ printf("**Exporting simulation values in file sim_values.txt\n"); exportSimValues( p, "sim_values.txt" ); @@ -4042,7 +4097,7 @@ exit_cond: ***********************************************************************/ -void executeControlledSim(Gia_Man_t * p, Cec4_Man_t * pMan, Cec_ParSimGen_t * pPars , int levelOrder, int experimentID){ +void executeControlledSim(Gia_Man_t * p, Cec4_Man_t * pMan, Cec_ParSimGen_t * pPars , int levelOrder, Vec_Ptr_t * vSimSave, int experimentID){ char * outGold; //int outGold_bitwidth = pPars->bitwidthOutgold; @@ -4069,7 +4124,7 @@ void executeControlledSim(Gia_Man_t * p, Cec4_Man_t * pMan, Cec_ParSimGen_t * pP if(pPars->fUseWatchlist){ vNodesWatchList = generateWatchList(p); } - status = computeInputVectors(p, pMan, pPars, luts_order, outGold, pPars->bitwidthOutgold, vLutsFaninCones, vNodesWatchList, experimentID); + status = computeInputVectors(p, pMan, pPars, luts_order, outGold, pPars->bitwidthOutgold, vLutsFaninCones, vNodesWatchList, vSimSave, experimentID); if( status == -1 ){ if(pPars->fVerbose || pPars->fVeryVerbose) printf("FAILED - no valid input vectors found for class %d\n", nthClass); @@ -4303,8 +4358,9 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ extern void Gia_ManDupMapping( Gia_Man_t * pNew, Gia_Man_t * p ); Cec4_Man_t * pManSim; - int i, k, iFan; + int i, k, iFan, nWordsPerCi; Gia_Man_t * pMapped; + Vec_Ptr_t * vSimPisSave; if (!Gia_ManHasMapping(p)){ // apply technology mapping if not already done @@ -4347,17 +4403,29 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ // generate vectors of fanouts Gia_generateFanoutMapping( pMapped ); - // simulate n rounds of random simulation and create classes - Cec4_ManSimAlloc( pMapped, 1 ); + assert( pPars->bitwidthSim > 0); + pMapped->nSimWords = (int) pPars->bitwidthSim / 64 + ((pPars->bitwidthSim % 64) > 0); + vSimPisSave = Vec_PtrAlloc( Gia_ManCiNum(pMapped) ); + for ( i = 0; i < Gia_ManCiNum(pMapped); i++ ){ + Vec_Wrd_t * vSim = Vec_WrdAlloc( pMapped->nSimWords ); + Vec_PtrPush( vSimPisSave, vSim ); + } + // simulate n rounds of random simulation and create classes + Cec4_ManSimAlloc( pMapped, pMapped->nSimWords ); if(pPars->nMaxIter >= 0){ - executeRandomSim( pMapped, pManSim, 0, pPars->nMaxIter, pPars->bitwidthSim , pPars->fVeryVerbose); + executeRandomSim( pMapped, pManSim, 0, pPars->nMaxIter, pPars->bitwidthSim , vSimPisSave, pPars->fVeryVerbose); } else if (pPars->nMaxIter == -1){ - executeRandomSim( pMapped, pManSim, 1, pPars->nMaxIter, pPars->bitwidthSim , pPars->fVeryVerbose); + executeRandomSim( pMapped, pManSim, 1, pPars->nMaxIter, pPars->bitwidthSim , vSimPisSave, pPars->fVeryVerbose); } else { printf("Invalid number of iterations %d\n", pPars->nMaxIter); return NULL; } + // extra data to compact multiple pi values in single words + pMapped->iData = ((Vec_Wrd_t *)Vec_PtrEntry( vSimPisSave, 0 ))->nSize; // [0:15] number of words filled + // [16:31] number of bits filled in the iData word + assert(pMapped->iData > 0); + Cec_RemoveNonLutNodes( pMapped ); // remove all the non-LUT nodes from the equivalence classes if(pPars->fVerbose || pPars->fVeryVerbose){ @@ -4369,7 +4437,7 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ //Cec4_ManPrintClasses2(pMapped); clock_t begin = clock(); assert(pPars->expId > 0); - executeControlledSim( pMapped, pManSim, pPars, -1 , pPars->expId ); + executeControlledSim( pMapped, pManSim, pPars, -1 , vSimPisSave, pPars->expId ); float implicationSuccessRate = (float)pPars->nImplicationSuccess / (float)pPars->nImplicationExecution; float implicationSuccessCheckRate = (float)pPars->nImplicationSuccessChecks / (float)pPars->nImplicationTotalChecks; @@ -4382,11 +4450,35 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ evaluate_equiv_classes(pMapped, 1); } + // save random and controlled sim pis values + if(p->vSimsPi != NULL){ + Vec_WrdFree( p->vSimsPi ); + } + nWordsPerCi = ((Vec_Wrd_t *)Vec_PtrEntry( vSimPisSave, 0 ))->nSize; + assert( nWordsPerCi > 0 ); + p->vSimsPi = Vec_WrdStart( Gia_ManCiNum(p) * nWordsPerCi ); + // copy the sim pis + assert( Gia_ManCiNum(p) == Vec_PtrSize(vSimPisSave) ); + for (i = 0; i < Gia_ManCiNum(p); i++){ + Vec_Wrd_t * vSim = (Vec_Wrd_t *)Vec_PtrEntry( vSimPisSave, i ); + assert( vSim->nSize == nWordsPerCi ); + word * pSim = Vec_WrdEntryP( p->vSimsPi, i * nWordsPerCi ); + for ( k = 0; k < nWordsPerCi; k++ ) + pSim[k] = Vec_WrdEntry( vSim, k ); + } + p->nSimWords = nWordsPerCi; + + //Vec_WrdDumpHex( "sim_vec.out", p->vSimsPi, nWordsPerCi , 1 ); // call SAT solver + /* Cec4_CallSATsolver(pMapped, pManSim, pPars->pCECPars); - + Gia_Man_t * ppNew; Gia_Obj_t * pObj; + Gia_ManForEachCo( pMapped, pObj, i ) + pObj->Value = Gia_ManAppendCo( pManSim->pNew, Gia_ObjFanin0Copy(pObj) ); + ppNew = Gia_ManCleanup( pManSim->pNew ); + */ if (pPars->fVerbose || pPars->fVeryVerbose){ pManSim->pPars->fVerbose = 1; // print the ending stats of sat calls } From 1a89f7ff63d7ce6349b9ef4eb7edf6c9a4b7fb2c Mon Sep 17 00:00:00 2001 From: Carmine50 Date: Tue, 24 Dec 2024 11:43:18 +0100 Subject: [PATCH 2/9] [CEC][SimGen][CLI] Changed function name and help message. Added new option to specify file where to dump simulation vectors. Commented out too verbose information --- src/base/abci/abc.c | 30 ++++++++++++++++++++---------- src/proof/cec/cec.h | 1 + src/proof/cec/cecSatG2.c | 7 ++++++- 3 files changed, 27 insertions(+), 11 deletions(-) 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 /* From 0ba2b7dae903318f046e7e2aae8c014550152fe7 Mon Sep 17 00:00:00 2001 From: Carmine50 Date: Tue, 24 Dec 2024 11:49:17 +0100 Subject: [PATCH 3/9] [CEC][SimGen][Clean codes] Removing unused parameters. --- src/proof/cec/cec.h | 1 - src/proof/cec/cecSatG2.c | 6 +++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index 3ef5454e1..fe1a2d518 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -219,7 +219,6 @@ 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 }; diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 2e25ff249..fab871f4a 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -252,8 +252,6 @@ void Cec_SimGenSetParDefault( Cec_ParSimGen_t * pPars ) pPars->nImplicationSuccess = 0; // the number of implication successes pPars->nImplicationTotalChecks = 0; // the number of implication checks 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 } @@ -4362,6 +4360,7 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ int i, k, iFan, nWordsPerCi; Gia_Man_t * pMapped; Vec_Ptr_t * vSimPisSave; + Cec_ParFra_t * pCECPars; if (!Gia_ManHasMapping(p)){ // apply technology mapping if not already done @@ -4377,7 +4376,8 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ if(pPars->fVerbose) printf("Using already mapped network\n"); } - pManSim = Cec4_ManCreate( pMapped, pPars->pCECPars ); + pCECPars = (Cec_ParFra_t *) malloc(sizeof( Cec_ParFra_t )); // parameters of CEC + pManSim = Cec4_ManCreate( pMapped, pCECPars ); Cec_DeriveSOPs( pMapped ); From 699c8c4c889a0cc1f9b7c31ad017995b80d77dd0 Mon Sep 17 00:00:00 2001 From: Carmine50 Date: Tue, 24 Dec 2024 11:50:11 +0100 Subject: [PATCH 4/9] [CEC][SimGen][Clean codes] Removing commented SAT calls operations. --- src/proof/cec/cecSatG2.c | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index fab871f4a..0d265f23d 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -4476,14 +4476,6 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ Vec_WrdDumpHex( pPars->pFileName, p->vSimsPi, nWordsPerCi , 1 ); } - // call SAT solver - /* - Cec4_CallSATsolver(pMapped, pManSim, pPars->pCECPars); - Gia_Man_t * ppNew; Gia_Obj_t * pObj; - Gia_ManForEachCo( pMapped, pObj, i ) - pObj->Value = Gia_ManAppendCo( pManSim->pNew, Gia_ObjFanin0Copy(pObj) ); - ppNew = Gia_ManCleanup( pManSim->pNew ); - */ if (pPars->fVerbose || pPars->fVeryVerbose){ pManSim->pPars->fVerbose = 1; // print the ending stats of sat calls } From 37979dbd94fdd86107c399c6cc842ebfe56ce147 Mon Sep 17 00:00:00 2001 From: Carmine50 Date: Tue, 24 Dec 2024 11:50:47 +0100 Subject: [PATCH 5/9] [CEC][SimGen][Clean codes] Removing commented SAT calls operations. --- src/proof/cec/cecSatG2.c | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 0d265f23d..acbb15cbd 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -4476,9 +4476,6 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ Vec_WrdDumpHex( pPars->pFileName, p->vSimsPi, nWordsPerCi , 1 ); } - if (pPars->fVerbose || pPars->fVeryVerbose){ - pManSim->pPars->fVerbose = 1; // print the ending stats of sat calls - } // free memory Vec_IntFree( pMapped->vTTLut ); Vec_StrFree( pMapped->vTTISOPs ); From 7c6d1ffd2ddc89b402b5e3a484cb47ed289e957b Mon Sep 17 00:00:00 2001 From: Carmine50 Date: Tue, 24 Dec 2024 11:59:23 +0100 Subject: [PATCH 6/9] [CEC][SimGen][Bugs] Fixing bugs and removing unused var. --- src/proof/cec/cecSatG2.c | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index acbb15cbd..3305f9e90 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -2959,7 +2959,7 @@ void saveSimVectors( Gia_Man_t * p, Vec_Ptr_t * pValues, int bitLength, int jth_ int nWords = bitLength / 64; assert(nWords == 0); // Not considering case with large outgold values Gia_ManForEachCiId( p, Id, i ){ - Vec_Wrd_t * pValuesPi = Vec_PtrEntry( pValues, i ); + Vec_Wrd_t * pValuesPi = (Vec_Wrd_t *) Vec_PtrEntry( pValues, i ); word pValuePiJWord = 0; if(kth_bit == 0){ Vec_WrdPush( pValuesPi, 0 ); @@ -3002,7 +3002,7 @@ void executeRandomSim( Gia_Man_t * p, Cec4_Man_t * pMan , int dynSim, int nMaxIt numClass = totalNumClasses(p); iNumber++; Gia_ManForEachCiId( p, Id, j ){ - Vec_Wrd_t * vSimPI = Vec_PtrEntry( vSimSave, j ); + Vec_Wrd_t * vSimPI = (Vec_Wrd_t *) Vec_PtrEntry( vSimSave, j ); word * pSim = Cec4_ObjSim( p, Id ); for( k = 0; k < p->nSimWords; k++ ){ Vec_WrdPush( vSimPI, pSim[k] ); @@ -3020,7 +3020,7 @@ void executeRandomSim( Gia_Man_t * p, Cec4_Man_t * pMan , int dynSim, int nMaxIt if (verbose) printf("Time elapsed: %f (classes size: %d)\n", (float)(clock() - start_time)/CLOCKS_PER_SEC, quality); Gia_ManForEachCiId( p, Id, j ){ - Vec_Wrd_t * vSimPI = Vec_PtrEntry( vSimSave, j ); + Vec_Wrd_t * vSimPI = (Vec_Wrd_t *) Vec_PtrEntry( vSimSave, j ); word * pSim = Cec4_ObjSim( p, Id ); for( k = 0; k < p->nSimWords; k++ ){ Vec_WrdPush( vSimPI, pSim[k] ); @@ -4357,7 +4357,7 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ extern void Gia_ManDupMapping( Gia_Man_t * pNew, Gia_Man_t * p ); Cec4_Man_t * pManSim; - int i, k, iFan, nWordsPerCi; + int i, k, nWordsPerCi; Gia_Man_t * pMapped; Vec_Ptr_t * vSimPisSave; Cec_ParFra_t * pCECPars; From 5961231ed19846599d3c450f215c448b5a2f846e Mon Sep 17 00:00:00 2001 From: Carmine50 Date: Tue, 24 Dec 2024 12:27:09 +0100 Subject: [PATCH 7/9] [CEC][SimGen][Clean codes] Disabling verbose. --- src/proof/cec/cecSatG2.c | 1 + 1 file changed, 1 insertion(+) diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 3305f9e90..45148cebc 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -4377,6 +4377,7 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ printf("Using already mapped network\n"); } pCECPars = (Cec_ParFra_t *) malloc(sizeof( Cec_ParFra_t )); // parameters of CEC + pManSim->pPars->fVerbose = 0; // disabling verbose sat solver pManSim = Cec4_ManCreate( pMapped, pCECPars ); Cec_DeriveSOPs( pMapped ); From 64e8bb02b9a7c28456c1d0a560e614c9086e7374 Mon Sep 17 00:00:00 2001 From: Carmine50 Date: Tue, 24 Dec 2024 14:48:57 +0100 Subject: [PATCH 8/9] [CEC][SimGen][Bits to Words] Changing the units of measure for random simulation from number bits to number words --- src/base/abci/abc.c | 8 +++---- src/proof/cec/cec.h | 4 ++-- src/proof/cec/cecSatG2.c | 49 ++++++++-------------------------------- 3 files changed, 15 insertions(+), 46 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c4cdfa202..d33db9428 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -39230,9 +39230,9 @@ int Abc_CommandAbc9AdvGenSim( 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': @@ -39300,9 +39300,9 @@ usage: 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 for random simulation [default = %d]\n", pPars->bitwidthSim ); + 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 maximum number of iterations [default = %d]\n", pPars->nMaxIter ); + 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 ); diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index fe1a2d518..ca7eed5a7 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -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 diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 45148cebc..20da24865 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -242,9 +242,9 @@ void Cec_SimGenSetParDefault( Cec_ParSimGen_t * pPars ) pPars->fVerbose = 0; // verbose output pPars->fVeryVerbose = 0; // verbose output and outputs files pPars->bitwidthOutgold = 2; // bitwidth of the output golden model - pPars->bitwidthSim = 31; // bitwidth of the simulation vectors + pPars->nSimWords = 4; // number of words in a round of random simulation pPars->expId = 1; // experiment ID - pPars->nMaxIter = -1; // the maximum number of iterations + pPars->nMaxIter = -1; // the maximum number of rounds of random simulation pPars->timeOutSim = 1000.0; // the timeout for simulation in sec pPars->fUseWatchlist = 0; // use watchlist pPars->fImplicationTime = 0.0; // time spent in implication @@ -2860,36 +2860,6 @@ void Cec_RemoveNonLutNodes( Gia_Man_t * p){ Vec_IntFree( vLutIds ); } -/**Function************************************************************* - - Synopsis [Simulate the CIs with random values with specific bitwidth.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - -static inline void Cec_ObjSimCiSimGen( Gia_Man_t * p, int iObj , int bitwidth) -{ - int w; - word * pSim = Cec4_ObjSim( p, iObj ); - word wMask = (1 << bitwidth) -1; - for ( w = 0; w < p->nSimWords; w++ ) - pSim[w] = Abc_RandomW( 0 ) & wMask; - pSim[0] <<= 1; -} - -void Cec_ManSimulateCisSimGen( Gia_Man_t * p, int bitwidth ) -{ - int i, Id; - Gia_ManForEachCiId( p, Id, i ) - Cec_ObjSimCiSimGen( p, Id , bitwidth); - p->iPatsPi = 0; -} - /**Function************************************************************* Synopsis [Evaluate equivalence classes.] @@ -2984,7 +2954,7 @@ void saveSimVectors( Gia_Man_t * p, Vec_Ptr_t * pValues, int bitLength, int jth_ ************************************************************************/ -void executeRandomSim( Gia_Man_t * p, Cec4_Man_t * pMan , int dynSim, int nMaxIter , int bitwidthSim , Vec_Ptr_t * vSimSave, int verbose ){ +void executeRandomSim( Gia_Man_t * p, Cec4_Man_t * pMan , int dynSim, int nMaxIter , Vec_Ptr_t * vSimSave, int verbose ){ clock_t start_time = clock(); int i, j, k, Id; @@ -2994,7 +2964,7 @@ void executeRandomSim( Gia_Man_t * p, Cec4_Man_t * pMan , int dynSim, int nMaxIt while (numClass != oldNumClass && iNumber < iMaxNumber) { oldNumClass = numClass; - Cec_ManSimulateCisSimGen( p, bitwidthSim ); + Cec4_ManSimulateCis( p ); Cec4_ManSimulate( p, pMan ); int quality = evaluate_equiv_classes(p, 0); if (verbose) @@ -3013,7 +2983,7 @@ void executeRandomSim( Gia_Man_t * p, Cec4_Man_t * pMan , int dynSim, int nMaxIt } else { for(i = 0; i < nMaxIter; i++){ - Cec_ManSimulateCisSimGen( p, bitwidthSim ); + Cec4_ManSimulateCis( p ); Cec4_ManSimulate( p, pMan ); int quality = evaluate_equiv_classes(p, 0); Cec_RemoveNonLutNodes( p ); @@ -4377,8 +4347,8 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ printf("Using already mapped network\n"); } pCECPars = (Cec_ParFra_t *) malloc(sizeof( Cec_ParFra_t )); // parameters of CEC - pManSim->pPars->fVerbose = 0; // disabling verbose sat solver pManSim = Cec4_ManCreate( pMapped, pCECPars ); + pManSim->pPars->fVerbose = 0; // disabling verbose sat solver Cec_DeriveSOPs( pMapped ); @@ -4407,8 +4377,7 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ // generate vectors of fanouts Gia_generateFanoutMapping( pMapped ); - assert( pPars->bitwidthSim > 0); - pMapped->nSimWords = (int) pPars->bitwidthSim / 64 + ((pPars->bitwidthSim % 64) > 0); + pMapped->nSimWords = (int) pPars->nSimWords ; vSimPisSave = Vec_PtrAlloc( Gia_ManCiNum(pMapped) ); for ( i = 0; i < Gia_ManCiNum(pMapped); i++ ){ Vec_Wrd_t * vSim = Vec_WrdAlloc( pMapped->nSimWords ); @@ -4417,9 +4386,9 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ // simulate n rounds of random simulation and create classes Cec4_ManSimAlloc( pMapped, pMapped->nSimWords ); if(pPars->nMaxIter >= 0){ - executeRandomSim( pMapped, pManSim, 0, pPars->nMaxIter, pPars->bitwidthSim , vSimPisSave, pPars->fVeryVerbose); + executeRandomSim( pMapped, pManSim, 0, pPars->nMaxIter, vSimPisSave, pPars->fVeryVerbose); } else if (pPars->nMaxIter == -1){ - executeRandomSim( pMapped, pManSim, 1, pPars->nMaxIter, pPars->bitwidthSim , vSimPisSave, pPars->fVeryVerbose); + executeRandomSim( pMapped, pManSim, 1, pPars->nMaxIter, vSimPisSave, pPars->fVeryVerbose); } else { printf("Invalid number of iterations %d\n", pPars->nMaxIter); return NULL; From a74da1c50bab5835b8b350305842861d308c7480 Mon Sep 17 00:00:00 2001 From: Carmine50 Date: Tue, 24 Dec 2024 14:54:59 +0100 Subject: [PATCH 9/9] [CEC][SAT Sweeping] Added new functionality in SAT sweeping function to use for simulation the PI vector present in vSimsPi data structure. --- src/proof/cec/cecSatG2.c | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 20da24865..1b0948de1 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -1863,7 +1863,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars ); Gia_Obj_t * pObj, * pRepr; - int i, fSimulate = 1; + int i, fSimulate = 1, Id; if ( pPars->fVerbose ) printf( "Solver type = %d. Simulate %d words in %d rounds. SAT with %d confs. Recycle after %d SAT calls.\n", pPars->jType, pPars->nWords, pPars->nRounds, pPars->nBTLimit, pPars->nCallsRecycle ); @@ -1888,6 +1888,22 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p } } + if( p->vSimsPi && p->nSimWords > 0){ // if the simulation pis are already set, do not generate new ones + pPars->nWords = p->nSimWords; + Vec_WrdFreeP( &p->vSims ); + p->vSims = Vec_WrdStart( Gia_ManObjNum(p) * pPars->nWords); + assert( Vec_WrdSize(p->vSimsPi) == Gia_ManCiNum(p) * p->nSimWords ); + Gia_ManForEachCiId(p, Id, i){ + memmove( Vec_WrdEntryP(p->vSims, Id*p->nSimWords), Vec_WrdEntryP(p->vSimsPi, i*p->nSimWords), sizeof(word)*p->nSimWords ); + } + Cec4_ManSimulate( p, pMan ); + if ( pPars->fCheckMiter && !Cec4_ManSimulateCos(p) ) // cex detected + goto finalize; + if ( fSimOnly ) + goto finalize; + goto execute_sat; + } + // simulate one round and create classes Cec4_ManSimAlloc( p, pPars->nWords ); Cec4_ManSimulateCis( p ); @@ -1922,6 +1938,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( i && i % 5 == 0 && pPars->fVerbose ) Cec4_ManPrintStats( p, pPars, pMan, 1 ); } + execute_sat: if ( i && i % 5 && pPars->fVerbose ) Cec4_ManPrintStats( p, pPars, pMan, 1 );