Version abc51120

13 files changed, 799 insertions, 129 deletions

diff --git a/src/base/seq/seq.h b/src/base/seq/seq.h
index 8e0d9c09..cbffe0bd 100644
--- a/src/base/seq/seq.h
+++ b/src/base/seq/seq.h
@@ -43,8 +43,11 @@ typedef struct Abc_Seq_t_  Abc_Seq_t;
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== seqFpgaCore.c ===============================================================*/
+extern Abc_Ntk_t *     Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int fVerbose );
 /*=== seqLatch.c ===============================================================*/
 extern void            Seq_NodeDupLats( Abc_Obj_t * pObjNew, Abc_Obj_t * pObj, int Edge );
+extern int             Seq_NodeCompareLats( Abc_Obj_t * pObj1, int Edge1, Abc_Obj_t * pObj2, int Edge2 );
 /*=== seqMan.c ===============================================================*/
 extern Abc_Seq_t *     Seq_Create( Abc_Ntk_t * pNtk );
 extern void            Seq_Resize( Abc_Seq_t * p, int nMaxId );
@@ -53,7 +56,7 @@ extern void            Seq_Delete( Abc_Seq_t * p );
 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 );
+extern void            Seq_NtkShareFanouts( 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 );
diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c
index 4c66576b..0816c673 100644
--- a/src/base/seq/seqCreate.c
+++ b/src/base/seq/seqCreate.c
@@ -6,7 +6,7 @@
 
   PackageName [Construction and manipulation of sequential AIGs.]
 
-  Synopsis    []
+  Synopsis    [Transformations to and from the sequential AIG.]
 
   Author      [Alan Mishchenko]
   
@@ -100,9 +100,9 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
         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; 
+        pObj->pCopy->Id     = pObj->Id;      // the ID is the same for both
+        pObj->pCopy->fPhase = pObj->fPhase;  // used to work with choices
+        pObj->pCopy->Level  = pObj->Level;   // used for upper bound on clock cycle
         Vec_PtrWriteEntry( pNtkNew->vObjs, pObj->pCopy->Id, pObj->pCopy );
         pNtkNew->nObjs++;
     }
diff --git a/src/base/seq/seqFpgaCore.c b/src/base/seq/seqFpgaCore.c
index 37ef6cb7..a40caf34 100644
--- a/src/base/seq/seqFpgaCore.c
+++ b/src/base/seq/seqFpgaCore.c
@@ -6,7 +6,7 @@
 
   PackageName [Construction and manipulation of sequential AIGs.]
 
-  Synopsis    []
+  Synopsis    [The core of FPGA mapping/retiming package.]
 
   Author      [Alan Mishchenko]
   
@@ -24,8 +24,14 @@
 ///                        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 );
+static Abc_Ntk_t *  Seq_NtkFpgaDup( Abc_Ntk_t * pNtk );
+static int          Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t *  Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtkNew );
+static int          Seq_FpgaMappingCount( Abc_Ntk_t * pNtk );
+static int          Seq_FpgaMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
+static DdNode *     Seq_FpgaMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
+static void         Seq_FpgaMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges );
+static Abc_Obj_t *  Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, Vec_Ptr_t * vLeaves );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -42,23 +48,28 @@ static Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Seq_NtkSeqFpgaRetime( Abc_Ntk_t * pNtk, int fVerbose )
+Abc_Ntk_t * Seq_NtkFpgaMapRetime( 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 );
+    // find the best mapping and retiming for all nodes (p->vLValues, p->vBestCuts, p->vLags)
+    Seq_FpgaMappingDelays( 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 );
+    pNtkNew = Seq_NtkFpgaDup( pNtk );
+    // implement the retiming
+    RetValue = Seq_NtkImplementRetiming( pNtkNew, ((Abc_Seq_t *)pNtkNew->pManFunc)->vLags, fVerbose );
     if ( RetValue == 0 )
         printf( "Retiming completed but initial state computation has failed.\n" );
+    // check the compatibility of initial states computed
+    if ( RetValue = Seq_NtkFpgaInitCompatible( pNtkNew ) )
+    {
+        printf( "The number of LUTs with incompatible edges = %d.\n", RetValue );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
     // create the final mapped network
-    pNtkMap = Seq_NtkSeqFpgaMapped( pNtkNew, pNtk );
+    pNtkMap = Seq_NtkSeqFpgaMapped( pNtkNew );
     Abc_NtkDelete( pNtkNew );
     return pNtkMap;
 }
@@ -67,82 +78,169 @@ Abc_Ntk_t * Seq_NtkSeqFpgaRetime( Abc_Ntk_t * pNtk, int fVerbose )
 
   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).]
+  Description [Information about mapping is given as mapping nodes (p->vMapAnds)
+  and best cuts for each node (p->vMapCuts).]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Seq_NtkSeqFpgaDup( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Seq_NtkFpgaDup( Abc_Ntk_t * pNtk )
 {
-    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Seq_t * pNew, * 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;
+    Abc_Obj_t * pObj, * pLeaf;
+    Vec_Ptr_t * vLeaves;
+    unsigned SeqEdge;
+    int i, k, nObjsNew;
     
     assert( Abc_NtkIsSeq(pNtk) );
 
-    // start the network
+    // start the expanded 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) );
+    nObjsNew = 1 + Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk) + Seq_FpgaMappingCount(pNtk);
+    Seq_Resize( pNtkNew->pManFunc, nObjsNew );
 
-    // create the nodes
+    // duplicate the nodes in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj );
+
+    // recursively construct the internals of each node
     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;
+        Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, pObj->Id << 8, 1, vLeaves );
     }
