diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-03-20 05:01:40 +0000 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-03-20 05:01:40 +0000 |
commit | 245532cad1d93f1347dec39035d6db7f8eebc2c6 (patch) | |
tree | bc6c52755f0962b9ac3360ed50520ee5ec3279e6 /src/base/wlc/wlcPth.c | |
parent | 027bb83e814d5aec18c080004854b9cc6b679ad9 (diff) | |
parent | 9a1ef0e5d0d4dbe26f9d0657ef53f9a482aed35d (diff) | |
download | abc-245532cad1d93f1347dec39035d6db7f8eebc2c6.tar.gz abc-245532cad1d93f1347dec39035d6db7f8eebc2c6.tar.bz2 abc-245532cad1d93f1347dec39035d6db7f8eebc2c6.zip |
Merged in ysho/abc (pull request #69)
Improvements to %pdra
Diffstat (limited to 'src/base/wlc/wlcPth.c')
-rw-r--r-- | src/base/wlc/wlcPth.c | 152 |
1 files changed, 152 insertions, 0 deletions
diff --git a/src/base/wlc/wlcPth.c b/src/base/wlc/wlcPth.c new file mode 100644 index 00000000..783dbe6f --- /dev/null +++ b/src/base/wlc/wlcPth.c @@ -0,0 +1,152 @@ +/**CFile**************************************************************** + + FileName [wlcPth.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Verilog parser.] + + Synopsis [Abstraction for word-level networks.] + + Author [Yen-Sheng Ho, Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: wlcPth.c $] + +***********************************************************************/ + +#include "wlc.h" +#include "sat/bmc/bmc.h" + +#ifdef ABC_USE_PTHREADS + +#ifdef _WIN32 +#include "../lib/pthread.h" +#else +#include <pthread.h> +#include <unistd.h> +#endif + +#endif + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pAig ); +extern int Abc_NtkDarBmc3( Abc_Ntk_t * pAbcNtk, Saig_ParBmc_t * pBmcPars, int fOrDecomp ); + +static volatile int g_nRunIds = 0; // the number of the last prover instance +int Wla_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; } +int Wla_GetGlobalRunId() { return g_nRunIds; } + +#ifndef ABC_USE_PTHREADS + +void Wla_ManJoinThread( Wla_Man_t * pWla, int RunId ) {} +void Wla_ManConcurrentBmc3( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppCex ) {} + +#else // pthreads are used + +// information given to the thread +typedef struct Bmc3_ThData_t_ +{ + Aig_Man_t * pAig; + Abc_Cex_t ** ppCex; + int RunId; + int fVerbose; +} Bmc3_ThData_t; + +// mutext to control access to shared variables +extern pthread_mutex_t g_mutex; + +void Wla_ManJoinThread( Wla_Man_t * pWla, int RunId ) +{ + int status; + if ( RunId == g_nRunIds ) + { + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); + ++g_nRunIds; + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + } + + status = pthread_join( *(pthread_t *)(pWla->pThread), NULL ); + assert( status == 0 ); + ABC_FREE( pWla->pThread ); + pWla->pThread = NULL; +} + +void * Wla_Bmc3Thread ( void * pArg ) +{ + int status; + int RetValue = -1; + Bmc3_ThData_t * pData = (Bmc3_ThData_t *)pArg; + Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase( pData->pAig ); + Saig_ParBmc_t BmcPars, *pBmcPars = &BmcPars; + Saig_ParBmcSetDefaultParams( pBmcPars ); + pBmcPars->pFuncStop = Wla_CallBackToStop; + pBmcPars->RunId = pData->RunId; + + RetValue = Abc_NtkDarBmc3( pAbcNtk, pBmcPars, 0 ); + + if ( RetValue == 0 ) + { + assert( pAbcNtk->pSeqModel ); + *(pData->ppCex) = pAbcNtk->pSeqModel; + pAbcNtk->pSeqModel = NULL; + + if ( pData->fVerbose ) + Abc_Print( 1, "Bmc3 found CEX. RunId=%d.\n", pData->RunId ); + + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); + ++g_nRunIds; + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + } + else + { + if ( pData->fVerbose ) + Abc_Print( 1, "Bmc3 was cancelled. RunId=%d.\n", pData->RunId ); + } + + // free memory + Abc_NtkDelete( pAbcNtk ); + Aig_ManStop( pData->pAig ); + ABC_FREE( pData ); + + // quit this thread + pthread_exit( NULL ); + assert(0); + return NULL; +} + +void Wla_ManConcurrentBmc3( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppCex ) +{ + int status; + Bmc3_ThData_t * pData; + + assert( pWla->pThread == NULL ); + pWla->pThread = (void *)ABC_CALLOC( pthread_t, 1 ); + + pData = ABC_CALLOC( Bmc3_ThData_t, 1 ); + pData->pAig = pAig; + pData->ppCex = ppCex; + pData->RunId = g_nRunIds; + pData->fVerbose = pWla->pPars->fVerbose; + + status = pthread_create( (pthread_t *)pWla->pThread, NULL, Wla_Bmc3Thread, pData ); + assert( status == 0 ); +} + +#endif // pthreads are used + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |