mainFrame.c 22 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
/**CFile****************************************************************

  FileName    [mainFrame.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [The main package.]

  Synopsis    [The global framework resides in this file.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: mainFrame.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

21
#include "base/abc/abc.h"
22
#include "mainInt.h"
23 24
#include "bool/dec/dec.h"
#include "misc/extra/extraBdd.h"
25
#include "map/if/if.h"
Alan Mishchenko committed
26

27 28 29 30

ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
31 32 33 34
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

Alan Mishchenko committed
35
static Abc_Frame_t * s_GlobalFrame = NULL;
Alan Mishchenko committed
36 37

////////////////////////////////////////////////////////////////////////
Alan Mishchenko committed
38
///                     FUNCTION DEFINITIONS                         ///
Alan Mishchenko committed
39 40 41 42
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

Alan Mishchenko committed
43 44 45 46 47 48 49 50 51
  Synopsis    [APIs to access parameters in the flobal frame.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
52 53 54
Vec_Ptr_t * Abc_FrameReadStore()                             { return s_GlobalFrame->vStore;       } 
int         Abc_FrameReadStoreSize()                         { return Vec_PtrSize(s_GlobalFrame->vStore); }
void *      Abc_FrameReadLibLut()                            { return s_GlobalFrame->pLibLut;      } 
Alan Mishchenko committed
55
void *      Abc_FrameReadLibBox()                            { return s_GlobalFrame->pLibBox;      } 
56 57 58
void *      Abc_FrameReadLibGen()                            { return s_GlobalFrame->pLibGen;      } 
void *      Abc_FrameReadLibGen2()                           { return s_GlobalFrame->pLibGen2;     } 
void *      Abc_FrameReadLibSuper()                          { return s_GlobalFrame->pLibSuper;    } 
59
void *      Abc_FrameReadLibScl()                            { return s_GlobalFrame->pLibScl;      } 
60 61
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;      } 
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 65 66 67
char *      Abc_FrameReadFlag( char * pFlag )                { return Cmd_FlagReadByName( s_GlobalFrame, pFlag );   } 

int         Abc_FrameReadBmcFrames( Abc_Frame_t * p )        { return s_GlobalFrame->nFrames;      }               
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 76 77 78
int         Abc_FrameReadCexPiNum( Abc_Frame_t * p )         { return s_GlobalFrame->pCex->nPis;   }               
int         Abc_FrameReadCexRegNum( Abc_Frame_t * p )        { return s_GlobalFrame->pCex->nRegs;  }               
int         Abc_FrameReadCexPo( Abc_Frame_t * p )            { return s_GlobalFrame->pCex->iPo;    }               
int         Abc_FrameReadCexFrame( Abc_Frame_t * p )         { return s_GlobalFrame->pCex->iFrame; }               
79 80

void        Abc_FrameSetLibLut( void * pLib )                { s_GlobalFrame->pLibLut   = pLib;    } 
Alan Mishchenko committed
81
void        Abc_FrameSetLibBox( void * pLib )                { s_GlobalFrame->pLibBox   = pLib;    } 
82 83 84
void        Abc_FrameSetLibGen( void * pLib )                { s_GlobalFrame->pLibGen   = pLib;    } 
void        Abc_FrameSetLibGen2( void * pLib )               { s_GlobalFrame->pLibGen2  = pLib;    } 
void        Abc_FrameSetLibSuper( void * pLib )              { s_GlobalFrame->pLibSuper = pLib;    } 
85 86 87
void        Abc_FrameSetFlag( char * pFlag, char * pValue )  { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue );               } 
void        Abc_FrameSetCex( Abc_Cex_t * pCex )              { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->pCex = pCex;       }
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 90
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;  }
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; }
Alan Mishchenko committed
91

92 93
int         Abc_FrameIsBatchMode()                           { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0;              } 

94 95
int         Abc_FrameIsBridgeMode()                          { return s_GlobalFrame ? s_GlobalFrame->fBridgeMode : 0;             } 
void        Abc_FrameSetBridgeMode()                         { if ( s_GlobalFrame ) s_GlobalFrame->fBridgeMode = 1;               } 
96

97 98 99 100 101
char *      Abc_FrameReadDrivingCell()                       { return s_GlobalFrame->pDrivingCell;    }              
float       Abc_FrameReadMaxLoad()                           { return s_GlobalFrame->MaxLoad;         }      
void        Abc_FrameSetDrivingCell( char * pName )          { ABC_FREE(s_GlobalFrame->pDrivingCell); s_GlobalFrame->pDrivingCell   = pName; }      
void        Abc_FrameSetMaxLoad( float Load )                { s_GlobalFrame->MaxLoad        = Load;  }      

Alan Mishchenko committed
102 103 104 105 106 107 108 109 110 111 112
/**Function*************************************************************

  Synopsis    [Returns 1 if the flag is enabled without value or with value 1.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
113
int Abc_FrameIsFlagEnabled( char * pFlag )
Alan Mishchenko committed
114 115 116 117 118 119 120 121 122 123 124 125 126 127
{
    char * pValue;
    // if flag is not defined, it is not enabled
    pValue = Abc_FrameReadFlag( pFlag );
    if ( pValue == NULL )
        return 0;
    // if flag is defined but value is not empty (no parameter) or "1", it is not enabled
    if ( strcmp(pValue, "") && strcmp(pValue, "1") )
        return 0;
    return 1;
}

/**Function*************************************************************

Alan Mishchenko committed
128 129 130 131 132 133 134 135 136 137 138 139
  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Frame_t * Abc_FrameAllocate()
{
    Abc_Frame_t * p;
Alan Mishchenko committed
140 141
    extern void define_cube_size( int n );
    extern void set_espresso_flags();
Alan Mishchenko committed
142
    // allocate and clean
143
    p = ABC_CALLOC( Abc_Frame_t, 1 );
Alan Mishchenko committed
144 145 146 147 148 149
    // get version
    p->sVersion = Abc_UtilsGetVersion( p );
    // set streams
    p->Err = stderr;
    p->Out = stdout;
    p->Hst = NULL;
150 151
    p->Status     = -1;
    p->nFrames    = -1;
Alan Mishchenko committed
152
    // set the starting step
153 154
    p->nSteps     =  1;
    p->fBatchMode =  0;
Alan Mishchenko committed
155 156
    // networks to be used by choice
    p->vStore = Vec_PtrAlloc( 16 );
157
    p->vAbcObjIds = Vec_IntAlloc( 0 );
Alan Mishchenko committed
158
    // initialize decomposition manager
Alan Mishchenko committed
159 160
//    define_cube_size(20);
//    set_espresso_flags();
Alan Mishchenko committed
161 162
    // initialize the trace manager
//    Abc_HManStart();
163
    p->vPlugInComBinPairs = Vec_PtrAlloc( 100 );
Alan Mishchenko committed
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
    return p;
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_FrameDeallocate( Abc_Frame_t * p )
{
Alan Mishchenko committed
181 182 183 184
    extern void Rwt_ManGlobalStop();
    extern void undefine_cube_size();
//    extern void Ivy_TruthManStop();
//    Abc_HManStop();
Alan Mishchenko committed
185
//    undefine_cube_size();
Alan Mishchenko committed
186 187
    Rwt_ManGlobalStop();
//    Ivy_TruthManStop();
188
    if ( p->vAbcObjIds)  Vec_IntFree( p->vAbcObjIds );
189 190
    if ( p->vCexVec   )  Vec_PtrFreeFree( p->vCexVec );
    if ( p->vPoEquivs )  Vec_VecFree( (Vec_Vec_t *)p->vPoEquivs );
191
    if ( p->vStatuses )  Vec_IntFree( p->vStatuses );
192 193 194 195 196 197 198
    if ( p->pManDec   )  Dec_ManStop( (Dec_Man_t *)p->pManDec );
    if ( p->dd        )  Extra_StopManager( p->dd );
    if ( p->vStore    )  Vec_PtrFree( p->vStore );
    if ( p->pSave1    )  Aig_ManStop( (Aig_Man_t *)p->pSave1 );
    if ( p->pSave2    )  Aig_ManStop( (Aig_Man_t *)p->pSave2 );
    if ( p->pSave3    )  Aig_ManStop( (Aig_Man_t *)p->pSave3 );
    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 202 203 204 205 206 207 208
    if ( p->vPlugInComBinPairs ) 
    {
        char * pTemp;
        int i;
        Vec_PtrForEachEntry( char *, p->vPlugInComBinPairs, pTemp, i )
            ABC_FREE( pTemp );
        Vec_PtrFree( p->vPlugInComBinPairs );
    }
209
    Vec_IntFreeP( &p->vIndFlops );
210
    Vec_PtrFreeP( &p->vLTLProperties_global );
Alan Mishchenko committed
211
    Abc_FrameDeleteAllNetworks( p );
212
    ABC_FREE( p->pDrivingCell );
213
    ABC_FREE( p->pCex2 );
214
    ABC_FREE( p->pCex );
Alan Mishchenko committed
215
    ABC_FREE( p );
Alan Mishchenko committed
216
    s_GlobalFrame = NULL;
Alan Mishchenko committed
217 218
}

Alan Mishchenko committed
219

Alan Mishchenko committed
220 221 222 223 224 225 226 227 228 229 230 231 232 233 234
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_FrameRestart( Abc_Frame_t * p )
{
}

Alan Mishchenko committed
235 236 237 238 239 240 241 242 243 244 245
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264
void Abc_FrameClearVerifStatus( Abc_Frame_t * p )
{
    p->nFrames = -1;
    p->Status  = -1;
    ABC_FREE( p->pCex );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_FrameShowProgress( Abc_Frame_t * p )
Alan Mishchenko committed
265 266 267 268
{
    return Abc_FrameIsFlagEnabled( "progressbar" );
}

Alan Mishchenko committed
269 270 271 272 273 274 275 276 277 278 279 280

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
281
Abc_Ntk_t * Abc_FrameReadNtk( Abc_Frame_t * p )
Alan Mishchenko committed
282 283 284 285 286 287 288 289 290 291 292 293 294 295 296
{
    return p->pNtkCur;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
Gia_Man_t * Abc_FrameReadGia( Abc_Frame_t * p )
{
    return p->pGia;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
FILE * Abc_FrameReadOut( Abc_Frame_t * p )
{
    return p->Out;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
FILE * Abc_FrameReadErr( Abc_Frame_t * p )
{
    return p->Err;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_FrameReadMode( Abc_Frame_t * p )
{
    int fShortNames;
    char * pValue;
    pValue = Cmd_FlagReadByName( p, "namemode" );
    if ( pValue == NULL )
        fShortNames = 0;
    else 
        fShortNames = atoi(pValue);
    return fShortNames;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
368
int Abc_FrameSetMode( Abc_Frame_t * p, int fNameMode )
Alan Mishchenko committed
369 370
{
    char Buffer[2];
371
    int fNameModeOld;
Alan Mishchenko committed
372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394
    fNameModeOld = Abc_FrameReadMode( p );
    Buffer[0] = '0' + fNameMode;
    Buffer[1] = 0;
    Cmd_FlagUpdateValue( p, "namemode", (char *)Buffer );
    return fNameModeOld;
}


/**Function*************************************************************

  Synopsis    [Sets the given network to be the current one.]

  Description [Takes the network and makes it the current network.
  The previous current network is attached to the given network as 
  a backup copy. In the stack of backup networks contains too many
  networks (defined by the paramater "savesteps"), the bottom
  most network is deleted.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
395
void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtkNew )
Alan Mishchenko committed
396
{
Alan Mishchenko committed
397
    Abc_Ntk_t * pNtk, * pNtk2, * pNtk3;
Alan Mishchenko committed
398 399 400 401
    int nNetsPresent;
    int nNetsToSave;
    char * pValue;

Alan Mishchenko committed
402 403 404
    if ( p->pNtkCur == pNtkNew )
        return;

Alan Mishchenko committed
405
    // link it to the previous network
Alan Mishchenko committed
406
    Abc_NtkSetBackup( pNtkNew, p->pNtkCur );
Alan Mishchenko committed
407
    // set the step of this network
Alan Mishchenko committed
408
    Abc_NtkSetStep( pNtkNew, ++p->nSteps );
Alan Mishchenko committed
409
    // set this network to be the current network
Alan Mishchenko committed
410
    p->pNtkCur = pNtkNew;
Alan Mishchenko committed
411 412 413 414 415 416 417 418 419 420 421

    // remove any extra network that may happen to be in the stack
    pValue = Cmd_FlagReadByName( p, "savesteps" );
    // if the value of steps to save is not set, assume 1-level undo
    if ( pValue == NULL )
        nNetsToSave = 1;
    else 
        nNetsToSave = atoi(pValue);
    
    // count the network, remember the last one, and the one before the last one
    nNetsPresent = 0;
Alan Mishchenko committed
422 423
    pNtk2 = pNtk3 = NULL;
    for ( pNtk = p->pNtkCur; pNtk; pNtk = Abc_NtkBackup(pNtk2) )
Alan Mishchenko committed
424 425
    {
        nNetsPresent++;
Alan Mishchenko committed
426 427
        pNtk3 = pNtk2;
        pNtk2 = pNtk;
Alan Mishchenko committed
428 429 430 431 432
    }

    // remove the earliest backup network if it is more steps away than we store
    if ( nNetsPresent - 1 > nNetsToSave )
    { // delete the last network
Alan Mishchenko committed
433
        Abc_NtkDelete( pNtk2 );
Alan Mishchenko committed
434
        // clean the pointer of the network before the last one
Alan Mishchenko committed
435
        Abc_NtkSetBackup( pNtk3, NULL );
Alan Mishchenko committed
436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
    }
}

/**Function*************************************************************

  Synopsis    [This procedure swaps the current and the backup network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p )
{
Alan Mishchenko committed
452
    Abc_Ntk_t * pNtkCur, * pNtkBack, * pNtkBack2;
Alan Mishchenko committed
453 454 455
    int iStepCur, iStepBack;

    pNtkCur  = p->pNtkCur;
Alan Mishchenko committed
456
    pNtkBack = Abc_NtkBackup( pNtkCur );
Alan Mishchenko committed
457 458 459
    iStepCur = Abc_NtkStep  ( pNtkCur );

    // if there is no backup nothing to reset
Alan Mishchenko committed
460
    if ( pNtkBack == NULL )
Alan Mishchenko committed
461 462 463
        return;

    // remember the backup of the backup
Alan Mishchenko committed
464 465
    pNtkBack2 = Abc_NtkBackup( pNtkBack );
    iStepBack = Abc_NtkStep  ( pNtkBack );
Alan Mishchenko committed
466 467

    // set pNtkCur to be the next after the backup's backup
Alan Mishchenko committed
468
    Abc_NtkSetBackup( pNtkCur, pNtkBack2 );
Alan Mishchenko committed
469 470 471
    Abc_NtkSetStep  ( pNtkCur, iStepBack );

    // set pNtkCur to be the next after the backup
Alan Mishchenko committed
472 473
    Abc_NtkSetBackup( pNtkBack, pNtkCur );
    Abc_NtkSetStep  ( pNtkBack, iStepCur );
Alan Mishchenko committed
474 475

    // set the current network
Alan Mishchenko committed
476
    p->pNtkCur = pNtkBack;
Alan Mishchenko committed
477 478 479 480 481 482 483 484 485 486 487 488 489 490 491
}


/**Function*************************************************************

  Synopsis    [Replaces the current network by the given one.]

  Description [This procedure does not modify the stack of saved
  networks.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
492
void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtk )
Alan Mishchenko committed
493
{
Alan Mishchenko committed
494
    if ( pNtk == NULL )
Alan Mishchenko committed
495 496
        return;

497 498 499
    if ( Abc_NtkPoNum(pNtk) == 0 )
        Abc_Print( 0, "The current network has no primary outputs. Some commands may not work correctly.\n" );

Alan Mishchenko committed
500
    // transfer the parameters to the new network
Alan Mishchenko committed
501
    if ( p->pNtkCur && Abc_FrameIsFlagEnabled( "backup" ) )
Alan Mishchenko committed
502
    {
Alan Mishchenko committed
503 504
        Abc_NtkSetBackup( pNtk, Abc_NtkBackup(p->pNtkCur) );
        Abc_NtkSetStep( pNtk, Abc_NtkStep(p->pNtkCur) );
Alan Mishchenko committed
505 506 507 508 509
        // delete the current network
        Abc_NtkDelete( p->pNtkCur );
    }
    else
    {
Alan Mishchenko committed
510 511
        Abc_NtkSetBackup( pNtk, NULL );
        Abc_NtkSetStep( pNtk, ++p->nSteps );
Alan Mishchenko committed
512 513 514
        // delete the current network if present but backup is disabled
        if ( p->pNtkCur )
            Abc_NtkDelete( p->pNtkCur );
Alan Mishchenko committed
515 516
    }
    // set the new current network
Alan Mishchenko committed
517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534
    p->pNtkCur = pNtk;
}

/**Function*************************************************************

  Synopsis    [Removes library binding of all currently stored networks.]

  Description [This procedure is called when the library is freed.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_FrameUnmapAllNetworks( Abc_Frame_t * p )
{
    Abc_Ntk_t * pNtk;
    for ( pNtk = p->pNtkCur; pNtk; pNtk = Abc_NtkBackup(pNtk) )
Alan Mishchenko committed
535
        if ( Abc_NtkHasMapping(pNtk) )
Alan Mishchenko committed
536
            Abc_NtkMapToSop( pNtk );
Alan Mishchenko committed
537 538 539 540 541 542 543 544 545 546 547 548 549 550 551
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p )
{
Alan Mishchenko committed
552
    Abc_Ntk_t * pNtk, * pNtk2;
Alan Mishchenko committed
553
    // delete all the currently saved networks
Alan Mishchenko committed
554 555 556 557 558 559
    for ( pNtk  = p->pNtkCur, 
          pNtk2 = pNtk? Abc_NtkBackup(pNtk): NULL; 
          pNtk; 
          pNtk  = pNtk2, 
          pNtk2 = pNtk? Abc_NtkBackup(pNtk): NULL )
        Abc_NtkDelete( pNtk );
Alan Mishchenko committed
560 561
    // set the current network empty
    p->pNtkCur = NULL;
Alan Mishchenko committed
562
//    fprintf( p->Out, "All networks have been deleted.\n" );
Alan Mishchenko committed
563 564 565 566 567 568 569 570 571 572 573 574 575 576 577
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_FrameSetGlobalFrame( Abc_Frame_t * p )
{
Alan Mishchenko committed
578
    s_GlobalFrame = p;
Alan Mishchenko committed
579 580 581 582 583 584 585 586 587 588 589 590 591 592 593
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Frame_t * Abc_FrameGetGlobalFrame()
{
Alan Mishchenko committed
594
    if ( s_GlobalFrame == 0 )
Alan Mishchenko committed
595 596
    {
        // start the framework
Alan Mishchenko committed
597
        s_GlobalFrame = Abc_FrameAllocate();
Alan Mishchenko committed
598
        // perform initializations
Alan Mishchenko committed
599
        Abc_FrameInit( s_GlobalFrame );
Alan Mishchenko committed
600
    }
Alan Mishchenko committed
601
    return s_GlobalFrame;
Alan Mishchenko committed
602 603
}

Alan Mishchenko committed
604 605 606 607 608 609 610 611 612 613 614 615 616 617 618
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Frame_t * Abc_FrameReadGlobalFrame()
{
    return s_GlobalFrame;
}
Alan Mishchenko committed
619

Alan Mishchenko committed
620 621 622 623 624 625 626 627 628 629 630 631 632 633 634
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_FrameSetSave1( void * pAig )
{
    Abc_Frame_t * pFrame = Abc_FrameGetGlobalFrame();
    if ( pFrame->pSave1 )
635
        Aig_ManStop( (Aig_Man_t *)pFrame->pSave1 );
Alan Mishchenko committed
636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653
    pFrame->pSave1 = pAig;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_FrameSetSave2( void * pAig )
{
    Abc_Frame_t * pFrame = Abc_FrameGetGlobalFrame();
    if ( pFrame->pSave2 )
654
        Aig_ManStop( (Aig_Man_t *)pFrame->pSave2 );
Alan Mishchenko committed
655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671
    pFrame->pSave2 = pAig;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void * Abc_FrameReadSave1()  { void * pAig = Abc_FrameGetGlobalFrame()->pSave1; Abc_FrameGetGlobalFrame()->pSave1 = NULL; return pAig; }
void * Abc_FrameReadSave2()  { void * pAig = Abc_FrameGetGlobalFrame()->pSave2; Abc_FrameGetGlobalFrame()->pSave2 = NULL; return pAig; }

672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705
/**Function*************************************************************

  Synopsis    [Returns 0/1 if pNtkCur is an AIG and PO is 0/1; -1 otherwise.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum )
{
    Abc_Obj_t * pObj;
    if ( p->pNtkCur == NULL )
        return -1;
    if ( !Abc_NtkIsStrash(p->pNtkCur) )
        return -1;
    if ( iPoNum < 0 || iPoNum >= Abc_NtkPoNum(p->pNtkCur) )
        return -1;
    pObj = Abc_NtkPo( p->pNtkCur, iPoNum );
    if ( !Abc_AigNodeIsConst(Abc_ObjFanin0(pObj)) )
        return -1;
    return !Abc_ObjFaninC0(pObj);
}
void Abc_FrameCheckPoConstTest( Abc_Frame_t * p )
{
    Abc_Obj_t * pObj;
    int i;
    Abc_NtkForEachPo( p->pNtkCur, pObj, i )
        printf( "%d = %d\n", i, Abc_FrameCheckPoConst(p, i) );
}


Alan Mishchenko committed
706 707 708 709 710
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


711 712
ABC_NAMESPACE_IMPL_END