+    assert( nObjsNew == pNtkNew->nObjs );
 
     // set the POs
-    Abc_NtkForEachPo( pNtk, pObj, i )
+    Abc_NtkFinalize( pNtk, pNtkNew );
+
+//Abc_NtkShowAig( pNtkNew );
+
+    // transfer the mapping info to the new manager
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
     {
-        pDriver    = Abc_ObjFanin0(pObj);
-        pDriverNew = Abc_ObjNotCond(pDriver->pNext, Abc_ObjFaninC0(pObj));
-        Abc_ObjAddFanin( pObj->pCopy, pDriverNew );
+        // convert the root node
+        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
+        // get the leaves of the cut
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // convert the leaf nodes
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+            // translate the old leaf into the leaf in the new network
+            Vec_PtrWriteEntry( vLeaves, k, (void *)((pLeaf->pCopy->Id << 8) | (SeqEdge & 255)) );
+//            printf( "%d -> %d\n", pLeaf->Id, pLeaf->pCopy->Id );
+        }
     }
+    pNew = pNtkNew->pManFunc;
+    pNew->nVarsMax  = p->nVarsMax;
+    pNew->vMapAnds  = p->vMapAnds;   p->vMapAnds  = NULL;
+    pNew->vMapCuts  = p->vMapCuts;   p->vMapCuts  = NULL;
 
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Seq_NtkSeqFpgaDup(): Network check has failed.\n" );
+        fprintf( stdout, "Seq_NtkFpgaDup(): Network check has failed.\n" );
     return pNtkNew;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the initial states are compatible.]
