1 /**CFile****************************************************************
2
3 FileName [mainFrame.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [The main package.]
8
9 Synopsis [The global framework resides in this file.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: mainFrame.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "base/abc/abc.h"
22 #include "mainInt.h"
23 #include "bool/dec/dec.h"
24 #include "map/if/if.h"
25 #include "aig/miniaig/ndr.h"
26
27 #ifdef ABC_USE_CUDD
28 #include "bdd/extrab/extraBdd.h"
29 #endif
30
31 ABC_NAMESPACE_IMPL_START
32
33
34 ////////////////////////////////////////////////////////////////////////
35 /// DECLARATIONS ///
36 ////////////////////////////////////////////////////////////////////////
37
38 static Abc_Frame_t * s_GlobalFrame = NULL;
39
40 ////////////////////////////////////////////////////////////////////////
41 /// FUNCTION DEFINITIONS ///
42 ////////////////////////////////////////////////////////////////////////
43
44 /**Function*************************************************************
45
46 Synopsis [APIs to access parameters in the flobal frame.]
47
48 Description []
49
50 SideEffects []
51
52 SeeAlso []
53
54 ***********************************************************************/
Abc_FrameReadStore()55 Vec_Ptr_t * Abc_FrameReadStore() { return s_GlobalFrame->vStore; }
Abc_FrameReadStoreSize()56 int Abc_FrameReadStoreSize() { return Vec_PtrSize(s_GlobalFrame->vStore); }
Abc_FrameReadLibLut()57 void * Abc_FrameReadLibLut() { return s_GlobalFrame->pLibLut; }
Abc_FrameReadLibBox()58 void * Abc_FrameReadLibBox() { return s_GlobalFrame->pLibBox; }
Abc_FrameReadLibGen()59 void * Abc_FrameReadLibGen() { return s_GlobalFrame->pLibGen; }
Abc_FrameReadLibGen2()60 void * Abc_FrameReadLibGen2() { return s_GlobalFrame->pLibGen2; }
Abc_FrameReadLibSuper()61 void * Abc_FrameReadLibSuper() { return s_GlobalFrame->pLibSuper; }
Abc_FrameReadLibScl()62 void * Abc_FrameReadLibScl() { return s_GlobalFrame->pLibScl; }
63 #ifdef ABC_USE_CUDD
Abc_FrameReadManDd()64 void * Abc_FrameReadManDd() { if ( s_GlobalFrame->dd == NULL ) s_GlobalFrame->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); return s_GlobalFrame->dd; }
65 #endif
Abc_FrameReadManDec()66 void * Abc_FrameReadManDec() { if ( s_GlobalFrame->pManDec == NULL ) s_GlobalFrame->pManDec = Dec_ManStart(); return s_GlobalFrame->pManDec; }
Abc_FrameReadManDsd()67 void * Abc_FrameReadManDsd() { return s_GlobalFrame->pManDsd; }
Abc_FrameReadManDsd2()68 void * Abc_FrameReadManDsd2() { return s_GlobalFrame->pManDsd2; }
Abc_FrameReadFlag(char * pFlag)69 char * Abc_FrameReadFlag( char * pFlag ) { return Cmd_FlagReadByName( s_GlobalFrame, pFlag ); }
70
Abc_FrameReadBmcFrames(Abc_Frame_t * p)71 int Abc_FrameReadBmcFrames( Abc_Frame_t * p ) { return s_GlobalFrame->nFrames; }
Abc_FrameReadProbStatus(Abc_Frame_t * p)72 int Abc_FrameReadProbStatus( Abc_Frame_t * p ) { return s_GlobalFrame->Status; }
Abc_FrameReadCex(Abc_Frame_t * p)73 void * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; }
Abc_FrameReadCexVec(Abc_Frame_t * p)74 Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ) { return s_GlobalFrame->vCexVec; }
Abc_FrameReadStatusVec(Abc_Frame_t * p)75 Vec_Int_t * Abc_FrameReadStatusVec( Abc_Frame_t * p ) { return s_GlobalFrame->vStatuses; }
Abc_FrameReadPoEquivs(Abc_Frame_t * p)76 Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ) { return s_GlobalFrame->vPoEquivs; }
Abc_FrameReadPoStatuses(Abc_Frame_t * p)77 Vec_Int_t * Abc_FrameReadPoStatuses( Abc_Frame_t * p ) { return s_GlobalFrame->vStatuses; }
Abc_FrameReadObjIds(Abc_Frame_t * p)78 Vec_Int_t * Abc_FrameReadObjIds( Abc_Frame_t * p ) { return s_GlobalFrame->vAbcObjIds; }
Abc_FrameReadJsonStrs(Abc_Frame_t * p)79 Abc_Nam_t * Abc_FrameReadJsonStrs( Abc_Frame_t * p ) { return s_GlobalFrame->pJsonStrs; }
Abc_FrameReadJsonObjs(Abc_Frame_t * p)80 Vec_Wec_t * Abc_FrameReadJsonObjs( Abc_Frame_t * p ) { return s_GlobalFrame->vJsonObjs; }
81
Abc_FrameReadCexPiNum(Abc_Frame_t * p)82 int Abc_FrameReadCexPiNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nPis; }
Abc_FrameReadCexRegNum(Abc_Frame_t * p)83 int Abc_FrameReadCexRegNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nRegs; }
Abc_FrameReadCexPo(Abc_Frame_t * p)84 int Abc_FrameReadCexPo( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->iPo; }
Abc_FrameReadCexFrame(Abc_Frame_t * p)85 int Abc_FrameReadCexFrame( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->iFrame; }
86
Abc_FrameInputNdr(Abc_Frame_t * pAbc,void * pData)87 void Abc_FrameInputNdr( Abc_Frame_t * pAbc, void * pData ) { Ndr_Delete(s_GlobalFrame->pNdr); s_GlobalFrame->pNdr = pData; }
Abc_FrameOutputNdr(Abc_Frame_t * pAbc)88 void * Abc_FrameOutputNdr( Abc_Frame_t * pAbc ) { void * pData = s_GlobalFrame->pNdr; s_GlobalFrame->pNdr = NULL; return pData; }
Abc_FrameOutputNdrArray(Abc_Frame_t * pAbc)89 int * Abc_FrameOutputNdrArray( Abc_Frame_t * pAbc ) { int * pArray = s_GlobalFrame->pNdrArray; s_GlobalFrame->pNdrArray = NULL; return pArray; }
90
Abc_FrameSetLibLut(void * pLib)91 void Abc_FrameSetLibLut( void * pLib ) { s_GlobalFrame->pLibLut = pLib; }
Abc_FrameSetLibBox(void * pLib)92 void Abc_FrameSetLibBox( void * pLib ) { s_GlobalFrame->pLibBox = pLib; }
Abc_FrameSetLibGen(void * pLib)93 void Abc_FrameSetLibGen( void * pLib ) { s_GlobalFrame->pLibGen = pLib; }
Abc_FrameSetLibGen2(void * pLib)94 void Abc_FrameSetLibGen2( void * pLib ) { s_GlobalFrame->pLibGen2 = pLib; }
Abc_FrameSetLibSuper(void * pLib)95 void Abc_FrameSetLibSuper( void * pLib ) { s_GlobalFrame->pLibSuper = pLib; }
Abc_FrameSetFlag(char * pFlag,char * pValue)96 void Abc_FrameSetFlag( char * pFlag, char * pValue ) { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue ); }
Abc_FrameSetCex(Abc_Cex_t * pCex)97 void Abc_FrameSetCex( Abc_Cex_t * pCex ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->pCex = pCex; }
Abc_FrameSetNFrames(int nFrames)98 void Abc_FrameSetNFrames( int nFrames ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->nFrames = nFrames; }
Abc_FrameSetStatus(int Status)99 void Abc_FrameSetStatus( int Status ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->Status = Status; }
Abc_FrameSetManDsd(void * pMan)100 void Abc_FrameSetManDsd( void * pMan ) { if (s_GlobalFrame->pManDsd && s_GlobalFrame->pManDsd != pMan) If_DsdManFree((If_DsdMan_t *)s_GlobalFrame->pManDsd, 0); s_GlobalFrame->pManDsd = pMan; }
Abc_FrameSetManDsd2(void * pMan)101 void Abc_FrameSetManDsd2( void * pMan ) { if (s_GlobalFrame->pManDsd2 && s_GlobalFrame->pManDsd2 != pMan) If_DsdManFree((If_DsdMan_t *)s_GlobalFrame->pManDsd2, 0); s_GlobalFrame->pManDsd2 = pMan; }
Abc_FrameSetInv(Vec_Int_t * vInv)102 void Abc_FrameSetInv( Vec_Int_t * vInv ) { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcInv); s_GlobalFrame->pAbcWlcInv = vInv; }
Abc_FrameSetJsonStrs(Abc_Nam_t * pStrs)103 void Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs ) { Abc_NamDeref( s_GlobalFrame->pJsonStrs ); s_GlobalFrame->pJsonStrs = pStrs; }
Abc_FrameSetJsonObjs(Vec_Wec_t * vObjs)104 void Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs ) { Vec_WecFreeP(&s_GlobalFrame->vJsonObjs ); s_GlobalFrame->vJsonObjs = vObjs; }
105
Abc_FrameIsBatchMode()106 int Abc_FrameIsBatchMode() { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0; }
107
Abc_FrameIsBridgeMode()108 int Abc_FrameIsBridgeMode() { return s_GlobalFrame ? s_GlobalFrame->fBridgeMode : 0; }
Abc_FrameSetBridgeMode()109 void Abc_FrameSetBridgeMode() { if ( s_GlobalFrame ) s_GlobalFrame->fBridgeMode = 1; }
110
Abc_FrameReadDrivingCell()111 char * Abc_FrameReadDrivingCell() { return s_GlobalFrame->pDrivingCell; }
Abc_FrameReadMaxLoad()112 float Abc_FrameReadMaxLoad() { return s_GlobalFrame->MaxLoad; }
Abc_FrameSetDrivingCell(char * pName)113 void Abc_FrameSetDrivingCell( char * pName ) { ABC_FREE(s_GlobalFrame->pDrivingCell); s_GlobalFrame->pDrivingCell = pName; }
Abc_FrameSetMaxLoad(float Load)114 void Abc_FrameSetMaxLoad( float Load ) { s_GlobalFrame->MaxLoad = Load; }
115
Abc_FrameReadArrayMapping(Abc_Frame_t * pAbc)116 int * Abc_FrameReadArrayMapping( Abc_Frame_t * pAbc ) { return pAbc->pArray; }
Abc_FrameSetArrayMapping(int * p)117 void Abc_FrameSetArrayMapping( int * p ) { ABC_FREE( s_GlobalFrame->pArray ); s_GlobalFrame->pArray = p; }
118
Abc_FrameReadBoxes(Abc_Frame_t * pAbc)119 int * Abc_FrameReadBoxes( Abc_Frame_t * pAbc ) { return pAbc->pBoxes; }
Abc_FrameSetBoxes(int * p)120 void Abc_FrameSetBoxes( int * p ) { ABC_FREE( s_GlobalFrame->pBoxes ); s_GlobalFrame->pBoxes = p; }
121
122 /**Function*************************************************************
123
124 Synopsis [Returns 1 if the flag is enabled without value or with value 1.]
125
126 Description []
127
128 SideEffects []
129
130 SeeAlso []
131
132 ***********************************************************************/
Abc_FrameIsFlagEnabled(char * pFlag)133 int Abc_FrameIsFlagEnabled( char * pFlag )
134 {
135 char * pValue;
136 // if flag is not defined, it is not enabled
137 pValue = Abc_FrameReadFlag( pFlag );
138 if ( pValue == NULL )
139 return 0;
140 // if flag is defined but value is not empty (no parameter) or "1", it is not enabled
141 if ( strcmp(pValue, "") && strcmp(pValue, "1") )
142 return 0;
143 return 1;
144 }
145
146 /**Function*************************************************************
147
148 Synopsis []
149
150 Description []
151
152 SideEffects []
153
154 SeeAlso []
155
156 ***********************************************************************/
Abc_FrameAllocate()157 Abc_Frame_t * Abc_FrameAllocate()
158 {
159 Abc_Frame_t * p;
160 extern void define_cube_size( int n );
161 extern void set_espresso_flags();
162 // allocate and clean
163 p = ABC_CALLOC( Abc_Frame_t, 1 );
164 // get version
165 p->sVersion = Abc_UtilsGetVersion( p );
166 // set streams
167 p->Err = stderr;
168 p->Out = stdout;
169 p->Hst = NULL;
170 p->Status = -1;
171 p->nFrames = -1;
172 // set the starting step
173 p->nSteps = 1;
174 p->fBatchMode = 0;
175 // networks to be used by choice
176 p->vStore = Vec_PtrAlloc( 16 );
177 p->vAbcObjIds = Vec_IntAlloc( 0 );
178 // initialize decomposition manager
179 // define_cube_size(20);
180 // set_espresso_flags();
181 // initialize the trace manager
182 // Abc_HManStart();
183 p->vPlugInComBinPairs = Vec_PtrAlloc( 100 );
184 return p;
185 }
186
187
188 /**Function*************************************************************
189
190 Synopsis []
191
192 Description []
193
194 SideEffects []
195
196 SeeAlso []
197
198 ***********************************************************************/
Abc_FrameDeallocate(Abc_Frame_t * p)199 void Abc_FrameDeallocate( Abc_Frame_t * p )
200 {
201 extern void Rwt_ManGlobalStop();
202 extern void undefine_cube_size();
203 // extern void Ivy_TruthManStop();
204 // Abc_HManStop();
205 // undefine_cube_size();
206 Rwt_ManGlobalStop();
207 // Ivy_TruthManStop();
208 if ( p->vAbcObjIds) Vec_IntFree( p->vAbcObjIds );
209 if ( p->vCexVec ) Vec_PtrFreeFree( p->vCexVec );
210 if ( p->vPoEquivs ) Vec_VecFree( (Vec_Vec_t *)p->vPoEquivs );
211 if ( p->vStatuses ) Vec_IntFree( p->vStatuses );
212 if ( p->pManDec ) Dec_ManStop( (Dec_Man_t *)p->pManDec );
213 #ifdef ABC_USE_CUDD
214 if ( p->dd ) Extra_StopManager( p->dd );
215 #endif
216 if ( p->vStore ) Vec_PtrFree( p->vStore );
217 if ( p->pSave1 ) Aig_ManStop( (Aig_Man_t *)p->pSave1 );
218 if ( p->pSave2 ) Aig_ManStop( (Aig_Man_t *)p->pSave2 );
219 if ( p->pSave3 ) Aig_ManStop( (Aig_Man_t *)p->pSave3 );
220 if ( p->pSave4 ) Aig_ManStop( (Aig_Man_t *)p->pSave4 );
221 if ( p->pManDsd ) If_DsdManFree( (If_DsdMan_t *)p->pManDsd, 0 );
222 if ( p->pManDsd2 ) If_DsdManFree( (If_DsdMan_t *)p->pManDsd2, 0 );
223 if ( p->pNtkBackup) Abc_NtkDelete( p->pNtkBackup );
224 if ( p->vPlugInComBinPairs )
225 {
226 char * pTemp;
227 int i;
228 Vec_PtrForEachEntry( char *, p->vPlugInComBinPairs, pTemp, i )
229 ABC_FREE( pTemp );
230 Vec_PtrFree( p->vPlugInComBinPairs );
231 }
232 Vec_IntFreeP( &p->vIndFlops );
233 Vec_PtrFreeP( &p->vLTLProperties_global );
234 Abc_FrameDeleteAllNetworks( p );
235 ABC_FREE( p->pDrivingCell );
236 ABC_FREE( p->pCex2 );
237 ABC_FREE( p->pCex );
238 Vec_IntFreeP( &p->pAbcWlcInv );
239 Abc_NamDeref( s_GlobalFrame->pJsonStrs );
240 Vec_WecFreeP( &s_GlobalFrame->vJsonObjs );
241 Ndr_Delete( s_GlobalFrame->pNdr );
242 ABC_FREE( s_GlobalFrame->pNdrArray );
243
244 Gia_ManStopP( &p->pGiaMiniAig );
245 Gia_ManStopP( &p->pGiaMiniLut );
246 Vec_IntFreeP( &p->vCopyMiniAig );
247 Vec_IntFreeP( &p->vCopyMiniLut );
248 ABC_FREE( p->pArray );
249 ABC_FREE( p->pBoxes );
250
251
252 ABC_FREE( p );
253 s_GlobalFrame = NULL;
254 }
255
256
257 /**Function*************************************************************
258
259 Synopsis []
260
261 Description []
262
263 SideEffects []
264
265 SeeAlso []
266
267 ***********************************************************************/
Abc_FrameRestart(Abc_Frame_t * p)268 void Abc_FrameRestart( Abc_Frame_t * p )
269 {
270 }
271
272 /**Function*************************************************************
273
274 Synopsis []
275
276 Description []
277
278 SideEffects []
279
280 SeeAlso []
281
282 ***********************************************************************/
Abc_FrameClearVerifStatus(Abc_Frame_t * p)283 void Abc_FrameClearVerifStatus( Abc_Frame_t * p )
284 {
285 p->nFrames = -1;
286 p->Status = -1;
287 ABC_FREE( p->pCex );
288 }
289
290 /**Function*************************************************************
291
292 Synopsis []
293
294 Description []
295
296 SideEffects []
297
298 SeeAlso []
299
300 ***********************************************************************/
Abc_FrameShowProgress(Abc_Frame_t * p)301 int Abc_FrameShowProgress( Abc_Frame_t * p )
302 {
303 return Abc_FrameIsFlagEnabled( "progressbar" );
304 }
305
306
307 /**Function*************************************************************
308
309 Synopsis []
310
311 Description []
312
313 SideEffects []
314
315 SeeAlso []
316
317 ***********************************************************************/
Abc_FrameReadNtk(Abc_Frame_t * p)318 Abc_Ntk_t * Abc_FrameReadNtk( Abc_Frame_t * p )
319 {
320 return p->pNtkCur;
321 }
322
323 /**Function*************************************************************
324
325 Synopsis []
326
327 Description []
328
329 SideEffects []
330
331 SeeAlso []
332
333 ***********************************************************************/
Abc_FrameReadGia(Abc_Frame_t * p)334 Gia_Man_t * Abc_FrameReadGia( Abc_Frame_t * p )
335 {
336 return p->pGia;
337 }
338
339 /**Function*************************************************************
340
341 Synopsis []
342
343 Description []
344
345 SideEffects []
346
347 SeeAlso []
348
349 ***********************************************************************/
Abc_FrameReadOut(Abc_Frame_t * p)350 FILE * Abc_FrameReadOut( Abc_Frame_t * p )
351 {
352 return p->Out;
353 }
354
355 /**Function*************************************************************
356
357 Synopsis []
358
359 Description []
360
361 SideEffects []
362
363 SeeAlso []
364
365 ***********************************************************************/
Abc_FrameReadErr(Abc_Frame_t * p)366 FILE * Abc_FrameReadErr( Abc_Frame_t * p )
367 {
368 return p->Err;
369 }
370
371 /**Function*************************************************************
372
373 Synopsis []
374
375 Description []
376
377 SideEffects []
378
379 SeeAlso []
380
381 ***********************************************************************/
Abc_FrameReadMode(Abc_Frame_t * p)382 int Abc_FrameReadMode( Abc_Frame_t * p )
383 {
384 int fShortNames;
385 char * pValue;
386 pValue = Cmd_FlagReadByName( p, "namemode" );
387 if ( pValue == NULL )
388 fShortNames = 0;
389 else
390 fShortNames = atoi(pValue);
391 return fShortNames;
392 }
393
394 /**Function*************************************************************
395
396 Synopsis []
397
398 Description []
399
400 SideEffects []
401
402 SeeAlso []
403
404 ***********************************************************************/
Abc_FrameSetMode(Abc_Frame_t * p,int fNameMode)405 int Abc_FrameSetMode( Abc_Frame_t * p, int fNameMode )
406 {
407 char Buffer[2];
408 int fNameModeOld;
409 fNameModeOld = Abc_FrameReadMode( p );
410 Buffer[0] = '0' + fNameMode;
411 Buffer[1] = 0;
412 Cmd_FlagUpdateValue( p, "namemode", (char *)Buffer );
413 return fNameModeOld;
414 }
415
416
417 /**Function*************************************************************
418
419 Synopsis [Sets the given network to be the current one.]
420
421 Description [Takes the network and makes it the current network.
422 The previous current network is attached to the given network as
423 a backup copy. In the stack of backup networks contains too many
424 networks (defined by the paramater "savesteps"), the bottom
425 most network is deleted.]
426
427 SideEffects []
428
429 SeeAlso []
430
431 ***********************************************************************/
Abc_FrameSetCurrentNetwork(Abc_Frame_t * p,Abc_Ntk_t * pNtkNew)432 void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtkNew )
433 {
434 Abc_Ntk_t * pNtk, * pNtk2, * pNtk3;
435 int nNetsPresent;
436 int nNetsToSave;
437 char * pValue;
438
439 if ( p->pNtkCur == pNtkNew )
440 return;
441
442 // link it to the previous network
443 Abc_NtkSetBackup( pNtkNew, p->pNtkCur );
444 // set the step of this network
445 Abc_NtkSetStep( pNtkNew, ++p->nSteps );
446 // set this network to be the current network
447 p->pNtkCur = pNtkNew;
448
449 // remove any extra network that may happen to be in the stack
450 pValue = Cmd_FlagReadByName( p, "savesteps" );
451 // if the value of steps to save is not set, assume 1-level undo
452 if ( pValue == NULL )
453 nNetsToSave = 1;
454 else
455 nNetsToSave = atoi(pValue);
456
457 // count the network, remember the last one, and the one before the last one
458 nNetsPresent = 0;
459 pNtk2 = pNtk3 = NULL;
460 for ( pNtk = p->pNtkCur; pNtk; pNtk = Abc_NtkBackup(pNtk2) )
461 {
462 nNetsPresent++;
463 pNtk3 = pNtk2;
464 pNtk2 = pNtk;
465 }
466
467 // remove the earliest backup network if it is more steps away than we store
468 if ( nNetsPresent - 1 > nNetsToSave )
469 { // delete the last network
470 Abc_NtkDelete( pNtk2 );
471 // clean the pointer of the network before the last one
472 Abc_NtkSetBackup( pNtk3, NULL );
473 }
474 }
475
476 /**Function*************************************************************
477
478 Synopsis [This procedure swaps the current and the backup network.]
479
480 Description []
481
482 SideEffects []
483
484 SeeAlso []
485
486 ***********************************************************************/
Abc_FrameSwapCurrentAndBackup(Abc_Frame_t * p)487 void Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p )
488 {
489 Abc_Ntk_t * pNtkCur, * pNtkBack, * pNtkBack2;
490 int iStepCur, iStepBack;
491
492 pNtkCur = p->pNtkCur;
493 pNtkBack = Abc_NtkBackup( pNtkCur );
494 iStepCur = Abc_NtkStep ( pNtkCur );
495
496 // if there is no backup nothing to reset
497 if ( pNtkBack == NULL )
498 return;
499
500 // remember the backup of the backup
501 pNtkBack2 = Abc_NtkBackup( pNtkBack );
502 iStepBack = Abc_NtkStep ( pNtkBack );
503
504 // set pNtkCur to be the next after the backup's backup
505 Abc_NtkSetBackup( pNtkCur, pNtkBack2 );
506 Abc_NtkSetStep ( pNtkCur, iStepBack );
507
508 // set pNtkCur to be the next after the backup
509 Abc_NtkSetBackup( pNtkBack, pNtkCur );
510 Abc_NtkSetStep ( pNtkBack, iStepCur );
511
512 // set the current network
513 p->pNtkCur = pNtkBack;
514 }
515
516
517 /**Function*************************************************************
518
519 Synopsis [Replaces the current network by the given one.]
520
521 Description [This procedure does not modify the stack of saved
522 networks.]
523
524 SideEffects []
525
526 SeeAlso []
527
528 ***********************************************************************/
Abc_FrameReplaceCurrentNetwork(Abc_Frame_t * p,Abc_Ntk_t * pNtk)529 void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtk )
530 {
531 if ( pNtk == NULL )
532 return;
533
534 if ( Abc_NtkPoNum(pNtk) == 0 )
535 Abc_Print( 0, "The current network has no primary outputs. Some commands may not work correctly.\n" );
536
537 // transfer the parameters to the new network
538 if ( p->pNtkCur && Abc_FrameIsFlagEnabled( "backup" ) )
539 {
540 Abc_NtkSetBackup( pNtk, Abc_NtkBackup(p->pNtkCur) );
541 Abc_NtkSetStep( pNtk, Abc_NtkStep(p->pNtkCur) );
542 // delete the current network
543 Abc_NtkDelete( p->pNtkCur );
544 }
545 else
546 {
547 Abc_NtkSetBackup( pNtk, NULL );
548 Abc_NtkSetStep( pNtk, ++p->nSteps );
549 // delete the current network if present but backup is disabled
550 if ( p->pNtkCur )
551 Abc_NtkDelete( p->pNtkCur );
552 }
553 // set the new current network
554 p->pNtkCur = pNtk;
555 }
556
557 /**Function*************************************************************
558
559 Synopsis [Removes library binding of all currently stored networks.]
560
561 Description [This procedure is called when the library is freed.]
562
563 SideEffects []
564
565 SeeAlso []
566
567 ***********************************************************************/
Abc_FrameUnmapAllNetworks(Abc_Frame_t * p)568 void Abc_FrameUnmapAllNetworks( Abc_Frame_t * p )
569 {
570 Abc_Ntk_t * pNtk;
571 for ( pNtk = p->pNtkCur; pNtk; pNtk = Abc_NtkBackup(pNtk) )
572 if ( Abc_NtkHasMapping(pNtk) )
573 Abc_NtkMapToSop( pNtk );
574 }
575
576 /**Function*************************************************************
577
578 Synopsis []
579
580 Description []
581
582 SideEffects []
583
584 SeeAlso []
585
586 ***********************************************************************/
Abc_FrameDeleteAllNetworks(Abc_Frame_t * p)587 void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p )
588 {
589 Abc_Ntk_t * pNtk, * pNtk2;
590 // delete all the currently saved networks
591 for ( pNtk = p->pNtkCur,
592 pNtk2 = pNtk? Abc_NtkBackup(pNtk): NULL;
593 pNtk;
594 pNtk = pNtk2,
595 pNtk2 = pNtk? Abc_NtkBackup(pNtk): NULL )
596 Abc_NtkDelete( pNtk );
597 // set the current network empty
598 p->pNtkCur = NULL;
599 // fprintf( p->Out, "All networks have been deleted.\n" );
600 Gia_ManStopP( &p->pGia );
601 Gia_ManStopP( &p->pGia2 );
602 Gia_ManStopP( &p->pGiaBest );
603 Gia_ManStopP( &p->pGiaBest2 );
604 Gia_ManStopP( &p->pGiaSaved );
605 }
606
607 /**Function*************************************************************
608
609 Synopsis []
610
611 Description []
612
613 SideEffects []
614
615 SeeAlso []
616
617 ***********************************************************************/
Abc_FrameSetGlobalFrame(Abc_Frame_t * p)618 void Abc_FrameSetGlobalFrame( Abc_Frame_t * p )
619 {
620 s_GlobalFrame = p;
621 }
622
623 /**Function*************************************************************
624
625 Synopsis []
626
627 Description []
628
629 SideEffects []
630
631 SeeAlso []
632
633 ***********************************************************************/
Abc_FrameGetGlobalFrame()634 Abc_Frame_t * Abc_FrameGetGlobalFrame()
635 {
636 if ( s_GlobalFrame == 0 )
637 {
638 // start the framework
639 s_GlobalFrame = Abc_FrameAllocate();
640 // perform initializations
641 Abc_FrameInit( s_GlobalFrame );
642 }
643 return s_GlobalFrame;
644 }
645
646 /**Function*************************************************************
647
648 Synopsis []
649
650 Description []
651
652 SideEffects []
653
654 SeeAlso []
655
656 ***********************************************************************/
Abc_FrameReadGlobalFrame()657 Abc_Frame_t * Abc_FrameReadGlobalFrame()
658 {
659 return s_GlobalFrame;
660 }
661
662 /**Function*************************************************************
663
664 Synopsis []
665
666 Description []
667
668 SideEffects []
669
670 SeeAlso []
671
672 ***********************************************************************/
Abc_FrameSetSave1(void * pAig)673 void Abc_FrameSetSave1( void * pAig )
674 {
675 Abc_Frame_t * pFrame = Abc_FrameGetGlobalFrame();
676 if ( pFrame->pSave1 )
677 Aig_ManStop( (Aig_Man_t *)pFrame->pSave1 );
678 pFrame->pSave1 = pAig;
679 }
680
681 /**Function*************************************************************
682
683 Synopsis []
684
685 Description []
686
687 SideEffects []
688
689 SeeAlso []
690
691 ***********************************************************************/
Abc_FrameSetSave2(void * pAig)692 void Abc_FrameSetSave2( void * pAig )
693 {
694 Abc_Frame_t * pFrame = Abc_FrameGetGlobalFrame();
695 if ( pFrame->pSave2 )
696 Aig_ManStop( (Aig_Man_t *)pFrame->pSave2 );
697 pFrame->pSave2 = pAig;
698 }
699
700 /**Function*************************************************************
701
702 Synopsis []
703
704 Description []
705
706 SideEffects []
707
708 SeeAlso []
709
710 ***********************************************************************/
Abc_FrameReadSave1()711 void * Abc_FrameReadSave1() { void * pAig = Abc_FrameGetGlobalFrame()->pSave1; Abc_FrameGetGlobalFrame()->pSave1 = NULL; return pAig; }
Abc_FrameReadSave2()712 void * Abc_FrameReadSave2() { void * pAig = Abc_FrameGetGlobalFrame()->pSave2; Abc_FrameGetGlobalFrame()->pSave2 = NULL; return pAig; }
713
714 /**Function*************************************************************
715
716 Synopsis [Returns 0/1 if pNtkCur is an AIG and PO is 0/1; -1 otherwise.]
717
718 Description []
719
720 SideEffects []
721
722 SeeAlso []
723
724 ***********************************************************************/
Abc_FrameCheckPoConst(Abc_Frame_t * p,int iPoNum)725 int Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum )
726 {
727 Abc_Obj_t * pObj;
728 if ( p->pNtkCur == NULL )
729 return -1;
730 if ( !Abc_NtkIsStrash(p->pNtkCur) )
731 return -1;
732 if ( iPoNum < 0 || iPoNum >= Abc_NtkPoNum(p->pNtkCur) )
733 return -1;
734 pObj = Abc_NtkPo( p->pNtkCur, iPoNum );
735 if ( !Abc_AigNodeIsConst(Abc_ObjFanin0(pObj)) )
736 return -1;
737 return !Abc_ObjFaninC0(pObj);
738 }
Abc_FrameCheckPoConstTest(Abc_Frame_t * p)739 void Abc_FrameCheckPoConstTest( Abc_Frame_t * p )
740 {
741 Abc_Obj_t * pObj;
742 int i;
743 Abc_NtkForEachPo( p->pNtkCur, pObj, i )
744 printf( "%d = %d\n", i, Abc_FrameCheckPoConst(p, i) );
745 }
746
747
748 ////////////////////////////////////////////////////////////////////////
749 /// END OF FILE ///
750 ////////////////////////////////////////////////////////////////////////
751
752
753 ABC_NAMESPACE_IMPL_END
754
755