Version abc51126

46 files changed, 3497 insertions, 1214 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 1985f4c8..1904a0b6 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -104,12 +104,12 @@ typedef enum {
 #define bool int
 #endif
 
-typedef struct Abc_Obj_t_     Abc_Obj_t;
-typedef struct Abc_Ntk_t_     Abc_Ntk_t;
-typedef struct Abc_Aig_t_     Abc_Aig_t;
-typedef struct Abc_ManTime_t_ Abc_ManTime_t;
-typedef struct Abc_ManCut_t_  Abc_ManCut_t;
-typedef struct Abc_Time_t_    Abc_Time_t;
+typedef struct Abc_Obj_t_       Abc_Obj_t;
+typedef struct Abc_Ntk_t_       Abc_Ntk_t;
+typedef struct Abc_Aig_t_       Abc_Aig_t;
+typedef struct Abc_ManTime_t_   Abc_ManTime_t;
+typedef struct Abc_ManCut_t_    Abc_ManCut_t;
+typedef struct Abc_Time_t_      Abc_Time_t;
 
 struct Abc_Time_t_
 {
@@ -122,19 +122,21 @@ struct Abc_Obj_t_ // 12 words
 {
     // high-level information
     Abc_Ntk_t *      pNtk;          // the host network
-    unsigned         Type    :  4;  // the object type
-    unsigned         fExor   :  1;  // marks AIG node that is a root of EXOR
-    unsigned         Id      : 27;  // the ID of the object
+    int              Id;            // the object ID
     // internal information
+    unsigned         Type    :  3;  // the object type
     unsigned         fMarkA  :  1;  // the multipurpose mark
     unsigned         fMarkB  :  1;  // the multipurpose mark
     unsigned         fMarkC  :  1;  // the multipurpose mark
     unsigned         fPhase  :  1;  // the flag to mark the phase of equivalent node
-    unsigned         TravId  : 12;  // the traversal ID
-    unsigned         Level   : 16;  // the level of the node
+    unsigned         fExor   :  1;  // marks AIG node that is a root of EXOR
+    unsigned         fCompl0 :  1;  // complemented attribute of the first fanin in the AIG
+    unsigned         fCompl1 :  1;  // complemented attribute of the second fanin in the AIG 
+    unsigned         TravId  : 10;  // the traversal ID (if changed, update Abc_NtkIncrementTravId)
+    unsigned         Level   : 12;  // the level of the node
     // connectivity
-    Vec_Fan_t        vFanins;       // the array of fanins
-    Vec_Fan_t        vFanouts;      // the array of fanouts
+    Vec_Int_t        vFanins;       // the array of fanins
+    Vec_Int_t        vFanouts;      // the array of fanouts
     // miscellaneous
     void *           pData;         // the network specific data (SOP, BDD, gate, equiv class, etc)
     Abc_Obj_t *      pNext;         // the next pointer in the hash table
@@ -268,8 +270,8 @@ static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i )       { assert( i
 static inline unsigned    Abc_ObjType( Abc_Obj_t * pObj )            { return pObj->Type;               }
 static inline unsigned    Abc_ObjId( Abc_Obj_t * pObj )              { return pObj->Id;                 }
 static inline int         Abc_ObjTravId( Abc_Obj_t * pObj )          { return pObj->TravId;             }
-static inline Vec_Fan_t * Abc_ObjFaninVec( Abc_Obj_t * pObj )        { return &pObj->vFanins;           }
-static inline Vec_Fan_t * Abc_ObjFanoutVec( Abc_Obj_t * pObj )       { return &pObj->vFanouts;          }
+static inline Vec_Int_t * Abc_ObjFaninVec( Abc_Obj_t * pObj )        { return &pObj->vFanins;           }
+static inline Vec_Int_t * Abc_ObjFanoutVec( Abc_Obj_t * pObj )       { return &pObj->vFanouts;          }
 static inline Abc_Obj_t * Abc_ObjCopy( Abc_Obj_t * pObj )            { return pObj->pCopy;              }
 static inline Abc_Ntk_t * Abc_ObjNtk( Abc_Obj_t * pObj )             { return pObj->pNtk;               }
 static inline void *      Abc_ObjData( Abc_Obj_t * pObj )            { return pObj->pData;              }
@@ -298,28 +300,28 @@ static inline bool        Abc_ObjIsCio( Abc_Obj_t * pObj )           { return pO
 // working with fanin/fanout edges
 static inline int         Abc_ObjFaninNum( Abc_Obj_t * pObj )        { return pObj->vFanins.nSize;      }
 static inline int         Abc_ObjFanoutNum( Abc_Obj_t * pObj )       { return pObj->vFanouts.nSize;     }
-static inline int         Abc_ObjFaninId( Abc_Obj_t * pObj, int i)   { return pObj->vFanins.pArray[i].iFan; }
-static inline int         Abc_ObjFaninId0( Abc_Obj_t * pObj )        { return pObj->vFanins.pArray[0].iFan; }
-static inline int         Abc_ObjFaninId1( Abc_Obj_t * pObj )        { return pObj->vFanins.pArray[1].iFan; }
-static inline int         Abc_ObjFanoutEdgeNum( Abc_Obj_t * pObj, Abc_Obj_t * pFanout )  { assert( Abc_NtkHasAig(pObj->pNtk) );  if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id ) return 0; if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id ) return 1; assert( 0 ); return -1;  }
-static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i )   { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ];   }
-static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj )         { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ];   }
-static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i )    { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan  ];   }
-static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj )          { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan  ];   }
-static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj )          { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan  ];   }
-static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )       { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj)  : pObj);  }
-static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj )      { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj);  }
-static inline bool        Abc_ObjFaninC( Abc_Obj_t * pObj, int i )   { return pObj->vFanins.pArray[i].fCompl;                               }
-static inline bool        Abc_ObjFaninC0( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[0].fCompl;                               }
-static inline bool        Abc_ObjFaninC1( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[1].fCompl;                               }
+static inline int         Abc_ObjFaninId( Abc_Obj_t * pObj, int i)   { return pObj->vFanins.pArray[i]; }
+static inline int         Abc_ObjFaninId0( Abc_Obj_t * pObj )        { return pObj->vFanins.pArray[0]; }
+static inline int         Abc_ObjFaninId1( Abc_Obj_t * pObj )        { return pObj->vFanins.pArray[1]; }
+static inline int         Abc_ObjFanoutEdgeNum( Abc_Obj_t * pObj, Abc_Obj_t * pFanout )  { assert( Abc_NtkHasAig(pObj->pNtk) );  if ( Abc_ObjFaninId0(pFanout) == pObj->Id ) return 0; if ( Abc_ObjFaninId1(pFanout) == pObj->Id ) return 1; assert( 0 ); return -1;  }
+static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i )   { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i] ];  }
+static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj )         { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0] ];  }
+static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i )    { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i] ];   }
+static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj )          { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0] ];   }
+static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj )          { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1] ];   }
+static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )       { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj)  : pObj); }
+static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj )      { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj); }
+static inline bool        Abc_ObjFaninC0( Abc_Obj_t * pObj )         { return pObj->fCompl0;                                                }
+static inline bool        Abc_ObjFaninC1( Abc_Obj_t * pObj )         { return pObj->fCompl1;                                                }
+static inline bool        Abc_ObjFaninC( Abc_Obj_t * pObj, int i )   { assert( i >=0 && i < 2 ); return i? pObj->fCompl1 : pObj->fCompl0;   }
+static inline void        Abc_ObjSetFaninC( Abc_Obj_t * pObj, int i ){ assert( i >=0 && i < 2 ); if ( i ) pObj->fCompl1 = 1; else pObj->fCompl0 = 1; }
+static inline void        Abc_ObjXorFaninC( Abc_Obj_t * pObj, int i ){ assert( i >=0 && i < 2 ); if ( i ) pObj->fCompl1^= 1; else pObj->fCompl0^= 1; }
 static inline Abc_Obj_t * Abc_ObjChild( Abc_Obj_t * pObj, int i )    { return Abc_ObjNotCond( Abc_ObjFanin(pObj,i), Abc_ObjFaninC(pObj,i) );}
 static inline Abc_Obj_t * Abc_ObjChild0( Abc_Obj_t * pObj )          { return Abc_ObjNotCond( Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );  }
 static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj )          { return Abc_ObjNotCond( Abc_ObjFanin1(pObj), Abc_ObjFaninC1(pObj) );  }
-static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) );}
-static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );  }
-static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) );  }
-static inline void        Abc_ObjSetFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl = 1;                               }
-static inline void        Abc_ObjXorFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl ^= 1;                              }
+static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) );  }
+static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );    }
+static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) );    }
 
 // checking the node type
 static inline bool        Abc_NodeIsAigAnd( Abc_Obj_t * pNode )      { assert(Abc_NtkHasAig(pNode->pNtk));           return Abc_ObjFaninNum(pNode) == 2;                         }
