1 /**CFile****************************************************************
2
3 FileName [absPth.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Abstraction package.]
8
9 Synopsis [Interface to pthreads.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: absPth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "abs.h"
22 #include "proof/pdr/pdr.h"
23 #include "proof/ssw/ssw.h"
24
25
26 #ifdef ABC_USE_PTHREADS
27
28 #ifdef _WIN32
29 #include "../lib/pthread.h"
30 #else
31 #include <pthread.h>
32 #include <unistd.h>
33 #endif
34
35 #endif
36
37 ABC_NAMESPACE_IMPL_START
38
39 ////////////////////////////////////////////////////////////////////////
40 /// DECLARATIONS ///
41 ////////////////////////////////////////////////////////////////////////
42
43 #ifndef ABC_USE_PTHREADS
44
Gia_GlaProveAbsracted(Gia_Man_t * p,int fSimpProver,int fVerbose)45 void Gia_GlaProveAbsracted( Gia_Man_t * p, int fSimpProver, int fVerbose ) {}
Gia_GlaProveCancel(int fVerbose)46 void Gia_GlaProveCancel( int fVerbose ) {}
Gia_GlaProveCheck(int fVerbose)47 int Gia_GlaProveCheck( int fVerbose ) { return 0; }
48
49 #else // pthreads are used
50
51 // information given to the thread
52 typedef struct Abs_ThData_t_
53 {
54 Aig_Man_t * pAig;
55 int fVerbose;
56 int RunId;
57 } Abs_ThData_t;
58
59 // mutext to control access to shared variables
60 pthread_mutex_t g_mutex = PTHREAD_MUTEX_INITIALIZER;
61 static volatile int g_nRunIds = 0; // the number of the last prover instance
62 static volatile int g_fAbstractionProved = 0; // set to 1 when prover successed to prove
63
64 // call back procedure for PDR
65 int Abs_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }
66
67 // test procedure to replace PDR
68 int Pdr_ManSolve_test( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
69 {
70 char * p = ABC_ALLOC( char, 111 );
71 while ( 1 )
72 {
73 if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) )
74 break;
75 }
76 ABC_FREE( p );
77 return -1;
78 }
79
80 ////////////////////////////////////////////////////////////////////////
81 /// FUNCTION DEFINITIONS ///
82 ////////////////////////////////////////////////////////////////////////
83
84 /**Function*************************************************************
85
86 Synopsis [Create one thread]
87
88 Description []
89
90 SideEffects []
91
92 SeeAlso []
93
94 ***********************************************************************/
95 void * Abs_ProverThread( void * pArg )
96 {
97 Abs_ThData_t * pThData = (Abs_ThData_t *)pArg;
98 Pdr_Par_t Pars, * pPars = &Pars;
99 int RetValue, status;
100 // call PDR
101 Pdr_ManSetDefaultParams( pPars );
102 pPars->fSilent = 1;
103 pPars->RunId = pThData->RunId;
104 pPars->pFuncStop = Abs_CallBackToStop;
105 RetValue = Pdr_ManSolve( pThData->pAig, pPars );
106 // update the result
107 if ( RetValue == 1 )
108 {
109 status = pthread_mutex_lock(&g_mutex); assert( status == 0 );
110 g_fAbstractionProved = 1;
111 status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
112 }
113 // quit this thread
114 if ( pThData->fVerbose )
115 {
116 if ( RetValue == 1 )
117 Abc_Print( 1, "Proved abstraction %d.\n", pThData->RunId );
118 else if ( RetValue == 0 )
119 Abc_Print( 1, "Disproved abstraction %d.\n", pThData->RunId );
120 else if ( RetValue == -1 )
121 Abc_Print( 1, "Cancelled abstraction %d.\n", pThData->RunId );
122 else assert( 0 );
123 }
124 // free memory
125 Aig_ManStop( pThData->pAig );
126 ABC_FREE( pThData );
127 // quit this thread
128 pthread_exit( NULL );
129 assert(0);
130 return NULL;
131 }
132 void Gia_GlaProveAbsracted( Gia_Man_t * pGia, int fSimpProver, int fVerbose )
133 {
134 extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
135 Abs_ThData_t * pThData;
136 Ssw_Pars_t Pars, * pPars = &Pars;
137 Aig_Man_t * pAig, * pTemp;
138 Gia_Man_t * pAbs;
139 pthread_t ProverThread;
140 int status;
141 // disable verbosity
142 // fVerbose = 0;
143 // create abstraction
144 assert( pGia->vGateClasses != NULL );
145 pAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses );
146 Gia_ManCleanValue( pGia );
147 pAig = Gia_ManToAigSimple( pAbs );
148 Gia_ManStop( pAbs );
149 // simplify abstraction
150 if ( fSimpProver )
151 {
152 Ssw_ManSetDefaultParams( pPars );
153 pPars->nFramesK = 4;
154 pAig = Ssw_SignalCorrespondence( pTemp = pAig, pPars );
155 //printf( "\n" );
156 //Aig_ManPrintStats( pTemp );
157 //Aig_ManPrintStats( pAig );
158 Aig_ManStop( pTemp );
159 }
160 // synthesize abstraction
161 // pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 );
162 // Aig_ManStop( pTemp );
163 // reset the proof
164 status = pthread_mutex_lock(&g_mutex); assert( status == 0 );
165 g_fAbstractionProved = 0;
166 status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
167 // collect thread data
168 pThData = ABC_CALLOC( Abs_ThData_t, 1 );
169 pThData->pAig = pAig;
170 pThData->fVerbose = fVerbose;
171 status = pthread_mutex_lock(&g_mutex); assert( status == 0 );
172 pThData->RunId = ++g_nRunIds;
173 status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
174 // create thread
175 if ( fVerbose ) Abc_Print( 1, "\nTrying to prove abstraction %d.\n", pThData->RunId );
176 status = pthread_create( &ProverThread, NULL, Abs_ProverThread, pThData );
177 assert( status == 0 );
178 }
179 void Gia_GlaProveCancel( int fVerbose )
180 {
181 int status;
182 status = pthread_mutex_lock(&g_mutex); assert( status == 0 );
183 g_nRunIds++;
184 status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
185 }
186 int Gia_GlaProveCheck( int fVerbose )
187 {
188 int status;
189 if ( g_fAbstractionProved == 0 )
190 return 0;
191 status = pthread_mutex_lock(&g_mutex); assert( status == 0 );
192 g_fAbstractionProved = 0;
193 status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
194 return 1;
195 }
196
197 #endif // pthreads are used
198
199 ////////////////////////////////////////////////////////////////////////
200 /// END OF FILE ///
201 ////////////////////////////////////////////////////////////////////////
202
203
204 ABC_NAMESPACE_IMPL_END
205
206