Merged in ysho/abc (pull request #69)

Improvements to %pdra

8 files changed, 272 insertions, 65 deletions

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;