@@ -473,6 +475,7 @@ extern void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
 /*=== abcLatch.c ==========================================================*/
 extern bool               Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
 extern int                Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk );
 /*=== abcMap.c ==========================================================*/
 extern int                Abc_NtkUnmap( Abc_Ntk_t * pNtk );
 /*=== abcMiter.c ==========================================================*/
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 9f5ebb64..53ad88c2 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -394,13 +394,15 @@ Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
 ***********************************************************************/
 void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis )
 {
-    Abc_Obj_t * pAnd, ** ppPlace;
+    Abc_Obj_t * pAnd, * pAnd0, * pAnd1, ** ppPlace;
     unsigned Key;
     assert( !Abc_ObjIsComplement(pThis) );
     assert( Abc_ObjIsNode(pThis) );
     assert( Abc_ObjFaninNum(pThis) == 2 );
     assert( pMan->pNtkAig == pThis->pNtk );
     // get the hash key for these two nodes
+    pAnd0 = Abc_ObjRegular( Abc_ObjChild0(pThis) );
+    pAnd1 = Abc_ObjRegular( Abc_ObjChild1(pThis) );
     Key = Abc_HashKey2( Abc_ObjChild0(pThis), Abc_ObjChild1(pThis), pMan->nBins );
     // find the matching node in the table
     ppPlace = pMan->pBins + Key;
@@ -479,7 +481,7 @@ void Abc_AigRehash( Abc_Aig_t * pMan )
 {
     Abc_Obj_t ** pBinsNew;
     Abc_Obj_t * pEnt, * pEnt2;
-    Abc_Fan_t * pArray;
+    int * pArray;
     unsigned Key;
     int Counter, Temp, i;
 
@@ -493,14 +495,14 @@ void Abc_AigRehash( Abc_Aig_t * pMan )
         {
             // swap the fanins if needed
             pArray = pEnt->vFanins.pArray;
-            if ( pArray[0].iFan > pArray[1].iFan )
+            if ( pArray[0] > pArray[1] )
             {
-                Temp = pArray[0].iFan;
-                pArray[0].iFan = pArray[1].iFan;
-                pArray[1].iFan = Temp;
-                Temp = pArray[0].fCompl;
-                pArray[0].fCompl = pArray[1].fCompl;
-                pArray[1].fCompl = Temp;
+                Temp = pArray[0];
+                pArray[0] = pArray[1];
+                pArray[1] = Temp;
+                Temp = pEnt->fCompl0;
+                pEnt->fCompl0 = pEnt->fCompl1;
+                pEnt->fCompl1 = Temp;
             }
             // rehash the node
             Key = Abc_HashKey2( Abc_ObjChild0(pEnt), Abc_ObjChild1(pEnt), pMan->nBins );
@@ -660,7 +662,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, int fUpdateLevel )
             continue;
         }
         // find the old node as a fanin of this fanout
-        iFanin = Vec_FanFindEntry( &pFanout->vFanins, pOld->Id );
+        iFanin = Vec_IntFind( &pFanout->vFanins, pOld->Id );
         assert( iFanin == 0 || iFanin == 1 );
         // get the new fanin
         pFanin1 = Abc_ObjNotCond( pNew, Abc_ObjFaninC(pFanout, iFanin) );
@@ -1009,7 +1011,7 @@ bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode )
     int i, iFanin;
     Abc_ObjForEachFanout( pNode, pFanout, i )
     {
-        iFanin = Vec_FanFindEntry( &pFanout->vFanins, pNode->Id );
+        iFanin = Vec_IntFind( &pFanout->vFanins, pNode->Id );
         assert( iFanin >= 0 );
         if ( Abc_ObjFaninC( pFanout, iFanin ) )
             return 1;
@@ -1038,7 +1040,7 @@ bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode )
     {
         if ( !Abc_NodeIsTravIdCurrent(pFanout) )
             continue;
-        iFanin = Vec_FanFindEntry( &pFanout->vFanins, pNode->Id );
+        iFanin = Vec_IntFind( &pFanout->vFanins, pNode->Id );
         assert( iFanin >= 0 );
         if ( Abc_ObjFaninC( pFanout, iFanin ) )
             return 1;
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 548a2294..0211e9f8 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -417,7 +417,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
     // go through the fanins of the object and make sure fanins have this object as a fanout
     Abc_ObjForEachFanin( pObj, pFanin, i )
     {
-        if ( Vec_FanFindEntry( &pFanin->vFanouts, pObj->Id ) == -1 )
+        if ( Vec_IntFind( &pFanin->vFanouts, pObj->Id ) == -1 )
         {
             fprintf( stdout, "NodeCheck: Object \"%s\" has fanin ", Abc_ObjName(pObj) );
             fprintf( stdout, "\"%s\" but the fanin does not have it as a fanout.\n", Abc_ObjName(pFanin) );
@@ -427,7 +427,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
     // go through the fanouts of the object and make sure fanouts have this object as a fanin
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
-        if ( Vec_FanFindEntry( &pFanout->vFanins, pObj->Id ) == -1 )
+        if ( Vec_IntFind( &pFanout->vFanins, pObj->Id ) == -1 )
         {
             fprintf( stdout, "NodeCheck: Object \"%s\" has fanout ", Abc_ObjName(pObj) );
             fprintf( stdout, "\"%s\" but the fanout does not have it as a fanin.\n", Abc_ObjName(pFanout) );
@@ -441,7 +441,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
     // make sure fanins are not duplicated
     for ( i = 0; i < pObj->vFanins.nSize; i++ )
         for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
-            if ( pObj->vFanins.pArray[k].iFan == pObj->vFanins.pArray[i].iFan )
+            if ( pObj->vFanins.pArray[k] == pObj->vFanins.pArray[i] )
             {
                 printf( "Warning: Node %s has", Abc_ObjName(pObj) );
                 printf( " duplicated fanin %s.\n", Abc_ObjName(Abc_ObjFanin(pObj,k)) );
@@ -454,7 +454,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
     // make sure fanouts are not duplicated
     for ( i = 0; i < pObj->vFanouts.nSize; i++ )
         for ( k = i + 1; k < pObj->vFanouts.nSize; k++ )
-            if ( pObj->vFanouts.pArray[k].iFan == pObj->vFanouts.pArray[i].iFan )
+            if ( pObj->vFanouts.pArray[k] == pObj->vFanouts.pArray[i] )
             {
                 printf( "Warning: Node %s has", Abc_ObjName(pObj) );
                 printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) );
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index dbd3e5fa..158edf65 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -221,6 +221,7 @@ bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode, * pFanin;
     int i, k;
+    assert( !Abc_NtkIsSeq(pNtk) );
     // set the traversal ID
     Abc_NtkIncrementTravId( pNtk );
     // mark the CIs
@@ -229,11 +230,16 @@ bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk )
     // go through the nodes
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
+        // check the fanins of the node
         Abc_ObjForEachFanin( pNode, pFanin, k )
-        {
             if ( !Abc_NodeIsTravIdCurrent(pFanin) )
                 return 0;
-        }
+        // check the choices of the node
+        if ( Abc_NtkIsStrash(pNtk) && Abc_NodeIsAigChoice(pNode) )
+            for ( pFanin = pNode->pData; pFanin; pFanin = pFanin->pData )
+                if ( !Abc_NodeIsTravIdCurrent(pFanin) )
+                    return 0;
+        // mark the node as visited
         Abc_NodeSetTravIdCurrent( pNode );
     }
     return 1;
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 983d41e4..59dff196 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -25,8 +25,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define ABC_LARGE_ID   ((1<<24)-1)   // should correspond to value in "vecFan.h"
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -48,10 +46,8 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     assert( !Abc_ObjIsComplement(pObj) );
     assert( pObj->pNtk == pFaninR->pNtk );
     assert( pObj->Id >= 0 && pFaninR->Id >= 0 );
-    assert( pObj->Id    < ABC_LARGE_ID );  // created but forgot to add it to the network?
-    assert( pFaninR->Id < ABC_LARGE_ID );  // created but forgot to add it to the network?
-    Vec_FanPush( pObj->pNtk->pMmStep, &pObj->vFanins,     Vec_Int2Fan(pFaninR->Id) );
-    Vec_FanPush( pObj->pNtk->pMmStep, &pFaninR->vFanouts, Vec_Int2Fan(pObj->Id)    );
+    Vec_IntPushMem( pObj->pNtk->pMmStep, &pObj->vFanins,     pFaninR->Id );
+    Vec_IntPushMem( pObj->pNtk->pMmStep, &pFaninR->vFanouts, pObj->Id    );
     if ( Abc_ObjIsComplement(pFanin) )
         Abc_ObjSetFaninC( pObj, Abc_ObjFaninNum(pObj)-1 );
 }
@@ -74,14 +70,12 @@ void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     assert( !Abc_ObjIsComplement(pFanin) );
     assert( pObj->pNtk == pFanin->pNtk );
     assert( pObj->Id >= 0 && pFanin->Id >= 0 );
-    assert( pObj->Id   < ABC_LARGE_ID );  // created but forgot to add it to the network?
-    assert( pFanin->Id < ABC_LARGE_ID );  // created but forgot to add it to the network?
-    if ( !Vec_FanDeleteEntry( &pObj->vFanins, pFanin->Id ) )
+    if ( !Vec_IntRemove( &pObj->vFanins, pFanin->Id ) )
     {
         printf( "The obj %d is not found among the fanins of obj %d ...\n", pFanin->Id, pObj->Id );
         return;
     }
-    if ( !Vec_FanDeleteEntry( &pFanin->vFanouts, pObj->Id ) )
+    if ( !Vec_IntRemove( &pFanin->vFanouts, pObj->Id ) )
     {
         printf( "The obj %d is not found among the fanouts of obj %d ...\n", pObj->Id, pFanin->Id );
         return;
@@ -102,16 +96,19 @@ void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
 ***********************************************************************/
 void Abc_ObjRemoveFanins( Abc_Obj_t * pObj )
 {
-    Vec_Fan_t * vFaninsOld;
+    Vec_Int_t * vFaninsOld;
     Abc_Obj_t * pFanin;
     int k;
     // remove old fanins
     vFaninsOld = &pObj->vFanins;
     for ( k = vFaninsOld->nSize - 1; k >= 0; k-- )
     {
-        pFanin = Abc_NtkObj( pObj->pNtk, vFaninsOld->pArray[k].iFan );
+        pFanin = Abc_NtkObj( pObj->pNtk, vFaninsOld->pArray[k] );
         Abc_ObjDeleteFanin( pObj, pFanin );
     }
+    pObj->fCompl0 = 0;
+    pObj->fCompl1 = 0;
+    assert( vFaninsOld->nSize == 0 );
 }
 
 /**Function*************************************************************
@@ -131,7 +128,7 @@ void Abc_ObjRemoveFanins( Abc_Obj_t * pObj )
 void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew )
 {
     Abc_Obj_t * pFaninNewR = Abc_ObjRegular(pFaninNew);
-    int iFanin, fCompl, nLats;
+    int iFanin, nLats;//, fCompl;
     assert( !Abc_ObjIsComplement(pObj) );
     assert( !Abc_ObjIsComplement(pFaninOld) );
     assert( pFaninOld != pFaninNewR );
@@ -139,29 +136,33 @@ void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFa
 //    assert( pObj != pFaninNewR );
     assert( pObj->pNtk == pFaninOld->pNtk );
     assert( pObj->pNtk == pFaninNewR->pNtk );
-    if ( (iFanin = Vec_FanFindEntry( &pObj->vFanins, pFaninOld->Id )) == -1 )
+    if ( (iFanin = Vec_IntFind( &pObj->vFanins, pFaninOld->Id )) == -1 )
     {
         printf( "Node %s is not among", Abc_ObjName(pFaninOld) );
         printf( " the fanins of node %s...\n", Abc_ObjName(pObj) );
         return;
     }
+
     // remember the attributes of the old fanin
-    fCompl = Abc_ObjFaninC(pObj, iFanin);
+//    fCompl = Abc_ObjFaninC(pObj, iFanin);
     // replace the old fanin entry by the new fanin entry (removes attributes)
-    Vec_FanWriteEntry( &pObj->vFanins, iFanin, Vec_Int2Fan(pFaninNewR->Id) );
+    Vec_IntWriteEntry( &pObj->vFanins, iFanin, pFaninNewR->Id );
     // set the attributes of the new fanin
-    if ( fCompl ^ Abc_ObjIsComplement(pFaninNew) )
-        Abc_ObjSetFaninC( pObj, iFanin );
+//    if ( fCompl ^ Abc_ObjIsComplement(pFaninNew) )
+//        Abc_ObjSetFaninC( pObj, iFanin );
+    if ( Abc_ObjIsComplement(pFaninNew) )
+        Abc_ObjXorFaninC( pObj, iFanin );
+
     if ( Abc_NtkIsSeq(pObj->pNtk) && (nLats = Seq_ObjFaninL(pObj, iFanin)) )
         Seq_ObjSetFaninL( pObj, iFanin, nLats );
     // update the fanout of the fanin
-    if ( !Vec_FanDeleteEntry( &pFaninOld->vFanouts, pObj->Id ) )
+    if ( !Vec_IntRemove( &pFaninOld->vFanouts, pObj->Id ) )
     {
         printf( "Node %s is not among", Abc_ObjName(pObj) );
         printf( " the fanouts of its old fanin %s...\n", Abc_ObjName(pFaninOld) );
 //        return;
     }
-    Vec_FanPush( pObj->pNtk->pMmStep, &pFaninNewR->vFanouts, Vec_Int2Fan(pObj->Id) );
+    Vec_IntPushMem( pObj->pNtk->pMmStep, &pFaninNewR->vFanouts, pObj->Id );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index a31f0b16..85dd9d8e 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -89,7 +89,38 @@ int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk )
     int i, Counter;
     Counter = 0;
     Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+//        if ( Abc_NtkLatchIsSelfFeed(pLatch) && Abc_ObjFanoutNum(pLatch) > 1 )
+//            printf( "Fanouts = %d.\n", Abc_ObjFanoutNum(pLatch) );
         Counter += Abc_NtkLatchIsSelfFeed( pLatch );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces self-feeding latches by latches with constant inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch;
+    int i, Counter;
+    Counter = 0;
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        if ( Abc_NtkLatchIsSelfFeed( pLatch ) )
+        {
+            Abc_ObjPatchFanin( pLatch, Abc_ObjFanin0(pLatch), Abc_NtkConst1(pNtk) );
+            Counter++;
+        }
+    }
     return Counter;
 }
 
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 9d649f6f..39184e01 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -326,6 +326,10 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
                     Seq_NodeDupLats( pObj->pCopy, pObj, k );
             }
         }
+        // relink the choice nodes
+        Abc_AigForEachAnd( pNtk, pObj, i )
+            if ( pObj->pData )
+                pObj->pCopy->pData = ((Abc_Obj_t *)pObj->pData)->pCopy;
     }
     else
     {
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index b144066f..481b069f 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -47,9 +47,9 @@ Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
     Abc_Obj_t * pObj;
     pObj = (Abc_Obj_t *)Extra_MmFixedEntryFetch( pNtk->pMmObj );
     memset( pObj, 0, sizeof(Abc_Obj_t) );
-    pObj->Id   = -1;
     pObj->pNtk = pNtk;
     pObj->Type = Type;
+    pObj->Id   = -1;
     return pObj;
 }
 
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 5d7b4302..8e1615d7 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -49,7 +49,7 @@ void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
     int i;
-    if ( pNtk->nTravIds == (1<<12)-1 )
+    if ( pNtk->nTravIds == (1<<10)-1 )
     {
         pNtk->nTravIds = 0;
         Abc_NtkForEachObj( pNtk, pObj, i )
@@ -260,7 +260,7 @@ int Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i, Counter;
-    if ( !Abc_NtkIsStrash(pNtk) )
+    if ( !Abc_NtkHasAig(pNtk) )
         return 0;
     Counter = 0;
     Abc_NtkForEachNode( pNtk, pNode, i )
@@ -966,7 +966,7 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk )
         Vec_PtrPush( vObjsNew, pNode );
     }
     // finally, internal nodes in the DFS order
-    vNodes = Abc_NtkDfs( pNtk, 1 );
+    vNodes = Abc_AigDfs( pNtk, 1, 0 );
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
         if ( pNode == pConst1 )
@@ -981,9 +981,9 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk )
     Abc_NtkForEachObj( pNtk, pNode, i )
     {
         Abc_ObjForEachFanin( pNode, pTemp, k )
-            pNode->vFanins.pArray[k].iFan = pTemp->Id;
+            pNode->vFanins.pArray[k] = pTemp->Id;
         Abc_ObjForEachFanout( pNode, pTemp, k )
-            pNode->vFanouts.pArray[k].iFan = pTemp->Id;
+            pNode->vFanouts.pArray[k] = pTemp->Id;
     }
 
     // replace the array of objs
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f7e7f763..0b24b3ff 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4741,7 +4741,7 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c, nLoops;
+    int c;//, nLoops;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -4778,11 +4778,11 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( nLoops = Abc_NtkCountSelfFeedLatches(pNtk) )
-    {
-        fprintf( pErr, "Cannot create sequential AIG because the network contains %d self-feeding latches.\n", nLoops );
-        return 0;
-    }
+//    if ( nLoops = Abc_NtkCountSelfFeedLatches(pNtk) )
+//    {
+//        fprintf( pErr, "Cannot create sequential AIG because the network contains %d self-feeding latches.\n", nLoops );
+//        return 0;
+//    }
 
     // get the new network
     pNtkRes = Abc_NtkAigToSeq( pNtk );
@@ -4854,8 +4854,8 @@ int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // share the latches on the fanout edges
-    if ( fShare )
-        Seq_NtkShareFanouts(pNtk);
+//    if ( fShare )
+//        Seq_NtkShareFanouts(pNtk);
 
     // get the new network
     pNtkRes = Abc_NtkSeqToLogicSop( pNtk );
@@ -4983,7 +4983,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c;
+    int c, nMaxIters;
     int fVerbose;
 
     pNtk = Abc_FrameReadNet(pAbc);
@@ -4991,12 +4991,24 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fVerbose = 0;
+    nMaxIters = 15;
+    fVerbose  =  0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "Ivh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'I':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nMaxIters = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nMaxIters < 0 ) 
+                goto usage;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -5020,7 +5032,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Seq_NtkFpgaMapRetime( pNtk, fVerbose );
+    pNtkRes = Seq_NtkFpgaMapRetime( pNtk, nMaxIters, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
@@ -5031,10 +5043,11 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: sfpga [-vh]\n" );
-    fprintf( pErr, "\t        performs integrated sequential FPGA mapping\n" );
-    fprintf( pErr, "\t-v    : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-h    : print the command usage\n");
+    fprintf( pErr, "usage: sfpga [-I num] [-vh]\n" );
+    fprintf( pErr, "\t         performs integrated sequential FPGA mapping\n" );
+    fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
 
@@ -5053,21 +5066,32 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c;
+    int c, nMaxIters;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkMapSeq( Abc_Ntk_t * pNtk, int fVerbose );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fVerbose = 1;
+    nMaxIters = 15;
+    fVerbose  =  1;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "Ivh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'I':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nMaxIters = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nMaxIters < 0 ) 
+                goto usage;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -5089,17 +5113,14 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Sequential standard cell mapping works only for sequential AIG (run \"seq\").\n" );
         return 1;
     }
-
-    printf( "This command is not yet implemented.\n" );
-    return 0;
-
-
+//    printf( "This command is not yet implemented.\n" );
+//    return 0;
 
     // get the new network
-    pNtkRes = Abc_NtkMapSeq( pNtk, fVerbose );
+    pNtkRes = Seq_MapRetime( pNtk, nMaxIters, fVerbose );
     if ( pNtkRes == NULL )
     {
-        fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
+        fprintf( pErr, "Sequential standard-cell mapping has failed.\n" );
         return 1;
     }
     // replace the current network
@@ -5107,10 +5128,11 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: smap [-vh]\n" );
-    fprintf( pErr, "\t        performs integrated sequential standard-cell mapping" );
-    fprintf( pErr, "\t-v    : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-h    : print the command usage\n");
+    fprintf( pErr, "usage: smap [-I num] [-vh]\n" );
+    fprintf( pErr, "\t         performs integrated sequential standard-cell mapping" );
+    fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
 
diff --git a/src/base/abci/abcAttach.c b/src/base/abci/abcAttach.c
index d97d50c5..78573718 100644
--- a/src/base/abci/abcAttach.c
+++ b/src/base/abci/abcAttach.c
@@ -187,7 +187,7 @@ int Abc_NodeAttach( Abc_Obj_t * pNode, Mio_Gate_t ** ppGates, unsigned ** puTrut
     Abc_ObjForEachFanin( pNode, pFanin, i )
         pTempInts[i] = pFanin->Id;
     for ( i = 0; i < nFanins; i++ )
-        pNode->vFanins.pArray[Perm[i]].iFan = pTempInts[i];
+        pNode->vFanins.pArray[Perm[i]] = pTempInts[i];
     // set the gate
     pNode->pCopy = (Abc_Obj_t *)pGate;
     return 1;
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index f285495c..3e34602d 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -185,12 +185,14 @@ void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p )
 Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
 {
     Cut_Man_t *  p;
-    Abc_Obj_t * pObj;
+    Abc_Obj_t * pObj, * pNode;
     int i, nIters, fStatus;
+    Vec_Int_t * vChoices;
     int clk = clock();
 
     assert( Abc_NtkIsSeq(pNtk) );
     assert( pParams->fSeq );
+//    assert( Abc_NtkIsDfsOrdered(pNtk) );
 
     // start the manager
     pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
@@ -202,7 +204,10 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     if ( Abc_ObjFanoutNum(pObj) > 0 )
         Cut_NodeSetTriv( p, pObj->Id );
     Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+//printf( "Setting trivial cut %d.\n", pObj->Id );
         Cut_NodeSetTriv( p, pObj->Id );
+    }
     // label the cutset nodes and set their number in the array
     // assign the elementary cuts to the cutset nodes
     Abc_SeqForEachCutsetNode( pNtk, pObj, i )
@@ -211,27 +216,40 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
         pObj->fMarkC = 1;
         pObj->pCopy = (Abc_Obj_t *)i;
         Cut_NodeSetTriv( p, pObj->Id );
+//printf( "Setting trivial cut %d.\n", pObj->Id );
     }
 
     // process the nodes
+    vChoices = Vec_IntAlloc( 100 );
     for ( nIters = 0; nIters < 10; nIters++ )
     {
 //printf( "ITERATION %d:\n", nIters );
         // compute the cuts for the internal nodes
         Abc_AigForEachAnd( pNtk, pObj, i )
+        {
             Abc_NodeGetCutsSeq( p, pObj, nIters==0 );
+            // add cuts due to choices
+            if ( Abc_NodeIsAigChoice(pObj) )
+            {
+                Vec_IntClear( vChoices );
+                for ( pNode = pObj; pNode; pNode = pNode->pData )
+                    Vec_IntPush( vChoices, pNode->Id );
+                Cut_NodeUnionCutsSeq( p, vChoices, (pObj->fMarkC ? (int)pObj->pCopy : -1), nIters==0 );
+            }
+        }
         // merge the new cuts with the old cuts
         Abc_NtkForEachPi( pNtk, pObj, i )
             Cut_NodeNewMergeWithOld( p, pObj->Id );
         Abc_AigForEachAnd( pNtk, pObj, i )
             Cut_NodeNewMergeWithOld( p, pObj->Id );
-        // for the cutset, merge temp with new
+        // for the cutset, transfer temp cuts to new cuts
         fStatus = 0;
         Abc_SeqForEachCutsetNode( pNtk, pObj, i )
             fStatus |= Cut_NodeTempTransferToNew( p, pObj->Id, i );
         if ( fStatus == 0 )
             break;
     }
+    Vec_IntFree( vChoices );
 
     // if the status is not finished, transfer new to old for the cutset
     Abc_SeqForEachCutsetNode( pNtk, pObj, i )
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index ac0d06be..bfc992ef 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -292,6 +292,7 @@ Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     }
     Extra_ProgressBarStop( pProgress );
+    Abc_NtkReassignIds( pNtkNew );
     return pNtkNew;
 }
 
@@ -495,6 +496,7 @@ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
     Abc_NtkFraigTrustOne( pNtk, pNtkNew );
     Abc_NtkFinalize( pNtk, pNtkNew );
+    Abc_NtkReassignIds( pNtkNew );
 
     // print a warning about choice nodes
     printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) );
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index b06e7889..5c629b30 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -108,7 +108,7 @@ bool Abc_NtkFxuCheck( Abc_Ntk_t * pNtk )
     {
         Abc_ObjForEachFanin( pNode, pFanin1, i )
         {
-            if ( Abc_ObjFaninC(pNode, i) )
+            if ( i < 2 && Abc_ObjFaninC(pNode, i) )
                 return 0;
             Abc_ObjForEachFanin( pNode, pFanin2, k )
             {
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index fbc5e3ee..783585af 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -467,9 +467,9 @@ void Abc_NodeBddReorder( reo_man * p, Abc_Obj_t * pNode )
     pNode->pData = bFunc;
     // update the fanin order
     Abc_ObjForEachFanin( pNode, pFanin, i )
-        pOrder[i] = pNode->vFanins.pArray[ pOrder[i] ].iFan;
+        pOrder[i] = pNode->vFanins.pArray[ pOrder[i] ];
     Abc_ObjForEachFanin( pNode, pFanin, i )
-        pNode->vFanins.pArray[i].iFan = pOrder[i];
+        pNode->vFanins.pArray[i] = pOrder[i];
     free( pOrder );
 }
 
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 2bdd419d..e96825bb 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -58,7 +58,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         fprintf( pFile, "  net = %5d", Abc_NtkNetNum(pNtk) );
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
     }
-    else if ( Abc_NtkIsStrash(pNtk) )
+    else if ( Abc_NtkHasAig(pNtk) )
     {
         fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
         if ( Num = Abc_NtkGetChoiceNum(pNtk) )
@@ -66,8 +66,6 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         if ( Num = Abc_NtkGetExorNum(pNtk) )
             fprintf( pFile, " (exor = %d)", Num );
     }
-    else if ( Abc_NtkIsSeq(pNtk) )
-        fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
     else 
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
 
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 2b62d40f..9fe5bea0 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -607,7 +607,7 @@ void Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, bool fConst0
     DdNode * bVar, * bTemp;
     int iFanin;
     assert( Abc_NtkIsBddLogic(pNode->pNtk) ); 
-    if ( (iFanin = Vec_FanFindEntry( &pNode->vFanins, pFanin->Id )) == -1 )
+    if ( (iFanin = Vec_IntFind( &pNode->vFanins, pFanin->Id )) == -1 )
     {
         printf( "Node %s should be among", Abc_ObjName(pFanin) );
         printf( " the fanins of node %s...\n", Abc_ObjName(pNode) );
@@ -635,7 +635,7 @@ void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin )
     DdNode * bVar, * bCof0, * bCof1;
     int iFanin;
     assert( Abc_NtkIsBddLogic(pNode->pNtk) ); 
-    if ( (iFanin = Vec_FanFindEntry( &pNode->vFanins, pFanin->Id )) == -1 )
+    if ( (iFanin = Vec_IntFind( &pNode->vFanins, pFanin->Id )) == -1 )
     {
         printf( "Node %s should be among", Abc_ObjName(pFanin) );
         printf( " the fanins of node %s...\n", Abc_ObjName(pNode) );
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 7343582b..7bece42e 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -315,7 +315,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
             fprintf( pFile, "Node%d%s",  Abc_ObjFaninId0(pNode), (Abc_ObjIsLatch(Abc_ObjFanin0(pNode))? "_out":"") );
             fprintf( pFile, " [" );
             fprintf( pFile, "style = %s", Abc_ObjFaninC0(pNode)? "dotted" : "bold" );
-            if ( Seq_ObjFaninL0(pNode) > 0 )
+            if ( Abc_NtkIsSeq(pNode->pNtk) && Seq_ObjFaninL0(pNode) > 0 )
             fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) );
             fprintf( pFile, "]" );
             fprintf( pFile, ";\n" );
@@ -330,7 +330,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
             fprintf( pFile, "Node%d%s",  Abc_ObjFaninId1(pNode), (Abc_ObjIsLatch(Abc_ObjFanin1(pNode))? "_out":"") );
             fprintf( pFile, " [" );
             fprintf( pFile, "style = %s", Abc_ObjFaninC1(pNode)? "dotted" : "bold" );
-            if ( Seq_ObjFaninL1(pNode) > 0 )
+            if ( Abc_NtkIsSeq(pNode->pNtk) && Seq_ObjFaninL1(pNode) > 0 )
             fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) );
             fprintf( pFile, "]" );
             fprintf( pFile, ";\n" );
diff --git a/src/base/seq/module.make b/src/base/seq/module.make
index 2bb176dc..fbb1015a 100644
--- a/src/base/seq/module.make
+++ b/src/base/seq/module.make
@@ -1,4 +1,6 @@
-SRC +=  src/base/seq/seqCreate.c \
+SRC +=    src/base/seq/seqAigCore.c \
+    src/base/seq/seqAigIter.c \
+    src/base/seq/seqCreate.c \
     src/base/seq/seqFpgaCore.c \
     src/base/seq/seqFpgaIter.c \
     src/base/seq/seqLatch.c \
diff --git a/src/base/seq/seq.h b/src/base/seq/seq.h
index 2e1fef91..368f8afc 100644
--- a/src/base/seq/seq.h
+++ b/src/base/seq/seq.h
@@ -43,8 +43,16 @@ typedef struct Abc_Seq_t_  Abc_Seq_t;
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== seqAigCore.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 );
 /*=== seqFpgaCore.c ===============================================================*/
-extern Abc_Ntk_t *     Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int fVerbose );
+extern Abc_Ntk_t *     Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
+/*=== seqMapCore.c ===============================================================*/
+extern Abc_Ntk_t *     Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
+/*=== seqRetCore.c ===========================================================*/
+extern Abc_Ntk_t *     Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int 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 );
@@ -57,10 +65,8 @@ 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_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 );
-extern void            Seq_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose );
+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 );
 /*=== seqUtil.c ==============================================================*/
 extern char *          Seq_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge );
 extern void            Seq_NtkLatchSetValues( Abc_Ntk_t * pNtk, Abc_InitType_t Init );
@@ -69,6 +75,7 @@ extern int             Seq_NtkLatchNumMax( Abc_Ntk_t * pNtk );
 extern int             Seq_NtkLatchNumShared( Abc_Ntk_t * pNtk );
 extern void            Seq_NtkLatchGetInitNums( Abc_Ntk_t * pNtk, int * pInits );
 extern int             Seq_NtkLatchGetEqualFaninNum( Abc_Ntk_t * pNtk );
