1 /**CFile****************************************************************
2
3 FileName [wlcPth.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Verilog parser.]
8
9 Synopsis [Abstraction for word-level networks.]
10
11 Author [Yen-Sheng Ho, Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: wlcPth.c $]
18
19 ***********************************************************************/
20
21 #include "wlc.h"
22 #include "sat/bmc/bmc.h"
23
24 #ifdef ABC_USE_PTHREADS
25
26 #ifdef _WIN32
27 #include "../lib/pthread.h"
28 #else
29 #include <pthread.h>
30 #include <unistd.h>
31 #endif
32
33 #endif
34
35 ABC_NAMESPACE_IMPL_START
36
37 ////////////////////////////////////////////////////////////////////////
38 /// DECLARATIONS ///
39 ////////////////////////////////////////////////////////////////////////
40
41 extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pAig );
42 extern int Abc_NtkDarBmc3( Abc_Ntk_t * pAbcNtk, Saig_ParBmc_t * pBmcPars, int fOrDecomp );
43 extern int Wla_ManShrinkAbs( Wla_Man_t * pWla, int nFrames, int RunId );
44
45 static volatile int g_nRunIds = 0; // the number of the last prover instance
Wla_CallBackToStop(int RunId)46 int Wla_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }
Wla_GetGlobalRunId()47 int Wla_GetGlobalRunId() { return g_nRunIds; }
48
49 #ifndef ABC_USE_PTHREADS
50
Wla_ManJoinThread(Wla_Man_t * pWla,int RunId)51 void Wla_ManJoinThread( Wla_Man_t * pWla, int RunId ) {}
Wla_ManConcurrentBmc3(Wla_Man_t * pWla,Aig_Man_t * pAig,Abc_Cex_t ** ppCex)52 void Wla_ManConcurrentBmc3( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppCex ) {}
53
54 #else // pthreads are used
55
56 // information given to the thread
57 typedef struct Bmc3_ThData_t_
58 {
59 Wla_Man_t * pWla;
60 Aig_Man_t * pAig;
61 Abc_Cex_t ** ppCex;
62 int RunId;
63 int fVerbose;
64 } Bmc3_ThData_t;
65
66 // mutext to control access to shared variables
67 extern pthread_mutex_t g_mutex;
68
Wla_ManJoinThread(Wla_Man_t * pWla,int RunId)69 void Wla_ManJoinThread( Wla_Man_t * pWla, int RunId )
70 {
71 int status;
72 if ( RunId == g_nRunIds )
73 {
74 status = pthread_mutex_lock(&g_mutex); assert( status == 0 );
75 ++g_nRunIds;
76 status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
77 }
78
79 status = pthread_join( *(pthread_t *)(pWla->pThread), NULL );
80 assert( status == 0 );
81 ABC_FREE( pWla->pThread );
82 pWla->pThread = NULL;
83 }
84
Wla_Bmc3Thread(void * pArg)85 void * Wla_Bmc3Thread ( void * pArg )
86 {
87 int status;
88 int RetValue = -1;
89 int nFramesNoChangeLim = 10;
90 Bmc3_ThData_t * pData = (Bmc3_ThData_t *)pArg;
91 Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase( pData->pAig );
92 Saig_ParBmc_t BmcPars, *pBmcPars = &BmcPars;
93 Saig_ParBmcSetDefaultParams( pBmcPars );
94 pBmcPars->pFuncStop = Wla_CallBackToStop;
95 pBmcPars->RunId = pData->RunId;
96
97 if ( pData->pWla->pPars->fShrinkAbs )
98 pBmcPars->nFramesMax = pData->pWla->iCexFrame + nFramesNoChangeLim;
99
100 RetValue = Abc_NtkDarBmc3( pAbcNtk, pBmcPars, 0 );
101
102 if ( RetValue == 0 )
103 {
104 assert( pAbcNtk->pSeqModel );
105 *(pData->ppCex) = pAbcNtk->pSeqModel;
106 pAbcNtk->pSeqModel = NULL;
107
108 if ( pData->fVerbose )
109 Abc_Print( 1, "Bmc3 found CEX. RunId=%d.\n", pData->RunId );
110
111 status = pthread_mutex_lock(&g_mutex); assert( status == 0 );
112 ++g_nRunIds;
113 status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
114 }
115 else if ( RetValue == -1 )
116 {
117 if ( pData->RunId < g_nRunIds && pData->fVerbose )
118 Abc_Print( 1, "Bmc3 was cancelled. RunId=%d.\n", pData->RunId );
119
120 if ( pData->pWla->nIters > 1 && pData->RunId == g_nRunIds )
121 {
122 RetValue = Wla_ManShrinkAbs( pData->pWla, pData->pWla->iCexFrame + nFramesNoChangeLim, pData->RunId );
123 pData->pWla->iCexFrame += nFramesNoChangeLim;
124
125 if ( RetValue == 1 )
126 {
127 pData->pWla->fNewAbs = 1;
128 status = pthread_mutex_lock(&g_mutex); assert( status == 0 );
129 ++g_nRunIds;
130 status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
131 }
132 }
133 }
134
135 // free memory
136 Abc_NtkDelete( pAbcNtk );
137 Aig_ManStop( pData->pAig );
138 ABC_FREE( pData );
139
140 // quit this thread
141 pthread_exit( NULL );
142 assert(0);
143 return NULL;
144 }
145
Wla_ManConcurrentBmc3(Wla_Man_t * pWla,Aig_Man_t * pAig,Abc_Cex_t ** ppCex)146 void Wla_ManConcurrentBmc3( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppCex )
147 {
148 int status;
149 Bmc3_ThData_t * pData;
150
151 assert( pWla->pThread == NULL );
152 pWla->pThread = (void *)ABC_CALLOC( pthread_t, 1 );
153
154 pData = ABC_CALLOC( Bmc3_ThData_t, 1 );
155 pData->pWla = pWla;
156 pData->pAig = pAig;
157 pData->ppCex = ppCex;
158 pData->RunId = g_nRunIds;
159 pData->fVerbose = pWla->pPars->fVerbose;
160
161 status = pthread_create( (pthread_t *)pWla->pThread, NULL, Wla_Bmc3Thread, pData );
162 assert( status == 0 );
163 }
164
165 #endif // pthreads are used
166
167 ////////////////////////////////////////////////////////////////////////
168 /// END OF FILE ///
169 ////////////////////////////////////////////////////////////////////////
170
171
172 ABC_NAMESPACE_IMPL_END
173
174