ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaTranStoch.c
Go to the documentation of this file.
1
20
21#include <base/abc/abc.h>
22#include <aig/aig/aig.h>
23#include <opt/dar/dar.h>
24#include <aig/gia/gia.h>
25#include <aig/gia/giaAig.h>
26#include <base/main/main.h>
27#include <base/main/mainInt.h>
28#include <map/mio/mio.h>
29#include <opt/sfm/sfm.h>
30#include <opt/fxu/fxu.h>
31
32#ifdef _MSC_VER
33#define unlink _unlink
34#else
35#include <unistd.h>
36#endif
37
38#ifdef ABC_USE_PTHREADS
39
40#ifdef _WIN32
41#include "../lib/pthread.h"
42#else
43#include <pthread.h>
44#endif
45
46#endif
47
49
50extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
51extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
52extern int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars );
53extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
54extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int nLitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose );
55
57 Abc_Ntk_t * pNtk;
58 Aig_Man_t * pMan = Gia_ManToAig( pGia, 0 );
59 pNtk = Abc_NtkFromAigPhase( pMan );
60 Aig_ManStop( pMan );
61 return pNtk;
62}
64 If_Par_t Pars, * pPars = &Pars;
65 If_ManSetDefaultPars( pPars );
67 pPars->nLutSize = pPars->pLutLib->LutMax;
68 return Abc_NtkIf( pNtk, pPars );
69}
71 Sfm_Par_t Pars, * pPars = &Pars;
72 Sfm_ParSetDefault( pPars );
73 Abc_NtkPerformMfs( pNtk, pPars );
74}
76 Gia_Man_t * pGia;
77 Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
78 pGia = Gia_ManFromAig( pAig );
79 Aig_ManStop( pAig );
80 return pGia;
81}
83 Fxu_Data_t Params, * p = &Params;
85 Abc_NtkFxPerform( pNtk, p->nNodesExt, p->LitCountMax, p->fCanonDivs, p->fVerbose, p->fVeryVerbose );
87}
89 Gia_Man_t * pNew;
90 Aig_Man_t * pAig, * pTemp;
91 Dar_RefPar_t Pars, * pPars = &Pars;
93 pPars->fUseZeros = 1;
94 pAig = Gia_ManToAig( pGia, 0 );
95 Dar_ManRefactor( pAig, pPars );
96 pAig = Aig_ManDupDfs( pTemp = pAig );
97 Aig_ManStop( pTemp );
98 pNew = Gia_ManFromAig( pAig );
99 Aig_ManStop( pAig );
100 return pNew;
101}
102
105 int nSeed;
106 int nHops;
109 int fMspf;
118
119#ifdef ABC_USE_PTHREADS
120 int nSp;
121 int nIte;
122 Gia_Man_t * pRes;
123 int fWorking;
124 pthread_mutex_t * mutex;
125#endif
126};
127
129
131#ifdef ABC_USE_PTHREADS
132 if ( p->fWorking )
133 pthread_mutex_lock( p->mutex );
134#endif
135}
137#ifdef ABC_USE_PTHREADS
138 if ( p->fWorking )
139 pthread_mutex_unlock( p->mutex );
140#endif
141}
142
144 Gia_Man_t * pGia, * pNew;
145 int i = 0, n;
146 pGia = Gia_ManDup( pOld );
147 do {
148 n = Gia_ManAndNum( pGia );
149 if ( p->fTruth )
150 pNew = Gia_ManTransductionTt( pGia, (p->fMerge? 8: 7), p->fMspf, p->nSeed++, 0, 0, 0, 0, p->pExdc, p->fNewLine, p->nVerbose > 0? p->nVerbose - 1: 0 );
151 else
152 pNew = Gia_ManTransductionBdd( pGia, (p->fMerge? 8: 7), p->fMspf, p->nSeed++, 0, 0, 0, 0, p->pExdc, p->fNewLine, p->nVerbose > 0? p->nVerbose - 1: 0 );
153 Gia_ManStop( pGia );
154 pGia = pNew;
155 if ( p->fRefactor ) {
156 pNew = Gia_ManTranStochRefactor( pGia );
157 Gia_ManStop( pGia );
158 pGia = pNew;
159 } else {
161 pNew = Gia_ManCompress2( pGia, 1, 0 );
163 Gia_ManStop( pGia );
164 pGia = pNew;
165 }
166 if ( p->nVerbose )
167 printf( "* ite %d : #nodes = %5d\n", i, Gia_ManAndNum( pGia ) );
168 i++;
169 } while ( n > Gia_ManAndNum( pGia ) );
170 return pGia;
171}
172
174 int i, n = Gia_ManAndNum( p->pStart );
175 Gia_Man_t * pGia, * pBest, * pNew;
176 Abc_Ntk_t * pNtk, * pNtkRes;
177 pGia = Gia_ManDup( p->pStart );
178 pBest = Gia_ManDup( pGia );
179 for ( i = 0; 1; i++ ) {
180 pNew = Gia_ManTranStochOpt1( p, pGia );
181 Gia_ManStop( pGia );
182 pGia = pNew;
183 if ( n > Gia_ManAndNum( pGia ) ) {
184 n = Gia_ManAndNum( pGia );
185 Gia_ManStop( pBest );
186 pBest = Gia_ManDup( pGia );
187 if ( p->fResetHop )
188 i = 0;
189 }
190 if ( i == p->nHops )
191 break;
192 if ( p->fZeroCostHop ) {
193 pNew = Gia_ManTranStochRefactor( pGia );
194 Gia_ManStop( pGia );
195 pGia = pNew;
196 } else {
198 pNtk = Gia_ManTranStochPut( pGia );
200 Gia_ManStop( pGia );
201 pNtkRes = Gia_ManTranStochIf( pNtk );
202 Abc_NtkDelete( pNtk );
203 pNtk = pNtkRes;
204 Gia_ManTranStochMfs2( pNtk );
206 pNtkRes = Abc_NtkStrash( pNtk, 0, 1, 0 );
208 Abc_NtkDelete( pNtk );
209 pNtk = pNtkRes;
210 pGia = Gia_ManTranStochGet( pNtk );
211 Abc_NtkDelete( pNtk );
212 }
213 if ( p->nVerbose )
214 printf( "* hop %d : #nodes = %5d\n", i, Gia_ManAndNum( pGia ) );
215 }
216 Gia_ManStop( pGia );
217 return pBest;
218}
219
221 int i, n = Gia_ManAndNum( p->pStart );
222 Gia_Man_t * pBest, * pNew;
223 pBest = Gia_ManDup( p->pStart );
224 for ( i = 0; i <= p->nRestarts; i++ ) {
225 p->nSeed = 1234 * (i + p->nSeedBase);
226 pNew = Gia_ManTranStochOpt2( p );
227 if ( p->nRestarts && p->nVerbose )
228 printf( "* res %2d : #nodes = %5d\n", i, Gia_ManAndNum( pNew ) );
229 if ( n > Gia_ManAndNum( pNew ) ) {
230 n = Gia_ManAndNum( pNew );
231 Gia_ManStop( pBest );
232 pBest = pNew;
233 } else {
234 Gia_ManStop( pNew );
235 }
236 }
237 return pBest;
238}
239
240#ifdef ABC_USE_PTHREADS
241void * Gia_ManTranStochWorkerThread( void * pArg ) {
243 volatile int * pPlace = &p->fWorking;
244 while ( 1 ) {
245 while ( *pPlace == 0 );
246 assert( p->fWorking );
247 if ( p->pStart == NULL ) {
248 pthread_exit( NULL );
249 assert( 0 );
250 return NULL;
251 }
252 p->nSeed = 1234 * (p->nIte + p->nSeedBase);
253 p->pRes = Gia_ManTranStochOpt2( p );
254 p->fWorking = 0;
255 }
256 assert( 0 );
257 return NULL;
258}
259#endif
260
261Gia_Man_t * Gia_ManTranStoch( Gia_Man_t * pGia, int nRestarts, int nHops, int nSeedBase, int fMspf, int fMerge, int fResetHop, int fZeroCostHop, int fRefactor, int fTruth, int fSingle, int fOriginalOnly, int fNewLine, Gia_Man_t * pExdc, int nThreads, int nVerbose ) {
262 int i, j = 0;
263 Gia_Man_t * pNew, * pBest, * pStart;
264 Abc_Ntk_t * pNtk, * pNtkRes; Vec_Ptr_t * vpStarts;
265 Gia_ManTranStochParam Par, *p = &Par;
266 p->nRestarts = nRestarts;
267 p->nHops = nHops;
268 p->nSeedBase = nSeedBase;
269 p->fMspf = fMspf;
270 p->fMerge = fMerge;
271 p->fResetHop = fResetHop;
272 p->fZeroCostHop = fZeroCostHop;
273 p->fRefactor = fRefactor;
274 p->fTruth = fTruth;
275 p->fNewLine = fNewLine;
276 p->pExdc = pExdc;
277 p->nVerbose = nVerbose;
278#ifdef ABC_USE_PTHREADS
279 p->fWorking = 0;
280#endif
281 // setup start points
282 vpStarts = Vec_PtrAlloc( 4 );
283 Vec_PtrPush( vpStarts, Gia_ManDup( pGia ) );
284 if ( !fOriginalOnly ) {
285 { // &put; collapse; st; &get;
286 pNtk = Gia_ManTranStochPut( pGia );
287 pNtkRes = Abc_NtkCollapse( pNtk, ABC_INFINITY, 0, 1, 0, 0, 0 );
288 Abc_NtkDelete( pNtk );
289 pNtk = pNtkRes;
290 pNtkRes = Abc_NtkStrash( pNtk, 0, 1, 0 );
291 Abc_NtkDelete( pNtk );
292 pNtk = pNtkRes;
293 pNew = Gia_ManTranStochGet( pNtk );
294 Abc_NtkDelete( pNtk );
295 Vec_PtrPush( vpStarts, pNew );
296 }
297 { // &ttopt;
298 pNew = Gia_ManTtopt( pGia, Gia_ManCiNum( pGia ), Gia_ManCoNum( pGia ), 100 );
299 Vec_PtrPush( vpStarts, pNew );
300 }
301 { // &put; collapse; sop; fx;
302 pNtk = Gia_ManTranStochPut( pGia );
303 pNtkRes = Abc_NtkCollapse( pNtk, ABC_INFINITY, 0, 1, 0, 0, 0 );
304 Abc_NtkDelete( pNtk );
305 pNtk = pNtkRes;
306 Abc_NtkToSop( pNtk, -1, ABC_INFINITY );
307 Gia_ManTranStochFx( pNtk );
308 pNtkRes = Abc_NtkStrash( pNtk, 0, 1, 0 );
309 Abc_NtkDelete( pNtk );
310 pNtk = pNtkRes;
311 pNew = Gia_ManTranStochGet( pNtk );
312 Abc_NtkDelete( pNtk );
313 Vec_PtrPush( vpStarts, pNew );
314 }
315 }
316 if ( fSingle ) {
317 pBest = (Gia_Man_t *)Vec_PtrEntry( vpStarts, 0 );
318 for ( i = 1; i < Vec_PtrSize( vpStarts ); i++ ) {
319 pStart = (Gia_Man_t *)Vec_PtrEntry( vpStarts, i );
320 if ( Gia_ManAndNum( pStart ) < Gia_ManAndNum( pBest ) ) {
321 Gia_ManStop( pBest );
322 pBest = pStart;
323 j = i;
324 } else {
326 }
327 }
328 Vec_PtrClear( vpStarts );
329 Vec_PtrPush( vpStarts, pBest );
330 }
331 // optimize
332 pBest = Gia_ManDup( pGia );
333 if ( nThreads == 1 ) {
334 Vec_PtrForEachEntry( Gia_Man_t *, vpStarts, pStart, i ) {
335 if ( p->nVerbose )
336 printf( "*begin starting point %d: #nodes = %5d\n", i + j, Gia_ManAndNum( pStart ) );
337 p->pStart = pStart;
338 pNew = Gia_ManTranStochOpt3( p );
339 if ( p->nVerbose )
340 printf( "*end starting point %d: #nodes = %5d\n", i + j, Gia_ManAndNum( pNew ) );
341 if ( Gia_ManAndNum( pBest ) > Gia_ManAndNum( pNew ) ) {
342 Gia_ManStop( pBest );
343 pBest = pNew;
344 } else {
345 Gia_ManStop( pNew );
346 }
348 }
349 } else {
350#ifdef ABC_USE_PTHREADS
351 static pthread_mutex_t mutex;
352 int k, status, nIte, fAssigned, fWorking;
353 Gia_ManTranStochParam ThData[100];
354 pthread_t WorkerThread[100];
355 p->pRes = NULL;
356 p->mutex = &mutex;
357 if ( p->nVerbose )
358 p->nVerbose--;
359 for ( i = 0; i < nThreads; i++ ) {
360 ThData[i] = *p;
361 status = pthread_create( WorkerThread + i, NULL, Gia_ManTranStochWorkerThread, (void *)(ThData + i) );
362 assert( status == 0 );
363 }
364 Vec_PtrForEachEntry( Gia_Man_t *, vpStarts, pStart, k ) {
365 for ( nIte = 0; nIte <= p->nRestarts; nIte++ ) {
366 fAssigned = 0;
367 while ( !fAssigned ) {
368 for ( i = 0; i < nThreads; i++ ) {
369 if ( ThData[i].fWorking )
370 continue;
371 if ( ThData[i].pRes != NULL ) {
372 if( nVerbose )
373 printf( "*sp %d res %4d : #nodes = %5d\n", ThData[i].nSp, ThData[i].nIte, Gia_ManAndNum( ThData[i].pRes ) );
374 if ( Gia_ManAndNum( pBest ) > Gia_ManAndNum( ThData[i].pRes ) ) {
375 Gia_ManStop( pBest );
376 pBest = ThData[i].pRes;
377 } else {
378 Gia_ManStop( ThData[i].pRes );
379 }
380 ThData[i].pRes = NULL;
381 }
382 ThData[i].nSp = j + k;
383 ThData[i].nIte = nIte;
384 ThData[i].pStart = pStart;
385 ThData[i].fWorking = 1;
386 fAssigned = 1;
387 break;
388 }
389 }
390 }
391 }
392 fWorking = 1;
393 while ( fWorking ) {
394 fWorking = 0;
395 for ( i = 0; i < nThreads; i++ ) {
396 if( ThData[i].fWorking ) {
397 fWorking = 1;
398 continue;
399 }
400 if ( ThData[i].pRes != NULL ) {
401 if( nVerbose )
402 printf( "*sp %d res %4d : #nodes = %5d\n", ThData[i].nSp, ThData[i].nIte, Gia_ManAndNum( ThData[i].pRes ) );
403 if ( Gia_ManAndNum( pBest ) > Gia_ManAndNum( ThData[i].pRes ) ) {
404 Gia_ManStop( pBest );
405 pBest = ThData[i].pRes;
406 } else {
407 Gia_ManStop( ThData[i].pRes );
408 }
409 ThData[i].pRes = NULL;
410 }
411 }
412 }
413 for ( i = 0; i < nThreads; i++ ) {
414 ThData[i].pStart = NULL;
415 ThData[i].fWorking = 1;
416 }
417#else
418 printf( "ERROR: pthread is off" );
419#endif
420 Vec_PtrForEachEntry( Gia_Man_t *, vpStarts, pStart, i )
422 }
423 if ( nVerbose )
424 printf( "best: %d\n", Gia_ManAndNum( pBest ) );
425 Vec_PtrFree( vpStarts );
426 ABC_FREE( pBest->pName );
427 ABC_FREE( pBest->pSpec );
428 pBest->pName = Abc_UtilStrsav( pGia->pName );
429 pBest->pSpec = Abc_UtilStrsav( pGia->pSpec );
430 return pBest;
431}
432
void Abc_NtkFxuFreeInfo(Fxu_Data_t *p)
Definition abcFxu.c:207
void Abc_NtkSetDefaultFxParams(Fxu_Data_t *p)
FUNCTION DEFINITIONS ///.
Definition abcFxu.c:52
ABC_DLL Abc_Ntk_t * Abc_NtkCollapse(Abc_Ntk_t *pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fDumpOrder, int fVerbose)
DECLARATIONS ///.
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
ABC_DLL int Abc_NtkToSop(Abc_Ntk_t *pNtk, int fMode, int nCubeLimit)
Definition abcFunc.c:1261
ABC_DLL Abc_Ntk_t * Abc_NtkStrash(Abc_Ntk_t *pNtk, int fAllNodes, int fCleanup, int fRecord)
Definition abcStrash.c:265
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition abcNtk.c:1421
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Aig_Man_t * Aig_ManDupDfs(Aig_Man_t *p)
Definition aigDup.c:563
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
ABC_DLL void * Abc_FrameReadLibLut()
Definition mainFrame.c:57
int Dar_ManRefactor(Aig_Man_t *pAig, Dar_RefPar_t *pPars)
Definition darRefact.c:496
struct Dar_RefPar_t_ Dar_RefPar_t
Definition dar.h:43
void Dar_ManDefaultRefParams(Dar_RefPar_t *pPars)
FUNCTION DEFINITIONS ///.
Definition darRefact.c:85
Cube * p
Definition exorList.c:222
typedefABC_NAMESPACE_HEADER_START struct FxuDataStruct Fxu_Data_t
INCLUDES ///.
Definition fxu.h:42
Gia_Man_t * Gia_ManCompress2(Gia_Man_t *p, int fUpdateLevel, int fVerbose)
Definition giaAig.c:592
Gia_Man_t * Gia_ManFromAig(Aig_Man_t *p)
INCLUDES ///.
Definition giaAig.c:76
Aig_Man_t * Gia_ManToAig(Gia_Man_t *p, int fChoices)
Definition giaAig.c:318
void Gia_ManTranStochMfs2(Abc_Ntk_t *pNtk)
int Abc_NtkPerformMfs(Abc_Ntk_t *pNtk, Sfm_Par_t *pPars)
Definition abcMfs.c:357
void Gia_ManTranStochLock(Gia_ManTranStochParam *p)
Gia_Man_t * Gia_ManTranStochOpt3(Gia_ManTranStochParam *p)
ABC_NAMESPACE_IMPL_START Abc_Ntk_t * Abc_NtkFromAigPhase(Aig_Man_t *pMan)
DECLARATIONS ///.
Definition abcDar.c:595
Gia_Man_t * Gia_ManTranStochOpt2(Gia_ManTranStochParam *p)
Abc_Ntk_t * Gia_ManTranStochIf(Abc_Ntk_t *pNtk)
Abc_Ntk_t * Gia_ManTranStochPut(Gia_Man_t *pGia)
void Gia_ManTranStochUnlock(Gia_ManTranStochParam *p)
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
Definition abcDar.c:237
Gia_Man_t * Gia_ManTranStoch(Gia_Man_t *pGia, int nRestarts, int nHops, int nSeedBase, int fMspf, int fMerge, int fResetHop, int fZeroCostHop, int fRefactor, int fTruth, int fSingle, int fOriginalOnly, int fNewLine, Gia_Man_t *pExdc, int nThreads, int nVerbose)
Gia_Man_t * Gia_ManTranStochOpt1(Gia_ManTranStochParam *p, Gia_Man_t *pOld)
Gia_Man_t * Gia_ManTranStochGet(Abc_Ntk_t *pNtk)
void Gia_ManTranStochFx(Abc_Ntk_t *pNtk)
Gia_Man_t * Gia_ManTranStochRefactor(Gia_Man_t *pGia)
int Abc_NtkFxPerform(Abc_Ntk_t *pNtk, int nNewNodesMax, int nLitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose)
Definition abcFx.c:309
Abc_Ntk_t * Abc_NtkIf(Abc_Ntk_t *pNtk, If_Par_t *pPars)
Definition abcIf.c:107
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition giaDup.c:720
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_Man_t * Gia_ManTransductionTt(Gia_Man_t *pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t *pExdc, int fNewLine, int nVerbose)
Gia_Man_t * Gia_ManTransductionBdd(Gia_Man_t *pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t *pExdc, int fNewLine, int nVerbose)
Gia_Man_t * Gia_ManTtopt(Gia_Man_t *p, int nIns, int nOuts, int nRounds)
struct If_Par_t_ If_Par_t
Definition if.h:78
struct If_LibLut_t_ If_LibLut_t
Definition if.h:82
void If_ManSetDefaultPars(If_Par_t *pPars)
FUNCTION DECLARATIONS ///.
Definition ifCore.c:47
struct Sfm_Par_t_ Sfm_Par_t
Definition sfm.h:42
void Sfm_ParSetDefault(Sfm_Par_t *pPars)
MACRO DEFINITIONS ///.
Definition sfmCore.c:46
pthread_mutex_t mutex
Definition starter.c:44
int fUseZeros
Definition dar.h:66
char * pSpec
Definition gia.h:100
char * pName
Definition gia.h:99
int LutMax
Definition if.h:190
int nLutSize
Definition if.h:104
If_LibLut_t * pLutLib
Definition if.h:175
#define assert(ex)
Definition util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55