+extern int             Seq_NtkCountNodesAboveLimit( Abc_Ntk_t * pNtk, int Limit );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c
new file mode 100644
index 00000000..d347d53e
--- /dev/null
+++ b/src/base/seq/seqAigCore.c
@@ -0,0 +1,970 @@
+/**CFile****************************************************************
+
+  FileName    [seqRetCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [The core of retiming procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqRetCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+/* 
+    Retiming can be represented in three equivalent forms:
+    - as a set of integer lags for each node (array of chars by node ID)
+    - as a set of node numbers with lag for each, fwd and bwd (two arrays of Seq_RetStep_t_)
+    - as a set of latch moves over the nodes, fwd and bwd (two arrays of node pointers Abc_Obj_t *)
+*/
+
+static void        Abc_ObjRetimeForward( Abc_Obj_t * pObj );
+static int         Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtk, stmm_table * tTable, Vec_Int_t * vValues );
+static void        Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable );
+static void        Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel );
+
+static void        Seq_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves );
+static int         Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int fVerbose );
+static void        Abc_ObjRetimeForward( Abc_Obj_t * pObj );
+static int         Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtk, stmm_table * tTable, Vec_Int_t * vValues );
+static void        Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable );
+static void        Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel );
+
+static Vec_Ptr_t * Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward );
+static Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, bool fForward );
+static Vec_Int_t * Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward );
+static void        Abc_ObjRetimeForwardTry( Abc_Obj_t * pObj, int nLatches );  
+static void        Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches );
+  
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs performs optimal delay retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fInitial, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    int RetValue;
+    if ( !fInitial )
+        Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC );
+    // get the retiming lags
+    Seq_AigRetimeDelayLags( 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( Seq_ObjFaninL0(pObj) >= 1 );
+    assert( Seq_ObjFaninL1(pObj) >= 1 );
+    // remove the init values from the fanins
+    Init0 = Seq_NodeDeleteFirst( pObj, 0 ); 
+    Init1 = Seq_NodeDeleteFirst( pObj, 1 );
+    assert( Init0 != ABC_INIT_NONE );
+    assert( Init1 != ABC_INIT_NONE );
+    // take into account the complements in the node
+    if ( Abc_ObjFaninC0(pObj) )
+    {
+        if ( Init0 == ABC_INIT_ZERO )
+            Init0 = ABC_INIT_ONE;
+        else if ( Init0 == ABC_INIT_ONE )
+            Init0 = ABC_INIT_ZERO;
+    }
+    if ( Abc_ObjFaninC1(pObj) )
+    {
+        if ( Init1 == ABC_INIT_ZERO )
+            Init1 = ABC_INIT_ONE;
+        else if ( Init1 == ABC_INIT_ONE )
+            Init1 = ABC_INIT_ZERO;
+    }
+    // compute the value at the output of the node
+    if ( Init0 == ABC_INIT_ZERO || Init1 == ABC_INIT_ZERO )
+        Init = ABC_INIT_ZERO;
+    else if ( Init0 == ABC_INIT_ONE && Init1 == ABC_INIT_ONE )
+        Init = ABC_INIT_ONE;
+    else
+        Init = ABC_INIT_DC;
+
+    // make sure the label is clean
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        assert( pFanout->fMarkC == 0 );
+    // add the init values to the fanouts
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        if ( pFanout->fMarkC )
+            continue;
+        pFanout->fMarkC = 1;
+        if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) )
+            Seq_NodeInsertLast( pFanout, Abc_ObjFanoutEdgeNum(pObj, pFanout), Init );
+        else
+        {
+            assert( Abc_ObjFanin0(pFanout) == pObj );
+            Seq_NodeInsertLast( pFanout, 0, Init );
+            Seq_NodeInsertLast( pFanout, 1, Init );
+        }
+    }
+    // clean the label
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        pFanout->fMarkC = 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the given retiming on the sequential AIG.]
+
+  Description [Returns 0 of initial state computation fails.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int fVerbose )
+{
+    Seq_RetEdge_t RetEdge;
+    stmm_table * tTable;
+    stmm_generator * gen;
+    Vec_Int_t * vValues;
+    Abc_Ntk_t * pNtkProb, * pNtkMiter, * pNtkCnf;
+    Abc_Obj_t * pNode, * pNodeNew;
+    int * pModel, RetValue, i, clk;
+
+    // return if the retiming is trivial
+    if ( Vec_PtrSize(vMoves) == 0 )
+        return 1;
+
+    // create the network for the initial state computation
+    // start the table and the array of PO values
+    pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    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 )
+    {
+        if ( Abc_ObjFaninId0(pFanout) == pObj->Id )
+        {
+            Init = Seq_NodeGetInitLast( pFanout, 0 );
+            if ( Init == ABC_INIT_ZERO )
+                fMet0 = 1;
+            else if ( Init == ABC_INIT_ONE )
+                fMet1 = 1;
+            else if ( Init == ABC_INIT_NONE )
+                fMetN = 1;
+        }
+        if ( Abc_ObjFaninId1(pFanout) == pObj->Id )
+        {
+            Init = Seq_NodeGetInitLast( pFanout, 1 );
+            if ( Init == ABC_INIT_ZERO )
+                fMet0 = 1;
+            else if ( Init == ABC_INIT_ONE )
+                fMet1 = 1;
+            else if ( Init == ABC_INIT_NONE )
+                fMetN = 1;
+        }
+    }
+
+    // consider the case when all fanout latches have don't-care values
+    // the new values on the fanin edges will be don't-cares
+    if ( !fMet0 && !fMet1 && !fMetN )
+    {
+        // make sure the label is clean
+        Abc_ObjForEachFanout( pObj, pFanout, i )
+            assert( pFanout->fMarkC == 0 );
+        // update the fanout edges
+        Abc_ObjForEachFanout( pObj, pFanout, i )
+        {
+            if ( pFanout->fMarkC )
+                continue;
+            pFanout->fMarkC = 1;
+            if ( Abc_ObjFaninId0(pFanout) == pObj->Id )
+                Seq_NodeDeleteLast( pFanout, 0 );
+            if ( Abc_ObjFaninId1(pFanout) == pObj->Id )
+                Seq_NodeDeleteLast( pFanout, 1 );
+        }
+        // clean the label
+        Abc_ObjForEachFanout( pObj, pFanout, i )
+            pFanout->fMarkC = 0;
+        // update the fanin edges
+        Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable );
+        Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable );
+        Seq_NodeInsertFirst( pObj, 0, ABC_INIT_DC );
+        Seq_NodeInsertFirst( pObj, 1, ABC_INIT_DC );
+        return 0;
+    }
+    // the initial values on the fanout edges contain 0, 1, or unknown
+    // the new values on the fanin edges will be unknown
+
+    // add new AND-gate to the network
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    pNodeNew->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+
+    // add PO fanouts if any
+    if ( fMet0 )
+    {
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
+        Vec_IntPush( vValues, 0 );
+    }
+    if ( fMet1 )
+    {
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
+        Vec_IntPush( vValues, 1 );
+    }
+
+    // make sure the label is clean
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        assert( pFanout->fMarkC == 0 );
+    // perform the changes
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        if ( pFanout->fMarkC )
+            continue;
+        pFanout->fMarkC = 1;
+        if ( Abc_ObjFaninId0(pFanout) == pObj->Id )
+        {
+            Edge = 0;
+            Value = Seq_NodeDeleteLast( pFanout, Edge );
+            if ( Value != ABC_INIT_NONE )
+                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 ( 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 );
+        }
+    }
+    // clean the label
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        pFanout->fMarkC = 0;
+
+    // update the fanin edges
+    Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable );
+    Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable );
+    Seq_NodeInsertFirst( pObj, 0, ABC_INIT_NONE );
+    Seq_NodeInsertFirst( pObj, 1, ABC_INIT_NONE );
+
+    // add the buffer
+    pBuffer = Abc_NtkCreateNode( pNtkNew );
+    pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+    Abc_ObjAddFanin( pNodeNew, pBuffer );
+    // point to it from the table
+    RetEdge.iNode  = pObj->Id;
+    RetEdge.iEdge  = 0;
+    RetEdge.iLatch = 0;
+    if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pBuffer ) )
+        assert( 0 );
+
+    // add the buffer
+    pBuffer = Abc_NtkCreateNode( pNtkNew );
+    pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+    Abc_ObjAddFanin( pNodeNew, pBuffer );
+    // point to it from the table
+    RetEdge.iNode  = pObj->Id;
+    RetEdge.iEdge  = 1;
+    RetEdge.iLatch = 0;
+    if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pBuffer ) )
+        assert( 0 );
+
+    // report conflict is found
+    return fMet0 && fMet1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generates the printable edge label with the initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable )
+{
+    Abc_Obj_t * pFanoutNew;
+    Seq_RetEdge_t RetEdge;
+    Abc_InitType_t Init;
+    int nLatches, i;
+
+    // get the number of latches on the edge
+    nLatches = Seq_ObjFaninL( pObj, Edge );
+    for ( i = nLatches - 1; i >= 0; i-- )
+    {
+        // get the value of this latch
+        Init = Seq_NodeGetInitOne( pObj, Edge, i );
+        if ( Init != ABC_INIT_NONE )
+            continue;
+        // get the retiming edge
+        RetEdge.iNode  = pObj->Id;
+        RetEdge.iEdge  = Edge;
+        RetEdge.iLatch = i;
+        // remove entry from table and add it with a different key
+        if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
+            assert( 0 );
+        RetEdge.iLatch++;
+        if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pFanoutNew ) )
+            assert( 0 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the initial values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel )
+{
+    Abc_Obj_t * pNode;
+    stmm_generator * gen;
+    Seq_RetEdge_t RetEdge;
+    Abc_InitType_t Init;
+    int i;
+
+    i = 0;
+    stmm_foreach_item( tTable, gen, (char **)&RetEdge, NULL )
+    {
+        pNode = Abc_NtkObj( pNtk, RetEdge.iNode );
+        Init = pModel? (pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC;
+        Seq_NodeSetInitOne( pNode, RetEdge.iEdge, RetEdge.iLatch, Init );
+        i++;
+    }
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs forward retiming of the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward )
+{
+    Vec_Ptr_t * vNodes, * vMoves;
+    Abc_Obj_t * pNode, * pFanout, * pFanin;
+    int i, k, nLatches;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    // assume that all nodes can be retimed
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        Vec_PtrPush( vNodes, pNode );
+        pNode->fMarkA = 1;
+    }
+    // process the nodes
+    vMoves = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+//        printf( "(%d,%d) ", Seq_ObjFaninL0(pNode), Seq_ObjFaninL0(pNode) );
+        // unmark the node as processed
+        pNode->fMarkA = 0;
+        // get the number of latches to retime
+        if ( fForward )
+            nLatches = Seq_ObjFaninLMin(pNode);
+        else
+            nLatches = Seq_ObjFanoutLMin(pNode);
+        if ( nLatches == 0 )
+            continue;
+        assert( nLatches > 0 );
+        // retime the latches forward
+        if ( fForward )
+            Abc_ObjRetimeForwardTry( pNode, nLatches );
+        else
+            Abc_ObjRetimeBackwardTry( pNode, nLatches );
+        // write the moves
+        for ( k = 0; k < nLatches; k++ )
+            Vec_PtrPush( vMoves, pNode );
+        // schedule fanouts for updating
+        if ( fForward )
+        {
+            Abc_ObjForEachFanout( pNode, pFanout, k )
+            {
+                if ( Abc_ObjFaninNum(pFanout) != 2 || pFanout->fMarkA )
+                    continue;
+                pFanout->fMarkA = 1;
+                Vec_PtrPush( vNodes, pFanout );
+            }
+        }
+        else
+        {
+            Abc_ObjForEachFanin( pNode, pFanin, k )
+            {
+                if ( Abc_ObjFaninNum(pFanin) != 2 || pFanin->fMarkA )
+                    continue;
+                pFanin->fMarkA = 1;
+                Vec_PtrPush( vNodes, pFanin );
+            }
+        }
+    }
+    Vec_PtrFree( vNodes );
+    // make sure the marks are clean the the retiming is final
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        assert( pNode->fMarkA == 0 );
+        if ( fForward ) 
+            assert( Seq_ObjFaninLMin(pNode) == 0 );
+        else
+            assert( Seq_ObjFanoutLMin(pNode) == 0 );
+    }
+    return vMoves;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Translates retiming steps into retiming moves.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, bool fForward )
+{
+    Seq_RetStep_t RetStep;
+    Vec_Ptr_t * vMoves;
+    Abc_Obj_t * pNode;
+    int i, k, iNode, nLatches, Number;
+    int fChange;
+    assert( Abc_NtkIsSeq( pNtk ) );
+
+/*
+    // try implementing all the moves at once
+    Vec_IntForEachEntry( vSteps, Number, i )
+    {
+        // get the retiming step
+        RetStep = Seq_Int2RetStep( Number );
+        // get the node to be retimed
+        pNode = Abc_NtkObj( pNtk, RetStep.iNode );
+        assert( RetStep.nLatches > 0 );
+        nLatches = RetStep.nLatches;
+
+        if ( fForward )
+            Abc_ObjRetimeForwardTry( pNode, nLatches );
+        else
+            Abc_ObjRetimeBackwardTry( pNode, nLatches );
+    }
+    // now look if any node has wrong number of latches
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        if ( Seq_ObjFaninL0(pNode) < 0 )
+            printf( "Wrong 0node %d.\n", pNode->Id );
+        if ( Seq_ObjFaninL1(pNode) < 0 )
+            printf( "Wrong 1node %d.\n", pNode->Id );
+    }
+    // try implementing all the moves at once
+    Vec_IntForEachEntry( vSteps, Number, i )
+    {
+        // get the retiming step
+        RetStep = Seq_Int2RetStep( Number );
+        // get the node to be retimed
+        pNode = Abc_NtkObj( pNtk, RetStep.iNode );
+        assert( RetStep.nLatches > 0 );
+        nLatches = RetStep.nLatches;
+
+        if ( !fForward )
+            Abc_ObjRetimeForwardTry( pNode, nLatches );
+        else
+            Abc_ObjRetimeBackwardTry( pNode, nLatches );
+    }
+*/
+
+    // process the nodes
+    vMoves = Vec_PtrAlloc( 100 );
+    while ( Vec_IntSize(vSteps) > 0 )
+    {
+        iNode = 0;
+        fChange = 0;
+        Vec_IntForEachEntry( vSteps, Number, i )
+        {
+            // get the retiming step
+            RetStep = Seq_Int2RetStep( Number );
+            // get the node to be retimed
+            pNode = Abc_NtkObj( pNtk, RetStep.iNode );
+            assert( RetStep.nLatches > 0 );
+            // get the number of latches that can be retimed
+            if ( fForward )
+                nLatches = Seq_ObjFaninLMin(pNode);
+            else
+                nLatches = Seq_ObjFanoutLMin(pNode);
+            if ( nLatches == 0 )
+            {
+                Vec_IntWriteEntry( vSteps, iNode++, Seq_RetStep2Int(RetStep) );
+                continue;
+            }
+            assert( nLatches > 0 );
+            fChange = 1;
+            // get the number of latches to be retimed over this node
+            nLatches = ABC_MIN( nLatches, (int)RetStep.nLatches );
+            // retime the latches forward
+            if ( fForward )
+                Abc_ObjRetimeForwardTry( pNode, nLatches );
+            else
+                Abc_ObjRetimeBackwardTry( pNode, nLatches );
+            // write the moves
+            for ( k = 0; k < nLatches; k++ )
+                Vec_PtrPush( vMoves, pNode );
+            // subtract the retiming performed
+            RetStep.nLatches -= nLatches;
+            // store the node if it is not retimed completely
+            if ( RetStep.nLatches > 0 )
+                Vec_IntWriteEntry( vSteps, iNode++, Seq_RetStep2Int(RetStep) );
+        }
+        // reduce the array
+        Vec_IntShrink( vSteps, iNode );
+        if ( !fChange )
+        {
+            printf( "Warning: %d strange steps (a minor bug to be fixed later).\n", Vec_IntSize(vSteps) );
+/*            
+            Vec_IntForEachEntry( vSteps, Number, i )
+            {
+                RetStep = Seq_Int2RetStep( Number );
+                printf( "%d(%d) ", RetStep.iNode, RetStep.nLatches );
+            }
+            printf( "\n" );
+*/            
+            break;
+        }
+    }
+    // undo the tentative retiming
+    if ( fForward )
+    {
+        Vec_PtrForEachEntryReverse( vMoves, pNode, i )
+            Abc_ObjRetimeBackwardTry( pNode, 1 );
+    }
+    else
+    {
+        Vec_PtrForEachEntryReverse( vMoves, pNode, i )
+            Abc_ObjRetimeForwardTry( pNode, 1 );
+    }
+    return vMoves;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Splits retiming into forward and backward.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward )
+{
+    Vec_Int_t * vNodes;
+    Seq_RetStep_t RetStep;
+    int Value, i;
+    vNodes = Vec_IntAlloc( 100 );
+    Vec_StrForEachEntry( vLags, Value, i )
+    {
+        if ( Value < 0 && fForward )
+        {
+            RetStep.iNode = i;
+            RetStep.nLatches = -Value;
+            Vec_IntPush( vNodes, Seq_RetStep2Int(RetStep) );
+        }
+        else if ( Value > 0 && !fForward )
+        {
+            RetStep.iNode = i;
+            RetStep.nLatches = Value;
+            Vec_IntPush( vNodes, Seq_RetStep2Int(RetStep) );
+        }
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retime node forward without initial states.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjRetimeForwardTry( Abc_Obj_t * pObj, int nLatches )  
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    // make sure it is an AND gate
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    // make sure it has enough latches
+//    assert( Seq_ObjFaninL0(pObj) >= nLatches );
+//    assert( Seq_ObjFaninL1(pObj) >= nLatches );
+    // subtract these latches on the fanin side
+    Seq_ObjAddFaninL0( pObj, -nLatches );
+    Seq_ObjAddFaninL1( pObj, -nLatches );
+    // make sure the label is clean
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        assert( pFanout->fMarkC == 0 );
+    // add these latches on the fanout side
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        if ( pFanout->fMarkC )
+            continue;
+        pFanout->fMarkC = 1;
+        if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) )
+            Seq_ObjAddFanoutL( pObj, pFanout, nLatches );
+        else
+        {
+            assert( Abc_ObjFanin0(pFanout) == pObj );
+            Seq_ObjAddFaninL0( pFanout, nLatches );
+            Seq_ObjAddFaninL1( pFanout, nLatches );
+        }
+    }
+    // clean the label
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        pFanout->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retime node backward without initial states.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches )  
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    // make sure it is an AND gate
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    // make sure the label is clean
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        assert( pFanout->fMarkC == 0 );
+    // subtract these latches on the fanout side
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        if ( pFanout->fMarkC )
+            continue;
+        pFanout->fMarkC = 1;
+//        assert( Abc_ObjFanoutL(pObj, pFanout) >= nLatches );
+        if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) )
+            Seq_ObjAddFanoutL( pObj, pFanout, -nLatches );
+        else
+        {
+            assert( Abc_ObjFanin0(pFanout) == pObj );
+            Seq_ObjAddFaninL0( pFanout, -nLatches );
+            Seq_ObjAddFaninL1( pFanout, -nLatches );
+        }
+    }
+    // clean the label
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        pFanout->fMarkC = 0;
+    // add these latches on the fanin side
+    Seq_ObjAddFaninL0( pObj, nLatches );
+    Seq_ObjAddFaninL1( pObj, nLatches );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqAigIter.c b/src/base/seq/seqAigIter.c
new file mode 100644
index 00000000..9b423d32
--- /dev/null
+++ b/src/base/seq/seqAigIter.c
@@ -0,0 +1,245 @@
+/**CFile****************************************************************
+
+  FileName    [seqRetIter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [The iterative L-Value computation for retiming procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqRetIter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the internal procedures
+static int Seq_RetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose );
+static int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose );
+static int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Retimes AIG for optimal delay using Pan's algorithm.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_AigRetimeDelayLags( 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 ) );
+
+    // get the upper bound on the clock period
+    FiMax = 2 + Seq_NtkLevelMax(pNtk);
+
+    // 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 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 )
+    {
+        NodeLag = Seq_NodeComputeLag( Seq_NodeGetLValue(pNode), FiBest );
+        Seq_NodeSetLag( pNode, NodeLag );
+    }
+/*
+    {
+        Abc_Obj_t * pFanin, * pFanout;
+        pNode = Abc_NtkObj( pNtk, 823 );
+        printf( "Node  %d.  Lag = %d. LValue = %d. Latches = (%d,%d) (%d,%d).\n", pNode->Id, Seq_NodeGetLag(pNode), Seq_NodeGetLValue(pNode), 
+            Seq_ObjFaninL0(pNode), Seq_ObjFaninL1(pNode), Seq_ObjFanoutL(pNode, Abc_NtkObj(pNtk, 826)), Seq_ObjFanoutL(pNode, Abc_NtkObj(pNtk, 1210)) );
+        pFanin = Abc_ObjFanin0( pNode );
+        printf( "Fanin %d.  Lag = %d. LValue = %d. Latches = (%d,%d)\n", pFanin->Id, Seq_NodeGetLag(pFanin), Seq_NodeGetLValue(pFanin),
+            Seq_ObjFaninL0(pFanin), Seq_ObjFaninL1(pFanin) );
+        pFanin = Abc_ObjFanin1( pNode );
+        printf( "Fanin %d.  Lag = %d. LValue = %d.\n", pFanin->Id, Seq_NodeGetLag(pFanin), Seq_NodeGetLValue(pFanin) );
+        Abc_ObjForEachFanout( pNode, pFanout, i )
+            printf( "Fanout %d.  Lag = %d. LValue = %d.\n", pFanout->Id, Seq_NodeGetLag(pFanout), Seq_NodeGetLValue(pFanout) );
+        Abc_ObjForEachFanout( Abc_ObjFanin0(pNode), pFanout, i )
+            printf( "Fanout %d.  Lag = %d. LValue = %d.\n", pFanout->Id, Seq_NodeGetLag(pFanout), Seq_NodeGetLValue(pFanout) );
+    }
+*/
+
+    // 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 of constants and PIs
+    pObj = Abc_NtkObj( pNtk, 0 );
+    Seq_NodeSetLValue( pObj, 0 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Seq_NodeSetLValue( pObj, 0 );
+
+    // update all values iteratively
+    Counter = 0;
+    for ( c = 0; c < p->nMaxIters; c++ )
+    {
+        fChange = 0;
+        Abc_AigForEachAnd( pNtk, pObj, i )
+        {
+            Counter++;
+            if ( Seq_NodeCutMan(pObj) )
+                RetValue = Seq_FpgaNodeUpdateLValue( pObj, Fi );
+            else
+                RetValue = Seq_RetimeNodeUpdateLValue( pObj, Fi );
+            if ( RetValue == SEQ_UPDATE_YES ) 
+                fChange = 1;
+        }
+        Abc_NtkForEachPo( pNtk, pObj, i )
+        {
+            if ( Seq_NodeCutMan(pObj) )
+                RetValue = Seq_FpgaNodeUpdateLValue( pObj, Fi );
+            else
+                RetValue = Seq_RetimeNodeUpdateLValue( pObj, Fi );
+            if ( RetValue == SEQ_UPDATE_FAIL )
+                break;
+        }
+        if ( RetValue == SEQ_UPDATE_FAIL )
+            break;
+        if ( fChange == 0 )
+            break;
+    }
+    if ( c == p->nMaxIters )
+    {
+        RetValue = SEQ_UPDATE_FAIL;
+        pReason = "(timeout)";
+    }
+    else
+        c++;
+    // report the results
+    if ( fVerbose )
+    {
+        if ( RetValue == SEQ_UPDATE_FAIL )
+            printf( "Period = %3d.  Iterations = %3d.  Updates = %10d.    Infeasible %s\n", Fi, c, Counter, pReason );
+        else
+            printf( "Period = %3d.  Iterations = %3d.  Updates = %10d.      Feasible\n",    Fi, c, Counter );
+    }
+    return RetValue != SEQ_UPDATE_FAIL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the node.]
+
+  Description [The node can be internal or a PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
+{
+    int lValueNew, lValueOld, lValue0, lValue1;
+    assert( !Abc_ObjIsPi(pObj) );
+    assert( Abc_ObjFaninNum(pObj) > 0 );
+    lValue0 = Seq_NodeGetLValue(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj);
+    if ( Abc_ObjIsPo(pObj) )
+        return (lValue0 > Fi)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO;
+    if ( Abc_ObjFaninNum(pObj) == 2 )
+        lValue1 = Seq_NodeGetLValue(Abc_ObjFanin1(pObj)) - Fi * Seq_ObjFaninL1(pObj);
+    else
+        lValue1 = -ABC_INFINITY;
+    lValueNew = 1 + ABC_MAX( lValue0, lValue1 );
+    lValueOld = Seq_NodeGetLValue(pObj);
+//    if ( lValueNew == lValueOld )
+    if ( lValueNew <= lValueOld )
+        return SEQ_UPDATE_NO;
+    Seq_NodeSetLValue( pObj, lValueNew );
+    return SEQ_UPDATE_YES;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c
index 05eebe15..d293b946 100644
--- a/src/base/seq/seqCreate.c
+++ b/src/base/seq/seqCreate.c
@@ -75,13 +75,16 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj, * pFaninNew;
     Vec_Int_t * vInitValues;
     Abc_InitType_t Init;
-    int i, k;
+    int i, k, RetValue;
 
     // make sure it is an AIG without self-feeding latches
     assert( Abc_NtkIsStrash(pNtk) );
-    assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
     assert( Abc_NtkIsDfsOrdered(pNtk) );
 
+    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) )
+        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+    assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
+
     // start the network
     pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );
     // duplicate the name and the spec
@@ -235,7 +238,6 @@ void Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk )
     }
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Converts a sequential AIG into a logic SOP network.]
@@ -251,6 +253,76 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pObjNew, * pFaninNew;
+    Seq_Lat_t * pRing;
+    int i;
+
+    assert( Abc_NtkIsSeq(pNtk) );
+    // start the network without latches
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    // duplicate the nodes
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        Abc_NtkDupObj(pNtkNew, pObj);
+        pObj->pCopy->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+    }
+    // share and create the latches
+    Seq_NtkShareLatches( pNtkNew, pNtk );
+    // connect the objects
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        if ( pRing = Seq_NodeGetRing(pObj,0) )
+            pFaninNew = pRing->pLatch;
+        else
+            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+
+        if ( pRing = Seq_NodeGetRing(pObj,1) )
+            pFaninNew = pRing->pLatch;
+        else
+            pFaninNew = Abc_ObjFanin1(pObj)->pCopy;
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+    // connect the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        if ( pRing = Seq_NodeGetRing(pObj,0) )
+            pFaninNew = pRing->pLatch;
+        else
+            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
+        pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+
+    // 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    [Converts a sequential AIG into a logic SOP network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkSeqToLogicSop_old( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pObjNew, * pFaninNew;
     int i;
 
     assert( Abc_NtkIsSeq(pNtk) );
diff --git a/src/base/seq/seqFpgaCore.c b/src/base/seq/seqFpgaCore.c
index cb000ab9..030efd80 100644
--- a/src/base/seq/seqFpgaCore.c
+++ b/src/base/seq/seqFpgaCore.c
@@ -29,9 +29,11 @@ static int          Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk, int fVerbose );
 static Abc_Ntk_t *  Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtkNew );
 static int          Seq_FpgaMappingCount( Abc_Ntk_t * pNtk );
 static int          Seq_FpgaMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
+static Abc_Obj_t *  Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves );
 static DdNode *     Seq_FpgaMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
 static void         Seq_FpgaMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges );
-static Abc_Obj_t *  Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves );
+static void         Seq_FpgaMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
+static DdNode *     Seq_FpgaMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -48,13 +50,25 @@ static Abc_Obj_t *  Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * p
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int fVerbose )
+Abc_Ntk_t * Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
 {
+    Abc_Seq_t * p = pNtk->pManFunc;
     Abc_Ntk_t * pNtkNew;
     Abc_Ntk_t * pNtkMap;
     int RetValue;
+
+    // get the LUT library
+    p->nVarsMax = Fpga_LutLibReadVarMax( Abc_FrameReadLibLut() );
+    p->nMaxIters = nMaxIters;
+
     // find the best mapping and retiming for all nodes (p->vLValues, p->vBestCuts, p->vLags)
     Seq_FpgaMappingDelays( pNtk, fVerbose );
+    if ( RetValue = Abc_NtkGetChoiceNum(pNtk) )
+    {
+        printf( "The network has %d choices. Deriving the resulting network is skipped.\n", RetValue );
+        return NULL;
+    }
+
     // duplicate the nodes contained in multiple cuts
     pNtkNew = Seq_NtkFpgaDup( pNtk );
 //    return pNtkNew;
@@ -67,14 +81,13 @@ Abc_Ntk_t * Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int fVerbose )
 
     // check the compatibility of initial states computed
     if ( RetValue = Seq_NtkFpgaInitCompatible( pNtkNew, fVerbose ) )
-    {
         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 );
     Abc_NtkDelete( pNtkNew );
+    if ( RetValue )
+        printf( "The number of LUTs with more than %d inputs = %d.\n", 
+            p->nVarsMax, Seq_NtkCountNodesAboveLimit(pNtkMap, p->nVarsMax) );
     return pNtkMap;
 }
 
@@ -125,7 +138,6 @@ Abc_Ntk_t * Seq_NtkFpgaDup( Abc_Ntk_t * pNtk )
     // duplicate the latches on the PO edges
     Abc_NtkForEachPo( pNtk, pObj, i )
         Seq_NodeDupLats( pObj->pCopy, pObj, 0 );
-//Abc_NtkShowAig( pNtkNew );
 
     // transfer the mapping info to the new manager
     Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
@@ -264,13 +276,11 @@ int Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk, int fVerbose )
 Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
-    Seq_Lat_t * pLat, * pRing;
     Abc_Ntk_t * pNtkMap; 
