text: /**CFile****************************************************************
  
    FileName    [giaSim.c]
  
    SystemName  [ABC: Logic synthesis and verification system.]
  
    PackageName [Scalable AIG package.]
  
    Synopsis    [Fast sequential simulator.]
  
    Author      [Alan Mishchenko]
    
    Affiliation [UC Berkeley]
  
    Date        [Ver. 1.0. Started - June 20, 2005.]
  
    Revision    [$Id: giaSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
  
  ***********************************************************************/
  
  #include "gia.h"
  #include "misc/util/utilTruth.h"
  
  ABC_NAMESPACE_IMPL_START
  
  
  ////////////////////////////////////////////////////////////////////////
  ///                        DECLARATIONS                              ///
  ////////////////////////////////////////////////////////////////////////
  
  static inline unsigned * Gia_SimData( Gia_ManSim_t * p, int i )    { return p->pDataSim + i * p->nWords;    }
  static inline unsigned * Gia_SimDataCi( Gia_ManSim_t * p, int i )  { return p->pDataSimCis + i * p->nWords; }
  static inline unsigned * Gia_SimDataCo( Gia_ManSim_t * p, int i )  { return p->pDataSimCos + i * p->nWords; }
  
  unsigned * Gia_SimDataExt( Gia_ManSim_t * p, int i )    { return Gia_SimData(p, i);    }
  unsigned * Gia_SimDataCiExt( Gia_ManSim_t * p, int i )  { return Gia_SimDataCi(p, i);  }
  unsigned * Gia_SimDataCoExt( Gia_ManSim_t * p, int i )  { return Gia_SimDataCo(p, i);  }
  
  ////////////////////////////////////////////////////////////////////////
  ///                     FUNCTION DEFINITIONS                         ///
  ////////////////////////////////////////////////////////////////////////
  
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Gia_ManSimCollect_rec( Gia_Man_t * pGia, Gia_Obj_t * pObj, Vec_Int_t * vVec )
  {
      Vec_IntPush( vVec, Gia_ObjToLit(pGia, pObj) );
      if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) )
          return;
      assert( Gia_ObjIsAnd(pObj) );
      Gia_ManSimCollect_rec( pGia, Gia_ObjChild0(pObj), vVec );
      Gia_ManSimCollect_rec( pGia, Gia_ObjChild1(pObj), vVec );
  }
  
  /**Function*************************************************************
  
    Synopsis    [Derives signal implications.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Gia_ManSimCollect( Gia_Man_t * pGia, Gia_Obj_t * pObj, Vec_Int_t * vVec )
  {
      Vec_IntClear( vVec );
      Gia_ManSimCollect_rec( pGia, pObj, vVec );
      Vec_IntUniqify( vVec );
  }
  
  /**Function*************************************************************
  
    Synopsis    [Finds signals, which reset flops to have constant values.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  Vec_Int_t * Gia_ManSimDeriveResets( Gia_Man_t * pGia )
  {
      int nImpLimit = 5;
      Vec_Int_t * vResult;
      Vec_Int_t * vCountLits, * vSuperGate;
      Gia_Obj_t * pObj;
      int i, k, Lit, Count;
      int Counter0 = 0, Counter1 = 0;
      int CounterPi0 = 0, CounterPi1 = 0;
      abctime clk = Abc_Clock();
  
      // create reset counters for each literal
      vCountLits = Vec_IntStart( 2 * Gia_ManObjNum(pGia) );
  
      // collect implications for each flop input driver
      vSuperGate = Vec_IntAlloc( 1000 );
      Gia_ManForEachRi( pGia, pObj, i )
      {
          if ( Gia_ObjFaninId0p(pGia, pObj) == 0 )
              continue;
          Vec_IntAddToEntry( vCountLits, Gia_ObjToLit(pGia, Gia_ObjChild0(pObj)), 1 );
          Gia_ManSimCollect( pGia, Gia_ObjFanin0(pObj), vSuperGate );
          Vec_IntForEachEntry( vSuperGate, Lit, k )
              Vec_IntAddToEntry( vCountLits, Lit, 1 );
      }
      Vec_IntFree( vSuperGate );
  
      // label signals whose counter if more than the limit
      vResult = Vec_IntStartFull( Gia_ManObjNum(pGia) );
      Vec_IntForEachEntry( vCountLits, Count, Lit )
      {
          if ( Count < nImpLimit )
              continue;
          pObj = Gia_ManObj( pGia, Abc_Lit2Var(Lit) );
          if ( Abc_LitIsCompl(Lit) ) // const 0
          {
  //            Ssm_ObjSetLogic0( pObj );
              Vec_IntWriteEntry( vResult, Abc_Lit2Var(Lit), 0 );
              CounterPi0 += Gia_ObjIsPi(pGia, pObj);
              Counter0++;
          }
          else
          {
  //            Ssm_ObjSetLogic1( pObj );
              Vec_IntWriteEntry( vResult, Abc_Lit2Var(Lit), 1 );
              CounterPi1 += Gia_ObjIsPi(pGia, pObj);
              Counter1++;
          }
  //        if ( Gia_ObjIsPi(pGia, pObj) )
  //            printf( "%d ", Count );
      }
  //    printf( "\n" );
      Vec_IntFree( vCountLits );
  
      printf( "Logic0 = %d (%d). Logic1 = %d (%d). ", Counter0, CounterPi0, Counter1, CounterPi1 );
      Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
      return vResult;
  }
  
  
  /**Function*************************************************************
  
    Synopsis    [This procedure sets default parameters.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p )
  {
      memset( p, 0, sizeof(Gia_ParSim_t) );
      // user-controlled parameters
      p->nWords       =   8;    // the number of machine words
      p->nIters       =  32;    // the number of timeframes
      p->RandSeed     =   0;    // the seed to generate random numbers
      p->TimeLimit    =  60;    // time limit in seconds
      p->fCheckMiter  =   0;    // check if miter outputs are non-zero 
      p->fVerbose     =   0;    // enables verbose output
      p->iOutFail     =  -1;    // index of the failed output
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Gia_ManSimDelete( Gia_ManSim_t * p )
  {
      Vec_IntFreeP( &p->vConsts );
      Vec_IntFreeP( &p->vCis2Ids );
      Gia_ManStopP( &p->pAig );
      ABC_FREE( p->pDataSim );
      ABC_FREE( p->pDataSimCis );
      ABC_FREE( p->pDataSimCos );
      ABC_FREE( p );
  }
  
  /**Function*************************************************************
  
    Synopsis    [Creates fast simulation manager.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  Gia_ManSim_t * Gia_ManSimCreate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
  {
      Gia_ManSim_t * p;
      int Entry, i;
      p = ABC_ALLOC( Gia_ManSim_t, 1 );
      memset( p, 0, sizeof(Gia_ManSim_t) );
      // look for reset signals
      if ( pPars->fVerbose )
          p->vConsts = Gia_ManSimDeriveResets( pAig );
      // derive the frontier
      p->pAig   = Gia_ManFront( pAig );
      p->pPars  = pPars;
      p->nWords = pPars->nWords;
      p->pDataSim = ABC_ALLOC( unsigned, p->nWords * p->pAig->nFront );
      p->pDataSimCis = ABC_ALLOC( unsigned, p->nWords * Gia_ManCiNum(p->pAig) );
      p->pDataSimCos = ABC_ALLOC( unsigned, p->nWords * Gia_ManCoNum(p->pAig) );
      if ( !p->pDataSim || !p->pDataSimCis || !p->pDataSimCos )
      { 
          Abc_Print( 1, "Simulator could not allocate %.2f GB for simulation info.\n", 
              4.0 * p->nWords * (p->pAig->nFront + Gia_ManCiNum(p->pAig) + Gia_ManCoNum(p->pAig)) / (1<<30) );
          Gia_ManSimDelete( p );
          return NULL;
      }
      p->vCis2Ids = Vec_IntAlloc( Gia_ManCiNum(p->pAig) );
      Vec_IntForEachEntry( pAig->vCis, Entry, i )
          Vec_IntPush( p->vCis2Ids, i );  //  do we need p->vCis2Ids?
      if ( pPars->fVerbose )
      Abc_Print( 1, "AIG = %7.2f MB.   Front mem = %7.2f MB.  Other mem = %7.2f MB.\n", 
          12.0*Gia_ManObjNum(p->pAig)/(1<<20), 
          4.0*p->nWords*p->pAig->nFront/(1<<20), 
          4.0*p->nWords*(Gia_ManCiNum(p->pAig) + Gia_ManCoNum(p->pAig))/(1<<20) );
  
      return p;
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  static inline void Gia_ManSimInfoRandom( Gia_ManSim_t * p, unsigned * pInfo )
  {
      int w;
      for ( w = p->nWords-1; w >= 0; w-- )
          pInfo[w] = Gia_ManRandom( 0 );
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  static inline void Gia_ManSimInfoZero( Gia_ManSim_t * p, unsigned * pInfo )
  {
      int w;
      for ( w = p->nWords-1; w >= 0; w-- )
          pInfo[w] = 0;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Returns index of the first pattern that failed.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  static inline int Gia_ManSimInfoIsZero( Gia_ManSim_t * p, unsigned * pInfo )
  {
      int w;
      for ( w = 0; w < p->nWords; w++ )
          if ( pInfo[w] )
              return 32*w + Gia_WordFindFirstBit( pInfo[w] );
      return -1;
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  static inline void Gia_ManSimInfoOne( Gia_ManSim_t * p, unsigned * pInfo )
  {
      int w;
      for ( w = p->nWords-1; w >= 0; w-- )
          pInfo[w] = ~0;
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  static inline void Gia_ManSimInfoCopy( Gia_ManSim_t * p, unsigned * pInfo, unsigned * pInfo0 )
  {
      int w;
      for ( w = p->nWords-1; w >= 0; w-- )
          pInfo[w] = pInfo0[w];
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  static inline void Gia_ManSimulateCi( Gia_ManSim_t * p, Gia_Obj_t * pObj, int iCi )
  {
      unsigned * pInfo  = Gia_SimData( p, Gia_ObjValue(pObj) );
      unsigned * pInfo0 = Gia_SimDataCi( p, iCi );
      int w;
      for ( w = p->nWords-1; w >= 0; w-- )
          pInfo[w] = pInfo0[w];
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  static inline void Gia_ManSimulateCo( Gia_ManSim_t * p, int iCo, Gia_Obj_t * pObj )
  {
      unsigned * pInfo  = Gia_SimDataCo( p, iCo );
      unsigned * pInfo0 = Gia_SimData( p, Gia_ObjDiff0(pObj) );
      int w;
      if ( Gia_ObjFaninC0(pObj) )
          for ( w = p->nWords-1; w >= 0; w-- )
              pInfo[w] = ~pInfo0[w];
      else 
          for ( w = p->nWords-1; w >= 0; w-- )
              pInfo[w] = pInfo0[w];
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  static inline void Gia_ManSimulateNode( Gia_ManSim_t * p, Gia_Obj_t * pObj )
  {
      unsigned * pInfo  = Gia_SimData( p, Gia_ObjValue(pObj) );
      unsigned * pInfo0 = Gia_SimData( p, Gia_ObjDiff0(pObj) );
      unsigned * pInfo1 = Gia_SimData( p, Gia_ObjDiff1(pObj) );
      int w;
      if ( Gia_ObjFaninC0(pObj) )
      {
          if (  Gia_ObjFaninC1(pObj) )
              for ( w = p->nWords-1; w >= 0; w-- )
                  pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
          else 
              for ( w = p->nWords-1; w >= 0; w-- )
                  pInfo[w] = ~pInfo0[w] & pInfo1[w];
      }
      else 
      {
          if (  Gia_ObjFaninC1(pObj) )
              for ( w = p->nWords-1; w >= 0; w-- )
                  pInfo[w] = pInfo0[w] & ~pInfo1[w];
          else 
              for ( w = p->nWords-1; w >= 0; w-- )
                  pInfo[w] = pInfo0[w] & pInfo1[w];
      }
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Gia_ManSimInfoInit( Gia_ManSim_t * p )
  {
      int iPioNum, i;
      Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
      {
          if ( iPioNum < Gia_ManPiNum(p->pAig) )
              Gia_ManSimInfoRandom( p, Gia_SimDataCi(p, i) );
          else
              Gia_ManSimInfoZero( p, Gia_SimDataCi(p, i) );
      }
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Gia_ManSimInfoTransfer( Gia_ManSim_t * p )
  {
      int iPioNum, i;
      Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
      {
          if ( iPioNum < Gia_ManPiNum(p->pAig) )
              Gia_ManSimInfoRandom( p, Gia_SimDataCi(p, i) );
          else
              Gia_ManSimInfoCopy( p, Gia_SimDataCi(p, i), Gia_SimDataCo(p, Gia_ManPoNum(p->pAig)+iPioNum-Gia_ManPiNum(p->pAig)) );
      }
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Gia_ManSimulateRound( Gia_ManSim_t * p )
  {
      Gia_Obj_t * pObj;
      int i, iCis = 0, iCos = 0;
      assert( p->pAig->nFront > 0 );
      assert( Gia_ManConst0(p->pAig)->Value == 0 );
      Gia_ManSimInfoZero( p, Gia_SimData(p, 0) );
      Gia_ManForEachObj1( p->pAig, pObj, i )
      {
          if ( Gia_ObjIsAndOrConst0(pObj) )
          {
              assert( Gia_ObjValue(pObj) < p->pAig->nFront );
              Gia_ManSimulateNode( p, pObj );
          }
          else if ( Gia_ObjIsCo(pObj) )
          {
              assert( Gia_ObjValue(pObj) == GIA_NONE );
              Gia_ManSimulateCo( p, iCos++, pObj );
          }
          else // if ( Gia_ObjIsCi(pObj) )
          {
              assert( Gia_ObjValue(pObj) < p->pAig->nFront );
              Gia_ManSimulateCi( p, pObj, iCis++ );
          }
      }
      assert( Gia_ManCiNum(p->pAig) == iCis );
      assert( Gia_ManCoNum(p->pAig) == iCos );
  }
  
  /**Function*************************************************************
  
    Synopsis    [Returns index of the PO and pattern that failed it.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  static inline int Gia_ManCheckPos( Gia_ManSim_t * p, int * piPo, int * piPat )
  {
      int i, iPat;
      for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
      {
          iPat = Gia_ManSimInfoIsZero( p, Gia_SimDataCo(p, i) );
          if ( iPat >= 0 )
          {
              *piPo = i;
              *piPat = iPat;
              return 1;
          }
      }
      return 0;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Returns the counter-example.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t * vCis2Ids )
  {
      Abc_Cex_t * p;
      unsigned * pData;
      int f, i, w, iPioId, Counter;
      p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
      p->iFrame = iFrame;
      p->iPo    = iOut;
      // fill in the binary data
      Counter = p->nRegs;
      pData = ABC_ALLOC( unsigned, nWords );
      for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
      for ( i = 0; i < Gia_ManPiNum(pAig); i++ )
      {
          iPioId = Vec_IntEntry( vCis2Ids, i );
          if ( iPioId >= p->nPis )
              continue;
          for ( w = nWords-1; w >= 0; w-- )
              pData[w] = Gia_ManRandom( 0 );
          if ( Abc_InfoHasBit( pData, iPat ) )
              Abc_InfoSetBit( p->pData, Counter + iPioId );
      }
      ABC_FREE( pData );
      return p;
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Gia_ManResetRandom( Gia_ParSim_t * pPars )
  {
      int i;
      Gia_ManRandom( 1 );
      for ( i = 0; i < pPars->RandSeed; i++ )
          Gia_ManRandom( 0 );
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
  {
      extern int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
      Gia_ManSim_t * p;
      abctime clkTotal = Abc_Clock();
      int i, iOut, iPat, RetValue = 0;
      abctime nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
      if ( pAig->pReprs && pAig->pNexts )
          return Gia_ManSimSimulateEquiv( pAig, pPars );
      ABC_FREE( pAig->pCexSeq );
      p = Gia_ManSimCreate( pAig, pPars );
      Gia_ManResetRandom( pPars );
      Gia_ManSimInfoInit( p );
      for ( i = 0; i < pPars->nIters; i++ )
      {
          Gia_ManSimulateRound( p );
          if ( pPars->fVerbose )
          {
              Abc_Print( 1, "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
              Abc_Print( 1, "Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC );
          }
          if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) )
          {
              Gia_ManResetRandom( pPars );
              pPars->iOutFail = iOut;
              pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
              Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", iOut, pAig->pName, i );
              if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
              {
  //                Abc_Print( 1, "\n" );
                  Abc_Print( 1, "\nGenerated counter-example is INVALID.                    " );
  //                Abc_Print( 1, "\n" );
              }
              else
              {
  //                Abc_Print( 1, "\n" );
  //                if ( pPars->fVerbose )
  //                Abc_Print( 1, "\nGenerated counter-example is verified correctly.         " );
  //                Abc_Print( 1, "\n" );
              }
              RetValue = 1;
              break;
          }
          if ( Abc_Clock() > nTimeToStop )
          {
              i++;
              break;
          }
          if ( i < pPars->nIters - 1 )
              Gia_ManSimInfoTransfer( p );
      }
      Gia_ManSimDelete( p );
      if ( pAig->pCexSeq == NULL )
          Abc_Print( 1, "No bug detected after simulating %d frames with %d words.  ", i, pPars->nWords );
      Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
      return RetValue;
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  Vec_Int_t * Gia_ManSimReadFile( char * pFileIn )
  {
      int c;
      Vec_Int_t * vPat;
      FILE * pFile = fopen( pFileIn, "rb" );
      if ( pFile == NULL )
      {
          printf( "Cannot open input file.\n" );
          return NULL;
      }
      vPat = Vec_IntAlloc( 1000 );
      while ( (c = fgetc(pFile)) != EOF )
          if ( c == '0' || c == '1' )
              Vec_IntPush( vPat, c - '0' );
      fclose( pFile );
      return vPat;
  }
  int Gia_ManSimWriteFile( char * pFileOut, Vec_Int_t * vPat, int nOuts )
  {
      int c, i;
      FILE * pFile = fopen( pFileOut, "wb" );
      if ( pFile == NULL )
      {
          printf( "Cannot open output file.\n" );
          return 0;
      }
      assert( Vec_IntSize(vPat) % nOuts == 0 );
      Vec_IntForEachEntry( vPat, c, i )
      {
          fputc( '0' + c, pFile );
          if ( i % nOuts == nOuts - 1 )
              fputc( '\n', pFile );
      }
      fclose( pFile );
      return 1;
  }
  Vec_Int_t * Gia_ManSimSimulateOne( Gia_Man_t * p, Vec_Int_t * vPat )
  {
      Vec_Int_t * vPatOut;
      Gia_Obj_t * pObj, * pObjRo;
      int i, k, f;
      assert( Vec_IntSize(vPat) % Gia_ManPiNum(p) == 0 );
      Gia_ManConst0(p)->fMark1 = 0;
      Gia_ManForEachRo( p, pObj, i )
          pObj->fMark1 = 0;
      vPatOut = Vec_IntAlloc( 1000 );
      for ( k = f = 0; f < Vec_IntSize(vPat) / Gia_ManPiNum(p); f++ )
      {
          Gia_ManForEachPi( p, pObj, i )
              pObj->fMark1 = Vec_IntEntry( vPat, k++ );
          Gia_ManForEachAnd( p, pObj, i )
              pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
          Gia_ManForEachCo( p, pObj, i )
              pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj));
          Gia_ManForEachPo( p, pObj, i )
              Vec_IntPush( vPatOut, pObj->fMark1 );
          Gia_ManForEachRiRo( p, pObj, pObjRo, i )
              pObjRo->fMark1 = pObj->fMark1;
      }
      assert( k == Vec_IntSize(vPat) );
      Gia_ManForEachObj( p, pObj, i )
          pObj->fMark1 = 0;
      return vPatOut;
  }
  void Gia_ManSimSimulatePattern( Gia_Man_t * p, char * pFileIn, char * pFileOut )
  {
      Vec_Int_t * vPat, * vPatOut;
      vPat = Gia_ManSimReadFile( pFileIn );
      if ( vPat == NULL )
          return;
      if ( Vec_IntSize(vPat) % Gia_ManPiNum(p) )
      {
          printf( "The number of 0s and 1s in the input file (%d) does not evenly divide by the number of primary inputs (%d).\n", 
              Vec_IntSize(vPat), Gia_ManPiNum(p) );
          Vec_IntFree( vPat );
          return;
      }
      vPatOut = Gia_ManSimSimulateOne( p, vPat );
      if ( Gia_ManSimWriteFile( pFileOut, vPatOut, Gia_ManPoNum(p) ) )
          printf( "Output patterns are written into file \"%s\".\n", pFileOut );
      Vec_IntFree( vPat );
      Vec_IntFree( vPatOut );
  }
  
  
  /**Function*************************************************************
  
    Synopsis    [Bit-parallel simulation during AIG construction.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  static inline word * Gia_ManBuiltInDataPi( Gia_Man_t * p, int iCiId )
  {
      return Vec_WrdEntryP( p->vSimsPi, p->nSimWords * iCiId );
  }
  static inline word * Gia_ManBuiltInData( Gia_Man_t * p, int iObj )
  {
      return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj );
  }
  static inline void Gia_ManBuiltInDataPrint( Gia_Man_t * p, int iObj )
  {
  //    printf( "Obj %6d : ", iObj ); Extra_PrintBinary( stdout, Gia_ManBuiltInData(p, iObj), p->nSimWords * 64 ); printf( "\n" );
  }
  void Gia_ManBuiltInSimStart( Gia_Man_t * p, int nWords, int nObjs )
  {
      int i, k;
      assert( !p->fBuiltInSim );
      assert( Gia_ManAndNum(p) == 0 );
      p->fBuiltInSim = 1;
      p->iPatsPi = 0;
      p->iPastPiMax = 0;
      p->nSimWords = nWords;
      p->nSimWordsMax = 8;
      Gia_ManRandomW( 1 );
      // init PI care info
      p->vSimsPi = Vec_WrdAlloc( p->nSimWords * Gia_ManCiNum(p) );
      Vec_WrdFill( p->vSimsPi, p->nSimWords * Gia_ManCiNum(p), 0 );
      // init object sim info
      p->vSims = Vec_WrdAlloc( p->nSimWords * nObjs );
      Vec_WrdFill( p->vSims, p->nSimWords, 0 );
      for ( i = 0; i < Gia_ManCiNum(p); i++ )
          for ( k = 0; k < p->nSimWords; k++ )
              Vec_WrdPush( p->vSims, Gia_ManRandomW(0) );
  }
  void Gia_ManBuiltInSimPerformInt( Gia_Man_t * p, int iObj )
  {
      Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); int w;
      word * pInfo  = Gia_ManBuiltInData( p, iObj ); 
      word * pInfo0 = Gia_ManBuiltInData( p, Gia_ObjFaninId0(pObj, iObj) );
      word * pInfo1 = Gia_ManBuiltInData( p, Gia_ObjFaninId1(pObj, iObj) ); 
      assert( p->fBuiltInSim || p->fIncrSim );
      if ( Gia_ObjFaninC0(pObj) )
      {
          if (  Gia_ObjFaninC1(pObj) )
              for ( w = 0; w < p->nSimWords; w++ )
                  pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
          else 
              for ( w = 0; w < p->nSimWords; w++ )
                  pInfo[w] = ~pInfo0[w] & pInfo1[w];
      }
      else 
      {
          if (  Gia_ObjFaninC1(pObj) )
              for ( w = 0; w < p->nSimWords; w++ )
                  pInfo[w] = pInfo0[w] & ~pInfo1[w];
          else 
              for ( w = 0; w < p->nSimWords; w++ )
                  pInfo[w] = pInfo0[w] & pInfo1[w];
      }
      assert( Vec_WrdSize(p->vSims) == Gia_ManObjNum(p) * p->nSimWords );
  }
  void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj )
  {
      int w;
      for ( w = 0; w < p->nSimWords; w++ )
          Vec_WrdPush( p->vSims, 0 );
      Gia_ManBuiltInSimPerformInt( p, iObj );
  }
  
  void Gia_ManBuiltInSimResimulateCone_rec( Gia_Man_t * p, int iObj )
  {
      Gia_Obj_t * pObj;
      if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
          return;
      Gia_ObjSetTravIdCurrentId(p, iObj);
      pObj = Gia_ManObj( p, iObj );
      if ( Gia_ObjIsCi(pObj) )
          return;
      assert( Gia_ObjIsAnd(pObj) );
      Gia_ManBuiltInSimResimulateCone_rec( p, Gia_ObjFaninId0(pObj, iObj) );
      Gia_ManBuiltInSimResimulateCone_rec( p, Gia_ObjFaninId1(pObj, iObj) );
      Gia_ManBuiltInSimPerformInt( p, iObj );
  }
  void Gia_ManBuiltInSimResimulateCone( Gia_Man_t * p, int iLit0, int iLit1 )
  {
      Gia_ManIncrementTravId( p );
      Gia_ManBuiltInSimResimulateCone_rec( p, Abc_Lit2Var(iLit0) );
      Gia_ManBuiltInSimResimulateCone_rec( p, Abc_Lit2Var(iLit1) );
  }
  void Gia_ManBuiltInSimResimulate( Gia_Man_t * p )
  {
      Gia_Obj_t * pObj;  int iObj;
      Gia_ManForEachAnd( p, pObj, iObj )
          Gia_ManBuiltInSimPerformInt( p, iObj );
  }
  
  int Gia_ManBuiltInSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 )
  {
      word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) );
      word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w;
      assert( p->fBuiltInSim || p->fIncrSim );
  
  //    printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) );
  //    Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" );
  //    Extra_PrintBinary( stdout, pInfo1, 64*p->nSimWords ); printf( "\n" );
  //    printf( "\n" );
  
      if ( Abc_LitIsCompl(iLit0) )
      {
          if (  Abc_LitIsCompl(iLit1) )
          {
              for ( w = 0; w < p->nSimWords; w++ )
                  if ( ~pInfo0[w] & ~pInfo1[w] )
                      return 1;
          }
          else 
          {
              for ( w = 0; w < p->nSimWords; w++ )
                  if ( ~pInfo0[w] & pInfo1[w] )
                      return 1;
          }
      }
      else 
      {
          if (  Abc_LitIsCompl(iLit1) )
          {
              for ( w = 0; w < p->nSimWords; w++ )
                  if ( pInfo0[w] & ~pInfo1[w] )
                      return 1;
          }
          else 
          {
              for ( w = 0; w < p->nSimWords; w++ )
                  if ( pInfo0[w] & pInfo1[w] )
                      return 1;
          }
      }
      return 0;
  }
  int Gia_ManBuiltInSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 )
  {
      word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) );
      word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w;
      assert( p->fBuiltInSim || p->fIncrSim );
  
  //    printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) );
  //    Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" );
  //    Extra_PrintBinary( stdout, pInfo1, 64*p->nSimWords ); printf( "\n" );
  //    printf( "\n" );
  
      if ( Abc_LitIsCompl(iLit0) )
      {
          if (  Abc_LitIsCompl(iLit1) )
          {
              for ( w = 0; w < p->nSimWords; w++ )
                  if ( ~pInfo0[w] != ~pInfo1[w] )
                      return 0;
          }
          else 
          {
              for ( w = 0; w < p->nSimWords; w++ )
                  if ( ~pInfo0[w] != pInfo1[w] )
                      return 0;
          }
      }
      else 
      {
          if (  Abc_LitIsCompl(iLit1) )
          {
              for ( w = 0; w < p->nSimWords; w++ )
                  if ( pInfo0[w] != ~pInfo1[w] )
                      return 0;
          }
          else 
          {
              for ( w = 0; w < p->nSimWords; w++ )
                  if ( pInfo0[w] != pInfo1[w] )
                      return 0;
          }
      }
      return 1;
  }
  
  int Gia_ManBuiltInSimPack( Gia_Man_t * p, Vec_Int_t * vPat )
  {
      int i, k, iLit;
      assert( Vec_IntSize(vPat) > 0 );
      //printf( "%d ", Vec_IntSize(vPat) );
      for ( i = 0; i < p->iPatsPi; i++ )
      {
          Vec_IntForEachEntry( vPat, iLit, k )
              if ( Abc_TtGetBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), i) && 
                   Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), i) == Abc_LitIsCompl(iLit) )
                  break;
          if ( k == Vec_IntSize(vPat) )
              return i; // success
      }
      return -1; // failure
  }
  // adds PI pattern to storage; the pattern comes in terms of CiIds
  int Gia_ManBuiltInSimAddPat( Gia_Man_t * p, Vec_Int_t * vPat )
  {
      int Period = 0xF;
      int fOverflow = p->iPatsPi == 64 * p->nSimWords && p->nSimWords == p->nSimWordsMax;
      int k, iLit, iPat = Gia_ManBuiltInSimPack( p, vPat );
      if ( iPat == -1 )
      {
          if ( fOverflow )
          {
              if ( (p->iPastPiMax & Period) == 0 )
                  Gia_ManBuiltInSimResimulate( p );
              iPat = p->iPastPiMax;
              //if ( p->iPastPiMax == 64 * p->nSimWordsMax - 1 )
              //    printf( "Completed the cycle.\n" );
              p->iPastPiMax = p->iPastPiMax == 64 * p->nSimWordsMax - 1 ? 0 : p->iPastPiMax + 1;
          }
          else
          {
              if ( p->iPatsPi && (p->iPatsPi & Period) == 0 )
                  Gia_ManBuiltInSimResimulate( p );
              if ( p->iPatsPi == 64 * p->nSimWords )
              {
                  Vec_Wrd_t * vTemp = Vec_WrdAlloc( 2 * Vec_WrdSize(p->vSims) ); 
                  word Data; int w, Count = 0, iObj = 0;
                  Vec_WrdForEachEntry( p->vSims, Data, w )
                  {
                      Vec_WrdPush( vTemp, Data );
                      if ( ++Count == p->nSimWords )
                      {
                          Gia_Obj_t * pObj = Gia_ManObj(p, iObj++);
                          if ( Gia_ObjIsCi(pObj) )
                              Vec_WrdPush( vTemp, Gia_ManRandomW(0) ); // Vec_WrdPush( vTemp, 0 );
                          else if ( Gia_ObjIsAnd(pObj) )
                              Vec_WrdPush( vTemp, pObj->fPhase ? ~(word)0 : 0 );
                          else
                              Vec_WrdPush( vTemp, 0 );
                          Count = 0;
                      }
                  }
                  assert( iObj == Gia_ManObjNum(p) );
                  Vec_WrdFree( p->vSims );
                  p->vSims = vTemp;
  
                  vTemp = Vec_WrdAlloc( 2 * Vec_WrdSize(p->vSimsPi) ); 
                  Count = 0;
                  Vec_WrdForEachEntry( p->vSimsPi, Data, w )
                  {
                      Vec_WrdPush( vTemp, Data );
                      if ( ++Count == p->nSimWords )
                      {
                          Vec_WrdPush( vTemp, 0 );
                          Count = 0;
                      }
                  }
                  Vec_WrdFree( p->vSimsPi );
                  p->vSimsPi = vTemp;
  
                  // update the word count
                  p->nSimWords++;
                  assert( Vec_WrdSize(p->vSims)   == p->nSimWords * Gia_ManObjNum(p) );
                  assert( Vec_WrdSize(p->vSimsPi) == p->nSimWords * Gia_ManCiNum(p)  );
                  //printf( "Resizing to %d words.\n", p->nSimWords );
              }
              iPat = p->iPatsPi++;
          }
      }
      assert( iPat >= 0 && iPat < p->iPatsPi );
      // add literals 
      if ( fOverflow )
      {
          int iVar;
          Vec_IntForEachEntry( &p->vSuppVars, iVar, k )
              if ( Abc_TtGetBit(Gia_ManBuiltInDataPi(p, iVar), iPat) )
                   Abc_TtXorBit(Gia_ManBuiltInDataPi(p, iVar), iPat);
          Vec_IntForEachEntry( vPat, iLit, k )
          {
              if ( Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat) == Abc_LitIsCompl(iLit) )
              Abc_TtXorBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat);
              Abc_TtXorBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), iPat);
          }
      }
      else
      {
          Vec_IntForEachEntry( vPat, iLit, k )
          {
              if ( Abc_TtGetBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), iPat) )
                  assert( Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat) != Abc_LitIsCompl(iLit) );
              else 
              {
                  if ( Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat) == Abc_LitIsCompl(iLit) )
                  Abc_TtXorBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat);
                  Abc_TtXorBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), iPat);
              }
          }
      }
      return 1;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Finds a satisfying assignment.]
  
    Description [Returns 1 if a sat assignment is found; 0 otherwise.]
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  int Gia_ManObjCheckSat_rec( Gia_Man_t * p, int iLit, Vec_Int_t * vObjs )
  {
      int iObj = Abc_Lit2Var(iLit);
      Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
      if ( pObj->fMark0 )
          return pObj->fMark1 == (unsigned)Abc_LitIsCompl(iLit);
      pObj->fMark0 = 1;
      pObj->fMark1 = Abc_LitIsCompl(iLit);
      Vec_IntPush( vObjs, iObj );
      if ( Gia_ObjIsAnd(pObj) )
      {
          if ( pObj->fMark1 == 0 ) // node value is 1
          {
              if ( !Gia_ManObjCheckSat_rec( p, Gia_ObjFaninLit0(pObj, iObj), vObjs ) )   return 0;
              if ( !Gia_ManObjCheckSat_rec( p, Gia_ObjFaninLit1(pObj, iObj), vObjs ) )   return 0;
          }
          else
          {
              if ( !Gia_ManObjCheckSat_rec( p, Abc_LitNot(Gia_ObjFaninLit0(pObj, iObj)), vObjs ) )   return 0;
          }
      }
      return 1;
  }
  int Gia_ManObjCheckOverlap1( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs )
  {
      Gia_Obj_t * pObj;
      int i, Res0, Res1 = 0;
  //    Gia_ManForEachObj( p, pObj, i )
  //        assert( pObj->fMark0 == 0 && pObj->fMark1 == 0 );
      Vec_IntClear( vObjs );
      Res0 = Gia_ManObjCheckSat_rec( p, iLit0, vObjs );
      if ( Res0 )
          Res1 = Gia_ManObjCheckSat_rec( p, iLit1, vObjs );
      Gia_ManForEachObjVec( vObjs, p, pObj, i )
          pObj->fMark0 = pObj->fMark1 = 0;
      return Res0 && Res1;
  }
  int Gia_ManObjCheckOverlap( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs )
  {
      if ( Gia_ManObjCheckOverlap1( p, iLit0, iLit1, vObjs ) )
          return 1;
      return Gia_ManObjCheckOverlap1( p, iLit1, iLit0, vObjs );
  }
  
  
  
  
  
  /**Function*************************************************************
  
    Synopsis    [Bit-parallel simulation during AIG construction.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Gia_ManIncrSimUpdate( Gia_Man_t * p )
  {
      int i, k;
      // extend timestamp info
      assert( Vec_IntSize(p->vTimeStamps) <= Gia_ManObjNum(p) );
      Vec_IntFillExtra( p->vTimeStamps, Gia_ManObjNum(p), 0 );
      // extend simulation info
      assert( Vec_WrdSize(p->vSims) <= Gia_ManObjNum(p) * p->nSimWords );
      Vec_WrdFillExtra( p->vSims,  Gia_ManObjNum(p) * p->nSimWords,  0 );
      // extend PI info
      assert( p->iNextPi <= Gia_ManCiNum(p) );
      for ( i = p->iNextPi; i < Gia_ManCiNum(p); i++ )
      {
          word * pSims = Gia_ManBuiltInData( p, Gia_ManCiIdToId(p, i) );
          for ( k = 0; k < p->nSimWords; k++ )
              pSims[k] = Gia_ManRandomW(0);
      }
      p->iNextPi = Gia_ManCiNum(p);
  }
  void Gia_ManIncrSimStart( Gia_Man_t * p, int nWords, int nObjs )
  {
      assert( !p->fIncrSim );
      p->fIncrSim  = 1;
      p->iPatsPi   = 0;
      p->nSimWords = nWords;
      // init time stamps
      p->iTimeStamp  = 1;
      p->vTimeStamps = Vec_IntAlloc( p->nSimWords );
      // init object sim info
      p->iNextPi = 0;       
      p->vSims   = Vec_WrdAlloc( p->nSimWords * nObjs );
      Gia_ManRandomW( 1 );
  }
  void Gia_ManIncrSimStop( Gia_Man_t * p )
  {
      assert( p->fIncrSim );
      p->fIncrSim   = 0;
      p->iPatsPi    = 0;
      p->nSimWords  = 0;
      p->iTimeStamp = 1;
      Vec_IntFreeP( &p->vTimeStamps );
      Vec_WrdFreeP( &p->vSims );
  }
  void Gia_ManIncrSimSet( Gia_Man_t * p, Vec_Int_t * vObjLits )
  {
      int i, iLit; 
      assert( Vec_IntSize(vObjLits) > 0 );
      p->iTimeStamp++;
      Vec_IntForEachEntry( vObjLits, iLit, i )
      {
          word * pSims = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit) );
          if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) )
              continue;
          //assert( Vec_IntEntry(p->vTimeStamps, Abc_Lit2Var(iLit)) == p->iTimeStamp-1 );
          Vec_IntWriteEntry(p->vTimeStamps, Abc_Lit2Var(iLit), p->iTimeStamp);
          if ( Abc_TtGetBit(pSims, p->iPatsPi) == Abc_LitIsCompl(iLit) )
               Abc_TtXorBit(pSims, p->iPatsPi);
      }
      p->iPatsPi = (p->iPatsPi == p->nSimWords * 64 - 1) ? 0 : p->iPatsPi + 1;
  }
  void Gia_ManIncrSimCone_rec( Gia_Man_t * p, int iObj )
  {
      Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
      if ( Gia_ObjIsCi(pObj) )
          return;
      if ( Vec_IntEntry(p->vTimeStamps, iObj) == p->iTimeStamp )
          return;
      assert( Vec_IntEntry(p->vTimeStamps, iObj) < p->iTimeStamp );
      Vec_IntWriteEntry( p->vTimeStamps, iObj, p->iTimeStamp );
      assert( Gia_ObjIsAnd(pObj) );
      Gia_ManIncrSimCone_rec( p, Gia_ObjFaninId0(pObj, iObj) );
      Gia_ManIncrSimCone_rec( p, Gia_ObjFaninId1(pObj, iObj) );
      Gia_ManBuiltInSimPerformInt( p, iObj );
  }
  int Gia_ManIncrSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 )
  {
      assert( iLit0 > 1 && iLit1 > 1 );
      Gia_ManIncrSimUpdate( p );
      Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) );
      Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) );
  //    return 0; // disable
      return Gia_ManBuiltInSimCheckOver( p, iLit0, iLit1 );
  }
  int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 )
  {
      assert( iLit0 > 1 && iLit1 > 1 );
      Gia_ManIncrSimUpdate( p );
      Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) );
      Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) );
  //    return 1; // disable
      return Gia_ManBuiltInSimCheckEqual( p, iLit0, iLit1 );
  }
  
  
  ////////////////////////////////////////////////////////////////////////
  ///                       END OF FILE                                ///
  ////////////////////////////////////////////////////////////////////////
  
  
  ABC_NAMESPACE_IMPL_END
  
  