diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 077c88d9b..5cb503463 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -51320,10 +51320,15 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fVerbose, int fVeryVerbose, int fSilent ); - int c, nProcs = 5, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; + typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; + typedef struct Wlc_BstPar_t_ Wlc_BstPar_t; + extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars ); + extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent ); + Gia_Man_t * pGiaUse = pAbc->pGia, * pGiaTemp = NULL; + Wlc_Ntk_t * pWlc = (Wlc_Ntk_t *)pAbc->pAbcWlc; + int c, nProcs = 5, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWsvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWusvwh" ) ) != EOF ) { switch ( c ) { @@ -51371,6 +51376,9 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nTimeOut3 <= 0 ) goto usage; break; + case 'u': + fUseUif ^= 1; + break; case 's': fSilent ^= 1; break; @@ -51386,27 +51394,56 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( pAbc->pGia == NULL ) + if ( fUseUif ) + { + pGiaUse = NULL; + if ( pWlc == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no word-level design for option \"-u\".\n" ); + return 1; + } + pGiaTemp = Wlc_NtkBitBlast( pWlc, NULL ); + if ( pGiaTemp == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve(): Word-level bit-blasting has failed.\n" ); + return 1; + } + if ( (Gia_ManPoNum(pGiaTemp) & 1) == 1 ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve(): Internal \"&miter -x\" requires even number of bit-level outputs.\n" ); + Gia_ManStop( pGiaTemp ); + return 1; + } + pGiaUse = Gia_ManTransformMiter2( pGiaTemp ); + Gia_ManStop( pGiaTemp ); + pGiaTemp = NULL; + } + if ( pGiaUse == NULL ) { Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no AIG.\n" ); return 1; } - if ( Gia_ManRegNum(pAbc->pGia) == 0 ) + if ( Gia_ManRegNum(pGiaUse) == 0 ) { Abc_Print( -1, "Abc_CommandAbc9SProve(): The problem is combinational.\n" ); + if ( fUseUif ) + Gia_ManStop( pGiaUse ); return 1; } - pAbc->Status = Cec_GiaProveTest( pAbc->pGia, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fVerbose, fVeryVerbose, fSilent ); - Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); + pAbc->Status = Cec_GiaProveTest( pGiaUse, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif, pWlc, fVerbose, fVeryVerbose, fSilent ); + Abc_FrameReplaceCex( pAbc, &pGiaUse->pCexSeq ); + if ( fUseUif ) + Gia_ManStop( pGiaUse ); return 0; usage: - Abc_Print( -2, "usage: &sprove [-PTUW num] [-svwh]\n" ); + Abc_Print( -2, "usage: &sprove [-PTUW num] [-usvwh]\n" ); Abc_Print( -2, "\t proves CEC problem by case-splitting\n" ); Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", nProcs ); Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut ); Abc_Print( -2, "\t-U num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut2 ); - Abc_Print( -2, "\t-W num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut3 ); + Abc_Print( -2, "\t-W num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut3 ); + Abc_Print( -2, "\t-u : enable concurrent UFAR on word-level design (uses internal %%blast + &miter -x)\n" ); Abc_Print( -2, "\t-s : enable silent computation (no reporting) [default = %s]\n", fSilent? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); diff --git a/src/opt/ufar/UfarCmd.cpp b/src/opt/ufar/UfarCmd.cpp index 5bedeeca6..37728b04d 100755 --- a/src/opt/ufar/UfarCmd.cpp +++ b/src/opt/ufar/UfarCmd.cpp @@ -48,6 +48,44 @@ void Ufar_Init(Abc_Frame_t *pAbc) //Cmd_CommandAdd( pAbc, "Word level Prove", "%%miter", Abc_CommandCreateMiter, 0 ); } +int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId ) +{ + UFAR::UfarManager manager; + timeval t1; + set set_op_types; + Wlc_Ntk_t * pUse = pNtk; + int RetValue = -1; + if ( pNtk == NULL ) + return -1; + if ( Wlc_NtkPoNum(pUse) == 2 ) + { + pUse = UFAR::CreateMiter( pUse, 0 ); + if ( pUse == NULL ) + return -1; + } + else if ( Wlc_NtkPoNum(pUse) != 1 ) + return -1; + set_op_types.insert( WLC_OBJ_ARI_MULTI ); + if ( !UFAR::HasOperator( pUse, set_op_types ) ) + { + if ( pUse != pNtk ) + Wlc_NtkFree( pUse ); + return -1; + } + manager.params = UFAR::UfarManager::Params(); + manager.params.RunId = RunId; + manager.params.pFuncStop = pFuncStop; + if ( nTimeOut > 0 ) + manager.params.nTimeout = nTimeOut; + manager.params.iVerbosity = fVerbose ? 1 : 0; + gettimeofday( &t1, NULL ); + manager.Initialize( pUse, set_op_types ); + RetValue = manager.PerformUIFProve( t1 ); + if ( pUse != pNtk ) + Wlc_NtkFree( pUse ); + return RetValue; +} + static int Abc_CommandCreateMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) { Wlc_Ntk_t * pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0); diff --git a/src/opt/ufar/UfarCmd.h b/src/opt/ufar/UfarCmd.h index d2b775269..52dfc8bb8 100755 --- a/src/opt/ufar/UfarCmd.h +++ b/src/opt/ufar/UfarCmd.h @@ -14,6 +14,9 @@ ABC_NAMESPACE_HEADER_START void Ufar_Init(Abc_Frame_t *pAbc); +typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; +extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId ); + ABC_NAMESPACE_HEADER_END #endif /* SRC_EXT2_UIF_UIFCMD_H_ */ diff --git a/src/opt/ufar/UfarMgr.cpp b/src/opt/ufar/UfarMgr.cpp index 67b5aed85..6973f69fb 100755 --- a/src/opt/ufar/UfarMgr.cpp +++ b/src/opt/ufar/UfarMgr.cpp @@ -819,8 +819,8 @@ void CexUifPairFinder::ComputeCoreUifPairs(const set& set_candidates, } void CexUifPairFinder::FindUifPairsBasic(const VecVecChar& cex_po_values, unsigned nLookBack, set& set_new_pairs) { - assert(Wlc_NtkPoNum(_pOrigNtk) == 1); - assert(Wlc_ObjRange(Wlc_NtkPo(_pOrigNtk, 0)) == 1); + if ( Wlc_NtkPoNum(_pOrigNtk) != 1 || Wlc_ObjRange(Wlc_NtkPo(_pOrigNtk, 0)) != 1 ) + return; _inputs.clear(); _outputs.clear(); @@ -879,8 +879,8 @@ void CexUifPairFinder::FindUifPairsBasic(const VecVecChar& cex_po_values, unsign } void CexUifPairFinder::FindUifPairs(const VecVecChar& cex_po_values, unsigned nLookBack, set& set_new_pairs) { - assert(Wlc_NtkPoNum(_pOrigNtk) == 1); - assert(Wlc_ObjRange(Wlc_NtkPo(_pOrigNtk, 0)) == 1); + if ( Wlc_NtkPoNum(_pOrigNtk) != 1 || Wlc_ObjRange(Wlc_NtkPo(_pOrigNtk, 0)) != 1 ) + return; _compute_max_bw(); @@ -931,7 +931,14 @@ void CexUifPairFinder::FindUifPairs(const VecVecChar& cex_po_values, unsigned nL } +static inline int Ufar_ShouldStop( const UfarManager::Params & p ) +{ + return p.pFuncStop && p.pFuncStop( p.RunId ); +} + UfarManager::Params::Params() : + RunId(-1), + pFuncStop(NULL), fCexMin(true), fPbaUif(false), fLazySim(true), @@ -1359,8 +1366,14 @@ void UfarManager::DetermineWhiteBoxes(Abc_Cex_t * pCex) { int UfarManager::VerifyCurrentAbstraction(Abc_Cex_t ** ppCex) { timeval t1, t2; gettimeofday(&t1, NULL); + if ( Ufar_ShouldStop(params) ) + return -1; Wlc_Ntk_t * pCurrent = BuildCurrentAbstraction(); + if ( Ufar_ShouldStop(params) ) { + Wlc_NtkFree(pCurrent); + return -1; + } if(!params.fileAbs.empty()) Wlc_WriteVer(pCurrent, &((params.fileAbs + "_abs.v")[0u]), 0, 0); @@ -1376,7 +1389,7 @@ int UfarManager::VerifyCurrentAbstraction(Abc_Cex_t ** ppCex) { } } */ - ret = verify_model(pCurrent, ppCex, ¶ms.fileName, ¶ms.parSetting, params.fSyn, &_timeout); + ret = verify_model(pCurrent, ppCex, ¶ms.fileName, ¶ms.parSetting, params.fSyn, &_timeout, params.pFuncStop, params.RunId); Wlc_NtkFree(pCurrent); gettimeofday(&t2, NULL); @@ -1428,6 +1441,8 @@ int UfarManager::PerformUIFProve(const timeval& timer) { if(!params.fileStatesOut.empty()) _dump_states(params.fileStatesOut); }; + if ( Ufar_ShouldStop(params) ) + return -1; if (!params.fileStatesIn.empty()) { _read_states(params.fileStatesIn); if (params.iExp != -1) _massage_state_b(); @@ -1435,6 +1450,8 @@ int UfarManager::PerformUIFProve(const timeval& timer) { } if (!params.fLazySim && !params.simSetting.empty()) { + if ( Ufar_ShouldStop(params) ) + return -1; unsigned origSize = _set_uif_pairs.size(); LOG(1) << "Try using simulation to find UIF pairs"; _simulate(); @@ -1450,6 +1467,8 @@ int UfarManager::PerformUIFProve(const timeval& timer) { while(true) { while(true) { + if ( Ufar_ShouldStop(params) ) + return -1; if (params.fPbaCex && mem.pCex2) { if(mem.pCex) Abc_CexFree(mem.pCex); mem.pCex = mem.pCex2; @@ -1462,6 +1481,8 @@ int UfarManager::PerformUIFProve(const timeval& timer) { } if (ret == 0) { // SAT + if ( Ufar_ShouldStop(params) ) + return -1; // GetOperatorsInCex(mem.pCex); if (verify_cex_on_original(_pOrigNtk, mem.pCex)) { PrintWordCEX(_pOrigNtk, mem.pCex, &_vec_orig_names); @@ -1470,11 +1491,15 @@ int UfarManager::PerformUIFProve(const timeval& timer) { unsigned n_before = _set_uif_pairs.size(); FindUifPairsUsingCex(mem.pCex, &mem.pCex2); + if ( Ufar_ShouldStop(params) ) + return -1; if (n_before == _set_uif_pairs.size()) { LOG(1) << "No new UIF pair is found in CEX"; if(!params.simSetting.empty()) { + if ( Ufar_ShouldStop(params) ) + return -1; LOG(1) << "Try using simulation to find UIF pairs"; _simulate(); FindUifPairsUsingSim(); @@ -1485,6 +1510,8 @@ int UfarManager::PerformUIFProve(const timeval& timer) { } if (params.nGrey) { + if ( Ufar_ShouldStop(params) ) + return -1; DetermineGreyness(mem.pCex); } @@ -1509,6 +1536,8 @@ int UfarManager::PerformUIFProve(const timeval& timer) { } } + if ( Ufar_ShouldStop(params) ) + return -1; DetermineWhiteBoxes(mem.pCex); ++n_iter_wb; diff --git a/src/opt/ufar/UfarMgr.h b/src/opt/ufar/UfarMgr.h index ad2f9c477..31b91ef40 100755 --- a/src/opt/ufar/UfarMgr.h +++ b/src/opt/ufar/UfarMgr.h @@ -60,6 +60,8 @@ class UfarManager { public: struct Params { Params(); + int RunId; + int (*pFuncStop)(int); bool fCexMin; bool fPbaUif; bool fLazySim; diff --git a/src/opt/untk/NtkNtk.cpp b/src/opt/untk/NtkNtk.cpp index 0c74a4761..97625f8bb 100755 --- a/src/opt/untk/NtkNtk.cpp +++ b/src/opt/untk/NtkNtk.cpp @@ -1119,7 +1119,8 @@ Wlc_Ntk_t * CreateMiter(Wlc_Ntk_t *pNtk, bool fXor) assert(Wlc_NtkPoNum(pNtk) == 2); Wlc_Ntk_t *pNew = Wlc_NtkDupDfsSimple(pNtk); - Wlc_NtkTransferNames( pNew, pNtk ); + if ( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(pNtk) ) + Wlc_NtkTransferNames( pNew, pNtk ); Wlc_Obj_t *pOldPo0 = Wlc_NtkPo(pNew, 0); Wlc_Obj_t *pOldPo1 = Wlc_NtkPo(pNew, 1); @@ -1145,7 +1146,8 @@ Wlc_Ntk_t * CreateMiter(Wlc_Ntk_t *pNtk, bool fXor) Wlc_NtkObj(pNew, iOldPo1)->fIsPo = 0; Wlc_Ntk_t *pNewNew = Wlc_NtkDupDfsSimple(pNew); - Wlc_NtkTransferNames( pNewNew, pNew ); + if ( !Wlc_NtkHasNameId(pNewNew) && Wlc_NtkHasNameId(pNew) ) + Wlc_NtkTransferNames( pNewNew, pNew ); Wlc_NtkFree(pNew); return pNewNew; } @@ -1245,9 +1247,11 @@ static void readCexFromFile(int& ret, FILE * file, Abc_Cex_t ** ppCex, int nOrig } } -int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, struct timespec * timeout) { +int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, struct timespec * timeout, int (*pFuncStop)(int), int RunId) { + if ( pFuncStop && pFuncStop(RunId) ) + return -1; if ( !pParSetting || pParSetting->empty() || Wlc_NtkFfNum(pNtk) == 0 ) - return bit_level_solve( pNtk, ppCex, pFileName, pParSetting, fSyn ); + return bit_level_solve( pNtk, ppCex, pFileName, pParSetting, fSyn, pFuncStop, RunId ); if(*ppCex) { Abc_CexFree(*ppCex); @@ -1262,11 +1266,15 @@ int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, ret = RunConcurrentSolver( pNtk, parSolvers, ppCex, timeout ); + if ( pFuncStop && pFuncStop(RunId) ) + return -1; return ret; } -int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn) { +int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, int (*pFuncStop)(int), int RunId) { + if ( pFuncStop && pFuncStop(RunId) ) + return -1; if(*ppCex) { Abc_CexFree(*ppCex); *ppCex = NULL; @@ -1303,6 +1311,8 @@ int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileNam Pdr_Par_t PdrPars, *pPdrPars = &PdrPars; Pdr_ManSetDefaultParams(pPdrPars); pPdrPars->nConfLimit = 0; + pPdrPars->RunId = RunId; + pPdrPars->pFuncStop = pFuncStop; //pPdrPars->fDumpInv = 1; Abc_FrameReadGlobalFrame()->pNtkCur = pAbcNtk; int res = Abc_NtkDarPdr(pAbcNtk, pPdrPars); diff --git a/src/opt/untk/NtkNtk.h b/src/opt/untk/NtkNtk.h index e3323f123..85d9ac935 100755 --- a/src/opt/untk/NtkNtk.h +++ b/src/opt/untk/NtkNtk.h @@ -136,8 +136,8 @@ void PrintWordCEX(Wlc_Ntk_t * pNtk, Abc_Cex_t * pCex, const std::vectorfSolved != 0; +} static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result ) { Par_ThData_t * pThData = (Par_ThData_t *)pUser; @@ -114,6 +126,12 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par { abctime clk = Abc_Clock(); int RetValue = -1; + if ( iEngine != PAR_ENGINE_UFAR && Gia_ManRegNum(p) == 0 ) + { + if ( fVerbose ) + printf( "Engine %d skipped because the current miter is combinational.\n", iEngine ); + return -1; + } //abctime clkStop = nTimeOut * CLOCKS_PER_SEC + Abc_Clock(); if ( fVerbose ) printf( "Calling engine %d with timeout %d sec.\n", iEngine, nTimeOut ); @@ -212,6 +230,15 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par } RetValue = Bmcg_ManPerform( p, pPars ); } + else if ( iEngine == PAR_ENGINE_UFAR ) + { + if ( pThData && pThData->pWlc ) + { + g_pUfarShare = pThData->pShare; + RetValue = Ufar_ProveWithTimeout( pThData->pWlc, pThData->nTimeOutU, fVerbose, Cec_SProveStopUfar, 0 ); + g_pUfarShare = NULL; + } + } else assert( 0 ); //while ( Abc_Clock() < clkStop ); if ( pThData && pThData->pShare && RetValue != -1 ) @@ -224,6 +251,8 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par } Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p ) { + if ( Gia_ManRegNum(p) == 0 ) + return Gia_ManDup( p ); Ssw_Pars_t Pars, * pPars = &Pars; Ssw_ManSetDefaultParams( pPars ); Aig_Man_t * pAig = Gia_ManToAigSimple( p ); @@ -235,6 +264,8 @@ Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p ) } Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p ) { + if ( Gia_ManRegNum(p) == 0 ) + return Gia_ManDup( p ); Cec_ParCor_t Pars, * pPars = &Pars; Cec_ManCorSetDefaultParams( pPars ); pPars->nBTLimit = 100; @@ -275,34 +306,36 @@ void * Cec_GiaProveWorkerThread( void * pArg ) assert( 0 ); return NULL; } -void Cec_GiaInitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int nTimeOut, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare ) +void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, int fUseUif, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare ) { int i, status; - assert( nProcs <= PAR_THR_MAX ); - for ( i = 0; i < nProcs; i++ ) + assert( nWorkers <= PAR_THR_MAX ); + for ( i = 0; i < nWorkers; i++ ) { ThData[i].p = Gia_ManDup(p); - ThData[i].iEngine = i; + ThData[i].iEngine = (fUseUif && i == nWorkers - 1) ? PAR_ENGINE_UFAR : i; ThData[i].nTimeOut = nTimeOut; ThData[i].fWorking = 0; ThData[i].Result = -1; ThData[i].fVerbose = fVerbose; + ThData[i].nTimeOutU= nTimeOutU; + ThData[i].pWlc = pWlc; ThData[i].pShare = pShare; if ( !WorkerThread ) continue; status = pthread_create( WorkerThread + i, NULL,Cec_GiaProveWorkerThread, (void *)(ThData + i) ); assert( status == 0 ); } - for ( i = 0; i < nProcs; i++ ) + for ( i = 0; i < nWorkers; i++ ) ThData[i].fWorking = 1; } -int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int RetValue, int * pRetEngine ) +int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine ) { int i; - for ( i = 0; i < nProcs; i++ ) + for ( i = 0; i < nWorkers; i++ ) { if ( RetValue == -1 && !ThData[i].fWorking && ThData[i].Result != -1 ) { RetValue = ThData[i].Result; - *pRetEngine = i; + *pRetEngine = ThData[i].iEngine; if ( !p->pCexSeq && ThData[i].p->pCexSeq ) p->pCexSeq = Abc_CexDup( ThData[i].p->pCexSeq, -1 ); } @@ -312,13 +345,13 @@ int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int Re return RetValue; } -int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fVerbose, int fVeryVerbose, int fSilent ) +int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent ) { abctime clkScorr = 0, clkTotal = Abc_Clock(); Par_ThData_t ThData[PAR_THR_MAX]; pthread_t WorkerThread[PAR_THR_MAX]; Par_Share_t Share; - int i, RetValue = -1, RetEngine = -2; + int i, nWorkers = nProcs + (fUseUif ? 1 : 0), RetValue = -1, RetEngine = -2; memset( &Share, 0, sizeof(Par_Share_t) ); Abc_CexFreeP( &p->pCexComb ); Abc_CexFreeP( &p->pCexSeq ); @@ -329,7 +362,8 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in fflush( stdout ); assert( nProcs == 3 || nProcs == 5 ); - Cec_GiaInitThreads( ThData, nProcs, p, nTimeOut, fVerbose, WorkerThread, &Share ); + assert( nWorkers <= PAR_THR_MAX ); + Cec_GiaInitThreads( ThData, nWorkers, p, nTimeOut, nTimeOut3, pWlc, fUseUif, fVerbose, WorkerThread, &Share ); // meanwhile, perform scorr Gia_Man_t * pScorr = Cec_GiaScorrNew( p ); @@ -337,7 +371,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in if ( Gia_ManAndNum(pScorr) == 0 ) RetValue = 1, RetEngine = -1; - RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine ); + RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); if ( RetValue == -1 ) { abctime clkScorr2, clkStart = Abc_Clock(); @@ -345,7 +379,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in printf( "Reduced the miter from %d to %d nodes. ", Gia_ManAndNum(p), Gia_ManAndNum(pScorr) ); Abc_PrintTime( 1, "Time", clkScorr ); } - Cec_GiaInitThreads( ThData, nProcs, pScorr, nTimeOut2, fVerbose, NULL, &Share ); + Cec_GiaInitThreads( ThData, nWorkers, pScorr, nTimeOut2, nTimeOut3, pWlc, fUseUif, fVerbose, NULL, &Share ); // meanwhile, perform scorr if ( Gia_ManAndNum(pScorr) < 100000 ) @@ -355,16 +389,16 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in if ( Gia_ManAndNum(pScorr2) == 0 ) RetValue = 1; - RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine ); + RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); if ( RetValue == -1 ) { if ( !fSilent && fVerbose ) { printf( "Reduced the miter from %d to %d nodes. ", Gia_ManAndNum(pScorr), Gia_ManAndNum(pScorr2) ); Abc_PrintTime( 1, "Time", clkScorr2 ); } - Cec_GiaInitThreads( ThData, nProcs, pScorr2, nTimeOut3, fVerbose, NULL, &Share ); + Cec_GiaInitThreads( ThData, nWorkers, pScorr2, nTimeOut3, nTimeOut3, pWlc, fUseUif, fVerbose, NULL, &Share ); - RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine ); + RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); // do something else } Gia_ManStop( pScorr2 ); @@ -373,7 +407,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in Gia_ManStop( pScorr ); // stop threads - for ( i = 0; i < nProcs; i++ ) + for ( i = 0; i < nWorkers; i++ ) { ThData[i].p = NULL; ThData[i].fWorking = 1;