-    Vec_Vec_t * vTotalEdges;
-    Vec_Ptr_t * vLeaves, * vMapEdges;
-    Abc_Obj_t * pObj, * pAnd, * pLeaf, * pFanout, * pFanin, * pLatch;
-    int i, k, m, Edge, nLatches, nLatchAfter;
-    unsigned SeqEdge;
+    Vec_Ptr_t * vLeaves;
+    Abc_Obj_t * pObj, * pLatch, * pFaninNew;
+    Seq_Lat_t * pRing;
+    int i;
 
     assert( Abc_NtkIsSeq(pNtk) );
 
@@ -278,87 +288,33 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
     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 );
-    }   
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+        pObj->pCopy = Abc_NtkCreateNode( pNtkMap );
+    // create and share the latches
+    Seq_NtkShareLatchesFpga( pNtkMap, pNtk, p->vMapAnds );
 
-    // construct nodes in the mapped network
-    vTotalEdges = Vec_VecStart( p->nVarsMax );
-    Vec_PtrForEachEntry( p->vMapAnds, pAnd, i )
+    // connect the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, 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 );
-            nLatchAfter = SeqEdge & 255;
-            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 == nLatchAfter );
-            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 );
-        }
+        // get the BDD of the node
+        pObj->pCopy->pData = Seq_FpgaMappingConnectBdd_rec( pNtk, pObj->Id << 8, NULL, -1, pObj, vLeaves );
+        Cudd_Ref( pObj->pCopy->pData );
+        // complement the BDD of the cut if it came from the opposite polarity choice cut
+//        if ( Vec_StrEntry(p->vPhase, i) )
+//            pObj->pCopy->pData = Cudd_Not( pObj->pCopy->pData );
     }
-    Vec_VecFree( vTotalEdges );
 
     // set the POs
     Abc_NtkForEachPo( pNtk, pObj, i )
     {
-        pFanin = Abc_ObjFanin0(pObj)->pCopy;
-        nLatches = Seq_NodeCountLats(pObj, 0);
-        assert( nLatches == Seq_ObjFaninL0(pObj) );
-        if ( nLatches > 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 );
+        if ( pRing = Seq_NodeGetRing(pObj,0) )
+            pFaninNew = pRing->pLatch;
+        else
+            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
+        pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
     }
 
     // add the latches and their names
@@ -368,10 +324,10 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
         Vec_PtrPush( pNtkMap->vCis, pLatch );
         Vec_PtrPush( pNtkMap->vCos, pLatch );
     }
-
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkMap, 1 );
-
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtkMap );
     if ( !Abc_NtkCheck( pNtkMap ) )
         fprintf( stdout, "Seq_NtkSeqFpgaMapped(): Network check has failed.\n" );
     return pNtkMap;
@@ -440,6 +396,52 @@ int Seq_FpgaMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vL
 
 /**Function*************************************************************
 
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+            return pObj->pCopy;
+    // continue unfolding
+    assert( Abc_NodeIsAigAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children    
+    pObjNew = fTop? pObj->pCopy : Abc_NtkCreateNode( pNtkNew );
+    // solve subproblems
+    pFaninNew0 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, LagCut, vLeaves );
+    pFaninNew1 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, LagCut, vLeaves );
+    // add the fanins to the node
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) );
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) );
+    Seq_NodeDupLats( pObjNew, pObj, 0 );
+    Seq_NodeDupLats( pObjNew, pObj, 1 );
+    // set the lag of the new node equal to the internal lag plus mapping/retiming lag
+    Seq_NodeSetLag( pObjNew, (char)(Lag + LagCut) );
+//    Seq_NodeSetLag( pObjNew, (char)(Lag) );
+    return pObjNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derives the BDD of the selected cut.]
 
   Description []
@@ -478,8 +480,6 @@ DdNode * Seq_FpgaMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqE
     bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );  Cudd_Ref( bFunc );
     Cudd_RecursiveDeref( dd, bFunc0 );
     Cudd_RecursiveDeref( dd, bFunc1 );
-    // complement the function if the node is created from the complimented cut
-    // ...
     // return the BDD
     Cudd_Deref( bFunc );
     return bFunc;
@@ -537,18 +537,33 @@ void Seq_FpgaMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * p
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves )
+void Seq_FpgaMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves )
 {
-    Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1;
+    Seq_Lat_t * pRing;
+    Abc_Obj_t * pObj, * pLeaf, * pFanin, * pFaninNew;
     unsigned SeqEdge0, SeqEdge1;
-    int Lag, i;
+    int Lag, i, k;
     // get the object and the lag
     pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
     Lag  = SeqEdge & 255;
-    // if the node is the fanin of the cut, return
+    // if the node is the fanin of the cut, add the connection and return
     Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
         if ( SeqEdge == (unsigned)pLeaf )
-            return pObj->pCopy;
+        {
+            assert( pPrev != NULL );
+            if ( pRing = Seq_NodeGetRing(pPrev,Edge) )
+                pFaninNew = pRing->pLatch;
+            else
+                pFaninNew = Abc_ObjFanin(pPrev,Edge)->pCopy;
+            // check if the root already has this fanin
+            Abc_ObjForEachFanin( pRoot, pFanin, k )
+                if ( pFanin == pFaninNew )
+                    return;
+            Abc_ObjAddFanin( pRoot->pCopy, pFaninNew );
+            return;
+        }
+    }
     // continue unfolding
     assert( Abc_NodeIsAigAnd(pObj) );
     // get new sequential edges
@@ -557,19 +572,69 @@ Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, uns
     SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
     SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
     // call for the children    
-    pObjNew = fTop? pObj->pCopy : Abc_NtkCreateNode( pNtkNew );
-    // solve subproblems
-    pFaninNew0 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, LagCut, vLeaves );
-    pFaninNew1 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, LagCut, vLeaves );
-    // add the fanins to the node
-    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) );
-    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) );
-    Seq_NodeDupLats( pObjNew, pObj, 0 );
-    Seq_NodeDupLats( pObjNew, pObj, 1 );
-    // set the lag of the new node equal to the internal lag plus mapping/retiming lag
-    Seq_NodeSetLag( pObjNew, (char)(Lag + LagCut) );
-//    Seq_NodeSetLag( pObjNew, (char)(Lag) );
-    return pObjNew;
+    Seq_FpgaMappingConnect_rec( pNtk, SeqEdge0, pObj, 0, pRoot, vLeaves );
+    Seq_FpgaMappingConnect_rec( pNtk, SeqEdge1, pObj, 1, pRoot, vLeaves );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Seq_FpgaMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves )
+{
+    Seq_Lat_t * pRing;
+    Abc_Obj_t * pObj, * pLeaf, * pFanin, * pFaninNew;
+    unsigned SeqEdge0, SeqEdge1;
+    DdManager * dd = pRoot->pCopy->pNtk->pManFunc;
+    DdNode * bFunc, * bFunc0, * bFunc1;
+    int Lag, i, k;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, add the connection and return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+            assert( pPrev != NULL );
+            if ( pRing = Seq_NodeGetRing(pPrev,Edge) )
+                pFaninNew = pRing->pLatch;
+            else
+                pFaninNew = Abc_ObjFanin(pPrev,Edge)->pCopy;
+            // check if the root already has this fanin
+            Abc_ObjForEachFanin( pRoot->pCopy, pFanin, k )
+                if ( pFanin == pFaninNew )
+                    return Cudd_bddIthVar( dd, k );
+            Abc_ObjAddFanin( pRoot->pCopy, pFaninNew );
+            return Cudd_bddIthVar( dd, k );
+        }
+    }
+    // continue unfolding
+    assert( Abc_NodeIsAigAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children    
+    bFunc0 = Seq_FpgaMappingConnectBdd_rec( pNtk, SeqEdge0, pObj, 0, pRoot, vLeaves );    Cudd_Ref( bFunc0 );
+    bFunc1 = Seq_FpgaMappingConnectBdd_rec( pNtk, SeqEdge1, pObj, 1, pRoot, vLeaves );    Cudd_Ref( bFunc1 );
+    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pObj) );
+    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pObj) );
+    // get the BDD of the node
+    bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );  Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( dd, bFunc0 );
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    // return the BDD
+    Cudd_Deref( bFunc );
+    return bFunc;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqFpgaIter.c b/src/base/seq/seqFpgaIter.c
index fc521158..9d4002bc 100644
--- a/src/base/seq/seqFpgaIter.c
+++ b/src/base/seq/seqFpgaIter.c
@@ -30,6 +30,7 @@ static void        Seq_FpgaMappingCollectNode_rec( Abc_Obj_t * pAnd, Vec_Ptr_t *
 static Cut_Cut_t * Seq_FpgaMappingSelectCut( Abc_Obj_t * pAnd );
 
 extern Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
+extern Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -53,9 +54,6 @@ void Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose )
     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)
@@ -68,13 +66,16 @@ void Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose )
     // compute the cuts
 clk = clock();
     p->pCutMan = Abc_NtkSeqCuts( pNtk, pParams );
+//    pParams->fSeq = 0;
+//    p->pCutMan = Abc_NtkCuts( pNtk, pParams );
 p->timeCuts = clock() - clk;
+
     if ( fVerbose )
     Cut_ManPrintStats( p->pCutMan );
 
     // compute the delays
 clk = clock();
-    Seq_NtkRetimeDelayLags( pNtk, fVerbose );
+    Seq_AigRetimeDelayLags( pNtk, fVerbose );
 p->timeDelay = clock() - clk;
 
     // collect the nodes and cuts used in the mapping
@@ -129,8 +130,6 @@ void Seq_FpgaMappingCollectNode_rec( Abc_Obj_t * pAnd, Vec_Ptr_t * vMapping, Vec
     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*************************************************************
@@ -237,6 +236,9 @@ int Seq_FpgaNodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
     }
     // get the arrival time of the best non-trivial cut
     pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj );
+    // skip the choice nodes
+    if ( pList == NULL )
+        return SEQ_UPDATE_NO;
     lValueNew = ABC_INFINITY;
     for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
     {
@@ -249,8 +251,8 @@ int Seq_FpgaNodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
 //    if ( lValueNew == lValueOld )
     if ( lValueNew <= lValueOld )
         return SEQ_UPDATE_NO;
-//printf( "%d ", lValueNew );
     Seq_NodeSetLValue( pObj, lValueNew );
+//printf( "%d -> %d   ", lValueOld, lValueNew );
     return SEQ_UPDATE_YES;
 }
 
diff --git a/src/base/seq/seqInt.h b/src/base/seq/seqInt.h
index a39a6d69..4503cef8 100644
--- a/src/base/seq/seqInt.h
+++ b/src/base/seq/seqInt.h
@@ -27,6 +27,10 @@
 
 #include "abc.h"
 #include "cut.h"
+#include "main.h"
+#include "mio.h"
+#include "mapper.h"
+#include "fpga.h"
 #include "seq.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -52,15 +56,23 @@ struct Abc_Seq_t_
     Vec_Ptr_t *         vInits;         // the initial states for each edge in the AIG
     Extra_MmFixed_t *   pMmInits;       // memory manager for latch structures used to remember init states
     int                 fVerbose;       // the verbose flag
+    float               fEpsilon;       // the accuracy for delay computation
+    int                 fStandCells;    // the flag denoting standard cell mapping
+    int                 nMaxIters;      // the max number of iterations
     // K-feasible cuts
     int                 nVarsMax;       // the max cut size
     Cut_Man_t *         pCutMan;        // cut manager
+    Map_SuperLib_t *    pSuperLib;      // the current supergate library
     // sequential arrival time computation
     Vec_Int_t *         vLValues;       // the arrival times (L-Values of nodes)
+    Vec_Int_t *         vLValuesN;      // the arrival times (L-Values of nodes)
     Vec_Str_t *         vLags;          // the lags of the mapped nodes
+    Vec_Str_t *         vLagsN;         // the lags of the mapped nodes
+    Vec_Str_t *         vUses;          // the phase usage
     // representation of the mapping
     Vec_Ptr_t *         vMapAnds;       // nodes visible in the mapping 
     Vec_Vec_t *         vMapCuts;       // best cuts for each node 
+    Vec_Vec_t *         vMapDelays;     // the delay of each fanin
     // runtime stats
     int                 timeCuts;       // runtime to compute the cuts
     int                 timeDelay;      // runtime to compute the L-values
@@ -75,6 +87,7 @@ struct Seq_Lat_t_
 {
     Seq_Lat_t *         pNext;          // the next Lat in the ring
     Seq_Lat_t *         pPrev;          // the prev Lat in the ring 
+    Abc_Obj_t *         pLatch;         // the real latch corresponding to Lat
 };
 
 // representation of latch on the edge
@@ -94,6 +107,19 @@ struct Seq_RetStep_t_ // 1 word
     unsigned            nLatches :  8;  // the number of latches to retime
 };
 
+// representation of one mapping match
+typedef struct Seq_Match_t_       Seq_Match_t;   
+struct Seq_Match_t_ // 3 words
+{
+    Abc_Obj_t *         pAnd;           // the AND gate used in the mapping
+    Cut_Cut_t *         pCut;           // the cut used to map it
+    Map_Super_t *       pSuper;         // the supergate used to implement the cut
+    unsigned            fCompl  :  1;   // the polarity of the AND gate
+    unsigned            fCutInv :  1;   // the polarity of the cut
+    unsigned            PolUse  :  2;   // the polarity use of this node
+    unsigned            uPhase  : 28;   // the phase assignment at the boundary
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -124,9 +150,15 @@ static inline int            Seq_ObjFaninLMax( Abc_Obj_t * pObj )
 
 // reading l-values and lags
 static inline Vec_Int_t *    Seq_NodeLValues( Abc_Obj_t * pNode )                    { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLValues;           }
+static inline Vec_Int_t *    Seq_NodeLValuesN( Abc_Obj_t * pNode )                   { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLValuesN;          }
 static inline int            Seq_NodeGetLValue( Abc_Obj_t * pNode )                  { return Vec_IntEntry( Seq_NodeLValues(pNode), (pNode)->Id );        }
 static inline void           Seq_NodeSetLValue( Abc_Obj_t * pNode, int Value )       { Vec_IntWriteEntry( Seq_NodeLValues(pNode), (pNode)->Id, Value );   }
+static inline float          Seq_NodeGetLValueP( Abc_Obj_t * pNode )                 { return Abc_Int2Float( Vec_IntEntry( Seq_NodeLValues(pNode), (pNode)->Id ) );        }
+static inline float          Seq_NodeGetLValueN( Abc_Obj_t * pNode )                 { return Abc_Int2Float( Vec_IntEntry( Seq_NodeLValuesN(pNode), (pNode)->Id ) );       }
+static inline void           Seq_NodeSetLValueP( Abc_Obj_t * pNode, float Value )    { Vec_IntWriteEntry( Seq_NodeLValues(pNode), (pNode)->Id, Abc_Float2Int(Value) );     }
+static inline void           Seq_NodeSetLValueN( Abc_Obj_t * pNode, float Value )    { Vec_IntWriteEntry( Seq_NodeLValuesN(pNode), (pNode)->Id, Abc_Float2Int(Value) );    }
 static inline int            Seq_NodeComputeLag( int LValue, int Fi )                { return (LValue + 1024*Fi)/Fi - 1024 - (int)(LValue % Fi == 0);     }
+static inline int            Seq_NodeComputeLagFloat( float LValue, float Fi )       { return ((int)ceil(LValue/Fi)) - 1;                                        }
 
 // reading the contents of the lat
 static inline Abc_InitType_t Seq_LatInit( Seq_Lat_t * pLat )  { return ((unsigned)pLat->pPrev) & 3;                                 }
@@ -141,14 +173,22 @@ static inline void           Seq_LatSetPrev( Seq_Lat_t * pLat, Seq_Lat_t * pPrev
 // accessing retiming lags
 static inline Cut_Man_t *    Seq_NodeCutMan( Abc_Obj_t * pNode )                      { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->pCutMan;                 }
 static inline Vec_Str_t *    Seq_NodeLags( Abc_Obj_t * pNode )                        { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLags;            }
+static inline Vec_Str_t *    Seq_NodeLagsN( Abc_Obj_t * pNode )                       { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLagsN;           }
 static inline char           Seq_NodeGetLag( Abc_Obj_t * pNode )                      { return Vec_StrEntry( Seq_NodeLags(pNode), (pNode)->Id );         }
+static inline char           Seq_NodeGetLagN( Abc_Obj_t * pNode )                     { return Vec_StrEntry( Seq_NodeLagsN(pNode), (pNode)->Id );        }
 static inline void           Seq_NodeSetLag( Abc_Obj_t * pNode, char Value )          { Vec_StrWriteEntry( Seq_NodeLags(pNode), (pNode)->Id, (Value) );  }
+static inline void           Seq_NodeSetLagN( Abc_Obj_t * pNode, char Value )         { Vec_StrWriteEntry( Seq_NodeLagsN(pNode), (pNode)->Id, (Value) ); }
+
+// phase usage
+static inline Vec_Str_t *    Seq_NodeUses( Abc_Obj_t * pNode )                        { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vUses;            }
+static inline char           Seq_NodeGetUses( Abc_Obj_t * pNode )                     { return Vec_StrEntry( Seq_NodeUses(pNode), (pNode)->Id );         }
+static inline void           Seq_NodeSetUses( Abc_Obj_t * pNode, char Value )         { Vec_StrWriteEntry( Seq_NodeUses(pNode), (pNode)->Id, (Value) );  }
 
 // accessing initial states
 static inline Vec_Ptr_t *    Seq_NodeLats( Abc_Obj_t * pObj )                                { return ((Abc_Seq_t*)pObj->pNtk->pManFunc)->vInits;                                           }
 static inline Seq_Lat_t *    Seq_NodeGetRing( Abc_Obj_t * pObj, int Edge )                   { return Vec_PtrEntry( Seq_NodeLats(pObj), (pObj->Id<<1)+Edge );                               }
 static inline void           Seq_NodeSetRing( Abc_Obj_t * pObj, int Edge, Seq_Lat_t * pLat ) { Vec_PtrWriteEntry( Seq_NodeLats(pObj), (pObj->Id<<1)+Edge, pLat );                           }
-static inline Seq_Lat_t *    Seq_NodeCreateLat( Abc_Obj_t * pObj )                           { return (Seq_Lat_t *)Extra_MmFixedEntryFetch( ((Abc_Seq_t*)pObj->pNtk->pManFunc)->pMmInits ); }
+static inline Seq_Lat_t *    Seq_NodeCreateLat( Abc_Obj_t * pObj )                           { Seq_Lat_t * p = (Seq_Lat_t *)Extra_MmFixedEntryFetch( ((Abc_Seq_t*)pObj->pNtk->pManFunc)->pMmInits ); p->pNext = p->pPrev = NULL; p->pLatch = NULL; return p; }
 static inline void           Seq_NodeRecycleLat( Abc_Obj_t * pObj, Seq_Lat_t * pLat )        { Extra_MmFixedEntryRecycle( ((Abc_Seq_t*)pObj->pNtk->pManFunc)->pMmInits, (char *)pLat );     }
 
 // getting hold of the structure storing initial states of the latches
@@ -167,18 +207,23 @@ static inline void           Seq_NodeSetInitOne( Abc_Obj_t * pObj, int Edge, int
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== seqAigIter.c =============================================================*/
+extern void                  Seq_AigRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose );
+extern int                   Seq_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags, int fVerbose );
+/*=== seqFpgaIter.c ============================================================*/
+extern void                  Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose );
+extern int                   Seq_FpgaNodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
+/*=== seqMapIter.c ============================================================*/
+extern void                  Seq_MapRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose );
+/*=== seqRetIter.c =============================================================*/
+extern void                  Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose );
 /*=== seqLatch.c ===============================================================*/
 extern void                  Seq_NodeInsertFirst( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init );  
 extern void                  Seq_NodeInsertLast( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init );  
 extern Abc_InitType_t        Seq_NodeDeleteFirst( Abc_Obj_t * pObj, int Edge );  
 extern Abc_InitType_t        Seq_NodeDeleteLast( Abc_Obj_t * pObj, int Edge );  
-/*=== seqFpgaIter.c ============================================================*/
-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_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_NtkLevelMax( Abc_Ntk_t * pNtk );
 extern int                   Seq_ObjFanoutLMax( Abc_Obj_t * pObj );
 extern int                   Seq_ObjFanoutLMin( Abc_Obj_t * pObj );
 extern int                   Seq_ObjFanoutLSum( Abc_Obj_t * pObj );
diff --git a/src/base/seq/seqMan.c b/src/base/seq/seqMan.c
index 109199fe..7dae5b23 100644
--- a/src/base/seq/seqMan.c
+++ b/src/base/seq/seqMan.c
@@ -49,12 +49,17 @@ 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) );
+    p->nMaxIters = 15;
+    p->pMmInits  = Extra_MmFixedStart( sizeof(Seq_Lat_t) );
+    p->fEpsilon  = (float)0.001;
     // create internal data structures
-    p->vNums    = Vec_IntStart( 2 * p->nSize ); 
-    p->vInits   = Vec_PtrStart( 2 * p->nSize ); 
-    p->vLValues = Vec_IntStart( p->nSize ); 
-    p->vLags    = Vec_StrStart( p->nSize ); 
+    p->vNums     = Vec_IntStart( 2 * p->nSize ); 
+    p->vInits    = Vec_PtrStart( 2 * p->nSize ); 
+    p->vLValues  = Vec_IntStart( p->nSize ); 
+    p->vLags     = Vec_StrStart( p->nSize ); 
+    p->vLValuesN = Vec_IntStart( p->nSize ); 
+    p->vLagsN    = Vec_StrStart( p->nSize ); 
+    p->vUses     = Vec_StrStart( p->nSize ); 
     return p;
 }
 
@@ -78,6 +83,9 @@ void Seq_Resize( Abc_Seq_t * p, int nMaxId )
     Vec_PtrFill( p->vInits,    2 * p->nSize, NULL ); 
     Vec_IntFill( p->vLValues,  p->nSize, 0 ); 
     Vec_StrFill( p->vLags,     p->nSize, 0 ); 
+    Vec_IntFill( p->vLValuesN, p->nSize, 0 ); 
+    Vec_StrFill( p->vLagsN,    p->nSize, 0 ); 
+    Vec_StrFill( p->vUses,     p->nSize, 0 ); 
 }
 
 
