text: /**CFile****************************************************************
  
    FileName    [seqInt.h]
  
    SystemName  [ABC: Logic synthesis and verification system.]
  
    PackageName [Construction and manipulation of sequential AIGs.]
  
    Synopsis    [Internal declarations.]
  
    Author      [Alan Mishchenko]
    
    Affiliation [UC Berkeley]
  
    Date        [Ver. 1.0. Started - June 20, 2005.]
  
    Revision    [$Id: seqInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
  
  ***********************************************************************/
   
  #ifndef __SEQ_INT_H__
  #define __SEQ_INT_H__
  
  #ifdef __cplusplus
  extern "C" {
  #endif
  
  ////////////////////////////////////////////////////////////////////////
  ///                          INCLUDES                                ///
  ////////////////////////////////////////////////////////////////////////
  
  #include "abc.h"
  #include "cut.h"
  #include "main.h"
  #include "mio.h"
  #include "mapper.h"
  #include "fpga.h"
  #include "seq.h"
  
  ////////////////////////////////////////////////////////////////////////
  ///                         PARAMETERS                               ///
  ////////////////////////////////////////////////////////////////////////
  
  #define SEQ_FULL_MASK        0xFFFFFFFF   
  
  // node status after updating its arrival time
  enum { SEQ_UPDATE_FAIL, SEQ_UPDATE_NO, SEQ_UPDATE_YES };
  
  ////////////////////////////////////////////////////////////////////////
  ///                         BASIC TYPES                              ///
  ////////////////////////////////////////////////////////////////////////
  
  // manager of sequential AIG
  struct Abc_Seq_t_
  {
      // sequential information
      Abc_Ntk_t *         pNtk;           // the network
      int                 nSize;          // the number of entries in all internal arrays
      Vec_Int_t *         vNums;          // the number of latches on each edge in the AIG
      Vec_Ptr_t *         vInits;         // the initial states for each edge in the AIG
      Extra_MmFixed_t *   pMmInits;       // memory manager for latch structures used to remember init states
      int                 fVerbose;       // the verbose flag
      float               fEpsilon;       // the accuracy for delay computation
      int                 fStandCells;    // the flag denoting standard cell mapping
      int                 nMaxIters;      // the max number of iterations
      int                 FiBestInt;      // the best clock period
      float               FiBestFloat;    // the best clock period
      // K-feasible cuts
      int                 nVarsMax;       // the max cut size
      Cut_Man_t *         pCutMan;        // cut manager
      Map_SuperLib_t *    pSuperLib;      // the current supergate library
      // sequential arrival time computation
      Vec_Int_t *         vAFlows;        // the area flow of each cut
      Vec_Int_t *         vLValues;       // the arrival times (L-Values of nodes)
      Vec_Int_t *         vLValuesN;      // the arrival times (L-Values of nodes)
      Vec_Str_t *         vLags;          // the lags of the mapped nodes
      Vec_Str_t *         vLagsN;         // the lags of the mapped nodes
      Vec_Str_t *         vUses;          // the phase usage
      // representation of the mapping
      Vec_Ptr_t *         vMapAnds;       // nodes visible in the mapping 
      Vec_Vec_t *         vMapCuts;       // best cuts for each node 
      Vec_Vec_t *         vMapDelays;     // the delay of each fanin
      Vec_Vec_t *         vMapFanins;     // the delay of each fanin
      // runtime stats
      int                 timeCuts;       // runtime to compute the cuts
      int                 timeDelay;      // runtime to compute the L-values
      int                 timeRet;        // runtime to retime the resulting network
      int                 timeNtk;        // runtime to create the final network
  
  };
  
  // data structure to store initial state
  typedef struct Seq_Lat_t_  Seq_Lat_t;
  struct Seq_Lat_t_
  {
      Seq_Lat_t *         pNext;          // the next Lat in the ring
      Seq_Lat_t *         pPrev;          // the prev Lat in the ring 
      Abc_Obj_t *         pLatch;         // the real latch corresponding to Lat
  };
  
  // representation of latch on the edge
  typedef struct Seq_RetEdge_t_       Seq_RetEdge_t;   
  struct Seq_RetEdge_t_ // 1 word
  {
      unsigned            iNode    : 24;  // the ID of the node
      unsigned            iEdge    :  1;  // the edge of the node
      unsigned            iLatch   :  7;  // the latch number counting from the node
  };
  
  // representation of one retiming step
  typedef struct Seq_RetStep_t_       Seq_RetStep_t;   
  struct Seq_RetStep_t_ // 1 word
  {
      unsigned            iNode    : 24;  // the ID of the node
      unsigned            nLatches :  8;  // the number of latches to retime
  };
  
  // representation of one mapping match
  typedef struct Seq_Match_t_       Seq_Match_t;   
  struct Seq_Match_t_ // 3 words
  {
      Abc_Obj_t *         pAnd;           // the AND gate used in the mapping
      Cut_Cut_t *         pCut;           // the cut used to map it
      Map_Super_t *       pSuper;         // the supergate used to implement the cut
      unsigned            fCompl  :  1;   // the polarity of the AND gate
      unsigned            fCutInv :  1;   // the polarity of the cut
      unsigned            PolUse  :  2;   // the polarity use of this node
      unsigned            uPhase  : 14;   // the phase assignment at the boundary
      unsigned            uPhaseR : 14;   // the real phase assignment at the boundary
  };
  
  ////////////////////////////////////////////////////////////////////////
  ///                      MACRO DEFINITIONS                           ///
  ////////////////////////////////////////////////////////////////////////
  
  // transforming retedges into ints and back
  static inline int            Seq_RetEdge2Int( Seq_RetEdge_t Val )  { return *((int *)&Val);           }
  static inline Seq_RetEdge_t  Seq_Int2RetEdge( int Num )            { return *((Seq_RetEdge_t *)&Num); }
  // transforming retsteps into ints and back
  static inline int            Seq_RetStep2Int( Seq_RetStep_t Val )  { return *((int *)&Val);           }
  static inline Seq_RetStep_t  Seq_Int2RetStep( int Num )            { return *((Seq_RetStep_t *)&Num); }
  
  // manipulating the number of latches on each edge
  static inline Vec_Int_t *    Seq_ObjLNums( Abc_Obj_t * pObj )                        { return ((Abc_Seq_t*)pObj->pNtk->pManFunc)->vNums;                    }
  static inline int            Seq_ObjFaninL( Abc_Obj_t * pObj, int i )                { return Vec_IntEntry(Seq_ObjLNums(pObj), 2*pObj->Id + i);             }
  static inline int            Seq_ObjFaninL0( Abc_Obj_t * pObj )                      { return Vec_IntEntry(Seq_ObjLNums(pObj), 2*pObj->Id + 0);             }
  static inline int            Seq_ObjFaninL1( Abc_Obj_t * pObj )                      { return Vec_IntEntry(Seq_ObjLNums(pObj), 2*pObj->Id + 1);             }
  static inline void           Seq_ObjSetFaninL( Abc_Obj_t * pObj, int i, int nLats )  { Vec_IntWriteEntry(Seq_ObjLNums(pObj), 2*pObj->Id + i, nLats);        }
  static inline void           Seq_ObjSetFaninL0( Abc_Obj_t * pObj, int nLats )        { Vec_IntWriteEntry(Seq_ObjLNums(pObj), 2*pObj->Id + 0, nLats);        }
  static inline void           Seq_ObjSetFaninL1( Abc_Obj_t * pObj, int nLats )        { Vec_IntWriteEntry(Seq_ObjLNums(pObj), 2*pObj->Id + 1, nLats);        }
  static inline void           Seq_ObjAddFaninL( Abc_Obj_t * pObj, int i, int nLats )  { Vec_IntAddToEntry(Seq_ObjLNums(pObj), 2*pObj->Id + i, nLats);        }
  static inline void           Seq_ObjAddFaninL0( Abc_Obj_t * pObj, int nLats )        { Vec_IntAddToEntry(Seq_ObjLNums(pObj), 2*pObj->Id + 0, nLats);        }
  static inline void           Seq_ObjAddFaninL1( Abc_Obj_t * pObj, int nLats )        { Vec_IntAddToEntry(Seq_ObjLNums(pObj), 2*pObj->Id + 1, nLats);        }
  static inline int            Seq_ObjFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) { return Seq_ObjFaninL( pFanout, Abc_ObjFanoutEdgeNum(pObj,pFanout) ); }
  static inline void           Seq_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats ) {  Seq_ObjSetFaninL( pFanout, Abc_ObjFanoutEdgeNum(pObj,pFanout), nLats );  }
  static inline void           Seq_ObjAddFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats ) {  Seq_ObjAddFaninL( pFanout, Abc_ObjFanoutEdgeNum(pObj,pFanout), nLats );  }
  static inline int            Seq_ObjFaninLMin( Abc_Obj_t * pObj )                    {  assert( Abc_ObjIsNode(pObj) ); return ABC_MIN( Seq_ObjFaninL0(pObj), Seq_ObjFaninL1(pObj) ); }
  static inline int            Seq_ObjFaninLMax( Abc_Obj_t * pObj )                    {  assert( Abc_ObjIsNode(pObj) ); return ABC_MAX( Seq_ObjFaninL0(pObj), Seq_ObjFaninL1(pObj) ); }
  
  // reading l-values and lags
  static inline Vec_Int_t *    Seq_NodeLValues( Abc_Obj_t * pNode )                    { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLValues;           }
  static inline Vec_Int_t *    Seq_NodeLValuesN( Abc_Obj_t * pNode )                   { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLValuesN;          }
  static inline int            Seq_NodeGetLValue( Abc_Obj_t * pNode )                  { return Vec_IntEntry( Seq_NodeLValues(pNode), (pNode)->Id );        }
  static inline void           Seq_NodeSetLValue( Abc_Obj_t * pNode, int Value )       { Vec_IntWriteEntry( Seq_NodeLValues(pNode), (pNode)->Id, Value );   }
  static inline float          Seq_NodeGetLValueP( Abc_Obj_t * pNode )                 { return Abc_Int2Float( Vec_IntEntry( Seq_NodeLValues(pNode), (pNode)->Id ) );        }
  static inline float          Seq_NodeGetLValueN( Abc_Obj_t * pNode )                 { return Abc_Int2Float( Vec_IntEntry( Seq_NodeLValuesN(pNode), (pNode)->Id ) );       }
  static inline void           Seq_NodeSetLValueP( Abc_Obj_t * pNode, float Value )    { Vec_IntWriteEntry( Seq_NodeLValues(pNode), (pNode)->Id, Abc_Float2Int(Value) );     }
  static inline void           Seq_NodeSetLValueN( Abc_Obj_t * pNode, float Value )    { Vec_IntWriteEntry( Seq_NodeLValuesN(pNode), (pNode)->Id, Abc_Float2Int(Value) );    }
  
  // reading area flows
  static inline Vec_Int_t *    Seq_NodeFlow( Abc_Obj_t * pNode )                       { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vAFlows;                        }
  static inline float          Seq_NodeGetFlow( Abc_Obj_t * pNode )                    { return Abc_Int2Float( Vec_IntEntry( Seq_NodeFlow(pNode), (pNode)->Id ) );      }
  static inline void           Seq_NodeSetFlow( Abc_Obj_t * pNode, float Value )       { Vec_IntWriteEntry( Seq_NodeFlow(pNode), (pNode)->Id, Abc_Float2Int(Value) );   }
  
  // reading the contents of the lat
  static inline Abc_InitType_t Seq_LatInit( Seq_Lat_t * pLat )  { return ((unsigned)pLat->pPrev) & 3;                                 }
  static inline Seq_Lat_t *    Seq_LatNext( Seq_Lat_t * pLat )  { return pLat->pNext;                                                 }
  static inline Seq_Lat_t *    Seq_LatPrev( Seq_Lat_t * pLat )  { return (void *)(((unsigned)pLat->pPrev) & (SEQ_FULL_MASK << 2));    }
  
  // setting the contents of the lat
  static inline void           Seq_LatSetInit( Seq_Lat_t * pLat, Abc_InitType_t Init )  { pLat->pPrev = (void *)( (3 & Init) | (((unsigned)pLat->pPrev) & (SEQ_FULL_MASK << 2)) );    }
  static inline void           Seq_LatSetNext( Seq_Lat_t * pLat, Seq_Lat_t * pNext )    { pLat->pNext = pNext;                                                                        }
  static inline void           Seq_LatSetPrev( Seq_Lat_t * pLat, Seq_Lat_t * pPrev )    { Abc_InitType_t Init = Seq_LatInit(pLat);  pLat->pPrev = pPrev;  Seq_LatSetInit(pLat, Init); }
  
  // accessing retiming lags
  static inline Cut_Man_t *    Seq_NodeCutMan( Abc_Obj_t * pNode )                      { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->pCutMan;                 }
  static inline Vec_Str_t *    Seq_NodeLags( Abc_Obj_t * pNode )                        { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLags;            }
  static inline Vec_Str_t *    Seq_NodeLagsN( Abc_Obj_t * pNode )                       { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLagsN;           }
  static inline char           Seq_NodeGetLag( Abc_Obj_t * pNode )                      { return Vec_StrEntry( Seq_NodeLags(pNode), (pNode)->Id );         }
  static inline char           Seq_NodeGetLagN( Abc_Obj_t * pNode )                     { return Vec_StrEntry( Seq_NodeLagsN(pNode), (pNode)->Id );        }
  static inline void           Seq_NodeSetLag( Abc_Obj_t * pNode, char Value )          { Vec_StrWriteEntry( Seq_NodeLags(pNode), (pNode)->Id, (Value) );  }
  static inline void           Seq_NodeSetLagN( Abc_Obj_t * pNode, char Value )         { Vec_StrWriteEntry( Seq_NodeLagsN(pNode), (pNode)->Id, (Value) ); }
  static inline int            Seq_NodeComputeLag( int LValue, int Fi )                 { return (LValue + 1024*Fi)/Fi - 1024 - (int)(LValue % Fi == 0);     }
  static inline int            Seq_NodeComputeLagFloat( float LValue, float Fi )        { return ((int)ceil(LValue/Fi)) - 1;                                        }
  
  // phase usage
  static inline Vec_Str_t *    Seq_NodeUses( Abc_Obj_t * pNode )                        { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vUses;            }
  static inline char           Seq_NodeGetUses( Abc_Obj_t * pNode )                     { return Vec_StrEntry( Seq_NodeUses(pNode), (pNode)->Id );         }
  static inline void           Seq_NodeSetUses( Abc_Obj_t * pNode, char Value )         { Vec_StrWriteEntry( Seq_NodeUses(pNode), (pNode)->Id, (Value) );  }
  
  // accessing initial states
  static inline Vec_Ptr_t *    Seq_NodeLats( Abc_Obj_t * pObj )                                { return ((Abc_Seq_t*)pObj->pNtk->pManFunc)->vInits;                                           }
  static inline Seq_Lat_t *    Seq_NodeGetRing( Abc_Obj_t * pObj, int Edge )                   { return Vec_PtrEntry( Seq_NodeLats(pObj), (pObj->Id<<1)+Edge );                               }
  static inline void           Seq_NodeSetRing( Abc_Obj_t * pObj, int Edge, Seq_Lat_t * pLat ) { Vec_PtrWriteEntry( Seq_NodeLats(pObj), (pObj->Id<<1)+Edge, pLat );                           }
  static inline Seq_Lat_t *    Seq_NodeCreateLat( Abc_Obj_t * pObj )                           { Seq_Lat_t * p = (Seq_Lat_t *)Extra_MmFixedEntryFetch( ((Abc_Seq_t*)pObj->pNtk->pManFunc)->pMmInits ); p->pNext = p->pPrev = NULL; p->pLatch = NULL; return p; }
  static inline void           Seq_NodeRecycleLat( Abc_Obj_t * pObj, Seq_Lat_t * pLat )        { Extra_MmFixedEntryRecycle( ((Abc_Seq_t*)pObj->pNtk->pManFunc)->pMmInits, (char *)pLat );     }
  
  // getting hold of the structure storing initial states of the latches
  static inline Seq_Lat_t *    Seq_NodeGetLatFirst( Abc_Obj_t * pObj, int Edge )               { return Seq_NodeGetRing(pObj, Edge);                      }
  static inline Seq_Lat_t *    Seq_NodeGetLatLast( Abc_Obj_t * pObj, int Edge )                { return Seq_LatPrev( Seq_NodeGetRing(pObj, Edge) );       }
  static inline Seq_Lat_t *    Seq_NodeGetLat( Abc_Obj_t * pObj, int Edge, int iLat )          { int c; Seq_Lat_t * pLat = Seq_NodeGetRing(pObj, Edge); for ( c = 0; c != iLat; c++ ) pLat = pLat->pNext; return pLat; }
  static inline int            Seq_NodeCountLats( Abc_Obj_t * pObj, int Edge )                 { int c; Seq_Lat_t * pLat, * pRing = Seq_NodeGetRing(pObj, Edge); if ( pRing == NULL ) return 0; for ( c = 0, pLat = pRing; !c || pLat != pRing; c++ )  pLat = pLat->pNext; return c; }
  static inline void           Seq_NodeCleanLats( Abc_Obj_t * pObj, int Edge )                 { int c; Seq_Lat_t * pLat, * pRing = Seq_NodeGetRing(pObj, Edge); if ( pRing == NULL ) return  ; for ( c = 0, pLat = pRing; !c || pLat != pRing; c++ )  pLat->pLatch = NULL, pLat = pLat->pNext; return;  }
  
  // getting/setting initial states of the latches
  static inline Abc_InitType_t Seq_NodeGetInitOne( Abc_Obj_t * pObj, int Edge, int iLat )      { return Seq_LatInit( Seq_NodeGetLat(pObj, Edge, iLat) );  }
  static inline Abc_InitType_t Seq_NodeGetInitFirst( Abc_Obj_t * pObj, int Edge )              { return Seq_LatInit( Seq_NodeGetLatFirst(pObj, Edge) );   }
  static inline Abc_InitType_t Seq_NodeGetInitLast( Abc_Obj_t * pObj, int Edge )               { return Seq_LatInit( Seq_NodeGetLatLast(pObj, Edge) );    }
  static inline void           Seq_NodeSetInitOne( Abc_Obj_t * pObj, int Edge, int iLat, Abc_InitType_t Init )  { Seq_LatSetInit( Seq_NodeGetLat(pObj, Edge, iLat), Init );  }
  
  ////////////////////////////////////////////////////////////////////////
  ///                    FUNCTION DECLARATIONS                         ///
  ////////////////////////////////////////////////////////////////////////
  
  /*=== seqAigIter.c =============================================================*/
  extern int                   Seq_AigRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose );
  extern int                   Seq_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags, int fVerbose );
  /*=== seqFpgaIter.c ============================================================*/
  extern int                   Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose );
  extern int                   Seq_FpgaNodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
  /*=== seqMapIter.c ============================================================*/
  extern int                   Seq_MapRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose );
  /*=== seqRetIter.c =============================================================*/
  extern int                   Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose );
  /*=== seqLatch.c ===============================================================*/
  extern void                  Seq_NodeInsertFirst( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init );  
  extern void                  Seq_NodeInsertLast( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init );  
  extern Abc_InitType_t        Seq_NodeDeleteFirst( Abc_Obj_t * pObj, int Edge );  
  extern Abc_InitType_t        Seq_NodeDeleteLast( Abc_Obj_t * pObj, int Edge );  
  /*=== seqUtil.c ================================================================*/
  extern int                   Seq_NtkLevelMax( Abc_Ntk_t * pNtk );
  extern int                   Seq_ObjFanoutLMax( Abc_Obj_t * pObj );
  extern int                   Seq_ObjFanoutLMin( Abc_Obj_t * pObj );
  extern int                   Seq_ObjFanoutLSum( Abc_Obj_t * pObj );
  extern int                   Seq_ObjFaninLSum( Abc_Obj_t * pObj );
  
  #ifdef __cplusplus
  }
  #endif
  
  #endif
  
  ////////////////////////////////////////////////////////////////////////
  ///                       END OF FILE                                ///
  ////////////////////////////////////////////////////////////////////////
  
  