%pdra: working on bmc3

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
 };

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 <pthread.h>
+#include <unistd.h>
+#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 ) {

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" );

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
 }