@@ -94,10 +102,19 @@ void Seq_Resize( Abc_Seq_t * p, int nMaxId )
 ***********************************************************************/
 void Seq_Delete( Abc_Seq_t * p )
 {
+    if ( p->fStandCells )
+    {
+        void * pVoid; int i;
+        Vec_PtrForEachEntry( p->vMapAnds, pVoid, i )
+            free( pVoid );
+    }
     if ( p->vMapAnds )  Vec_PtrFree( p->vMapAnds );  // the nodes used in the mapping
     if ( p->vMapCuts )  Vec_VecFree( p->vMapCuts );  // the cuts used in the mapping
     if ( p->vLValues )  Vec_IntFree( p->vLValues );  // the arrival times (L-Values of nodes)
     if ( p->vLags )     Vec_StrFree( p->vLags );     // the lags of the mapped nodes
+    if ( p->vLValuesN ) Vec_IntFree( p->vLValuesN ); // the arrival times (L-Values of nodes)
+    if ( p->vLagsN )    Vec_StrFree( p->vLagsN );    // the lags of the mapped nodes
+    if ( p->vUses )     Vec_StrFree( p->vUses );     // the uses of phases
     if ( p->vInits )    Vec_PtrFree( p->vInits );    // the initial values of the latches
     if ( p->vNums )     Vec_IntFree( p->vNums );     // the numbers of latches
     Extra_MmFixedStop( p->pMmInits, 0 );
diff --git a/src/base/seq/seqMapCore.c b/src/base/seq/seqMapCore.c
index 8c72538b..4f5a5e73 100644
--- a/src/base/seq/seqMapCore.c
+++ b/src/base/seq/seqMapCore.c
@@ -19,18 +19,250 @@
 ***********************************************************************/
 
 #include "seqInt.h"
+#include "main.h"
+#include "mio.h"
+#include "mapper.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern Abc_Ntk_t *  Seq_NtkMapDup( Abc_Ntk_t * pNtk );
+extern int          Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose );
+extern Abc_Ntk_t *  Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk );
+
+static int          Seq_MapMappingCount( Abc_Ntk_t * pNtk );
+static int          Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
+static Abc_Obj_t *  Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves );
+static DdNode *     Seq_MapMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
+static void         Seq_MapMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges );
+static void         Seq_MapMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
+static DdNode *     Seq_MapMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Performs Map mapping and retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Ntk_t * pNtkMap;
+    int RetValue;
+
+    // derive the supergate library
+    if ( Abc_FrameReadLibSuper() == NULL && Abc_FrameReadLibGen() )
+    {
+        printf( "A simple supergate library is derived from gate library \"%s\".\n", 
+            Mio_LibraryReadName(Abc_FrameReadLibGen()) );
+        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen() );
+    }
+    p->pSuperLib   = Abc_FrameReadLibSuper();
+    p->nVarsMax    = Map_SuperLibReadVarsMax(p->pSuperLib);
+    p->nMaxIters   = nMaxIters;
+    p->fStandCells = 1;
+
+    // find the best mapping and retiming for all nodes (p->vLValues, p->vBestCuts, p->vLags)
+    Seq_MapRetimeDelayLags( pNtk, fVerbose );
+    if ( RetValue = Abc_NtkGetChoiceNum(pNtk) )
+    {
+        printf( "The network has %d choices. Deriving the resulting network is skipped.\n", RetValue );
+        return NULL;
+    }
+    return NULL;
+
+    // duplicate the nodes contained in multiple cuts
+    pNtkNew = Seq_NtkMapDup( pNtk );
+//    return pNtkNew;
+    
+    // implement the retiming
+    RetValue = Seq_NtkImplementRetiming( pNtkNew, ((Abc_Seq_t *)pNtkNew->pManFunc)->vLags, fVerbose );
+    if ( RetValue == 0 )
+        printf( "Retiming completed but initial state computation has failed.\n" );
+//    return pNtkNew;
+
+    // check the compatibility of initial states computed
+    if ( RetValue = Seq_NtkMapInitCompatible( pNtkNew, fVerbose ) )
+    {
+        printf( "The number of LUTs with incompatible edges = %d.\n", RetValue );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+
+    // create the final mapped network
+    pNtkMap = Seq_NtkSeqMapMapped( pNtkNew );
+    Abc_NtkDelete( pNtkNew );
+    return pNtkMap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the network by duplicating some of the nodes.]
+
+  Description [Information about mapping is given as mapping nodes (p->vMapAnds)
+  and best cuts for each node (p->vMapCuts).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * pNew, * p = pNtk->pManFunc;
+    Seq_Match_t * pMatch;
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pLeaf, * pDriver, * pDriverNew;
+    Vec_Ptr_t * vLeaves;
+    unsigned SeqEdge;
+    int i, k, nObjsNew, Lag;
+    
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    // start the expanded network
+    pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
+    Abc_NtkCleanNext( pNtk );
+
+    // start the new sequential AIG manager
+    nObjsNew = 1 + Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk) + Seq_MapMappingCount(pNtk);
+    Seq_Resize( pNtkNew->pManFunc, nObjsNew );
+
+    // duplicate the nodes in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+        if ( pMatch->fCompl )
+            pMatch->pAnd->pNext = Abc_NtkCreateNode( pNtkNew );
+        else
+            pMatch->pAnd->pCopy = Abc_NtkCreateNode( pNtkNew );
+
+    // recursively construct the internals of each node
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+    {
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        Seq_MapMappingBuild_rec( pNtkNew, pNtk, pObj->Id << 8, 1, Seq_NodeGetLag(pObj), vLeaves );
+    }
+    assert( nObjsNew == pNtkNew->nObjs );
+
+    // set the POs
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        pDriver    = Abc_ObjFanin0(pObj);
+        pDriverNew = Abc_ObjFaninC0(pObj)? pDriver->pNext : pDriver->pCopy;
+        Abc_ObjAddFanin( pObj->pCopy, pDriverNew );
+    }
+
+    // duplicate the latches on the PO edges
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_NodeDupLats( pObj->pCopy, pObj, 0 );
+
+    // transfer the mapping info to the new manager
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        // convert the root node
+//        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
+        pMatch->pAnd = pMatch->pAnd->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 );
+//            Lag = (SeqEdge & 255);// + Seq_NodeGetLag(pObj) - Seq_NodeGetLag(pLeaf);
+            Lag = (SeqEdge & 255) + Seq_NodeGetLag(pObj) - Seq_NodeGetLag(pLeaf);
+            assert( Lag >= 0 );
+            // translate the old leaf into the leaf in the new network
+            Vec_PtrWriteEntry( vLeaves, k, (void *)((pLeaf->pCopy->Id << 8) | Lag) );
+//            printf( "%d -> %d\n", pLeaf->Id, pLeaf->pCopy->Id );
+        }
+    }
+    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_NtkMapDup(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the initial states are compatible.]
+
+  Description [Checks of all the initial states on the fanins edges
+  of the cut have compatible number of latches and initial states.
+  If this is not true, then the mapped network with the does not have initial 
+  state. Returns the number of LUTs with incompatible edges.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the final mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk )
+{
+    return NULL;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nodes in the bag.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapMappingCount( Abc_Ntk_t * pNtk )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Vec_Ptr_t * vLeaves;
+    Abc_Obj_t * pAnd;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( p->vMapAnds, pAnd, i )
+    {
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        Counter += Seq_MapMappingCount_rec( pNtk, pAnd->Id << 8, vLeaves );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nodes in the bag.]
 
   Description []
                
@@ -39,6 +271,76 @@
   SeeAlso     []
 
 ***********************************************************************/
+int Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj, * pLeaf;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+            return 0;
+    // continue unfolding
+    assert( Abc_NodeIsAigAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children
+    return 1 + Seq_MapMappingCount_rec( pNtk, SeqEdge0, vLeaves ) + 
+        Seq_MapMappingCount_rec( pNtk, SeqEdge1, vLeaves );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+            return pObj->pCopy;
+    // continue unfolding
+    assert( Abc_NodeIsAigAnd(pObj) );
+    // get new sequential edges
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
+    // call for the children    
+    pObjNew = fTop? pObj->pCopy : Abc_NtkCreateNode( pNtkNew );
+    // solve subproblems
+    pFaninNew0 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, LagCut, vLeaves );
+    pFaninNew1 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, LagCut, vLeaves );
+    // add the fanins to the node
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) );
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) );
+    Seq_NodeDupLats( pObjNew, pObj, 0 );
+    Seq_NodeDupLats( pObjNew, pObj, 1 );
+    // set the lag of the new node equal to the internal lag plus mapping/retiming lag
+    Seq_NodeSetLag( pObjNew, (char)(Lag + LagCut) );
+//    Seq_NodeSetLag( pObjNew, (char)(Lag) );
+    return pObjNew;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/seq/seqMapIter.c b/src/base/seq/seqMapIter.c
index 5f59ca50..5a8b57bd 100644
--- a/src/base/seq/seqMapIter.c
+++ b/src/base/seq/seqMapIter.c
@@ -19,10 +19,19 @@
 ***********************************************************************/
 
 #include "seqInt.h"
