%pdra: working on bmc3

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
+