From 7713e94a1aee256db65a1939f1daafdec61d6675 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 18 Mar 2017 14:23:09 -0700 Subject: %pdra: isolated the procedure for checking comb. unsat --- src/base/wlc/wlcAbs.c | 86 +++++++++++++++++++++++++++++---------------------- 1 file changed, 49 insertions(+), 37 deletions(-) (limited to 'src') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index c89ed187..3373cdd9 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -1251,6 +1251,54 @@ Aig_Man_t * Wla_ManBitBlast( Wla_Man_t * pWla, Wlc_Ntk_t * pAbs ) return pAig; } +int Wla_ManCheckCombUnsat( Wla_Man_t * pWla, Aig_Man_t * pAig ) +{ + Pdr_Man_t * pPdr; + abctime clk; + int RetValue = -1; + + if ( Aig_ManAndNum( pAig ) <= 20000 ) + { + Aig_Man_t * pAigScorr; + Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars; + int nAnds; + + clk = Abc_Clock(); + + Ssw_ManSetDefaultParams( pScorrPars ); + pScorrPars->fStopWhenGone = 1; + pScorrPars->nFramesK = 1; + pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars ); + assert ( pAigScorr ); + nAnds = Aig_ManAndNum( pAigScorr); + Aig_ManStop( pAigScorr ); + + if ( nAnds == 0 ) + { + if ( pWla->pPars->fVerbose ) + Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk ); + return 1; + } + else if ( pWla->pPars->fVerbose ) + { + Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + } + + clk = Abc_Clock(); + + pWla->pPdrPars->fVerbose = 0; + pPdr = Pdr_ManStart( pAig, pWla->pPdrPars, NULL ); + RetValue = IPdr_ManCheckCombUnsat( pPdr ); + Pdr_ManStop( pPdr ); + pWla->pPdrPars->fVerbose = pWla->pPars->fPdrVerbose; + + pWla->tPdr += Abc_Clock() - clk; + + return RetValue; +} + int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) { abctime clk; @@ -1259,45 +1307,9 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) if ( pWla->vClauses && pWla->pPars->fCheckCombUnsat ) { - if ( Aig_ManAndNum( pAig ) <= 20000 ) - { - Aig_Man_t * pAigScorr; - Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars; - int nAnds; - - clk = Abc_Clock(); - - Ssw_ManSetDefaultParams( pScorrPars ); - pScorrPars->fStopWhenGone = 1; - pScorrPars->nFramesK = 1; - pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars ); - assert ( pAigScorr ); - nAnds = Aig_ManAndNum( pAigScorr); - Aig_ManStop( pAigScorr ); - - if ( nAnds == 0 ) - { - if ( pWla->pPars->fVerbose ) - Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk ); - return 1; - } - else if ( pWla->pPars->fVerbose ) - { - Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - } - } - clk = Abc_Clock(); - pWla->pPdrPars->fVerbose = 0; - pPdr = Pdr_ManStart( pAig, pWla->pPdrPars, NULL ); - RetValue = IPdr_ManCheckCombUnsat( pPdr ); - Pdr_ManStop( pPdr ); - pWla->pPdrPars->fVerbose = pWla->pPars->fPdrVerbose; - - pWla->tPdr += Abc_Clock() - clk; - + RetValue = Wla_ManCheckCombUnsat( pWla, pAig ); if ( RetValue == 1 ) { if ( pWla->pPars->fVerbose ) -- cgit v1.2.3 From 0d054904e0416179c8c2bf12dc47b520a2922a32 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 18 Mar 2017 15:23:50 -0700 Subject: %pdra: working on bmc3 --- src/base/wlc/wlc.h | 1 + src/base/wlc/wlcAbs.c | 84 +++++++++++++++++++++++++++++++++++++++++++++++++++ src/base/wlc/wlcCom.c | 8 +++-- src/base/wlc/wlcNtk.c | 1 + 4 files changed, 92 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 53936cc9..0e28f98d 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -180,6 +180,7 @@ struct Wlc_Par_t_ int fCheckCombUnsat; // Check if ABS becomes comb. unsat int fAbs2; // Use UFAR style createAbs int fProofUsePPI; // Use PPI values in PBR + int fUseBmc3; // Run BMC3 in parallel int fVerbose; // verbose output int fPdrVerbose; // verbose output }; diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 3373cdd9..29f66ee3 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -25,6 +25,17 @@ #include "aig/gia/giaAig.h" #include "sat/bmc/bmc.h" +#ifdef ABC_USE_PTHREADS + +#ifdef _WIN32 +#include "../lib/pthread.h" +#else +#include +#include +#endif + +#endif + ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// @@ -67,6 +78,18 @@ struct Wla_Man_t_ abctime tPbr; }; +// information given to the thread +typedef struct Bmc3_ThData_t_ +{ + Aig_Man_t * pAig; + Abc_Cex_t ** ppCex; + int RunId; +} Bmc3_ThData_t; + +// mutext to control access to shared variables +extern pthread_mutex_t g_mutex; +static volatile int g_nRunIds = 0; // the number of the last prover instance + int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b ) { return (*a)->second < (*b)->second; @@ -1299,11 +1322,59 @@ int Wla_ManCheckCombUnsat( Wla_Man_t * pWla, Aig_Man_t * pAig ) return RetValue; } +int Bmc3_test( Aig_Man_t * pAig, int RunId, Abc_Cex_t ** ppCex ) +{ + char * p = ABC_ALLOC( char, 111 ); + while ( 1 ) + { + if ( RunId < g_nRunIds ) + break; + } + ABC_FREE( p ); + return -1; +} + +void * Wla_Bmc3Thread ( void * pArg ) +{ + int RetValue = -1; + Bmc3_ThData_t * pData = (Bmc3_ThData_t *)pArg; + RetValue = Bmc3_test( pData->pAig, pData->RunId, pData->ppCex ); + + if ( RetValue == -1 ) + Abc_Print( 1, "Cancelled bmc3 %d.\n", pData->RunId ); + + // free memory + Aig_ManStop( pData->pAig ); + ABC_FREE( pData ); + + // quit this thread + pthread_exit( NULL ); + assert(0); + return NULL; +} + +void Wla_ManConcurrentBmc3( pthread_t * pThread, Aig_Man_t * pAig ) +{ + int status; + + Bmc3_ThData_t * pData; + pData = ABC_CALLOC( Bmc3_ThData_t, 1 ); + pData->pAig = pAig; + pData->ppCex = NULL; + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); + pData->RunId = ++g_nRunIds; + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + + status = pthread_create( pThread, NULL, Wla_Bmc3Thread, pData ); + assert( status == 0 ); +} + int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) { abctime clk; Pdr_Man_t * pPdr; int RetValue = -1; + int status; if ( pWla->vClauses && pWla->pPars->fCheckCombUnsat ) { @@ -1321,6 +1392,19 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) Abc_PrintTime( 1, "Check comb. unsat failed. Time", Abc_Clock() - clk ); } + if ( pWla->pPars->fUseBmc3 ) + { + pthread_t Bmc3Thread; + + Wla_ManConcurrentBmc3( &Bmc3Thread, Aig_ManDupSimple(pAig) ); + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); + ++g_nRunIds; + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + + status = pthread_join( Bmc3Thread, NULL ); + assert( status == 0 ); + } + clk = Abc_Clock(); pPdr = Pdr_ManStart( pAig, pWla->pPdrPars, NULL ); if ( pWla->vClauses ) { diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 209a3865..871b3e5d 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -464,7 +464,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Wlc_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcdipmuxvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcdipqmuxvwh" ) ) != EOF ) { switch ( c ) { @@ -558,6 +558,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'p': pPars->fPushClauses ^= 1; break; + case 'q': + pPars->fUseBmc3 ^= 1; + break; case 'm': pPars->fMFFC ^= 1; break; @@ -584,7 +587,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) Wlc_NtkPdrAbs( pNtk, pPars ); return 0; usage: - Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcdipmxuvwh]\n" ); + Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcdipqmxuvwh]\n" ); Abc_Print( -2, "\t abstraction for word-level networks\n" ); Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); @@ -601,6 +604,7 @@ usage: Abc_Print( -2, "\t-i : toggle using PPI values in proof-based refinement [default = %s]\n", pPars->fProofUsePPI? "yes": "no" ); Abc_Print( -2, "\t-u : toggle checking combinationally unsat [default = %s]\n", pPars->fCheckCombUnsat? "yes": "no" ); Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" ); + Abc_Print( -2, "\t-q : toggle running bmc3 in parallel for CEX [default = %s]\n", pPars->fUseBmc3? "yes": "no" ); Abc_Print( -2, "\t-m : toggle refining the whole MFFC of a PPI [default = %s]\n", pPars->fMFFC? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" ); diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 8c6f8fbe..d1eaf7c5 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -124,6 +124,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) pPars->fCheckCombUnsat = 0; // Check if ABS becomes comb. unsat pPars->fAbs2 = 0; // Use UFAR style createAbs pPars->fProofUsePPI = 0; // Use PPI values in PBR + pPars->fUseBmc3 = 0; // Run BMC3 in parallel pPars->fVerbose = 0; // verbose output` pPars->fPdrVerbose = 0; // show verbose PDR output } -- cgit v1.2.3 From 3bddf938765c61f67d98451679670434783a7845 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 19 Mar 2017 12:07:45 -0700 Subject: %pdra: working on bmc3 --- src/base/wlc/wlcAbs.c | 90 ++++++++++++++++++++++++++++++++++----------------- 1 file changed, 60 insertions(+), 30 deletions(-) (limited to 'src') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 29f66ee3..b58ef5b5 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -48,6 +48,9 @@ extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPu extern int IPdr_ManCheckCombUnsat( Pdr_Man_t * p ); extern int IPdr_ManReduceClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses ); extern void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs ); +extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pAig ); +extern int Abc_NtkDarBmc3( Abc_Ntk_t * pAbcNtk, Saig_ParBmc_t * pBmcPars, int fOrDecomp ); +extern int Abs_CallBackToStop( int RunId ); typedef struct Int_Pair_t_ Int_Pair_t; struct Int_Pair_t_ @@ -89,6 +92,7 @@ typedef struct Bmc3_ThData_t_ // mutext to control access to shared variables extern pthread_mutex_t g_mutex; static volatile int g_nRunIds = 0; // the number of the last prover instance +static int Wla_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; } int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b ) { @@ -1322,28 +1326,35 @@ int Wla_ManCheckCombUnsat( Wla_Man_t * pWla, Aig_Man_t * pAig ) return RetValue; } -int Bmc3_test( Aig_Man_t * pAig, int RunId, Abc_Cex_t ** ppCex ) -{ - char * p = ABC_ALLOC( char, 111 ); - while ( 1 ) - { - if ( RunId < g_nRunIds ) - break; - } - ABC_FREE( p ); - return -1; -} - void * Wla_Bmc3Thread ( void * pArg ) { + int status; int RetValue = -1; Bmc3_ThData_t * pData = (Bmc3_ThData_t *)pArg; - RetValue = Bmc3_test( pData->pAig, pData->RunId, pData->ppCex ); + Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase( pData->pAig ); + Saig_ParBmc_t BmcPars, *pBmcPars = &BmcPars; + Saig_ParBmcSetDefaultParams( pBmcPars ); + + RetValue = Abc_NtkDarBmc3( pAbcNtk, pBmcPars, 0 ); - if ( RetValue == -1 ) - Abc_Print( 1, "Cancelled bmc3 %d.\n", pData->RunId ); + if ( RetValue == 0 ) + { + assert( pAbcNtk->pSeqModel ); + *(pData->ppCex) = pAbcNtk->pSeqModel; + pAbcNtk->pSeqModel = NULL; + 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 + { + Abc_Print( 1, "BMC3 got cancelled. RunId=%d.\n", pData->RunId ); + } // free memory + Abc_NtkDelete( pAbcNtk ); Aig_ManStop( pData->pAig ); ABC_FREE( pData ); @@ -1353,17 +1364,15 @@ void * Wla_Bmc3Thread ( void * pArg ) return NULL; } -void Wla_ManConcurrentBmc3( pthread_t * pThread, Aig_Man_t * pAig ) +void Wla_ManConcurrentBmc3( pthread_t * pThread, Aig_Man_t * pAig, Abc_Cex_t ** ppCex ) { int status; Bmc3_ThData_t * pData; pData = ABC_CALLOC( Bmc3_ThData_t, 1 ); pData->pAig = pAig; - pData->ppCex = NULL; - status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); - pData->RunId = ++g_nRunIds; - status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + pData->ppCex = ppCex; + pData->RunId = g_nRunIds; status = pthread_create( pThread, NULL, Wla_Bmc3Thread, pData ); assert( status == 0 ); @@ -1373,8 +1382,11 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) { abctime clk; Pdr_Man_t * pPdr; + Abc_Cex_t * pBmcCex = NULL; + pthread_t * pBmc3Thread = NULL; int RetValue = -1; int status; + int RunId = g_nRunIds; if ( pWla->vClauses && pWla->pPars->fCheckCombUnsat ) { @@ -1394,15 +1406,11 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) if ( pWla->pPars->fUseBmc3 ) { - pthread_t Bmc3Thread; + pWla->pPdrPars->RunId = g_nRunIds; + pWla->pPdrPars->pFuncStop = Wla_CallBackToStop; - Wla_ManConcurrentBmc3( &Bmc3Thread, Aig_ManDupSimple(pAig) ); - status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); - ++g_nRunIds; - status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); - - status = pthread_join( Bmc3Thread, NULL ); - assert( status == 0 ); + pBmc3Thread = ABC_CALLOC( pthread_t, 1 ); + Wla_ManConcurrentBmc3( pBmc3Thread, Aig_ManDupSimple( pAig ), &pBmcCex ); } clk = Abc_Clock(); @@ -1418,8 +1426,30 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) pWla->vClauses = IPdr_ManSaveClauses( pPdr, 0 ); Pdr_ManStop( pPdr ); - pWla->pCex = pAig->pSeqModel; - pAig->pSeqModel = NULL; + + if ( pWla->pPars->fUseBmc3 ) + { + 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( *pBmc3Thread, NULL ); + assert( status == 0 ); + ABC_FREE( pBmc3Thread ); + } + + if ( pBmcCex ) + { + pWla->pCex = pBmcCex ; + } + else + { + pWla->pCex = pAig->pSeqModel; + pAig->pSeqModel = NULL; + } // consider outcomes if ( pWla->pCex == NULL ) -- cgit v1.2.3 From 51fbf37cb42951c668e9fa4df9ddd99897a6fb4d Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 19 Mar 2017 12:41:06 -0700 Subject: %pdra: working on bmc3 --- src/base/wlc/wlcAbs.c | 15 +++++++++++---- src/sat/bmc/bmc.h | 2 ++ src/sat/bmc/bmcBmc3.c | 6 ++++++ 3 files changed, 19 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index b58ef5b5..8f3fe92f 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -87,6 +87,7 @@ 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 @@ -1334,6 +1335,8 @@ void * Wla_Bmc3Thread ( void * 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 ); @@ -1342,7 +1345,9 @@ void * Wla_Bmc3Thread ( void * pArg ) assert( pAbcNtk->pSeqModel ); *(pData->ppCex) = pAbcNtk->pSeqModel; pAbcNtk->pSeqModel = NULL; - Abc_Print( 1, "BMC3 found CEX. RunId=%d.\n", pData->RunId ); + + 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; @@ -1350,7 +1355,8 @@ void * Wla_Bmc3Thread ( void * pArg ) } else { - Abc_Print( 1, "BMC3 got cancelled. RunId=%d.\n", pData->RunId ); + if ( pData->fVerbose ) + Abc_Print( 1, "Bmc3 was cancelled. RunId=%d.\n", pData->RunId ); } // free memory @@ -1364,7 +1370,7 @@ void * Wla_Bmc3Thread ( void * pArg ) return NULL; } -void Wla_ManConcurrentBmc3( pthread_t * pThread, Aig_Man_t * pAig, Abc_Cex_t ** ppCex ) +void Wla_ManConcurrentBmc3( pthread_t * pThread, Aig_Man_t * pAig, Abc_Cex_t ** ppCex, int fVerbose ) { int status; @@ -1373,6 +1379,7 @@ void Wla_ManConcurrentBmc3( pthread_t * pThread, Aig_Man_t * pAig, Abc_Cex_t ** pData->pAig = pAig; pData->ppCex = ppCex; pData->RunId = g_nRunIds; + pData->fVerbose = fVerbose; status = pthread_create( pThread, NULL, Wla_Bmc3Thread, pData ); assert( status == 0 ); @@ -1410,7 +1417,7 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) pWla->pPdrPars->pFuncStop = Wla_CallBackToStop; pBmc3Thread = ABC_CALLOC( pthread_t, 1 ); - Wla_ManConcurrentBmc3( pBmc3Thread, Aig_ManDupSimple( pAig ), &pBmcCex ); + Wla_ManConcurrentBmc3( pBmc3Thread, Aig_ManDupSimple( pAig ), &pBmcCex, pWla->pPars->fVerbose ); } clk = Abc_Clock(); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index a3f353c2..22ae765d 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -73,6 +73,8 @@ struct Saig_ParBmc_t_ int nDropOuts; // the number of dropped outputs abctime timeLastSolved; // the time when the last output was solved int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode + int RunId; // BMC id in this run + int(*pFuncStop)(int); // callback to terminate }; diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index ccd0bb90..34fdf45f 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1533,6 +1533,12 @@ clkOther += Abc_Clock() - clk2; Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut ); goto finish; } + if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) ) + { + if ( !pPars->fSilent ) + Abc_Print( 1, "Bmc3 got callbacks.\n" ); + goto finish; + } // skip solved outputs if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) continue; -- cgit v1.2.3 From 875411985ccbacfc7947e80ad2d04059e0ae99a4 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 19 Mar 2017 14:21:19 -0700 Subject: %pdra: working on bmc3 --- src/base/wlc/module.make | 1 + src/base/wlc/wlc.h | 23 +++++++ src/base/wlc/wlcAbs.c | 148 +++++---------------------------------------- src/base/wlc/wlcPth.c | 152 +++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 192 insertions(+), 132 deletions(-) create mode 100644 src/base/wlc/wlcPth.c (limited to 'src') diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make index 29770937..32586c9e 100644 --- a/src/base/wlc/module.make +++ b/src/base/wlc/module.make @@ -1,6 +1,7 @@ SRC += src/base/wlc/wlcAbs.c \ src/base/wlc/wlcAbs2.c \ src/base/wlc/wlcAbc.c \ + src/base/wlc/wlcPth.c \ src/base/wlc/wlcBlast.c \ src/base/wlc/wlcCom.c \ src/base/wlc/wlcGraft.c \ diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 0e28f98d..5d4f374e 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -185,6 +185,29 @@ struct Wlc_Par_t_ int fPdrVerbose; // verbose output }; +typedef struct Wla_Man_t_ Wla_Man_t; +struct Wla_Man_t_ +{ + Wlc_Ntk_t * p; + Wlc_Par_t * pPars; + Vec_Vec_t * vClauses; + Vec_Int_t * vBlacks; + Abc_Cex_t * pCex; + Gia_Man_t * pGia; + Vec_Bit_t * vUnmark; + void * pPdrPars; + void * pThread; + + int nIters; + int nTotalCla; + int nDisj; + int nNDisj; + + abctime tPdr; + abctime tCbr; + abctime tPbr; +}; + static inline int Wlc_NtkObjNum( Wlc_Ntk_t * p ) { return p->iObj - 1; } static inline int Wlc_NtkObjNumMax( Wlc_Ntk_t * p ) { return p->iObj; } static inline int Wlc_NtkPiNum( Wlc_Ntk_t * p ) { return Vec_IntSize(&p->vPis); } diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 8f3fe92f..f069c95f 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -25,17 +25,6 @@ #include "aig/gia/giaAig.h" #include "sat/bmc/bmc.h" -#ifdef ABC_USE_PTHREADS - -#ifdef _WIN32 -#include "../lib/pthread.h" -#else -#include -#include -#endif - -#endif - ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// @@ -48,9 +37,10 @@ extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPu extern int IPdr_ManCheckCombUnsat( Pdr_Man_t * p ); extern int IPdr_ManReduceClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses ); extern void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs ); -extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pAig ); -extern int Abc_NtkDarBmc3( Abc_Ntk_t * pAbcNtk, Saig_ParBmc_t * pBmcPars, int fOrDecomp ); -extern int Abs_CallBackToStop( int RunId ); +extern void Wla_ManJoinThread( Wla_Man_t * pWla, int RunId ); +extern void Wla_ManConcurrentBmc3( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppCex ); +extern int Wla_CallBackToStop( int RunId ); +extern int Wla_GetGlobalRunId(); typedef struct Int_Pair_t_ Int_Pair_t; struct Int_Pair_t_ @@ -59,42 +49,6 @@ struct Int_Pair_t_ int second; }; -typedef struct Wla_Man_t_ Wla_Man_t; -struct Wla_Man_t_ -{ - Wlc_Ntk_t * p; - Wlc_Par_t * pPars; - Pdr_Par_t * pPdrPars; - Vec_Vec_t * vClauses; - Vec_Int_t * vBlacks; - Abc_Cex_t * pCex; - Gia_Man_t * pGia; - Vec_Bit_t * vUnmark; - - int nIters; - int nTotalCla; - int nDisj; - int nNDisj; - - abctime tPdr; - abctime tCbr; - abctime tPbr; -}; - -// 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; -static volatile int g_nRunIds = 0; // the number of the last prover instance -static int Wla_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; } - int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b ) { return (*a)->second < (*b)->second; @@ -1282,6 +1236,7 @@ Aig_Man_t * Wla_ManBitBlast( Wla_Man_t * pWla, Wlc_Ntk_t * pAbs ) int Wla_ManCheckCombUnsat( Wla_Man_t * pWla, Aig_Man_t * pAig ) { Pdr_Man_t * pPdr; + Pdr_Par_t * pPdrPars = (Pdr_Par_t *)pWla->pPdrPars; abctime clk; int RetValue = -1; @@ -1316,84 +1271,25 @@ int Wla_ManCheckCombUnsat( Wla_Man_t * pWla, Aig_Man_t * pAig ) clk = Abc_Clock(); - pWla->pPdrPars->fVerbose = 0; - pPdr = Pdr_ManStart( pAig, pWla->pPdrPars, NULL ); + pPdrPars->fVerbose = 0; + pPdr = Pdr_ManStart( pAig, pPdrPars, NULL ); RetValue = IPdr_ManCheckCombUnsat( pPdr ); Pdr_ManStop( pPdr ); - pWla->pPdrPars->fVerbose = pWla->pPars->fPdrVerbose; + pPdrPars->fVerbose = pWla->pPars->fPdrVerbose; pWla->tPdr += Abc_Clock() - clk; return RetValue; } -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( pthread_t * pThread, Aig_Man_t * pAig, Abc_Cex_t ** ppCex, int fVerbose ) -{ - int status; - - Bmc3_ThData_t * pData; - pData = ABC_CALLOC( Bmc3_ThData_t, 1 ); - pData->pAig = pAig; - pData->ppCex = ppCex; - pData->RunId = g_nRunIds; - pData->fVerbose = fVerbose; - - status = pthread_create( pThread, NULL, Wla_Bmc3Thread, pData ); - assert( status == 0 ); -} - int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) { abctime clk; Pdr_Man_t * pPdr; + Pdr_Par_t * pPdrPars = (Pdr_Par_t *)pWla->pPdrPars; Abc_Cex_t * pBmcCex = NULL; - pthread_t * pBmc3Thread = NULL; int RetValue = -1; - int status; - int RunId = g_nRunIds; + int RunId = Wla_GetGlobalRunId(); if ( pWla->vClauses && pWla->pPars->fCheckCombUnsat ) { @@ -1413,15 +1309,14 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) if ( pWla->pPars->fUseBmc3 ) { - pWla->pPdrPars->RunId = g_nRunIds; - pWla->pPdrPars->pFuncStop = Wla_CallBackToStop; + pPdrPars->RunId = RunId; + pPdrPars->pFuncStop = Wla_CallBackToStop; - pBmc3Thread = ABC_CALLOC( pthread_t, 1 ); - Wla_ManConcurrentBmc3( pBmc3Thread, Aig_ManDupSimple( pAig ), &pBmcCex, pWla->pPars->fVerbose ); + Wla_ManConcurrentBmc3( pWla, Aig_ManDupSimple(pAig), &pBmcCex ); } clk = Abc_Clock(); - pPdr = Pdr_ManStart( pAig, pWla->pPdrPars, NULL ); + pPdr = Pdr_ManStart( pAig, pPdrPars, NULL ); if ( pWla->vClauses ) { assert( Vec_VecSize( pWla->vClauses) >= 2 ); IPdr_ManRestore( pPdr, pWla->vClauses, NULL ); @@ -1435,18 +1330,7 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) if ( pWla->pPars->fUseBmc3 ) - { - 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( *pBmc3Thread, NULL ); - assert( status == 0 ); - ABC_FREE( pBmc3Thread ); - } + Wla_ManJoinThread( pWla, RunId ); if ( pBmcCex ) { @@ -1551,7 +1435,7 @@ Wla_Man_t * Wla_ManStart( Wlc_Ntk_t * pNtk, Wlc_Par_t * pPars ) pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization) pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this } - p->pPdrPars = pPdrPars; + p->pPdrPars = (void *)pPdrPars; p->nIters = 1; p->nTotalCla = 0; 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 +#include +#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 + -- cgit v1.2.3