+#include "main.h"
+#include "mio.h"
+#include "mapperInt.h"
 
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
+// the internal procedures
+static float Seq_MapRetimeDelayLagsInternal( Abc_Ntk_t * pNtk, int fVerbose );
+static float Seq_MapRetimeSearch_rec( Abc_Ntk_t * pNtk, float FiMin, float FiMax, float Delta, int fVerbose );
+static int   Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose );
+static int   Seq_MapNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, float DelayInv );
+static float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMapping, Vec_Vec_t * vMapCuts );
+static void  Seq_MapCanonicizeTruthTables( Abc_Ntk_t * pNtk );
+
+extern Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -30,7 +39,236 @@
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Computes the retiming lags for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_MapRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Cut_Params_t Params, * pParams = &Params;
+    Abc_Obj_t * pObj;
+    float TotalArea, FiBest;
+    int i, clk;
+
+    // set defaults for cut computation
+    memset( pParams, 0, sizeof(Cut_Params_t) );
+    pParams->nVarsMax  = p->nVarsMax;  // the max cut size ("k" of the k-feasible cuts)
+    pParams->nKeepMax  = 1000;  // the max number of cuts kept at a node
+    pParams->fTruth    = 1;     // compute truth tables
+    pParams->fFilter   = 1;     // filter dominated cuts
+    pParams->fSeq      = 1;     // compute sequential cuts
+    pParams->fVerbose  = fVerbose;     // the verbosiness flag
+
+    // compute the cuts
+clk = clock();
+    p->pCutMan = Abc_NtkSeqCuts( pNtk, pParams );
+p->timeCuts = clock() - clk;
+    if ( fVerbose )
+        Cut_ManPrintStats( p->pCutMan );
+
+    // compute canonical forms of the truth tables of the cuts
+    Seq_MapCanonicizeTruthTables( pNtk );
+
+    // compute the delays
+clk = clock();
+    FiBest = Seq_MapRetimeDelayLagsInternal( 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 );
+    TotalArea = 0.0;
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        TotalArea += Seq_MapCollectNode_rec( Abc_ObjChild0(pObj), FiBest, p->vMapAnds, p->vMapCuts );
+
+    // clean the marks
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->fMarkA = pObj->fMarkB = 0;
+
+    if ( fVerbose )
+        printf( "Total area = %6.2f.\n", TotalArea );
+
+    // remove the cuts
+    Cut_ManStop( p->pCutMan );
+    p->pCutMan = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retimes AIG for optimal delay using Pan's algorithm.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Seq_MapRetimeDelayLagsInternal( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Obj_t * pNode;
+    float FiMax, FiBest, Delta;
+    int i, RetValue;
+    char NodeLag;
+
+    assert( Abc_NtkIsSeq( pNtk ) );
+
+    // assign the accuracy for min-period computation
+    Delta = Mio_LibraryReadDelayNand2Max(Abc_FrameReadLibGen());
+    if ( Delta == 0.0 )
+    {
+        Delta = Mio_LibraryReadDelayAnd2Max(Abc_FrameReadLibGen());
+        if ( Delta == 0.0 )
+        {
+            printf( "Cannot retime/map if the library does not have NAND2 or AND2.\n" );
+            return 0.0;
+        }
+    }
+
+    // get the upper bound on the clock period
+    FiMax = Delta * (2 + Seq_NtkLevelMax(pNtk));
+    Delta /= 2;
+
+    // make sure this clock period is feasible
+    assert( Seq_MapRetimeForPeriod( pNtk, FiMax, fVerbose ) );
+
+    // search for the optimal clock period between 0 and nLevelMax
+    FiBest = Seq_MapRetimeSearch_rec( pNtk, 0.0, FiMax, Delta, fVerbose );
+
+    // recompute the best l-values
+    RetValue = Seq_MapRetimeForPeriod( pNtk, FiBest, fVerbose );
+    assert( RetValue );
+
+    // write the retiming lags for both phases of each node
+    Vec_StrFill( p->vLags,  p->nSize, 0 );
+    Vec_StrFill( p->vLagsN, p->nSize, 0 );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueP(pNode), FiBest );
+        Seq_NodeSetLag( pNode, NodeLag );
+        NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueN(pNode), FiBest );
+        Seq_NodeSetLagN( pNode, NodeLag );
+    }
+
+    // print the result
+    if ( fVerbose )
+    printf( "The best clock period is %6.2f.\n", FiBest );
+    return FiBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs binary search for the optimal clock period.]
+
+  Description [Assumes that FiMin is infeasible while FiMax is feasible.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Seq_MapRetimeSearch_rec( Abc_Ntk_t * pNtk, float FiMin, float FiMax, float Delta, int fVerbose )
+{
+    float Median;
+    assert( FiMin < FiMax );
+    if ( FiMin + Delta >= FiMax )
+        return FiMax;
+    Median = FiMin + (FiMax - FiMin)/2;
+    if ( Seq_MapRetimeForPeriod( pNtk, Median, fVerbose ) )
+        return Seq_MapRetimeSearch_rec( pNtk, FiMin, Median, Delta, fVerbose ); // Median is feasible
+    else 
+        return Seq_MapRetimeSearch_rec( pNtk, Median, FiMax, Delta, fVerbose ); // Median is infeasible
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if retiming with this clock period is feasible.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Obj_t * pObj;
+    float DelayInv = Mio_LibraryReadDelayInvMax(Abc_FrameReadLibGen());
+    int i, c, RetValue, fChange, Counter;
+    char * pReason = "";
+
+    // set l-values of all nodes to be minus infinity
+    Vec_IntFill( p->vLValues,  p->nSize, -ABC_INFINITY );
+    Vec_IntFill( p->vLValuesN, p->nSize, -ABC_INFINITY );
+    Vec_StrFill( p->vUses,     p->nSize, 0             );
+
+    // set l-values of constants and PIs
+    pObj = Abc_NtkObj( pNtk, 0 );
+    Seq_NodeSetLValueP( pObj, 0.0 );
+    Seq_NodeSetLValueN( pObj, 0.0 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        Seq_NodeSetLValueP( pObj, 0.0 );
+        Seq_NodeSetLValueN( pObj, DelayInv );
+    }
+
+    // update all values iteratively
+    Counter = 0;
+    for ( c = 0; c < p->nMaxIters; c++ )
+    {
+        fChange = 0;
+        Abc_AigForEachAnd( pNtk, pObj, i )
+        {
+            Counter++;
+            RetValue = Seq_MapNodeUpdateLValue( pObj, Fi, DelayInv );
+            if ( RetValue == SEQ_UPDATE_YES ) 
+                fChange = 1;
+        }
+        Abc_NtkForEachPo( pNtk, pObj, i )
+        {
+            RetValue = Seq_MapNodeUpdateLValue( pObj, Fi, DelayInv );
+            if ( RetValue == SEQ_UPDATE_FAIL )
+                break;
+        }
+        if ( RetValue == SEQ_UPDATE_FAIL )
+            break;
+        if ( fChange == 0 )
+            break;
+    }
+    if ( c == p->nMaxIters )
+    {
+        RetValue = SEQ_UPDATE_FAIL;
+        pReason = "(timeout)";
+    }
+    else
+        c++;
+
+    // report the results
+    if ( fVerbose )
+    {
+        if ( RetValue == SEQ_UPDATE_FAIL )
+            printf( "Period = %6.2f.  Iterations = %3d.  Updates = %10d.    Infeasible %s\n", Fi, c, Counter, pReason );
+        else
+            printf( "Period = %6.2f.  Iterations = %3d.  Updates = %10d.      Feasible\n",    Fi, c, Counter );
+    }
+    return RetValue != SEQ_UPDATE_FAIL;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the cut.]
 
   Description []
                
@@ -39,9 +277,280 @@
   SeeAlso     []
 
 ***********************************************************************/
+float Seq_MapSuperGetArrival( Abc_Obj_t * pObj, float Fi, Seq_Match_t * pMatch, float DelayMax )
+{
+    Abc_Seq_t * p = pObj->pNtk->pManFunc;
+    Abc_Obj_t * pFanin;
+    float lValueCur, lValueMax;
+    int i;
+    lValueMax = -ABC_INFINITY;
+    for ( i = pMatch->pCut->nLeaves - 1; i >= 0; i-- )
+    {
+        // get the arrival time of the fanin
+        pFanin = Abc_NtkObj( pObj->pNtk, pMatch->pCut->pLeaves[i] >> 8 );
+        if ( pMatch->uPhase & (1 << i) )
+            lValueCur = Seq_NodeGetLValueN(pFanin) - Fi * (pMatch->pCut->pLeaves[i] & 255);
+        else
+            lValueCur = Seq_NodeGetLValueP(pFanin) - Fi * (pMatch->pCut->pLeaves[i] & 255);
+        // add the arrival time of this pin
+        if ( lValueMax < lValueCur + pMatch->pSuper->tDelaysR[i].Worst )
+            lValueMax = lValueCur + pMatch->pSuper->tDelaysR[i].Worst;
+        if ( lValueMax < lValueCur + pMatch->pSuper->tDelaysF[i].Worst )
+            lValueMax = lValueCur + pMatch->pSuper->tDelaysF[i].Worst;
+        if ( lValueMax > DelayMax + p->fEpsilon )
+            return ABC_INFINITY;
+    }
+    return lValueMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Seq_MapNodeComputeCut(  Abc_Obj_t * pObj, Cut_Cut_t * pCut, int fCompl, float Fi, Seq_Match_t * pMatchBest )
+{
+    Seq_Match_t Match, * pMatchCur = &Match;
+    Abc_Seq_t * p = pObj->pNtk->pManFunc;
+    Map_Super_t * pSuper, * pSuperList;
+    unsigned uCanon[2];
+    float lValueBest, lValueCur;
+    int i;
+    assert( pCut->nLeaves < 6 );
+    // get the canonical truth table of this cut
+    uCanon[0] = uCanon[1] = (fCompl? pCut->uCanon0 : pCut->uCanon1);
+    // match the given phase of the cut
+    pSuperList = Map_SuperTableLookupC( p->pSuperLib, uCanon );
+    // compute the arrival times of each supergate
+    lValueBest = ABC_INFINITY;
+    for ( pSuper = pSuperList; pSuper; pSuper = pSuper->pNext )
+    {
+        // create the match
+        pMatchCur->pCut   = pCut;
+        pMatchCur->pSuper = pSuper;
+        // get the phase
+        for ( i = 0; i < (int)pSuper->nPhases; i++ )
+        {
+            pMatchCur->uPhase = (fCompl? pCut->Num0 : pCut->Num1) ^ pSuper->uPhases[i];
+            // find the arrival time of this match
+            lValueCur = Seq_MapSuperGetArrival( pObj, Fi, pMatchCur, lValueBest );
+            if ( lValueBest > lValueCur )
+            {
+                lValueBest = lValueCur;
+                if ( pMatchBest )
+                    *pMatchBest = *pMatchCur;
+            }
+        }
+    }
+    return lValueBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the node.]
+
+  Description [The node can be internal or a PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Seq_MapNodeComputePhase( Abc_Obj_t * pObj, int fCompl, float Fi, Seq_Match_t * pMatchBest )
+{
+    Seq_Match_t Match, * pMatchCur = &Match;
+    Cut_Cut_t * pList, * pCut;
+    float lValueNew, lValueCut;
+    // get the list of cuts
+    pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj );
+    // get the arrival time of the best non-trivial cut
+    lValueNew = ABC_INFINITY;
+    for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
+    {
+        lValueCut = Seq_MapNodeComputeCut( pObj, pCut, fCompl, Fi, pMatchBest? pMatchCur : NULL );
+        if ( lValueNew > lValueCut )
+        {
+            lValueNew = lValueCut;
+            if ( pMatchBest )
+                *pMatchBest = *pMatchCur;
+        }
+    }
+    return lValueNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the node.]
+
+  Description [The node can be internal or a PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, float DelayInv )
+{
+    Abc_Seq_t * p = pObj->pNtk->pManFunc;
+    Cut_Cut_t * pList;
+    char Use;
+    float lValueOld0, lValueOld1, lValue0, lValue1, lValue;
+    assert( !Abc_ObjIsPi(pObj) );
+    assert( Abc_ObjFaninNum(pObj) > 0 );
+    // consider the case of the PO
+    if ( Abc_ObjIsPo(pObj) )
+    {
+        if ( Abc_ObjFaninC0(pObj) ) // PO requires negative polarity
+            lValue = Seq_NodeGetLValueN(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj);
+        else
+            lValue = Seq_NodeGetLValueP(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj);
+        return (lValue > Fi + p->fEpsilon)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO;
+    }
+    // get the cuts
+    pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj );
+    if ( pList == NULL )
+        return SEQ_UPDATE_NO;
+    // compute the arrival time of both phases
+    lValue0 = Seq_MapNodeComputePhase( pObj, 1, Fi, NULL );
+    lValue1 = Seq_MapNodeComputePhase( pObj, 0, Fi, NULL );
+    // consider the case when negative phase is too slow
+    if ( lValue0 > lValue1 + DelayInv + p->fEpsilon )
+        lValue0 = lValue1 + DelayInv, Use = 2;
+    else if ( lValue1 > lValue0 + DelayInv + p->fEpsilon )
+        lValue1 = lValue0 + DelayInv, Use = 1;
+    else
+        Use = 3;
+    // set the uses of the phases
+    Seq_NodeSetUses( pObj, Use );
+    // get the old arrival times
+    lValueOld0 = Seq_NodeGetLValueN(pObj);
+    lValueOld1 = Seq_NodeGetLValueP(pObj);
+    // compare 
+    if ( lValue0 <= lValueOld0 + p->fEpsilon && lValue1 <= lValueOld1 + p->fEpsilon )
+        return SEQ_UPDATE_NO;
+    // update the values
+    if ( lValue0 > lValueOld0 + p->fEpsilon )
+        Seq_NodeSetLValueN( pObj, lValue0 );
+    if ( lValue1 > lValueOld1 + p->fEpsilon )
+        Seq_NodeSetLValueP( pObj, lValue1 );
+    return SEQ_UPDATE_YES;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the parameters of the best mapping/retiming for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMapping, Vec_Vec_t * vMapCuts )
+{
+    Seq_Match_t * pMatch;
+    Abc_Obj_t * pFanin;
+    int k, fCompl, Use;
+    float Area;
+
+    // get the polarity of the node
+    fCompl = Abc_ObjIsComplement(pAnd);
+    pAnd   = Abc_ObjRegular(pAnd);
+
+    // skip visited nodes
+    if ( fCompl )
+    {
+        if ( pAnd->fMarkB )
+            return 0.0;
+        pAnd->fMarkB = 1;
+    }
+    else
+    {
+        if ( pAnd->fMarkA )
+            return 0.0;
+        pAnd->fMarkA = 1;
+    }
+
+    // skip if this is a non-PI node
+    if ( !Abc_NodeIsAigAnd(pAnd) )
+    {
+        if ( Abc_ObjIsPi(pAnd) && fCompl )
+            return Mio_LibraryReadAreaInv(Abc_FrameReadLibGen());   
+        return 0.0;
+    }
+
+    // check the uses of this node
+    Use = Seq_NodeGetUses( pAnd );
+    if ( fCompl && Use == 2 )  // the neg phase is required; the pos phase is used
+    {
+        Area = Seq_MapCollectNode_rec( pAnd, FiBest, vMapping, vMapCuts );
+        return Area + Mio_LibraryReadAreaInv(Abc_FrameReadLibGen()); 
+    }
+    if ( !fCompl && Use == 1 )  // the pos phase is required; the neg phase is used
+    {
+        Area = Seq_MapCollectNode_rec( Abc_ObjNot(pAnd), FiBest, vMapping, vMapCuts );
+        return Area + Mio_LibraryReadAreaInv(Abc_FrameReadLibGen()); 
+    }
+
+    // get the best match
+    pMatch = ALLOC( Seq_Match_t, 1 );
+    Seq_MapNodeComputePhase( pAnd, fCompl, FiBest, pMatch );
+    pMatch->pAnd    = pAnd;
+    pMatch->fCompl  = fCompl;
+    pMatch->fCutInv = pMatch->pCut->fCompl;
+    pMatch->PolUse  = Use;
+
+    // call for the fanin cuts
+    Area = pMatch->pSuper->Area;
+    for ( k = 0; k < (int)pMatch->pCut->nLeaves; k++ )
+    {
+        pFanin = Abc_NtkObj( pAnd->pNtk, pMatch->pCut->pLeaves[k] >> 8 );
+        if ( pMatch->uPhase & (1 << k) )
+            pFanin = Abc_ObjNot( pFanin ); 
+        Area += Seq_MapCollectNode_rec( pFanin, FiBest, vMapping, vMapCuts );
+    }
+
+    // add this node
+    Vec_PtrPush( vMapping, pMatch );
+    for ( k = 0; k < (int)pMatch->pCut->nLeaves; k++ )
+        Vec_VecPush( vMapCuts, Vec_PtrSize(vMapping)-1, (void *)pMatch->pCut->pLeaves[k] );
+
+    return Area;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the canonical versions of the truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_MapCanonicizeTruthTables( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    Cut_Cut_t * pCut, * pList;
+    int i;
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj );
+        for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
+            Cut_TruthCanonicize( pCut );
+    }
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index 373e77bd..c746f9a4 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    [The core of retiming procedures.]
+  Synopsis    [The core of FPGA mapping/retiming package.]
 
   Author      [Alan Mishchenko]
   
@@ -19,36 +19,17 @@
 ***********************************************************************/
 
 #include "seqInt.h"
+#include "dec.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 );
-  
+static Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk );
+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 );
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -56,7 +37,7 @@ static void        Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches );
 
 /**Function*************************************************************
 
-  Synopsis    [Performs performs optimal delay retiming.]
+  Synopsis    [Performs FPGA mapping and retiming.]
 
   Description []
                
@@ -65,148 +46,31 @@ static void        Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches );
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fInitial, int fVerbose )
+Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
 {
-    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Seq_t * p;
+    Abc_Ntk_t * pNtkAig, * pNtkNew;
     int RetValue;
-    if ( !fInitial )
-        Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC );
-    // get the retiming lags
-    Seq_NtkRetimeDelayLags( pNtk, fVerbose );
-    // implement this retiming
-    RetValue = Seq_NtkImplementRetiming( pNtk, p->vLags, fVerbose );
+    assert( !Abc_NtkHasAig(pNtk) );
+    // derive the isomorphic seq AIG
+    pNtkAig = Seq_NtkRetimeDerive( pNtk );
+    p = pNtkAig->pManFunc;
+    p->nMaxIters = nMaxIters;
+    // find the best mapping and retiming 
+    Seq_NtkRetimeDelayLags( pNtk, pNtkAig, fVerbose );
+    // implement the retiming
+    RetValue = Seq_NtkImplementRetiming( pNtkAig, p->vLags, fVerbose );
     if ( RetValue == 0 )
         printf( "Retiming completed but initial state computation has failed.\n" );
+    // create the final mapped network
+    pNtkNew = Seq_NtkRetimeReconstruct( pNtk, pNtkAig );
+    Abc_NtkDelete( pNtkAig );
+    return pNtkNew;
 }
 
 /**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.]
+  Synopsis    [Derives the isomorphic seq AIG.]
 
   Description []
                
@@ -215,347 +79,118 @@ void Seq_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_ObjRetimeForward( Abc_Obj_t * pObj )  
-{
-    Abc_Obj_t * pFanout;
-    int Init0, Init1, Init, i;
-    assert( Abc_ObjFaninNum(pObj) == 2 );
-    assert( Seq_ObjFaninL0(pObj) >= 1 );
-    assert( Seq_ObjFaninL1(pObj) >= 1 );
-    // remove the init values from the fanins
-    Init0 = Seq_NodeDeleteFirst( pObj, 0 ); 
-    Init1 = Seq_NodeDeleteFirst( pObj, 1 );
-    assert( Init0 != ABC_INIT_NONE );
-    assert( Init1 != ABC_INIT_NONE );
-    // take into account the complements in the node
-    if ( Abc_ObjFaninC0(pObj) )
-    {
-        if ( Init0 == ABC_INIT_ZERO )
-            Init0 = ABC_INIT_ONE;
-        else if ( Init0 == ABC_INIT_ONE )
-            Init0 = ABC_INIT_ZERO;
-    }
-    if ( Abc_ObjFaninC1(pObj) )
-    {
-        if ( Init1 == ABC_INIT_ZERO )
-            Init1 = ABC_INIT_ONE;
-        else if ( Init1 == ABC_INIT_ONE )
-            Init1 = ABC_INIT_ZERO;
-    }
-    // compute the value at the output of the node
-    if ( Init0 == ABC_INIT_ZERO || Init1 == ABC_INIT_ZERO )
-        Init = ABC_INIT_ZERO;
-    else if ( Init0 == ABC_INIT_ONE && Init1 == ABC_INIT_ONE )
-        Init = ABC_INIT_ONE;
-    else
-        Init = ABC_INIT_DC;
-
-    // make sure the label is clean
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        assert( pFanout->fMarkC == 0 );
-    // add the init values to the fanouts
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-    {
-        if ( pFanout->fMarkC )
-            continue;
-        pFanout->fMarkC = 1;
-        if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) )
-            Seq_NodeInsertLast( pFanout, Abc_ObjFanoutEdgeNum(pObj, pFanout), Init );
-        else
-        {
-            assert( Abc_ObjFanin0(pFanout) == pObj );
-            Seq_NodeInsertLast( pFanout, 0, Init );
-            Seq_NodeInsertLast( pFanout, 1, Init );
-        }
-    }
-    // clean the label
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        pFanout->fMarkC = 0;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Implements the given retiming on the sequential AIG.]
-
-  Description [Returns 0 of initial state computation fails.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int fVerbose )
+Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
 {
-    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 ) )
+    Abc_Seq_t * p;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pFanin, * pFanout;
+    int i, k, RetValue;
+    char * pSop;
+
+    // make sure it is an AIG without self-feeding latches
+    assert( !Abc_NtkHasAig(pNtk) );
+    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) )
+        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+    assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
+
+    if ( 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_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
+
+    // create one AND for each logic node
+    Abc_NtkForEachNode( pNtk, pObj, i )
     {
-        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;
+        pObj->pCopy = Abc_NtkCreateNode( pNtkNew );
+        pObj->pCopy->pCopy = pObj;
     }
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
 
-    // check if conflict is found
-    if ( RetValue )
+    // create internal AND nodes w/o strashing for each logic node (including constants)
+    Abc_NtkForEachNode( pNtk, pObj, i )
     {
-        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" );
+        // get the SOP of the node
+        if ( Abc_NtkHasMapping(pNtk) )
+            pSop = Mio_GateReadSop(pObj->pData);
         else
-            printf( "Seq_NtkImplementRetimingBackward: The SAT problem timed out. DC latch values are used.\n" );
-        stmm_free_table( tTable );
-        return 0;
+            pSop = pObj->pData;
+        pFanin = Seq_NodeRetimeDerive( pNtkNew, pObj, pSop );
+        Abc_ObjAddFanin( pObj->pCopy, pFanin );
+        Abc_ObjAddFanin( pObj->pCopy, pFanin );
     }
 
-    // set the values of the latches
-    Abc_NtkRetimeSetInitialValues( pNtk, tTable, pModel );
-    stmm_free_table( tTable );
-    free( pModel );
-    return 1;
-}
+    // connect the POs...
 
-/**Function*************************************************************
+    
+    // start the storage for initial states
+    p = pNtkNew->pManFunc;
+    Seq_Resize( p, Abc_NtkObjNumMax(pNtkNew) );
 
-  Synopsis    [Retimes node backward by one latch.]
+    // 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) );
 
-  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 )
+    // collect the nodes in the topological order
+    p->vMapAnds   = Abc_NtkDfs( pNtk, 0 );
+    p->vMapCuts   = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
+    p->vMapDelays = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
     {
-        if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
+        // change the node to be the new one
+        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
+        // collect the new fanins of this node
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Vec_VecPush( p->vMapCuts, i, pFanin->pCopy );
+        // collect the delay info
+        if ( !Abc_NtkHasMapping(pNtk) )
         {
-            Init = Seq_NodeGetInitLast( pFanout, 0 );
-            if ( Init == ABC_INIT_ZERO )
-                fMet0 = 1;
-            else if ( Init == ABC_INIT_ONE )
-                fMet1 = 1;
-            else if ( Init == ABC_INIT_NONE )
-                fMetN = 1;
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                Vec_VecPush( p->vMapDelays, i, (void *)Abc_Float2Int(1.0) );
         }
-        if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
-        {
-            Init = Seq_NodeGetInitLast( pFanout, 1 );
-            if ( Init == ABC_INIT_ZERO )
-                fMet0 = 1;
-            else if ( Init == ABC_INIT_ONE )
-                fMet1 = 1;
-            else if ( Init == ABC_INIT_NONE )
-                fMetN = 1;
-        }
-    }
-
-    // consider the case when all fanout latches have don't-care values
-    // the new values on the fanin edges will be don't-cares
-    if ( !fMet0 && !fMet1 && !fMetN )
-    {
-        // make sure the label is clean
-        Abc_ObjForEachFanout( pObj, pFanout, i )
-            assert( pFanout->fMarkC == 0 );
-        // update the fanout edges
-        Abc_ObjForEachFanout( pObj, pFanout, i )
-        {
-            if ( pFanout->fMarkC )
-                continue;
-            pFanout->fMarkC = 1;
-            if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
-                Seq_NodeDeleteLast( pFanout, 0 );
-            if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
-                Seq_NodeDeleteLast( pFanout, 1 );
-        }
-        // clean the label
-        Abc_ObjForEachFanout( pObj, pFanout, i )
-            pFanout->fMarkC = 0;
-        // update the fanin edges
-        Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable );
-        Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable );
-        Seq_NodeInsertFirst( pObj, 0, ABC_INIT_DC );
-        Seq_NodeInsertFirst( pObj, 1, ABC_INIT_DC );
-        return 0;
-    }
-    // the initial values on the fanout edges contain 0, 1, or unknown
-    // the new values on the fanin edges will be unknown
-
-    // add new AND-gate to the network
-    pNodeNew = Abc_NtkCreateNode( pNtkNew );
-    pNodeNew->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
-
-    // add PO fanouts if any
-    if ( fMet0 )
-    {
-        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
-        Vec_IntPush( vValues, 0 );
-    }
-    if ( fMet1 )
-    {
-        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
-        Vec_IntPush( vValues, 1 );
-    }
-
-    // make sure the label is clean
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        assert( pFanout->fMarkC == 0 );
-    // perform the changes
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-    {
-        if ( pFanout->fMarkC )
-            continue;
-        pFanout->fMarkC = 1;
-        if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
-        {
-            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 ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
+        else
         {
-            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 );
+            Mio_Pin_t * pPin = Mio_GateReadPins(pObj->pData);
+            float Max, tDelayBlockRise, tDelayBlockFall;
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+            {
+                tDelayBlockRise = (float)Mio_PinReadDelayBlockRise( pPin );  
+                tDelayBlockFall = (float)Mio_PinReadDelayBlockFall( pPin ); 
+                Max = ABC_MAX( tDelayBlockRise, tDelayBlockFall );
+                Vec_VecPush( p->vMapDelays, i, (void *)Abc_Float2Int(Max) );
+                pPin = Mio_PinReadNext(pPin);
+            }
         }
     }
-    // clean the label
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        pFanout->fMarkC = 0;
-
-    // update the fanin edges
-    Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable );
-    Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable );
-    Seq_NodeInsertFirst( pObj, 0, ABC_INIT_NONE );
-    Seq_NodeInsertFirst( pObj, 1, ABC_INIT_NONE );
-
-    // add the buffer
-    pBuffer = Abc_NtkCreateNode( pNtkNew );
-    pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
-    Abc_ObjAddFanin( pNodeNew, pBuffer );
-    // point to it from the table
-    RetEdge.iNode  = pObj->Id;
-    RetEdge.iEdge  = 0;
-    RetEdge.iLatch = 0;
-    if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pBuffer ) )
-        assert( 0 );
 
-    // add the buffer
-    pBuffer = Abc_NtkCreateNode( pNtkNew );
-    pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
-    Abc_ObjAddFanin( pNodeNew, pBuffer );
-    // point to it from the table
-    RetEdge.iNode  = pObj->Id;
-    RetEdge.iEdge  = 1;
-    RetEdge.iLatch = 0;
-    if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pBuffer ) )
-        assert( 0 );
+    // set the cutset composed of latch drivers
+//    Abc_NtkAigCutsetCopy( pNtk );
+    Seq_NtkLatchGetEqualFaninNum( pNtkNew );
 
-    // report conflict is found
-    return fMet0 && fMet1;
+    // 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, "Seq_NtkRetimeDerive(): Network check has failed.\n" );
+    return pNtkNew;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Generates the printable edge label with the initial state.]
+  Synopsis    [Add sequential edges.]
 
   Description []
                
@@ -564,37 +199,27 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable )
+void Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init )
 {
-    Abc_Obj_t * pFanoutNew;
-    Seq_RetEdge_t RetEdge;
-    Abc_InitType_t Init;
-    int nLatches, i;
-
-    // get the number of latches on the edge
-    nLatches = Seq_ObjFaninL( pObj, Edge );
-    for ( i = nLatches - 1; i >= 0; i-- )
-    {
-        // get the value of this latch
-        Init = Seq_NodeGetInitOne( pObj, Edge, i );
-        if ( Init != ABC_INIT_NONE )
-            continue;
-        // get the retiming edge
-        RetEdge.iNode  = pObj->Id;
-        RetEdge.iEdge  = Edge;
-        RetEdge.iLatch = i;
-        // remove entry from table and add it with a different key
-        if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
-            assert( 0 );
-        RetEdge.iLatch++;
-        if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pFanoutNew ) )
-            assert( 0 );
-    }
+    Abc_Obj_t * pFanin;
+    // consider the first fanin
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        Seq_NodeAddEdges_rec( pGoal, pFanin, Init );
+    else if ( pFanin == pGoal )
+        Seq_NodeInsertFirst( pNode, 0, Init );
+    // consider the second fanin
+    pFanin = Abc_ObjFanin1(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        Seq_NodeAddEdges_rec( pGoal, pFanin, Init );
+    else if ( pFanin == pGoal )
+        Seq_NodeInsertFirst( pNode, 1, Init );
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Sets the initial values.]
+  Synopsis    [Strashes one logic node using its SOP.]
 
   Description []
                
@@ -603,29 +228,45 @@ void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * t
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel )
+Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop )
 {
-    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 )
+    Dec_Graph_t * pFForm;
+    Dec_Node_t * pNode;
+    Abc_Obj_t * pAnd;
+    int i, nFanins;
+
+    // get the number of node's fanins
+    nFanins = Abc_ObjFaninNum( pRoot );
+    assert( nFanins == Abc_SopGetVarNum(pSop) );
+    if ( nFanins < 2 )
     {
-        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++;
+        if ( Abc_SopIsConst1(pSop) )
+            return Abc_NtkConst1(pNtkNew);
+        else if ( Abc_SopIsConst0(pSop) )
+            return Abc_ObjNot( Abc_NtkConst1(pNtkNew) );
+        else if ( Abc_SopIsBuf(pSop) )
+            return Abc_ObjFanin0(pRoot)->pCopy;
+        else if ( Abc_SopIsInv(pSop) )
+            return Abc_ObjNot( Abc_ObjFanin0(pRoot)->pCopy );
+        assert( 0 );
+        return NULL;
     }
-}
 
+    // perform factoring
+    pFForm = Dec_Factor( pSop );
+    // collect the fanins
+    Dec_GraphForEachLeaf( pFForm, pNode, i )
+        pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy;
+    // perform strashing
+    pAnd = Dec_GraphToNetworkNoStrash( pNtkNew, pFForm );
+    Dec_GraphFree( pFForm );
+    return pAnd;
+}
 
 
 /**Function*************************************************************
 
-  Synopsis    [Performs forward retiming of the sequential AIG.]
+  Synopsis    [Reconstructs the network after retiming.]
 
   Description []
                
@@ -634,333 +275,66 @@ void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int *
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward )
+Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk )
 {
-    Vec_Ptr_t * vNodes, * vMoves;
-    Abc_Obj_t * pNode, * pFanout, * pFanin;
-    int i, k, nLatches;
-    assert( Abc_NtkIsSeq( pNtk ) );
-    // assume that all nodes can be retimed
-    vNodes = Vec_PtrAlloc( 100 );
-    Abc_AigForEachAnd( pNtk, pNode, i )
-    {
-        Vec_PtrPush( vNodes, pNode );
-        pNode->fMarkA = 1;
-    }
-    // process the nodes
-    vMoves = Vec_PtrAlloc( 100 );
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-//        printf( "(%d,%d) ", Seq_ObjFaninL0(pNode), Seq_ObjFaninL0(pNode) );
-        // unmark the node as processed
-        pNode->fMarkA = 0;
-        // get the number of latches to retime
-        if ( fForward )
-            nLatches = Seq_ObjFaninLMin(pNode);
-        else
-            nLatches = Seq_ObjFanoutLMin(pNode);
-        if ( nLatches == 0 )
-            continue;
-        assert( nLatches > 0 );
-        // retime the latches forward
-        if ( fForward )
-            Abc_ObjRetimeForwardTry( pNode, nLatches );
-        else
-            Abc_ObjRetimeBackwardTry( pNode, nLatches );
-        // write the moves
-        for ( k = 0; k < nLatches; k++ )
-            Vec_PtrPush( vMoves, pNode );
-        // schedule fanouts for updating
-        if ( fForward )
-        {
-            Abc_ObjForEachFanout( pNode, pFanout, k )
-            {
-                if ( Abc_ObjFaninNum(pFanout) != 2 || pFanout->fMarkA )
-                    continue;
-                pFanout->fMarkA = 1;
-                Vec_PtrPush( vNodes, pFanout );
-            }
-        }
-        else
-        {
-            Abc_ObjForEachFanin( pNode, pFanin, k )
-            {
-                if ( Abc_ObjFaninNum(pFanin) != 2 || pFanin->fMarkA )
-                    continue;
-                pFanin->fMarkA = 1;
-                Vec_PtrPush( vNodes, pFanin );
-            }
-        }
-    }
-    Vec_PtrFree( vNodes );
-    // make sure the marks are clean the the retiming is final
-    Abc_AigForEachAnd( pNtk, pNode, i )
-    {
-        assert( pNode->fMarkA == 0 );
-        if ( fForward ) 
-            assert( Seq_ObjFaninLMin(pNode) == 0 );
-        else
-            assert( Seq_ObjFanoutLMin(pNode) == 0 );
-    }
-    return vMoves;
-}
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Seq_Lat_t * pRing;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pFaninNew, * pObjNew;
+    int i;
 
-/**Function*************************************************************
+    assert( !Abc_NtkIsSeq(pNtkOld) );
+    assert( Abc_NtkIsSeq(pNtk) );
 
-  Synopsis    [Translates retiming steps into retiming moves.]
+    // start the final network
+    pNtkNew = Abc_NtkStartFrom( pNtk, pNtkOld->ntkType, pNtkOld->ntkFunc );
 
-  Description []
-               
-  SideEffects []
+    // copy the internal nodes
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj );
 
-  SeeAlso     []
+    // share the latches
+    Seq_NtkShareLatches( pNtkNew, pNtk );
 
-***********************************************************************/
-Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, bool fForward )
-{
-    Seq_RetStep_t RetStep;
-    Vec_Ptr_t * vMoves;
-    Abc_Obj_t * pNode;
-    int i, k, iNode, nLatches, Number;
-    int fChange;
-    assert( Abc_NtkIsSeq( pNtk ) );
-
-/*
-    // try implementing all the moves at once
-    Vec_IntForEachEntry( vSteps, Number, i )
+    // connect the objects
+    Abc_AigForEachAnd( pNtk, pObj, i )
     {
-        // get the retiming step
-        RetStep = Seq_Int2RetStep( Number );
-        // get the node to be retimed
-        pNode = Abc_NtkObj( pNtk, RetStep.iNode );
-        assert( RetStep.nLatches > 0 );
-        nLatches = RetStep.nLatches;
-
-        if ( fForward )
-            Abc_ObjRetimeForwardTry( pNode, nLatches );
+        if ( pRing = Seq_NodeGetRing(pObj,0) )
+            pFaninNew = pRing->pLatch;
         else
-            Abc_ObjRetimeBackwardTry( pNode, nLatches );
-    }
-    // now look if any node has wrong number of latches
-    Abc_AigForEachAnd( pNtk, pNode, i )
-    {
-        if ( Seq_ObjFaninL0(pNode) < 0 )
-            printf( "Wrong 0node %d.\n", pNode->Id );
-        if ( Seq_ObjFaninL1(pNode) < 0 )
-            printf( "Wrong 1node %d.\n", pNode->Id );
-    }
-    // try implementing all the moves at once
-    Vec_IntForEachEntry( vSteps, Number, i )
-    {
-        // get the retiming step
-        RetStep = Seq_Int2RetStep( Number );
-        // get the node to be retimed
-        pNode = Abc_NtkObj( pNtk, RetStep.iNode );
-        assert( RetStep.nLatches > 0 );
-        nLatches = RetStep.nLatches;
-
-        if ( !fForward )
-            Abc_ObjRetimeForwardTry( pNode, nLatches );
-        else
-            Abc_ObjRetimeBackwardTry( pNode, nLatches );
-    }
-*/
+            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
 
-    // process the nodes
-    vMoves = Vec_PtrAlloc( 100 );
-    while ( Vec_IntSize(vSteps) > 0 )
-    {
-        iNode = 0;
-        fChange = 0;
-        Vec_IntForEachEntry( vSteps, Number, i )
-        {
-            // get the retiming step
-            RetStep = Seq_Int2RetStep( Number );
-            // get the node to be retimed
-            pNode = Abc_NtkObj( pNtk, RetStep.iNode );
-            assert( RetStep.nLatches > 0 );
-            // get the number of latches that can be retimed
-            if ( fForward )
-                nLatches = Seq_ObjFaninLMin(pNode);
-            else
-                nLatches = Seq_ObjFanoutLMin(pNode);
-            if ( nLatches == 0 )
-            {
-                Vec_IntWriteEntry( vSteps, iNode++, Seq_RetStep2Int(RetStep) );
-                continue;
-            }
-            assert( nLatches > 0 );
-            fChange = 1;
-            // get the number of latches to be retimed over this node
-            nLatches = ABC_MIN( nLatches, (int)RetStep.nLatches );
-            // retime the latches forward
-            if ( fForward )
-                Abc_ObjRetimeForwardTry( pNode, nLatches );
-            else
-                Abc_ObjRetimeBackwardTry( pNode, nLatches );
-            // write the moves
-            for ( k = 0; k < nLatches; k++ )
-                Vec_PtrPush( vMoves, pNode );
-            // subtract the retiming performed
-            RetStep.nLatches -= nLatches;
-            // store the node if it is not retimed completely
-            if ( RetStep.nLatches > 0 )
-                Vec_IntWriteEntry( vSteps, iNode++, Seq_RetStep2Int(RetStep) );
-        }
-        // reduce the array
-        Vec_IntShrink( vSteps, iNode );
-        if ( !fChange )
-        {
-            printf( "Warning: %d strange steps (a minor bug to be fixed later).\n", Vec_IntSize(vSteps) );
-/*            
-            Vec_IntForEachEntry( vSteps, Number, i )
-            {
-                RetStep = Seq_Int2RetStep( Number );
-                printf( "%d(%d) ", RetStep.iNode, RetStep.nLatches );
-            }
-            printf( "\n" );
-*/            
-            break;
-        }
-    }
-    // undo the tentative retiming
-    if ( fForward )
-    {
-        Vec_PtrForEachEntryReverse( vMoves, pNode, i )
-            Abc_ObjRetimeBackwardTry( pNode, 1 );
-    }
-    else
-    {
-        Vec_PtrForEachEntryReverse( vMoves, pNode, i )
-            Abc_ObjRetimeForwardTry( pNode, 1 );
-    }
-    return vMoves;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Splits retiming into forward and backward.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward )
-{
-    Vec_Int_t * vNodes;
-    Seq_RetStep_t RetStep;
-    int Value, i;
-    vNodes = Vec_IntAlloc( 100 );
-    Vec_StrForEachEntry( vLags, Value, i )
-    {
-        if ( Value < 0 && fForward )
-        {
-            RetStep.iNode = i;
-            RetStep.nLatches = -Value;
-            Vec_IntPush( vNodes, Seq_RetStep2Int(RetStep) );
-        }
-        else if ( Value > 0 && !fForward )
-        {
-            RetStep.iNode = i;
-            RetStep.nLatches = Value;
-            Vec_IntPush( vNodes, Seq_RetStep2Int(RetStep) );
-        }
+        if ( pRing = Seq_NodeGetRing(pObj,1) )
+            pFaninNew = pRing->pLatch;
+        else
+            pFaninNew = Abc_ObjFanin1(pObj)->pCopy;
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
     }
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Retime node forward without initial states.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_ObjRetimeForwardTry( Abc_Obj_t * pObj, int nLatches )  
-{
-    Abc_Obj_t * pFanout;
-    int i;
-    // make sure it is an AND gate
-    assert( Abc_ObjFaninNum(pObj) == 2 );
-    // make sure it has enough latches
-//    assert( Seq_ObjFaninL0(pObj) >= nLatches );
-//    assert( Seq_ObjFaninL1(pObj) >= nLatches );
-    // subtract these latches on the fanin side
-    Seq_ObjAddFaninL0( pObj, -nLatches );
-    Seq_ObjAddFaninL1( pObj, -nLatches );
-    // make sure the label is clean
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        assert( pFanout->fMarkC == 0 );
-    // add these latches on the fanout side
-    Abc_ObjForEachFanout( pObj, pFanout, i )
+    // connect the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
     {
-        if ( pFanout->fMarkC )
-            continue;
-        pFanout->fMarkC = 1;
-        if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) )
-            Seq_ObjAddFanoutL( pObj, pFanout, nLatches );
+        if ( pRing = Seq_NodeGetRing(pObj,0) )
+            pFaninNew = pRing->pLatch;
         else
-        {
-            assert( Abc_ObjFanin0(pFanout) == pObj );
-            Seq_ObjAddFaninL0( pFanout, nLatches );
-            Seq_ObjAddFaninL1( pFanout, nLatches );
-        }
+            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
+        pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
     }
