Version abc51127

9 files changed, 317 insertions, 90 deletions

diff --git a/src/base/seq/seq.h b/src/base/seq/seq.h
index 368f8afc..a644303f 100644
--- a/src/base/seq/seq.h
+++ b/src/base/seq/seq.h
@@ -44,7 +44,7 @@ typedef struct Abc_Seq_t_  Abc_Seq_t;
 ////////////////////////////////////////////////////////////////////////
 
 /*=== seqAigCore.c ===========================================================*/
-extern void            Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fInitial, int fVerbose );
+extern void            Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose );
 extern void            Seq_NtkSeqRetimeForward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose );
 extern void            Seq_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose );
 /*=== seqFpgaCore.c ===============================================================*/
@@ -52,7 +52,7 @@ extern Abc_Ntk_t *     Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int nMaxIters, in
 /*=== seqMapCore.c ===============================================================*/
 extern Abc_Ntk_t *     Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
 /*=== seqRetCore.c ===========================================================*/
-extern Abc_Ntk_t *     Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
+extern Abc_Ntk_t *     Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose );
 /*=== seqLatch.c ===============================================================*/
 extern void            Seq_NodeDupLats( Abc_Obj_t * pObjNew, Abc_Obj_t * pObj, int Edge );
 extern int             Seq_NodeCompareLats( Abc_Obj_t * pObj1, int Edge1, Abc_Obj_t * pObj2, int Edge2 );
@@ -63,10 +63,12 @@ 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 );
+extern bool            Abc_NtkSeqCheck( Abc_Ntk_t * pNtk ); 
 /*=== seqShare.c =============================================================*/
 extern void            Seq_NtkShareFanouts( Abc_Ntk_t * pNtk );
 extern void            Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk );
 extern void            Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds );
+extern void            Seq_NtkShareLatchesClean( Abc_Ntk_t * pNtk );
 /*=== seqUtil.c ==============================================================*/
 extern char *          Seq_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge );
 extern void            Seq_NtkLatchSetValues( Abc_Ntk_t * pNtk, Abc_InitType_t Init );
diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c
index d347d53e..5dca2e86 100644
--- a/src/base/seq/seqAigCore.c
+++ b/src/base/seq/seqAigCore.c
@@ -65,13 +65,14 @@ static void        Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches );
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fInitial, int fVerbose )
+void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
     int RetValue;
     if ( !fInitial )
         Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC );
     // get the retiming lags
+    p->nMaxIters = nMaxIters;
     Seq_AigRetimeDelayLags( pNtk, fVerbose );
     // implement this retiming
     RetValue = Seq_NtkImplementRetiming( pNtk, p->vLags, fVerbose );
@@ -490,31 +491,33 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t
         {
             Edge = 0;
             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 = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed
-            if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
-                assert( 0 );
-            // create the fanout of the AND gate
-            Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+            if ( Value == ABC_INIT_NONE )
+            {
+                // value is unknown, remove it from the table
+                RetEdge.iNode  = pFanout->Id;
+                RetEdge.iEdge  = Edge;
+                RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed
+                if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
+                    assert( 0 );
+                // create the fanout of the AND gate
+                Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+            }
         }
         if ( Abc_ObjFaninId1(pFanout) == pObj->Id )
         {
             Edge = 1;
             Value = Seq_NodeDeleteLast( pFanout, Edge );
-            if ( Value != ABC_INIT_NONE )
-                continue;
-            // value is unknown, remove it from the table
-            RetEdge.iNode  = pFanout->Id;
-            RetEdge.iEdge  = Edge;
-            RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed
-            if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
-                assert( 0 );
-            // create the fanout of the AND gate
-            Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+            if ( Value == ABC_INIT_NONE )
+            {
+                // value is unknown, remove it from the table
+                RetEdge.iNode  = pFanout->Id;
+                RetEdge.iEdge  = Edge;
+                RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed
+                if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
+                    assert( 0 );
+                // create the fanout of the AND gate
+                Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+            }
         }
     }
     // clean the label
diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c
index d293b946..d94e8e82 100644
--- a/src/base/seq/seqCreate.c
+++ b/src/base/seq/seqCreate.c
@@ -164,7 +164,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
     Seq_NtkLatchGetEqualFaninNum( pNtkNew );
 
     // copy EXDC and check correctness
