summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abclib.dsp4
-rw-r--r--src/base/wlc/module.make1
-rw-r--r--src/base/wlc/wlc.h24
-rw-r--r--src/base/wlc/wlcAbs.c143
-rw-r--r--src/base/wlc/wlcCom.c8
-rw-r--r--src/base/wlc/wlcNtk.c1
-rw-r--r--src/base/wlc/wlcPth.c152
-rw-r--r--src/sat/bmc/bmc.h2
-rw-r--r--src/sat/bmc/bmcBmc3.c6
9 files changed, 276 insertions, 65 deletions
diff --git a/abclib.dsp b/abclib.dsp
index b04d8b54..0068855a 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -787,6 +787,10 @@ SOURCE=.\src\base\wlc\wlcAbs.c
# End Source File
# Begin Source File
+SOURCE=.\src\base\wlc\wlcPth.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\base\wlc\wlcAbs2.c
# End Source File
# Begin Source File
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 53936cc9..5d4f374e 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -180,10 +180,34 @@ 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
};
+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 c89ed187..f069c95f 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -37,6 +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 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_
@@ -45,28 +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;
-};
-
int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b )
{
return (*a)->second < (*b)->second;
@@ -1251,53 +1233,69 @@ 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;
+ Pdr_Par_t * pPdrPars = (Pdr_Par_t *)pWla->pPdrPars;
+ 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();
+
+ pPdrPars->fVerbose = 0;
+ pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
+ RetValue = IPdr_ManCheckCombUnsat( pPdr );
+ Pdr_ManStop( pPdr );
+ 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;
Pdr_Man_t * pPdr;
+ Pdr_Par_t * pPdrPars = (Pdr_Par_t *)pWla->pPdrPars;
+ Abc_Cex_t * pBmcCex = NULL;
int RetValue = -1;
+ int RunId = Wla_GetGlobalRunId();
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 )
@@ -1309,8 +1307,16 @@ 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 )
+ {
+ pPdrPars->RunId = RunId;
+ pPdrPars->pFuncStop = Wla_CallBackToStop;
+
+ 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 );
@@ -1322,8 +1328,19 @@ 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 )
+ Wla_ManJoinThread( pWla, RunId );
+
+ if ( pBmcCex )
+ {
+ pWla->pCex = pBmcCex ;
+ }
+ else
+ {
+ pWla->pCex = pAig->pSeqModel;
+ pAig->pSeqModel = NULL;
+ }
// consider outcomes
if ( pWla->pCex == NULL )
@@ -1418,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/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
}
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
+
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;
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-30 03:03:55 +0000