+
+  Description [Checks of all the initial states on the fanins edges
+  of the cut have compatible number of latches and initial states.
+  If this is not true, then the mapped network with the does not have initial 
+  state. Returns the number of LUTs with incompatible edges.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Obj_t * pAnd, * pLeaf, * pFanout0, * pFanout1;
+    Vec_Vec_t * vTotalEdges;
+    Vec_Ptr_t * vLeaves, * vEdges;
+    int i, k, m, Edge0, Edge1, nLatchBefore, nLatchAfter, nLatches1, nLatches2;
+    unsigned SeqEdge;
+    int CountBad = 0;
+
+    vTotalEdges = Vec_VecStart( p->nVarsMax );
+    // go through all the nodes (cuts) used in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pAnd, i )
+    {
+//        printf( "*** Node %d.\n", pAnd->Id );
+
+        // get the cut of this gate
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+
+        // get the edges pointing to the leaves
+        Vec_VecClear( vTotalEdges );
+        Seq_FpgaMappingEdges_rec( pNtk, pAnd->Id << 8, NULL, vLeaves, vTotalEdges );
+
+        // for each leaf, consider its edges
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+            nLatchBefore = SeqEdge & 255;
+
+            // get the resulting lag of this node
+            nLatchAfter = nLatchBefore + Seq_NodeGetLag(pAnd) - Seq_NodeGetLag(pLeaf);
+            assert( nLatchAfter >= 0 );
+            if ( nLatchAfter == 0 )
+                continue;
+
+            // go through the edges
+            vEdges = Vec_VecEntry( vTotalEdges, k );
+            pFanout0 = NULL;
+            Vec_PtrForEachEntry( vEdges, pFanout1, m )
+            {
+                Edge1    = Abc_ObjIsComplement(pFanout1);
+                pFanout1 = Abc_ObjRegular(pFanout1);
+//printf( "Fanin = %d. Fanout = %d.\n", pLeaf->Id, pFanout1->Id );
+
+                // make sure this is the same fanin
+                if ( Edge1 )
+                    assert( pLeaf == Abc_ObjFanin1(pFanout1) );
+                else
+                    assert( pLeaf == Abc_ObjFanin0(pFanout1) );
+
+                // save the first one
+                if ( pFanout0 == NULL )
+                {
+                    pFanout0 = pFanout1;
+                    Edge0    = Edge1;
+                    continue;
+                }
+                // compare the rings
+                // if they have different number of latches, this is the bug
+                nLatches1 = Seq_NodeCountLats(pFanout0, Edge0);
+                nLatches2 = Seq_NodeCountLats(pFanout1, Edge1);
+                assert( nLatches1 == nLatches2 );
+                assert( nLatches1 > 0 );
+
+                // if they have different initial states, this is the problem
+                if ( !Seq_NodeCompareLats(pFanout0, Edge0, pFanout1, Edge1) )
+                {
+                    CountBad++;
+                    break;
+                }
+            }
+        }
+    }
+    Vec_VecFree( vTotalEdges );
+    return CountBad;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Derives the final mapped network.]
@@ -154,15 +252,314 @@ Abc_Ntk_t * Seq_NtkSeqFpgaDup( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
 {
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Seq_Lat_t * pLat, * pRing;
     Abc_Ntk_t * pNtkMap; 
-    pNtkMap = NULL;
+    Vec_Vec_t * vTotalEdges;
+    Vec_Ptr_t * vLeaves, * vMapEdges;
+    Abc_Obj_t * pObj, * pAnd, * pLeaf, * pFanout, * pFanin, * pLatch;
+    int i, k, m, Edge, nLatches, nLatchBefore, nLatchAfter;
+    unsigned SeqEdge;
+
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    // start the network
+    pNtkMap = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+
+    // duplicate the nodes used in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pAnd, i )
+    {
+        pAnd->pCopy = Abc_NtkCreateNode( pNtkMap );
+        // get the leaves of this gate
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // get the BDD of the node
+        pAnd->pCopy->pData = Seq_FpgaMappingBdd_rec( pNtkMap->pManFunc, pNtk, pAnd->Id << 8, vLeaves );
+        Cudd_Ref( pAnd->pCopy->pData );
+    }   
+
+    // construct nodes in the mapped network
+    vTotalEdges = Vec_VecStart( p->nVarsMax );
+    Vec_PtrForEachEntry( p->vMapAnds, pAnd, i )
+    {
+        // get the leaves of this gate
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // get the edges pointing to the leaves
+        Vec_VecClear( vTotalEdges );
+        Seq_FpgaMappingEdges_rec( pNtk, pAnd->Id << 8, NULL, vLeaves, vTotalEdges );
+        // for each leaf, consider its edges
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+            nLatchBefore = SeqEdge & 255;
+
+            // get the resulting lag of this node
+            nLatchAfter = nLatchBefore + Seq_NodeGetLag(pAnd) - Seq_NodeGetLag(pLeaf);
+            assert( nLatchAfter >= 0 );
+            if ( nLatchAfter == 0 )
+            {
+                // add the fanin
+                Abc_ObjAddFanin( pAnd->pCopy, pLeaf->pCopy );
+                continue;
+            }
+
+            // get the first edge
+            vMapEdges = Vec_VecEntry( vTotalEdges, k );
+            pFanout = Vec_PtrEntry( vMapEdges, 0 );
+            Edge    = Abc_ObjIsComplement(pFanout);
+            pFanout = Abc_ObjRegular(pFanout);
+            // make sure this is the same fanin
+            if ( Edge )
+                assert( pLeaf == Abc_ObjFanin1(pFanout) );
+            else
+                assert( pLeaf == Abc_ObjFanin0(pFanout) );
+            nLatches = Seq_NodeCountLats(pFanout, Edge);
+            assert( nLatches > 0 );
+
+            // for each implicit latch add the real latch
+            pFanin = pLeaf->pCopy;
+            pRing  = Seq_NodeGetRing(pFanout, Edge);
+            for ( m = 0, pLat = Seq_LatPrev(pRing); m < nLatches; m++, pLat = Seq_LatPrev(pLat) )
+            {
+                pLatch = Abc_NtkCreateLatch( pNtkMap );
+                pLatch->pData = (void *)Seq_LatInit(pLat);
+                Abc_ObjAddFanin( pLatch, pFanin );
+                pFanin = pLatch;
+            }
+            // finally connect to the latch
+            Abc_ObjAddFanin( pAnd->pCopy, pFanin );
+        }
+    }
+    Vec_VecFree( vTotalEdges );
+
+    // set the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0(pObj)->pCopy;
+        if ( Abc_ObjFaninL0(pObj) > 0 )
+        {
+            pRing = Seq_NodeGetRing(pObj, 0);
+            for ( m = 0, pLat = Seq_LatPrev(pRing); m < nLatches; m++, pLat = Seq_LatPrev(pLat) )
+            {
+                pLatch = Abc_NtkCreateLatch( pNtkMap );
+                pLatch->pData = (void *)Seq_LatInit(pLat);
+                Abc_ObjAddFanin( pLatch, pFanin );
+                pFanin = pLatch;
+            }
+        }
+        pFanin = Abc_ObjNotCond(pFanin, Abc_ObjFaninC0(pObj));
+        Abc_ObjAddFanin( pObj->pCopy, pFanin );
+    }
+
+    // add the latches and their names
+    Abc_NtkAddDummyLatchNames( pNtkMap );
+    Abc_NtkForEachLatch( pNtkMap, pLatch, i )
+    {
+        Vec_PtrPush( pNtkMap->vCis, pLatch );
+        Vec_PtrPush( pNtkMap->vCos, pLatch );
+    }
+
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkMap, 1 );
+
     if ( !Abc_NtkCheck( pNtkMap ) )
         fprintf( stdout, "Seq_NtkSeqFpgaMapped(): Network check has failed.\n" );
     return pNtkMap;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nodes in the bag.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_FpgaMappingCount( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Vec_Ptr_t * vLeaves;
+    Abc_Obj_t * pAnd;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( p->vMapAnds, pAnd, i )
+    {
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        Counter += Seq_FpgaMappingCount_rec( pNtk, pAnd->Id << 8, vLeaves );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nodes in the bag.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_FpgaMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj, * pLeaf;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+            return 0;
+    // continue unfolding
+    assert( Abc_NodeIsAigAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Abc_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Abc_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Abc_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Abc_ObjFaninL1(pObj);
+    // call for the children
+    return 1 + Seq_FpgaMappingCount_rec( pNtk, SeqEdge0, vLeaves ) + 
+        Seq_FpgaMappingCount_rec( pNtk, SeqEdge1, vLeaves );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the BDD of the selected cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Seq_FpgaMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj, * pLeaf;
+    DdNode * bFunc0, * bFunc1, * bFunc;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+            return Cudd_bddIthVar( dd, i );
+    // continue unfolding
+    assert( Abc_NodeIsAigAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Abc_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Abc_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Abc_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Abc_ObjFaninL1(pObj);
+    // call for the children
+    bFunc0 = Seq_FpgaMappingBdd_rec( dd, pNtk, SeqEdge0, vLeaves );    Cudd_Ref( bFunc0 );
+    bFunc1 = Seq_FpgaMappingBdd_rec( dd, pNtk, SeqEdge1, vLeaves );    Cudd_Ref( bFunc1 );
+    // get the BDD of the node
+    bFunc  = Cudd_bddAnd( dd, Cudd_NotCond(bFunc0, Abc_ObjFaninC0(pObj)), Cudd_NotCond(bFunc1, Abc_ObjFaninC1(pObj)) );  Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( dd, bFunc0 );
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    // return the BDD
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_FpgaMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges )
+{
+    Abc_Obj_t * pObj, * pLeaf;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+            assert( pPrev != NULL );
+            Vec_VecPush( vMapEdges, i, pPrev );
+            return;
+        }
+    }
+    // continue unfolding
+    assert( Abc_NodeIsAigAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Abc_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Abc_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Abc_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Abc_ObjFaninL1(pObj);
+    // call for the children    
+    Seq_FpgaMappingEdges_rec( pNtk, SeqEdge0, pObj            , vLeaves, vMapEdges );
+    Seq_FpgaMappingEdges_rec( pNtk, SeqEdge1, Abc_ObjNot(pObj), vLeaves, vMapEdges );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1;
+    unsigned SeqEdge0, SeqEdge1;
+    int TotalLag, Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+            return pObj->pCopy;
+    // continue unfolding
+    assert( Abc_NodeIsAigAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Abc_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Abc_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Abc_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Abc_ObjFaninL1(pObj);
+    // call for the children    
+    pObjNew = fTop? pObj->pCopy : Abc_NtkCreateNode( pNtkNew );
+    // solve subproblems
+    pFaninNew0 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, vLeaves );
+    pFaninNew1 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, vLeaves );
+    // add the fanins to the node
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) );
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) );
+    Seq_NodeDupLats( pObjNew, pObj, 0 );
+    Seq_NodeDupLats( pObjNew, pObj, 1 );
+    // set the lag of the new node equal to the internal lag plus mapping/retiming lag
+    TotalLag = Lag + Seq_NodeGetLag(pObj);
+    Seq_NodeSetLag( pObjNew, (char)TotalLag );
+    return pObjNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqFpgaIter.c b/src/base/seq/seqFpgaIter.c
index cb0c739b..c2777606 100644
--- a/src/base/seq/seqFpgaIter.c
+++ b/src/base/seq/seqFpgaIter.c
@@ -6,7 +6,7 @@
 
   PackageName [Construction and manipulation of sequential AIGs.]
 