-    // clean the label
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        pFanout->fMarkC = 0;
-}
-
-/**Function*************************************************************
 
-  Synopsis    [Retime node backward without initial states.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches )  
-{
-    Abc_Obj_t * pFanout;
-    int i;
-    // make sure it is an AND gate
-    assert( Abc_ObjFaninNum(pObj) == 2 );
-    // make sure the label is clean
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        assert( pFanout->fMarkC == 0 );
-    // subtract these latches on the fanout side
-    Abc_ObjForEachFanout( pObj, pFanout, i )
+    // add the latches and their names
+    Abc_NtkAddDummyLatchNames( pNtkNew );
+    Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
     {
-        if ( pFanout->fMarkC )
-            continue;
-        pFanout->fMarkC = 1;
-//        assert( Abc_ObjFanoutL(pObj, pFanout) >= nLatches );
-        if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) )
-            Seq_ObjAddFanoutL( pObj, pFanout, -nLatches );
-        else
-        {
-            assert( Abc_ObjFanin0(pFanout) == pObj );
-            Seq_ObjAddFaninL0( pFanout, -nLatches );
-            Seq_ObjAddFaninL1( pFanout, -nLatches );
-        }
+        Vec_PtrPush( pNtkNew->vCis, pObjNew );
+        Vec_PtrPush( pNtkNew->vCos, pObjNew );
     }
-    // clean the label
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        pFanout->fMarkC = 0;
-    // add these latches on the fanin side
-    Seq_ObjAddFaninL0( pObj, nLatches );
-    Seq_ObjAddFaninL1( pObj, nLatches );
+    // 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;
+
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqRetIter.c b/src/base/seq/seqRetIter.c
index 6f7a320a..5c65e72e 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    [The iterative L-Value computation for retiming procedures.]
+  Synopsis    [Iterative delay computation in FPGA mapping/retiming package.]
 
   Author      [Alan Mishchenko]
   
@@ -19,15 +19,17 @@
 ***********************************************************************/
 
 #include "seqInt.h"
+#include "main.h"
+#include "fpga.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-// the internal procedures
-static int Seq_RetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose );
-static int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose );
-static int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
+static float Seq_NtkMappingSearch_rec( Abc_Ntk_t * pNtk, float FiMin, float FiMax, float Delta, int fVerbose );
+static int   Seq_NtkMappingForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose );
+static int   Seq_NtkNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vDelays );
+static void  Seq_NodeRetimeSetLag_rec( Abc_Obj_t * pNode, char Lag );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -35,7 +37,7 @@ static int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
 
 /**Function*************************************************************
 
-  Synopsis    [Retimes AIG for optimal delay using Pan's algorithm.]
+  Synopsis    [Computes the retiming lags for arbitrary network.]
 
   Description []
                
@@ -44,73 +46,67 @@ static int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
+void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
     Abc_Obj_t * pNode;
-    int i, FiMax, FiBest, RetValue;
+    float FiMax, FiBest, Delta;
+    int i, RetValue;
     char NodeLag;
 
     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;
+    // the root AND gates and node delay should be assigned
+    assert( p->vMapAnds );
+    assert( p->vMapCuts );
+    assert( p->vMapDelays );
+
+    // guess the upper bound on the clock period
+    if ( Abc_NtkHasMapping(pNtkOld) )
+    {
+        // assign the accuracy for min-period computation
+        Delta = Mio_LibraryReadDelayNand2Max(Abc_FrameReadLibGen());
+        if ( Delta == 0.0 )
+        {
+            Delta = Mio_LibraryReadDelayAnd2Max(Abc_FrameReadLibGen());
+            if ( Delta == 0.0 )
+            {
+                printf( "Cannot retime/map if the library does not have NAND2 or AND2.\n" );
+                return;
+            }
+        }
+        // get the upper bound on the clock period
+        FiMax = Delta * (2 + Seq_NtkLevelMax(pNtk));
+        Delta /= 2;
+    }
+    else
+    {
+        FiMax = (float)2.0 + Abc_NtkGetLevelNum(pNtkOld);
+        Delta = 1;
+    }
 
     // make sure this clock period is feasible
-    assert( Seq_RetimeForPeriod( pNtk, FiMax, fVerbose ) );
+    assert( Seq_NtkMappingForPeriod( pNtk, FiMax, fVerbose ) );
 
     // search for the optimal clock period between 0 and nLevelMax
-    FiBest = Seq_RetimeSearch_rec( pNtk, 0, FiMax, fVerbose );
+    FiBest = Seq_NtkMappingSearch_rec( pNtk, 0.0, FiMax, Delta, fVerbose );
 
     // recompute the best l-values
-    RetValue = Seq_RetimeForPeriod( pNtk, FiBest, fVerbose );
+    RetValue = Seq_NtkMappingForPeriod( pNtk, FiBest, fVerbose );
     assert( RetValue );
 
-    // write the retiming lags
-    Vec_StrFill( p->vLags, p->nSize, 0 );
-    Abc_AigForEachAnd( pNtk, pNode, i )
-    {
-        NodeLag = Seq_NodeComputeLag( Seq_NodeGetLValue(pNode), FiBest );
-        Seq_NodeSetLag( pNode, NodeLag );
-    }
-/*
+    // write the retiming lags for both phases of each node
+    Vec_StrFill( p->vLags,  p->nSize, 0 );
+    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
     {
-        Abc_Obj_t * pFanin, * pFanout;
-        pNode = Abc_NtkObj( pNtk, 823 );
-        printf( "Node  %d.  Lag = %d. LValue = %d. Latches = (%d,%d) (%d,%d).\n", pNode->Id, Seq_NodeGetLag(pNode), Seq_NodeGetLValue(pNode), 
-            Seq_ObjFaninL0(pNode), Seq_ObjFaninL1(pNode), Seq_ObjFanoutL(pNode, Abc_NtkObj(pNtk, 826)), Seq_ObjFanoutL(pNode, Abc_NtkObj(pNtk, 1210)) );
-        pFanin = Abc_ObjFanin0( pNode );
-        printf( "Fanin %d.  Lag = %d. LValue = %d. Latches = (%d,%d)\n", pFanin->Id, Seq_NodeGetLag(pFanin), Seq_NodeGetLValue(pFanin),
-            Seq_ObjFaninL0(pFanin), Seq_ObjFaninL1(pFanin) );
-        pFanin = Abc_ObjFanin1( pNode );
-        printf( "Fanin %d.  Lag = %d. LValue = %d.\n", pFanin->Id, Seq_NodeGetLag(pFanin), Seq_NodeGetLValue(pFanin) );
-        Abc_ObjForEachFanout( pNode, pFanout, i )
-            printf( "Fanout %d.  Lag = %d. LValue = %d.\n", pFanout->Id, Seq_NodeGetLag(pFanout), Seq_NodeGetLValue(pFanout) );
-        Abc_ObjForEachFanout( Abc_ObjFanin0(pNode), pFanout, i )
-            printf( "Fanout %d.  Lag = %d. LValue = %d.\n", pFanout->Id, Seq_NodeGetLag(pFanout), Seq_NodeGetLValue(pFanout) );
+        NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueP(pNode), FiBest );
+//        Seq_NodeSetLag( pNode, NodeLag );
+        Seq_NodeRetimeSetLag_rec( pNode, NodeLag );
     }
-*/
 
     // 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" );
-*/
+        printf( "The best clock period is %6.2f.\n", FiBest );
 }
 
 /**Function*************************************************************
@@ -124,17 +120,17 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Seq_RetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose )
+float Seq_NtkMappingSearch_rec( Abc_Ntk_t * pNtk, float FiMin, float FiMax, float Delta, int fVerbose )
 {
-    int Median;
+    float Median;
     assert( FiMin < FiMax );
-    if ( FiMin + 1 == FiMax )
+    if ( FiMin + Delta >= 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
+    if ( Seq_NtkMappingForPeriod( pNtk, Median, fVerbose ) )
+        return Seq_NtkMappingSearch_rec( pNtk, FiMin, Median, Delta, fVerbose ); // Median is feasible
     else 
-        return Seq_RetimeSearch_rec( pNtk, Median, FiMax, fVerbose ); // Median is infeasible
+        return Seq_NtkMappingSearch_rec( pNtk, Median, FiMax, Delta, fVerbose ); // Median is infeasible
 }
 
 /**Function*************************************************************
@@ -148,78 +144,63 @@ int Seq_RetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose )
+int Seq_NtkMappingForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
+    Vec_Ptr_t * vLeaves, * vDelays;
     Abc_Obj_t * pObj;
-    int nMaxSteps = 10;
     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 );
+    Vec_IntFill( p->vLValues,  p->nSize, -ABC_INFINITY );
 
     // set l-values of constants and PIs
     pObj = Abc_NtkObj( pNtk, 0 );
-    Seq_NodeSetLValue( pObj, 0 );
+    Seq_NodeSetLValueP( pObj, 0.0 );
     Abc_NtkForEachPi( pNtk, pObj, i )
-        Seq_NodeSetLValue( pObj, 0 );
+        Seq_NodeSetLValueP( pObj, 0.0 );
 
     // update all values iteratively
     Counter = 0;
-    for ( c = 0; c < nMaxSteps; c++ )
+    for ( c = 0; c < p->nMaxIters; c++ )
     {
         fChange = 0;
-        Abc_AigForEachAnd( pNtk, pObj, i )
+        Vec_PtrForEachEntry( p->vMapAnds, 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;
-            if ( RetValue == SEQ_UPDATE_NO ) 
-                continue;
-            fChange = 1;
+            vLeaves = Vec_VecEntry( p->vMapCuts, i );
+            vDelays = Vec_VecEntry( p->vMapDelays, i );
+            RetValue = Seq_NtkNodeUpdateLValue( pObj, Fi, vLeaves, vDelays );
+            if ( RetValue == SEQ_UPDATE_YES ) 
+                fChange = 1;
         }
         Abc_NtkForEachPo( pNtk, pObj, i )
         {
-            if ( Seq_NodeCutMan(pObj) )
-                RetValue = Seq_FpgaNodeUpdateLValue( pObj, Fi );
-            else
-                RetValue = Seq_RetimeNodeUpdateLValue( pObj, Fi );
-//printf( "Node = %d. Value = %d. \n", pObj->Id, RetValue );
-            Counter++;
+            RetValue = Seq_NtkNodeUpdateLValue( pObj, Fi, NULL, NULL );
             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 == nMaxSteps )
+    if ( c == p->nMaxIters )
     {
         RetValue = SEQ_UPDATE_FAIL;
         pReason = "(timeout)";
     }
-
-//Abc_NtkForEachObj( pNtk, pObj, i )
-//printf( "%d ", Seq_NodeGetLValue(pObj) );
-//printf( "\n" );
+    else
+        c++;
 
     // report the results
     if ( fVerbose )
     {
         if ( RetValue == SEQ_UPDATE_FAIL )
-            printf( "Period = %3d.  Iterations = %3d.  Updates = %10d.    Infeasible %s\n", Fi, c, Counter, pReason );
+            printf( "Period = %6.2f.  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 = %6.2f.  Iterations = %3d.  Updates = %10d.      Feasible\n",    Fi, c, Counter );
     }
     return RetValue != SEQ_UPDATE_FAIL;
 }
@@ -235,27 +216,66 @@ int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
+int Seq_NtkNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vDelays )
 {
-    int lValueNew, lValueOld, lValue0, lValue1;
+    Abc_Seq_t * p = pObj->pNtk->pManFunc;
+    float lValueOld, lValueNew, lValueCur, lValuePin;
+    unsigned SeqEdge;
+    Abc_Obj_t * pLeaf;
+    int i;
+
     assert( !Abc_ObjIsPi(pObj) );
     assert( Abc_ObjFaninNum(pObj) > 0 );
-    lValue0 = Seq_NodeGetLValue(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj);
+    // consider the case of the PO
     if ( Abc_ObjIsPo(pObj) )
-        return (lValue0 > Fi)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO;
-    if ( Abc_ObjFaninNum(pObj) == 2 )
-        lValue1 = Seq_NodeGetLValue(Abc_ObjFanin1(pObj)) - Fi * Seq_ObjFaninL1(pObj);
-    else
-        lValue1 = -ABC_INFINITY;
-    lValueNew = 1 + ABC_MAX( lValue0, lValue1 );
-    lValueOld = Seq_NodeGetLValue(pObj);
-//    if ( lValueNew == lValueOld )
-    if ( lValueNew <= lValueOld )
+    {
+        lValueCur = Seq_NodeGetLValueP(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj);
+        return (lValueCur > Fi + p->fEpsilon)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO;
+    }
+    // get the new arrival time of the cut output
+    lValueNew = -ABC_INFINITY;
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        SeqEdge   = (unsigned)pLeaf;
+        pLeaf     = Abc_NtkObj( pObj->pNtk, SeqEdge >> 8 );
+        lValueCur = Seq_NodeGetLValueP(pLeaf) - Fi * (SeqEdge & 255);
+        lValuePin = Abc_Int2Float( (int)Vec_PtrEntry(vDelays, i) );
+        if ( lValueNew < lValuePin + lValueCur )
+            lValueNew = lValuePin + lValueCur;
+    }
+    // compare 
+    lValueOld = Seq_NodeGetLValueP( pObj );
+    if ( lValueNew <= lValueOld + p->fEpsilon )
         return SEQ_UPDATE_NO;
-    Seq_NodeSetLValue( pObj, lValueNew );
+    // update the values
+    if ( lValueNew > lValueOld + p->fEpsilon )
+        Seq_NodeSetLValueP( pObj, lValueNew );
     return SEQ_UPDATE_YES;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Add sequential edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodeRetimeSetLag_rec( Abc_Obj_t * pNode, char Lag )
+{
+    if ( pNode->pCopy )
+        return;
+    Seq_NodeRetimeSetLag_rec( Abc_ObjFanin0(pNode), Lag );
+    Seq_NodeRetimeSetLag_rec( Abc_ObjFanin1(pNode), Lag );
+    Seq_NodeSetLag( pNode, Lag );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqShare.c b/src/base/seq/seqShare.c
index 818dca23..5f5f1731 100644
--- a/src/base/seq/seqShare.c
+++ b/src/base/seq/seqShare.c
@@ -160,8 +160,188 @@ void Seq_NodeShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNode
         Abc_ObjPatchFanin( pFanout, pNode, pBuffer );
 }
 
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Maps virtual latches into real latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Seq_NtkShareLatchesKey( Abc_Obj_t * pObj, Abc_InitType_t Init )
+{
+    return (pObj->Id << 2) | Init;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Maps virtual latches into real latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_NtkShareLatches_rec( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj, Seq_Lat_t * pRing, int nLatch, stmm_table * tLatchMap )
+{
+    Abc_Obj_t * pLatch, * pFanin;
+    Abc_InitType_t Init;
+    unsigned Key;
+    if ( nLatch == 0 )
+        return pObj;
+    assert( pRing->pLatch == NULL );
+    // get the latch on the previous level
+    pFanin = Seq_NtkShareLatches_rec( pNtk, pObj, Seq_LatNext(pRing), nLatch - 1, tLatchMap );
+
+    // get the initial state
+    Init = Seq_LatInit( pRing );
+    // check if the latch with this initial state exists
+    Key = Seq_NtkShareLatchesKey( pFanin, Init );
+    if ( stmm_lookup( tLatchMap, (char *)Key, (char **)&pLatch ) )
+        return pRing->pLatch = pLatch;
+
+    // does not exist
+    if ( Init != ABC_INIT_DC )
+    {
+        // check if the don't-care exists
+        Key = Seq_NtkShareLatchesKey( pFanin, ABC_INIT_DC );
+        if ( stmm_lookup( tLatchMap, (char *)Key, (char **)&pLatch ) ) // yes
+        {
+            // update the table
+            stmm_delete( tLatchMap, (char **)&Key, (char **)&pLatch );
+            Key = Seq_NtkShareLatchesKey( pFanin, Init );
+            stmm_insert( tLatchMap, (char *)Key, (char *)pLatch );
+            // change don't-care to the given value
+            pLatch->pData = (void *)Init;
+            return pRing->pLatch = pLatch;
+        }
+
+        // add the latch with this value
+        pLatch = Abc_NtkCreateLatch( pNtk );
+        pLatch->pData = (void *)Init;
+        Abc_ObjAddFanin( pLatch, pFanin );
+        // add it to the table
+        Key = Seq_NtkShareLatchesKey( pFanin, Init );
+        stmm_insert( tLatchMap, (char *)Key, (char *)pLatch );
+        return pRing->pLatch = pLatch;
+    }
+    // the init value is the don't-care
+
+    // check if care values exist
+    Key = Seq_NtkShareLatchesKey( pFanin, ABC_INIT_ZERO );
+    if ( stmm_lookup( tLatchMap, (char *)Key, (char **)&pLatch ) )
+    {
+        Seq_LatSetInit( pRing, ABC_INIT_ZERO );
+        return pRing->pLatch = pLatch;
+    }
+    Key = Seq_NtkShareLatchesKey( pFanin, ABC_INIT_ONE );
+    if ( stmm_lookup( tLatchMap, (char *)Key, (char **)&pLatch ) )
+    {
+        Seq_LatSetInit( pRing, ABC_INIT_ONE );
+        return pRing->pLatch = pLatch;
+    }
+
+    // create the don't-care latch
+    pLatch = Abc_NtkCreateLatch( pNtk );
+    pLatch->pData = (void *)ABC_INIT_DC;
+    Abc_ObjAddFanin( pLatch, pFanin );
+    // add it to the table
+    Key = Seq_NtkShareLatchesKey( pFanin, ABC_INIT_DC );
+    stmm_insert( tLatchMap, (char *)Key, (char *)pLatch );
+    return pRing->pLatch = pLatch;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Maps virtual latches into real latches.]
+
+  Description [Creates new latches and assigns them to virtual latches
+  on the edges of a sequential AIG. The nodes of the new network should
+  be created before this procedure is called.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk )
+{ 
+    Abc_Obj_t * pObj;
+    stmm_table * tLatchMap;
+    int i;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    tLatchMap = stmm_init_table( stmm_ptrcmp, stmm_ptrhash );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        Seq_NtkShareLatches_rec( pNtkNew, Abc_ObjFanin0(pObj)->pCopy, Seq_NodeGetRing(pObj,0), Seq_NodeCountLats(pObj,0), tLatchMap );
+        Seq_NtkShareLatches_rec( pNtkNew, Abc_ObjFanin1(pObj)->pCopy, Seq_NodeGetRing(pObj,1), Seq_NodeCountLats(pObj,1), tLatchMap );
+    }
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_NtkShareLatches_rec( pNtkNew, Abc_ObjFanin0(pObj)->pCopy, Seq_NodeGetRing(pObj,0), Seq_NodeCountLats(pObj,0), tLatchMap );
+    stmm_free_table( tLatchMap );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Maps virtual latches into real latches.]
+
+  Description [Creates new latches and assigns them to virtual latches
+  on the edges of a sequential AIG. The nodes of the new network should
+  be created before this procedure is called.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds )
+{ 
+    Abc_Obj_t * pObj, * pFanout;
+    stmm_table * tLatchMap;
+    int i, k, nOldNodes;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    // start the table
+    tLatchMap = stmm_init_table( stmm_ptrcmp, stmm_ptrhash );
+    // remember the old nodes
+    nOldNodes = Vec_PtrSize( vMapAnds );
+    // add constant and PIs
+    Vec_PtrPush( vMapAnds, Abc_NtkConst1(pNtk) );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Vec_PtrPush( vMapAnds, pObj );
+    // process nodes used in the mapping
+    Vec_PtrForEachEntry( vMapAnds, pObj, i )
+    {
+        // make sure the label is clean
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            assert( pFanout->fMarkC == 0 );
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+        {
+            if ( pFanout->fMarkC )
+                continue;
+            pFanout->fMarkC = 1;
+            if ( Abc_ObjFaninId0(pFanout) == pObj->Id )
+                Seq_NtkShareLatches_rec( pNtkNew, pObj->pCopy, Seq_NodeGetRing(pFanout,0), Seq_NodeCountLats(pFanout,0), tLatchMap );
+            if ( Abc_ObjFaninId1(pFanout) == pObj->Id )
+                Seq_NtkShareLatches_rec( pNtkNew, pObj->pCopy, Seq_NodeGetRing(pFanout,1), Seq_NodeCountLats(pFanout,1), tLatchMap );
+        }
+        // clean the label
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            pFanout->fMarkC = 0;
+    }
+    stmm_free_table( tLatchMap );
+    // return to the old array
+    Vec_PtrShrink( vMapAnds, nOldNodes );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/base/seq/seqUtil.c b/src/base/seq/seqUtil.c
index b126b043..a3b8bc84 100644
--- a/src/base/seq/seqUtil.c
+++ b/src/base/seq/seqUtil.c
@@ -39,6 +39,37 @@
   SeeAlso     []
 
 ***********************************************************************/
