Version abc71001

17 files changed, 7089 insertions, 0 deletions

diff --git a/src/base/seq/module.make b/src/base/seq/module.make
new file mode 100644
index 00000000..c7716180
--- /dev/null
+++ b/src/base/seq/module.make
@@ -0,0 +1,14 @@
+SRC +=    src/base/seq/seqAigCore.c \
+    src/base/seq/seqAigIter.c \
+    src/base/seq/seqCreate.c \
+    src/base/seq/seqFpgaCore.c \
+    src/base/seq/seqFpgaIter.c \
+    src/base/seq/seqLatch.c \
+    src/base/seq/seqMan.c \
+    src/base/seq/seqMapCore.c \
+    src/base/seq/seqMapIter.c \
+    src/base/seq/seqMaxMeanCycle.c \
+    src/base/seq/seqRetCore.c \
+    src/base/seq/seqRetIter.c \
+    src/base/seq/seqShare.c \
+    src/base/seq/seqUtil.c
diff --git a/src/base/seq/seq.h b/src/base/seq/seq.h
new file mode 100644
index 00000000..d3c9abda
--- /dev/null
+++ b/src/base/seq/seq.h
@@ -0,0 +1,101 @@
+/**CFile****************************************************************
+
+  FileName    [seq.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seq.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __SEQ_H__
+#define __SEQ_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Abc_Seq_t_  Abc_Seq_t;
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== seqAigCore.c ===========================================================*/
+extern void            Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose );
+extern void            Seq_NtkSeqRetimeForward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose );
+extern void            Seq_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose );
+/*=== seqFpgaCore.c ===============================================================*/
+extern Abc_Ntk_t *     Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
+/*=== seqMapCore.c ===============================================================*/
+extern Abc_Ntk_t *     Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
+/*=== seqRetCore.c ===========================================================*/
+extern Abc_Ntk_t *     Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose );
+/*=== seqLatch.c ===============================================================*/
+extern void            Seq_NodeDupLats( Abc_Obj_t * pObjNew, Abc_Obj_t * pObj, int Edge );
+extern int             Seq_NodeCompareLats( Abc_Obj_t * pObj1, int Edge1, Abc_Obj_t * pObj2, int Edge2 );
+/*=== seqMan.c ===============================================================*/
+extern Abc_Seq_t *     Seq_Create( Abc_Ntk_t * pNtk );
+extern void            Seq_Resize( Abc_Seq_t * p, int nMaxId );
+extern void            Seq_Delete( Abc_Seq_t * p );
+/*=== seqMaxMeanCycle.c ======================================================*/
+extern float           Seq_NtkHoward( Abc_Ntk_t * pNtk, int fVerbose );
+extern void            Seq_NtkSkewForward( Abc_Ntk_t * pNtk, float period, int fMinimize );
+/*=== abcSeq.c ===============================================================*/
+extern Abc_Ntk_t *     Abc_NtkAigToSeq( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *     Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk );
+extern bool            Abc_NtkSeqCheck( Abc_Ntk_t * pNtk ); 
+/*=== seqShare.c =============================================================*/
+extern void            Seq_NtkShareFanouts( Abc_Ntk_t * pNtk );
+extern void            Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk );
+extern void            Seq_NtkShareLatchesMapping( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds, int fFpga );
+extern void            Seq_NtkShareLatchesClean( Abc_Ntk_t * pNtk );
+/*=== seqUtil.c ==============================================================*/
+extern char *          Seq_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge );
+extern void            Seq_NtkLatchSetValues( Abc_Ntk_t * pNtk, Abc_InitType_t Init );
+extern int             Seq_NtkLatchNum( Abc_Ntk_t * pNtk );
+extern int             Seq_NtkLatchNumMax( Abc_Ntk_t * pNtk );
+extern int             Seq_NtkLatchNumShared( Abc_Ntk_t * pNtk );
+extern void            Seq_NtkLatchGetInitNums( Abc_Ntk_t * pNtk, int * pInits );
+extern int             Seq_NtkLatchGetEqualFaninNum( Abc_Ntk_t * pNtk );
+extern int             Seq_NtkCountNodesAboveLimit( Abc_Ntk_t * pNtk, int Limit );
+extern int             Seq_MapComputeAreaFlows( Abc_Ntk_t * pNtk, int fVerbose );
+extern Vec_Ptr_t *     Seq_NtkReachNodes( Abc_Ntk_t * pNtk, int fFromPos );
+extern int             Seq_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c
new file mode 100644
index 00000000..42fa14a2
--- /dev/null
+++ b/src/base/seq/seqAigCore.c
@@ -0,0 +1,977 @@
+/**CFile****************************************************************
+
+  FileName    [seqRetCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [The core of retiming procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqRetCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+/* 
+    Retiming can be represented in three equivalent forms:
+    - as a set of integer lags for each node (array of chars by node ID)
+    - as a set of node numbers with lag for each, fwd and bwd (two arrays of Seq_RetStep_t_)
+    - as a set of latch moves over the nodes, fwd and bwd (two arrays of node pointers Abc_Obj_t *)
+*/
+
+static void        Abc_ObjRetimeForward( Abc_Obj_t * pObj );
+static int         Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtk, stmm_table * tTable, Vec_Int_t * vValues );
+static void        Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable );
+static void        Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel );
+
+static void        Seq_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves );
+static int         Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int fVerbose );
+static void        Abc_ObjRetimeForward( Abc_Obj_t * pObj );
+static int         Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtk, stmm_table * tTable, Vec_Int_t * vValues );
+static void        Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable );
+static void        Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel );
+
+static Vec_Ptr_t * Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward );
+static Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, bool fForward );
+static Vec_Int_t * Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward );
+static void        Abc_ObjRetimeForwardTry( Abc_Obj_t * pObj, int nLatches );  
+static void        Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches );
+  
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs performs optimal delay retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    int RetValue;
+    if ( !fInitial )
+        Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC );
+    // get the retiming lags
+    p->nMaxIters = nMaxIters;
+    if ( !Seq_AigRetimeDelayLags( pNtk, fVerbose ) )
+        return;
+    // implement this retiming
+    RetValue = Seq_NtkImplementRetiming( pNtk, p->vLags, fVerbose );
+    if ( RetValue == 0 )
+        printf( "Retiming completed but initial state computation has failed.\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs most forward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkSeqRetimeForward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose )
+{
+    Vec_Ptr_t * vMoves;
+    Abc_Obj_t * pNode;
+    int i;
+    if ( !fInitial )
+        Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC );
+    // get the forward moves
+    vMoves = Abc_NtkUtilRetimingTry( pNtk, 1 );
+    // undo the forward moves
+    Vec_PtrForEachEntryReverse( vMoves, pNode, i )
+        Abc_ObjRetimeBackwardTry( pNode, 1 );
+    // implement this forward retiming
+    Seq_NtkImplementRetimingForward( pNtk, vMoves );
+    Vec_PtrFree( vMoves ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs most backward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose )
+{
+    Vec_Ptr_t * vMoves;
+    Abc_Obj_t * pNode;
+    int i, RetValue;
+    if ( !fInitial )
+        Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC );
+    // get the backward moves
+    vMoves = Abc_NtkUtilRetimingTry( pNtk, 0 );
+    // undo the backward moves
+    Vec_PtrForEachEntryReverse( vMoves, pNode, i )
+        Abc_ObjRetimeForwardTry( pNode, 1 );
+    // implement this backward retiming
+    RetValue = Seq_NtkImplementRetimingBackward( pNtk, vMoves, fVerbose );
+    Vec_PtrFree( vMoves ); 
+    if ( RetValue == 0 )
+        printf( "Retiming completed but initial state computation has failed.\n" );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the retiming on the sequential AIG.]
+
+  Description [Split the retiming into forward and backward.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags, int fVerbose )
+{
+    Vec_Int_t * vSteps;
+    Vec_Ptr_t * vMoves;
+    int RetValue;
+
+    // forward retiming
+    vSteps = Abc_NtkUtilRetimingSplit( vLags, 1 );
+    // translate each set of steps into moves
+    if ( fVerbose )
+    printf( "The number of forward steps  = %6d.\n", Vec_IntSize(vSteps) );
+    vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 1 );
+    if ( fVerbose )
+    printf( "The number of forward moves  = %6d.\n", Vec_PtrSize(vMoves) );
+    // implement this retiming
+    Seq_NtkImplementRetimingForward( pNtk, vMoves );
+    Vec_IntFree( vSteps );
+    Vec_PtrFree( vMoves );
+
+    // backward retiming
+    vSteps = Abc_NtkUtilRetimingSplit( vLags, 0 );
+    // translate each set of steps into moves
+    if ( fVerbose )
+    printf( "The number of backward steps = %6d.\n", Vec_IntSize(vSteps) );
+    vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 0 );
+    if ( fVerbose )
+    printf( "The number of backward moves = %6d.\n", Vec_PtrSize(vMoves) );
+    // implement this retiming
+    RetValue = Seq_NtkImplementRetimingBackward( pNtk, vMoves, fVerbose );
+    Vec_IntFree( vSteps );
+    Vec_PtrFree( vMoves );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the given retiming on the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    Vec_PtrForEachEntry( vMoves, pNode, i )
+        Abc_ObjRetimeForward( pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retimes node forward by one latch.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjRetimeForward( Abc_Obj_t * pObj )  
+{
+    Abc_Obj_t * pFanout;
+    int Init0, Init1, Init, i;
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    assert( Seq_ObjFaninL0(pObj) >= 1 );
+    assert( Seq_ObjFaninL1(pObj) >= 1 );
+    // remove the init values from the fanins
+    Init0 = Seq_NodeDeleteFirst( pObj, 0 ); 
+    Init1 = Seq_NodeDeleteFirst( pObj, 1 );
+    assert( Init0 != ABC_INIT_NONE );
+    assert( Init1 != ABC_INIT_NONE );
+    // take into account the complements in the node
+    if ( Abc_ObjFaninC0(pObj) )
+    {
+        if ( Init0 == ABC_INIT_ZERO )
+            Init0 = ABC_INIT_ONE;
+        else if ( Init0 == ABC_INIT_ONE )
+            Init0 = ABC_INIT_ZERO;
+    }
+    if ( Abc_ObjFaninC1(pObj) )
+    {
+        if ( Init1 == ABC_INIT_ZERO )
+            Init1 = ABC_INIT_ONE;
+        else if ( Init1 == ABC_INIT_ONE )
+            Init1 = ABC_INIT_ZERO;
+    }
+    // compute the value at the output of the node
+    if ( Init0 == ABC_INIT_ZERO || Init1 == ABC_INIT_ZERO )
+        Init = ABC_INIT_ZERO;
+    else if ( Init0 == ABC_INIT_ONE && Init1 == ABC_INIT_ONE )
+        Init = ABC_INIT_ONE;
+    else
+        Init = ABC_INIT_DC;
+
+    // make sure the label is clean
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        assert( pFanout->fMarkC == 0 );
+    // add the init values to the fanouts
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        if ( pFanout->fMarkC )
+            continue;
+        pFanout->fMarkC = 1;
+        if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) )
+            Seq_NodeInsertLast( pFanout, Abc_ObjFanoutEdgeNum(pObj, pFanout), Init );
+        else
+        {
+            assert( Abc_ObjFanin0(pFanout) == pObj );
+            Seq_NodeInsertLast( pFanout, 0, Init );
+            Seq_NodeInsertLast( pFanout, 1, Init );
+        }
+    }
+    // clean the label
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        pFanout->fMarkC = 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the given retiming on the sequential AIG.]
+
+  Description [Returns 0 of initial state computation fails.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int fVerbose )
+{
+    Seq_RetEdge_t RetEdge;
+    stmm_table * tTable;
+    stmm_generator * gen;
+    Vec_Int_t * vValues;
+    Abc_Ntk_t * pNtkProb, * pNtkMiter, * pNtkCnf;
+    Abc_Obj_t * pNode, * pNodeNew;
+    int * pModel, RetValue, i, clk;
+
+    // return if the retiming is trivial
+    if ( Vec_PtrSize(vMoves) == 0 )
+        return 1;
+
+    // create the network for the initial state computation
+    // start the table and the array of PO values
+    pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+    tTable   = stmm_init_table( stmm_numcmp, stmm_numhash );
+    vValues  = Vec_IntAlloc( 100 );
+
+    // perform the backward moves and build the network for initial state computation
+    RetValue = 0;
+    Vec_PtrForEachEntry( vMoves, pNode, i )
+        RetValue |= Abc_ObjRetimeBackward( pNode, pNtkProb, tTable, vValues );
+
+    // add the PIs corresponding to the white spots
+    stmm_foreach_item( tTable, gen, (char **)&RetEdge, (char **)&pNodeNew )
+        Abc_ObjAddFanin( pNodeNew, Abc_NtkCreatePi(pNtkProb) );
+
+    // add the PI/PO names
+    Abc_NtkAddDummyPiNames( pNtkProb );
+    Abc_NtkAddDummyPoNames( pNtkProb );
+    Abc_NtkAddDummyAssertNames( pNtkProb );
+
+    // make sure everything is okay with the network structure
+    if ( !Abc_NtkDoCheck( pNtkProb ) )
+    {
+        printf( "Seq_NtkImplementRetimingBackward: The internal network check has failed.\n" );
+        Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL );
+        Abc_NtkDelete( pNtkProb );
+        stmm_free_table( tTable );
+        Vec_IntFree( vValues );
+        return 0;
+    }
+
+    // check if conflict is found
+    if ( RetValue )
+    {
+        printf( "Seq_NtkImplementRetimingBackward: A top level conflict is detected. DC latch values are used.\n" );
+        Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL );
+        Abc_NtkDelete( pNtkProb );
+        stmm_free_table( tTable );
+        Vec_IntFree( vValues );
+        return 0;
+    }
+
+    // get the miter cone
+    pNtkMiter = Abc_NtkCreateTarget( pNtkProb, pNtkProb->vCos, vValues );
+    Abc_NtkDelete( pNtkProb );
+    Vec_IntFree( vValues );
+
+    if ( fVerbose )
+    printf( "The number of ANDs in the AIG = %5d.\n", Abc_NtkNodeNum(pNtkMiter) );
+
+    // transform the miter into a logic network for efficient CNF construction
+//    pNtkCnf = Abc_Ntk_Renode( pNtkMiter, 0, 100, 1, 0, 0 );
+//    Abc_NtkDelete( pNtkMiter );
+    pNtkCnf = pNtkMiter;
+
+    // solve the miter
+clk = clock();
+//    RetValue = Abc_NtkMiterSat_OldAndRusty( pNtkCnf, 30, 0 );
+    RetValue = Abc_NtkMiterSat( pNtkCnf, (sint64)500000, (sint64)50000000, 0, 0, NULL, NULL );
+if ( fVerbose )
+if ( clock() - clk > 100 )
+{
+PRT( "SAT solving time", clock() - clk );
+}
+    pModel = pNtkCnf->pModel;  pNtkCnf->pModel = NULL;
+    Abc_NtkDelete( pNtkCnf );
+
+    // analyze the result
+    if ( RetValue == -1 || RetValue == 1 )
+    {
+        Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL );
+        if ( RetValue == 1 )
+            printf( "Seq_NtkImplementRetimingBackward: The problem is unsatisfiable. DC latch values are used.\n" );
+        else
+            printf( "Seq_NtkImplementRetimingBackward: The SAT problem timed out. DC latch values are used.\n" );
+        stmm_free_table( tTable );
+        return 0;
+    }
+
+    // set the values of the latches
+    Abc_NtkRetimeSetInitialValues( pNtk, tTable, pModel );
+    stmm_free_table( tTable );
+    free( pModel );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retimes node backward by one latch.]
+
+  Description [Constructs the problem for initial state computation.
+  Returns 1 if the conflict is found.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * tTable, Vec_Int_t * vValues )  
+{
+    Abc_Obj_t * pFanout;
+    Abc_InitType_t Init, Value;
+    Seq_RetEdge_t RetEdge;
+    Abc_Obj_t * pNodeNew, * pFanoutNew, * pBuffer;
+    int i, Edge, fMet0, fMet1, fMetN;
+
+    // make sure the node can be retimed
+    assert( Seq_ObjFanoutLMin(pObj) > 0 );
+    // get the fanout values
+    fMet0 = fMet1 = fMetN = 0;
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        if ( Abc_ObjFaninId0(pFanout) == pObj->Id )
+        {
+            Init = Seq_NodeGetInitLast( pFanout, 0 );
+            if ( Init == ABC_INIT_ZERO )
+                fMet0 = 1;
+            else if ( Init == ABC_INIT_ONE )
+                fMet1 = 1;
+            else if ( Init == ABC_INIT_NONE )
+                fMetN = 1;
+        }
+        if ( Abc_ObjFaninId1(pFanout) == pObj->Id )
+        {
+            Init = Seq_NodeGetInitLast( pFanout, 1 );
+            if ( Init == ABC_INIT_ZERO )
+                fMet0 = 1;
+            else if ( Init == ABC_INIT_ONE )
+                fMet1 = 1;
+            else if ( Init == ABC_INIT_NONE )
+                fMetN = 1;
+        }
+    }
+
+    // consider the case when all fanout latches have don't-care values
+    // the new values on the fanin edges will be don't-cares
+    if ( !fMet0 && !fMet1 && !fMetN )
+    {
+        // make sure the label is clean
+        Abc_ObjForEachFanout( pObj, pFanout, i )
+            assert( pFanout->fMarkC == 0 );
+        // update the fanout edges
+        Abc_ObjForEachFanout( pObj, pFanout, i )
+        {
+            if ( pFanout->fMarkC )
+                continue;
+            pFanout->fMarkC = 1;
+            if ( Abc_ObjFaninId0(pFanout) == pObj->Id )
+                Seq_NodeDeleteLast( pFanout, 0 );
+            if ( Abc_ObjFaninId1(pFanout) == pObj->Id )
+                Seq_NodeDeleteLast( pFanout, 1 );
+        }
+        // clean the label
+        Abc_ObjForEachFanout( pObj, pFanout, i )
+            pFanout->fMarkC = 0;
+        // update the fanin edges
+        Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable );
+        Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable );
+        Seq_NodeInsertFirst( pObj, 0, ABC_INIT_DC );
+        Seq_NodeInsertFirst( pObj, 1, ABC_INIT_DC );
+        return 0;
+    }
+    // the initial values on the fanout edges contain 0, 1, or unknown
+    // the new values on the fanin edges will be unknown
+
+    // add new AND-gate to the network
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    pNodeNew->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+
+    // add PO fanouts if any
+    if ( fMet0 )
+    {
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
+        Vec_IntPush( vValues, 0 );
+    }
+    if ( fMet1 )
+    {
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
+        Vec_IntPush( vValues, 1 );
+    }
+
+    // make sure the label is clean
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        assert( pFanout->fMarkC == 0 );
+    // perform the changes
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        if ( pFanout->fMarkC )
+            continue;
+        pFanout->fMarkC = 1;
+        if ( Abc_ObjFaninId0(pFanout) == pObj->Id )
+        {
+            Edge = 0;
+            Value = Seq_NodeDeleteLast( pFanout, Edge );
+            if ( Value == ABC_INIT_NONE )
+            {
+                // value is unknown, remove it from the table
+                RetEdge.iNode  = pFanout->Id;
+                RetEdge.iEdge  = Edge;
+                RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed
+                if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
+                    assert( 0 );
+                // create the fanout of the AND gate
+                Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+            }
+        }
+        if ( Abc_ObjFaninId1(pFanout) == pObj->Id )
+        {
+            Edge = 1;
+            Value = Seq_NodeDeleteLast( pFanout, Edge );
+            if ( Value == ABC_INIT_NONE )
+            {
+                // value is unknown, remove it from the table
+                RetEdge.iNode  = pFanout->Id;
+                RetEdge.iEdge  = Edge;
+                RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed
+                if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
+                    assert( 0 );
+                // create the fanout of the AND gate
+                Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+            }
+        }
+    }
+    // clean the label
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        pFanout->fMarkC = 0;
+
+    // update the fanin edges
+    Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable );
+    Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable );
+    Seq_NodeInsertFirst( pObj, 0, ABC_INIT_NONE );
+    Seq_NodeInsertFirst( pObj, 1, ABC_INIT_NONE );
+
+    // add the buffer
+    pBuffer = Abc_NtkCreateNode( pNtkNew );
+    pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+    Abc_ObjAddFanin( pNodeNew, pBuffer );
+    // point to it from the table
+    RetEdge.iNode  = pObj->Id;
+    RetEdge.iEdge  = 0;
+    RetEdge.iLatch = 0;
+    if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pBuffer ) )
+        assert( 0 );
+
+    // add the buffer
+    pBuffer = Abc_NtkCreateNode( pNtkNew );
+    pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+    Abc_ObjAddFanin( pNodeNew, pBuffer );
+    // point to it from the table
+    RetEdge.iNode  = pObj->Id;
+    RetEdge.iEdge  = 1;
+    RetEdge.iLatch = 0;
+    if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pBuffer ) )
+        assert( 0 );
+
+    // report conflict is found
+    return fMet0 && fMet1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generates the printable edge label with the initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable )
+{
+    Abc_Obj_t * pFanoutNew;
+    Seq_RetEdge_t RetEdge;
+    Abc_InitType_t Init;
+    int nLatches, i;
+
+    // get the number of latches on the edge
+    nLatches = Seq_ObjFaninL( pObj, Edge );
+    for ( i = nLatches - 1; i >= 0; i-- )
+    {
+        // get the value of this latch
+        Init = Seq_NodeGetInitOne( pObj, Edge, i );
+        if ( Init != ABC_INIT_NONE )
+            continue;
+        // get the retiming edge
+        RetEdge.iNode  = pObj->Id;
+        RetEdge.iEdge  = Edge;
+        RetEdge.iLatch = i;
+        // remove entry from table and add it with a different key
+        if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
+            assert( 0 );
+        RetEdge.iLatch++;
+        if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pFanoutNew ) )
+            assert( 0 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the initial values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel )
+{
+    Abc_Obj_t * pNode;
+    stmm_generator * gen;
+    Seq_RetEdge_t RetEdge;
+    Abc_InitType_t Init;
+    int i;
+
+    i = 0;
+    stmm_foreach_item( tTable, gen, (char **)&RetEdge, NULL )
+    {
+        pNode = Abc_NtkObj( pNtk, RetEdge.iNode );
+        Init = pModel? (pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC;
+        Seq_NodeSetInitOne( pNode, RetEdge.iEdge, RetEdge.iLatch, Init );
+        i++;
+    }
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs forward retiming of the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward )
+{
+    Vec_Ptr_t * vNodes, * vMoves;
+    Abc_Obj_t * pNode, * pFanout, * pFanin;
+    int i, k, nLatches;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    // assume that all nodes can be retimed
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        Vec_PtrPush( vNodes, pNode );
+        pNode->fMarkA = 1;
+    }
+    // process the nodes
+    vMoves = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+//        printf( "(%d,%d) ", Seq_ObjFaninL0(pNode), Seq_ObjFaninL0(pNode) );
+        // unmark the node as processed
+        pNode->fMarkA = 0;
+        // get the number of latches to retime
+        if ( fForward )
+            nLatches = Seq_ObjFaninLMin(pNode);
+        else
+            nLatches = Seq_ObjFanoutLMin(pNode);
+        if ( nLatches == 0 )
+            continue;
+        assert( nLatches > 0 );
+        // retime the latches forward
+        if ( fForward )
+            Abc_ObjRetimeForwardTry( pNode, nLatches );
+        else
+            Abc_ObjRetimeBackwardTry( pNode, nLatches );
+        // write the moves
+        for ( k = 0; k < nLatches; k++ )
+            Vec_PtrPush( vMoves, pNode );
+        // schedule fanouts for updating
+        if ( fForward )
+        {
+            Abc_ObjForEachFanout( pNode, pFanout, k )
+            {
+                if ( Abc_ObjFaninNum(pFanout) != 2 || pFanout->fMarkA )
+                    continue;
+                pFanout->fMarkA = 1;
+                Vec_PtrPush( vNodes, pFanout );
+            }
+        }
+        else
+        {
+            Abc_ObjForEachFanin( pNode, pFanin, k )
+            {
+                if ( Abc_ObjFaninNum(pFanin) != 2 || pFanin->fMarkA )
+                    continue;
+                pFanin->fMarkA = 1;
+                Vec_PtrPush( vNodes, pFanin );
+            }
+        }
+    }
+    Vec_PtrFree( vNodes );
+    // make sure the marks are clean the the retiming is final
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        assert( pNode->fMarkA == 0 );
+        if ( fForward ) 
+            assert( Seq_ObjFaninLMin(pNode) == 0 );
+        else
+            assert( Seq_ObjFanoutLMin(pNode) == 0 );
+    }
+    return vMoves;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Translates retiming steps into retiming moves.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, bool fForward )
+{
+    Seq_RetStep_t RetStep;
+    Vec_Ptr_t * vMoves;
+    Abc_Obj_t * pNode;
+    int i, k, iNode, nLatches, Number;
+    int fChange;
+    assert( Abc_NtkIsSeq( pNtk ) );
+
+/*
+    // try implementing all the moves at once
+    Vec_IntForEachEntry( vSteps, Number, i )
+    {
+        // get the retiming step
+        RetStep = Seq_Int2RetStep( Number );
+        // get the node to be retimed
+        pNode = Abc_NtkObj( pNtk, RetStep.iNode );
+        assert( RetStep.nLatches > 0 );
+        nLatches = RetStep.nLatches;
+
+        if ( fForward )
+            Abc_ObjRetimeForwardTry( pNode, nLatches );
+        else
+            Abc_ObjRetimeBackwardTry( pNode, nLatches );
+    }
+    // now look if any node has wrong number of latches
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        if ( Seq_ObjFaninL0(pNode) < 0 )
+            printf( "Wrong 0node %d.\n", pNode->Id );
+        if ( Seq_ObjFaninL1(pNode) < 0 )
+            printf( "Wrong 1node %d.\n", pNode->Id );
+    }
+    // try implementing all the moves at once
+    Vec_IntForEachEntry( vSteps, Number, i )
+    {
+        // get the retiming step
+        RetStep = Seq_Int2RetStep( Number );
+        // get the node to be retimed
+        pNode = Abc_NtkObj( pNtk, RetStep.iNode );
+        assert( RetStep.nLatches > 0 );
+        nLatches = RetStep.nLatches;
+
+        if ( !fForward )
+            Abc_ObjRetimeForwardTry( pNode, nLatches );
+        else
+            Abc_ObjRetimeBackwardTry( pNode, nLatches );
+    }
+*/
+
+    // process the nodes
+    vMoves = Vec_PtrAlloc( 100 );
+    while ( Vec_IntSize(vSteps) > 0 )
+    {
+        iNode = 0;
+        fChange = 0;
+        Vec_IntForEachEntry( vSteps, Number, i )
+        {
+            // get the retiming step
+            RetStep = Seq_Int2RetStep( Number );
+            // get the node to be retimed
+            pNode = Abc_NtkObj( pNtk, RetStep.iNode );
+            assert( RetStep.nLatches > 0 );
+            // get the number of latches that can be retimed
+            if ( fForward )
+                nLatches = Seq_ObjFaninLMin(pNode);
+            else
+                nLatches = Seq_ObjFanoutLMin(pNode);
+            if ( nLatches == 0 )
+            {
+                Vec_IntWriteEntry( vSteps, iNode++, Seq_RetStep2Int(RetStep) );
+                continue;
+            }
+            assert( nLatches > 0 );
+            fChange = 1;
+            // get the number of latches to be retimed over this node
+            nLatches = ABC_MIN( nLatches, (int)RetStep.nLatches );
+            // retime the latches forward
+            if ( fForward )
+                Abc_ObjRetimeForwardTry( pNode, nLatches );
+            else
+                Abc_ObjRetimeBackwardTry( pNode, nLatches );
+            // write the moves
+            for ( k = 0; k < nLatches; k++ )
+                Vec_PtrPush( vMoves, pNode );
+            // subtract the retiming performed
+            RetStep.nLatches -= nLatches;
+            // store the node if it is not retimed completely
+            if ( RetStep.nLatches > 0 )
+                Vec_IntWriteEntry( vSteps, iNode++, Seq_RetStep2Int(RetStep) );
+        }
+        // reduce the array
+        Vec_IntShrink( vSteps, iNode );
+        if ( !fChange )
+        {
+            printf( "Warning: %d strange steps (a minor bug to be fixed later).\n", Vec_IntSize(vSteps) );
+/*
+            Vec_IntForEachEntry( vSteps, Number, i )
+            {
+                RetStep = Seq_Int2RetStep( Number );
+                printf( "%d(%d) ", RetStep.iNode, RetStep.nLatches );
+            }
+            printf( "\n" );
+*/
+            break;
+        }
+    }
+    // undo the tentative retiming
+    if ( fForward )
+    {
+        Vec_PtrForEachEntryReverse( vMoves, pNode, i )
+            Abc_ObjRetimeBackwardTry( pNode, 1 );
+    }
+    else
+    {
+        Vec_PtrForEachEntryReverse( vMoves, pNode, i )
+            Abc_ObjRetimeForwardTry( pNode, 1 );
+    }
+    return vMoves;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Splits retiming into forward and backward.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward )
+{
+    Vec_Int_t * vNodes;
+    Seq_RetStep_t RetStep;
+    int Value, i;
+    vNodes = Vec_IntAlloc( 100 );
+    Vec_StrForEachEntry( vLags, Value, i )
+    {
+        if ( Value < 0 && fForward )
+        {
+            RetStep.iNode = i;
+            RetStep.nLatches = -Value;
+            Vec_IntPush( vNodes, Seq_RetStep2Int(RetStep) );
+        }
+        else if ( Value > 0 && !fForward )
+        {
+            RetStep.iNode = i;
+            RetStep.nLatches = Value;
+            Vec_IntPush( vNodes, Seq_RetStep2Int(RetStep) );
+        }
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retime node forward without initial states.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjRetimeForwardTry( Abc_Obj_t * pObj, int nLatches )  
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    // make sure it is an AND gate
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    // make sure it has enough latches
+//    assert( Seq_ObjFaninL0(pObj) >= nLatches );
+//    assert( Seq_ObjFaninL1(pObj) >= nLatches );
+    // subtract these latches on the fanin side
+    Seq_ObjAddFaninL0( pObj, -nLatches );
+    Seq_ObjAddFaninL1( pObj, -nLatches );
+    // make sure the label is clean
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        assert( pFanout->fMarkC == 0 );
+    // add these latches on the fanout side
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        if ( pFanout->fMarkC )
+            continue;
+        pFanout->fMarkC = 1;
+        if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) )
+            Seq_ObjAddFanoutL( pObj, pFanout, nLatches );
+        else
+        {
+            assert( Abc_ObjFanin0(pFanout) == pObj );
+            Seq_ObjAddFaninL0( pFanout, nLatches );
+            Seq_ObjAddFaninL1( pFanout, nLatches );
+        }
+    }
+    // clean the label
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        pFanout->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retime node backward without initial states.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches )  
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    // make sure it is an AND gate
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    // make sure the label is clean
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        assert( pFanout->fMarkC == 0 );
+    // subtract these latches on the fanout side
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        if ( pFanout->fMarkC )
+            continue;
+        pFanout->fMarkC = 1;
+//        assert( Abc_ObjFanoutL(pObj, pFanout) >= nLatches );
+        if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) )
+            Seq_ObjAddFanoutL( pObj, pFanout, -nLatches );
+        else
+        {
+            assert( Abc_ObjFanin0(pFanout) == pObj );
+            Seq_ObjAddFaninL0( pFanout, -nLatches );
+            Seq_ObjAddFaninL1( pFanout, -nLatches );
+        }
+    }
+    // clean the label
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        pFanout->fMarkC = 0;
+    // add these latches on the fanin side
+    Seq_ObjAddFaninL0( pObj, nLatches );
+    Seq_ObjAddFaninL1( pObj, nLatches );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqAigIter.c b/src/base/seq/seqAigIter.c
new file mode 100644
index 00000000..392638b8
--- /dev/null
+++ b/src/base/seq/seqAigIter.c
@@ -0,0 +1,268 @@
+/**CFile****************************************************************
+
+  FileName    [seqRetIter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [The iterative L-Value computation for retiming procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqRetIter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the internal procedures
+static int Seq_RetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose );
+static int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose );
+static int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Retimes AIG for optimal delay using Pan's algorithm.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_AigRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Obj_t * pNode;
+    int i, FiMax, RetValue, clk, clkIter;
+    char NodeLag;
+
+    assert( Abc_NtkIsSeq( pNtk ) );
+
+    // get the upper bound on the clock period
+    FiMax = 2 + Seq_NtkLevelMax(pNtk);
+
+    // make sure this clock period is feasible
+    if ( !Seq_RetimeForPeriod( pNtk, FiMax, fVerbose ) )
+    {
+        Vec_StrFill( p->vLags, p->nSize, 0 );
+        printf( "Error: The upper bound on the clock period cannot be computed.\n" );
+        printf( "The reason for this error may be the presence in the circuit of logic\n" );
+        printf( "that is not reachable from the PIs. Mapping/retiming is not performed.\n" );
+        return 0;
+    }
+
+    // search for the optimal clock period between 0 and nLevelMax
+clk = clock();
+    p->FiBestInt = Seq_RetimeSearch_rec( pNtk, 0, FiMax, fVerbose );
+clkIter = clock() - clk;
+
+    // recompute the best l-values
+    RetValue = Seq_RetimeForPeriod( pNtk, p->FiBestInt, fVerbose );
+    assert( RetValue );
+
+    // fix the problem with non-converged delays
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        if ( Seq_NodeGetLValue(pNode) < -ABC_INFINITY/2 )
+            Seq_NodeSetLValue( pNode, 0 );
+
+    // write the retiming lags
+    Vec_StrFill( p->vLags, p->nSize, 0 );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        NodeLag = Seq_NodeComputeLag( Seq_NodeGetLValue(pNode), p->FiBestInt );
+        Seq_NodeSetLag( pNode, NodeLag );
+    }
+
+    // print the result
+    if ( fVerbose )
+    printf( "The best clock period is %3d.\n", p->FiBestInt );
+
+/*
+    printf( "lvalues and lags : " );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        printf( "%d=%d(%d) ", pNode->Id, Seq_NodeGetLValue(pNode), Seq_NodeGetLag(pNode) );
+    printf( "\n" );
+*/
+/*
+    {
+        FILE * pTable;
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  pNtk->pName );
+        fprintf( pTable, "%d ", FiBest );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+    }
+*/
+/*
+    {
+        FILE * pTable;
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  pNtk->pName );
+        fprintf( pTable, "%.2f ", (float)(p->timeCuts)/(float)(CLOCKS_PER_SEC) );
+        fprintf( pTable, "%.2f ", (float)(clkIter)/(float)(CLOCKS_PER_SEC) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+    }
+*/
+    return 1;
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs binary search for the optimal clock period.]
+
+  Description [Assumes that FiMin is infeasible while FiMax is feasible.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_RetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose )
+{
+    int Median;
+    assert( FiMin < FiMax );
+    if ( FiMin + 1 == FiMax )
+        return FiMax;
+    Median = FiMin + (FiMax - FiMin)/2;
+    if ( Seq_RetimeForPeriod( pNtk, Median, fVerbose ) )
+        return Seq_RetimeSearch_rec( pNtk, FiMin, Median, fVerbose ); // Median is feasible
+    else 
+        return Seq_RetimeSearch_rec( pNtk, Median, FiMax, fVerbose ); // Median is infeasible
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if retiming with this clock period is feasible.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Obj_t * pObj;
+    int i, c, RetValue, fChange, Counter;
+    char * pReason = "";
+
+    // set l-values of all nodes to be minus infinity
+    Vec_IntFill( p->vLValues, p->nSize, -ABC_INFINITY );
+
+    // set l-values of constants and PIs
+    pObj = Abc_NtkObj( pNtk, 0 );
+    Seq_NodeSetLValue( pObj, 0 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Seq_NodeSetLValue( pObj, 0 );
+
+    // update all values iteratively
+    Counter = 0;
+    for ( c = 0; c < p->nMaxIters; c++ )
+    {
+        fChange = 0;
+        Abc_AigForEachAnd( pNtk, pObj, i )
+        {
+            Counter++;
+            if ( Seq_NodeCutMan(pObj) )
+                RetValue = Seq_FpgaNodeUpdateLValue( pObj, Fi );
+            else
+                RetValue = Seq_RetimeNodeUpdateLValue( pObj, Fi );
+            if ( RetValue == SEQ_UPDATE_YES ) 
+                fChange = 1;
+        }
+        Abc_NtkForEachPo( pNtk, pObj, i )
+        {
+            if ( Seq_NodeCutMan(pObj) )
+                RetValue = Seq_FpgaNodeUpdateLValue( pObj, Fi );
+            else
+                RetValue = Seq_RetimeNodeUpdateLValue( pObj, Fi );
+            if ( RetValue == SEQ_UPDATE_FAIL )
+                break;
+        }
+        if ( RetValue == SEQ_UPDATE_FAIL )
+            break;
+        if ( fChange == 0 )
+            break;
+    }
+    if ( c == p->nMaxIters )
+    {
+        RetValue = SEQ_UPDATE_FAIL;
+        pReason = "(timeout)";
+    }
+    else
+        c++;
+    // report the results
+    if ( fVerbose )
+    {
+        if ( RetValue == SEQ_UPDATE_FAIL )
+            printf( "Period = %3d.  Iterations = %3d.  Updates = %10d.    Infeasible %s\n", Fi, c, Counter, pReason );
+        else
+            printf( "Period = %3d.  Iterations = %3d.  Updates = %10d.      Feasible\n",    Fi, c, Counter );
+    }
+/*
+    // check if any AND gates have infinite delay
+    Counter = 0;
+    Abc_AigForEachAnd( pNtk, pObj, i )
+        Counter += (Seq_NodeGetLValue(pObj) < -ABC_INFINITY/2);
+    if ( Counter > 0 )
+        printf( "Warning: %d internal nodes have wrong l-values!\n", Counter );
+*/
+    return RetValue != SEQ_UPDATE_FAIL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the node.]
+
+  Description [The node can be internal or a PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
+{
+    int lValueNew, lValueOld, lValue0, lValue1;
+    assert( !Abc_ObjIsPi(pObj) );
+    assert( Abc_ObjFaninNum(pObj) > 0 );
+    lValue0 = Seq_NodeGetLValue(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj);
+    if ( Abc_ObjIsPo(pObj) )
+        return (lValue0 > Fi)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO;
+    if ( Abc_ObjFaninNum(pObj) == 2 )
+        lValue1 = Seq_NodeGetLValue(Abc_ObjFanin1(pObj)) - Fi * Seq_ObjFaninL1(pObj);
+    else
+        lValue1 = -ABC_INFINITY;
+    lValueNew = 1 + ABC_MAX( lValue0, lValue1 );
+    lValueOld = Seq_NodeGetLValue(pObj);
+//    if ( lValueNew == lValueOld )
+    if ( lValueNew <= lValueOld )
+        return SEQ_UPDATE_NO;
+    Seq_NodeSetLValue( pObj, lValueNew );
+    return SEQ_UPDATE_YES;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c
new file mode 100644
index 00000000..16c7cc92
--- /dev/null
+++ b/src/base/seq/seqCreate.c
@@ -0,0 +1,482 @@
+/**CFile****************************************************************
+
+  FileName    [seqCreate.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [Transformations to and from the sequential AIG.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqCreate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+
+/*
+    A sequential network is similar to AIG in that it contains only
+    AND gates. However, the AND-gates are currently not hashed. 
+
+    When converting AIG into sequential AIG:
+    - Const1/PIs/POs remain the same as in the original AIG.
+    - Instead of the latches, a new cutset is added, which is currently
+      defined as a set of AND gates that have a latch among their fanouts.
+    - The edges of a sequential AIG are labeled with latch attributes
+      in addition to the complementation attibutes. 
+    - The attributes contain information about the number of latches 
+      and their initial states. 
+    - The number of latches is stored directly on the edges. The initial 
+      states are stored in the sequential AIG manager.
+
+    In the current version of the code, the sequential AIG is static 
+    in the sense that the new AIG nodes are never created.
+    The retiming (or retiming/mapping) is performed by moving the
+    latches over the static nodes of the AIG.
+    The new initial state after backward retiming is computed 
+    by setting up and solving a SAT problem.
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObjNew, Abc_Obj_t * pObj, int Edge, Vec_Int_t * vInitValues );
+static void        Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk );
+static Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, Seq_Lat_t * pRing, int nLatches );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Converts combinational AIG with latches into sequential AIG.]
+
+  Description [The const/PI/PO nodes are duplicated. The internal
+  nodes are duplicated in the topological order. The dangling nodes
+  are not duplicated. The choice nodes are duplicated.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pFaninNew;
+    Vec_Int_t * vInitValues;
+    Abc_InitType_t Init;
+    int i, k, RetValue;
+
+    // make sure it is an AIG without self-feeding latches
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkIsDfsOrdered(pNtk) );
+
+    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) )
+        printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
+    assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
+
+    // start the network
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG, 1 );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+
+    // map the constant nodes
+    Abc_NtkCleanCopy( pNtk );
+    Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
+
+    // copy all objects, except the latches and constant
+    Vec_PtrFill( pNtkNew->vObjs, Abc_NtkObjNumMax(pNtk), NULL );
+    Vec_PtrWriteEntry( pNtkNew->vObjs, 0, Abc_AigConst1(pNtk)->pCopy );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( i == 0 || Abc_ObjIsLatch(pObj) )
+            continue;
+        pObj->pCopy = Abc_ObjAlloc( pNtkNew, pObj->Type );
+        pObj->pCopy->Id     = pObj->Id;      // the ID is the same for both
+        pObj->pCopy->fPhase = pObj->fPhase;  // used to work with choices
+        pObj->pCopy->Level  = pObj->Level;   // used for upper bound on clock cycle
+        Vec_PtrWriteEntry( pNtkNew->vObjs, pObj->pCopy->Id, pObj->pCopy );
+        pNtkNew->nObjs++;
+    }
+    pNtkNew->nObjCounts[ABC_OBJ_NODE] = pNtk->nObjCounts[ABC_OBJ_NODE];
+
+    // create PI/PO and their names
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        Vec_PtrPush( pNtkNew->vPis, pObj->pCopy );
+        Vec_PtrPush( pNtkNew->vCis, pObj->pCopy );
+        Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
+    }
+    Abc_NtkForEachPo( pNtk, pObj, i ) 
+    {
+        Vec_PtrPush( pNtkNew->vPos, pObj->pCopy );
+        Vec_PtrPush( pNtkNew->vCos, pObj->pCopy );
+        Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
+    }
+    Abc_NtkForEachAssert( pNtk, pObj, i ) 
+    {
+        Vec_PtrPush( pNtkNew->vAsserts, pObj->pCopy );
+        Vec_PtrPush( pNtkNew->vCos, pObj->pCopy );
+        Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
+    }
+
+    // relink the choice nodes
+    Abc_AigForEachAnd( pNtk, pObj, i )
+        if ( pObj->pData )
+            pObj->pCopy->pData = ((Abc_Obj_t *)pObj->pData)->pCopy;
+
+    // start the storage for initial states
+    Seq_Resize( pNtkNew->pManFunc, Abc_NtkObjNumMax(pNtkNew) );
+    // reconnect the internal nodes
+    vInitValues = Vec_IntAlloc( 100 );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        // skip constants, PIs, and latches
+        if ( Abc_ObjFaninNum(pObj) == 0 || Abc_ObjIsLatch(pObj) )
+            continue;
+        // process the first fanin
+        Vec_IntClear( vInitValues );
+        pFaninNew = Abc_NodeAigToSeq( pObj->pCopy, pObj, 0, vInitValues );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        // store the initial values
+        Vec_IntForEachEntry( vInitValues, Init, k )
+            Seq_NodeInsertFirst( pObj->pCopy, 0, Init );
+        // skip single-input nodes
+        if ( Abc_ObjFaninNum(pObj) == 1 )
+            continue;
+        // process the second fanin
+        Vec_IntClear( vInitValues );
+        pFaninNew = Abc_NodeAigToSeq( pObj->pCopy, pObj, 1, vInitValues );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        // store the initial values
+        Vec_IntForEachEntry( vInitValues, Init, k )
+            Seq_NodeInsertFirst( pObj->pCopy, 1, Init );
+    }
+    Vec_IntFree( vInitValues );
+
+    // set the cutset composed of latch drivers
+    Abc_NtkAigCutsetCopy( pNtk );
+    Seq_NtkLatchGetEqualFaninNum( pNtkNew );
+
+    // copy EXDC and check correctness
+    if ( pNtk->pExdc )
+        fprintf( stdout, "Warning: EXDC is not copied when converting to sequential AIG.\n" );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkAigToSeq(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determines the fanin that is transparent for latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObjNew, Abc_Obj_t * pObj, int Edge, Vec_Int_t * vInitValues )
+{
+    Abc_Obj_t * pFanin, * pFaninNew;
+    Abc_InitType_t Init;
+    // get the given fanin of the node
+    pFanin = Abc_ObjFanin( pObj, Edge );
+    // if fanin is the internal node, return its copy in the corresponding polarity
+    if ( !Abc_ObjIsLatch(pFanin) )
+        return Abc_ObjNotCond( pFanin->pCopy, Abc_ObjFaninC(pObj, Edge) );
+    // fanin is a latch
+    // get the new fanins
+    pFaninNew = Abc_NodeAigToSeq( pObjNew, pFanin, 0, vInitValues );
+    // get the initial state
+    Init = Abc_LatchInit(pFanin);
+    // complement the initial state if the inv is retimed over the latch
+    if ( Abc_ObjIsComplement(pFaninNew) ) 
+    {
+        if ( Init == ABC_INIT_ZERO )
+            Init = ABC_INIT_ONE;
+        else if ( Init == ABC_INIT_ONE )
+            Init = ABC_INIT_ZERO;
+        else if ( Init != ABC_INIT_DC )
+            assert( 0 );
+    }
+    // record the initial state
+    Vec_IntPush( vInitValues, Init );
+    return Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC(pObj, Edge) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the cut set nodes.]
+
+  Description [These are internal AND gates that have latch fanouts.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch, * pDriver, * pDriverNew;
+    int i;
+    Abc_NtkIncrementTravId(pNtk);
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        pDriver = Abc_ObjFanin0(pLatch);
+        if ( Abc_NodeIsTravIdCurrent(pDriver) || !Abc_AigNodeIsAnd(pDriver) )
+            continue;
+        Abc_NodeSetTravIdCurrent(pDriver);
+        pDriverNew = pDriver->pCopy;
+        Vec_PtrPush( pDriverNew->pNtk->vCutSet, pDriverNew );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts a sequential AIG into a logic SOP network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pFaninNew;
+    Seq_Lat_t * pRing;
+    int i;
+
+    assert( Abc_NtkIsSeq(pNtk) );
+    // start the network without latches
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    // duplicate the nodes
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        Abc_NtkDupObj(pNtkNew, pObj, 0);
+        pObj->pCopy->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+    }
+    // share and create the latches
+    Seq_NtkShareLatches( pNtkNew, pNtk );
+    // connect the objects
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        if ( pRing = Seq_NodeGetRing(pObj,0) )
+            pFaninNew = pRing->pLatch;
+        else
+            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+
+        if ( pRing = Seq_NodeGetRing(pObj,1) )
+            pFaninNew = pRing->pLatch;
+        else
+            pFaninNew = Abc_ObjFanin1(pObj)->pCopy;
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+    // connect the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        if ( pRing = Seq_NodeGetRing(pObj,0) )
+            pFaninNew = pRing->pLatch;
+        else
+            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
+        pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+    // clean the latch pointers
+    Seq_NtkShareLatchesClean( pNtk );
+
+    // add the latches and their names
+    Abc_NtkAddDummyBoxNames( pNtkNew );
+    Abc_NtkOrderCisCos( pNtkNew );
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkSeqToLogicSop(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Converts a sequential AIG into a logic SOP network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkSeqToLogicSop_old( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pFaninNew;
+    int i;
+
+    assert( Abc_NtkIsSeq(pNtk) );
+    // start the network without latches
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+
+    // duplicate the nodes, create node functions
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        // skip the constant
+        if ( Abc_ObjFaninNum(pObj) == 0 )
+            continue;
+        // duplicate the node
+        Abc_NtkDupObj(pNtkNew, pObj, 0);
+        if ( Abc_ObjFaninNum(pObj) == 1 )
+        {
+            assert( !Abc_ObjFaninC0(pObj) );
+            pObj->pCopy->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+            continue;
+        }
+        pObj->pCopy->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+    }
+    // connect the objects
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        assert( (int)pObj->Id == i );
+        // skip PIs and the constant
+        if ( Abc_ObjFaninNum(pObj) == 0 )
+            continue;
+        // create the edge
+        pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin0(pObj), Seq_NodeGetRing(pObj,0), Seq_ObjFaninL0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        if ( Abc_ObjFaninNum(pObj) == 1 )
+        {
+            // create the complemented edge
+            if ( Abc_ObjFaninC0(pObj) )
+                Abc_ObjSetFaninC( pObj->pCopy, 0 );
+            continue;
+        }
+        // create the edge
+        pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin1(pObj), Seq_NodeGetRing(pObj,1), Seq_ObjFaninL1(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        // the complemented edges are subsumed by the node function
+    }
+    // add the latches and their names
+    Abc_NtkAddDummyBoxNames( pNtkNew );
+    Abc_NtkOrderCisCos( pNtkNew );
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkSeqToLogicSop(): Network check has failed.\n" );
+    return pNtkNew;
+}
+ 
+
+/**Function*************************************************************
+
+  Synopsis    [Creates latches on one edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, Seq_Lat_t * pRing, int nLatches )
+{
+    Abc_Obj_t * pLatch;
+    if ( nLatches == 0 )
+    {
+        assert( pFanin->pCopy );
+        return pFanin->pCopy;
+    }
+    pFanin = Abc_NodeSeqToLogic( pNtkNew, pFanin, Seq_LatNext(pRing), nLatches - 1 );
+    pLatch = Abc_NtkCreateLatch( pNtkNew );
+    pLatch->pData = (void *)Seq_LatInit( pRing );
+    Abc_ObjAddFanin( pLatch, pFanin );
+    return pLatch;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Makes sure that every node in the table is in the network and vice versa.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkSeqCheck( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, nFanins;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+        {
+            if ( pObj != Abc_AigConst1(pNtk) )
+            {
+                printf( "Abc_SeqCheck: The AIG has non-standard constant nodes.\n" );
+                return 0;
+            }
+            continue;
+        }
+        if ( nFanins == 1 )
+        {
+            printf( "Abc_SeqCheck: The AIG has single input nodes.\n" );
+            return 0;
+        }
+        if ( nFanins > 2 )
+        {
+            printf( "Abc_SeqCheck: The AIG has non-standard nodes.\n" );
+            return 0;
+        }
+    }
+    // check the correctness of the internal representation of the initial states
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+            continue;
+        if ( nFanins == 1 )
+        {
+            if ( Seq_NodeCountLats(pObj, 0) != Seq_ObjFaninL0(pObj) )
+            {
+                printf( "Abc_SeqCheck: Node %d has mismatch in the number of latches.\n", Abc_ObjName(pObj) );
+                return 0;
+            }
+        }
+        // look at both inputs
+        if ( Seq_NodeCountLats(pObj, 0) != Seq_ObjFaninL0(pObj) )
+        {
+            printf( "Abc_SeqCheck: The first fanin of node %d has mismatch in the number of latches.\n", Abc_ObjName(pObj) );
+            return 0;
+        }
+        if ( Seq_NodeCountLats(pObj, 1) != Seq_ObjFaninL1(pObj) )
+        {
+            printf( "Abc_SeqCheck: The second fanin of node %d has mismatch in the number of latches.\n", Abc_ObjName(pObj) );
+            return 0;
+        }
+    }
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqFpgaCore.c b/src/base/seq/seqFpgaCore.c
new file mode 100644
index 00000000..b106ded2
--- /dev/null
+++ b/src/base/seq/seqFpgaCore.c
@@ -0,0 +1,643 @@
+/**CFile****************************************************************
+
+  FileName    [seqFpgaCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [The core of FPGA mapping/retiming package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqFpgaCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t *  Seq_NtkFpgaDup( Abc_Ntk_t * pNtk );
+static int          Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk, int fVerbose );
+static Abc_Ntk_t *  Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtkNew );
+static int          Seq_FpgaMappingCount( Abc_Ntk_t * pNtk );
+static int          Seq_FpgaMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
+static Abc_Obj_t *  Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves );
+static DdNode *     Seq_FpgaMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
+static void         Seq_FpgaMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges );
+static void         Seq_FpgaMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
+static DdNode *     Seq_FpgaMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs FPGA mapping and retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Ntk_t * pNtkMap;
+    int RetValue;
+
+    // get the LUT library
+    p->nVarsMax = Fpga_LutLibReadVarMax( Abc_FrameReadLibLut() );
+    p->nMaxIters = nMaxIters;
+
+    // find the best mapping and retiming for all nodes (p->vLValues, p->vBestCuts, p->vLags)
+    if ( !Seq_FpgaMappingDelays( pNtk, fVerbose ) )
+        return NULL;
+    if ( RetValue = Abc_NtkGetChoiceNum(pNtk) )
+    {
+        printf( "The network has %d choices. The resulting network is not derived (this is temporary).\n", RetValue );
+        printf( "The mininum clock period computed is %d.\n", p->FiBestInt );
+        return NULL;
+    }
+
+    // duplicate the nodes contained in multiple cuts
+    pNtkNew = Seq_NtkFpgaDup( pNtk );
+//    return pNtkNew;
+    
+    // implement the retiming
+    RetValue = Seq_NtkImplementRetiming( pNtkNew, ((Abc_Seq_t *)pNtkNew->pManFunc)->vLags, fVerbose );
+    if ( RetValue == 0 )
+        printf( "Retiming completed but initial state computation has failed.\n" );
+//    return pNtkNew;
+
+    // check the compatibility of initial states computed
+    if ( RetValue = Seq_NtkFpgaInitCompatible( pNtkNew, fVerbose ) )
+        printf( "The number of LUTs with incompatible edges = %d.\n", RetValue );
+
+    // create the final mapped network
+    pNtkMap = Seq_NtkSeqFpgaMapped( pNtkNew );
+    Abc_NtkDelete( pNtkNew );
+    if ( RetValue )
+        printf( "The number of LUTs with more than %d inputs = %d.\n", 
+            p->nVarsMax, Seq_NtkCountNodesAboveLimit(pNtkMap, p->nVarsMax) );
+    return pNtkMap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the network by duplicating some of the nodes.]
+
+  Description [Information about mapping is given as mapping nodes (p->vMapAnds)
+  and best cuts for each node (p->vMapCuts).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkFpgaDup( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * pNew, * p = pNtk->pManFunc;
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pLeaf;
+    Vec_Ptr_t * vLeaves;
+    unsigned SeqEdge;
+    int i, k, nObjsNew, Lag;
+    
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    // start the expanded network
+    pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
+
+    // start the new sequential AIG manager
+    nObjsNew = 1 + Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk) + Seq_FpgaMappingCount(pNtk);
+    Seq_Resize( pNtkNew->pManFunc, nObjsNew );
+
+    // duplicate the nodes in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+
+    // recursively construct the internals of each node
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+    {
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, pObj->Id << 8, 1, Seq_NodeGetLag(pObj), vLeaves );
+    }
+    assert( nObjsNew == pNtkNew->nObjs );
+
+    // set the POs
+    Abc_NtkFinalize( pNtk, pNtkNew );
+    // duplicate the latches on the PO edges
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_NodeDupLats( pObj->pCopy, pObj, 0 );
+
+    // transfer the mapping info to the new manager
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+    {
+        // get the leaves of the cut
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // convert the leaf nodes
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+            Lag = (SeqEdge & 255) + Seq_NodeGetLag(pObj) - Seq_NodeGetLag(pLeaf);
+            assert( Lag >= 0 );
+            // translate the old leaf into the leaf in the new network
+            Vec_PtrWriteEntry( vLeaves, k, (void *)((pLeaf->pCopy->Id << 8) | Lag) );
+//            printf( "%d -> %d\n", pLeaf->Id, pLeaf->pCopy->Id );
+        }
+        // convert the root node
+        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
+    }
+    pNew = pNtkNew->pManFunc;
+    pNew->nVarsMax  = p->nVarsMax;
+    pNew->vMapAnds  = p->vMapAnds;   p->vMapAnds  = NULL;
+    pNew->vMapCuts  = p->vMapCuts;   p->vMapCuts  = NULL;
+
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Seq_NtkFpgaDup(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the initial states are compatible.]
+
+  Description [Checks of all the initial states on the fanins edges
+  of the cut have compatible number of latches and initial states.
+  If this is not true, then the mapped network with the does not have initial 
+  state. Returns the number of LUTs with incompatible edges.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Obj_t * pAnd, * pLeaf, * pFanout0, * pFanout1;
+    Vec_Vec_t * vTotalEdges;
+    Vec_Ptr_t * vLeaves, * vEdges;
+    int i, k, m, Edge0, Edge1, nLatchAfter, nLatches1, nLatches2;
+    unsigned SeqEdge;
+    int CountBad = 0, CountAll = 0;
+
+    vTotalEdges = Vec_VecStart( p->nVarsMax );
+    // go through all the nodes (cuts) used in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pAnd, i )
+    {
+//        printf( "*** Node %d.\n", pAnd->Id );
+
+        // get the cut of this gate
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+
+        // get the edges pointing to the leaves
+        Vec_VecClear( vTotalEdges );
+        Seq_FpgaMappingEdges_rec( pNtk, pAnd->Id << 8, NULL, vLeaves, vTotalEdges );
+
+        // for each leaf, consider its edges
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+            nLatchAfter = SeqEdge & 255;
+            if ( nLatchAfter == 0 )
+                continue;
+
+            // go through the edges
+            vEdges = Vec_VecEntry( vTotalEdges, k );
+            pFanout0 = NULL;
+            Vec_PtrForEachEntry( vEdges, pFanout1, m )
+            {
+                Edge1    = Abc_ObjIsComplement(pFanout1);
+                pFanout1 = Abc_ObjRegular(pFanout1);
+//printf( "Fanin = %d. Fanout = %d.\n", pLeaf->Id, pFanout1->Id );
+
+                // make sure this is the same fanin
+                if ( Edge1 )
+                    assert( pLeaf == Abc_ObjFanin1(pFanout1) );
+                else
+                    assert( pLeaf == Abc_ObjFanin0(pFanout1) );
+
+                // save the first one
+                if ( pFanout0 == NULL )
+                {
+                    pFanout0 = pFanout1;
+                    Edge0    = Edge1;
+                    continue;
+                }
+                // compare the rings
+                // if they have different number of latches, this is the bug
+                nLatches1 = Seq_NodeCountLats(pFanout0, Edge0);
+                nLatches2 = Seq_NodeCountLats(pFanout1, Edge1);
+                assert( nLatches1 == nLatches2 );
+                assert( nLatches1 == nLatchAfter );
+                assert( nLatches1 > 0 );
+
+                // if they have different initial states, this is the problem
+                if ( !Seq_NodeCompareLats(pFanout0, Edge0, pFanout1, Edge1) )
+                {
+                    CountBad++;
+                    break;
+                }
+                CountAll++;
+            }
+        }
+    }
+    if ( fVerbose )
+        printf( "The number of pairs of edges checked = %d.\n", CountAll );
+    Vec_VecFree( vTotalEdges );
+    return CountBad;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the final mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Ntk_t * pNtkMap; 
+    Vec_Ptr_t * vLeaves;
+    Abc_Obj_t * pObj, * pFaninNew;
+    Seq_Lat_t * pRing;
+    int i;
+
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    // start the network
+    pNtkMap = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+
+    // duplicate the nodes used in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+        pObj->pCopy = Abc_NtkCreateNode( pNtkMap );
+
+    // create and share the latches
+    Seq_NtkShareLatchesMapping( pNtkMap, pNtk, p->vMapAnds, 1 );
+
+    // connect the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+    {
+        // get the leaves of this gate
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // get the BDD of the node
+        pObj->pCopy->pData = Seq_FpgaMappingConnectBdd_rec( pNtk, pObj->Id << 8, NULL, -1, pObj, vLeaves );
+        Cudd_Ref( pObj->pCopy->pData );
+        // complement the BDD of the cut if it came from the opposite polarity choice cut
+//        if ( Vec_StrEntry(p->vPhase, i) )
+//            pObj->pCopy->pData = Cudd_Not( pObj->pCopy->pData );
+    }
+
+    // set the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        if ( pRing = Seq_NodeGetRing(pObj,0) )
+            pFaninNew = pRing->pLatch;
+        else
+            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
+        pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+
+    // add the latches and their names
+    Abc_NtkAddDummyBoxNames( pNtkMap );
+    Abc_NtkOrderCisCos( pNtkMap );
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkMap, 1 );
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtkMap );
+    if ( !Abc_NtkCheck( pNtkMap ) )
+        fprintf( stdout, "Seq_NtkSeqFpgaMapped(): Network check has failed.\n" );
+    return pNtkMap;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nodes in the bag.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_FpgaMappingCount( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Vec_Ptr_t * vLeaves;
+    Abc_Obj_t * pAnd;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( p->vMapAnds, pAnd, i )
+    {
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        Counter += Seq_FpgaMappingCount_rec( pNtk, pAnd->Id << 8, vLeaves );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nodes in the bag.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_FpgaMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj, * pLeaf;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+            return 0;
+    // continue unfolding
+    assert( Abc_AigNodeIsAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children
+    return 1 + Seq_FpgaMappingCount_rec( pNtk, SeqEdge0, vLeaves ) + 
+        Seq_FpgaMappingCount_rec( pNtk, SeqEdge1, vLeaves );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+            return pObj->pCopy;
+    // continue unfolding
+    assert( Abc_AigNodeIsAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children    
+    pObjNew = fTop? pObj->pCopy : Abc_NtkCreateNode( pNtkNew );
+    // solve subproblems
+    pFaninNew0 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, LagCut, vLeaves );
+    pFaninNew1 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, LagCut, vLeaves );
+    // add the fanins to the node
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) );
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) );
+    Seq_NodeDupLats( pObjNew, pObj, 0 );
+    Seq_NodeDupLats( pObjNew, pObj, 1 );
+    // set the lag of the new node equal to the internal lag plus mapping/retiming lag
+    Seq_NodeSetLag( pObjNew, (char)(Lag + LagCut) );
+//    Seq_NodeSetLag( pObjNew, (char)(Lag) );
+    return pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the BDD of the selected cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Seq_FpgaMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj, * pLeaf;
+    DdNode * bFunc0, * bFunc1, * bFunc;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+            return Cudd_bddIthVar( dd, i );
+    // continue unfolding
+    assert( Abc_AigNodeIsAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children
+    bFunc0 = Seq_FpgaMappingBdd_rec( dd, pNtk, SeqEdge0, vLeaves );    Cudd_Ref( bFunc0 );
+    bFunc1 = Seq_FpgaMappingBdd_rec( dd, pNtk, SeqEdge1, vLeaves );    Cudd_Ref( bFunc1 );
+    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pObj) );
+    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pObj) );
+    // get the BDD of the node
+    bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );  Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( dd, bFunc0 );
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    // return the BDD
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_FpgaMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges )
+{
+    Abc_Obj_t * pObj, * pLeaf;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+            assert( pPrev != NULL );
+            Vec_VecPush( vMapEdges, i, pPrev );
+            return;
+        }
+    }
+    // continue unfolding
+    assert( Abc_AigNodeIsAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children    
+    Seq_FpgaMappingEdges_rec( pNtk, SeqEdge0, pObj            , vLeaves, vMapEdges );
+    Seq_FpgaMappingEdges_rec( pNtk, SeqEdge1, Abc_ObjNot(pObj), vLeaves, vMapEdges );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_FpgaMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves )
+{
+    Seq_Lat_t * pRing;
+    Abc_Obj_t * pObj, * pLeaf, * pFanin, * pFaninNew;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i, k;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, add the connection and return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+            assert( pPrev != NULL );
+            if ( pRing = Seq_NodeGetRing(pPrev,Edge) )
+                pFaninNew = pRing->pLatch;
+            else
+                pFaninNew = Abc_ObjFanin(pPrev,Edge)->pCopy;
+            // check if the root already has this fanin
+            Abc_ObjForEachFanin( pRoot, pFanin, k )
+                if ( pFanin == pFaninNew )
+                    return;
+            Abc_ObjAddFanin( pRoot->pCopy, pFaninNew );
+            return;
+        }
+    }
+    // continue unfolding
+    assert( Abc_AigNodeIsAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children    
+    Seq_FpgaMappingConnect_rec( pNtk, SeqEdge0, pObj, 0, pRoot, vLeaves );
+    Seq_FpgaMappingConnect_rec( pNtk, SeqEdge1, pObj, 1, pRoot, vLeaves );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Seq_FpgaMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves )
+{
+    Seq_Lat_t * pRing;
+    Abc_Obj_t * pObj, * pLeaf, * pFanin, * pFaninNew;
+    unsigned SeqEdge0, SeqEdge1;
+    DdManager * dd = pRoot->pCopy->pNtk->pManFunc;
+    DdNode * bFunc, * bFunc0, * bFunc1;
+    int Lag, i, k;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, add the connection and return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+            assert( pPrev != NULL );
+            if ( pRing = Seq_NodeGetRing(pPrev,Edge) )
+                pFaninNew = pRing->pLatch;
+            else
+                pFaninNew = Abc_ObjFanin(pPrev,Edge)->pCopy;
+            // check if the root already has this fanin
+            Abc_ObjForEachFanin( pRoot->pCopy, pFanin, k )
+                if ( pFanin == pFaninNew )
+                    return Cudd_bddIthVar( dd, k );
+            Abc_ObjAddFanin( pRoot->pCopy, pFaninNew );
+            return Cudd_bddIthVar( dd, k );
+        }
+    }
+    // continue unfolding
+    assert( Abc_AigNodeIsAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children    
+    bFunc0 = Seq_FpgaMappingConnectBdd_rec( pNtk, SeqEdge0, pObj, 0, pRoot, vLeaves );    Cudd_Ref( bFunc0 );
+    bFunc1 = Seq_FpgaMappingConnectBdd_rec( pNtk, SeqEdge1, pObj, 1, pRoot, vLeaves );    Cudd_Ref( bFunc1 );
+    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pObj) );
+    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pObj) );
+    // get the BDD of the node
+    bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );  Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( dd, bFunc0 );
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    // return the BDD
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqFpgaIter.c b/src/base/seq/seqFpgaIter.c
new file mode 100644
index 00000000..a300b362
--- /dev/null
+++ b/src/base/seq/seqFpgaIter.c
@@ -0,0 +1,270 @@
+/**CFile****************************************************************
+
+  FileName    [seqFpgaIter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [Iterative delay computation in FPGA mapping/retiming package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqFpgaIter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+#include "main.h"
+#include "fpga.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void        Seq_FpgaMappingCollectNode_rec( Abc_Obj_t * pAnd, Vec_Ptr_t * vMapping, Vec_Vec_t * vMapCuts );
+static Cut_Cut_t * Seq_FpgaMappingSelectCut( Abc_Obj_t * pAnd );
+
+extern Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
+extern Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the retiming lags for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Cut_Params_t Params, * pParams = &Params;
+    Abc_Obj_t * pObj;
+    int i, clk;
+
+    // set defaults for cut computation
+    memset( pParams, 0, sizeof(Cut_Params_t) );
+    pParams->nVarsMax  = p->nVarsMax;  // the max cut size ("k" of the k-feasible cuts)
+    pParams->nKeepMax  = 1000;  // the max number of cuts kept at a node
+    pParams->fTruth    = 0;     // compute truth tables
+    pParams->fFilter   = 1;     // filter dominated cuts
+    pParams->fSeq      = 1;     // compute sequential cuts
+    pParams->fVerbose  = fVerbose;     // the verbosiness flag
+
+    // compute the cuts
+clk = clock();
+    p->pCutMan = Abc_NtkSeqCuts( pNtk, pParams );
+//    pParams->fSeq = 0;
+//    p->pCutMan = Abc_NtkCuts( pNtk, pParams );
+p->timeCuts = clock() - clk;
+
+    if ( fVerbose )
+    Cut_ManPrintStats( p->pCutMan );
+
+    // compute area flows
+//    Seq_MapComputeAreaFlows( pNtk, fVerbose );
+
+    // compute the delays
+clk = clock();
+    if ( !Seq_AigRetimeDelayLags( pNtk, fVerbose ) )
+        return 0;
+    p->timeDelay = clock() - clk;
+
+    // collect the nodes and cuts used in the mapping
+    p->vMapAnds = Vec_PtrAlloc( 1000 );
+    p->vMapCuts = Vec_VecAlloc( 1000 );
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_FpgaMappingCollectNode_rec( Abc_ObjFanin0(pObj), p->vMapAnds, p->vMapCuts );
+
+    if ( fVerbose )
+    printf( "The number of LUTs = %d.\n", Vec_PtrSize(p->vMapAnds) );
+
+    // remove the cuts
+    Cut_ManStop( p->pCutMan );
+    p->pCutMan = NULL;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the parameters of the best mapping/retiming for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_FpgaMappingCollectNode_rec( Abc_Obj_t * pAnd, Vec_Ptr_t * vMapping, Vec_Vec_t * vMapCuts )
+{
+    Abc_Obj_t * pFanin;
+    Cut_Cut_t * pCutBest;
+    int k;
+
+    // skip if this is a non-PI node
+    if ( !Abc_AigNodeIsAnd(pAnd) )
+        return;
+    // skip a visited node
+    if ( Abc_NodeIsTravIdCurrent(pAnd) )
+        return;
+    Abc_NodeSetTravIdCurrent(pAnd);
+
+    // visit the fanins of the node
+    pCutBest = Seq_FpgaMappingSelectCut( pAnd );
+    for ( k = 0; k < (int)pCutBest->nLeaves; k++ )
+    {
+        pFanin = Abc_NtkObj( pAnd->pNtk, pCutBest->pLeaves[k] >> 8 );
+        Seq_FpgaMappingCollectNode_rec( pFanin, vMapping, vMapCuts );
+    }
+
+    // add this node
+    Vec_PtrPush( vMapping, pAnd );
+    for ( k = 0; k < (int)pCutBest->nLeaves; k++ )
+        Vec_VecPush( vMapCuts, Vec_PtrSize(vMapping)-1, (void *)pCutBest->pLeaves[k] );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Selects the best cut to represent the node in the mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Seq_FpgaMappingSelectCut( Abc_Obj_t * pAnd )
+{
+    Abc_Obj_t * pFanin;
+    Cut_Cut_t * pCut, * pCutBest, * pList;
+    float CostCur, CostMin = ABC_INFINITY;
+    int ArrivalCut, ArrivalMin, i;
+    // get the arrival time of the best non-trivial cut
+    ArrivalMin = Seq_NodeGetLValue( pAnd );
+    // iterate through the cuts and select the one with the minimum cost
+    pList = Abc_NodeReadCuts( Seq_NodeCutMan(pAnd), pAnd );
+    CostMin = ABC_INFINITY;
+    pCutBest = NULL;
+    for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
+    {
+        ArrivalCut = *((int *)&pCut->uSign);
+//        assert( ArrivalCut >= ArrivalMin );
+        if ( ArrivalCut > ArrivalMin )
+            continue;
+        CostCur = 0.0;
+        for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        {
+            pFanin = Abc_NtkObj( pAnd->pNtk, pCut->pLeaves[i] >> 8 );
+            if ( Abc_ObjIsPi(pFanin) )
+                continue;
+            if ( Abc_NodeIsTravIdCurrent(pFanin) )
+                continue;
+            CostCur += (float)(1.0 / Abc_ObjFanoutNum(pFanin));
+//            CostCur += Seq_NodeGetFlow( pFanin );
+        }
+        if ( CostMin > CostCur )
+        {
+            CostMin = CostCur;
+            pCutBest = pCut;
+        }
+    }
+    assert( pCutBest != NULL );
+    return pCutBest;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the cut.]
+
+  Description [The node should be internal.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Seq_FpgaCutUpdateLValue( Cut_Cut_t * pCut, Abc_Obj_t * pObj, int Fi )
+{
+    Abc_Obj_t * pFanin;
+    int i, lValueMax, lValueCur;
+    assert( Abc_AigNodeIsAnd(pObj) );
+    lValueMax = -ABC_INFINITY;
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+    {
+//        lValue0 = Seq_NodeGetLValue(Abc_ObjFanin0(pObj)) - Fi * Abc_ObjFaninL0(pObj);
+        pFanin    = Abc_NtkObj(pObj->pNtk, pCut->pLeaves[i] >> 8);
+        lValueCur = Seq_NodeGetLValue(pFanin) - Fi * (pCut->pLeaves[i] & 255);
+        if ( lValueMax < lValueCur )
+            lValueMax = lValueCur;
+    }
+    lValueMax += 1;
+    *((int *)&pCut->uSign) = lValueMax;
+    return lValueMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the node.]
+
+  Description [The node can be internal or a PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_FpgaNodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
+{
+    Cut_Cut_t * pCut, * pList;
+    int lValueNew, lValueOld, lValueCut;
+    assert( !Abc_ObjIsPi(pObj) );
+    assert( Abc_ObjFaninNum(pObj) > 0 );
+    if ( Abc_ObjIsPo(pObj) )
+    {
+        lValueNew = Seq_NodeGetLValue(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj);
+        return (lValueNew > Fi)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO;
+    }
+    // get the arrival time of the best non-trivial cut
+    pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj );
+    // skip the choice nodes
+    if ( pList == NULL )
+        return SEQ_UPDATE_NO;
+    lValueNew = ABC_INFINITY;
+    for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
+    {
+        lValueCut = Seq_FpgaCutUpdateLValue( pCut, pObj, Fi );
+        if ( lValueNew > lValueCut )
+            lValueNew = lValueCut;
+    }
+    // compare the arrival time with the previous arrival time
+    lValueOld = Seq_NodeGetLValue(pObj);
+//    if ( lValueNew == lValueOld )
+    if ( lValueNew <= lValueOld )
+        return SEQ_UPDATE_NO;
+    Seq_NodeSetLValue( pObj, lValueNew );
+//printf( "%d -> %d   ", lValueOld, lValueNew );
+    return SEQ_UPDATE_YES;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqInt.h b/src/base/seq/seqInt.h
new file mode 100644
index 00000000..221efc91
--- /dev/null
+++ b/src/base/seq/seqInt.h
@@ -0,0 +1,256 @@
+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/seq/seqLatch.c b/src/base/seq/seqLatch.c
new file mode 100644
index 00000000..cb3e1e36
--- /dev/null
+++ b/src/base/seq/seqLatch.c
@@ -0,0 +1,223 @@
+/**CFile****************************************************************
+
+  FileName    [seqLatch.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [Manipulation of latch data structures representing initial states.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqLatch.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Insert the first Lat on the edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodeInsertFirst( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )  
+{ 
+    Seq_Lat_t * pLat, * pRing, * pPrev;
+    pRing = Seq_NodeGetRing( pObj, Edge );
+    pLat  = Seq_NodeCreateLat( pObj );
+    if ( pRing == NULL )
+    {
+        Seq_LatSetPrev( pLat, pLat );
+        Seq_LatSetNext( pLat, pLat );
+        Seq_NodeSetRing( pObj, Edge, pLat );
+    }
+    else
+    {
+        pPrev = Seq_LatPrev( pRing );
+        Seq_LatSetPrev( pLat, pPrev );
+        Seq_LatSetNext( pPrev, pLat );
+        Seq_LatSetPrev( pRing, pLat );
+        Seq_LatSetNext( pLat, pRing );
+        Seq_NodeSetRing( pObj, Edge, pLat );  // rotate the ring to make pLat the first
+    }
+    Seq_LatSetInit( pLat, Init );
+    Seq_ObjAddFaninL( pObj, Edge, 1 );
+    assert( pLat->pLatch == NULL );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Insert the last Lat on the edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodeInsertLast( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )  
+{ 
+    Seq_Lat_t * pLat, * pRing, * pPrev;
+    pRing = Seq_NodeGetRing( pObj, Edge );
+    pLat  = Seq_NodeCreateLat( pObj );
+    if ( pRing == NULL )
+    {
+        Seq_LatSetPrev( pLat, pLat );
+        Seq_LatSetNext( pLat, pLat );
+        Seq_NodeSetRing( pObj, Edge, pLat );
+    }
+    else
+    {
+        pPrev = Seq_LatPrev( pRing );
+        Seq_LatSetPrev( pLat, pPrev );
+        Seq_LatSetNext( pPrev, pLat );
+        Seq_LatSetPrev( pRing, pLat );
+        Seq_LatSetNext( pLat, pRing );
+    }
+    Seq_LatSetInit( pLat, Init );
+    Seq_ObjAddFaninL( pObj, Edge, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Delete the first Lat on the edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_InitType_t Seq_NodeDeleteFirst( Abc_Obj_t * pObj, int Edge )  
+{ 
+    Abc_InitType_t Init;
+    Seq_Lat_t * pLat, * pRing, * pPrev, * pNext;
+    pRing = Seq_NodeGetRing( pObj, Edge );
+    pLat  = pRing; // consider the first latch
+    if ( pLat->pNext == pLat )
+        Seq_NodeSetRing( pObj, Edge, NULL );
+    else
+    {
+        pPrev = Seq_LatPrev( pLat );
+        pNext = Seq_LatNext( pLat );
+        Seq_LatSetPrev( pNext, pPrev );
+        Seq_LatSetNext( pPrev, pNext );
+        Seq_NodeSetRing( pObj, Edge, pNext ); // rotate the ring
+    }
+    Init = Seq_LatInit( pLat );
+    Seq_NodeRecycleLat( pObj, pLat );
+    Seq_ObjAddFaninL( pObj, Edge, -1 );
+    return Init;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Delete the last Lat on the edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_InitType_t Seq_NodeDeleteLast( Abc_Obj_t * pObj, int Edge )  
+{
+    Abc_InitType_t Init;
+    Seq_Lat_t * pLat, * pRing, * pPrev, * pNext;
+    pRing = Seq_NodeGetRing( pObj, Edge );
+    pLat  = Seq_LatPrev( pRing ); // consider the last latch
+    if ( pLat->pNext == pLat )
+        Seq_NodeSetRing( pObj, Edge, NULL );
+    else
+    {
+        pPrev = Seq_LatPrev( pLat );
+        pNext = Seq_LatNext( pLat );
+        Seq_LatSetPrev( pNext, pPrev );
+        Seq_LatSetNext( pPrev, pNext );
+    }
+    Init = Seq_LatInit( pLat );
+    Seq_NodeRecycleLat( pObj, pLat ); 
+    Seq_ObjAddFaninL( pObj, Edge, -1 );
+    return Init;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Insert the last Lat on the edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodeDupLats( Abc_Obj_t * pObjNew, Abc_Obj_t * pObj, int Edge )  
+{ 
+    Seq_Lat_t * pRing, * pLat;
+    int i, nLatches;
+    pRing = Seq_NodeGetRing( pObj, Edge );
+    if ( pRing == NULL )
+        return;
+    nLatches = Seq_NodeCountLats( pObj, Edge );
+    for ( i = 0, pLat = pRing; i < nLatches; i++, pLat = pLat->pNext )
+        Seq_NodeInsertLast( pObjNew, Edge, Seq_LatInit(pLat) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Insert the last Lat on the edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NodeCompareLats( Abc_Obj_t * pObj1, int Edge1, Abc_Obj_t * pObj2, int Edge2 )  
+{ 
+    Seq_Lat_t * pRing1, * pRing2, * pLat1, * pLat2;
+    int i, nLatches1, nLatches2;
+
+    nLatches1 = Seq_NodeCountLats( pObj1, Edge1 );
+    nLatches2 = Seq_NodeCountLats( pObj2, Edge2 );
+    if ( nLatches1 != nLatches2 )
+        return 0;
+
+    pRing1 = Seq_NodeGetRing( pObj1, Edge1 );
+    pRing2 = Seq_NodeGetRing( pObj2, Edge2 );
+    for ( i = 0, pLat1 = pRing1, pLat2 = pRing2; i < nLatches1; i++, pLat1 = pLat1->pNext, pLat2 = pLat2->pNext )
+        if ( Seq_LatInit(pLat1) != Seq_LatInit(pLat2) )
+            return 0;
+
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqMan.c b/src/base/seq/seqMan.c
new file mode 100644
index 00000000..bdfb2630
--- /dev/null
+++ b/src/base/seq/seqMan.c
@@ -0,0 +1,133 @@
+/**CFile****************************************************************
+
+  FileName    [seqMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [Manager of sequential AIG containing.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates sequential AIG manager.]
+
+  Description [The manager contains all the data structures needed to 
+  represent sequential AIG and compute stand-alone retiming as well as 
+  the integrated mapping/retiming of the sequential AIG.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Seq_t * Seq_Create( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * p;
+    // start the manager
+    p = ALLOC( Abc_Seq_t, 1 );
+    memset( p, 0, sizeof(Abc_Seq_t) );
+    p->pNtk  = pNtk;
+    p->nSize = 1000;
+    p->nMaxIters = 15;
+    p->pMmInits  = Extra_MmFixedStart( sizeof(Seq_Lat_t) );
+    p->fEpsilon  = (float)0.001;
+    // create internal data structures
+    p->vNums     = Vec_IntStart( 2 * p->nSize ); 
+    p->vInits    = Vec_PtrStart( 2 * p->nSize ); 
+    p->vLValues  = Vec_IntStart( p->nSize ); 
+    p->vLags     = Vec_StrStart( p->nSize ); 
+    p->vLValuesN = Vec_IntStart( p->nSize ); 
+    p->vAFlows   = Vec_IntStart( p->nSize ); 
+    p->vLagsN    = Vec_StrStart( p->nSize ); 
+    p->vUses     = Vec_StrStart( p->nSize ); 
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates sequential AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_Resize( Abc_Seq_t * p, int nMaxId )
+{
+    if ( p->nSize > nMaxId )
+        return;
+    p->nSize = nMaxId + 1;
+    Vec_IntFill( p->vNums,     2 * p->nSize, 0 ); 
+    Vec_PtrFill( p->vInits,    2 * p->nSize, NULL ); 
+    Vec_IntFill( p->vLValues,  p->nSize, 0 ); 
+    Vec_StrFill( p->vLags,     p->nSize, 0 ); 
+    Vec_IntFill( p->vLValuesN, p->nSize, 0 ); 
+    Vec_IntFill( p->vAFlows,   p->nSize, 0 ); 
+    Vec_StrFill( p->vLagsN,    p->nSize, 0 ); 
+    Vec_StrFill( p->vUses,     p->nSize, 0 ); 
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates sequential AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_Delete( Abc_Seq_t * p )
+{
+    if ( p->fStandCells && p->vMapAnds )
+    {
+        void * pVoid; int i;
+        Vec_PtrForEachEntry( p->vMapAnds, pVoid, i )
+            free( pVoid );
+    }
+    if ( p->vMapDelays )  Vec_VecFree( p->vMapDelays );  // the nodes used in the mapping
+    if ( p->vMapFanins )  Vec_VecFree( p->vMapFanins );  // the cuts used in the mapping
+    if ( p->vMapAnds )    Vec_PtrFree( p->vMapAnds );    // the nodes used in the mapping
+    if ( p->vMapCuts )    Vec_VecFree( p->vMapCuts );    // the cuts used in the mapping
+    if ( p->vLValues )    Vec_IntFree( p->vLValues );    // the arrival times (L-Values of nodes)
+    if ( p->vLags )       Vec_StrFree( p->vLags );       // the lags of the mapped nodes
+    if ( p->vLValuesN )   Vec_IntFree( p->vLValuesN );   // the arrival times (L-Values of nodes)
+    if ( p->vAFlows )     Vec_IntFree( p->vAFlows );     // the arrival times (L-Values of nodes)
+    if ( p->vLagsN )      Vec_StrFree( p->vLagsN );      // the lags of the mapped nodes
+    if ( p->vUses )       Vec_StrFree( p->vUses );       // the uses of phases
+    if ( p->vInits )      Vec_PtrFree( p->vInits );      // the initial values of the latches
+    if ( p->vNums )       Vec_IntFree( p->vNums );       // the numbers of latches
+    Extra_MmFixedStop( p->pMmInits );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqMapCore.c b/src/base/seq/seqMapCore.c
new file mode 100644
index 00000000..c465f31f
--- /dev/null
+++ b/src/base/seq/seqMapCore.c
@@ -0,0 +1,652 @@
+/**CFile****************************************************************
+
+  FileName    [seqMapCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [The core of SC mapping/retiming package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqMapCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+#include "main.h"
+#include "mio.h"
+#include "mapper.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern Abc_Ntk_t *  Seq_NtkMapDup( Abc_Ntk_t * pNtk );
+extern int          Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose );
+extern Abc_Ntk_t *  Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk );
+
+static int          Seq_MapMappingCount( Abc_Ntk_t * pNtk );
+static int          Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
+static Abc_Obj_t *  Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int fCompl, int LagCut, Vec_Ptr_t * vLeaves, unsigned uPhase );
+static DdNode *     Seq_MapMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
+static void         Seq_MapMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges );
+static void         Seq_MapMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
+static DdNode *     Seq_MapMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs Map mapping and retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Ntk_t * pNtkMap;
+    int RetValue;
+
+    // derive the supergate library
+    if ( Abc_FrameReadLibSuper() == NULL && Abc_FrameReadLibGen() )
+    {
+        printf( "A simple supergate library is derived from gate library \"%s\".\n", 
+            Mio_LibraryReadName(Abc_FrameReadLibGen()) );
+        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen() );
+    }
+    p->pSuperLib   = Abc_FrameReadLibSuper();
+    p->nVarsMax    = Map_SuperLibReadVarsMax(p->pSuperLib);
+    p->nMaxIters   = nMaxIters;
+    p->fStandCells = 1;
+
+    // find the best mapping and retiming for all nodes (p->vLValues, p->vBestCuts, p->vLags)
+    if ( !Seq_MapRetimeDelayLags( pNtk, fVerbose ) )
+        return NULL;
+    if ( RetValue = Abc_NtkGetChoiceNum(pNtk) )
+    {
+        printf( "The network has %d choices. The resulting network is not derived (this is temporary).\n", RetValue );
+        printf( "The mininum clock period computed is %5.2f.\n", p->FiBestFloat );
+        return NULL;
+    }
+    printf( "The mininum clock period computed is %5.2f.\n", p->FiBestFloat );
+    printf( "The resulting network is derived as BDD logic network (this is temporary).\n" );
+
+    // duplicate the nodes contained in multiple cuts
+    pNtkNew = Seq_NtkMapDup( pNtk );
+    
+    // implement the retiming
+    RetValue = Seq_NtkImplementRetiming( pNtkNew, ((Abc_Seq_t *)pNtkNew->pManFunc)->vLags, fVerbose );
+    if ( RetValue == 0 )
+        printf( "Retiming completed but initial state computation has failed.\n" );
+
+    // check the compatibility of initial states computed
+    if ( RetValue = Seq_NtkMapInitCompatible( pNtkNew, fVerbose ) )
+        printf( "The number of LUTs with incompatible edges = %d.\n", RetValue );
+//    return pNtkNew;
+
+    // create the final mapped network
+    pNtkMap = Seq_NtkSeqMapMapped( pNtkNew );
+    Abc_NtkDelete( pNtkNew );
+    return pNtkMap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the network by duplicating some of the nodes.]
+
+  Description [Information about mapping is given as mapping nodes (p->vMapAnds)
+  and best cuts for each node (p->vMapCuts).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * pNew, * p = pNtk->pManFunc;
+    Seq_Match_t * pMatch;
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pFanin, * pFaninNew, * pLeaf;
+    Vec_Ptr_t * vLeaves;
+    unsigned SeqEdge;
+    int i, k, nObjsNew, Lag;
+    
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    // start the expanded network
+    pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
+    Abc_NtkCleanNext(pNtk);
+
+    // start the new sequential AIG manager
+    nObjsNew = 1 + Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk) + Seq_MapMappingCount(pNtk);
+    Seq_Resize( pNtkNew->pManFunc, nObjsNew );
+
+    // duplicate the nodes in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+//        Abc_NtkDupObj( pNtkNew, pMatch->pAnd );
+        if ( !pMatch->fCompl )
+            pMatch->pAnd->pCopy = Abc_NtkCreateNode( pNtkNew );
+        else
+            pMatch->pAnd->pNext = Abc_NtkCreateNode( pNtkNew );
+    }
+
+    // compute the real phase assignment
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        pMatch->uPhaseR = 0;
+        // get the leaves of the cut
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // convert the leaf nodes
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+
+            // set the phase
+            if ( pMatch->uPhase & (1 << k) ) // neg is required
+            {
+                if ( pLeaf->pNext ) // neg is available
+                    pMatch->uPhaseR |= (1 << k); // neg is used
+//                else
+//                    Seq_NodeSetLag( pLeaf, Seq_NodeGetLagN(pLeaf) );
+            }
+            else // pos is required
+            {
+                if ( pLeaf->pCopy == NULL ) // pos is not available
+                    pMatch->uPhaseR |= (1 << k); // neg is used
+//                else
+//                    Seq_NodeSetLagN( pLeaf, Seq_NodeGetLag(pLeaf) );
+            }
+        }
+    }
+
+
+    // recursively construct the internals of each node
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+//        if ( pMatch->pSuper == NULL )
+//        {
+//            int x = 0;
+//        }
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        if ( !pMatch->fCompl )
+            Seq_MapMappingBuild_rec( pNtkNew, pNtk, pMatch->pAnd->Id << 8, 1, pMatch->fCompl, Seq_NodeGetLag(pMatch->pAnd), vLeaves, pMatch->uPhaseR );
+        else
+            Seq_MapMappingBuild_rec( pNtkNew, pNtk, pMatch->pAnd->Id << 8, 1, pMatch->fCompl, Seq_NodeGetLagN(pMatch->pAnd), vLeaves, pMatch->uPhaseR );
+    }
+    assert( nObjsNew == pNtkNew->nObjs );
+
+    // set the POs
+//    Abc_NtkFinalize( pNtk, pNtkNew );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        if ( Abc_ObjFaninC0(pObj) )
+            pFaninNew = pFanin->pNext ? pFanin->pNext : pFanin->pCopy;
+        else
+            pFaninNew = pFanin->pCopy ? pFanin->pCopy : pFanin->pNext;
+        pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+
+    // duplicate the latches on the PO edges
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_NodeDupLats( pObj->pCopy, pObj, 0 );
+
+    // transfer the mapping info to the new manager
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        // get the leaves of the cut
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // convert the leaf nodes
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+
+//            Lag = (SeqEdge & 255) + Seq_NodeGetLag(pMatch->pAnd) - Seq_NodeGetLag(pLeaf);
+            Lag = (SeqEdge & 255) + 
+                (pMatch->fCompl?                     Seq_NodeGetLagN(pMatch->pAnd) : Seq_NodeGetLag(pMatch->pAnd)) - 
+                (((pMatch->uPhaseR & (1 << k)) > 0)? Seq_NodeGetLagN(pLeaf)        : Seq_NodeGetLag(pLeaf)       );
+
+            assert( Lag >= 0 );
+
+            // translate the old leaf into the leaf in the new network
+//            if ( pMatch->uPhase & (1 << k) ) // negative phase is required
+//                pFaninNew = pLeaf->pNext? pLeaf->pNext : pLeaf->pCopy;
+//            else // positive phase is required
+//                pFaninNew = pLeaf->pCopy? pLeaf->pCopy : pLeaf->pNext;
+
+            // translate the old leaf into the leaf in the new network
+            if ( pMatch->uPhaseR & (1 << k) ) // negative phase is required
+                pFaninNew = pLeaf->pNext;
+            else // positive phase is required
+                pFaninNew = pLeaf->pCopy;
+
+            Vec_PtrWriteEntry( vLeaves, k, (void *)((pFaninNew->Id << 8) | Lag) );
+//            printf( "%d -> %d\n", pLeaf->Id, pLeaf->pCopy->Id );
+
+            // UPDATE PHASE!!!   leaving only those bits that require inverters
+        }
+        // convert the root node
+//        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
+        pMatch->pAnd = pMatch->fCompl? pMatch->pAnd->pNext : pMatch->pAnd->pCopy;
+    }
+    pNew = pNtkNew->pManFunc;
+    pNew->nVarsMax    = p->nVarsMax;
+    pNew->vMapAnds    = p->vMapAnds;     p->vMapAnds    = NULL;
+    pNew->vMapCuts    = p->vMapCuts;     p->vMapCuts    = NULL;
+    pNew->fStandCells = p->fStandCells;  p->fStandCells = 0;
+
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Seq_NtkMapDup(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the initial states are compatible.]
+
+  Description [Checks of all the initial states on the fanins edges
+  of the cut have compatible number of latches and initial states.
+  If this is not true, then the mapped network with the does not have initial 
+  state. Returns the number of LUTs with incompatible edges.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Seq_Match_t * pMatch;
+    Abc_Obj_t * pAnd, * pLeaf, * pFanout0, * pFanout1;
+    Vec_Vec_t * vTotalEdges;
+    Vec_Ptr_t * vLeaves, * vEdges;
+    int i, k, m, Edge0, Edge1, nLatchAfter, nLatches1, nLatches2;
+    unsigned SeqEdge;
+    int CountBad = 0, CountAll = 0;
+
+    vTotalEdges = Vec_VecStart( p->nVarsMax );
+    // go through all the nodes (cuts) used in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        pAnd = pMatch->pAnd;
+//        printf( "*** Node %d.\n", pAnd->Id );
+
+        // get the cut of this gate
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+
+        // get the edges pointing to the leaves
+        Vec_VecClear( vTotalEdges );
+        Seq_MapMappingEdges_rec( pNtk, pAnd->Id << 8, NULL, vLeaves, vTotalEdges );
+
+        // for each leaf, consider its edges
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+            nLatchAfter = SeqEdge & 255;
+            if ( nLatchAfter == 0 )
+                continue;
+
+            // go through the edges
+            vEdges = Vec_VecEntry( vTotalEdges, k );
+            pFanout0 = NULL;
+            Vec_PtrForEachEntry( vEdges, pFanout1, m )
+            {
+                Edge1    = Abc_ObjIsComplement(pFanout1);
+                pFanout1 = Abc_ObjRegular(pFanout1);
+//printf( "Fanin = %d. Fanout = %d.\n", pLeaf->Id, pFanout1->Id );
+
+                // make sure this is the same fanin
+                if ( Edge1 )
+                    assert( pLeaf == Abc_ObjFanin1(pFanout1) );
+                else
+                    assert( pLeaf == Abc_ObjFanin0(pFanout1) );
+
+                // save the first one
+                if ( pFanout0 == NULL )
+                {
+                    pFanout0 = pFanout1;
+                    Edge0    = Edge1;
+                    continue;
+                }
+                // compare the rings
+                // if they have different number of latches, this is the bug
+                nLatches1 = Seq_NodeCountLats(pFanout0, Edge0);
+                nLatches2 = Seq_NodeCountLats(pFanout1, Edge1);
+                assert( nLatches1 == nLatches2 );
+                assert( nLatches1 == nLatchAfter );
+                assert( nLatches1 > 0 );
+
+                // if they have different initial states, this is the problem
+                if ( !Seq_NodeCompareLats(pFanout0, Edge0, pFanout1, Edge1) )
+                {
+                    CountBad++;
+                    break;
+                }
+                CountAll++;
+            }
+        }
+    }
+    if ( fVerbose )
+        printf( "The number of pairs of edges checked = %d.\n", CountAll );
+    Vec_VecFree( vTotalEdges );
+    return CountBad;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the final mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Seq_Match_t * pMatch;
+    Abc_Ntk_t * pNtkMap; 
+    Vec_Ptr_t * vLeaves;
+    Abc_Obj_t * pObj, * pFaninNew;
+    Seq_Lat_t * pRing;
+    int i;
+
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    // start the network
+    pNtkMap = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+
+    // duplicate the nodes used in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+        pMatch->pAnd->pCopy = Abc_NtkCreateNode( pNtkMap );
+
+    // create and share the latches
+    Seq_NtkShareLatchesMapping( pNtkMap, pNtk, p->vMapAnds, 0 );
+
+    // connect the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        pObj = pMatch->pAnd;
+        // get the leaves of this gate
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // get the BDD of the node
+        pObj->pCopy->pData = Seq_MapMappingConnectBdd_rec( pNtk, pObj->Id << 8, NULL, -1, pObj, vLeaves );
+        Cudd_Ref( pObj->pCopy->pData );
+        // complement the BDD of the cut if it came from the opposite polarity choice cut
+//        if ( Vec_StrEntry(p->vPhase, i) )
+//            pObj->pCopy->pData = Cudd_Not( pObj->pCopy->pData );
+    }
+
+    // set the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        if ( pRing = Seq_NodeGetRing(pObj,0) )
+            pFaninNew = pRing->pLatch;
+        else
+            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
+        pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+
+    // add the latches and their names
+    Abc_NtkAddDummyBoxNames( pNtkMap );
+    Abc_NtkOrderCisCos( pNtkMap );
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkMap, 1 );
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtkMap );
+    if ( !Abc_NtkCheck( pNtkMap ) )
+        fprintf( stdout, "Seq_NtkSeqFpgaMapped(): Network check has failed.\n" );
+    return pNtkMap;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nodes in the bag.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapMappingCount( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Vec_Ptr_t * vLeaves;
+    Seq_Match_t * pMatch;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        Counter += Seq_MapMappingCount_rec( pNtk, pMatch->pAnd->Id << 8, vLeaves );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nodes in the bag.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj, * pLeaf;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+            return 0;
+    // continue unfolding
+    assert( Abc_AigNodeIsAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children
+    return 1 + Seq_MapMappingCount_rec( pNtk, SeqEdge0, vLeaves ) + 
+        Seq_MapMappingCount_rec( pNtk, SeqEdge1, vLeaves );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int fCompl, int LagCut, Vec_Ptr_t * vLeaves, unsigned uPhase )
+{
+    Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+//            if ( uPhase & (1 << i) ) // negative phase is required
+//                return pObj->pNext? pObj->pNext : pObj->pCopy;
+//            else // positive phase is required
+//                return pObj->pCopy? pObj->pCopy : pObj->pNext;
+
+            if ( uPhase & (1 << i) ) // negative phase is required
+                return pObj->pNext;
+            else // positive phase is required
+                return pObj->pCopy;
+        }
+    // continue unfolding
+    assert( Abc_AigNodeIsAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children    
+    pObjNew = fTop? (fCompl? pObj->pNext : pObj->pCopy) : Abc_NtkCreateNode( pNtkNew );
+    // solve subproblems
+    pFaninNew0 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, fCompl, LagCut, vLeaves, uPhase );
+    pFaninNew1 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, fCompl, LagCut, vLeaves, uPhase );
+    // add the fanins to the node
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) );
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) );
+    Seq_NodeDupLats( pObjNew, pObj, 0 );
+    Seq_NodeDupLats( pObjNew, pObj, 1 );
+    // set the lag of the new node equal to the internal lag plus mapping/retiming lag
+    Seq_NodeSetLag( pObjNew, (char)(Lag + LagCut) );
+//    Seq_NodeSetLag( pObjNew, (char)(Lag) );
+    return pObjNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_MapMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges )
+{
+    Abc_Obj_t * pObj, * pLeaf;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+            assert( pPrev != NULL );
+            Vec_VecPush( vMapEdges, i, pPrev );
+            return;
+        }
+    }
+    // continue unfolding
+    assert( Abc_AigNodeIsAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children    
+    Seq_MapMappingEdges_rec( pNtk, SeqEdge0, pObj            , vLeaves, vMapEdges );
+    Seq_MapMappingEdges_rec( pNtk, SeqEdge1, Abc_ObjNot(pObj), vLeaves, vMapEdges );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Seq_MapMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves )
+{
+    Seq_Lat_t * pRing;
+    Abc_Obj_t * pObj, * pLeaf, * pFanin, * pFaninNew;
+    unsigned SeqEdge0, SeqEdge1;
+    DdManager * dd = pRoot->pCopy->pNtk->pManFunc;
+    DdNode * bFunc, * bFunc0, * bFunc1;
+    int Lag, i, k;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, add the connection and return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+            assert( pPrev != NULL );
+            if ( pRing = Seq_NodeGetRing(pPrev,Edge) )
+                pFaninNew = pRing->pLatch;
+            else
+                pFaninNew = Abc_ObjFanin(pPrev,Edge)->pCopy;
+
+            // check if the root already has this fanin
+            Abc_ObjForEachFanin( pRoot->pCopy, pFanin, k )
+                if ( pFanin == pFaninNew )
+                    return Cudd_bddIthVar( dd, k );
+            Abc_ObjAddFanin( pRoot->pCopy, pFaninNew );
+            return Cudd_bddIthVar( dd, k );
+        }
+    }
+    // continue unfolding
+    assert( Abc_AigNodeIsAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children    
+    bFunc0 = Seq_MapMappingConnectBdd_rec( pNtk, SeqEdge0, pObj, 0, pRoot, vLeaves );    Cudd_Ref( bFunc0 );
+    bFunc1 = Seq_MapMappingConnectBdd_rec( pNtk, SeqEdge1, pObj, 1, pRoot, vLeaves );    Cudd_Ref( bFunc1 );
+    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pObj) );
+    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pObj) );
+    // get the BDD of the node
+    bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );  Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( dd, bFunc0 );
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    // return the BDD
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqMapIter.c b/src/base/seq/seqMapIter.c
new file mode 100644
index 00000000..30333cea
--- /dev/null
+++ b/src/base/seq/seqMapIter.c
@@ -0,0 +1,623 @@
+/**CFile****************************************************************
+
+  FileName    [seqMapIter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [Iterative delay computation in SC mapping/retiming package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqMapIter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+#include "main.h"
+#include "mio.h"
+#include "mapperInt.h"
+
+// the internal procedures
+static float Seq_MapRetimeDelayLagsInternal( Abc_Ntk_t * pNtk, int fVerbose );
+static float Seq_MapRetimeSearch_rec( Abc_Ntk_t * pNtk, float FiMin, float FiMax, float Delta, int fVerbose );
+static int   Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose );
+static int   Seq_MapNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, float DelayInv );
+static float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMapping, Vec_Vec_t * vMapCuts );
+static void  Seq_MapCanonicizeTruthTables( Abc_Ntk_t * pNtk );
+
+extern Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the retiming lags for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Cut_Params_t Params, * pParams = &Params;
+    Abc_Obj_t * pObj;
+    float TotalArea;
+    int i, clk;
+
+    // set defaults for cut computation
+    memset( pParams, 0, sizeof(Cut_Params_t) );
+    pParams->nVarsMax  = p->nVarsMax;  // the max cut size ("k" of the k-feasible cuts)
+    pParams->nKeepMax  = 1000;  // the max number of cuts kept at a node
+    pParams->fTruth    = 1;     // compute truth tables
+    pParams->fFilter   = 1;     // filter dominated cuts
+    pParams->fSeq      = 1;     // compute sequential cuts
+    pParams->fVerbose  = fVerbose;     // the verbosiness flag
+
+    // compute the cuts
+clk = clock();
+    p->pCutMan = Abc_NtkSeqCuts( pNtk, pParams );
+p->timeCuts = clock() - clk;
+    if ( fVerbose )
+        Cut_ManPrintStats( p->pCutMan );
+
+    // compute canonical forms of the truth tables of the cuts
+    Seq_MapCanonicizeTruthTables( pNtk );
+
+    // compute area flows
+//    Seq_MapComputeAreaFlows( pNtk, fVerbose );
+
+    // compute the delays
+clk = clock();
+    p->FiBestFloat = Seq_MapRetimeDelayLagsInternal( pNtk, fVerbose );
+    if ( p->FiBestFloat == 0.0 )
+        return 0;
+p->timeDelay = clock() - clk;
+/*
+    {
+        FILE * pTable;
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  pNtk->pName );
+        fprintf( pTable, "%.2f ", p->FiBestFloat );
+        fprintf( pTable, "%.2f ", (float)(p->timeCuts)/(float)(CLOCKS_PER_SEC) );
+        fprintf( pTable, "%.2f ", (float)(p->timeDelay)/(float)(CLOCKS_PER_SEC) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+    }
+*/
+    // clean the marks
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        assert( !pObj->fMarkA && !pObj->fMarkB );
+
+    // collect the nodes and cuts used in the mapping
+    p->vMapAnds = Vec_PtrAlloc( 1000 );
+    p->vMapCuts = Vec_VecAlloc( 1000 );
+    TotalArea = 0.0;
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        TotalArea += Seq_MapCollectNode_rec( Abc_ObjChild0(pObj), p->FiBestFloat, p->vMapAnds, p->vMapCuts );
+
+    // clean the marks
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->fMarkA = pObj->fMarkB = 0;
+
+    if ( fVerbose )
+        printf( "Total area = %6.2f.\n", TotalArea );
+
+    // remove the cuts
+    Cut_ManStop( p->pCutMan );
+    p->pCutMan = NULL;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retimes AIG for optimal delay using Pan's algorithm.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Seq_MapRetimeDelayLagsInternal( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Obj_t * pNode;
+    float FiMax, FiBest, Delta;
+    int i, RetValue;
+    char NodeLag;
+
+    assert( Abc_NtkIsSeq( pNtk ) );
+
+    // assign the accuracy for min-period computation
+    Delta = Mio_LibraryReadDelayNand2Max(Abc_FrameReadLibGen());
+    if ( Delta == 0.0 )
+    {
+        Delta = Mio_LibraryReadDelayAnd2Max(Abc_FrameReadLibGen());
+        if ( Delta == 0.0 )
+        {
+            printf( "Cannot retime/map if the library does not have NAND2 or AND2.\n" );
+            return 0.0;
+        }
+    }
+
+    // get the upper bound on the clock period
+    FiMax = Delta * (5 + Seq_NtkLevelMax(pNtk));
+    Delta /= 2;
+
+    // make sure this clock period is feasible
+    if ( !Seq_MapRetimeForPeriod( pNtk, FiMax, fVerbose ) )
+    {
+        Vec_StrFill( p->vLags, p->nSize, 0 );
+        Vec_StrFill( p->vLagsN, p->nSize, 0 );
+        printf( "Error: The upper bound on the clock period cannot be computed.\n" );
+        printf( "The reason for this error may be the presence in the circuit of logic\n" );
+        printf( "that is not reachable from the PIs. Mapping/retiming is not performed.\n" );
+        return 0;
+    }
+
+    // search for the optimal clock period between 0 and nLevelMax
+    FiBest = Seq_MapRetimeSearch_rec( pNtk, 0.0, FiMax, Delta, fVerbose );
+
+    // recompute the best l-values
+    RetValue = Seq_MapRetimeForPeriod( pNtk, FiBest, fVerbose );
+    assert( RetValue );
+
+    // fix the problem with non-converged delays
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        if ( Seq_NodeGetLValueP(pNode) < -ABC_INFINITY/2 )
+            Seq_NodeSetLValueP( pNode, 0 );
+        if ( Seq_NodeGetLValueN(pNode) < -ABC_INFINITY/2 )
+            Seq_NodeSetLValueN( pNode, 0 );
+    }
+
+    // write the retiming lags for both phases of each node
+    Vec_StrFill( p->vLags,  p->nSize, 0 );
+    Vec_StrFill( p->vLagsN, p->nSize, 0 );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueP(pNode), FiBest );
+        Seq_NodeSetLag( pNode, NodeLag );
+        NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueN(pNode), FiBest );
+        Seq_NodeSetLagN( pNode, NodeLag );
+//printf( "%6d=(%d,%d) ", pNode->Id, Seq_NodeGetLag(pNode), Seq_NodeGetLagN(pNode) );
+//        if ( Seq_NodeGetLag(pNode) != Seq_NodeGetLagN(pNode) )
+//        {
+//printf( "%6d=(%d,%d) ", pNode->Id, Seq_NodeGetLag(pNode), Seq_NodeGetLagN(pNode) );
+//        }
+    }
+//printf( "\n\n" );
+
+    // print the result
+    if ( fVerbose )
+    printf( "The best clock period after mapping/retiming is %6.2f.\n", FiBest );
+    return FiBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs binary search for the optimal clock period.]
+
+  Description [Assumes that FiMin is infeasible while FiMax is feasible.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Seq_MapRetimeSearch_rec( Abc_Ntk_t * pNtk, float FiMin, float FiMax, float Delta, int fVerbose )
+{
+    float Median;
+    assert( FiMin < FiMax );
+    if ( FiMin + Delta >= FiMax )
+        return FiMax;
+    Median = FiMin + (FiMax - FiMin)/2;
+    if ( Seq_MapRetimeForPeriod( pNtk, Median, fVerbose ) )
+        return Seq_MapRetimeSearch_rec( pNtk, FiMin, Median, Delta, fVerbose ); // Median is feasible
+    else 
+        return Seq_MapRetimeSearch_rec( pNtk, Median, FiMax, Delta, fVerbose ); // Median is infeasible
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if retiming with this clock period is feasible.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Obj_t * pObj;
+    float DelayInv = Mio_LibraryReadDelayInvMax(Abc_FrameReadLibGen());
+    int i, c, RetValue, fChange, Counter;
+    char * pReason = "";
+
+    // set l-values of all nodes to be minus infinity
+    Vec_IntFill( p->vLValues,  p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
+    Vec_IntFill( p->vLValuesN, p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
+    Vec_StrFill( p->vUses,     p->nSize, 0 );
+
+    // set l-values of constants and PIs
+    pObj = Abc_NtkObj( pNtk, 0 );
+    Seq_NodeSetLValueP( pObj, 0.0 );
+    Seq_NodeSetLValueN( pObj, 0.0 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        Seq_NodeSetLValueP( pObj, 0.0 );
+        Seq_NodeSetLValueN( pObj, DelayInv );
+    }
+
+    // update all values iteratively
+    Counter = 0;
+    for ( c = 0; c < p->nMaxIters; c++ )
+    {
+        fChange = 0;
+        Abc_AigForEachAnd( pNtk, pObj, i )
+        {
+            Counter++;
+            RetValue = Seq_MapNodeUpdateLValue( pObj, Fi, DelayInv );
+            if ( RetValue == SEQ_UPDATE_YES ) 
+                fChange = 1;
+        }
+        Abc_NtkForEachPo( pNtk, pObj, i )
+        {
+            RetValue = Seq_MapNodeUpdateLValue( pObj, Fi, DelayInv );
+            if ( RetValue == SEQ_UPDATE_FAIL )
+                break;
+        }
+        if ( RetValue == SEQ_UPDATE_FAIL )
+            break;
+        if ( fChange == 0 )
+            break;
+//printf( "\n\n" );
+    }
+    if ( c == p->nMaxIters )
+    {
+        RetValue = SEQ_UPDATE_FAIL;
+        pReason = "(timeout)";
+    }
+    else
+        c++;
+
+    // report the results
+    if ( fVerbose )
+    {
+        if ( RetValue == SEQ_UPDATE_FAIL )
+            printf( "Period = %6.2f.  Iterations = %3d.  Updates = %10d.    Infeasible %s\n", Fi, c, Counter, pReason );
+        else
+            printf( "Period = %6.2f.  Iterations = %3d.  Updates = %10d.      Feasible\n",    Fi, c, Counter );
+    }
+    return RetValue != SEQ_UPDATE_FAIL;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Seq_MapSuperGetArrival( Abc_Obj_t * pObj, float Fi, Seq_Match_t * pMatch, float DelayMax )
+{
+    Abc_Seq_t * p = pObj->pNtk->pManFunc;
+    Abc_Obj_t * pFanin;
+    float lValueCur, lValueMax;
+    int i;
+    lValueMax = -ABC_INFINITY;
+    for ( i = pMatch->pCut->nLeaves - 1; i >= 0; i-- )
+    {
+        // get the arrival time of the fanin
+        pFanin = Abc_NtkObj( pObj->pNtk, pMatch->pCut->pLeaves[i] >> 8 );
+        if ( pMatch->uPhase & (1 << i) )
+            lValueCur = Seq_NodeGetLValueN(pFanin) - Fi * (pMatch->pCut->pLeaves[i] & 255);
+        else
+            lValueCur = Seq_NodeGetLValueP(pFanin) - Fi * (pMatch->pCut->pLeaves[i] & 255);
+        // add the arrival time of this pin
+        if ( lValueMax < lValueCur + pMatch->pSuper->tDelaysR[i].Worst )
+            lValueMax = lValueCur + pMatch->pSuper->tDelaysR[i].Worst;
+        if ( lValueMax < lValueCur + pMatch->pSuper->tDelaysF[i].Worst )
+            lValueMax = lValueCur + pMatch->pSuper->tDelaysF[i].Worst;
+        if ( lValueMax > DelayMax + p->fEpsilon )
+            return ABC_INFINITY;
+    }
+    return lValueMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Seq_MapNodeComputeCut(  Abc_Obj_t * pObj, Cut_Cut_t * pCut, int fCompl, float Fi, Seq_Match_t * pMatchBest )
+{
+    Seq_Match_t Match, * pMatchCur = &Match;
+    Abc_Seq_t * p = pObj->pNtk->pManFunc;
+    Map_Super_t * pSuper, * pSuperList;
+    unsigned uCanon[2];
+    float lValueBest, lValueCur;
+    int i;
+    assert( pCut->nLeaves < 6 );
+    // get the canonical truth table of this cut
+    uCanon[0] = uCanon[1] = (fCompl? pCut->uCanon0 : pCut->uCanon1);
+    if ( uCanon[0] == 0 || ~uCanon[0] == 0 )
+    {
+        if ( pMatchBest )
+        {
+            memset( pMatchBest, 0, sizeof(Seq_Match_t) );
+            pMatchBest->pCut = pCut;
+        }
+        return (float)0.0;
+    }
+    // match the given phase of the cut
+    pSuperList = Map_SuperTableLookupC( p->pSuperLib, uCanon );
+    // compute the arrival times of each supergate
+    lValueBest = ABC_INFINITY;
+    for ( pSuper = pSuperList; pSuper; pSuper = pSuper->pNext )
+    {
+        // create the match
+        pMatchCur->pCut   = pCut;
+        pMatchCur->pSuper = pSuper;
+        // get the phase
+        for ( i = 0; i < (int)pSuper->nPhases; i++ )
+        {
+            pMatchCur->uPhase = (fCompl? pCut->Num0 : pCut->Num1) ^ pSuper->uPhases[i];
+            // find the arrival time of this match
+            lValueCur = Seq_MapSuperGetArrival( pObj, Fi, pMatchCur, lValueBest );
+            if ( lValueBest > lValueCur )//&& lValueCur > -ABC_INFINITY/2 )
+            {
+                lValueBest = lValueCur;
+                if ( pMatchBest )
+                    *pMatchBest = *pMatchCur;
+            }
+        }
+    }
+//    assert( lValueBest < ABC_INFINITY/2 );
+    return lValueBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the node.]
+
+  Description [The node can be internal or a PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Seq_MapNodeComputePhase( Abc_Obj_t * pObj, int fCompl, float Fi, Seq_Match_t * pMatchBest )
+{
+    Seq_Match_t Match, * pMatchCur = &Match;
+    Cut_Cut_t * pList, * pCut;
+    float lValueBest, lValueCut;
+    // get the list of cuts
+    pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj );
+    // get the arrival time of the best non-trivial cut
+    lValueBest = ABC_INFINITY;
+    for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
+    {
+        lValueCut = Seq_MapNodeComputeCut( pObj, pCut, fCompl, Fi, pMatchBest? pMatchCur : NULL );
+        if ( lValueBest > lValueCut )
+        {
+            lValueBest = lValueCut;
+            if ( pMatchBest )
+                *pMatchBest = *pMatchCur;
+        }
+    }
+//    assert( lValueBest < ABC_INFINITY/2 );
+    return lValueBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the node.]
+
+  Description [The node can be internal or a PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, float DelayInv )
+{
+    Abc_Seq_t * p = pObj->pNtk->pManFunc;
+    Cut_Cut_t * pList;
+    char Use;
+    float lValueOld0, lValueOld1, lValue0, lValue1, lValue;
+    assert( !Abc_ObjIsPi(pObj) );
+    assert( Abc_ObjFaninNum(pObj) > 0 );
+    // consider the case of the PO
+    if ( Abc_ObjIsPo(pObj) )
+    {
+        if ( Abc_ObjFaninC0(pObj) ) // PO requires negative polarity
+            lValue = Seq_NodeGetLValueN(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj);
+        else
+            lValue = Seq_NodeGetLValueP(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj);
+        return (lValue > Fi + p->fEpsilon)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO;
+    }
+    // get the cuts
+    pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj );
+    if ( pList == NULL )
+        return SEQ_UPDATE_NO;
+    // compute the arrival time of both phases
+    lValue0 = Seq_MapNodeComputePhase( pObj, 1, Fi, NULL );
+    lValue1 = Seq_MapNodeComputePhase( pObj, 0, Fi, NULL );
+    // consider the case when negative phase is too slow
+    if ( lValue0 > lValue1 + DelayInv + p->fEpsilon )
+        lValue0 = lValue1 + DelayInv, Use = 2;
+    else if ( lValue1 > lValue0 + DelayInv + p->fEpsilon )
+        lValue1 = lValue0 + DelayInv, Use = 1;
+    else
+        Use = 3;
+    // set the uses of the phases
+    Seq_NodeSetUses( pObj, Use );
+    // get the old arrival times
+    lValueOld0 = Seq_NodeGetLValueN(pObj);
+    lValueOld1 = Seq_NodeGetLValueP(pObj);
+    // compare 
+    if ( lValue0 <= lValueOld0 + p->fEpsilon && lValue1 <= lValueOld1 + p->fEpsilon )
+        return SEQ_UPDATE_NO;
+    assert( lValue0 < ABC_INFINITY/2 );
+    assert( lValue1 < ABC_INFINITY/2 );
+    // update the values
+    if ( lValue0 > lValueOld0 + p->fEpsilon )
+        Seq_NodeSetLValueN( pObj, lValue0 );
+    if ( lValue1 > lValueOld1 + p->fEpsilon )
+        Seq_NodeSetLValueP( pObj, lValue1 );
+//printf( "%6d=(%4.2f,%4.2f) ", pObj->Id, Seq_NodeGetLValueP(pObj), Seq_NodeGetLValueN(pObj) );
+    return SEQ_UPDATE_YES;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the parameters of the best mapping/retiming for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMapping, Vec_Vec_t * vMapCuts )
+{
+    Seq_Match_t * pMatch;
+    Abc_Obj_t * pFanin;
+    int k, fCompl, Use;
+    float AreaInv = Mio_LibraryReadAreaInv(Abc_FrameReadLibGen());
+    float Area;
+
+    // get the polarity of the node
+    fCompl = Abc_ObjIsComplement(pAnd);
+    pAnd   = Abc_ObjRegular(pAnd);
+
+    // skip visited nodes
+    if ( !fCompl )
+    {  // need the positive polarity
+        if ( pAnd->fMarkA )
+            return 0.0;
+        pAnd->fMarkA = 1;
+    }
+    else
+    {   // need the negative polarity
+        if ( pAnd->fMarkB )
+            return 0.0;
+        pAnd->fMarkB = 1;
+    }
+
+    // skip if this is a PI or a constant
+    if ( !Abc_AigNodeIsAnd(pAnd) )
+    {
+        if ( Abc_ObjIsPi(pAnd) && fCompl )
+            return AreaInv;   
+        return 0.0;
+    }
+
+    // check the uses of this node
+    Use = Seq_NodeGetUses( pAnd );
+    if ( !fCompl && Use == 1 )  // the pos phase is required; only the neg phase is used
+    {
+        Area = Seq_MapCollectNode_rec( Abc_ObjNot(pAnd), FiBest, vMapping, vMapCuts );
+        return Area + AreaInv; 
+    }
+    if ( fCompl && Use == 2 )  // the neg phase is required; only the pos phase is used
+    {
+        Area = Seq_MapCollectNode_rec( pAnd, FiBest, vMapping, vMapCuts );
+        return Area + AreaInv; 
+    }
+    // both phases are used; the needed one can be selected
+
+    // get the best match
+    pMatch = ALLOC( Seq_Match_t, 1 );
+    memset( pMatch, 1, sizeof(Seq_Match_t) );
+    Seq_MapNodeComputePhase( pAnd, fCompl, FiBest, pMatch );
+    pMatch->pAnd    = pAnd;
+    pMatch->fCompl  = fCompl;
+    pMatch->fCutInv = pMatch->pCut->fCompl;
+    pMatch->PolUse  = Use;
+
+    // call for the fanin cuts
+    Area = pMatch->pSuper? pMatch->pSuper->Area : (float)0.0;
+    for ( k = 0; k < (int)pMatch->pCut->nLeaves; k++ )
+    {
+        pFanin = Abc_NtkObj( pAnd->pNtk, pMatch->pCut->pLeaves[k] >> 8 );
+        if ( pMatch->uPhase & (1 << k) )
+            pFanin = Abc_ObjNot( pFanin ); 
+        Area += Seq_MapCollectNode_rec( pFanin, FiBest, vMapping, vMapCuts );
+    }
+
+    // add this node
+    Vec_PtrPush( vMapping, pMatch );
+    for ( k = 0; k < (int)pMatch->pCut->nLeaves; k++ )
+        Vec_VecPush( vMapCuts, Vec_PtrSize(vMapping)-1, (void *)pMatch->pCut->pLeaves[k] );
+
+    // the cut will become unavailable when the cuts are deallocated
+    pMatch->pCut = NULL;
+
+    return Area;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the canonical versions of the truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_MapCanonicizeTruthTables( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    Cut_Cut_t * pCut, * pList;
+    int i;
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj );
+        if ( pList == NULL )
+            continue;
+        for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
+            Cut_TruthNCanonicize( pCut );
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqMaxMeanCycle.c b/src/base/seq/seqMaxMeanCycle.c
new file mode 100644
index 00000000..46d73cbd
--- /dev/null
+++ b/src/base/seq/seqMaxMeanCycle.c
@@ -0,0 +1,567 @@
+/**CFile****************************************************************
+
+  FileName    [seqMaxMeanCycle.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [Efficient computation of maximum mean cycle times.]
+
+  Author      [Aaron P. Hurst]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 15, 2006.]
+
+  Revision    [$Id: seqMaxMeanCycle.c,v 1.00 2005/05/15 00:00:00 ahurst Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+#include "hash.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Abc_ManTime_t_
+{
+    Abc_Time_t     tArrDef;
+    Abc_Time_t     tReqDef;
+    Vec_Ptr_t  *   vArrs;
+    Vec_Ptr_t  *   vReqs;
+};
+
+typedef struct Seq_HowardData_t_
+{
+  char   visited;
+  int    mark;
+  int    policy;
+  float  cycle;
+  float  skew;
+  float  delay;
+} Seq_HowardData_t;
+
+// accessing the arrival and required times of a node
+static inline Abc_Time_t * Abc_NodeArrival( Abc_Obj_t * pNode )  {  return pNode->pNtk->pManTime->vArrs->pArray[pNode->Id];  }
+static inline Abc_Time_t * Abc_NodeRequired( Abc_Obj_t * pNode ) {  return pNode->pNtk->pManTime->vReqs->pArray[pNode->Id];  }
+
+Hash_Ptr_t * Seq_NtkPathDelays( Abc_Ntk_t * pNtk, int fVerbose );
+void Seq_NtkMergePios( Abc_Ntk_t * pNtk, Hash_Ptr_t * hFwdDelays, int fVerbose );
+
+void Seq_NtkHowardLoop( Abc_Ntk_t * pNtk, Hash_Ptr_t * hFwdDelays,
+                        Hash_Ptr_t * hNodeData, int node,
+                        int *howardDepth, float *howardDelay, int *howardSink,
+                        float *maxMeanCycle);
+void Abc_NtkDfsReverse_rec2( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Vec_Ptr_t * vEndpoints );
+
+#define Seq_NtkGetPathDelay( hFwdDelays, from, to ) \
+  (Hash_PtrExists(hFwdDelays, from)?Hash_FltEntry( ((Hash_Flt_t *)Hash_PtrEntry(hFwdDelays, from, 0)), to, 0):0 )
+
+#define HOWARD_EPSILON 1e-3
+#define ZERO_SLOP      1e-5
+#define REMOVE_ZERO_SLOP( x ) \
+  (x = (x > -ZERO_SLOP && x < ZERO_SLOP)?0:x)
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes maximum mean cycle time.]
+
+  Description [Uses Howard's algorithm.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Seq_NtkHoward( Abc_Ntk_t * pNtk, int fVerbose ) {
+
+  Abc_Obj_t *  pObj;
+  Hash_Ptr_t * hFwdDelays;
+  Hash_Flt_t * hOutgoing;
+  Hash_Ptr_Entry_t * pSourceEntry, * pNodeEntry;
+  Hash_Flt_Entry_t * pSinkEntry;
+  int          i, j, iteration = 0;
+  int          source, sink;
+  int          fChanged;
+  int          howardDepth, howardSink = 0;
+  float        delay, howardDelay, t;
+  float        maxMeanCycle = -ABC_INFINITY;
+  Hash_Ptr_t *       hNodeData;
+  Seq_HowardData_t * pNodeData, * pSourceData, * pSinkData;
+
+  // gather timing constraints
+  hFwdDelays = Seq_NtkPathDelays( pNtk, fVerbose );
+  Seq_NtkMergePios( pNtk, hFwdDelays, fVerbose );
+
+  // initialize data, create initial policy
+  hNodeData = Hash_PtrAlloc( hFwdDelays->nSize );
+  Hash_PtrForEachEntry( hFwdDelays, pSourceEntry, i ) {
+    Hash_PtrWriteEntry( hNodeData, pSourceEntry->key, 
+                        (pNodeData = ALLOC(Seq_HowardData_t, 1)) );
+    pNodeData->skew = 0.0;
+    pNodeData->policy = 0;
+    hOutgoing = (Hash_Flt_t *)(pSourceEntry->data);
+    assert(hOutgoing);
+
+    Hash_FltForEachEntry( hOutgoing, pSinkEntry, j ) {
+      sink = pSinkEntry->key;
+      delay = pSinkEntry->data;
+       if (delay > pNodeData->skew) {
+        pNodeData->policy = sink;
+        pNodeData->skew = delay;
+      }
+    }
+  }
+
+  // iteratively refine policy
+  do {
+    iteration++;
+    fChanged = 0;
+    howardDelay = 0.0;
+    howardDepth = 0;
+
+    // reset data
+    Hash_PtrForEachEntry( hNodeData, pNodeEntry, i ) {
+      pNodeData = (Seq_HowardData_t *)pNodeEntry->data;
+      pNodeData->skew = -ABC_INFINITY;
+      pNodeData->cycle = -ABC_INFINITY;
+      pNodeData->mark = 0;
+      pNodeData->visited = 0;
+    }
+
+    // find loops in policy graph
+    Hash_PtrForEachEntry( hNodeData, pNodeEntry, i ) {
+      pNodeData = (Seq_HowardData_t *)(pNodeEntry->data);
+      assert(pNodeData);
+      if (!pNodeData->visited)
+        Seq_NtkHowardLoop( pNtk, hFwdDelays, 
+                           hNodeData, pNodeEntry->key,
+                           &howardDepth, &howardDelay, &howardSink, &maxMeanCycle);
+    }
+
+    if (!howardSink) {
+      return -1;
+    }
+
+    // improve policy by tightening loops
+    Hash_PtrForEachEntry( hFwdDelays, pSourceEntry, i ) {
+      source = pSourceEntry->key;
+      pSourceData = (Seq_HowardData_t *)Hash_PtrEntry( hNodeData, source, 0 );
+      assert(pSourceData);
+      hOutgoing = (Hash_Flt_t *)(pSourceEntry->data);
+      assert(hOutgoing);
+      Hash_FltForEachEntry( hOutgoing, pSinkEntry, j ) {
+        sink = pSinkEntry->key;
+        pSinkData = (Seq_HowardData_t *)Hash_PtrEntry( hNodeData, sink, 0 );
+        assert(pSinkData);
+        delay = pSinkEntry->data;
+        
+        if (pSinkData->cycle > pSourceData->cycle + HOWARD_EPSILON) {
+          fChanged = 1;
+          pSourceData->cycle = pSinkData->cycle;
+          pSourceData->policy = sink;
+        }
+      }
+    }
+
+    // improve policy by correcting skews
+    if (!fChanged) {
+      Hash_PtrForEachEntry( hFwdDelays, pSourceEntry, i ) {
+        source = pSourceEntry->key;
+        pSourceData = (Seq_HowardData_t *)Hash_PtrEntry( hNodeData, source, 0 );
+        assert(pSourceData);
+        hOutgoing = (Hash_Flt_t *)(pSourceEntry->data);
+        assert(hOutgoing);
+        Hash_FltForEachEntry( hOutgoing, pSinkEntry, j ) {
+          sink = pSinkEntry->key;
+          pSinkData = (Seq_HowardData_t *)Hash_PtrEntry( hNodeData, sink, 0 );
+          assert(pSinkData);
+          delay = pSinkEntry->data;
+
+          if (pSinkData->cycle < 0.0 || pSinkData->cycle < pSourceData->cycle)
+            continue;
+
+          t = delay - pSinkData->cycle + pSinkData->skew;
+          if (t > pSourceData->skew + HOWARD_EPSILON) {
+            fChanged = 1;
+            pSourceData->skew = t;
+            pSourceData->policy = sink;
+          }
+        }
+      }
+    }
+
+    if (fVerbose) printf("Iteration %d \t Period = %.2f\n", iteration, maxMeanCycle);
+  } while (fChanged);
+
+  // set global skew, mmct
+  pNodeData = Hash_PtrEntry( hNodeData, -1, 0 );
+  pNtk->globalSkew = -pNodeData->skew;
+  pNtk->maxMeanCycle = maxMeanCycle;
+
+  // set endpoint skews
+  Vec_FltGrow( pNtk->vSkews, Abc_NtkLatchNum( pNtk ) );
+  pNtk->vSkews->nSize =  Abc_NtkLatchNum( pNtk );
+  Abc_NtkForEachLatch( pNtk, pObj, i ) {
+    pNodeData = Hash_PtrEntry( hNodeData, pObj->Id, 0 );
+    // skews are set based on latch # NOT id #
+    Abc_NtkSetLatSkew( pNtk, i, pNodeData->skew );
+  }
+
+  // free node data
+  Hash_PtrForEachEntry( hNodeData, pNodeEntry, i ) {
+    pNodeData = (Seq_HowardData_t *)(pNodeEntry->data);
+    FREE( pNodeData );
+  }
+  Hash_PtrFree(hNodeData);
+
+  // free delay data
+  Hash_PtrForEachEntry( hFwdDelays, pSourceEntry, i ) {
+    Hash_FltFree( (Hash_Flt_t *)(pSourceEntry->data) );
+  }
+  Hash_PtrFree(hFwdDelays);
+
+  return maxMeanCycle;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the mean cycle times of current policy graph.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkHowardLoop( Abc_Ntk_t * pNtk, Hash_Ptr_t * hFwdDelays,
+                        Hash_Ptr_t * hNodeData, int node,
+                        int *howardDepth, float *howardDelay, int *howardSink,
+                        float *maxMeanCycle) {
+  
+  Seq_HowardData_t * pNodeData, *pToData;
+  float delay, t;
+
+  pNodeData = (Seq_HowardData_t *)Hash_PtrEntry( hNodeData, node, 0 );
+  assert(pNodeData);
+  pNodeData->visited = 1;
+  pNodeData->mark = ++(*howardDepth);
+  pNodeData->delay = (*howardDelay);
+  if (pNodeData->policy) {
+    pToData = (Seq_HowardData_t *)Hash_PtrEntry( hNodeData, pNodeData->policy, 0 );
+    assert(pToData);
+    delay = Seq_NtkGetPathDelay( hFwdDelays, node, pNodeData->policy );
+    assert(delay > 0.0);
+    (*howardDelay) += delay;
+    if (pToData->mark) {
+      t = (*howardDelay - pToData->delay) / (*howardDepth - pToData->mark + 1);
+      pNodeData->cycle = t;
+      pNodeData->skew = 0.0;
+      if (*maxMeanCycle < t) {
+        *maxMeanCycle = t;
+        *howardSink = pNodeData->policy;
+      }
+    } else {
+      if(!pToData->visited) {
+        Seq_NtkHowardLoop(pNtk, hFwdDelays, hNodeData, pNodeData->policy,
+                          howardDepth, howardDelay, howardSink, maxMeanCycle);
+      }
+      if(pToData->cycle > 0) {
+        t = delay - pToData->cycle + pToData->skew;
+    pNodeData->skew = t;
+    pNodeData->cycle = pToData->cycle;
+      }
+    }
+  }
+  *howardDelay = pNodeData->delay;
+  pNodeData->mark = 0;
+  --(*howardDepth);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the register-to-register delays.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hash_Ptr_t * Seq_NtkPathDelays( Abc_Ntk_t * pNtk, int fVerbose ) {
+
+  Abc_Time_t * pTime, ** ppTimes;
+  Abc_Obj_t * pObj, * pDriver, * pStart, * pFanout;
+  Vec_Ptr_t * vNodes, * vEndpoints;
+  int i, j, nPaths = 0;
+  Hash_Flt_t *  hOutgoing;
+  Hash_Ptr_t *  hFwdDelays;
+  float     nMaxPath = 0, nSumPath = 0;
+
+  extern void Abc_NtkTimePrepare( Abc_Ntk_t * pNtk );
+  extern void Abc_NodeDelayTraceArrival( Abc_Obj_t * pNode );
+
+  if (fVerbose) printf("Gathering path delays...\n");
+
+  hFwdDelays = Hash_PtrAlloc( Abc_NtkCiNum( pNtk ) );
+
+  assert( Abc_NtkIsMappedLogic(pNtk) );
+
+  Abc_NtkTimePrepare( pNtk );
+  ppTimes = (Abc_Time_t **)pNtk->pManTime->vArrs->pArray;
+  vNodes = Vec_PtrAlloc( 100 );
+  vEndpoints = Vec_PtrAlloc( 100 );
+
+  // set the initial times (i.e. ignore all inputs)
+  Abc_NtkForEachObj( pNtk, pObj, i) {
+    pTime = ppTimes[pObj->Id];
+    pTime->Fall = pTime->Rise = pTime->Worst = -ABC_INFINITY;    
+  }
+
+  // starting at each Ci, compute timing forward
+  Abc_NtkForEachCi( pNtk, pStart, j ) {
+    
+    hOutgoing = Hash_FltAlloc( 10 );
+    Hash_PtrWriteEntry( hFwdDelays, pStart->Id, (void *)(hOutgoing) );
+
+    // seed the starting point of interest
+    pTime = ppTimes[pStart->Id];
+    pTime->Fall = pTime->Rise = pTime->Worst = 0.0;
+
+    // find a DFS ordering from the start
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NodeSetTravIdCurrent( pStart );
+    pObj = Abc_ObjFanout0Ntk(pStart);
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+      Abc_NtkDfsReverse_rec2( pFanout, vNodes, vEndpoints );
+    if ( Abc_ObjIsCo( pStart ) )
+      Vec_PtrPush( vEndpoints, pStart );
+
+    // do timing analysis
+    for ( i = vNodes->nSize-1; i >= 0; --i )
+      Abc_NodeDelayTraceArrival( vNodes->pArray[i] );
+
+    // there is a path to each set of Co endpoints
+    Vec_PtrForEachEntry( vEndpoints, pObj, i )
+    {
+      assert(pObj);
+      assert( Abc_ObjIsCo( pObj ) );
+      pDriver = Abc_ObjFanin0(pObj);
+      pTime   = Abc_NodeArrival(pDriver);
+      if ( pTime->Worst > 0 ) {
+        Hash_FltWriteEntry( hOutgoing, pObj->Id, pTime->Worst );
+        nPaths++;
+        // if (fVerbose) printf("\tpath %d,%d delay = %f\n", pStart->Id, pObj->Id, pTime->Worst);
+        nSumPath += pTime->Worst;
+        if (pTime->Worst > nMaxPath)
+          nMaxPath = pTime->Worst;
+      }
+    }
+
+    // clear the times that were altered
+    for ( i = 0; i < vNodes->nSize; i++ ) {
+      pObj = (Abc_Obj_t *)(vNodes->pArray[i]);
+      pTime = ppTimes[pObj->Id];
+      pTime->Fall = pTime->Rise = pTime->Worst = -ABC_INFINITY;
+    }
+    pTime = ppTimes[pStart->Id];
+    pTime->Fall = pTime->Rise = pTime->Worst = -ABC_INFINITY;
+    
+    Vec_PtrClear( vNodes );
+    Vec_PtrClear( vEndpoints );
+  }
+
+  Vec_PtrFree( vNodes );
+
+  // rezero Cis (note: these should be restored to values if they were nonzero)
+  Abc_NtkForEachCi( pNtk, pObj, i) {
+    pTime = ppTimes[pObj->Id];
+    pTime->Fall = pTime->Rise = pTime->Worst = 0.0;    
+  }
+
+  if (fVerbose) printf("Num. paths = %d\tMax. Path Delay = %.2f\tAvg. Path Delay = %.2f\n", nPaths, nMaxPath, nSumPath / nPaths);
+  return hFwdDelays;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Merges all the Pios together into one ID = -1.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkMergePios( Abc_Ntk_t * pNtk, Hash_Ptr_t * hFwdDelays, 
+                       int fVerbose ) {
+
+  Abc_Obj_t *        pObj;
+  Hash_Flt_Entry_t * pSinkEntry;
+  Hash_Ptr_Entry_t * pSourceEntry;
+  Hash_Flt_t *       hOutgoing, * hPioSource;
+  int                i, j;
+  int                source, sink, nMerges = 0;
+  float              delay = 0, max_delay = 0;
+  Vec_Int_t *        vFreeList;
+
+  vFreeList = Vec_IntAlloc( 10 );
+
+  // create a new "-1" source entry for the Pios
+  hPioSource = Hash_FltAlloc( 100 );
+  Hash_PtrWriteEntry( hFwdDelays, -1, (void *)(hPioSource) );
+
+  // merge all edges with a Pio as a source
+  Abc_NtkForEachPi( pNtk, pObj, i ) {
+    source = pObj->Id;
+    hOutgoing = (Hash_Flt_t *)Hash_PtrEntry( hFwdDelays, source, 0 );
+    if (!hOutgoing) continue;
+
+    Hash_PtrForEachEntry( hOutgoing, pSinkEntry, j ) {
+      nMerges++;
+      sink = pSinkEntry->key;
+      delay = pSinkEntry->data;
+      if (Hash_FltEntry( hPioSource, sink, 1 ) < delay) {
+        Hash_FltWriteEntry( hPioSource, sink, delay );
+      }
+    }
+
+    Hash_FltFree( hOutgoing );
+    Hash_PtrRemove( hFwdDelays, source );
+  }
+
+  // merge all edges with a Pio as a sink
+  Hash_PtrForEachEntry( hFwdDelays, pSourceEntry, i ) {
+    hOutgoing = (Hash_Flt_t *)(pSourceEntry->data);
+    Hash_FltForEachEntry( hOutgoing, pSinkEntry, j ) {
+      sink = pSinkEntry->key;
+      delay = pSinkEntry->data;
+
+      max_delay = -ABC_INFINITY;
+      if (Abc_ObjIsPo( Abc_NtkObj( pNtk, sink ) )) {
+        nMerges++;
+        if (delay > max_delay)
+          max_delay = delay;
+        Vec_IntPush( vFreeList, sink );
+      }
+    }
+    if (max_delay != -ABC_INFINITY)
+      Hash_FltWriteEntry( hOutgoing, -1, delay );
+    // do freeing
+    while( vFreeList->nSize > 0 ) {
+      Hash_FltRemove( hOutgoing, Vec_IntPop( vFreeList ) );
+    }
+  }
+
+  if (fVerbose) printf("Merged %d paths into one Pio node\n", nMerges);
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [This is a modification of routine from abcDfs.c]
+
+  Description [Recursive DFS from a starting point.  Keeps the endpoints.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDfsReverse_rec2( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Vec_Ptr_t * vEndpoints )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    assert( !Abc_ObjIsNet(pNode) );
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // terminate at the Co
+    if ( Abc_ObjIsCo(pNode) ) {
+      Vec_PtrPush( vEndpoints, pNode );
+      return;
+    }
+    assert( Abc_ObjIsNode( pNode ) );
+    // visit the transitive fanin of the node
+    pNode = Abc_ObjFanout0Ntk(pNode);
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+      Abc_NtkDfsReverse_rec2( pFanout, vNodes, vEndpoints );
+    // add the node after the fanins have been added
+    Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts all skews into forward skews 0<skew<T.]
+
+  Description [Can also minimize total skew by changing global skew.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkSkewForward( Abc_Ntk_t * pNtk, float period, int fMinimize ) {
+  
+  Abc_Obj_t * pObj;
+  int         i;
+  float       skew;
+  float       currentSum = 0, bestSum = ABC_INFINITY;
+  float       currentOffset = 0, nextStep, bestOffset = 0;
+  
+  assert( pNtk->vSkews->nSize >= Abc_NtkLatchNum( pNtk )-1 );
+
+  if (fMinimize) {
+    // search all offsets for the one that minimizes sum of skews
+    while(currentOffset < period) {
+      currentSum = 0;
+      nextStep = period;
+      Abc_NtkForEachLatch( pNtk, pObj, i ) {
+        skew = Abc_NtkGetLatSkew( pNtk, i ) + currentOffset;
+        skew = (float)(skew - period*floor(skew/period));
+        currentSum += skew;
+        if (skew > ZERO_SLOP && skew < nextStep) {
+          nextStep = skew;
+        }
+      }
+
+      if (currentSum < bestSum) {
+        bestSum = currentSum;
+        bestOffset = currentOffset;
+      }
+      currentOffset += nextStep;
+    }
+    printf("Offseting all skews by %.2f\n", bestOffset);
+  }
+
+  // convert global skew into forward skew
+  pNtk->globalSkew = pNtk->globalSkew - bestOffset;
+  pNtk->globalSkew = (float)(pNtk->globalSkew - period*floor(pNtk->globalSkew/period));
+  assert(pNtk->globalSkew>= 0 && pNtk->globalSkew < period);
+    
+  // convert endpoint skews into forward skews
+  Abc_NtkForEachLatch( pNtk, pObj, i ) {
+    skew = Abc_NtkGetLatSkew( pNtk, i ) + bestOffset;
+    skew = (float)(skew - period*floor(skew/period));
+    REMOVE_ZERO_SLOP( skew );
+    assert(skew >=0  && skew < period);
+
+    Abc_NtkSetLatSkew( pNtk, i, skew );
+  }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
new file mode 100644
index 00000000..27638644
--- /dev/null
+++ b/src/base/seq/seqRetCore.c
@@ -0,0 +1,492 @@
+/**CFile****************************************************************
+
+  FileName    [seqRetCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [The core of FPGA mapping/retiming package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqRetCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+#include "dec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose );
+static Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop, Vec_Ptr_t * vFanins );
+static Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq );
+static Abc_Obj_t * Seq_EdgeReconstruct_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode );
+static Abc_Obj_t * Seq_EdgeReconstructPO( Abc_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs FPGA mapping and retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose )
+{
+    Abc_Seq_t * p;
+    Abc_Ntk_t * pNtkSeq, * pNtkNew;
+    int RetValue;
+    assert( !Abc_NtkHasAig(pNtk) );
+    // derive the isomorphic seq AIG
+    pNtkSeq = Seq_NtkRetimeDerive( pNtk, fVerbose );
+    p = pNtkSeq->pManFunc;
+    p->nMaxIters = nMaxIters;
+
+    if ( !fInitial )
+        Seq_NtkLatchSetValues( pNtkSeq, ABC_INIT_DC );
+    // find the best mapping and retiming 
+    if ( !Seq_NtkRetimeDelayLags( pNtk, pNtkSeq, fVerbose ) )
+        return NULL;
+
+    // implement the retiming
+    RetValue = Seq_NtkImplementRetiming( pNtkSeq, p->vLags, fVerbose );
+    if ( RetValue == 0 )
+        printf( "Retiming completed but initial state computation has failed.\n" );
+//return pNtkSeq;
+
+    // create the final mapped network
+    pNtkNew = Seq_NtkRetimeReconstruct( pNtk, pNtkSeq );
+    Abc_NtkDelete( pNtkSeq );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the isomorphic seq AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pFanin, * pMirror;
+    Vec_Ptr_t * vMapAnds, * vMirrors;
+    Vec_Vec_t * vMapFanins;
+    int i, k, RetValue, fHasBdds;
+    char * pSop;
+
+    // make sure it is an AIG without self-feeding latches
+    assert( !Abc_NtkHasAig(pNtk) );
+    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) )
+        printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
+    assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
+
+    // remove the dangling nodes
+    Abc_NtkCleanup( pNtk, fVerbose );
+
+    // transform logic functions from BDD to SOP
+    if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Seq_NtkRetimeDerive(): Converting to SOPs has failed.\n" );
+            return NULL;
+        }
+    }
+
+    // start the network
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG, 1 );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+
+    // map the constant nodes
+    Abc_NtkCleanCopy( pNtk );
+    // clone the PIs/POs/latches
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+    // copy the names
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
+
+    // create one AND for each logic node in the topological order
+    vMapAnds = Abc_NtkDfs( pNtk, 0 );
+    Vec_PtrForEachEntry( vMapAnds, pObj, i )
+    {
+        if ( pObj->Id == 0 )
+        {
+            pObj->pCopy = Abc_AigConst1(pNtkNew);
+            continue;
+        }
+        pObj->pCopy = Abc_NtkCreateNode( pNtkNew );
+    }
+
+    // make the new seq AIG point to the old network through pNext
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( pObj->pCopy ) pObj->pCopy->pNext = pObj;
+
+    // make latches point to the latch fanins
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        assert( !Abc_ObjIsLatch(Abc_ObjFanin0(pObj)) );
+        pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
+    }
+
+    // create internal AND nodes w/o strashing for each logic node (including constants)
+    vMapFanins = Vec_VecStart( Vec_PtrSize(vMapAnds) );
+    Vec_PtrForEachEntry( vMapAnds, pObj, i )
+    {
+        // get the SOP of the node
+        if ( Abc_NtkHasMapping(pNtk) )
+            pSop = Mio_GateReadSop(pObj->pData);
+        else
+            pSop = pObj->pData;
+        pFanin = Seq_NodeRetimeDerive( pNtkNew, pObj, pSop, Vec_VecEntry(vMapFanins, i) );
+        Abc_ObjAddFanin( pObj->pCopy, pFanin );
+        Abc_ObjAddFanin( pObj->pCopy, pFanin );
+    }
+    // connect the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
+    
+    // start the storage for initial states
+    p = pNtkNew->pManFunc;
+    Seq_Resize( p, Abc_NtkObjNumMax(pNtkNew) );
+
+    // add the sequential edges
+    Vec_PtrForEachEntry( vMapAnds, pObj, i )
+    {
+        vMirrors = Vec_VecEntry( vMapFanins, i );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            pMirror = Vec_PtrEntry( vMirrors, k );
+            if ( Abc_ObjIsLatch(pFanin) )
+            {
+                Seq_NodeInsertFirst( pMirror, 0, Abc_LatchInit(pFanin) );
+                Seq_NodeInsertFirst( pMirror, 1, Abc_LatchInit(pFanin) );
+            }
+        }
+    }
+    // add the sequential edges to the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        if ( Abc_ObjIsLatch(pFanin) )
+            Seq_NodeInsertFirst( pObj->pCopy, 0, Abc_LatchInit(pFanin) );
+    }
+
+
+    // save the fanin/delay info
+    p->vMapAnds   = vMapAnds;
+    p->vMapFanins = vMapFanins;
+    p->vMapCuts   = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
+    p->vMapDelays = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+    {
+        // change the node to be the new one
+        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
+        // collect the new fanins of this node
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Vec_VecPush( p->vMapCuts, i, (void *)( (pFanin->pCopy->Id << 8) | Abc_ObjIsLatch(pFanin) ) );
+        // collect the delay info
+        if ( !Abc_NtkHasMapping(pNtk) )
+        {
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                Vec_VecPush( p->vMapDelays, i, (void *)Abc_Float2Int(1.0) );
+        }
+        else
+        {
+            Mio_Pin_t * pPin = Mio_GateReadPins(pObj->pData);
+            float Max, tDelayBlockRise, tDelayBlockFall;
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+            {
+                tDelayBlockRise = (float)Mio_PinReadDelayBlockRise( pPin );  
+                tDelayBlockFall = (float)Mio_PinReadDelayBlockFall( pPin ); 
+                Max = ABC_MAX( tDelayBlockRise, tDelayBlockFall );
+                Vec_VecPush( p->vMapDelays, i, (void *)Abc_Float2Int(Max) );
+                pPin = Mio_PinReadNext(pPin);
+            }
+        }
+    }
+
+    // set the cutset composed of latch drivers
+//    Abc_NtkAigCutsetCopy( pNtk );
+//    Seq_NtkLatchGetEqualFaninNum( pNtkNew );
+
+    // convert the network back into BDDs if this is how it was
+    if ( fHasBdds )
+        Abc_NtkSopToBdd(pNtk);
+
+    // copy EXDC and check correctness
+    if ( pNtk->pExdc )
+        fprintf( stdout, "Warning: EXDC is not copied when converting to sequential AIG.\n" );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Seq_NtkRetimeDerive(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop, Vec_Ptr_t * vFanins )
+{
+    Dec_Graph_t * pFForm;
+    Dec_Node_t * pNode;
+    Abc_Obj_t * pResult, * pFanin, * pMirror;
+    int i, nFanins;
+
+    // get the number of node's fanins
+    nFanins = Abc_ObjFaninNum( pRoot );
+    assert( nFanins == Abc_SopGetVarNum(pSop) );
+    if ( nFanins < 2 )
+    {
+        if ( Abc_SopIsConst1(pSop) )
+            pFanin = Abc_AigConst1(pNtkNew);
+        else if ( Abc_SopIsConst0(pSop) )
+            pFanin = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
+        else if ( Abc_SopIsBuf(pSop) )
+            pFanin = Abc_ObjFanin0(pRoot)->pCopy;
+        else if ( Abc_SopIsInv(pSop) )
+            pFanin = Abc_ObjNot( Abc_ObjFanin0(pRoot)->pCopy );
+        else
+            assert( 0 );
+        // create the node with these fanins
+        pMirror = Abc_NtkCreateNode( pNtkNew );
+        Abc_ObjAddFanin( pMirror, pFanin );
+        Abc_ObjAddFanin( pMirror, pFanin );
+        Vec_PtrPush( vFanins, pMirror );
+        return pMirror;
+    }
+
+    // perform factoring
+    pFForm = Dec_Factor( pSop );
+    // collect the fanins
+    Dec_GraphForEachLeaf( pFForm, pNode, i )
+    {
+        pFanin = Abc_ObjFanin(pRoot,i)->pCopy;
+        pMirror = Abc_NtkCreateNode( pNtkNew );
+        Abc_ObjAddFanin( pMirror, pFanin );
+        Abc_ObjAddFanin( pMirror, pFanin );
+        Vec_PtrPush( vFanins, pMirror );
+        pNode->pFunc = pMirror;
+    }
+    // perform strashing
+    pResult = Dec_GraphToNetworkNoStrash( pNtkNew, pFForm );
+    Dec_GraphFree( pFForm );
+    return pResult;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the network after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
+{
+    Abc_Seq_t * p = pNtkSeq->pManFunc;
+    Seq_Lat_t * pRing0, * pRing1;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pFanin, * pFaninNew, * pMirror;
+    Vec_Ptr_t * vMirrors;
+    int i, k;
+
+    assert( !Abc_NtkIsSeq(pNtkOld) );
+    assert( Abc_NtkIsSeq(pNtkSeq) );
+
+    // transfer the pointers pNtkOld->pNtkSeq from pCopy to pNext
+    Abc_NtkForEachObj( pNtkOld, pObj, i )
+        pObj->pNext = pObj->pCopy;
+
+    // start the final network
+    pNtkNew = Abc_NtkStartFrom( pNtkSeq, pNtkOld->ntkType, pNtkOld->ntkFunc );
+
+    // transfer the pointers to the old network
+    if ( Abc_AigConst1(pNtkOld) ) 
+        Abc_AigConst1(pNtkOld)->pCopy = Abc_AigConst1(pNtkNew);
+    Abc_NtkForEachPi( pNtkOld, pObj, i )
+        pObj->pCopy = pObj->pNext->pCopy;
+    Abc_NtkForEachPo( pNtkOld, pObj, i )
+        pObj->pCopy = pObj->pNext->pCopy;
+
+    // copy the internal nodes of the old network into the new network
+    // transfer the pointers pNktOld->pNtkNew to pNtkSeq->pNtkNew
+    Abc_NtkForEachNode( pNtkOld, pObj, i )
+    {
+        if ( i == 0 ) continue;
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+        pObj->pNext->pCopy = pObj->pCopy;
+    }
+    Abc_NtkForEachLatch( pNtkOld, pObj, i )
+        pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
+
+    // share the latches
+    Seq_NtkShareLatches( pNtkNew, pNtkSeq );
+
+    // connect the objects
+//    Abc_NtkForEachNode( pNtkOld, pObj, i )
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+    {
+        // pObj is from pNtkSeq - transform to pNtkOld
+        pObj = pObj->pNext;
+        // iterate through the fanins of this node in the old network
+        vMirrors = Vec_VecEntry( p->vMapFanins, i );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            pMirror = Vec_PtrEntry( vMirrors, k );
+            assert( Seq_ObjFaninL0(pMirror) == Seq_ObjFaninL1(pMirror) );
+            pRing0 = Seq_NodeGetRing( pMirror, 0 );
+            pRing1 = Seq_NodeGetRing( pMirror, 1 );
+            if ( pRing0 == NULL )
+            {
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+                continue;
+            }
+//            assert( pRing0->pLatch == pRing1->pLatch );
+            if ( pRing0->pLatch->pData > pRing1->pLatch->pData )
+                Abc_ObjAddFanin( pObj->pCopy, pRing0->pLatch );
+            else
+                Abc_ObjAddFanin( pObj->pCopy, pRing1->pLatch );
+        }
+    }
+
+    // connect the POs
+    Abc_NtkForEachPo( pNtkOld, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        pRing0 = Seq_NodeGetRing( Abc_NtkPo(pNtkSeq, i), 0 );
+        if ( pRing0 )
+            pFaninNew = pRing0->pLatch;
+        else 
+            pFaninNew = pFanin->pCopy;
+        assert( pFaninNew != NULL );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+
+    // clean the result of latch sharing
+    Seq_NtkShareLatchesClean( pNtkSeq );
+
+    // add the latches and their names
+    Abc_NtkAddDummyBoxNames( pNtkNew );
+    Abc_NtkOrderCisCos( pNtkNew );
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Seq_NtkRetimeReconstruct(): Network check has failed.\n" );
+    return pNtkNew;
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the network after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_EdgeReconstruct_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode )
+{
+    Seq_Lat_t * pRing;
+    Abc_Obj_t * pFanin, * pRes = NULL;
+
+    if ( !Abc_AigNodeIsAnd(pNode) )
+        return NULL;
+
+    // consider the first fanin
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        pRes = Seq_EdgeReconstruct_rec( pGoal, pFanin );
+    else if ( pFanin == pGoal )
+    {
+        if ( pRing = Seq_NodeGetRing( pNode, 0 ) )
+            pRes = pRing->pLatch;
+        else
+            pRes = pFanin->pCopy;
+    }
+    if ( pRes != NULL )
+        return pRes;
+
+    // consider the second fanin
+    pFanin = Abc_ObjFanin1(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        pRes = Seq_EdgeReconstruct_rec( pGoal, pFanin );
+    else if ( pFanin == pGoal )
+    {
+        if ( pRing = Seq_NodeGetRing( pNode, 1 ) )
+            pRes = pRing->pLatch;
+        else
+            pRes = pFanin->pCopy;
+    }
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the network after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_EdgeReconstructPO( Abc_Obj_t * pNode )
+{
+    Seq_Lat_t * pRing;
+    assert( Abc_ObjIsPo(pNode) );
+    if ( pRing = Seq_NodeGetRing( pNode, 0 ) )
+        return pRing->pLatch;
+    else
+        return Abc_ObjFanin0(pNode)->pCopy;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqRetIter.c b/src/base/seq/seqRetIter.c
new file mode 100644
index 00000000..99c50914
--- /dev/null
+++ b/src/base/seq/seqRetIter.c
@@ -0,0 +1,403 @@
+/**CFile****************************************************************
+
+  FileName    [seqRetIter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [Iterative delay computation in FPGA mapping/retiming package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqRetIter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+#include "main.h"
+#include "fpga.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static float Seq_NtkMappingSearch_rec( Abc_Ntk_t * pNtk, float FiMin, float FiMax, float Delta, int fVerbose );
+static int   Seq_NtkMappingForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose );
+static int   Seq_NtkNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vDelays );
+static void  Seq_NodeRetimeSetLag_rec( Abc_Obj_t * pNode, char Lag );
+
+static void  Seq_NodePrintInfo( Abc_Obj_t * pNode );
+static void  Seq_NodePrintInfoPlus( Abc_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the retiming lags for arbitrary network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Obj_t * pNode;
+    float FiMax, Delta;
+    int i, RetValue;
+    char NodeLag;
+
+    assert( Abc_NtkIsSeq( pNtk ) );
+
+    // the root AND gates and node delay should be assigned
+    assert( p->vMapAnds );
+    assert( p->vMapCuts );
+    assert( p->vMapDelays );
+    assert( p->vMapFanins );
+
+    // guess the upper bound on the clock period
+    if ( Abc_NtkHasMapping(pNtkOld) )
+    {
+        // assign the accuracy for min-period computation
+        Delta = Mio_LibraryReadDelayNand2Max(Abc_FrameReadLibGen());
+        if ( Delta == 0.0 )
+        {
+            Delta = Mio_LibraryReadDelayAnd2Max(Abc_FrameReadLibGen());
+            if ( Delta == 0.0 )
+            {
+                printf( "Cannot retime/map if the library does not have NAND2 or AND2.\n" );
+                return 0;
+            }
+        }
+        // get the upper bound on the clock period
+        FiMax = Delta * 2 + Abc_NtkDelayTrace(pNtkOld);
+        Delta /= 2;
+    }
+    else
+    {
+        FiMax = (float)2.0 + Abc_NtkGetLevelNum(pNtkOld);
+        Delta = 1;
+    }
+
+    // make sure this clock period is feasible
+    if ( !Seq_NtkMappingForPeriod( pNtk, FiMax, fVerbose ) )
+    {
+        printf( "Error: The upper bound on the clock period cannot be computed.\n" );
+        printf( "The reason for this error may be the presence in the circuit of logic\n" );
+        printf( "that is not reachable from the PIs. Mapping/retiming is not performed.\n" );
+        return 0;
+    }
+ 
+    // search for the optimal clock period between 0 and nLevelMax
+    p->FiBestFloat = Seq_NtkMappingSearch_rec( pNtk, 0.0, FiMax, Delta, fVerbose );
+
+    // recompute the best l-values
+    RetValue = Seq_NtkMappingForPeriod( pNtk, p->FiBestFloat, fVerbose );
+    assert( RetValue );
+
+    // fix the problem with non-converged delays
+    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+        if ( Seq_NodeGetLValueP(pNode) < -ABC_INFINITY/2 )
+            Seq_NodeSetLValueP( pNode, 0 );
+
+    // experiment by adding an epsilon to all LValues
+//    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+//        Seq_NodeSetLValueP( pNode, Seq_NodeGetLValueP(pNode) - p->fEpsilon );
+
+    // save the retiming lags
+    // mark the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+        pNode->fMarkA = 1;
+    // process the nodes
+    Vec_StrFill( p->vLags,  p->nSize, 0 );
+    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+    {
+        if ( Vec_PtrSize( Vec_VecEntry(p->vMapCuts, i) ) == 0 )
+        {
+            Seq_NodeSetLag( pNode, 0 );
+            continue;
+        }
+        NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueP(pNode), p->FiBestFloat );
+        Seq_NodeRetimeSetLag_rec( pNode, NodeLag );
+    }
+    // unmark the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+        pNode->fMarkA = 0;
+
+    // print the result
+    if ( fVerbose )
+        printf( "The best clock period is %6.2f.\n", p->FiBestFloat );
+/*
+    {
+        FILE * pTable;
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  pNtk->pName );
+        fprintf( pTable, "%.2f ", FiBest );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+    }
+*/
+//    Seq_NodePrintInfo( Abc_NtkObj(pNtk, 847) );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs binary search for the optimal clock period.]
+
+  Description [Assumes that FiMin is infeasible while FiMax is feasible.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Seq_NtkMappingSearch_rec( Abc_Ntk_t * pNtk, float FiMin, float FiMax, float Delta, int fVerbose )
+{
+    float Median;
+    assert( FiMin < FiMax );
+    if ( FiMin + Delta >= FiMax )
+        return FiMax;
+    Median = FiMin + (FiMax - FiMin)/2;
+    if ( Seq_NtkMappingForPeriod( pNtk, Median, fVerbose ) )
+        return Seq_NtkMappingSearch_rec( pNtk, FiMin, Median, Delta, fVerbose ); // Median is feasible
+    else 
+        return Seq_NtkMappingSearch_rec( pNtk, Median, FiMax, Delta, fVerbose ); // Median is infeasible
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if retiming with this clock period is feasible.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkMappingForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Vec_Ptr_t * vLeaves, * vDelays;
+    Abc_Obj_t * pObj;
+    int i, c, RetValue, fChange, Counter;
+    char * pReason = "";
+
+    // set l-values of all nodes to be minus infinity
+    Vec_IntFill( p->vLValues,  p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
+
+    // set l-values of constants and PIs
+    pObj = Abc_NtkObj( pNtk, 0 );
+    Seq_NodeSetLValueP( pObj, 0.0 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Seq_NodeSetLValueP( pObj, 0.0 );
+
+    // update all values iteratively
+    Counter = 0;
+    for ( c = 0; c < p->nMaxIters; c++ )
+    {
+        fChange = 0;
+        Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+        {
+            Counter++;
+            vLeaves = Vec_VecEntry( p->vMapCuts, i );
+            vDelays = Vec_VecEntry( p->vMapDelays, i );
+            if ( Vec_PtrSize(vLeaves) == 0 )
+            {
+                Seq_NodeSetLValueP( pObj, 0.0 );
+                continue;
+            }
+            RetValue = Seq_NtkNodeUpdateLValue( pObj, Fi, vLeaves, vDelays );
+            if ( RetValue == SEQ_UPDATE_YES ) 
+                fChange = 1;
+        }
+        Abc_NtkForEachPo( pNtk, pObj, i )
+        {
+            RetValue = Seq_NtkNodeUpdateLValue( pObj, Fi, NULL, NULL );
+            if ( RetValue == SEQ_UPDATE_FAIL )
+                break;
+        }
+        if ( RetValue == SEQ_UPDATE_FAIL )
+            break;
+        if ( fChange == 0 )
+            break;
+    }
+    if ( c == p->nMaxIters )
+    {
+        RetValue = SEQ_UPDATE_FAIL;
+        pReason = "(timeout)";
+    }
+    else
+        c++;
+
+    // report the results
+    if ( fVerbose )
+    {
+        if ( RetValue == SEQ_UPDATE_FAIL )
+            printf( "Period = %6.2f.  Iterations = %3d.  Updates = %10d.    Infeasible %s\n", Fi, c, Counter, pReason );
+        else
+            printf( "Period = %6.2f.  Iterations = %3d.  Updates = %10d.      Feasible\n",    Fi, c, Counter );
+    }
+    return RetValue != SEQ_UPDATE_FAIL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the node.]
+
+  Description [The node can be internal or a PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vDelays )
+{
+    Abc_Seq_t * p = pObj->pNtk->pManFunc;
+    float lValueOld, lValueNew, lValueCur, lValuePin;
+    unsigned SeqEdge;
+    Abc_Obj_t * pLeaf;
+    int i;
+
+    assert( !Abc_ObjIsPi(pObj) );
+    assert( Abc_ObjFaninNum(pObj) > 0 );
+    // consider the case of the PO
+    if ( Abc_ObjIsPo(pObj) )
+    {
+        lValueCur = Seq_NodeGetLValueP(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj);
+        return (lValueCur > Fi + p->fEpsilon)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO;
+    }
+    // get the new arrival time of the cut output
+    lValueNew = -ABC_INFINITY;
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        SeqEdge   = (unsigned)pLeaf;
+        pLeaf     = Abc_NtkObj( pObj->pNtk, SeqEdge >> 8 );
+        lValueCur = Seq_NodeGetLValueP(pLeaf) - Fi * (SeqEdge & 255);
+        lValuePin = Abc_Int2Float( (int)Vec_PtrEntry(vDelays, i) );
+        if ( lValueNew < lValuePin + lValueCur )
+            lValueNew = lValuePin + lValueCur;
+    }
+    // compare 
+    lValueOld = Seq_NodeGetLValueP( pObj );
+    if ( lValueNew <= lValueOld + p->fEpsilon )
+        return SEQ_UPDATE_NO;
+    // update the values
+    if ( lValueNew > lValueOld + p->fEpsilon )
+        Seq_NodeSetLValueP( pObj, lValueNew );
+    return SEQ_UPDATE_YES;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Add sequential edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodeRetimeSetLag_rec( Abc_Obj_t * pNode, char Lag )
+{
+    Abc_Obj_t * pFanin;
+    if ( !Abc_AigNodeIsAnd(pNode) )
+        return;
+    Seq_NodeSetLag( pNode, Lag );
+    // consider the first fanin
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( pFanin->fMarkA == 0 ) // internal node
+        Seq_NodeRetimeSetLag_rec( pFanin, Lag );
+    // consider the second fanin
+    pFanin = Abc_ObjFanin1(pNode);
+    if ( pFanin->fMarkA == 0 ) // internal node
+        Seq_NodeRetimeSetLag_rec( pFanin, Lag );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Add sequential edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodePrintInfo( Abc_Obj_t * pNode )
+{
+    Abc_Seq_t * p = pNode->pNtk->pManFunc;
+    Abc_Obj_t * pFanin, * pObj, * pLeaf;
+    Vec_Ptr_t * vLeaves;
+    unsigned SeqEdge;
+    int i, Number;
+
+    // print the node
+    printf( "    Node      = %6d.  LValue = %7.2f.  Lag = %2d.\n", 
+        pNode->Id, Seq_NodeGetLValueP(pNode), Seq_NodeGetLag(pNode) );
+
+    // find the number
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, Number )
+        if ( pObj == pNode )
+            break;
+
+    // get the leaves
+    vLeaves = Vec_VecEntry( p->vMapCuts, Number );
+
+    // print the leaves
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        SeqEdge   = (unsigned)pLeaf;
+        pFanin    = Abc_NtkObj( pNode->pNtk, SeqEdge >> 8 );
+        // print the leaf
+        printf( "    Fanin%d(%d) = %6d.  LValue = %7.2f.  Lag = %2d.\n", i, SeqEdge & 255,
+            pFanin->Id, Seq_NodeGetLValueP(pFanin), Seq_NodeGetLag(pFanin) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add sequential edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodePrintInfoPlus( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    printf( "CENTRAL NODE:\n" );
+    Seq_NodePrintInfo( pNode );
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+    {
+        printf( "FANOUT%d:\n", i );
+        Seq_NodePrintInfo( pFanout );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqShare.c b/src/base/seq/seqShare.c
new file mode 100644
index 00000000..742de46b
--- /dev/null
+++ b/src/base/seq/seqShare.c
@@ -0,0 +1,388 @@
+/**CFile****************************************************************
+
+  FileName    [seqShare.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [Latch sharing at the fanout stems.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqShare.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Seq_NodeShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
+static void Seq_NodeShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNodes );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the sequential AIG to take fanout sharing into account.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkShareFanouts( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    int i;
+    vNodes = Vec_PtrAlloc( 10 );
+    // share the PI latches
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Seq_NodeShareFanouts( pObj, vNodes );
+    // share the node latches
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Seq_NodeShareFanouts( pObj, vNodes );
+    Vec_PtrFree( vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the node to take fanout sharing into account.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodeShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pFanout;
+    Abc_InitType_t Type;
+    int nLatches[4], i;
+    // skip the node with only one fanout
+    if ( Abc_ObjFanoutNum(pNode) < 2 )
+        return;
+    // clean the the fanout counters
+    for ( i = 0; i < 4; i++ )
+        nLatches[i] = 0;
+    // find the number of fanouts having latches of each type
+    Abc_ObjForEachFanout( pNode, pFanout, i )  
+    {
+        if ( Seq_ObjFanoutL(pNode, pFanout) == 0 )
+            continue;
+        Type = Seq_NodeGetInitLast( pFanout, Abc_ObjFanoutEdgeNum(pNode, pFanout) );
+        nLatches[Type]++;
+    }
+    // decide what to do
+    if ( nLatches[ABC_INIT_ZERO] > 1 && nLatches[ABC_INIT_ONE] > 1 ) // 0-group and 1-group
+    {
+        Seq_NodeShareOne( pNode, ABC_INIT_ZERO, vNodes );     // shares 0 and DC
+        Seq_NodeShareOne( pNode, ABC_INIT_ONE,  vNodes );     // shares 1 and DC
+    }
+    else if ( nLatches[ABC_INIT_ZERO] > 1 ) // 0-group
+        Seq_NodeShareOne( pNode, ABC_INIT_ZERO, vNodes );     // shares 0 and DC
+    else if ( nLatches[ABC_INIT_ONE] > 1 ) // 1-group
+        Seq_NodeShareOne( pNode, ABC_INIT_ONE,  vNodes );     // shares 1 and DC
+    else if ( nLatches[ABC_INIT_DC] > 1 ) // DC-group
+    {
+        if ( nLatches[ABC_INIT_ZERO] > 0 )
+            Seq_NodeShareOne( pNode, ABC_INIT_ZERO, vNodes ); // shares 0 and DC
+        else 
+            Seq_NodeShareOne( pNode, ABC_INIT_ONE,  vNodes ); // shares 1 and DC
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the node to take fanout sharing into account.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodeShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNodes )
+{
+    Vec_Int_t * vNums  = Seq_ObjLNums( pNode );
+    Vec_Ptr_t * vInits = Seq_NodeLats( pNode );
+    Abc_Obj_t * pFanout, * pBuffer;
+    Abc_InitType_t Type, InitNew;
+    int i;
+    // collect the fanouts that satisfy the property (have initial value Init or DC)
+    InitNew = ABC_INIT_DC;
+    Vec_PtrClear( vNodes );
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+    {
+        if ( Seq_ObjFanoutL(pNode, pFanout) == 0 )
+            continue;
+        Type = Seq_NodeGetInitLast( pFanout, Abc_ObjFanoutEdgeNum(pNode, pFanout) );
+        if ( Type == Init )
+            InitNew = Init;
+        if ( Type == Init || Type == ABC_INIT_DC )
+        {
+            Vec_PtrPush( vNodes, pFanout );
+            Seq_NodeDeleteLast( pFanout, Abc_ObjFanoutEdgeNum(pNode, pFanout) );
+        }
+    }
+    // create the new buffer
+    pBuffer = Abc_NtkCreateNode( pNode->pNtk );
+    Abc_ObjAddFanin( pBuffer, pNode );
+
+    // grow storage for initial states
+    Vec_PtrGrow( vInits, 2 * pBuffer->Id + 2 );
+    for ( i = Vec_PtrSize(vInits); i < 2 * (int)pBuffer->Id + 2; i++ )
+        Vec_PtrPush( vInits, NULL );
+    // grow storage for numbers of latches
+    Vec_IntGrow( vNums, 2 * pBuffer->Id + 2 );
+    for ( i = Vec_IntSize(vNums); i < 2 * (int)pBuffer->Id + 2; i++ )
+        Vec_IntPush( vNums, 0 );
+    // insert the new latch
+    Seq_NodeInsertFirst( pBuffer, 0, InitNew );
+
+    // redirect the fanouts
+    Vec_PtrForEachEntry( vNodes, pFanout, i )
+        Abc_ObjPatchFanin( pFanout, pNode, pBuffer );
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Maps virtual latches into real latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Seq_NtkShareLatchesKey( Abc_Obj_t * pObj, Abc_InitType_t Init )
+{
+    return (pObj->Id << 2) | Init;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Maps virtual latches into real latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_NtkShareLatches_rec( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj, Seq_Lat_t * pRing, int nLatch, stmm_table * tLatchMap )
+{
+    Abc_Obj_t * pLatch, * pFanin;
+    Abc_InitType_t Init;
+    unsigned Key;
+    if ( nLatch == 0 )
+        return pObj;
+    assert( pRing->pLatch == NULL );
+    // get the latch on the previous level
+    pFanin = Seq_NtkShareLatches_rec( pNtk, pObj, Seq_LatNext(pRing), nLatch - 1, tLatchMap );
+
+    // get the initial state
+    Init = Seq_LatInit( pRing );
+    // check if the latch with this initial state exists
+    Key = Seq_NtkShareLatchesKey( pFanin, Init );
+    if ( stmm_lookup( tLatchMap, (char *)Key, (char **)&pLatch ) )
+        return pRing->pLatch = pLatch;
+
+    // does not exist
+    if ( Init != ABC_INIT_DC )
+    {
+        // check if the don't-care exists
+        Key = Seq_NtkShareLatchesKey( pFanin, ABC_INIT_DC );
+        if ( stmm_lookup( tLatchMap, (char *)Key, (char **)&pLatch ) ) // yes
+        {
+            // update the table
+            stmm_delete( tLatchMap, (char **)&Key, (char **)&pLatch );
+            Key = Seq_NtkShareLatchesKey( pFanin, Init );
+            stmm_insert( tLatchMap, (char *)Key, (char *)pLatch );
+            // change don't-care to the given value
+            pLatch->pData = (void *)Init;
+            return pRing->pLatch = pLatch;
+        }
+
+        // add the latch with this value
+        pLatch = Abc_NtkCreateLatch( pNtk );
+        pLatch->pData = (void *)Init;
+        Abc_ObjAddFanin( pLatch, pFanin );
+        // add it to the table
+        Key = Seq_NtkShareLatchesKey( pFanin, Init );
+        stmm_insert( tLatchMap, (char *)Key, (char *)pLatch );
+        return pRing->pLatch = pLatch;
+    }
+    // the init value is the don't-care
+
+    // check if care values exist
+    Key = Seq_NtkShareLatchesKey( pFanin, ABC_INIT_ZERO );
+    if ( stmm_lookup( tLatchMap, (char *)Key, (char **)&pLatch ) )
+    {
+        Seq_LatSetInit( pRing, ABC_INIT_ZERO );
+        return pRing->pLatch = pLatch;
+    }
+    Key = Seq_NtkShareLatchesKey( pFanin, ABC_INIT_ONE );
+    if ( stmm_lookup( tLatchMap, (char *)Key, (char **)&pLatch ) )
+    {
+        Seq_LatSetInit( pRing, ABC_INIT_ONE );
+        return pRing->pLatch = pLatch;
+    }
+
+    // create the don't-care latch
+    pLatch = Abc_NtkCreateLatch( pNtk );
+    pLatch->pData = (void *)ABC_INIT_DC;
+    Abc_ObjAddFanin( pLatch, pFanin );
+    // add it to the table
+    Key = Seq_NtkShareLatchesKey( pFanin, ABC_INIT_DC );
+    stmm_insert( tLatchMap, (char *)Key, (char *)pLatch );
+    return pRing->pLatch = pLatch;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Maps virtual latches into real latches.]
+
+  Description [Creates new latches and assigns them to virtual latches
+  on the edges of a sequential AIG. The nodes of the new network should
+  be created before this procedure is called.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk )
+{ 
+    Abc_Obj_t * pObj, * pFanin;
+    stmm_table * tLatchMap;
+    int i;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    tLatchMap = stmm_init_table( stmm_ptrcmp, stmm_ptrhash );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        Seq_NtkShareLatches_rec( pNtkNew, pFanin->pCopy, Seq_NodeGetRing(pObj,0), Seq_NodeCountLats(pObj,0), tLatchMap );
+        pFanin = Abc_ObjFanin1(pObj);
+        Seq_NtkShareLatches_rec( pNtkNew, pFanin->pCopy, Seq_NodeGetRing(pObj,1), Seq_NodeCountLats(pObj,1), tLatchMap );
+    }
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_NtkShareLatches_rec( pNtkNew, Abc_ObjFanin0(pObj)->pCopy, Seq_NodeGetRing(pObj,0), Seq_NodeCountLats(pObj,0), tLatchMap );
+    stmm_free_table( tLatchMap );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Maps virtual latches into real latches.]
+
+  Description [Creates new latches and assigns them to virtual latches
+  on the edges of a sequential AIG. The nodes of the new network should
+  be created before this procedure is called.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkShareLatchesMapping( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds, int fFpga )
+{ 
+    Seq_Match_t * pMatch;
+    Abc_Obj_t * pObj, * pFanout;
+    stmm_table * tLatchMap;
+    Vec_Ptr_t * vNodes;
+    int i, k;
+    assert( Abc_NtkIsSeq( pNtk ) );
+
+    // start the table
+    tLatchMap = stmm_init_table( stmm_ptrcmp, stmm_ptrhash );
+
+    // create the array of all nodes with sharable fanouts
+    vNodes = Vec_PtrAlloc( 100 );
+    Vec_PtrPush( vNodes, Abc_AigConst1(pNtk) );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Vec_PtrPush( vNodes, pObj );
+    if ( fFpga )
+    {
+        Vec_PtrForEachEntry( vMapAnds, pObj, i )
+            Vec_PtrPush( vNodes, pObj );
+    }
+    else 
+    {
+        Vec_PtrForEachEntry( vMapAnds, pMatch, i )
+            Vec_PtrPush( vNodes, pMatch->pAnd );
+    }
+
+    // process nodes used in the mapping
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // make sure the label is clean
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            assert( pFanout->fMarkC == 0 );
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+        {
+            if ( pFanout->fMarkC )
+                continue;
+            pFanout->fMarkC = 1;
+            if ( Abc_ObjFaninId0(pFanout) == pObj->Id )
+                Seq_NtkShareLatches_rec( pNtkNew, pObj->pCopy, Seq_NodeGetRing(pFanout,0), Seq_NodeCountLats(pFanout,0), tLatchMap );
+            if ( Abc_ObjFaninId1(pFanout) == pObj->Id )
+                Seq_NtkShareLatches_rec( pNtkNew, pObj->pCopy, Seq_NodeGetRing(pFanout,1), Seq_NodeCountLats(pFanout,1), tLatchMap );
+        }
+        // clean the label
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            pFanout->fMarkC = 0;
+    }
+    stmm_free_table( tLatchMap );
+    // return to the old array
+    Vec_PtrFree( vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Clean the latches after sharing them.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkShareLatchesClean( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        Seq_NodeCleanLats( pObj, 0 );
+        Seq_NodeCleanLats( pObj, 1 );
+    }
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_NodeCleanLats( pObj, 0 );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqUtil.c b/src/base/seq/seqUtil.c
new file mode 100644
index 00000000..55b9df8e
--- /dev/null
+++ b/src/base/seq/seqUtil.c
@@ -0,0 +1,597 @@
+/**CFile****************************************************************
+
+  FileName    [seqUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [Various utilities working with sequential AIGs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the maximum latch number on any of the fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkLevelMax( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, Result;
+    assert( Abc_NtkIsSeq(pNtk) );
+    Result = 0;
+    Abc_NtkForEachPo( pNtk, pNode, i )
+    {
+        pNode = Abc_ObjFanin0(pNode);
+        if ( Result < (int)pNode->Level )
+            Result = pNode->Level;
+    }
+    Abc_SeqForEachCutsetNode( pNtk, pNode, i )
+    {
+        if ( Result < (int)pNode->Level )
+            Result = pNode->Level;
+    }
+    return Result;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the maximum latch number on any of the fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_ObjFanoutLMax( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanout;
+    int i, nLatchCur, nLatchRes;
+    if ( Abc_ObjFanoutNum(pObj) == 0 )
+        return 0;
+    nLatchRes = 0;
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        nLatchCur = Seq_ObjFanoutL(pObj, pFanout);
+        if ( nLatchRes < nLatchCur )
+            nLatchRes = nLatchCur;
+    }
+    assert( nLatchRes >= 0 );
+    return nLatchRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the minimum latch number on any of the fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_ObjFanoutLMin( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanout;
+    int i, nLatchCur, nLatchRes;
+    if ( Abc_ObjFanoutNum(pObj) == 0 )
+        return 0;
+    nLatchRes = ABC_INFINITY;
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        nLatchCur = Seq_ObjFanoutL(pObj, pFanout);
+        if ( nLatchRes > nLatchCur )
+            nLatchRes = nLatchCur;
+    }
+    assert( nLatchRes < ABC_INFINITY );
+    return nLatchRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the sum of latches on the fanout edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_ObjFanoutLSum( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanout;
+    int i, nSum = 0;
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        nSum += Seq_ObjFanoutL(pObj, pFanout);
+    return nSum;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the sum of latches on the fanin edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_ObjFaninLSum( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i, nSum = 0;
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        nSum += Seq_ObjFaninL(pObj, i);
+    return nSum;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generates the printable edge label with the initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Seq_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge )
+{
+    static char Buffer[1000];
+    Abc_InitType_t Init;
+    int nLatches, i;
+    nLatches = Seq_ObjFaninL( pObj, Edge );
+    for ( i = 0; i < nLatches; i++ )
+    {
+        Init = Seq_LatInit( Seq_NodeGetLat(pObj, Edge, i) );
+        if ( Init == ABC_INIT_NONE )
+            Buffer[i] = '_';
+        else if ( Init == ABC_INIT_ZERO )
+            Buffer[i] = '0';
+        else if ( Init == ABC_INIT_ONE )
+            Buffer[i] = '1';
+        else if ( Init == ABC_INIT_DC )
+            Buffer[i] = 'x';
+        else assert( 0 );
+    }
+    Buffer[nLatches] = 0;
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the given value to all the latches of the edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodeLatchSetValues( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )
+{ 
+    Seq_Lat_t * pLat, * pRing;
+    int c; 
+    pRing = Seq_NodeGetRing(pObj, Edge);
+    if ( pRing == NULL ) 
+        return; 
+    for ( c = 0, pLat = pRing; !c || pLat != pRing; c++, pLat = pLat->pNext )
+        Seq_LatSetInit( pLat, Init );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the given value to all the latches of the edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkLatchSetValues( Abc_Ntk_t * pNtk, Abc_InitType_t Init )
+{ 
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_NodeLatchSetValues( pObj, 0, Init );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        Seq_NodeLatchSetValues( pObj, 0, Init );
+        Seq_NodeLatchSetValues( pObj, 1, Init );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of latches in the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkLatchNum( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, Counter;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    Counter = 0;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Counter += Seq_ObjFaninLSum( pObj );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Counter += Seq_ObjFaninLSum( pObj );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of latches in the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkLatchNumMax( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, Max, Cur;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    Max = 0;
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        Cur = Seq_ObjFaninLMax( pObj );
+        if ( Max < Cur )
+            Max = Cur;
+    }
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        Cur = Seq_ObjFaninL0( pObj );
+        if ( Max < Cur )
+            Max = Cur;
+    }
+    return Max;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of latches in the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkLatchNumShared( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, Counter;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    Counter = 0;
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Counter += Seq_ObjFanoutLMax( pObj );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Counter += Seq_ObjFanoutLMax( pObj );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of latches in the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_ObjLatchGetInitNums( Abc_Obj_t * pObj, int Edge, int * pInits )
+{
+    Abc_InitType_t Init;
+    int nLatches, i;
+    nLatches = Seq_ObjFaninL( pObj, Edge );
+    for ( i = 0; i < nLatches; i++ )
+    {
+        Init = Seq_NodeGetInitOne( pObj, Edge, i );
+        pInits[Init]++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of latches in the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkLatchGetInitNums( Abc_Ntk_t * pNtk, int * pInits )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    for ( i = 0; i < 4; i++ )    
+        pInits[i] = 0;
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_ObjLatchGetInitNums( pObj, 0, pInits );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) > 0 )
+            Seq_ObjLatchGetInitNums( pObj, 0, pInits );
+        if ( Abc_ObjFaninNum(pObj) > 1 )
+            Seq_ObjLatchGetInitNums( pObj, 1, pInits );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Report nodes with equal fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkLatchGetEqualFaninNum( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, Counter;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    Counter = 0;
+    Abc_AigForEachAnd( pNtk, pObj, i )
+        if ( Abc_ObjFaninId0(pObj) == Abc_ObjFaninId1(pObj) )
+            Counter++;
+    if ( Counter )
+        printf( "The number of nodes with equal fanins = %d.\n", Counter );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the maximum latch number on any of the fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkCountNodesAboveLimit( Abc_Ntk_t * pNtk, int Limit )
+{
+    Abc_Obj_t * pNode;
+    int i, Counter;
+    assert( !Abc_NtkIsSeq(pNtk) );
+    Counter = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( Abc_ObjFaninNum(pNode) > Limit )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area flows.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapComputeAreaFlows( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Obj_t * pObj;
+    float AFlow;
+    int i, c;
+
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    Vec_IntFill( p->vAFlows, p->nSize, Abc_Float2Int( (float)0.0 ) );
+
+    // update all values iteratively
+    for ( c = 0; c < 7; c++ )
+    {
+        Abc_AigForEachAnd( pNtk, pObj, i )
+        {
+            AFlow = (float)1.0 + Seq_NodeGetFlow( Abc_ObjFanin0(pObj) ) + Seq_NodeGetFlow( Abc_ObjFanin1(pObj) );
+            AFlow /= Abc_ObjFanoutNum(pObj);
+            pObj->pNext = (void *)Abc_Float2Int( AFlow );
+        }
+        Abc_AigForEachAnd( pNtk, pObj, i )
+        {
+            AFlow = Abc_Int2Float( (int)pObj->pNext );
+            pObj->pNext = NULL;
+            Seq_NodeSetFlow( pObj, AFlow );
+
+//            printf( "%5d : %6.1f\n", pObj->Id, Seq_NodeGetFlow(pObj) );
+        }
+//        printf( "\n" );
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects all the internal nodes reachable from POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkReachNodesFromPos_rec( Abc_Obj_t * pAnd, Vec_Ptr_t * vNodes )
+{
+    // skip if this is a non-PI node
+    if ( !Abc_AigNodeIsAnd(pAnd) )
+        return;
+    // skip a visited node
+    if ( Abc_NodeIsTravIdCurrent(pAnd) )
+        return;
+    Abc_NodeSetTravIdCurrent(pAnd);
+    // visit the fanin nodes
+    Seq_NtkReachNodesFromPos_rec( Abc_ObjFanin0(pAnd), vNodes );
+    Seq_NtkReachNodesFromPos_rec( Abc_ObjFanin1(pAnd), vNodes );
+    // add this node
+    Vec_PtrPush( vNodes, pAnd );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects all the internal nodes reachable from POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkReachNodesFromPis_rec( Abc_Obj_t * pAnd, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pFanout;
+    int k;
+    // skip if this is a non-PI node
+    if ( !Abc_AigNodeIsAnd(pAnd) )
+        return;
+    // skip a visited node
+    if ( Abc_NodeIsTravIdCurrent(pAnd) )
+        return;
+    Abc_NodeSetTravIdCurrent(pAnd);
+    // visit the fanin nodes
+    Abc_ObjForEachFanout( pAnd, pFanout, k )
+        Seq_NtkReachNodesFromPis_rec( pFanout, vNodes );
+    // add this node
+    Vec_PtrPush( vNodes, pAnd );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects all the internal nodes reachable from POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Seq_NtkReachNodes( Abc_Ntk_t * pNtk, int fFromPos )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pFanout;
+    int i, k;
+    assert( Abc_NtkIsSeq(pNtk) );
+    vNodes = Vec_PtrAlloc( 1000 );
+    Abc_NtkIncrementTravId( pNtk );
+    if ( fFromPos )
+    {
+        // traverse the cone of each PO
+        Abc_NtkForEachPo( pNtk, pObj, i )
+            Seq_NtkReachNodesFromPos_rec( Abc_ObjFanin0(pObj), vNodes );
+    }
+    else
+    {
+        // tranvers the reverse cone of the constant node
+        pObj = Abc_AigConst1( pNtk );
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            Seq_NtkReachNodesFromPis_rec( pFanout, vNodes );
+        // tranvers the reverse cone of the PIs
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            Abc_ObjForEachFanout( pObj, pFanout, k )
+                Seq_NtkReachNodesFromPis_rec( pFanout, vNodes );
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform sequential cleanup.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Vec_Ptr_t * vNodesPo, * vNodesPi;
+    int Counter = 0;
+    assert( Abc_NtkIsSeq(pNtk) );
+    // collect the nodes reachable from POs and PIs
+    vNodesPo = Seq_NtkReachNodes( pNtk, 1 );
+    vNodesPi = Seq_NtkReachNodes( pNtk, 0 );
+    printf( "Total nodes = %6d. Reachable from POs = %6d. Reachable from PIs = %6d.\n", 
+        Abc_NtkNodeNum(pNtk), Vec_PtrSize(vNodesPo), Vec_PtrSize(vNodesPi) );
+    if ( Abc_NtkNodeNum(pNtk) > Vec_PtrSize(vNodesPo) )
+    {
+//        Counter = Abc_NtkReduceNodes( pNtk, vNodesPo );
+        Counter = 0;
+        if ( fVerbose )
+            printf( "Cleanup removed %d nodes that are not reachable from the POs.\n", Counter );
+    }
+    Vec_PtrFree( vNodesPo );
+    Vec_PtrFree( vNodesPi );
+    return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+