-  Synopsis    []
+  Synopsis    [Iterative delay computation in FPGA mapping/retiming package.]
 
   Author      [Alan Mishchenko]
   
@@ -19,18 +19,25 @@
 ***********************************************************************/
 
 #include "seqInt.h"
+#include "main.h"
+#include "fpga.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static void        Seq_FpgaMappingCollectNode_rec( Abc_Obj_t * pAnd, Vec_Ptr_t * vMapping, Vec_Vec_t * vMapCuts );
+static Cut_Cut_t * Seq_FpgaMappingSelectCut( Abc_Obj_t * pAnd );
+
+extern Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Computes the retiming lags for FPGA mapping.]
 
   Description []
                
@@ -39,10 +46,214 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_NtkSeqFpgaMapping( Abc_Ntk_t * pNtk, int fVerbose )
+void Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose )
 {
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Cut_Params_t Params, * pParams = &Params;
+    Abc_Obj_t * pObj;
+    int i, clk;
+
+    // get the LUT library
+    p->nVarsMax = Fpga_LutLibReadVarMax( Abc_FrameReadLibLut() );
+
+    // set defaults for cut computation
+    memset( pParams, 0, sizeof(Cut_Params_t) );
+    pParams->nVarsMax  = p->nVarsMax;  // the max cut size ("k" of the k-feasible cuts)
+    pParams->nKeepMax  = 1000;  // the max number of cuts kept at a node
+    pParams->fTruth    = 0;     // compute truth tables
+    pParams->fFilter   = 1;     // filter dominated cuts
+    pParams->fSeq      = 1;     // compute sequential cuts
+    pParams->fVerbose  = 0;     // the verbosiness flag
+
+    // compute the cuts
+clk = clock();
+    p->pCutMan = Abc_NtkSeqCuts( pNtk, pParams );
+p->timeCuts = clock() - clk;
+    if ( fVerbose )
+    Cut_ManPrintStats( p->pCutMan );
+
+    // compute the delays
+clk = clock();
+    Seq_NtkRetimeDelayLags( pNtk, fVerbose );
+p->timeDelay = clock() - clk;
+
+    // collect the nodes and cuts used in the mapping
+    p->vMapAnds = Vec_PtrAlloc( 1000 );
+    p->vMapCuts = Vec_VecAlloc( 1000 );
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_FpgaMappingCollectNode_rec( Abc_ObjFanin0(pObj), p->vMapAnds, p->vMapCuts );
+
+printf( "The number of LUTs = %d.\n", Vec_PtrSize(p->vMapAnds) );
+
+    // remove the cuts
+    Cut_ManStop( p->pCutMan );
+    p->pCutMan = NULL;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Derives the parameters of the best mapping/retiming for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_FpgaMappingCollectNode_rec( Abc_Obj_t * pAnd, Vec_Ptr_t * vMapping, Vec_Vec_t * vMapCuts )
+{
+    Abc_Obj_t * pFanin;
+    Cut_Cut_t * pCutBest;
+    int k;
+
+    // skip if this is a non-PI node
+    if ( !Abc_NodeIsAigAnd(pAnd) )
+        return;
+    // skip a visited node
+    if ( Abc_NodeIsTravIdCurrent(pAnd) )
+        return;
+    Abc_NodeSetTravIdCurrent(pAnd);
+
+    // visit the fanins of the node
+    pCutBest = Seq_FpgaMappingSelectCut( pAnd );
+    for ( k = 0; k < (int)pCutBest->nLeaves; k++ )
+    {
+        pFanin = Abc_NtkObj( pAnd->pNtk, pCutBest->pLeaves[k] >> 8 );
+        Seq_FpgaMappingCollectNode_rec( pFanin, vMapping, vMapCuts );
+    }
+
+    // add this node
+    Vec_PtrPush( vMapping, pAnd );
+    for ( k = 0; k < (int)pCutBest->nLeaves; k++ )
+        Vec_VecPush( vMapCuts, Vec_PtrSize(vMapping)-1, (void *)pCutBest->pLeaves[k] );
+
+//printf( "Adding %d.\n", pAnd->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Selects the best cut to represent the node in the mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Seq_FpgaMappingSelectCut( Abc_Obj_t * pAnd )
+{
+    Abc_Obj_t * pFanin;
+    Cut_Cut_t * pCut, * pCutBest, * pList;
+    float CostCur, CostMin = ABC_INFINITY;
+    int ArrivalCut, ArrivalMin, i;
+    // get the arrival time of the best non-trivial cut
+    ArrivalMin = Seq_NodeGetLValue( pAnd );
+    // iterate through the cuts and with the one with the minimum cost
+    pList = Abc_NodeReadCuts( Seq_NodeCutMan(pAnd), pAnd );
+    CostMin = ABC_INFINITY;
+    pCutBest = NULL;
+    for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
+    {
+        ArrivalCut = *((int *)&pCut->uSign);
+        assert( ArrivalCut >= ArrivalMin );
+        if ( ArrivalCut > ArrivalMin )
+            continue;
+        CostCur = 0.0;
+        for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        {
+            pFanin = Abc_NtkObj( pAnd->pNtk, pCut->pLeaves[i] >> 8 );
+            if ( Abc_ObjIsPi(pFanin) )
+                continue;
+            if ( Abc_NodeIsTravIdCurrent(pFanin) )
+                continue;
+            CostCur += (float)(1.0 / Abc_ObjFanoutNum(pFanin));
+        }
+        if ( CostMin > CostCur )
+        {
+            CostMin = CostCur;
+            pCutBest = pCut;
+        }
+    }
+    assert( pCutBest != NULL );
+    return pCutBest;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the cut.]
+
+  Description [The node should be internal.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Seq_FpgaCutUpdateLValue( Cut_Cut_t * pCut, Abc_Obj_t * pObj, int Fi )
+{
+    Abc_Obj_t * pFanin;
+    int i, lValueMax, lValueCur;
+    assert( Abc_NodeIsAigAnd(pObj) );
+    lValueMax = -ABC_INFINITY;
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+    {
+//        lValue0 = Seq_NodeGetLValue(Abc_ObjFanin0(pObj)) - Fi * Abc_ObjFaninL0(pObj);
+        pFanin    = Abc_NtkObj(pObj->pNtk, pCut->pLeaves[i] >> 8);
+        lValueCur = Seq_NodeGetLValue(pFanin) - Fi * (pCut->pLeaves[i] & 255);
+        if ( lValueMax < lValueCur )
+            lValueMax = lValueCur;
+    }
+    lValueMax += 1;
+    *((int *)&pCut->uSign) = lValueMax;
+    return lValueMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the node.]
+
+  Description [The node can be internal or a PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_FpgaNodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
+{
+    Cut_Cut_t * pCut, * pList;
+    int lValueNew, lValueOld, lValueCut;
+    assert( !Abc_ObjIsPi(pObj) );
+    assert( Abc_ObjFaninNum(pObj) > 0 );
+    if ( Abc_ObjIsPo(pObj) )
+    {
+        lValueNew = Seq_NodeGetLValue(Abc_ObjFanin0(pObj)) - Fi * Abc_ObjFaninL0(pObj);
+        return (lValueNew > Fi)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO;
+    }
+    // get the arrival time of the best non-trivial cut
+    pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj );
+    lValueNew = ABC_INFINITY;
+    for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
+    {
+        lValueCut = Seq_FpgaCutUpdateLValue( pCut, pObj, Fi );
+        if ( lValueNew > lValueCut )
+            lValueNew = lValueCut;
+    }
+    // compare the arrival time with the previous arrival time
+    lValueOld = Seq_NodeGetLValue(pObj);
+//    if ( lValueNew == lValueOld )
+    if ( lValueNew <= lValueOld )
+        return SEQ_UPDATE_NO;
+//printf( "%d ", lValueNew );
+    Seq_NodeSetLValue( pObj, lValueNew );
+    return SEQ_UPDATE_YES;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqInt.h b/src/base/seq/seqInt.h
index 2159480a..6cb1fecc 100644
--- a/src/base/seq/seqInt.h
+++ b/src/base/seq/seqInt.h
@@ -6,7 +6,7 @@
 
   PackageName [Construction and manipulation of sequential AIGs.]
 
-  Synopsis    [External declarations.]
+  Synopsis    [Internal declarations.]
 
   Author      [Alan Mishchenko]
   
@@ -26,6 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include "abc.h"
+#include "cut.h"
 #include "seq.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -34,6 +35,9 @@
 
 #define SEQ_FULL_MASK        0xFFFFFFFF   
 
+// node status after updating its arrival time
+enum { SEQ_UPDATE_FAIL, SEQ_UPDATE_NO, SEQ_UPDATE_YES };
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -41,20 +45,21 @@
 // manager of sequential AIG
 struct Abc_Seq_t_
 {
+    // sequential information
     Abc_Ntk_t *         pNtk;           // the network
     int                 nSize;          // the number of entries in all internal arrays
     Vec_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
+    // K-feasible cuts
+    int                 nVarsMax;       // the max cut size
+    Cut_Man_t *         pCutMan;        // cut manager
+    // sequential arrival time computation
     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
@@ -99,11 +104,17 @@ static inline Seq_RetEdge_t  Seq_Int2RetEdge( int Num )            { return *((S
 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 l-values and lags
+static inline Vec_Int_t *    Seq_NodeLValues( Abc_Obj_t * pNode )               { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLValues;           }
+static inline 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 best cuts at each node
+static inline Cut_Man_t *    Seq_NodeCutMan( Abc_Obj_t * pNode )                { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->pCutMan;                 }
+//static inline Vec_Ptr_t *    Seq_NodeCutBests( Abc_Obj_t * pNode )              { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vBestCuts;               }
+//static inline Cut_Cut_t *    Seq_NodeGetCutBest( Abc_Obj_t * pNode )            { return Vec_PtrEntry( Seq_NodeCutBests(pNode), (pNode)->Id );            }
+//static inline void           Seq_NodeSetCutBest( Abc_Obj_t * pNode, Cut_Cut_t * pCut ) { Vec_PtrWriteEntry( Seq_NodeCutBests(pNode), (pNode)->Id, pCut ); }
 
 // reading the contents of the lat
 static inline Abc_InitType_t Seq_LatInit( Seq_Lat_t * pLat )  { return ((unsigned)pLat->pPrev) & 3;                                 }
@@ -149,9 +160,10 @@ extern void                  Seq_NodeInsertLast( Abc_Obj_t * pObj, int Edge, Abc
 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 );
+extern void                  Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose );
+extern int                   Seq_FpgaNodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
 /*=== seqRetIter.c =============================================================*/
-extern void                  Seq_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose );
+extern void                  Seq_NtkRetimeDelayLags( 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 );
diff --git a/src/base/seq/seqLatch.c b/src/base/seq/seqLatch.c
index 61a71fef..f5106b24 100644
--- a/src/base/seq/seqLatch.c
+++ b/src/base/seq/seqLatch.c
@@ -185,6 +185,36 @@ void Seq_NodeDupLats( Abc_Obj_t * pObjNew, Abc_Obj_t * pObj, int Edge )
         Seq_NodeInsertLast( pObjNew, Edge, Seq_LatInit(pLat) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Insert the last Lat on the edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NodeCompareLats( Abc_Obj_t * pObj1, int Edge1, Abc_Obj_t * pObj2, int Edge2 )  
+{ 
+    Seq_Lat_t * pRing1, * pRing2, * pLat1, * pLat2;
+    int i, nLatches1, nLatches2;
+
+    nLatches1 = Seq_NodeCountLats( pObj1, Edge1 );
+    nLatches2 = Seq_NodeCountLats( pObj2, Edge2 );
+    if ( nLatches1 != nLatches2 )
+        return 0;
+
+    pRing1 = Seq_NodeGetRing( pObj1, Edge1 );
+    pRing2 = Seq_NodeGetRing( pObj2, Edge2 );
+    for ( i = 0, pLat1 = pRing1, pLat2 = pRing2; i < nLatches1; i++, pLat1 = pLat1->pNext, pLat2 = pLat2->pNext )
+        if ( Seq_LatInit(pLat1) != Seq_LatInit(pLat2) )
+            return 0;
+
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqMan.c b/src/base/seq/seqMan.c
index 95192ae2..7074f28d 100644
--- a/src/base/seq/seqMan.c
+++ b/src/base/seq/seqMan.c
@@ -6,7 +6,7 @@
 
   PackageName [Construction and manipulation of sequential AIGs.]
 
-  Synopsis    []
+  Synopsis    [Manager of sequential AIG containing.]
 
   Author      [Alan Mishchenko]
   
@@ -32,7 +32,9 @@
 
   Synopsis    [Allocates sequential AIG manager.]
 
-  Description []
+  Description [The manager contains all the data structures needed to 
+  represent sequential AIG and compute stand-alone retiming as well as 
+  the integrated mapping/retiming of the sequential AIG.]
                
   SideEffects []
 
@@ -47,9 +49,9 @@ Abc_Seq_t * Seq_Create( Abc_Ntk_t * pNtk )
     memset( p, 0, sizeof(Abc_Seq_t) );
     p->pNtk  = pNtk;
     p->nSize = 1000;
+    p->pMmInits = Extra_MmFixedStart( sizeof(Seq_Lat_t) );
     // 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;
@@ -71,9 +73,9 @@ 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 ); 
+    Vec_PtrFill( p->vInits,    2 * p->nSize, NULL ); 
+    Vec_IntFill( p->vLValues,  p->nSize, 0 ); 
+    Vec_StrFill( p->vLags,     p->nSize, 0 ); 
 }
 
 
@@ -92,13 +94,9 @@ 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 );
+    if ( p->vInits )    Vec_PtrFree( p->vInits );    // the initial values of the latches
     Extra_MmFixedStop( p->pMmInits, 0 );
     free( p );
 }
diff --git a/src/base/seq/seqMapCore.c b/src/base/seq/seqMapCore.c
index be02d4a7..8c72538b 100644
--- a/src/base/seq/seqMapCore.c
+++ b/src/base/seq/seqMapCore.c
@@ -6,7 +6,7 @@
 
   PackageName [Construction and manipulation of sequential AIGs.]
 
-  Synopsis    []
+  Synopsis    [The core of SC mapping/retiming package.]
 
   Author      [Alan Mishchenko]
   
diff --git a/src/base/seq/seqMapIter.c b/src/base/seq/seqMapIter.c
index ec954d68..5f59ca50 100644
--- a/src/base/seq/seqMapIter.c
+++ b/src/base/seq/seqMapIter.c
@@ -6,7 +6,7 @@
 
   PackageName [Construction and manipulation of sequential AIGs.]
 
-  Synopsis    []
+  Synopsis    [Iterative delay computation in SC mapping/retiming package.]
 
   Author      [Alan Mishchenko]
   
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index 94c2b944..03b86451 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -6,7 +6,7 @@
 
   PackageName [Construction and manipulation of sequential AIGs.]
 
-  Synopsis    []
+  Synopsis    [The core of retiming procedures.]
 
   Author      [Alan Mishchenko]
   
@@ -72,7 +72,7 @@ void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fInitial, int fVerbose )
     if ( !fInitial )
         Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC );
     // get the retiming lags
-    Seq_NtkSeqRetimeDelayLags( pNtk, fVerbose );
+    Seq_NtkRetimeDelayLags( pNtk, fVerbose );
     // implement this retiming
     RetValue = Seq_NtkImplementRetiming( pNtk, p->vLags, fVerbose );
     if ( RetValue == 0 )
diff --git a/src/base/seq/seqRetIter.c b/src/base/seq/seqRetIter.c
index ee2c31b2..af239f81 100644
--- a/src/base/seq/seqRetIter.c
+++ b/src/base/seq/seqRetIter.c
@@ -6,7 +6,7 @@
 
   PackageName [Construction and manipulation of sequential AIGs.]
 
-  Synopsis    []
+  Synopsis    [The iterative L-Value computation for retiming procedures.]
 
   Author      [Alan Mishchenko]
   
@@ -27,10 +27,7 @@
 // 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 };
+static int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -47,11 +44,12 @@ enum { SEQ_UPDATE_FAIL, SEQ_UPDATE_NO, SEQ_UPDATE_YES };
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
+void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
     Abc_Obj_t * pNode;
     int i, FiMax, FiBest, RetValue;
+    char NodeLag;
 
     assert( Abc_NtkIsSeq( pNtk ) );
 
@@ -69,14 +67,17 @@ void Seq_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
     // search for the optimal clock period between 0 and nLevelMax
     FiBest = Seq_RetimeSearch_rec( pNtk, 0, FiMax, fVerbose );
 
-    // recompute the best LValues
+    // recompute the best l-values
     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) );
