text: /**CFile****************************************************************
  
    FileName    [saigIoa.c]
  
    SystemName  [ABC: Logic synthesis and verification system.]
  
    PackageName [Sequential AIG package.]
  
    Synopsis    [Input/output for sequential AIGs using BLIF files.]
  
    Author      [Alan Mishchenko]
    
    Affiliation [UC Berkeley]
  
    Date        [Ver. 1.0. Started - June 20, 2005.]
  
    Revision    [$Id: saigIoa.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
  
  ***********************************************************************/
  
  #include <math.h>
  #include "saig.h"
  
  ABC_NAMESPACE_IMPL_START
  
  
  ////////////////////////////////////////////////////////////////////////
  ///                        DECLARATIONS                              ///
  ////////////////////////////////////////////////////////////////////////
  
  ////////////////////////////////////////////////////////////////////////
  ///                     FUNCTION DEFINITIONS                         ///
  ////////////////////////////////////////////////////////////////////////
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  char * Saig_ObjName( Aig_Man_t * p, Aig_Obj_t * pObj )
  {
      static char Buffer[16];
      if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
          sprintf( Buffer, "n%0*d", Abc_Base10Log(Aig_ManObjNumMax(p)), Aig_ObjId(pObj) );
      else if ( Saig_ObjIsPi(p, pObj) )
          sprintf( Buffer, "pi%0*d", Abc_Base10Log(Saig_ManPiNum(p)), Aig_ObjCioId(pObj) );
      else if ( Saig_ObjIsPo(p, pObj) )
          sprintf( Buffer, "po%0*d", Abc_Base10Log(Saig_ManPoNum(p)), Aig_ObjCioId(pObj) );
      else if ( Saig_ObjIsLo(p, pObj) )
          sprintf( Buffer, "lo%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPiNum(p) );
      else if ( Saig_ObjIsLi(p, pObj) )
          sprintf( Buffer, "li%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPoNum(p) );
      else 
          assert( 0 );
      return Buffer;
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
  {
      FILE * pFile;
      Aig_Obj_t * pObj, * pObjLi, * pObjLo;
      int i;
      if ( Aig_ManCoNum(p) == 0 )
      {
          printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
          return;
      }
      Aig_ManSetCioIds( p );
      // write input file
      pFile = fopen( pFileName, "w" );
      if ( pFile == NULL )
      {
          printf( "Saig_ManDumpBlif(): Cannot open file for writing.\n" );
          return;
      }
      fprintf( pFile, "# BLIF file written by procedure Saig_ManDumpBlif()\n" );
      fprintf( pFile, "# If unedited, this file can be read by Saig_ManReadBlif()\n" );
      fprintf( pFile, "# AIG stats: pi=%d po=%d reg=%d and=%d obj=%d maxid=%d\n", 
          Saig_ManPiNum(p), Saig_ManPoNum(p), Saig_ManRegNum(p), 
          Aig_ManNodeNum(p), Aig_ManObjNum(p), Aig_ManObjNumMax(p) );
      fprintf( pFile, ".model %s\n", p->pName );
      // write primary inputs
      fprintf( pFile, ".inputs" );
      Aig_ManForEachPiSeq( p, pObj, i )
          fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
      fprintf( pFile, "\n" );
      // write primary outputs
      fprintf( pFile, ".outputs" );
      Aig_ManForEachPoSeq( p, pObj, i )
          fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
      fprintf( pFile, "\n" );
      // write registers
      if ( Aig_ManRegNum(p) )
      {
          Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
          {
              fprintf( pFile, ".latch" );
              fprintf( pFile, " %s", Saig_ObjName(p, pObjLi) );
              fprintf( pFile, " %s", Saig_ObjName(p, pObjLo) );
              fprintf( pFile, " 0\n" );
          }
      } 
      // check if constant is used
      if ( Aig_ObjRefs(Aig_ManConst1(p)) )
          fprintf( pFile, ".names %s\n 1\n", Saig_ObjName(p, Aig_ManConst1(p)) );
      // write the nodes in the DFS order
      Aig_ManForEachNode( p, pObj, i )
      {
          fprintf( pFile, ".names" );
          fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
          fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin1(pObj)) );
          fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
          fprintf( pFile, "\n%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
      }
      // write the POs
      Aig_ManForEachCo( p, pObj, i )
      {
          fprintf( pFile, ".names" );
          fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
          fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
          fprintf( pFile, "\n%d 1\n", !Aig_ObjFaninC0(pObj) );
      }
      fprintf( pFile, ".end\n" );
      fclose( pFile );
  }
  
  /**Function*************************************************************
  
    Synopsis    [Reads one token from file.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  char * Saig_ManReadToken( FILE * pFile )
  {
      static char Buffer[1000];
      if ( fscanf( pFile, "%s", Buffer ) == 1 )
          return Buffer;
      return NULL;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Returns the corresponding number.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  int Saig_ManReadNumber( Aig_Man_t * p, char * pToken )
  {
      if ( pToken[0] == 'n' )
          return atoi( pToken + 1 );
      if ( pToken[0] == 'p' )
          return atoi( pToken + 2 );
      if ( pToken[0] == 'l' )
          return atoi( pToken + 2 );
      assert( 0 );
      return -1;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Returns the corresponding node.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  Aig_Obj_t * Saig_ManReadNode( Aig_Man_t * p, int * pNum2Id, char * pToken )
  {
      int Num;
      if ( pToken[0] == 'n' )
      {
          Num = atoi( pToken + 1 );
          return Aig_ManObj( p, pNum2Id[Num] );
      }
      if ( pToken[0] == 'p' )
      {
          pToken++;
          if ( pToken[0] == 'i' )
          {
              Num = atoi( pToken + 1 );
              return Aig_ManCi( p, Num );
          }
          if ( pToken[0] == 'o' )
              return NULL;
          assert( 0 );
          return NULL;
      }
      if ( pToken[0] == 'l' )
      {
          pToken++;
          if ( pToken[0] == 'o' )
          {
              Num = atoi( pToken + 1 );
              return Saig_ManLo( p, Num );
          }
          if ( pToken[0] == 'i' )
              return NULL;
          assert( 0 );
          return NULL;
      }
      assert( 0 );
      return NULL;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Reads BLIF previously dumped by Saig_ManDumpBlif().]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  Aig_Man_t * Saig_ManReadBlif( char * pFileName )
  {
      FILE * pFile;
      Aig_Man_t * p;
      Aig_Obj_t * pFanin0, * pFanin1, * pNode;
      char * pToken;
      int i, nPis, nPos, nRegs, Number;
      int * pNum2Id = NULL;  // mapping of node numbers in the file into AIG node IDs
      // open the file
      pFile = fopen( pFileName, "r" );
      if ( pFile == NULL )
      {
          printf( "Saig_ManReadBlif(): Cannot open file for reading.\n" );
          return NULL;
      }
      // skip through the comments
      for ( i = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; i++ );
      if ( pToken == NULL ) 
          { printf( "Saig_ManReadBlif(): Error 1.\n" ); return NULL; }
      // get he model
      pToken = Saig_ManReadToken( pFile );
      if ( pToken == NULL ) 
          { printf( "Saig_ManReadBlif(): Error 2.\n" ); return NULL; }
      // start the package
      p = Aig_ManStart( 10000 );
      p->pName = Abc_UtilStrsav( pToken );
      p->pSpec = Abc_UtilStrsav( pFileName );
      // count PIs
      pToken = Saig_ManReadToken( pFile );
      if ( pToken == NULL || strcmp( pToken, ".inputs" ) ) 
          { printf( "Saig_ManReadBlif(): Error 3.\n" ); Aig_ManStop(p); return NULL; }
      for ( nPis = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPis++ );
      // count POs
      if ( pToken == NULL || strcmp( pToken, ".outputs" ) ) 
          { printf( "Saig_ManReadBlif(): Error 4.\n" ); Aig_ManStop(p); return NULL; }
      for ( nPos = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPos++ );
      // count latches
      if ( pToken == NULL ) 
          { printf( "Saig_ManReadBlif(): Error 5.\n" ); Aig_ManStop(p); return NULL; }
      for ( nRegs = 0; strcmp( pToken, ".latch" ) == 0; nRegs++ )
      {
          pToken = Saig_ManReadToken( pFile );
          if ( pToken == NULL ) 
              { printf( "Saig_ManReadBlif(): Error 6.\n" ); Aig_ManStop(p); return NULL; }
          pToken = Saig_ManReadToken( pFile );
          if ( pToken == NULL ) 
              { printf( "Saig_ManReadBlif(): Error 7.\n" ); Aig_ManStop(p); return NULL; }
          pToken = Saig_ManReadToken( pFile );
          if ( pToken == NULL ) 
              { printf( "Saig_ManReadBlif(): Error 8.\n" ); Aig_ManStop(p); return NULL; }
          pToken = Saig_ManReadToken( pFile );
          if ( pToken == NULL ) 
              { printf( "Saig_ManReadBlif(): Error 9.\n" ); Aig_ManStop(p); return NULL; }
      }
      // create PIs and LOs
      for ( i = 0; i < nPis + nRegs; i++ )
          Aig_ObjCreateCi( p );
      Aig_ManSetRegNum( p, nRegs );
      // create nodes
      for ( i = 0; strcmp( pToken, ".names" ) == 0; i++ )
      {
          // first token
          pToken = Saig_ManReadToken( pFile );
          if ( i == 0 && pToken[0] == 'n' )
          { // constant node
              // read 1
              pToken = Saig_ManReadToken( pFile );
              if ( pToken == NULL || strcmp( pToken, "1" ) ) 
                  { printf( "Saig_ManReadBlif(): Error 10.\n" ); Aig_ManStop(p); return NULL; }
              // read next
              pToken = Saig_ManReadToken( pFile );
              if ( pToken == NULL ) 
                  { printf( "Saig_ManReadBlif(): Error 11.\n" ); Aig_ManStop(p); return NULL; }
              continue;
          }
          pFanin0 = Saig_ManReadNode( p, pNum2Id, pToken );
  
          // second token
          pToken = Saig_ManReadToken( pFile );
          if ( (pToken[0] == 'p' && pToken[1] == 'o') || (pToken[0] == 'l' && pToken[1] == 'i') )
          { // buffer
              // read complemented attribute
              pToken = Saig_ManReadToken( pFile );
              if ( pToken == NULL ) 
                  { printf( "Saig_ManReadBlif(): Error 12.\n" ); Aig_ManStop(p); return NULL; }
              if ( pToken[0] == '0' )
                  pFanin0 = Aig_Not(pFanin0);
              // read 1
              pToken = Saig_ManReadToken( pFile );
              if ( pToken == NULL || strcmp( pToken, "1" ) ) 
                  { printf( "Saig_ManReadBlif(): Error 13.\n" ); Aig_ManStop(p); return NULL; }
              Aig_ObjCreateCo( p, pFanin0 );
              // read next
              pToken = Saig_ManReadToken( pFile );
              if ( pToken == NULL ) 
                  { printf( "Saig_ManReadBlif(): Error 14.\n" ); Aig_ManStop(p); return NULL; }
              continue;
          }
  
          // third token
          // regular node
          pFanin1 = Saig_ManReadNode( p, pNum2Id, pToken );
          pToken = Saig_ManReadToken( pFile );
          Number = Saig_ManReadNumber( p, pToken );
          // allocate mapping
          if ( pNum2Id == NULL )
          {
  //            extern double pow( double x, double y );
              int Size = (int)pow(10.0, (double)(strlen(pToken) - 1));
              pNum2Id = ABC_CALLOC( int, Size );
          }
  
          // other tokens
          // get the complemented attributes
          pToken = Saig_ManReadToken( pFile );
          if ( pToken == NULL ) 
              { printf( "Saig_ManReadBlif(): Error 15.\n" ); Aig_ManStop(p); return NULL; }
          if ( pToken[0] == '0' )
              pFanin0 = Aig_Not(pFanin0);
          if ( pToken[1] == '0' )
              pFanin1 = Aig_Not(pFanin1);
          // read 1
          pToken = Saig_ManReadToken( pFile );
          if ( pToken == NULL || strcmp( pToken, "1" ) ) 
              { printf( "Saig_ManReadBlif(): Error 16.\n" ); Aig_ManStop(p); return NULL; }
          // read next
          pToken = Saig_ManReadToken( pFile );
          if ( pToken == NULL ) 
              { printf( "Saig_ManReadBlif(): Error 17.\n" ); Aig_ManStop(p); return NULL; }
  
          // create new node
          pNode = Aig_And( p, pFanin0, pFanin1 );
          if ( Aig_IsComplement(pNode) )
              { printf( "Saig_ManReadBlif(): Error 18.\n" ); Aig_ManStop(p); return NULL; }
          // set mapping
          pNum2Id[ Number ] = pNode->Id;
      }
      if ( pToken == NULL || strcmp( pToken, ".end" ) ) 
          { printf( "Saig_ManReadBlif(): Error 19.\n" ); Aig_ManStop(p); return NULL; }
      if ( nPos + nRegs != Aig_ManCoNum(p) ) 
          { printf( "Saig_ManReadBlif(): Error 20.\n" ); Aig_ManStop(p); return NULL; }
      // add non-node objects to the mapping
      Aig_ManForEachCi( p, pNode, i )
          pNum2Id[pNode->Id] = pNode->Id;
  //    ABC_FREE( pNum2Id );
      p->pData = pNum2Id;
      // check the new manager
      Aig_ManSetRegNum( p, nRegs );
      if ( !Aig_ManCheck(p) )
          printf( "Saig_ManReadBlif(): Check has failed.\n" );
      return p;
  }
  
  ////////////////////////////////////////////////////////////////////////
  ///                       END OF FILE                                ///
  ////////////////////////////////////////////////////////////////////////
  
  
  ABC_NAMESPACE_IMPL_END
  
  