diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1c9d9f6d5..824c09003 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -478,7 +478,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 ); @@ -1279,7 +1279,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 ); @@ -39331,7 +39331,7 @@ usage: /**Function************************************************************* - Synopsis [Abc_CommandAbc9SimGen] + Synopsis [Abc_CommandAbc9AdvGenSim] Description [This function calls SimGen tool] @@ -39341,7 +39341,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 ); @@ -39350,7 +39350,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 ) { @@ -39382,9 +39382,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': @@ -39409,6 +39409,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; @@ -39439,13 +39448,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-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 ); diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index 4db2df726..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 @@ -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 }; //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 33259bfe4..1b0948de1 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 @@ -252,8 +252,7 @@ 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 } /**Function************************************************************* @@ -1864,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 ); @@ -1889,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 ); @@ -1923,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 ); @@ -2861,36 +2877,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.] @@ -2942,6 +2928,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_Wrd_t *) 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,34 +2971,48 @@ 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 , 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){ 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) 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_Wrd_t *) Vec_PtrEntry( vSimSave, j ); + word * pSim = Cec4_ObjSim( p, Id ); + for( k = 0; k < p->nSimWords; k++ ){ + Vec_WrdPush( vSimPI, pSim[k] ); + } + } } } 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 ); 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_Wrd_t *) Vec_PtrEntry( vSimSave, j ); + word * pSim = Cec4_ObjSim( p, Id ); + for( k = 0; k < p->nSimWords; k++ ){ + Vec_WrdPush( vSimPI, pSim[k] ); + } + } } } } @@ -3893,7 +3924,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 +4041,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 +4083,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 +4110,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 +4344,10 @@ 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, nWordsPerCi; Gia_Man_t * pMapped; + Vec_Ptr_t * vSimPisSave; + Cec_ParFra_t * pCECPars; if (!Gia_ManHasMapping(p)){ // apply technology mapping if not already done @@ -4320,10 +4363,13 @@ 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 ); + pManSim->pPars->fVerbose = 0; // disabling verbose sat solver Cec_DeriveSOPs( pMapped ); + /* if (pPars->fVeryVerbose) { printf("**Printing LUTs information**\n"); @@ -4335,6 +4381,7 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){ printISOPLUT( pMapped, i ); } } + */ // compute MFFCs Gia_ManLevelNum( pMapped); // compute levels @@ -4347,17 +4394,28 @@ 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 ); + 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 ); + 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, vSimPisSave, pPars->fVeryVerbose); } else if (pPars->nMaxIter == -1){ - executeRandomSim( pMapped, pManSim, 1, pPars->nMaxIter, pPars->bitwidthSim , pPars->fVeryVerbose); + executeRandomSim( pMapped, pManSim, 1, pPars->nMaxIter, 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 +4427,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,14 +4440,29 @@ 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 ); - - // call SAT solver - Cec4_CallSATsolver(pMapped, pManSim, pPars->pCECPars); - - if (pPars->fVerbose || pPars->fVeryVerbose){ - pManSim->pPars->fVerbose = 1; // print the ending stats of sat calls + // 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; + + if (pPars->pFileName != NULL){ + Vec_WrdDumpHex( pPars->pFileName, p->vSimsPi, nWordsPerCi , 1 ); + } + // free memory Vec_IntFree( pMapped->vTTLut ); Vec_StrFree( pMapped->vTTISOPs );