+int Seq_NtkLevelMax( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, Result;
+    assert( Abc_NtkIsSeq(pNtk) );
+    Result = 0;
+    Abc_NtkForEachPo( pNtk, pNode, i )
+    {
+        pNode = Abc_ObjFanin0(pNode);
+        if ( Result < (int)pNode->Level )
+            Result = pNode->Level;
+    }
+    Abc_SeqForEachCutsetNode( pNtk, pNode, i )
+    {
+        if ( Result < (int)pNode->Level )
+            Result = pNode->Level;
+    }
+    return Result;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the maximum latch number on any of the fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Seq_ObjFanoutLMax( Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanout;
@@ -363,6 +394,29 @@ int Seq_NtkLatchGetEqualFaninNum( Abc_Ntk_t * pNtk )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the maximum latch number on any of the fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkCountNodesAboveLimit( Abc_Ntk_t * pNtk, int Limit )
+{
+    Abc_Obj_t * pNode;
+    int i, Counter;
+    assert( !Abc_NtkIsSeq(pNtk) );
+    Counter = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( Abc_ObjFaninNum(pNode) > Limit )
+            Counter++;
+    return Counter;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/fpga/fpga.c b/src/map/fpga/fpga.c
index 2f399e6e..68b5f124 100644
--- a/src/map/fpga/fpga.c
+++ b/src/map/fpga/fpga.c
@@ -57,8 +57,8 @@ void Fpga_Init( Abc_Frame_t * pAbc )
 {
     // set the default library
     //Fpga_LutLib_t s_LutLib = { "lutlib", 6, {0,1,2,4,8,16,32}, {0,1,2,3,4,5,6} };
-    //Fpga_LutLib_t s_LutLib = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} };
-    Fpga_LutLib_t s_LutLib = { "lutlib", 4, {0,1,1,1,1}, {0,1,1,1,1} };
+    Fpga_LutLib_t s_LutLib = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} };
+    //Fpga_LutLib_t s_LutLib = { "lutlib", 4, {0,1,1,1,1}, {0,1,1,1,1} };
     //Fpga_LutLib_t s_LutLib = { "lutlib", 3, {0,1,1,1}, {0,1,1,1} };
 
     Abc_FrameSetLibLut( Fpga_LutLibDup(&s_LutLib) );
diff --git a/src/map/mapper/mapperTree.c b/src/map/mapper/mapperTree.c
index 3f0e3134..9656b0f5 100644
--- a/src/map/mapper/mapperTree.c
+++ b/src/map/mapper/mapperTree.c
@@ -439,6 +439,9 @@ int Map_LibraryDeriveGateInfo( Map_SuperLib_t * pLib, st_table * tExcludeGate )
                 pGate->tDelayMax.Fall = pGate->tDelaysF[k].Rise;
             if ( pGate->tDelayMax.Fall < pGate->tDelaysF[k].Fall )
                 pGate->tDelayMax.Fall = pGate->tDelaysF[k].Fall;
+
+            pGate->tDelaysF[k].Worst = MAP_MAX( pGate->tDelaysF[k].Fall, pGate->tDelaysF[k].Rise );
+            pGate->tDelaysR[k].Worst = MAP_MAX( pGate->tDelaysR[k].Fall, pGate->tDelaysR[k].Rise );
         }
 
         // count gates and area of the supergate
diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h
index 307cdd8d..0e2c085d 100644
--- a/src/map/mio/mio.h
+++ b/src/map/mio/mio.h
@@ -90,6 +90,7 @@ extern float             Mio_LibraryReadDelayInvMax( Mio_Library_t * pLib );
 extern float             Mio_LibraryReadDelayNand2Rise( Mio_Library_t * pLib );
 extern float             Mio_LibraryReadDelayNand2Fall( Mio_Library_t * pLib );
 extern float             Mio_LibraryReadDelayNand2Max( Mio_Library_t * pLib );
+extern float             Mio_LibraryReadDelayAnd2Max( Mio_Library_t * pLib );
 extern float             Mio_LibraryReadAreaInv    ( Mio_Library_t * pLib );
 extern float             Mio_LibraryReadAreaBuf    ( Mio_Library_t * pLib );
 extern float             Mio_LibraryReadAreaNand2  ( Mio_Library_t * pLib );
diff --git a/src/map/mio/mioApi.c b/src/map/mio/mioApi.c
index 90a0af93..a9aaac19 100644
--- a/src/map/mio/mioApi.c
+++ b/src/map/mio/mioApi.c
@@ -53,6 +53,7 @@ float             Mio_LibraryReadDelayInvMax   ( Mio_Library_t * pLib )  { retur
 float             Mio_LibraryReadDelayNand2Rise( Mio_Library_t * pLib )  { return (float)(pLib->pGateNand2? pLib->pGateNand2->pPins->dDelayBlockRise : 0.0); }
 float             Mio_LibraryReadDelayNand2Fall( Mio_Library_t * pLib )  { return (float)(pLib->pGateNand2? pLib->pGateNand2->pPins->dDelayBlockFall : 0.0); }
 float             Mio_LibraryReadDelayNand2Max ( Mio_Library_t * pLib )  { return (float)(pLib->pGateNand2? pLib->pGateNand2->pPins->dDelayBlockMax  : 0.0); }
+float             Mio_LibraryReadDelayAnd2Max  ( Mio_Library_t * pLib )  { return (float)(pLib->pGateAnd2?  pLib->pGateAnd2->pPins->dDelayBlockMax   : 0.0); }
 float             Mio_LibraryReadAreaInv       ( Mio_Library_t * pLib )  { return (float)(pLib->pGateInv?   pLib->pGateInv->dArea   : 0.0); }
 float             Mio_LibraryReadAreaBuf       ( Mio_Library_t * pLib )  { return (float)(pLib->pGateBuf?   pLib->pGateBuf->dArea   : 0.0); }
 float             Mio_LibraryReadAreaNand2     ( Mio_Library_t * pLib )  { return (float)(pLib->pGateNand2? pLib->pGateNand2->dArea : 0.0); }
diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h
index 4f81a004..f5ecf9bd 100644
--- a/src/misc/vec/vec.h
+++ b/src/misc/vec/vec.h
@@ -29,7 +29,6 @@
 #define inline __inline // compatible with MS VS 6.0
 #endif
 
-#include "vecFan.h"
 #include "vecInt.h"
 #include "vecStr.h"
 #include "vecPtr.h"
diff --git a/src/misc/vec/vecFan.h b/src/misc/vec/vecFan_.h
index 1493014a..1493014a 100644
--- a/src/misc/vec/vecFan.h
+++ b/src/misc/vec/vecFan_.h
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 3c767f20..2d36addd 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -457,6 +457,41 @@ static inline void Vec_IntPush( Vec_Int_t * p, int Entry )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int Entry )
+{
+    if ( p->nSize == p->nCap )
+    {
+        int * pArray;
+        int i;
+
+        if ( p->nSize == 0 )
+            p->nCap = 1;
+        pArray = (int *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 );
+//        pArray = ALLOC( int, p->nCap * 2 );
+        if ( p->pArray )
+        {
+            for ( i = 0; i < p->nSize; i++ )
+                pArray[i] = p->pArray[i];
+            Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
+//            free( p->pArray );
+        }
+        p->nCap *= 2;
+        p->pArray = pArray;
+    }
+    p->pArray[p->nSize++] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline void Vec_IntPushOrder( Vec_Int_t * p, int Entry )
 {
     int i;
@@ -516,6 +551,26 @@ static inline int Vec_IntPop( Vec_Int_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Find entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntFind( Vec_Int_t * p, int Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -525,16 +580,19 @@ static inline int Vec_IntPop( Vec_Int_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Vec_IntRemove( Vec_Int_t * p, int Entry )
+static inline int Vec_IntRemove( Vec_Int_t * p, int Entry )
 {
     int i;
     for ( i = 0; i < p->nSize; i++ )
         if ( p->pArray[i] == Entry )
             break;
+    if ( i == p->nSize )
+        return 0;
     assert( i < p->nSize );
     for ( i++; i < p->nSize; i++ )
         p->pArray[i-1] = p->pArray[i];
     p->nSize--;
+    return 1;
 }
 
 /**Function*************************************************************
diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index f518e8c4..5c9b2e8e 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -69,6 +69,8 @@ struct Cut_CutStruct_t_
     unsigned           nVarsMax   :  4;   // the max number of vars [4-6]
     unsigned           nLeaves    :  4;   // the number of leaves [4-6]
     unsigned           uSign;             // the signature
+    unsigned           uCanon0;           // the canonical form 
+    unsigned           uCanon1;           // the canonical form 
     Cut_Cut_t *        pNext;             // the next cut in the list
     int                pLeaves[0];        // the array of leaves
 };
@@ -113,6 +115,7 @@ extern int              Cut_ManReadVarsMax( Cut_Man_t * p );
 /*=== cutNode.c ==========================================================*/
 extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv ); 
 extern Cut_Cut_t *      Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes );
+extern Cut_Cut_t *      Cut_NodeUnionCutsSeq( Cut_Man_t * p, Vec_Int_t * vNodes, int CutSetNum, int fFirst );
 /*=== cutSeq.c ==========================================================*/
 extern void             Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int nLat0, int nLat1, int fTriv, int CutSetNum );
 extern void             Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node );
@@ -126,6 +129,8 @@ extern int              Cut_OracleReadDrop( Cut_Oracle_t * p );
 extern void             Cut_OracleNodeSetTriv( Cut_Oracle_t * p, int Node );
 extern Cut_Cut_t *      Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 );
 extern void             Cut_OracleTryDroppingCuts( Cut_Oracle_t * p, int Node );
+/*=== cutTruth.c ==========================================================*/
+extern void             Cut_TruthCanonicize( Cut_Cut_t * pCut );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 80568d71..0268ba19 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -376,6 +376,7 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
     // start with the elementary cut
     if ( fTriv ) 
     {
+//        printf( "Creating trivial cut %d.\n", Node );
         pTemp0 = Cut_CutCreateTriv( p, Node );
         Cut_ListAdd( pSuper, pTemp0 );
         p->nNodeCuts++;
@@ -542,6 +543,189 @@ p->timeUnion += clock() - clk;
     return pList;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts by unioning cuts at a choice node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_NodeUnionCutsSeq( Cut_Man_t * p, Vec_Int_t * vNodes, int CutSetNum, int fFirst )
+{
+    Cut_List_t Super, * pSuper = &Super;
+    Cut_Cut_t * pList, * pListStart, * pCut, * pCut2, * pTop;
+    int i, k, Node, Root, Limit = p->pParams->nVarsMax;
+    int clk = clock();
+
+    // start the new list
+    Cut_ListStart( pSuper );
+
+    // remember the root node to save the resulting cuts
+    Root = Vec_IntEntry( vNodes, 0 );
+    p->nNodeCuts = 1;
+
+    // store the original lists for comparison
+    p->pCompareOld = Cut_NodeReadCutsOld( p, Root );
+    p->pCompareNew = (CutSetNum >= 0)? Cut_NodeReadCutsNew( p, Root ) : NULL;
+
+    // get the topmost cut
+    pTop = NULL;
+    if ( (pTop = Cut_NodeReadCutsOld( p, Root )) == NULL )
+        pTop = Cut_NodeReadCutsNew( p, Root );
+    assert( pTop != NULL );
+
+    // collect small cuts first
+    Vec_PtrClear( p->vTemp );
+    Vec_IntForEachEntry( vNodes, Node, i )
+    {
+        // get the cuts of this node
+        if ( i == 0 && CutSetNum >= 0 )
+        {
+            pList = Cut_NodeReadCutsTemp( p, CutSetNum );
+            Cut_NodeWriteCutsTemp( p, CutSetNum, NULL );
+        }
+        else
+        {
+            pList = Cut_NodeReadCutsNew( p, Node );
+            Cut_NodeWriteCutsNew( p, Node, NULL );
+        }
+        if ( pList == NULL )
+            continue;
+
+        // process the cuts
+        if ( fFirst )
+        {
+            // remember the starting point
+            pListStart = pList->pNext;
+            pList->pNext = NULL;
+            // save or recycle the elementary cut
+            if ( i == 0 )
+                Cut_ListAdd( pSuper, pList );
+            else
+                Cut_CutRecycle( p, pList );
+        }
+        else
+            pListStart = pList;
+
+        // save all the cuts that are smaller than the limit
+        Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
+        {
+            if ( pCut->nLeaves == (unsigned)Limit )
+            {
+                Vec_PtrPush( p->vTemp, pCut );
+                break;
+            }
+            // check containment
+//            if ( p->pParams->fFilter && Cut_CutFilterOne( p, pSuper, pCut ) )
+//                continue;
+            if ( p->pParams->fFilter )
+            {
+                if ( Cut_CutFilterOne(p, pSuper, pCut) )
+                    continue;
+                if ( p->pParams->fSeq )
+                {
+                    if ( p->pCompareOld && Cut_CutFilterOld(p, p->pCompareOld, pCut) )
+                        continue;
+                    if ( p->pCompareNew && Cut_CutFilterOld(p, p->pCompareNew, pCut) )
+                        continue;
+                }
+            }
+
+            // set the complemented bit by comparing the first cut with the current cut
+            pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+            pListStart = pCut->pNext;
+            pCut->pNext = NULL;
+            // add to the list
+            Cut_ListAdd( pSuper, pCut );
+            if ( ++p->nNodeCuts == p->pParams->nKeepMax )
+            {
+                // recycle the rest of the cuts of this node
+                Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
+                    Cut_CutRecycle( p, pCut );
+                // recycle all cuts of other nodes
+                Vec_IntForEachEntryStart( vNodes, Node, k, i+1 )
+                    Cut_NodeFreeCuts( p, Node );
+                // recycle the saved cuts of other nodes
+                Vec_PtrForEachEntry( p->vTemp, pList, k )
+                    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+                        Cut_CutRecycle( p, pCut );
+                goto finish;
+            }
+        }
+    } 
+    // collect larger cuts next
+    Vec_PtrForEachEntry( p->vTemp, pList, i )
+    {
+        Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+        {
+            // check containment
+//            if ( p->pParams->fFilter && Cut_CutFilterOne( p, pSuper, pCut ) )
+//                continue;
+            if ( p->pParams->fFilter )
+            {
+                if ( Cut_CutFilterOne(p, pSuper, pCut) )
+                    continue;
+                if ( p->pParams->fSeq )
+                {
+                    if ( p->pCompareOld && Cut_CutFilterOld(p, p->pCompareOld, pCut) )
+                        continue;
+                    if ( p->pCompareNew && Cut_CutFilterOld(p, p->pCompareNew, pCut) )
+                        continue;
+                }
+            }
+
+            // set the complemented bit
+            pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+            pListStart   = pCut->pNext;
+            pCut->pNext  = NULL;
+            // add to the list
+            Cut_ListAdd( pSuper, pCut );
+            if ( ++p->nNodeCuts == p->pParams->nKeepMax )
+            {
+                // recycle the rest of the cuts
+                Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
+                    Cut_CutRecycle( p, pCut );
+                // recycle the saved cuts of other nodes
+                Vec_PtrForEachEntryStart( p->vTemp, pList, k, i+1 )
+                    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+                        Cut_CutRecycle( p, pCut );
+                goto finish;
+            }
+        }
+    }
+finish :
+    // set the cuts at the node
+    pList = Cut_ListFinish( pSuper );
+
+    // set the lists at the node
+//    assert( Cut_NodeReadCutsNew(p, Root) == NULL );
+//    Cut_NodeWriteCutsNew( p, Root, pList );
+    if ( CutSetNum >= 0 )
+    {
+        assert( Cut_NodeReadCutsTemp(p, CutSetNum) == NULL );
+        Cut_NodeWriteCutsTemp( p, CutSetNum, pList );
+    }
+    else
+    {
+        assert( Cut_NodeReadCutsNew(p, Root) == NULL );
+        Cut_NodeWriteCutsNew( p, Root, pList );
+    }
+
+p->timeUnion += clock() - clk;
+    // filter the cuts
+//clk = clock();
+//    if ( p->pParams->fFilter )
+//        Cut_CutFilter( p, pList );
+//p->timeFilter += clock() - clk;
+//    if ( fFirst )
+//        p->nNodes -= vNodes->nSize - 1;
+    return pList;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/opt/cut/cutTruth.c b/src/opt/cut/cutTruth.c
index 28984e5a..b65e5eff 100644
--- a/src/opt/cut/cutTruth.c
+++ b/src/opt/cut/cutTruth.c
@@ -107,6 +107,48 @@ void Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, i
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
+  Description [This procedure cannot be used while recording oracle
+  because it will overwrite Num0 and Num1.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_TruthCanonicize( Cut_Cut_t * pCut )
+{
+    unsigned uTruth;
+    unsigned * uCanon2;
+    char * pPhases2;
+    assert( pCut->nVarsMax < 6 );
+
+    // get the direct truth table
+    uTruth = *Cut_CutReadTruth(pCut);
+
+    // compute the direct truth table
+    Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
+//    uCanon[0] = uCanon2[0];
+//    uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
+//    uPhases[0] = pPhases2[0];
+    pCut->uCanon0 = uCanon2[0];
+    pCut->Num0    = pPhases2[0];
+
+    // get the complemented truth table
+    uTruth = ~*Cut_CutReadTruth(pCut);
+
+    // compute the direct truth table
+    Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
+//    uCanon[0] = uCanon2[0];
+//    uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
+//    uPhases[0] = pPhases2[0];
+    pCut->uCanon1 = uCanon2[0];
+    pCut->Num1    = pPhases2[0];
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
index aa2a7039..b6b2524b 100644
--- a/src/opt/dec/dec.h
+++ b/src/opt/dec/dec.h
@@ -96,6 +96,7 @@ struct Dec_Man_t_
 
 /*=== decAbc.c ========================================================*/
 extern Abc_Obj_t *    Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
+extern Abc_Obj_t *    Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
 extern int            Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
 extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
 /*=== decFactor.c ========================================================*/
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
index 6782a02f..1416cf0d 100644
--- a/src/opt/dec/decAbc.c
+++ b/src/opt/dec/decAbc.c
@@ -63,6 +63,44 @@ Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph )
 
 /**Function*************************************************************
 
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+  of the leaves of the graph before calling this procedure.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph )
+{
+    Abc_Obj_t * pAnd, * pAnd0, * pAnd1;
+    Dec_Node_t * pNode;
+    int i;
+    // check for constant function
+    if ( Dec_GraphIsConst(pGraph) )
+        return Abc_ObjNotCond( Abc_NtkConst1(pNtk), Dec_GraphIsComplement(pGraph) );
+    // check for a literal
+    if ( Dec_GraphIsVar(pGraph) )
+        return Abc_ObjNotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+    // build the AIG nodes corresponding to the AND gates of the graph
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        pAnd0 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
+        pAnd1 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
+//        pNode->pFunc = Abc_AigAnd( pNtk->pManFunc, pAnd0, pAnd1 );
+        pAnd = Abc_NtkCreateNode( pNtk );
+        Abc_ObjAddFanin( pAnd, pAnd0 );
+        Abc_ObjAddFanin( pAnd, pAnd1 );
+        pNode->pFunc = pAnd;
+    }
+    // complement the result if necessary
+    return Abc_ObjNotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of new nodes added when using this graph.]
 
   Description [AIG nodes for the fanins should be assigned to pNode->pFunc 
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index 24b86c95..02b7605c 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -24,11 +24,11 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void        Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_t * vFanins, int * pOrder );
+static void        Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder );
 static int         Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY );
 static void        Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext );
 static Fxu_Cube *  Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode );
-static Abc_Fan_t * s_pLits;
+static int * s_pLits;
 
 extern int         Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );
 
@@ -53,7 +53,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
     Fxu_Var * pVar;
     Fxu_Cube * pCubeFirst, * pCubeNew;
     Fxu_Cube * pCube1, * pCube2;
-    Vec_Fan_t * vFanins;
+    Vec_Int_t * vFanins;
     char * pSopCover;
     char * pSopCube;
     int * pOrder, nBitsMax;
@@ -151,7 +151,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
             pOrder[v] = v;
         // reorder the fanins
         qsort( (void *)pOrder, nFanins, sizeof(int),(int (*)(const void *, const void *))Fxu_CreateMatrixLitCompare);
-        assert( s_pLits[ pOrder[0] ].iFan < s_pLits[ pOrder[nFanins-1] ].iFan );
+        assert( s_pLits[ pOrder[0] ] < s_pLits[ pOrder[nFanins-1] ] );
         // create the corresponding cubes in the matrix
         pCubeFirst = NULL;
         c = 0;
@@ -214,7 +214,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
   SeeAlso     []
 
 ***********************************************************************/
-void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_t * vFanins, int * pOrder )
+void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder )
 {
     Fxu_Var * pVar;
     int Value, i;
@@ -224,12 +224,12 @@ void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube,
         Value = pSopCube[pOrder[i]];
         if ( Value == '0' )
         {
-            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]].iFan + 1 ];  // CST
+            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] + 1 ];  // CST
             Fxu_MatrixAddLiteral( p, pCube, pVar );
         }
         else if ( Value == '1' )
         {
-            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]].iFan ];  // CST
+            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] ];  // CST
             Fxu_MatrixAddLiteral( p, pCube, pVar );
         }
     }
@@ -409,7 +409,7 @@ Fxu_Cube * Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iV
 ***********************************************************************/
 int Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY )
 {
-    return s_pLits[*ptrX].iFan - s_pLits[*ptrY].iFan;
+    return s_pLits[*ptrX] - s_pLits[*ptrY];
 } 
 
 ////////////////////////////////////////////////////////////////////////