+    {
+        NodeLag = Seq_NodeComputeLag( Seq_NodeGetLValue(pNode), FiBest );
+        Seq_NodeSetLag( pNode, NodeLag );
+    }
 
     // print the result
     if ( fVerbose )
@@ -140,7 +141,7 @@ int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose )
     // 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
+    // set l-values of constants and PIs
     pObj = Abc_NtkObj( pNtk, 0 );
     Seq_NodeSetLValue( pObj, 0 );
     Abc_NtkForEachPi( pNtk, pObj, i )
@@ -151,13 +152,27 @@ int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose )
     for ( c = 0; c < 20; c++ )
     {
         fChange = 0;
-        Abc_NtkForEachObj( pNtk, pObj, i )
+        Abc_AigForEachAnd( pNtk, pObj, i )
         {
-            if ( Abc_ObjIsPi(pObj) )
-                continue;
-            if ( Abc_ObjFaninNum(pObj) == 0 )
+            if ( Seq_NodeCutMan(pObj) )
+                RetValue = Seq_FpgaNodeUpdateLValue( pObj, Fi );
+            else
+                RetValue = Seq_RetimeNodeUpdateLValue( pObj, Fi );
+//printf( "Node = %d. Value = %d. \n", pObj->Id, RetValue );
+            Counter++;
+            if ( RetValue == SEQ_UPDATE_FAIL )
+                break;
+            if ( RetValue == SEQ_UPDATE_NO ) 
                 continue;
-            RetValue = Seq_NodeUpdateLValue( pObj, Fi );
+            fChange = 1;
+        }
+        Abc_NtkForEachPo( pNtk, pObj, i )
+        {
+            if ( Seq_NodeCutMan(pObj) )
+                RetValue = Seq_FpgaNodeUpdateLValue( pObj, Fi );
+            else
+                RetValue = Seq_RetimeNodeUpdateLValue( pObj, Fi );
+//printf( "Node = %d. Value = %d. \n", pObj->Id, RetValue );
             Counter++;
             if ( RetValue == SEQ_UPDATE_FAIL )
                 break;
@@ -176,13 +191,17 @@ int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose )
         pReason = "(timeout)";
     }
 