-    if ( pNtkNew->pExdc )
+    if ( pNtk->pExdc )
         fprintf( stdout, "Warning: EXDC is not copied when converting to sequential AIG.\n" );
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkAigToSeq(): Network check has failed.\n" );
@@ -292,6 +292,8 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
         pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
         Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
     }
+    // clean the latch pointers
+    Seq_NtkShareLatchesClean( pNtk );
 
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkNew );
@@ -408,6 +410,73 @@ Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, Seq_Lat
     return pLatch;    
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Makes sure that every node in the table is in the network and vice versa.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkSeqCheck( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, nFanins;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+        {
+            if ( pObj != Abc_NtkConst1(pNtk) )
+            {
+                printf( "Abc_SeqCheck: The AIG has non-standard constant nodes.\n" );
+                return 0;
+            }
+            continue;
+        }
+        if ( nFanins == 1 )
+        {
+            printf( "Abc_SeqCheck: The AIG has single input nodes.\n" );
+            return 0;
+        }
+        if ( nFanins > 2 )
+        {
+            printf( "Abc_SeqCheck: The AIG has non-standard nodes.\n" );
+            return 0;
+        }
+    }
+    // check the correctness of the internal representation of the initial states
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+            continue;
+        if ( nFanins == 1 )
+        {
+            if ( Seq_NodeCountLats(pObj, 0) != Seq_ObjFaninL0(pObj) )
+            {
+                printf( "Abc_SeqCheck: Node %d has mismatch in the number of latches.\n", Abc_ObjName(pObj) );
+                return 0;
+            }
+        }
+        // look at both inputs
+        if ( Seq_NodeCountLats(pObj, 0) != Seq_ObjFaninL0(pObj) )
+        {
+            printf( "Abc_SeqCheck: The first fanin of node %d has mismatch in the number of latches.\n", Abc_ObjName(pObj) );
+            return 0;
+        }
+        if ( Seq_NodeCountLats(pObj, 1) != Seq_ObjFaninL1(pObj) )
+        {
+            printf( "Abc_SeqCheck: The second fanin of node %d has mismatch in the number of latches.\n", Abc_ObjName(pObj) );
+            return 0;
+        }
+    }
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqInt.h b/src/base/seq/seqInt.h
index 4503cef8..c0f3e907 100644
--- a/src/base/seq/seqInt.h
+++ b/src/base/seq/seqInt.h
@@ -195,7 +195,8 @@ static inline void           Seq_NodeRecycleLat( Abc_Obj_t * pObj, Seq_Lat_t * p
 static inline Seq_Lat_t *    Seq_NodeGetLatFirst( Abc_Obj_t * pObj, int Edge )               { return Seq_NodeGetRing(pObj, Edge);                      }
 static inline Seq_Lat_t *    Seq_NodeGetLatLast( Abc_Obj_t * pObj, int Edge )                { return Seq_LatPrev( Seq_NodeGetRing(pObj, Edge) );       }
 static inline Seq_Lat_t *    Seq_NodeGetLat( Abc_Obj_t * pObj, int Edge, int iLat )          { int c; Seq_Lat_t * pLat = Seq_NodeGetRing(pObj, Edge); for ( c = 0; c != iLat; c++ ) pLat = pLat->pNext; return pLat; }
-static inline int            Seq_NodeCountLats( Abc_Obj_t * pObj, int Edge )                 { int c; Seq_Lat_t * pLat, * pRing = Seq_NodeGetRing(pObj, Edge); if ( pRing == NULL ) return 0; for ( c = 0, pLat = pRing; !c || pLat != pRing; c++ )      pLat = pLat->pNext; return c; }
+static inline int            Seq_NodeCountLats( Abc_Obj_t * pObj, int Edge )                 { int c; Seq_Lat_t * pLat, * pRing = Seq_NodeGetRing(pObj, Edge); if ( pRing == NULL ) return 0; for ( c = 0, pLat = pRing; !c || pLat != pRing; c++ )  pLat = pLat->pNext; return c; }
+static inline void           Seq_NodeCleanLats( Abc_Obj_t * pObj, int Edge )                 { int c; Seq_Lat_t * pLat, * pRing = Seq_NodeGetRing(pObj, Edge); if ( pRing == NULL ) return  ; for ( c = 0, pLat = pRing; !c || pLat != pRing; c++ )  pLat->pLatch = NULL, pLat = pLat->pNext; return;  }
 
 // getting/setting initial states of the latches
 static inline Abc_InitType_t Seq_NodeGetInitOne( Abc_Obj_t * pObj, int Edge, int iLat )      { return Seq_LatInit( Seq_NodeGetLat(pObj, Edge, iLat) );  }
diff --git a/src/base/seq/seqLatch.c b/src/base/seq/seqLatch.c
index 8f861004..cb3e1e36 100644
--- a/src/base/seq/seqLatch.c
+++ b/src/base/seq/seqLatch.c
@@ -61,6 +61,7 @@ void Seq_NodeInsertFirst( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )
     }
     Seq_LatSetInit( pLat, Init );
     Seq_ObjAddFaninL( pObj, Edge, 1 );
