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