Version abc51114

14 files changed, 2764 insertions, 0 deletions

diff --git a/src/base/seq/module.make b/src/base/seq/module.make
new file mode 100644
index 00000000..2bb176dc
--- /dev/null
+++ b/src/base/seq/module.make
@@ -0,0 +1,11 @@
+SRC +=  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/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..8e0d9c09
--- /dev/null
+++ b/src/base/seq/seq.h
@@ -0,0 +1,74 @@
+/**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__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Abc_Seq_t_  Abc_Seq_t;
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== seqLatch.c ===============================================================*/
+extern void            Seq_NodeDupLats( Abc_Obj_t * pObjNew, Abc_Obj_t * pObj, int Edge );
+/*=== 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 );
+/*=== abcSeq.c ===============================================================*/
+extern Abc_Ntk_t *     Abc_NtkAigToSeq( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *     Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk );
+/*=== seqShare.c =============================================================*/
+extern void                  Seq_NtkSeqShareFanouts( Abc_Ntk_t * pNtk );
+/*=== seqRetCore.c ===========================================================*/
+extern void            Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, 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 );
+/*=== 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 );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c
new file mode 100644
index 00000000..4c66576b
--- /dev/null
+++ b/src/base/seq/seqCreate.c
@@ -0,0 +1,342 @@
+/**CFile****************************************************************
+
+  FileName    [seqCreate.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    []
+
+  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;
+
+    // make sure it is an AIG without self-feeding latches
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
+    assert( Abc_NtkIsDfsOrdered(pNtk) );
+
+    // start the network
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );
+    // duplicate the name and the spec
+    pNtkNew->pName = util_strsav(pNtk->pName);
+    pNtkNew->pSpec = util_strsav(pNtk->pSpec);
+
+    // map the constant nodes
+    Abc_NtkCleanCopy( pNtk );
+    Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew);
+
+    // copy all objects, except the latches and constant
+    Vec_PtrFill( pNtkNew->vObjs, Abc_NtkObjNumMax(pNtk), NULL );
+    Vec_PtrWriteEntry( pNtkNew->vObjs, 0, Abc_NtkConst1(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;
+        pObj->pCopy->fPhase = pObj->fPhase; 
+        pObj->pCopy->Level  = pObj->Level; 
+        Vec_PtrWriteEntry( pNtkNew->vObjs, pObj->pCopy->Id, pObj->pCopy );
+        pNtkNew->nObjs++;
+    }
+    pNtkNew->nNodes = pNtk->nNodes;
+    pNtkNew->nPis   = pNtk->nPis;
+    pNtkNew->nPos   = pNtk->nPos;
+
+    // create PI/PO and their names
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        Vec_PtrPush( pNtkNew->vCis, pObj->pCopy );
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+    }
+    Abc_NtkForEachPo( pNtk, pObj, i ) 
+    {
+        Vec_PtrPush( pNtkNew->vCos, pObj->pCopy );
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+    }
+
+    // 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 );
+
+    // copy EXDC and check correctness
+    if ( pNtkNew->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_NodeIsAigAnd(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, * pObjNew, * 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);
+        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), Abc_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), Abc_ObjFaninL1(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        // the complemented edges are subsumed by the node function
+    }
+    // add the latches and their names
+    Abc_NtkAddDummyLatchNames( pNtkNew );
+    Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
+    {
+        Vec_PtrPush( pNtkNew->vCis, pObjNew );
+        Vec_PtrPush( pNtkNew->vCos, pObjNew );
+    }
+    // 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;    
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqFpgaCore.c b/src/base/seq/seqFpgaCore.c
new file mode 100644
index 00000000..37ef6cb7
--- /dev/null
+++ b/src/base/seq/seqFpgaCore.c
@@ -0,0 +1,170 @@
+/**CFile****************************************************************
+
+  FileName    [seqFpgaCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    []
+
+  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_NtkSeqFpgaDup( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs FPGA mapping and retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkSeqFpgaRetime( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Ntk_t * pNtkMap;
+    int RetValue;
+    // find the best mapping and retiming (p->vMapping, p->vLags)
+    Seq_NtkSeqFpgaMapping( pNtk, fVerbose );
+    // duplicate the nodes contained in multiple cuts
+    pNtkNew = Seq_NtkSeqFpgaDup( pNtk );
+    // implement this retiming
+    p = pNtkNew->pManFunc;
+    RetValue = Seq_NtkImplementRetiming( pNtkNew, p->vLags, fVerbose );
+    if ( RetValue == 0 )
+        printf( "Retiming completed but initial state computation has failed.\n" );
+    // create the final mapped network
+    pNtkMap = Seq_NtkSeqFpgaMapped( pNtkNew, pNtk );
+    Abc_NtkDelete( pNtkNew );
+    return pNtkMap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the network by duplicating some of the nodes.]
+
+  Description [Information about mapping is given as 
+  (1) array of mapping nodes (p->vMapAnds), 
+  (2) array of best cuts for each node (p->vMapCuts), 
+  (3) array of nodes subsumed by each cut (p->vMapBags),
+  (4) array of lags of each node in the cut (p->vMapLags).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkSeqFpgaDup( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pLeaf, * pNode, * pDriver, * pDriverNew;
+    Vec_Ptr_t * vLeaves, * vInside, * vLags;
+    int i, k, TotalLag;
+    
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    // start the network
+    pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
+
+    // set the next pointers
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pObj->pNext = pObj->pCopy;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pNext = NULL;
+
+    // start the new sequential AIG manager
+    Seq_Resize( pNtkNew->pManFunc, 10 + Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk) + Vec_VecSizeSize(p->vMapBags) );
+
+    // create the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+    {
+        // make sure the leaves are assigned
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            assert( pLeaf->pNext );
+            pLeaf->pCopy = pLeaf->pNext;
+        }
+        // recursively construct the internals
+        vInside = Vec_VecEntry( p->vMapBags, i );
+        vLags   = Vec_VecEntry( p->vMapLags, i );
+        Vec_PtrForEachEntry( vInside, pNode, k )
+        {
+            Abc_NtkDupObj( pNtkNew, pNode );
+            Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) );
+            Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild1Copy(pNode) );
+            Abc_ObjSetFaninL( pNode->pCopy, 0, Abc_ObjFaninL(pNode, 0) );
+            Abc_ObjSetFaninL( pNode->pCopy, 1, Abc_ObjFaninL(pNode, 1) );
+            Seq_NodeDupLats( pNode->pCopy, pNode, 0 );
+            Seq_NodeDupLats( pNode->pCopy, pNode, 1 );
+            // set the lag of the new node
+            TotalLag = Seq_NodeGetLag(pObj) + (char)Vec_PtrEntry(vLags, k);
+            Seq_NodeSetLag( pNode->pCopy, (char)TotalLag );
+        }
+        // set the copy of the last node
+        pObj->pNext = pObj->pCopy;
+    }
+
+    // set the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        pDriver    = Abc_ObjFanin0(pObj);
+        pDriverNew = Abc_ObjNotCond(pDriver->pNext, Abc_ObjFaninC0(pObj));
+        Abc_ObjAddFanin( pObj->pCopy, pDriverNew );
+    }
+
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Seq_NtkSeqFpgaDup(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the final mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkMap; 
+    pNtkMap = NULL;
+    if ( !Abc_NtkCheck( pNtkMap ) )
+        fprintf( stdout, "Seq_NtkSeqFpgaMapped(): Network check has failed.\n" );
+    return pNtkMap;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqFpgaIter.c b/src/base/seq/seqFpgaIter.c
new file mode 100644
index 00000000..cb0c739b
--- /dev/null
+++ b/src/base/seq/seqFpgaIter.c
@@ -0,0 +1,50 @@
+/**CFile****************************************************************
+
+  FileName    [seqFpgaIter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    []
+
+  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"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkSeqFpgaMapping( Abc_Ntk_t * pNtk, int fVerbose )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqInt.h b/src/base/seq/seqInt.h
new file mode 100644
index 00000000..2159480a
--- /dev/null
+++ b/src/base/seq/seqInt.h
@@ -0,0 +1,167 @@
+/**CFile****************************************************************
+
+  FileName    [seqInt.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: seqInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __SEQ_INT_H__
+#define __SEQ_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "abc.h"
+#include "seq.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+#define SEQ_FULL_MASK        0xFFFFFFFF   
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// manager of sequential AIG
+struct Abc_Seq_t_
+{
+    Abc_Ntk_t *         pNtk;           // the network
+    int                 nSize;          // the number of entries in all internal arrays
+    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
+    // the arrival times
+    Vec_Int_t *         vLValues;       // the arrival times (L-Values of nodes)
+    Vec_Ptr_t *         vBestCuts;      // the best cuts for nodes
+    Vec_Str_t *         vLags;          // the lags of the mapped nodes
+    // 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 *         vMapBags;       // nodes subsumed by each cut
+    Vec_Vec_t *         vMapLags;       // the internal lags of each node in the bag
+    // 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 
+};
+
+// 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
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      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); }
+
+// storing arrival times in the nodes
+static inline Vec_Int_t *    Seq_NodeLValues( Abc_Obj_t * pNode )               { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLValues;            }
+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 int            Seq_NodeComputeLag( int LValue, int Fi )           { return (LValue + 1024*Fi)/Fi - 1024 - (int)(LValue % Fi == 0);      }
+
+// 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 Vec_Str_t *    Seq_NodeLags( Abc_Obj_t * pNode )                        { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLags;            }
+static inline char           Seq_NodeGetLag( Abc_Obj_t * pNode )                      { return Vec_StrEntry( Seq_NodeLags(pNode), (pNode)->Id );         }
+static inline void           Seq_NodeSetLag( Abc_Obj_t * pNode, char Value )          { Vec_StrWriteEntry( Seq_NodeLags(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 )                           { return (Seq_Lat_t *)Extra_MmFixedEntryFetch( ((Abc_Seq_t*)pObj->pNtk->pManFunc)->pMmInits ); }
+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; }
+
+// 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                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== 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 );  
+/*=== seqFpgaIter.c ============================================================*/
+extern void                  Seq_NtkSeqFpgaMapping( Abc_Ntk_t * pNtk, int fVerbose );
+/*=== seqRetIter.c =============================================================*/
+extern void                  Seq_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose );
+extern int                   Seq_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags, int fVerbose );
+/*=== seqUtil.c ================================================================*/
+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 );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/base/seq/seqLatch.c b/src/base/seq/seqLatch.c
new file mode 100644
index 00000000..61a71fef
--- /dev/null
+++ b/src/base/seq/seqLatch.c
@@ -0,0 +1,192 @@
+/**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 );
+    Abc_ObjAddFaninL( pObj, Edge, 1 );
+}
+
+/**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 );
+    Abc_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 );
+    Abc_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 ); 
+    Abc_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) );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqMan.c b/src/base/seq/seqMan.c
new file mode 100644
index 00000000..95192ae2
--- /dev/null
+++ b/src/base/seq/seqMan.c
@@ -0,0 +1,110 @@
+/**CFile****************************************************************
+
+  FileName    [seqMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    []
+
+  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 []
+               
+  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;
+    // create internal data structures
+    p->vInits   = Vec_PtrStart( 2 * p->nSize ); 
+    p->pMmInits = Extra_MmFixedStart( sizeof(Seq_Lat_t) );
+    p->vLValues = Vec_IntStart( p->nSize ); 
+    p->vLags    = 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_PtrFill( p->vInits,   2 * p->nSize, NULL ); 
+    Vec_IntFill( p->vLValues, p->nSize, 0 ); 
+    Vec_StrFill( p->vLags,    p->nSize, 0 ); 
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates sequential AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_Delete( Abc_Seq_t * p )
+{
+    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->vMapBags )  Vec_VecFree( p->vMapBags );  // the nodes included in the cuts used in the mapping
+    if ( p->vMapLags )  Vec_VecFree( p->vMapLags );  // the lags of the mapped nodes
+
+    if ( p->vBestCuts ) Vec_PtrFree( p->vBestCuts ); // the best cuts for nodes
+    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
+    Vec_PtrFree( p->vInits );
+    Extra_MmFixedStop( p->pMmInits, 0 );
+    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..be02d4a7
--- /dev/null
+++ b/src/base/seq/seqMapCore.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [seqMapCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    []
+
+  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"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqMapIter.c b/src/base/seq/seqMapIter.c
new file mode 100644
index 00000000..ec954d68
--- /dev/null
+++ b/src/base/seq/seqMapIter.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [seqMapIter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    []
+
+  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"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
new file mode 100644
index 00000000..94c2b944
--- /dev/null
+++ b/src/base/seq/seqRetCore.c
@@ -0,0 +1,822 @@
+/**CFile****************************************************************
+
+  FileName    [seqRetCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    []
+
+  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 fInitial, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    int RetValue;
+    if ( !fInitial )
+        Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC );
+    // get the retiming lags
+    Seq_NtkSeqRetimeDelayLags( pNtk, fVerbose );
+    // 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( Abc_ObjFaninL0(pObj) >= 1 );
+    assert( Abc_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;
+    // add the init values to the fanouts
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        Seq_NodeInsertLast( pFanout, Abc_ObjFanoutEdgeNum(pObj, pFanout), Init );
+}
+
+
+
+/**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 );
+    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 );
+
+    // 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_NtkCreateCone( 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_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 );
+    Abc_NtkDelete( pNtkMiter );
+
+    // solve the miter
+clk = clock();
+    RetValue = Abc_NtkMiterSat( pNtkCnf, 30, 0 );
+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 )
+    {
+        Init = Seq_NodeGetInitLast( pFanout, Abc_ObjFanoutEdgeNum(pObj, pFanout) );
+        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 latchs have don't-care values
+    // the new values on the fanin edges will be don't-cares
+    if ( !fMet0 && !fMet1 && !fMetN )
+    {
+        // update the fanout edges
+        Abc_ObjForEachFanout( pObj, pFanout, i )
+            Seq_NodeDeleteLast( pFanout, Abc_ObjFanoutEdgeNum(pObj, pFanout) );
+        // 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 );
+    }
+
+    // perform the changes
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        Edge = Abc_ObjFanoutEdgeNum( pObj, pFanout );
+        Value = Seq_NodeDeleteLast( pFanout, Edge );
+        if ( Value != ABC_INIT_NONE )
+            continue;
+        // value is unknown, remove it from the table
+        RetEdge.iNode  = pFanout->Id;
+        RetEdge.iEdge  = Edge;
+        RetEdge.iLatch = Abc_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 );
+    }
+
+    // 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 = Abc_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) ", Abc_ObjFaninL0(pNode), Abc_ObjFaninL0(pNode) );
+        // unmark the node as processed
+        pNode->fMarkA = 0;
+        // get the number of latches to retime
+        if ( fForward )
+            nLatches = Abc_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( Abc_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 ) );
+    // 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 = Abc_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( Abc_ObjFaninL0(pObj) >= nLatches );
+//    assert( Abc_ObjFaninL1(pObj) >= nLatches );
+    // subtract these latches on the fanin side
+    Abc_ObjAddFaninL0( pObj, -nLatches );
+    Abc_ObjAddFaninL1( pObj, -nLatches );
+    // add these latches on the fanout size
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        Abc_ObjAddFanoutL( pObj, pFanout, nLatches );
+}
+
+/**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 );
+    // subtract these latches on the fanout side
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+//        assert( Abc_ObjFanoutL(pObj, pFanout) >= nLatches );
+        Abc_ObjAddFanoutL( pObj, pFanout, -nLatches );
+    }
+    // add these latches on the fanin size
+    Abc_ObjAddFaninL0( pObj, nLatches );
+    Abc_ObjAddFaninL1( pObj, nLatches );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqRetIter.c b/src/base/seq/seqRetIter.c
new file mode 100644
index 00000000..ee2c31b2
--- /dev/null
+++ b/src/base/seq/seqRetIter.c
@@ -0,0 +1,226 @@
+/**CFile****************************************************************
+
+  FileName    [seqRetIter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    []
+
+  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_NodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
+
+// node status after updating its arrival time
+enum { SEQ_UPDATE_FAIL, SEQ_UPDATE_NO, SEQ_UPDATE_YES };
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Retimes AIG for optimal delay using Pan's algorithm.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Obj_t * pNode;
+    int i, FiMax, FiBest, RetValue;
+
+    assert( Abc_NtkIsSeq( pNtk ) );
+
+    // get the upper bound on the clock period
+//    FiMax = Abc_NtkNodeNum(pNtk);
+    FiMax = 0;
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        if ( FiMax < (int)pNode->Level )
+            FiMax = pNode->Level;
+    FiMax += 2;
+
+    // make sure this clock period is feasible
+    assert( Seq_RetimeForPeriod( pNtk, FiMax, fVerbose ) );
+
+    // search for the optimal clock period between 0 and nLevelMax
+    FiBest = Seq_RetimeSearch_rec( pNtk, 0, FiMax, fVerbose );
+
+    // recompute the best LValues
+    RetValue = Seq_RetimeForPeriod( pNtk, FiBest, fVerbose );
+    assert( RetValue );
+
+    // write the retiming lags
+    Vec_StrFill( p->vLags, p->nSize, 0 );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        Seq_NodeSetLag( pNode, (char)Seq_NodeComputeLag(Seq_NodeGetLValue(pNode), FiBest) );
+
+    // print the result
+    if ( fVerbose )
+    printf( "The best clock period is %3d.\n", FiBest );
+
+/*
+    printf( "LValues : " );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        printf( "%d=%d ", i, Seq_NodeGetLValue(pNode) );
+    printf( "\n" );
+    printf( "Lags : " );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        if ( Vec_StrEntry(p->vLags,i) != 0 )
+            printf( "%d=%d(%d)(%d) ", i, Vec_StrEntry(p->vLags,i), Seq_NodeGetLValue(pNode), Seq_NodeGetLValue(pNode) - FiBest * Vec_StrEntry(p->vLags,i) );
+    printf( "\n" );
+*/
+}
+
+/**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 for the constant 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 < 20; c++ )
+    {
+        fChange = 0;
+        Abc_NtkForEachObj( pNtk, pObj, i )
+        {
+            if ( Abc_ObjIsPi(pObj) )
+                continue;
+            if ( Abc_ObjFaninNum(pObj) == 0 )
+                continue;
+            RetValue = Seq_NodeUpdateLValue( pObj, Fi );
+            Counter++;
+            if ( RetValue == SEQ_UPDATE_FAIL )
+                break;
+            if ( RetValue == SEQ_UPDATE_NO ) 
+                continue;
+            fChange = 1;
+        }
+        if ( RetValue == SEQ_UPDATE_FAIL )
+            break;
+        if ( fChange == 0 )
+            break;
+    }
+    if ( c == 20 )
+    {
+        RetValue = SEQ_UPDATE_FAIL;
+        pReason = "(timeout)";
+    }
+
+    // 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 );
+    }
+    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_NodeUpdateLValue( 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 * Abc_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 * Abc_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/seqShare.c b/src/base/seq/seqShare.c
new file mode 100644
index 00000000..8f7432f0
--- /dev/null
+++ b/src/base/seq/seqShare.c
@@ -0,0 +1,161 @@
+/**CFile****************************************************************
+
+  FileName    [seqShare.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    []
+
+  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 Abc_NodeSeqShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
+static void Abc_NodeSeqShareOne( 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_NtkSeqShareFanouts( 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 )
+        Abc_NodeSeqShareFanouts( pObj, vNodes );
+    // share the node latches
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Abc_NodeSeqShareFanouts( pObj, vNodes );
+    Vec_PtrFree( vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the node to take fanout sharing into account.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSeqShareFanouts( 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 ( Abc_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
+    {
+        Abc_NodeSeqShareOne( pNode, ABC_INIT_ZERO, vNodes );     // shares 0 and DC
+        Abc_NodeSeqShareOne( pNode, ABC_INIT_ONE,  vNodes );     // shares 1 and DC
+    }
+    else if ( nLatches[ABC_INIT_ZERO] > 1 ) // 0-group
+        Abc_NodeSeqShareOne( pNode, ABC_INIT_ZERO, vNodes );     // shares 0 and DC
+    else if ( nLatches[ABC_INIT_ONE] > 1 ) // 1-group
+        Abc_NodeSeqShareOne( pNode, ABC_INIT_ONE,  vNodes );     // shares 1 and DC
+    else if ( nLatches[ABC_INIT_DC] > 1 ) // DC-group
+    {
+        if ( nLatches[ABC_INIT_ZERO] > 0 )
+            Abc_NodeSeqShareOne( pNode, ABC_INIT_ZERO, vNodes ); // shares 0 and DC
+        else 
+            Abc_NodeSeqShareOne( pNode, ABC_INIT_ONE,  vNodes ); // shares 1 and DC
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the node to take fanout sharing into account.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNodes )
+{
+    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 ( Abc_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 );
+    Seq_NodeInsertFirst( pBuffer, 0, InitNew );
+
+    // redirect the fanouts
+    Vec_PtrForEachEntry( vNodes, pFanout, i )
+        Abc_ObjPatchFanin( pFanout, pNode, pBuffer );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqUtil.c b/src/base/seq/seqUtil.c
new file mode 100644
index 00000000..ce92bd33
--- /dev/null
+++ b/src/base/seq/seqUtil.c
@@ -0,0 +1,345 @@
+/**CFile****************************************************************
+
+  FileName    [seqUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    []
+
+  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_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 = Abc_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 = Abc_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 += Abc_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 += Abc_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 = Abc_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 = Abc_ObjFaninLMax( pObj );
+        if ( Max < Cur )
+            Max = Cur;
+    }
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        Cur = Abc_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 = Abc_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 );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+