+    assert( pLat->pLatch == NULL );
 }
 
 /**Function*************************************************************
diff --git a/src/base/seq/seqMapIter.c b/src/base/seq/seqMapIter.c
index 5a8b57bd..284fd27d 100644
--- a/src/base/seq/seqMapIter.c
+++ b/src/base/seq/seqMapIter.c
@@ -207,8 +207,8 @@ int Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
     char * pReason = "";
 
     // set l-values of all nodes to be minus infinity
-    Vec_IntFill( p->vLValues,  p->nSize, -ABC_INFINITY );
-    Vec_IntFill( p->vLValuesN, p->nSize, -ABC_INFINITY );
+    Vec_IntFill( p->vLValues,  p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
+    Vec_IntFill( p->vLValuesN, p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
     Vec_StrFill( p->vUses,     p->nSize, 0             );
 
     // set l-values of constants and PIs
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index c746f9a4..154f8dad 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -25,11 +25,12 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose );
 static Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
 static void        Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init );
-static Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk );
-
+static Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq );
+static Abc_Obj_t * Seq_EdgeReconstruct_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode );
+static Abc_Obj_t * Seq_EdgeReconstructPO( Abc_Obj_t * pNode );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -46,25 +47,31 @@ static Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pN
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
+Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose )
 {
     Abc_Seq_t * p;
-    Abc_Ntk_t * pNtkAig, * pNtkNew;
+    Abc_Ntk_t * pNtkSeq, * pNtkNew;
     int RetValue;
     assert( !Abc_NtkHasAig(pNtk) );
     // derive the isomorphic seq AIG
-    pNtkAig = Seq_NtkRetimeDerive( pNtk );
-    p = pNtkAig->pManFunc;
+    pNtkSeq = Seq_NtkRetimeDerive( pNtk, fVerbose );
+    p = pNtkSeq->pManFunc;
     p->nMaxIters = nMaxIters;
+
+    if ( !fInitial )
+        Seq_NtkLatchSetValues( pNtkSeq, ABC_INIT_DC );
     // find the best mapping and retiming 
-    Seq_NtkRetimeDelayLags( pNtk, pNtkAig, fVerbose );
+    Seq_NtkRetimeDelayLags( pNtk, pNtkSeq, fVerbose );
     // implement the retiming
-    RetValue = Seq_NtkImplementRetiming( pNtkAig, p->vLags, fVerbose );
+    RetValue = Seq_NtkImplementRetiming( pNtkSeq, p->vLags, fVerbose );
     if ( RetValue == 0 )
         printf( "Retiming completed but initial state computation has failed.\n" );
+
+//return pNtkSeq;
+
     // create the final mapped network
-    pNtkNew = Seq_NtkRetimeReconstruct( pNtk, pNtkAig );
-    Abc_NtkDelete( pNtkAig );
+    pNtkNew = Seq_NtkRetimeReconstruct( pNtk, pNtkSeq );
+    Abc_NtkDelete( pNtkSeq );
     return pNtkNew;
 }
 
@@ -79,12 +86,12 @@ Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Abc_Seq_t * p;
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pObj, * pFanin, * pFanout;
-    int i, k, RetValue;
+    int i, k, RetValue, fHasBdds;
     char * pSop;
 
     // make sure it is an AIG without self-feeding latches
@@ -93,35 +100,52 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
         printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
     assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
 
-    if ( Abc_NtkIsBddLogic(pNtk) )
+    // remove the dangling nodes
+    Abc_NtkCleanup( pNtk, fVerbose );
+
+    // transform logic functions from BDD to SOP
+    if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
         Abc_NtkBddToSop(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 );
     // clone the PIs/POs/latches
     Abc_NtkForEachPi( pNtk, pObj, i )
-        Abc_NtkDupObj(pNtkNew, pObj);
+        Abc_NtkDupObj( pNtkNew, pObj );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj );
+    // copy the names
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
     Abc_NtkForEachPo( pNtk, pObj, i )
-        Abc_NtkDupObj(pNtkNew, pObj);
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
 
     // create one AND for each logic node
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
+        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
+            continue;
         pObj->pCopy = Abc_NtkCreateNode( pNtkNew );
         pObj->pCopy->pCopy = pObj;
     }
+    // make latches point to the latch fanins
     Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        assert( !Abc_ObjIsLatch(Abc_ObjFanin0(pObj)) );
         pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
+    }
 
     // create internal AND nodes w/o strashing for each logic node (including constants)
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
+        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
+            continue;
         // get the SOP of the node
         if ( Abc_NtkHasMapping(pNtk) )
             pSop = Mio_GateReadSop(pObj->pData);
@@ -131,9 +155,9 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
         Abc_ObjAddFanin( pObj->pCopy, pFanin );
         Abc_ObjAddFanin( pObj->pCopy, pFanin );
     }
-
-    // connect the POs...
-
+    // connect the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
     
     // start the storage for initial states
     p = pNtkNew->pManFunc;
@@ -142,7 +166,15 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
     // add the sequential edges
     Abc_NtkForEachLatch( pNtk, pObj, i )
         Abc_ObjForEachFanout( pObj, pFanout, k )
-            Seq_NodeAddEdges_rec( Abc_ObjFanin0(pObj)->pCopy, pFanout->pCopy, Abc_LatchInit(pObj) );
+        {
+            if ( pObj->pCopy == Abc_ObjFanin0(pFanout->pCopy) )
+            {
+                Seq_NodeInsertFirst( pFanout->pCopy, 0, Abc_LatchInit(pObj) );
+                Seq_NodeInsertFirst( pFanout->pCopy, 1, Abc_LatchInit(pObj) );
+                continue;
+            }
+            Seq_NodeAddEdges_rec( pObj->pCopy, Abc_ObjFanin0(pFanout->pCopy), Abc_LatchInit(pObj) );
+        }
 
     // collect the nodes in the topological order
     p->vMapAnds   = Abc_NtkDfs( pNtk, 0 );
@@ -154,7 +186,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
         Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
         // collect the new fanins of this node
         Abc_ObjForEachFanin( pObj, pFanin, k )
-            Vec_VecPush( p->vMapCuts, i, pFanin->pCopy );
+            Vec_VecPush( p->vMapCuts, i, (void *)( (pFanin->pCopy->Id << 8) | Abc_ObjIsLatch(pFanin) ) );
         // collect the delay info
         if ( !Abc_NtkHasMapping(pNtk) )
         {
@@ -178,10 +210,14 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
 
     // set the cutset composed of latch drivers
 //    Abc_NtkAigCutsetCopy( pNtk );
-    Seq_NtkLatchGetEqualFaninNum( pNtkNew );
+//    Seq_NtkLatchGetEqualFaninNum( pNtkNew );
+
+    // convert the network back into BDDs if this is how it was
+    if ( fHasBdds )
+        Abc_NtkSopToBdd(pNtk);
 
     // copy EXDC and check correctness
-    if ( pNtkNew->pExdc )
+    if ( pNtk->pExdc )
         fprintf( stdout, "Warning: EXDC is not copied when converting to sequential AIG.\n" );
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Seq_NtkRetimeDerive(): Network check has failed.\n" );
@@ -202,6 +238,9 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
 void Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init )
 {
     Abc_Obj_t * pFanin;
+    assert( !Abc_ObjIsLatch(pNode) );
+    if ( !Abc_NodeIsAigAnd(pNode) )
+        return;
     // consider the first fanin
     pFanin = Abc_ObjFanin0(pNode);
     if ( pFanin->pCopy == NULL ) // internal node
@@ -275,53 +314,55 @@ Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char *
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
 {
-    Abc_Seq_t * p = pNtk->pManFunc;
-    Seq_Lat_t * pRing;
+    Abc_Seq_t * p = pNtkSeq->pManFunc;
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj, * pFaninNew, * pObjNew;
-    int i;
+    Abc_Obj_t * pObj, * pObjNew, * pFanin, * pFaninNew;
+    int i, k;
 
     assert( !Abc_NtkIsSeq(pNtkOld) );
-    assert( Abc_NtkIsSeq(pNtk) );
+    assert( Abc_NtkIsSeq(pNtkSeq) );
+
+    // transfer the pointers pNtkOld->pNtkSeq from pCopy to pNext
+    Abc_NtkForEachObj( pNtkOld, pObj, i )
+        pObj->pNext = pObj->pCopy;
 
     // start the final network
-    pNtkNew = Abc_NtkStartFrom( pNtk, pNtkOld->ntkType, pNtkOld->ntkFunc );
+    pNtkNew = Abc_NtkStartFrom( pNtkSeq, pNtkOld->ntkType, pNtkOld->ntkFunc );
 
-    // copy the internal nodes
-    Abc_NtkForEachNode( pNtk, pObj, i )
+    // copy the internal nodes of the old network into the new network
+    // transfer the pointers pNktOld->pNtkNew to pNtkSeq->pNtkNew
+    Abc_NtkForEachNode( pNtkOld, pObj, i )
+    {
+        if ( i == 0 ) continue;
         Abc_NtkDupObj( pNtkNew, pObj );
+        pObj->pNext->pCopy = pObj->pCopy;
+    }
 
     // share the latches
-    Seq_NtkShareLatches( pNtkNew, pNtk );
+    Seq_NtkShareLatches( pNtkNew, pNtkSeq );
 
     // connect the objects
-    Abc_AigForEachAnd( pNtk, pObj, i )
-    {
-        if ( pRing = Seq_NodeGetRing(pObj,0) )
-            pFaninNew = pRing->pLatch;
-        else
-            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
-        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    Abc_NtkForEachNode( pNtkOld, pObj, i )
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            pFaninNew = Seq_EdgeReconstruct_rec( pFanin->pNext, pObj->pNext );
+            assert( pFaninNew != NULL );
+            Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        }
 
-        if ( pRing = Seq_NodeGetRing(pObj,1) )
-            pFaninNew = pRing->pLatch;
-        else
-            pFaninNew = Abc_ObjFanin1(pObj)->pCopy;
-        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
-    }
     // connect the POs
-    Abc_NtkForEachPo( pNtk, pObj, i )
+    Abc_NtkForEachPo( pNtkOld, pObj, i )
     {
-        if ( pRing = Seq_NodeGetRing(pObj,0) )
-            pFaninNew = pRing->pLatch;
-        else
-            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
-        pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
-        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        pFaninNew = Seq_EdgeReconstructPO( pObj->pNext );
+        assert( pFaninNew != NULL );
+        Abc_ObjAddFanin( pObj->pNext->pCopy, pFaninNew );
     }
 
+    // clean the result of latch sharing
+    Seq_NtkShareLatchesClean( pNtkSeq );
+
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkNew );
     Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
@@ -330,13 +371,81 @@ Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk )
         Vec_PtrPush( pNtkNew->vCos, pObjNew );
     }
     // fix the problem with complemented and duplicated CO edges
-    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkSeqToLogicSop(): Network check has failed.\n" );
+        fprintf( stdout, "Seq_NtkRetimeReconstruct(): Network check has failed.\n" );
     return pNtkNew;
 
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the network after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_EdgeReconstruct_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode )
+{
+    Seq_Lat_t * pRing;
+    Abc_Obj_t * pFanin, * pRes = NULL;
+
+    if ( !Abc_NodeIsAigAnd(pNode) )
+        return NULL;
+
+    // consider the first fanin
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        pRes = Seq_EdgeReconstruct_rec( pGoal, pFanin );
+    else if ( pFanin == pGoal )
+    {
+        if ( pRing = Seq_NodeGetRing( pNode, 0 ) )
+            pRes = pRing->pLatch;
+        else
+            pRes = pFanin->pCopy;
+    }
+    if ( pRes != NULL )
+        return pRes;
+
+    // consider the second fanin
+    pFanin = Abc_ObjFanin1(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        pRes = Seq_EdgeReconstruct_rec( pGoal, pFanin );
+    else if ( pFanin == pGoal )
+    {
+        if ( pRing = Seq_NodeGetRing( pNode, 1 ) )
+            pRes = pRing->pLatch;
+        else
+            pRes = pFanin->pCopy;
+    }
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the network after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_EdgeReconstructPO( Abc_Obj_t * pNode )
+{
+    Seq_Lat_t * pRing;
+    assert( Abc_ObjIsPo(pNode) );
+    if ( pRing = Seq_NodeGetRing( pNode, 0 ) )
+        return pRing->pLatch;
+    else
+        return Abc_ObjFanin0(pNode)->pCopy;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqRetIter.c b/src/base/seq/seqRetIter.c
index 5c65e72e..1b8ac71c 100644
--- a/src/base/seq/seqRetIter.c
+++ b/src/base/seq/seqRetIter.c
@@ -76,7 +76,7 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
             }
         }
         // get the upper bound on the clock period
-        FiMax = Delta * (2 + Seq_NtkLevelMax(pNtk));
+        FiMax = Delta * 2 + Abc_NtkDelayTrace(pNtkOld);
         Delta /= 2;
     }
     else
@@ -95,14 +95,24 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
     RetValue = Seq_NtkMappingForPeriod( pNtk, FiBest, fVerbose );
     assert( RetValue );
 
-    // write the retiming lags for both phases of each node
+    // experiment by adding an epsilon to all LValues
+//    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+//        Seq_NodeSetLValueP( pNode, Seq_NodeGetLValueP(pNode) - p->fEpsilon );
+
+    // save the retiming lags
+    // mark the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+        pNode->fMarkA = 1;
+    // process the nodes
     Vec_StrFill( p->vLags,  p->nSize, 0 );
     Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
     {
         NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueP(pNode), FiBest );
-//        Seq_NodeSetLag( pNode, NodeLag );
         Seq_NodeRetimeSetLag_rec( pNode, NodeLag );
     }
+    // unmark the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+        pNode->fMarkA = 0;
 
     // print the result
     if ( fVerbose )
@@ -153,7 +163,7 @@ int Seq_NtkMappingForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
     char * pReason = "";
 
     // set l-values of all nodes to be minus infinity
-    Vec_IntFill( p->vLValues,  p->nSize, -ABC_INFINITY );
+    Vec_IntFill( p->vLValues,  p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
 
     // set l-values of constants and PIs
     pObj = Abc_NtkObj( pNtk, 0 );
@@ -268,11 +278,18 @@ int Seq_NtkNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, Vec_Ptr_t * vLeaves, Ve
 ***********************************************************************/
 void Seq_NodeRetimeSetLag_rec( Abc_Obj_t * pNode, char Lag )
 {
-    if ( pNode->pCopy )
+    Abc_Obj_t * pFanin;
+    if ( !Abc_NodeIsAigAnd(pNode) )
         return;
-    Seq_NodeRetimeSetLag_rec( Abc_ObjFanin0(pNode), Lag );
-    Seq_NodeRetimeSetLag_rec( Abc_ObjFanin1(pNode), Lag );
     Seq_NodeSetLag( pNode, Lag );
+    // consider the first fanin
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( pFanin->fMarkA == 0 ) // internal node
+        Seq_NodeRetimeSetLag_rec( pFanin, Lag );
+    // consider the second fanin
+    pFanin = Abc_ObjFanin1(pNode);
+    if ( pFanin->fMarkA == 0 ) // internal node
+        Seq_NodeRetimeSetLag_rec( pFanin, Lag );
 }
 
 
diff --git a/src/base/seq/seqShare.c b/src/base/seq/seqShare.c
index 5f5f1731..417dcc83 100644
--- a/src/base/seq/seqShare.c
+++ b/src/base/seq/seqShare.c
@@ -342,6 +342,31 @@ void Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t *
     Vec_PtrShrink( vMapAnds, nOldNodes );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Clean the latches after sharing them.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkShareLatchesClean( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        Seq_NodeCleanLats( pObj, 0 );
+        Seq_NodeCleanLats( pObj, 1 );
+    }
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_NodeCleanLats( pObj, 0 );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////