+//Abc_NtkForEachObj( pNtk, pObj, i )
+//printf( "%d ", Seq_NodeGetLValue(pObj) );
+//printf( "\n" );
+
     // report the results
     if ( fVerbose )
     {
         if ( RetValue == SEQ_UPDATE_FAIL )
-            printf( "Period = %3d.  Iterations = %3d.  Updates = %10d.  Infeasible %s\n", Fi, c, Counter, pReason );
+            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 );
+            printf( "Period = %3d.  Iterations = %3d.  Updates = %10d.      Feasible\n",    Fi, c, Counter );
     }
     return RetValue != SEQ_UPDATE_FAIL;
 }
@@ -198,7 +217,7 @@ int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Seq_NodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
+int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
 {
     int lValueNew, lValueOld, lValue0, lValue1;
     assert( !Abc_ObjIsPi(pObj) );
diff --git a/src/base/seq/seqShare.c b/src/base/seq/seqShare.c
index 8f7432f0..aafc7dc5 100644
--- a/src/base/seq/seqShare.c
+++ b/src/base/seq/seqShare.c
@@ -6,7 +6,7 @@
 
   PackageName [Construction and manipulation of sequential AIGs.]
 
-  Synopsis    []
+  Synopsis    [Latch sharing at the fanout stems.]
 
   Author      [Alan Mishchenko]
   
@@ -24,8 +24,8 @@
 ///                        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 );
+static void Seq_NodeShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
+static void Seq_NodeShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNodes );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -42,7 +42,7 @@ static void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_NtkSeqShareFanouts( Abc_Ntk_t * pNtk )
+void Seq_NtkShareFanouts( Abc_Ntk_t * pNtk )
 {
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pObj;
@@ -50,10 +50,10 @@ void Seq_NtkSeqShareFanouts( Abc_Ntk_t * pNtk )
     vNodes = Vec_PtrAlloc( 10 );
     // share the PI latches
     Abc_NtkForEachPi( pNtk, pObj, i )
-        Abc_NodeSeqShareFanouts( pObj, vNodes );
+        Seq_NodeShareFanouts( pObj, vNodes );
     // share the node latches
     Abc_NtkForEachNode( pNtk, pObj, i )
-        Abc_NodeSeqShareFanouts( pObj, vNodes );
+        Seq_NodeShareFanouts( pObj, vNodes );
     Vec_PtrFree( vNodes );
 }
 
@@ -68,7 +68,7 @@ void Seq_NtkSeqShareFanouts( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeSeqShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+void Seq_NodeShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 {
     Abc_Obj_t * pFanout;
     Abc_InitType_t Type;
@@ -90,19 +90,19 @@ void Abc_NodeSeqShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
     // 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
+        Seq_NodeShareOne( pNode, ABC_INIT_ZERO, vNodes );     // shares 0 and DC
+        Seq_NodeShareOne( pNode, ABC_INIT_ONE,  vNodes );     // shares 1 and DC
     }
     else if ( nLatches[ABC_INIT_ZERO] > 1 ) // 0-group
-        Abc_NodeSeqShareOne( pNode, ABC_INIT_ZERO, vNodes );     // shares 0 and DC
+        Seq_NodeShareOne( 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
+        Seq_NodeShareOne( pNode, ABC_INIT_ONE,  vNodes );     // shares 1 and DC
     else if ( nLatches[ABC_INIT_DC] > 1 ) // DC-group
     {
         if ( nLatches[ABC_INIT_ZERO] > 0 )
-            Abc_NodeSeqShareOne( pNode, ABC_INIT_ZERO, vNodes ); // shares 0 and DC
+            Seq_NodeShareOne( pNode, ABC_INIT_ZERO, vNodes ); // shares 0 and DC
         else 
-            Abc_NodeSeqShareOne( pNode, ABC_INIT_ONE,  vNodes ); // shares 1 and DC
+            Seq_NodeShareOne( pNode, ABC_INIT_ONE,  vNodes ); // shares 1 and DC
     }
 }
 
@@ -117,7 +117,7 @@ void Abc_NodeSeqShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNodes )
+void Seq_NodeShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNodes )
 {
     Vec_Ptr_t * vInits = Seq_NodeLats( pNode );
     Abc_Obj_t * pFanout, * pBuffer;
diff --git a/src/base/seq/seqUtil.c b/src/base/seq/seqUtil.c
index ce92bd33..3a80bd3c 100644
--- a/src/base/seq/seqUtil.c
+++ b/src/base/seq/seqUtil.c
@@ -6,7 +6,7 @@
 
   PackageName [Construction and manipulation of sequential AIGs.]
 
-  Synopsis    []
+  Synopsis    [Various utilities working with sequential AIGs.]
 
   Author      [Alan Mishchenko]