Version abc51128

17 files changed, 1653 insertions, 197 deletions

diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 6fae871d..8383251a 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -235,8 +235,8 @@ Abc_Ntk_t * Abc_NtkStartRead( char * pName )
     // allocate the empty network
     pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP );
     // set the specs
-    pNtkNew->pName = util_strsav( pName );
-    pNtkNew->pSpec = util_strsav( pName );
+    pNtkNew->pName = util_strsav( Extra_FileNameGeneric(pName) );
+    pNtkNew->pSpec = util_strsav( Extra_FileNameGeneric(pName) );
     return pNtkNew;
 }
 
@@ -313,7 +313,11 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
         // copy the nodes
         Abc_NtkForEachObj( pNtk, pObj, i )
             if ( pObj->pCopy == NULL )
+            {
                 Abc_NtkDupObj(pNtkNew, pObj);
+                pObj->pCopy->Level = pObj->Level;
+                pObj->pCopy->fPhase = pObj->fPhase;
+            }
         // connect the nodes
         Abc_NtkForEachObj( pNtk, pObj, i )
         {
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index db2d08a7..91adbabc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5100,17 +5100,16 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Abc_NtkHasAig(pNtk) )
     {
+        // quit if there are choice nodes
+        if ( Abc_NtkGetChoiceNum(pNtk) )
+        {
+            fprintf( pErr, "Currently cannot retime networks with choice nodes.\n" );
+            return 0;
+        }
         if ( Abc_NtkIsStrash(pNtk) )
             pNtkRes = Abc_NtkAigToSeq(pNtk);
         else
-        {
-            if ( Abc_NtkGetChoiceNum(pNtk) )
-            {
-                fprintf( pErr, "Currently cannot retime networks with choice nodes.\n" );
-                return 0;
-            }
             pNtkRes = Abc_NtkDup(pNtk);
-        }
         // retime the network
         if ( fForward )
             Seq_NtkSeqRetimeForward( pNtkRes, fInitial, fVerbose );
@@ -5118,11 +5117,13 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
             Seq_NtkSeqRetimeBackward( pNtkRes, fInitial, fVerbose );
         else
             Seq_NtkSeqRetimeDelay( pNtkRes, nMaxIters, fInitial, fVerbose );
-        // convert from the sequential AIG
+        // if the network is an AIG, convert the result into an AIG
         if ( Abc_NtkIsStrash(pNtk) )
         {
             pNtkRes = Abc_NtkSeqToLogicSop( pNtkTemp = pNtkRes );
             Abc_NtkDelete( pNtkTemp );
+            pNtkRes = Abc_NtkStrash( pNtkTemp = pNtkRes, 0, 0 );
+            Abc_NtkDelete( pNtkTemp );
         }
     }
     else
@@ -5162,7 +5163,7 @@ usage:
 int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Ntk_t * pNtk, * pNtkNew, * pNtkRes;
     int c, nMaxIters;
     int fVerbose;
 
@@ -5205,26 +5206,65 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsSeq(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
     {
-        fprintf( pErr, "Sequential FPGA mapping works only for sequential AIG (run \"seq\").\n" );
-        return 0;
+        // quit if there are choice nodes
+        if ( Abc_NtkGetChoiceNum(pNtk) )
+        {
+            fprintf( pErr, "Currently cannot map/retime networks with choice nodes.\n" );
+            return 0;
+        }
+        if ( Abc_NtkIsStrash(pNtk) )
+            pNtkNew = Abc_NtkAigToSeq(pNtk);
+        else
+            pNtkNew = Abc_NtkDup(pNtk);
+    }
+    else
+    {
+        // strash and balance the network
+        pNtkNew = Abc_NtkStrash( pNtk, 0, 0 );
+        if ( pNtkNew == NULL )
+        {
+            fprintf( pErr, "Strashing before FPGA mapping/retiming has failed.\n" );
+            return 1;
+        }
+
+        pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0 );
+        Abc_NtkDelete( pNtkRes );
+        if ( pNtkNew == NULL )
+        {
+            fprintf( pErr, "Balancing before FPGA mapping has failed.\n" );
+            return 1;
+        }
+
+        // convert into a sequential AIG
+        pNtkNew = Abc_NtkAigToSeq( pNtkRes = pNtkNew );
+        Abc_NtkDelete( pNtkRes );
+        if ( pNtkNew == NULL )
+        {
+            fprintf( pErr, "Converting into a seq AIG before FPGA mapping/retiming has failed.\n" );
+            return 1;
+        }
+
+        fprintf( pOut, "The network was strashed and balanced before FPGA mapping/retiming.\n" );
     }
 
     // get the new network
-    pNtkRes = Seq_NtkFpgaMapRetime( pNtk, nMaxIters, fVerbose );
+    pNtkRes = Seq_NtkFpgaMapRetime( pNtkNew, nMaxIters, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
         return 0;
     }
+    Abc_NtkDelete( pNtkNew );
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
     fprintf( pErr, "usage: sfpga [-I num] [-vh]\n" );
-    fprintf( pErr, "\t         performs integrated sequential FPGA mapping\n" );
+    fprintf( pErr, "\t         performs integrated sequential FPGA mapping/retiming\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");
@@ -5245,7 +5285,7 @@ usage:
 int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Ntk_t * pNtk, * pNtkNew, * pNtkRes;
     int c, nMaxIters;
     int fVerbose;
 
@@ -5255,7 +5295,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nMaxIters = 15;
-    fVerbose  =  1;
+    fVerbose  =  0;
     util_getopt_reset();
     while ( ( c = util_getopt( argc, argv, "Ivh" ) ) != EOF )
     {
@@ -5288,28 +5328,66 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsSeq(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
     {
-        fprintf( pErr, "Sequential standard cell mapping works only for sequential AIG (run \"seq\").\n" );
-        return 1;
+        // quit if there are choice nodes
+        if ( Abc_NtkGetChoiceNum(pNtk) )
+        {
+            fprintf( pErr, "Currently cannot map/retime networks with choice nodes.\n" );
+            return 0;
+        }
+        if ( Abc_NtkIsStrash(pNtk) )
+            pNtkNew = Abc_NtkAigToSeq(pNtk);
+        else
+            pNtkNew = Abc_NtkDup(pNtk);
+    }
+    else
+    {
+        // strash and balance the network
+        pNtkNew = Abc_NtkStrash( pNtk, 0, 0 );
+        if ( pNtkNew == NULL )
+        {
+            fprintf( pErr, "Strashing before SC mapping/retiming has failed.\n" );
+            return 1;
+        }
+
+        pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0 );
+        Abc_NtkDelete( pNtkRes );
+        if ( pNtkNew == NULL )
+        {
+            fprintf( pErr, "Balancing before SC mapping/retiming has failed.\n" );
+            return 1;
+        }
+
+        // convert into a sequential AIG
+        pNtkNew = Abc_NtkAigToSeq( pNtkRes = pNtkNew );
+        Abc_NtkDelete( pNtkRes );
+        if ( pNtkNew == NULL )
+        {
+            fprintf( pErr, "Converting into a seq AIG before SC mapping/retiming has failed.\n" );
+            return 1;
+        }
+
+        fprintf( pOut, "The network was strashed and balanced before SC mapping/retiming.\n" );
     }
-//    printf( "This command is not yet implemented.\n" );
-//    return 0;
 
     // get the new network
-    pNtkRes = Seq_MapRetime( pNtk, nMaxIters, fVerbose );
+    pNtkRes = Seq_MapRetime( pNtkNew, nMaxIters, fVerbose );
     if ( pNtkRes == NULL )
     {
-        fprintf( pErr, "Sequential standard-cell mapping has failed.\n" );
+        fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
         return 1;
     }
+    Abc_NtkDelete( pNtkNew );
+
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
     fprintf( pErr, "usage: smap [-I num] [-vh]\n" );
-    fprintf( pErr, "\t         performs integrated sequential standard-cell mapping" );
+    fprintf( pErr, "\t         performs integrated sequential standard-cell mapping/retiming\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");
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index d00b265a..373c4636 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -26,6 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static char * Abc_NtkPrintSop( char * pSop );
+static int    Abc_NtkCountLogicNodes( Vec_Ptr_t * vNodes );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -181,7 +182,7 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     fprintf( pFile, "          fontsize=18,\n" );
     fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
     fprintf( pFile, "          label=\"" );
-    fprintf( pFile, "The set contains %d nodes and spans %d levels.", vNodes->nSize, LevelMax - LevelMin + 1 );
+    fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Abc_NtkCountLogicNodes(vNodes), LevelMax - LevelMin + 1 );
     fprintf( pFile, "\\n" );
     fprintf( pFile, "\"\n" );
     fprintf( pFile, "         ];\n" );
@@ -526,7 +527,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     fprintf( pFile, "          fontsize=18,\n" );
     fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
     fprintf( pFile, "          label=\"" );
-    fprintf( pFile, "The set contains %d nodes and spans %d levels.", vNodes->nSize, LevelMax - LevelMin + 1 );
+    fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Abc_NtkCountLogicNodes(vNodes), LevelMax - LevelMin + 1 );
     fprintf( pFile, "\\n" );
     fprintf( pFile, "\"\n" );
     fprintf( pFile, "         ];\n" );
@@ -701,6 +702,32 @@ char * Abc_NtkPrintSop( char * pSop )
     return Buffer;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the printable SOP form.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCountLogicNodes( Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pObj;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        if ( !Abc_ObjIsNode(pObj) )
+            continue;
+        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
+            continue;
+        Counter ++;
+    }
+    return Counter;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seq.h b/src/base/seq/seq.h
index a644303f..323466a0 100644
--- a/src/base/seq/seq.h
+++ b/src/base/seq/seq.h
@@ -67,7 +67,7 @@ extern bool            Abc_NtkSeqCheck( Abc_Ntk_t * pNtk );
 /*=== seqShare.c =============================================================*/
 extern void            Seq_NtkShareFanouts( Abc_Ntk_t * pNtk );
 extern void            Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk );
-extern void            Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds );
+extern void            Seq_NtkShareLatchesMapping( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds, int fFpga );
 extern void            Seq_NtkShareLatchesClean( Abc_Ntk_t * pNtk );
 /*=== seqUtil.c ==============================================================*/
 extern char *          Seq_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge );
@@ -78,6 +78,7 @@ extern int             Seq_NtkLatchNumShared( Abc_Ntk_t * pNtk );
 extern void            Seq_NtkLatchGetInitNums( Abc_Ntk_t * pNtk, int * pInits );
 extern int             Seq_NtkLatchGetEqualFaninNum( Abc_Ntk_t * pNtk );
 extern int             Seq_NtkCountNodesAboveLimit( Abc_Ntk_t * pNtk, int Limit );
+extern int             Seq_MapComputeAreaFlows( Abc_Ntk_t * pNtk, int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c
index 5dca2e86..9b1e69a5 100644
--- a/src/base/seq/seqAigCore.c
+++ b/src/base/seq/seqAigCore.c
@@ -815,14 +815,14 @@ Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, b
         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;
         }
     }
diff --git a/src/base/seq/seqFpgaCore.c b/src/base/seq/seqFpgaCore.c
index 030efd80..705f553d 100644
--- a/src/base/seq/seqFpgaCore.c
+++ b/src/base/seq/seqFpgaCore.c
@@ -82,6 +82,7 @@ Abc_Ntk_t * Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int nMaxIters, 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 );
+
     // create the final mapped network
     pNtkMap = Seq_NtkSeqFpgaMapped( pNtkNew );
     Abc_NtkDelete( pNtkNew );
@@ -142,8 +143,6 @@ Abc_Ntk_t * Seq_NtkFpgaDup( Abc_Ntk_t * pNtk )
     // transfer the mapping info to the new manager
     Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
     {
-        // convert the root node
-        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
         // get the leaves of the cut
         vLeaves = Vec_VecEntry( p->vMapCuts, i );
         // convert the leaf nodes
@@ -151,13 +150,14 @@ Abc_Ntk_t * Seq_NtkFpgaDup( Abc_Ntk_t * pNtk )
         {
             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 );
         }
+        // convert the root node
+        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
     }
     pNew = pNtkNew->pManFunc;
     pNew->nVarsMax  = p->nVarsMax;
@@ -290,8 +290,9 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
     // duplicate the nodes used in the mapping
     Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
         pObj->pCopy = Abc_NtkCreateNode( pNtkMap );
+
     // create and share the latches
-    Seq_NtkShareLatchesFpga( pNtkMap, pNtk, p->vMapAnds );
+    Seq_NtkShareLatchesMapping( pNtkMap, pNtk, p->vMapAnds, 1 );
 
     // connect the nodes
     Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
diff --git a/src/base/seq/seqFpgaIter.c b/src/base/seq/seqFpgaIter.c
index 9d4002bc..96874db3 100644
--- a/src/base/seq/seqFpgaIter.c
+++ b/src/base/seq/seqFpgaIter.c
@@ -73,6 +73,9 @@ p->timeCuts = clock() - clk;
     if ( fVerbose )
     Cut_ManPrintStats( p->pCutMan );
 
+    // compute area flows
+//    Seq_MapComputeAreaFlows( pNtk, fVerbose );
+
     // compute the delays
 clk = clock();
     Seq_AigRetimeDelayLags( pNtk, fVerbose );
@@ -170,6 +173,7 @@ Cut_Cut_t * Seq_FpgaMappingSelectCut( Abc_Obj_t * pAnd )
             if ( Abc_NodeIsTravIdCurrent(pFanin) )
                 continue;
             CostCur += (float)(1.0 / Abc_ObjFanoutNum(pFanin));
+//            CostCur += Seq_NodeGetFlow( pFanin );
         }
         if ( CostMin > CostCur )
         {
diff --git a/src/base/seq/seqInt.h b/src/base/seq/seqInt.h
index c0f3e907..5532b490 100644
--- a/src/base/seq/seqInt.h
+++ b/src/base/seq/seqInt.h
@@ -64,6 +64,7 @@ struct Abc_Seq_t_
     Cut_Man_t *         pCutMan;        // cut manager
     Map_SuperLib_t *    pSuperLib;      // the current supergate library
     // sequential arrival time computation
+    Vec_Int_t *         vAFlows;        // the area flow of each cut
     Vec_Int_t *         vLValues;       // the arrival times (L-Values of nodes)
     Vec_Int_t *         vLValuesN;      // the arrival times (L-Values of nodes)
     Vec_Str_t *         vLags;          // the lags of the mapped nodes
@@ -73,6 +74,7 @@ struct Abc_Seq_t_
     Vec_Ptr_t *         vMapAnds;       // nodes visible in the mapping 
     Vec_Vec_t *         vMapCuts;       // best cuts for each node 
     Vec_Vec_t *         vMapDelays;     // the delay of each fanin
+    Vec_Vec_t *         vMapFanins;     // the delay of each fanin
     // runtime stats
     int                 timeCuts;       // runtime to compute the cuts
     int                 timeDelay;      // runtime to compute the L-values
@@ -117,7 +119,8 @@ struct Seq_Match_t_ // 3 words
     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
+    unsigned            uPhase  : 14;   // the phase assignment at the boundary
+    unsigned            uPhaseR : 14;   // the real phase assignment at the boundary
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -157,8 +160,11 @@ static inline float          Seq_NodeGetLValueP( Abc_Obj_t * pNode )
 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 area flows
+static inline Vec_Int_t *    Seq_NodeFlow( Abc_Obj_t * pNode )                       { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vAFlows;                        }
+static inline float          Seq_NodeGetFlow( Abc_Obj_t * pNode )                    { return Abc_Int2Float( Vec_IntEntry( Seq_NodeFlow(pNode), (pNode)->Id ) );      }
+static inline void           Seq_NodeSetFlow( Abc_Obj_t * pNode, float Value )       { Vec_IntWriteEntry( Seq_NodeFlow(pNode), (pNode)->Id, Abc_Float2Int(Value) );   }
 
 // reading the contents of the lat
 static inline Abc_InitType_t Seq_LatInit( Seq_Lat_t * pLat )  { return ((unsigned)pLat->pPrev) & 3;                                 }
@@ -178,6 +184,8 @@ static inline char           Seq_NodeGetLag( Abc_Obj_t * pNode )
 static inline char           Seq_NodeGetLagN( Abc_Obj_t * pNode )                     { return Vec_StrEntry( Seq_NodeLagsN(pNode), (pNode)->Id );        }
 static inline void           Seq_NodeSetLag( Abc_Obj_t * pNode, char Value )          { Vec_StrWriteEntry( Seq_NodeLags(pNode), (pNode)->Id, (Value) );  }
 static inline void           Seq_NodeSetLagN( Abc_Obj_t * pNode, char Value )         { Vec_StrWriteEntry( Seq_NodeLagsN(pNode), (pNode)->Id, (Value) ); }
+static inline int            Seq_NodeComputeLag( int LValue, int Fi )                 { return (LValue + 1024*Fi)/Fi - 1024 - (int)(LValue % Fi == 0);     }
+static inline int            Seq_NodeComputeLagFloat( float LValue, float Fi )        { return ((int)ceil(LValue/Fi)) - 1;                                        }
 
 // phase usage
 static inline Vec_Str_t *    Seq_NodeUses( Abc_Obj_t * pNode )                        { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vUses;            }
diff --git a/src/base/seq/seqMan.c b/src/base/seq/seqMan.c
index 7dae5b23..405eeb39 100644
--- a/src/base/seq/seqMan.c
+++ b/src/base/seq/seqMan.c
@@ -58,6 +58,7 @@ Abc_Seq_t * Seq_Create( Abc_Ntk_t * pNtk )
     p->vLValues  = Vec_IntStart( p->nSize ); 
     p->vLags     = Vec_StrStart( p->nSize ); 
     p->vLValuesN = Vec_IntStart( p->nSize ); 
+    p->vAFlows   = Vec_IntStart( p->nSize ); 
     p->vLagsN    = Vec_StrStart( p->nSize ); 
     p->vUses     = Vec_StrStart( p->nSize ); 
     return p;
@@ -84,6 +85,7 @@ void Seq_Resize( Abc_Seq_t * p, int nMaxId )
     Vec_IntFill( p->vLValues,  p->nSize, 0 ); 
     Vec_StrFill( p->vLags,     p->nSize, 0 ); 
     Vec_IntFill( p->vLValuesN, p->nSize, 0 ); 
+    Vec_IntFill( p->vAFlows,   p->nSize, 0 ); 
     Vec_StrFill( p->vLagsN,    p->nSize, 0 ); 
     Vec_StrFill( p->vUses,     p->nSize, 0 ); 
 }
@@ -102,21 +104,24 @@ void Seq_Resize( Abc_Seq_t * p, int nMaxId )
 ***********************************************************************/
 void Seq_Delete( Abc_Seq_t * p )
 {
-    if ( p->fStandCells )
+    if ( p->fStandCells && p->vMapAnds )
     {
         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
+    if ( p->vMapDelays )  Vec_VecFree( p->vMapDelays );  // the nodes used in the mapping
+    if ( p->vMapFanins )  Vec_VecFree( p->vMapFanins );  // the cuts used in the mapping
+    if ( p->vMapAnds )    Vec_PtrFree( p->vMapAnds );    // the nodes used in the mapping
+    if ( p->vMapCuts )    Vec_VecFree( p->vMapCuts );    // the cuts used in the mapping
+    if ( p->vLValues )    Vec_IntFree( p->vLValues );    // the arrival times (L-Values of nodes)
+    if ( p->vLags )       Vec_StrFree( p->vLags );       // the lags of the mapped nodes
+    if ( p->vLValuesN )   Vec_IntFree( p->vLValuesN );   // the arrival times (L-Values of nodes)
+    if ( p->vAFlows )     Vec_IntFree( p->vAFlows );     // the arrival times (L-Values of nodes)
+    if ( p->vLagsN )      Vec_StrFree( p->vLagsN );      // the lags of the mapped nodes
+    if ( p->vUses )       Vec_StrFree( p->vUses );       // the uses of phases
+    if ( p->vInits )      Vec_PtrFree( p->vInits );      // the initial values of the latches
+    if ( p->vNums )       Vec_IntFree( p->vNums );       // the numbers of latches
     Extra_MmFixedStop( p->pMmInits, 0 );
     free( p );
 }
diff --git a/src/base/seq/seqMapCore.c b/src/base/seq/seqMapCore.c
index 4f5a5e73..bbcc9a7c 100644
--- a/src/base/seq/seqMapCore.c
+++ b/src/base/seq/seqMapCore.c
@@ -33,13 +33,12 @@ 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 Abc_Obj_t *  Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int fCompl, int LagCut, Vec_Ptr_t * vLeaves, unsigned uPhase );
 static DdNode *     Seq_MapMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
 static void         Seq_MapMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges );
 static void         Seq_MapMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
 static DdNode *     Seq_MapMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -81,25 +80,19 @@ Abc_Ntk_t * Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
         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;
-    }
+//    return pNtkNew;
 
     // create the final mapped network
     pNtkMap = Seq_NtkSeqMapMapped( pNtkNew );
@@ -124,7 +117,7 @@ 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;
+    Abc_Obj_t * pObj, * pFanin, * pFaninNew, * pLeaf;
     Vec_Ptr_t * vLeaves;
     unsigned SeqEdge;
     int i, k, nObjsNew, Lag;
@@ -133,7 +126,7 @@ Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
 
     // start the expanded network
     pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
-    Abc_NtkCleanNext( pNtk );
+    Abc_NtkCleanNext(pNtk);
 
     // start the new sequential AIG manager
     nObjsNew = 1 + Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk) + Seq_MapMappingCount(pNtk);
@@ -141,25 +134,71 @@ Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
 
     // duplicate the nodes in the mapping
     Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
-        if ( pMatch->fCompl )
-            pMatch->pAnd->pNext = Abc_NtkCreateNode( pNtkNew );
-        else
+    {
+//        Abc_NtkDupObj( pNtkNew, pMatch->pAnd );
+        if ( !pMatch->fCompl )
             pMatch->pAnd->pCopy = Abc_NtkCreateNode( pNtkNew );
+        else
+            pMatch->pAnd->pNext = Abc_NtkCreateNode( pNtkNew );
+    }
+
+    // compute the real phase assignment
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        pMatch->uPhaseR = 0;
+        // get the leaves of the cut
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // convert the leaf nodes
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+
+            // set the phase
+            if ( pMatch->uPhase & (1 << k) ) // neg is required
+            {
+                if ( pLeaf->pNext ) // neg is available
+                    pMatch->uPhaseR |= (1 << k); // neg is used
+//                else
+//                    Seq_NodeSetLag( pLeaf, Seq_NodeGetLagN(pLeaf) );
+            }
+            else // pos is required
+            {
+                if ( pLeaf->pCopy == NULL ) // pos is not available
+                    pMatch->uPhaseR |= (1 << k); // neg is used
+//                else
+//                    Seq_NodeSetLagN( pLeaf, Seq_NodeGetLag(pLeaf) );
+            }
+        }
+    }
+
 
     // recursively construct the internals of each node
-    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
     {
+//        if ( pMatch->pSuper == NULL )
+//        {
+//            int x = 0;
+//        }
         vLeaves = Vec_VecEntry( p->vMapCuts, i );
-        Seq_MapMappingBuild_rec( pNtkNew, pNtk, pObj->Id << 8, 1, Seq_NodeGetLag(pObj), vLeaves );
+        if ( !pMatch->fCompl )
+            Seq_MapMappingBuild_rec( pNtkNew, pNtk, pMatch->pAnd->Id << 8, 1, pMatch->fCompl, Seq_NodeGetLag(pMatch->pAnd), vLeaves, pMatch->uPhaseR );
+        else
+            Seq_MapMappingBuild_rec( pNtkNew, pNtk, pMatch->pAnd->Id << 8, 1, pMatch->fCompl, Seq_NodeGetLagN(pMatch->pAnd), vLeaves, pMatch->uPhaseR );
     }
     assert( nObjsNew == pNtkNew->nObjs );
 
     // set the POs
-    Abc_NtkForEachCo( pNtk, pObj, i )
+//    Abc_NtkFinalize( pNtk, pNtkNew );
+    Abc_NtkForEachPo( pNtk, pObj, i )
     {
-        pDriver    = Abc_ObjFanin0(pObj);
-        pDriverNew = Abc_ObjFaninC0(pObj)? pDriver->pNext : pDriver->pCopy;
-        Abc_ObjAddFanin( pObj->pCopy, pDriverNew );
+        pFanin = Abc_ObjFanin0(pObj);
+        if ( Abc_ObjFaninC0(pObj) )
+            pFaninNew = pFanin->pNext ? pFanin->pNext : pFanin->pCopy;
+        else
+            pFaninNew = pFanin->pCopy ? pFanin->pCopy : pFanin->pNext;
+        pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
     }
 
     // duplicate the latches on the PO edges
@@ -169,9 +208,6 @@ Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
     // 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
@@ -179,25 +215,46 @@ Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
         {
             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);
+
+//            Lag = (SeqEdge & 255) + Seq_NodeGetLag(pMatch->pAnd) - Seq_NodeGetLag(pLeaf);
+            Lag = (SeqEdge & 255) + 
+                (pMatch->fCompl?                     Seq_NodeGetLagN(pMatch->pAnd) : Seq_NodeGetLag(pMatch->pAnd)) - 
+                (((pMatch->uPhaseR & (1 << k)) > 0)? Seq_NodeGetLagN(pLeaf)        : Seq_NodeGetLag(pLeaf)       );
+
             assert( Lag >= 0 );
+
+            // translate the old leaf into the leaf in the new network
+//            if ( pMatch->uPhase & (1 << k) ) // negative phase is required
+//                pFaninNew = pLeaf->pNext? pLeaf->pNext : pLeaf->pCopy;
+//            else // positive phase is required
+//                pFaninNew = pLeaf->pCopy? pLeaf->pCopy : pLeaf->pNext;
+
             // translate the old leaf into the leaf in the new network
-            Vec_PtrWriteEntry( vLeaves, k, (void *)((pLeaf->pCopy->Id << 8) | Lag) );
+            if ( pMatch->uPhaseR & (1 << k) ) // negative phase is required
+                pFaninNew = pLeaf->pNext;
+            else // positive phase is required
+                pFaninNew = pLeaf->pCopy;
+
+            Vec_PtrWriteEntry( vLeaves, k, (void *)((pFaninNew->Id << 8) | Lag) );
 //            printf( "%d -> %d\n", pLeaf->Id, pLeaf->pCopy->Id );
+
+            // UPDATE PHASE!!!   leaving only those bits that require inverters
         }
+        // convert the root node
+//        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
+        pMatch->pAnd = pMatch->fCompl? pMatch->pAnd->pNext : pMatch->pAnd->pCopy;
     }
     pNew = pNtkNew->pManFunc;
-    pNew->nVarsMax  = p->nVarsMax;
-    pNew->vMapAnds  = p->vMapAnds;   p->vMapAnds  = NULL;
-    pNew->vMapCuts  = p->vMapCuts;   p->vMapCuts  = NULL;
+    pNew->nVarsMax    = p->nVarsMax;
+    pNew->vMapAnds    = p->vMapAnds;     p->vMapAnds    = NULL;
+    pNew->vMapCuts    = p->vMapCuts;     p->vMapCuts    = NULL;
+    pNew->fStandCells = p->fStandCells;  p->fStandCells = 0;
 
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Seq_NtkMapDup(): Network check has failed.\n" );
     return pNtkNew;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Checks if the initial states are compatible.]
@@ -214,7 +271,82 @@ Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 int Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose )
 {
-    return 1;
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Seq_Match_t * pMatch;
+    Abc_Obj_t * pAnd, * pLeaf, * pFanout0, * pFanout1;
+    Vec_Vec_t * vTotalEdges;
+    Vec_Ptr_t * vLeaves, * vEdges;
+    int i, k, m, Edge0, Edge1, nLatchAfter, nLatches1, nLatches2;
+    unsigned SeqEdge;
+    int CountBad = 0, CountAll = 0;
+
+    vTotalEdges = Vec_VecStart( p->nVarsMax );
+    // go through all the nodes (cuts) used in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        pAnd = pMatch->pAnd;
+//        printf( "*** Node %d.\n", pAnd->Id );
+
+        // get the cut of this gate
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+
+        // get the edges pointing to the leaves
+        Vec_VecClear( vTotalEdges );
+        Seq_MapMappingEdges_rec( pNtk, pAnd->Id << 8, NULL, vLeaves, vTotalEdges );
+
+        // for each leaf, consider its edges
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+            nLatchAfter = SeqEdge & 255;
+            if ( nLatchAfter == 0 )
+                continue;
+
+            // go through the edges
+            vEdges = Vec_VecEntry( vTotalEdges, k );
+            pFanout0 = NULL;
+            Vec_PtrForEachEntry( vEdges, pFanout1, m )
+            {
+                Edge1    = Abc_ObjIsComplement(pFanout1);
+                pFanout1 = Abc_ObjRegular(pFanout1);
+//printf( "Fanin = %d. Fanout = %d.\n", pLeaf->Id, pFanout1->Id );
+
+                // make sure this is the same fanin
+                if ( Edge1 )
+                    assert( pLeaf == Abc_ObjFanin1(pFanout1) );
+                else
+                    assert( pLeaf == Abc_ObjFanin0(pFanout1) );
+
+                // save the first one
+                if ( pFanout0 == NULL )
+                {
+                    pFanout0 = pFanout1;
+                    Edge0    = Edge1;
+                    continue;
+                }
+                // compare the rings
+                // if they have different number of latches, this is the bug
+                nLatches1 = Seq_NodeCountLats(pFanout0, Edge0);
+                nLatches2 = Seq_NodeCountLats(pFanout1, Edge1);
+                assert( nLatches1 == nLatches2 );
+                assert( nLatches1 == nLatchAfter );
+                assert( nLatches1 > 0 );
+
+                // if they have different initial states, this is the problem
+                if ( !Seq_NodeCompareLats(pFanout0, Edge0, pFanout1, Edge1) )
+                {
+                    CountBad++;
+                    break;
+                }
+                CountAll++;
+            }
+        }
+    }
+    if ( fVerbose )
+        printf( "The number of pairs of edges checked = %d.\n", CountAll );
+    Vec_VecFree( vTotalEdges );
+    return CountBad;
 }
 
 /**Function*************************************************************
@@ -230,7 +362,65 @@ int Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose )
 ***********************************************************************/
 Abc_Ntk_t * Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk )
 {
-    return NULL;
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Seq_Match_t * pMatch;
+    Abc_Ntk_t * pNtkMap; 
+    Vec_Ptr_t * vLeaves;
+    Abc_Obj_t * pObj, * pLatch, * pFaninNew;
+    Seq_Lat_t * pRing;
+    int i;
+
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    // start the network
+    pNtkMap = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+
+    // duplicate the nodes used in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+        pMatch->pAnd->pCopy = Abc_NtkCreateNode( pNtkMap );
+
+    // create and share the latches
+    Seq_NtkShareLatchesMapping( pNtkMap, pNtk, p->vMapAnds, 0 );
+
+    // connect the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        pObj = pMatch->pAnd;
+        // get the leaves of this gate
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // get the BDD of the node
+        pObj->pCopy->pData = Seq_MapMappingConnectBdd_rec( pNtk, pObj->Id << 8, NULL, -1, pObj, vLeaves );
+        Cudd_Ref( pObj->pCopy->pData );
+        // complement the BDD of the cut if it came from the opposite polarity choice cut
+//        if ( Vec_StrEntry(p->vPhase, i) )
+//            pObj->pCopy->pData = Cudd_Not( pObj->pCopy->pData );
+    }
+
+    // set the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        if ( pRing = Seq_NodeGetRing(pObj,0) )
+            pFaninNew = pRing->pLatch;
+        else
+            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
+        pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+
+    // add the latches and their names
+    Abc_NtkAddDummyLatchNames( pNtkMap );
+    Abc_NtkForEachLatch( pNtkMap, pLatch, i )
+    {
+        Vec_PtrPush( pNtkMap->vCis, pLatch );
+        Vec_PtrPush( pNtkMap->vCos, pLatch );
+    }
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkMap, 1 );
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtkMap );
+    if ( !Abc_NtkCheck( pNtkMap ) )
+        fprintf( stdout, "Seq_NtkSeqFpgaMapped(): Network check has failed.\n" );
+    return pNtkMap;
 }
 
 
@@ -250,12 +440,12 @@ int Seq_MapMappingCount( Abc_Ntk_t * pNtk )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
     Vec_Ptr_t * vLeaves;
-    Abc_Obj_t * pAnd;
+    Seq_Match_t * pMatch;
     int i, Counter = 0;
-    Vec_PtrForEachEntry( p->vMapAnds, pAnd, i )
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
     {
         vLeaves = Vec_VecEntry( p->vMapCuts, i );
-        Counter += Seq_MapMappingCount_rec( pNtk, pAnd->Id << 8, vLeaves );
+        Counter += Seq_MapMappingCount_rec( pNtk, pMatch->pAnd->Id << 8, vLeaves );
     }
     return Counter;
 }
@@ -306,7 +496,7 @@ int Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLe
   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 * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int fCompl, int LagCut, Vec_Ptr_t * vLeaves, unsigned uPhase )
 {
     Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1;
     unsigned SeqEdge0, SeqEdge1;
@@ -317,7 +507,17 @@ Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsi
     // if the node is the fanin of the cut, return
     Vec_PtrForEachEntry( vLeaves, pLeaf, i )
         if ( SeqEdge == (unsigned)pLeaf )
-            return pObj->pCopy;
+        {
+//            if ( uPhase & (1 << i) ) // negative phase is required
+//                return pObj->pNext? pObj->pNext : pObj->pCopy;
+//            else // positive phase is required
+//                return pObj->pCopy? pObj->pCopy : pObj->pNext;
+
+            if ( uPhase & (1 << i) ) // negative phase is required
+                return pObj->pNext;
+            else // positive phase is required
+                return pObj->pCopy;
+        }
     // continue unfolding
     assert( Abc_NodeIsAigAnd(pObj) );
     // get new sequential edges
@@ -326,10 +526,10 @@ Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsi
     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 );
+    pObjNew = fTop? (fCompl? pObj->pNext : 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 );
+    pFaninNew0 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, fCompl, LagCut, vLeaves, uPhase );
+    pFaninNew1 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, fCompl, LagCut, vLeaves, uPhase );
     // add the fanins to the node
     Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) );
     Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) );
@@ -342,6 +542,109 @@ Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsi
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_MapMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges )
+{
+    Abc_Obj_t * pObj, * pLeaf;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+            assert( pPrev != NULL );
+            Vec_VecPush( vMapEdges, i, pPrev );
+            return;
+        }
+    }
+    // continue unfolding
+    assert( Abc_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    
+    Seq_MapMappingEdges_rec( pNtk, SeqEdge0, pObj            , vLeaves, vMapEdges );
+    Seq_MapMappingEdges_rec( pNtk, SeqEdge1, Abc_ObjNot(pObj), vLeaves, vMapEdges );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the edges pointing to the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Seq_MapMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves )
+{
+    Seq_Lat_t * pRing;
+    Abc_Obj_t * pObj, * pLeaf, * pFanin, * pFaninNew;
+    unsigned SeqEdge0, SeqEdge1;
+    DdManager * dd = pRoot->pCopy->pNtk->pManFunc;
+    DdNode * bFunc, * bFunc0, * bFunc1;
+    int Lag, i, k;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, add the connection and return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+            assert( pPrev != NULL );
+            if ( pRing = Seq_NodeGetRing(pPrev,Edge) )
+                pFaninNew = pRing->pLatch;
+            else
+                pFaninNew = Abc_ObjFanin(pPrev,Edge)->pCopy;
+
+            // check if the root already has this fanin
+            Abc_ObjForEachFanin( pRoot->pCopy, pFanin, k )
+                if ( pFanin == pFaninNew )
+                    return Cudd_bddIthVar( dd, k );
+            Abc_ObjAddFanin( pRoot->pCopy, pFaninNew );
+            return Cudd_bddIthVar( dd, k );
+        }
+    }
+    // continue unfolding
+    assert( Abc_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_MapMappingConnectBdd_rec( pNtk, SeqEdge0, pObj, 0, pRoot, vLeaves );    Cudd_Ref( bFunc0 );
+    bFunc1 = Seq_MapMappingConnectBdd_rec( pNtk, SeqEdge1, pObj, 1, pRoot, vLeaves );    Cudd_Ref( bFunc1 );
+    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pObj) );
+    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pObj) );
+    // get the BDD of the node
+    bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );  Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( dd, bFunc0 );
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    // return the BDD
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqMapCore_old.c b/src/base/seq/seqMapCore_old.c
new file mode 100644
index 00000000..cc31de10
--- /dev/null
+++ b/src/base/seq/seqMapCore_old.c
@@ -0,0 +1,361 @@
+/**CFile****************************************************************
+
+  FileName    [seqMapCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [The core of SC mapping/retiming package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqMapCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+#include "main.h"
+#include "mio.h"
+#include "mapper.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern Abc_Ntk_t *  Seq_NtkMapDup( Abc_Ntk_t * pNtk );
+extern int          Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose );
+extern Abc_Ntk_t *  Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk );
+
+static int          Seq_MapMappingCount( Abc_Ntk_t * pNtk );
+static int          Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
+static Abc_Obj_t *  Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int fCompl, int LagCut, Vec_Ptr_t * vLeaves, unsigned uPhase );
+static DdNode *     Seq_MapMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
+static void         Seq_MapMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges );
+static void         Seq_MapMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
+static DdNode *     Seq_MapMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs Map mapping and retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Ntk_t * pNtkMap;
+    int RetValue;
+
+    // derive the supergate library
+    if ( Abc_FrameReadLibSuper() == NULL && Abc_FrameReadLibGen() )
+    {
+        printf( "A simple supergate library is derived from gate library \"%s\".\n", 
+            Mio_LibraryReadName(Abc_FrameReadLibGen()) );
+        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen() );
+    }
+    p->pSuperLib   = Abc_FrameReadLibSuper();
+    p->nVarsMax    = Map_SuperLibReadVarsMax(p->pSuperLib);
+    p->nMaxIters   = nMaxIters;
+    p->fStandCells = 1;
+
+    // find the best mapping and retiming for all nodes (p->vLValues, p->vBestCuts, p->vLags)
+    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;
+    }
+
+    // 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, * pFanin, * pFaninNew, * pLeaf;
+    Vec_Ptr_t * vLeaves;
+    unsigned SeqEdge;
+    int i, k, nObjsNew, Lag;
+    
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    // start the expanded network
+    pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
+    Abc_NtkCleanNext(pNtk);
+
+    // start the new sequential AIG manager
+    nObjsNew = 1 + Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk) + Seq_MapMappingCount(pNtk);
+    Seq_Resize( pNtkNew->pManFunc, nObjsNew );
+
+    // duplicate the nodes in the mapping
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+//        Abc_NtkDupObj( pNtkNew, pMatch->pAnd );
+        if ( !pMatch->fCompl )
+            pMatch->pAnd->pCopy = Abc_NtkCreateNode( pNtkNew );
+        else
+            pMatch->pAnd->pNext = Abc_NtkCreateNode( pNtkNew );
+    }
+
+    // recursively construct the internals of each node
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        Seq_MapMappingBuild_rec( pNtkNew, pNtk, pMatch->pAnd->Id << 8, 1, pMatch->fCompl, Seq_NodeGetLag(pMatch->pAnd), vLeaves, pMatch->uPhase );
+    }
+    assert( nObjsNew == pNtkNew->nObjs );
+
+    // set the POs
+//    Abc_NtkFinalize( pNtk, pNtkNew );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        if ( Abc_ObjFaninC0(pObj) )
+            pFaninNew = pFanin->pNext ? pFanin->pNext : Abc_ObjNot(pFanin->pCopy);
+        else
+            pFaninNew = pFanin->pCopy ? pFanin->pCopy : Abc_ObjNot(pFanin->pNext);
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+
+    // duplicate the latches on the PO edges
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_NodeDupLats( pObj->pCopy, pObj, 0 );
+
+    // transfer the mapping info to the new manager
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        // get the leaves of the cut
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        // convert the leaf nodes
+        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
+        {
+            SeqEdge = (unsigned)pLeaf;
+            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+            Lag = (SeqEdge & 255) + Seq_NodeGetLag(pMatch->pAnd) - Seq_NodeGetLag(pLeaf);
+            assert( Lag >= 0 );
+            // translate the old leaf into the leaf in the new network
+//            Vec_PtrWriteEntry( vLeaves, k, (void *)((pLeaf->pCopy->Id << 8) | Lag) );
+
+//            printf( "%d -> %d\n", pLeaf->Id, pLeaf->pCopy->Id );
+        }
+        // convert the root node
+//        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
+        pMatch->pAnd = pMatch->pAnd->pCopy;
+    }
+    pNew = pNtkNew->pManFunc;
+    pNew->nVarsMax  = p->nVarsMax;
+    pNew->vMapAnds  = p->vMapAnds;   p->vMapAnds  = NULL;
+    pNew->vMapCuts  = p->vMapCuts;   p->vMapCuts  = NULL;
+
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Seq_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;
+    Seq_Match_t * pMatch;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
+    {
+        vLeaves = Vec_VecEntry( p->vMapCuts, i );
+        Counter += Seq_MapMappingCount_rec( pNtk, pMatch->pAnd->Id << 8, vLeaves );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nodes in the bag.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj, * pLeaf;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+            return 0;
+    // continue unfolding
+    assert( Abc_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 fCompl, int LagCut, Vec_Ptr_t * vLeaves, unsigned uPhase )
+{
+    Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1;
+    unsigned SeqEdge0, SeqEdge1;
+    int Lag, i;
+    // get the object and the lag
+    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
+    Lag  = SeqEdge & 255;
+    // if the node is the fanin of the cut, return
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( SeqEdge == (unsigned)pLeaf )
+        {
+//            if ( uPhase & (1 << i) ) // negative phase is required
+//                return pObj->pNext? pObj->pNext : Abc_ObjNot(pObj->pCopy);
+//            else // positive phase is required
+//                return pObj->pCopy? pObj->pCopy : Abc_ObjNot(pObj->pNext);
+            return pObj->pCopy? pObj->pCopy : Abc_ObjNot(pObj->pNext);
+        }
+    // 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? (fCompl? pObj->pNext : pObj->pCopy) : Abc_NtkCreateNode( pNtkNew );
+    // solve subproblems
+    pFaninNew0 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, fCompl, LagCut, vLeaves, uPhase );
+    pFaninNew1 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, fCompl, LagCut, vLeaves, uPhase );
+    // add the fanins to the node
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) );
+    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) );
+    Seq_NodeDupLats( pObjNew, pObj, 0 );
+    Seq_NodeDupLats( pObjNew, pObj, 1 );
+    // set the lag of the new node equal to the internal lag plus mapping/retiming lag
+    Seq_NodeSetLag( pObjNew, (char)(Lag + LagCut) );
+//    Seq_NodeSetLag( pObjNew, (char)(Lag) );
+    return pObjNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqMapIter.c b/src/base/seq/seqMapIter.c
index 284fd27d..b93e5dbe 100644
--- a/src/base/seq/seqMapIter.c
+++ b/src/base/seq/seqMapIter.c
@@ -75,11 +75,18 @@ p->timeCuts = clock() - clk;
     // compute canonical forms of the truth tables of the cuts
     Seq_MapCanonicizeTruthTables( pNtk );
 
+    // compute area flows
+//    Seq_MapComputeAreaFlows( pNtk, fVerbose );
+
     // compute the delays
 clk = clock();
     FiBest = Seq_MapRetimeDelayLagsInternal( pNtk, fVerbose );
 p->timeDelay = clock() - clk;
 
+    // clean the marks
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        assert( !pObj->fMarkA && !pObj->fMarkB );
+
     // collect the nodes and cuts used in the mapping
     p->vMapAnds = Vec_PtrAlloc( 1000 );
     p->vMapCuts = Vec_VecAlloc( 1000 );
@@ -133,7 +140,7 @@ float Seq_MapRetimeDelayLagsInternal( Abc_Ntk_t * pNtk, int fVerbose )
     }
 
     // get the upper bound on the clock period
-    FiMax = Delta * (2 + Seq_NtkLevelMax(pNtk));
+    FiMax = Delta * (5 + Seq_NtkLevelMax(pNtk));
     Delta /= 2;
 
     // make sure this clock period is feasible
@@ -155,11 +162,17 @@ float Seq_MapRetimeDelayLagsInternal( Abc_Ntk_t * pNtk, int fVerbose )
         Seq_NodeSetLag( pNode, NodeLag );
         NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueN(pNode), FiBest );
         Seq_NodeSetLagN( pNode, NodeLag );
+//printf( "%6d=(%d,%d) ", pNode->Id, Seq_NodeGetLag(pNode), Seq_NodeGetLagN(pNode) );
+//        if ( Seq_NodeGetLag(pNode) != Seq_NodeGetLagN(pNode) )
+//        {
+//printf( "%6d=(%d,%d) ", pNode->Id, Seq_NodeGetLag(pNode), Seq_NodeGetLagN(pNode) );
+//        }
     }
+//printf( "\n\n" );
 
     // print the result
-    if ( fVerbose )
-    printf( "The best clock period is %6.2f.\n", FiBest );
+//    if ( fVerbose )
+    printf( "The best clock period after mapping/retiming is %6.2f.\n", FiBest );
     return FiBest;
 }
 
@@ -209,7 +222,7 @@ int Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
     // set l-values of all nodes to be minus infinity
     Vec_IntFill( p->vLValues,  p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
     Vec_IntFill( p->vLValuesN, p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
-    Vec_StrFill( p->vUses,     p->nSize, 0             );
+    Vec_StrFill( p->vUses,     p->nSize, 0 );
 
     // set l-values of constants and PIs
     pObj = Abc_NtkObj( pNtk, 0 );
@@ -243,6 +256,7 @@ int Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
             break;
         if ( fChange == 0 )
             break;
+//printf( "\n\n" );
     }
     if ( c == p->nMaxIters )
     {
@@ -265,7 +279,6 @@ int Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
 
 
 
-
 /**Function*************************************************************
 
   Synopsis    [Computes the l-value of the cut.]
@@ -325,6 +338,15 @@ float Seq_MapNodeComputeCut(  Abc_Obj_t * pObj, Cut_Cut_t * pCut, int fCompl, fl
     assert( pCut->nLeaves < 6 );
     // get the canonical truth table of this cut
     uCanon[0] = uCanon[1] = (fCompl? pCut->uCanon0 : pCut->uCanon1);
+    if ( uCanon[0] == 0 || ~uCanon[0] == 0 )
+    {
+        if ( pMatchBest )
+        {
+            memset( pMatchBest, 0, sizeof(Seq_Match_t) );
+            pMatchBest->pCut = pCut;
+        }
+        return (float)0.0;
+    }
     // match the given phase of the cut
     pSuperList = Map_SuperTableLookupC( p->pSuperLib, uCanon );
     // compute the arrival times of each supergate
@@ -340,7 +362,7 @@ float Seq_MapNodeComputeCut(  Abc_Obj_t * pObj, Cut_Cut_t * pCut, int fCompl, fl
             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 )
+            if ( lValueBest > lValueCur )//&& lValueCur > -ABC_INFINITY/2 )
             {
                 lValueBest = lValueCur;
                 if ( pMatchBest )
@@ -348,6 +370,7 @@ float Seq_MapNodeComputeCut(  Abc_Obj_t * pObj, Cut_Cut_t * pCut, int fCompl, fl
             }
         }
     }
+//    assert( lValueBest < ABC_INFINITY/2 );
     return lValueBest;
 }
 
@@ -366,22 +389,23 @@ float Seq_MapNodeComputePhase( Abc_Obj_t * pObj, int fCompl, float Fi, Seq_Match
 {
     Seq_Match_t Match, * pMatchCur = &Match;
     Cut_Cut_t * pList, * pCut;
-    float lValueNew, lValueCut;
+    float lValueBest, lValueCut;
     // get the list of cuts
     pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj );
     // get the arrival time of the best non-trivial cut
-    lValueNew = ABC_INFINITY;
+    lValueBest = ABC_INFINITY;
     for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
     {
         lValueCut = Seq_MapNodeComputeCut( pObj, pCut, fCompl, Fi, pMatchBest? pMatchCur : NULL );
-        if ( lValueNew > lValueCut )
+        if ( lValueBest > lValueCut )
         {
-            lValueNew = lValueCut;
+            lValueBest = lValueCut;
             if ( pMatchBest )
                 *pMatchBest = *pMatchCur;
         }
     }
-    return lValueNew;
+//    assert( lValueBest < ABC_INFINITY/2 );
+    return lValueBest;
 }
 
 /**Function*************************************************************
@@ -434,11 +458,14 @@ int Seq_MapNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, float DelayInv )
     // compare 
     if ( lValue0 <= lValueOld0 + p->fEpsilon && lValue1 <= lValueOld1 + p->fEpsilon )
         return SEQ_UPDATE_NO;
+    assert( lValue0 < ABC_INFINITY/2 );
+    assert( lValue1 < ABC_INFINITY/2 );
     // update the values
     if ( lValue0 > lValueOld0 + p->fEpsilon )
         Seq_NodeSetLValueN( pObj, lValue0 );
     if ( lValue1 > lValueOld1 + p->fEpsilon )
         Seq_NodeSetLValueP( pObj, lValue1 );
+//printf( "%6d=(%4.2f,%4.2f) ", pObj->Id, Seq_NodeGetLValueP(pObj), Seq_NodeGetLValueN(pObj) );
     return SEQ_UPDATE_YES;
 }
 
@@ -460,6 +487,7 @@ float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMappi
     Seq_Match_t * pMatch;
     Abc_Obj_t * pFanin;
     int k, fCompl, Use;
+    float AreaInv = Mio_LibraryReadAreaInv(Abc_FrameReadLibGen());
     float Area;
 
     // get the polarity of the node
@@ -467,42 +495,44 @@ float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMappi
     pAnd   = Abc_ObjRegular(pAnd);
 
     // skip visited nodes
-    if ( fCompl )
-    {
-        if ( pAnd->fMarkB )
+    if ( !fCompl )
+    {  // need the positive polarity
+        if ( pAnd->fMarkA )
             return 0.0;
-        pAnd->fMarkB = 1;
+        pAnd->fMarkA = 1;
     }
     else
-    {
-        if ( pAnd->fMarkA )
+    {   // need the negative polarity
+        if ( pAnd->fMarkB )
             return 0.0;
-        pAnd->fMarkA = 1;
+        pAnd->fMarkB = 1;
     }
 
-    // skip if this is a non-PI node
+    // skip if this is a PI or a constant
     if ( !Abc_NodeIsAigAnd(pAnd) )
     {
         if ( Abc_ObjIsPi(pAnd) && fCompl )
-            return Mio_LibraryReadAreaInv(Abc_FrameReadLibGen());   
+            return AreaInv;   
         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
+    if ( !fCompl && Use == 1 )  // the pos phase is required; only the neg phase is used
     {
-        Area = Seq_MapCollectNode_rec( pAnd, FiBest, vMapping, vMapCuts );
-        return Area + Mio_LibraryReadAreaInv(Abc_FrameReadLibGen()); 
+        Area = Seq_MapCollectNode_rec( Abc_ObjNot(pAnd), FiBest, vMapping, vMapCuts );
+        return Area + AreaInv; 
     }
-    if ( !fCompl && Use == 1 )  // the pos phase is required; the neg phase is used
+    if ( fCompl && Use == 2 )  // the neg phase is required; only the pos phase is used
     {
-        Area = Seq_MapCollectNode_rec( Abc_ObjNot(pAnd), FiBest, vMapping, vMapCuts );
-        return Area + Mio_LibraryReadAreaInv(Abc_FrameReadLibGen()); 
+        Area = Seq_MapCollectNode_rec( pAnd, FiBest, vMapping, vMapCuts );
+        return Area + AreaInv; 
     }
+    // both phases are used; the needed one can be selected
 
     // get the best match
     pMatch = ALLOC( Seq_Match_t, 1 );
+    memset( pMatch, 1, sizeof(Seq_Match_t) );
     Seq_MapNodeComputePhase( pAnd, fCompl, FiBest, pMatch );
     pMatch->pAnd    = pAnd;
     pMatch->fCompl  = fCompl;
@@ -510,7 +540,7 @@ float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMappi
     pMatch->PolUse  = Use;
 
     // call for the fanin cuts
-    Area = pMatch->pSuper->Area;
+    Area = pMatch->pSuper? pMatch->pSuper->Area : (float)0.0;
     for ( k = 0; k < (int)pMatch->pCut->nLeaves; k++ )
     {
         pFanin = Abc_NtkObj( pAnd->pNtk, pMatch->pCut->pLeaves[k] >> 8 );
@@ -524,6 +554,9 @@ float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMappi
     for ( k = 0; k < (int)pMatch->pCut->nLeaves; k++ )
         Vec_VecPush( vMapCuts, Vec_PtrSize(vMapping)-1, (void *)pMatch->pCut->pLeaves[k] );
 
+    // the cut will become unavailable when the cuts are deallocated
+    pMatch->pCut = NULL;
+
     return Area;
 }
 
@@ -551,6 +584,7 @@ void Seq_MapCanonicizeTruthTables( Abc_Ntk_t * pNtk )
     }
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index 154f8dad..f989eefb 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -26,8 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose );
-static Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
-static void        Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init );
+static Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop, Vec_Ptr_t * vFanins );
 static Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq );
 static Abc_Obj_t * Seq_EdgeReconstruct_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode );
 static Abc_Obj_t * Seq_EdgeReconstructPO( Abc_Obj_t * pNode );
@@ -66,7 +65,6 @@ Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fV
     RetValue = Seq_NtkImplementRetiming( pNtkSeq, p->vLags, fVerbose );
     if ( RetValue == 0 )
         printf( "Retiming completed but initial state computation has failed.\n" );
-
 //return pNtkSeq;
 
     // create the final mapped network
@@ -90,7 +88,9 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Abc_Seq_t * p;
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj, * pFanin, * pFanout;
+    Abc_Obj_t * pObj, * pFanin, * pMirror;
+    Vec_Ptr_t * vMapAnds, * vMirrors;
+    Vec_Vec_t * vMapFanins;
     int i, k, RetValue, fHasBdds;
     char * pSop;
 
@@ -126,14 +126,22 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
     Abc_NtkForEachPo( pNtk, pObj, i )
         Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
 
-    // create one AND for each logic node
-    Abc_NtkForEachNode( pNtk, pObj, i )
+    // create one AND for each logic node in the topological order
+    vMapAnds = Abc_NtkDfs( pNtk, 0 );
+    Vec_PtrForEachEntry( vMapAnds, pObj, i )
     {
-        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
+        if ( pObj->Id == 0 )
+        {
+            pObj->pCopy = Abc_NtkConst1(pNtkNew);
             continue;
+        }
         pObj->pCopy = Abc_NtkCreateNode( pNtkNew );
-        pObj->pCopy->pCopy = pObj;
     }
+
+    // make the new seq AIG point to the old network through pNext
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( pObj->pCopy ) pObj->pCopy->pNext = pObj;
+
     // make latches point to the latch fanins
     Abc_NtkForEachLatch( pNtk, pObj, i )
     {
@@ -142,16 +150,15 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
     }
 
     // create internal AND nodes w/o strashing for each logic node (including constants)
-    Abc_NtkForEachNode( pNtk, pObj, i )
+    vMapFanins = Vec_VecStart( Vec_PtrSize(vMapAnds) );
+    Vec_PtrForEachEntry( vMapAnds, pObj, i )
     {
-        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
-            continue;
         // get the SOP of the node
         if ( Abc_NtkHasMapping(pNtk) )
             pSop = Mio_GateReadSop(pObj->pData);
         else
             pSop = pObj->pData;
-        pFanin = Seq_NodeRetimeDerive( pNtkNew, pObj, pSop );
+        pFanin = Seq_NodeRetimeDerive( pNtkNew, pObj, pSop, Vec_VecEntry(vMapFanins, i) );
         Abc_ObjAddFanin( pObj->pCopy, pFanin );
         Abc_ObjAddFanin( pObj->pCopy, pFanin );
     }
@@ -164,20 +171,31 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
     Seq_Resize( p, Abc_NtkObjNumMax(pNtkNew) );
 
     // add the sequential edges
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-        Abc_ObjForEachFanout( pObj, pFanout, k )
+    Vec_PtrForEachEntry( vMapAnds, pObj, i )
+    {
+        vMirrors = Vec_VecEntry( vMapFanins, i );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
         {
-            if ( pObj->pCopy == Abc_ObjFanin0(pFanout->pCopy) )
+            pMirror = Vec_PtrEntry( vMirrors, k );
+            if ( Abc_ObjIsLatch(pFanin) )
             {
-                Seq_NodeInsertFirst( pFanout->pCopy, 0, Abc_LatchInit(pObj) );
-                Seq_NodeInsertFirst( pFanout->pCopy, 1, Abc_LatchInit(pObj) );
-                continue;
+                Seq_NodeInsertFirst( pMirror, 0, Abc_LatchInit(pFanin) );
+                Seq_NodeInsertFirst( pMirror, 1, Abc_LatchInit(pFanin) );
             }
-            Seq_NodeAddEdges_rec( pObj->pCopy, Abc_ObjFanin0(pFanout->pCopy), Abc_LatchInit(pObj) );
         }
+    }
+    // add the sequential edges to the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        if ( Abc_ObjIsLatch(pFanin) )
+            Seq_NodeInsertFirst( pObj->pCopy, 0, Abc_LatchInit(pFanin) );
+    }
+
 
-    // collect the nodes in the topological order
-    p->vMapAnds   = Abc_NtkDfs( pNtk, 0 );
+    // save the fanin/delay info
+    p->vMapAnds   = vMapAnds;
+    p->vMapFanins = vMapFanins;
     p->vMapCuts   = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
     p->vMapDelays = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
     Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
@@ -224,37 +242,6 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
     return pNtkNew;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Add sequential edges.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init )
-{
-    Abc_Obj_t * pFanin;
-    assert( !Abc_ObjIsLatch(pNode) );
-    if ( !Abc_NodeIsAigAnd(pNode) )
-        return;
-    // consider the first fanin
-    pFanin = Abc_ObjFanin0(pNode);
-    if ( pFanin->pCopy == NULL ) // internal node
-        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*************************************************************
 
@@ -267,11 +254,11 @@ void Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop )
+Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop, Vec_Ptr_t * vFanins )
 {
     Dec_Graph_t * pFForm;
     Dec_Node_t * pNode;
-    Abc_Obj_t * pAnd;
+    Abc_Obj_t * pResult, * pFanin, * pMirror;
     int i, nFanins;
 
     // get the number of node's fanins
@@ -280,26 +267,39 @@ Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char *
     if ( nFanins < 2 )
     {
         if ( Abc_SopIsConst1(pSop) )
-            return Abc_NtkConst1(pNtkNew);
+            pFanin = Abc_NtkConst1(pNtkNew);
         else if ( Abc_SopIsConst0(pSop) )
-            return Abc_ObjNot( Abc_NtkConst1(pNtkNew) );
+            pFanin = Abc_ObjNot( Abc_NtkConst1(pNtkNew) );
         else if ( Abc_SopIsBuf(pSop) )
-            return Abc_ObjFanin0(pRoot)->pCopy;
+            pFanin = Abc_ObjFanin0(pRoot)->pCopy;
         else if ( Abc_SopIsInv(pSop) )
-            return Abc_ObjNot( Abc_ObjFanin0(pRoot)->pCopy );
-        assert( 0 );
-        return NULL;
+            pFanin = Abc_ObjNot( Abc_ObjFanin0(pRoot)->pCopy );
+        else
+            assert( 0 );
+        // create the node with these fanins
+        pMirror = Abc_NtkCreateNode( pNtkNew );
+        Abc_ObjAddFanin( pMirror, pFanin );
+        Abc_ObjAddFanin( pMirror, pFanin );
+        Vec_PtrPush( vFanins, pMirror );
+        return pMirror;
     }
 
     // perform factoring
     pFForm = Dec_Factor( pSop );
     // collect the fanins
     Dec_GraphForEachLeaf( pFForm, pNode, i )
-        pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy;
+    {
+        pFanin = Abc_ObjFanin(pRoot,i)->pCopy;
+        pMirror = Abc_NtkCreateNode( pNtkNew );
+        Abc_ObjAddFanin( pMirror, pFanin );
+        Abc_ObjAddFanin( pMirror, pFanin );
+        Vec_PtrPush( vFanins, pMirror );
+        pNode->pFunc = pMirror;
+    }
     // perform strashing
-    pAnd = Dec_GraphToNetworkNoStrash( pNtkNew, pFForm );
+    pResult = Dec_GraphToNetworkNoStrash( pNtkNew, pFForm );
     Dec_GraphFree( pFForm );
-    return pAnd;
+    return pResult;
 }
 
 
@@ -317,8 +317,10 @@ Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char *
 Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
 {
     Abc_Seq_t * p = pNtkSeq->pManFunc;
+    Seq_Lat_t * pRing0, * pRing1;
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj, * pObjNew, * pFanin, * pFaninNew;
+    Abc_Obj_t * pObj, * pObjNew, * pFanin, * pFaninNew, * pMirror;
+    Vec_Ptr_t * vMirrors;
     int i, k;
 
     assert( !Abc_NtkIsSeq(pNtkOld) );
@@ -331,6 +333,14 @@ Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
     // start the final network
     pNtkNew = Abc_NtkStartFrom( pNtkSeq, pNtkOld->ntkType, pNtkOld->ntkFunc );
 
+    // transfer the pointers to the old network
+    if ( Abc_NtkConst1(pNtkOld) ) 
+        Abc_NtkConst1(pNtkOld)->pCopy = Abc_NtkConst1(pNtkNew);
+    Abc_NtkForEachPi( pNtkOld, pObj, i )
+        pObj->pCopy = pObj->pNext->pCopy;
+    Abc_NtkForEachPo( pNtkOld, pObj, i )
+        pObj->pCopy = pObj->pNext->pCopy;
+
     // copy the internal nodes of the old network into the new network
     // transfer the pointers pNktOld->pNtkNew to pNtkSeq->pNtkNew
     Abc_NtkForEachNode( pNtkOld, pObj, i )
@@ -339,25 +349,50 @@ Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
         Abc_NtkDupObj( pNtkNew, pObj );
         pObj->pNext->pCopy = pObj->pCopy;
     }
+    Abc_NtkForEachLatch( pNtkOld, pObj, i )
+        pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
 
     // share the latches
     Seq_NtkShareLatches( pNtkNew, pNtkSeq );
 
     // connect the objects
-    Abc_NtkForEachNode( pNtkOld, pObj, i )
+//    Abc_NtkForEachNode( pNtkOld, pObj, i )
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+    {
+        // pObj is from pNtkSeq - transform to pNtkOld
+        pObj = pObj->pNext;
+        // iterate through the fanins of this node in the old network
+        vMirrors = Vec_VecEntry( p->vMapFanins, i );
         Abc_ObjForEachFanin( pObj, pFanin, k )
         {
-            pFaninNew = Seq_EdgeReconstruct_rec( pFanin->pNext, pObj->pNext );
-            assert( pFaninNew != NULL );
-            Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+            pMirror = Vec_PtrEntry( vMirrors, k );
+            assert( Seq_ObjFaninL0(pMirror) == Seq_ObjFaninL1(pMirror) );
+            pRing0 = Seq_NodeGetRing( pMirror, 0 );
+            pRing1 = Seq_NodeGetRing( pMirror, 1 );
+            if ( pRing0 == NULL )
+            {
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+                continue;
+            }
+//            assert( pRing0->pLatch == pRing1->pLatch );
+            if ( pRing0->pLatch->pData > pRing1->pLatch->pData )
+                Abc_ObjAddFanin( pObj->pCopy, pRing0->pLatch );
+            else
+                Abc_ObjAddFanin( pObj->pCopy, pRing1->pLatch );
         }
+    }
 
     // connect the POs
     Abc_NtkForEachPo( pNtkOld, pObj, i )
     {
-        pFaninNew = Seq_EdgeReconstructPO( pObj->pNext );
+        pFanin = Abc_ObjFanin0(pObj);
+        pRing0 = Seq_NodeGetRing( Abc_NtkPo(pNtkSeq, i), 0 );
+        if ( pRing0 )
+            pFaninNew = pRing0->pLatch;
+        else 
+            pFaninNew = pFanin->pCopy;
         assert( pFaninNew != NULL );
-        Abc_ObjAddFanin( pObj->pNext->pCopy, pFaninNew );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
     }
 
     // clean the result of latch sharing
diff --git a/src/base/seq/seqRetCore_old.c b/src/base/seq/seqRetCore_old.c
new file mode 100644
index 00000000..154f8dad
--- /dev/null
+++ b/src/base/seq/seqRetCore_old.c
@@ -0,0 +1,453 @@
+/**CFile****************************************************************
+
+  FileName    [seqRetCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Construction and manipulation of sequential AIGs.]
+
+  Synopsis    [The core of FPGA mapping/retiming package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: seqRetCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "seqInt.h"
+#include "dec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose );
+static Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
+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 * pNtkSeq );
+static Abc_Obj_t * Seq_EdgeReconstruct_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode );
+static Abc_Obj_t * Seq_EdgeReconstructPO( Abc_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs FPGA mapping and retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose )
+{
+    Abc_Seq_t * p;
+    Abc_Ntk_t * pNtkSeq, * pNtkNew;
+    int RetValue;
+    assert( !Abc_NtkHasAig(pNtk) );
+    // derive the isomorphic seq AIG
+    pNtkSeq = Seq_NtkRetimeDerive( pNtk, fVerbose );
+    p = pNtkSeq->pManFunc;
+    p->nMaxIters = nMaxIters;
+
+    if ( !fInitial )
+        Seq_NtkLatchSetValues( pNtkSeq, ABC_INIT_DC );
+    // find the best mapping and retiming 
+    Seq_NtkRetimeDelayLags( pNtk, pNtkSeq, fVerbose );
+    // implement the retiming
+    RetValue = Seq_NtkImplementRetiming( pNtkSeq, p->vLags, fVerbose );
+    if ( RetValue == 0 )
+        printf( "Retiming completed but initial state computation has failed.\n" );
+
+//return pNtkSeq;
+
+    // create the final mapped network
+    pNtkNew = Seq_NtkRetimeReconstruct( pNtk, pNtkSeq );
+    Abc_NtkDelete( pNtkSeq );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the isomorphic seq AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pFanin, * pFanout;
+    int i, k, RetValue, fHasBdds;
+    char * pSop;
+
+    // make sure it is an AIG without self-feeding latches
+    assert( !Abc_NtkHasAig(pNtk) );
+    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) )
+        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+    assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
+
+    // remove the dangling nodes
+    Abc_NtkCleanup( pNtk, fVerbose );
+
+    // transform logic functions from BDD to SOP
+    if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
+        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 );
+    // copy the names
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+
+    // create one AND for each logic node
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
+            continue;
+        pObj->pCopy = Abc_NtkCreateNode( pNtkNew );
+        pObj->pCopy->pCopy = pObj;
+    }
+    // make latches point to the latch fanins
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        assert( !Abc_ObjIsLatch(Abc_ObjFanin0(pObj)) );
+        pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
+    }
+
+    // create internal AND nodes w/o strashing for each logic node (including constants)
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
+            continue;
+        // get the SOP of the node
+        if ( Abc_NtkHasMapping(pNtk) )
+            pSop = Mio_GateReadSop(pObj->pData);
+        else
+            pSop = pObj->pData;
+        pFanin = Seq_NodeRetimeDerive( pNtkNew, pObj, pSop );
+        Abc_ObjAddFanin( pObj->pCopy, pFanin );
+        Abc_ObjAddFanin( pObj->pCopy, pFanin );
+    }
+    // connect the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
+    
+    // start the storage for initial states
+    p = pNtkNew->pManFunc;
+    Seq_Resize( p, Abc_NtkObjNumMax(pNtkNew) );
+
+    // add the sequential edges
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+        {
+            if ( pObj->pCopy == Abc_ObjFanin0(pFanout->pCopy) )
+            {
+                Seq_NodeInsertFirst( pFanout->pCopy, 0, Abc_LatchInit(pObj) );
+                Seq_NodeInsertFirst( pFanout->pCopy, 1, Abc_LatchInit(pObj) );
+                continue;
+            }
+            Seq_NodeAddEdges_rec( pObj->pCopy, Abc_ObjFanin0(pFanout->pCopy), Abc_LatchInit(pObj) );
+        }
+
+    // collect the nodes in the topological order
+    p->vMapAnds   = Abc_NtkDfs( pNtk, 0 );
+    p->vMapCuts   = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
+    p->vMapDelays = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
+    {
+        // change the node to be the new one
+        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
+        // collect the new fanins of this node
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Vec_VecPush( p->vMapCuts, i, (void *)( (pFanin->pCopy->Id << 8) | Abc_ObjIsLatch(pFanin) ) );
+        // collect the delay info
+        if ( !Abc_NtkHasMapping(pNtk) )
+        {
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                Vec_VecPush( p->vMapDelays, i, (void *)Abc_Float2Int(1.0) );
+        }
+        else
+        {
+            Mio_Pin_t * pPin = Mio_GateReadPins(pObj->pData);
+            float Max, tDelayBlockRise, tDelayBlockFall;
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+            {
+                tDelayBlockRise = (float)Mio_PinReadDelayBlockRise( pPin );  
+                tDelayBlockFall = (float)Mio_PinReadDelayBlockFall( pPin ); 
+                Max = ABC_MAX( tDelayBlockRise, tDelayBlockFall );
+                Vec_VecPush( p->vMapDelays, i, (void *)Abc_Float2Int(Max) );
+                pPin = Mio_PinReadNext(pPin);
+            }
+        }
+    }
+
+    // set the cutset composed of latch drivers
+//    Abc_NtkAigCutsetCopy( pNtk );
+//    Seq_NtkLatchGetEqualFaninNum( pNtkNew );
+
+    // convert the network back into BDDs if this is how it was
+    if ( fHasBdds )
+        Abc_NtkSopToBdd(pNtk);
+
+    // copy EXDC and check correctness
+    if ( pNtk->pExdc )
+        fprintf( stdout, "Warning: EXDC is not copied when converting to sequential AIG.\n" );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Seq_NtkRetimeDerive(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add sequential edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init )
+{
+    Abc_Obj_t * pFanin;
+    assert( !Abc_ObjIsLatch(pNode) );
+    if ( !Abc_NodeIsAigAnd(pNode) )
+        return;
+    // consider the first fanin
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        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    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop )
+{
+    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 )
+    {
+        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    [Reconstructs the network after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
+{
+    Abc_Seq_t * p = pNtkSeq->pManFunc;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pObjNew, * pFanin, * pFaninNew;
+    int i, k;
+
+    assert( !Abc_NtkIsSeq(pNtkOld) );
+    assert( Abc_NtkIsSeq(pNtkSeq) );
+
+    // transfer the pointers pNtkOld->pNtkSeq from pCopy to pNext
+    Abc_NtkForEachObj( pNtkOld, pObj, i )
+        pObj->pNext = pObj->pCopy;
+
+    // start the final network
+    pNtkNew = Abc_NtkStartFrom( pNtkSeq, pNtkOld->ntkType, pNtkOld->ntkFunc );
+
+    // copy the internal nodes of the old network into the new network
+    // transfer the pointers pNktOld->pNtkNew to pNtkSeq->pNtkNew
+    Abc_NtkForEachNode( pNtkOld, pObj, i )
+    {
+        if ( i == 0 ) continue;
+        Abc_NtkDupObj( pNtkNew, pObj );
+        pObj->pNext->pCopy = pObj->pCopy;
+    }
+
+    // share the latches
+    Seq_NtkShareLatches( pNtkNew, pNtkSeq );
+
+    // connect the objects
+    Abc_NtkForEachNode( pNtkOld, pObj, i )
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            pFaninNew = Seq_EdgeReconstruct_rec( pFanin->pNext, pObj->pNext );
+            assert( pFaninNew != NULL );
+            Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        }
+
+    // connect the POs
+    Abc_NtkForEachPo( pNtkOld, pObj, i )
+    {
+        pFaninNew = Seq_EdgeReconstructPO( pObj->pNext );
+        assert( pFaninNew != NULL );
+        Abc_ObjAddFanin( pObj->pNext->pCopy, pFaninNew );
+    }
+
+    // clean the result of latch sharing
+    Seq_NtkShareLatchesClean( pNtkSeq );
+
+    // add the latches and their names
+    Abc_NtkAddDummyLatchNames( pNtkNew );
+    Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
+    {
+        Vec_PtrPush( pNtkNew->vCis, pObjNew );
+        Vec_PtrPush( pNtkNew->vCos, pObjNew );
+    }
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Seq_NtkRetimeReconstruct(): Network check has failed.\n" );
+    return pNtkNew;
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the network after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_EdgeReconstruct_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode )
+{
+    Seq_Lat_t * pRing;
+    Abc_Obj_t * pFanin, * pRes = NULL;
+
+    if ( !Abc_NodeIsAigAnd(pNode) )
+        return NULL;
+
+    // consider the first fanin
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        pRes = Seq_EdgeReconstruct_rec( pGoal, pFanin );
+    else if ( pFanin == pGoal )
+    {
+        if ( pRing = Seq_NodeGetRing( pNode, 0 ) )
+            pRes = pRing->pLatch;
+        else
+            pRes = pFanin->pCopy;
+    }
+    if ( pRes != NULL )
+        return pRes;
+
+    // consider the second fanin
+    pFanin = Abc_ObjFanin1(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        pRes = Seq_EdgeReconstruct_rec( pGoal, pFanin );
+    else if ( pFanin == pGoal )
+    {
+        if ( pRing = Seq_NodeGetRing( pNode, 1 ) )
+            pRes = pRing->pLatch;
+        else
+            pRes = pFanin->pCopy;
+    }
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the network after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_EdgeReconstructPO( Abc_Obj_t * pNode )
+{
+    Seq_Lat_t * pRing;
+    assert( Abc_ObjIsPo(pNode) );
+    if ( pRing = Seq_NodeGetRing( pNode, 0 ) )
+        return pRing->pLatch;
+    else
+        return Abc_ObjFanin0(pNode)->pCopy;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/seq/seqRetIter.c b/src/base/seq/seqRetIter.c
index 1b8ac71c..6fe571f0 100644
--- a/src/base/seq/seqRetIter.c
+++ b/src/base/seq/seqRetIter.c
@@ -31,6 +31,9 @@ static int   Seq_NtkMappingForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
 static int   Seq_NtkNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vDelays );
 static void  Seq_NodeRetimeSetLag_rec( Abc_Obj_t * pNode, char Lag );
 
+static void  Seq_NodePrintInfo( Abc_Obj_t * pNode );
+static void  Seq_NodePrintInfoPlus( Abc_Obj_t * pNode );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -60,6 +63,7 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
     assert( p->vMapAnds );
     assert( p->vMapCuts );
     assert( p->vMapDelays );
+    assert( p->vMapFanins );
 
     // guess the upper bound on the clock period
     if ( Abc_NtkHasMapping(pNtkOld) )
@@ -107,6 +111,11 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
     Vec_StrFill( p->vLags,  p->nSize, 0 );
     Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
     {
+        if ( Vec_PtrSize( Vec_VecEntry(p->vMapCuts, i) ) == 0 )
+        {
+            Seq_NodeSetLag( pNode, 0 );
+            continue;
+        }
         NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueP(pNode), FiBest );
         Seq_NodeRetimeSetLag_rec( pNode, NodeLag );
     }
@@ -117,6 +126,8 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
     // print the result
     if ( fVerbose )
         printf( "The best clock period is %6.2f.\n", FiBest );
+
+//    Seq_NodePrintInfo( Abc_NtkObj(pNtk, 847) );
 }
 
 /**Function*************************************************************
@@ -181,6 +192,11 @@ int Seq_NtkMappingForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
             Counter++;
             vLeaves = Vec_VecEntry( p->vMapCuts, i );
             vDelays = Vec_VecEntry( p->vMapDelays, i );
+            if ( Vec_PtrSize(vLeaves) == 0 )
+            {
+                Seq_NodeSetLValueP( pObj, 0.0 );
+                continue;
+            }
             RetValue = Seq_NtkNodeUpdateLValue( pObj, Fi, vLeaves, vDelays );
             if ( RetValue == SEQ_UPDATE_YES ) 
                 fChange = 1;
@@ -293,6 +309,72 @@ void Seq_NodeRetimeSetLag_rec( Abc_Obj_t * pNode, char Lag )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Add sequential edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodePrintInfo( Abc_Obj_t * pNode )
+{
+    Abc_Seq_t * p = pNode->pNtk->pManFunc;
+    Abc_Obj_t * pFanin, * pObj, * pLeaf;
+    Vec_Ptr_t * vLeaves;
+    unsigned SeqEdge;
+    int i, Number;
+
+    // print the node
+    printf( "    Node      = %6d.  LValue = %7.2f.  Lag = %2d.\n", 
+        pNode->Id, Seq_NodeGetLValueP(pNode), Seq_NodeGetLag(pNode) );
+
+    // find the number
+    Vec_PtrForEachEntry( p->vMapAnds, pObj, Number )
+        if ( pObj == pNode )
+            break;
+
+    // get the leaves
+    vLeaves = Vec_VecEntry( p->vMapCuts, Number );
+
+    // print the leaves
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+    {
+        SeqEdge   = (unsigned)pLeaf;
+        pFanin    = Abc_NtkObj( pNode->pNtk, SeqEdge >> 8 );
+        // print the leaf
+        printf( "    Fanin%d(%d) = %6d.  LValue = %7.2f.  Lag = %2d.\n", i, SeqEdge & 255,
+            pFanin->Id, Seq_NodeGetLValueP(pFanin), Seq_NodeGetLag(pFanin) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add sequential edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NodePrintInfoPlus( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    printf( "CENTRAL NODE:\n" );
+    Seq_NodePrintInfo( pNode );
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+    {
+        printf( "FANOUT%d:\n", i );
+        Seq_NodePrintInfo( pFanout );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqShare.c b/src/base/seq/seqShare.c
index 417dcc83..fd2e8189 100644
--- a/src/base/seq/seqShare.c
+++ b/src/base/seq/seqShare.c
@@ -275,15 +275,17 @@ Abc_Obj_t * Seq_NtkShareLatches_rec( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj, Seq_Lat
 ***********************************************************************/
 void Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk )
 { 
-    Abc_Obj_t * pObj;
+    Abc_Obj_t * pObj, * pFanin;
     stmm_table * tLatchMap;
     int i;
     assert( Abc_NtkIsSeq( pNtk ) );
     tLatchMap = stmm_init_table( stmm_ptrcmp, stmm_ptrhash );
     Abc_AigForEachAnd( pNtk, pObj, i )
     {
-        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 );
+        pFanin = Abc_ObjFanin0(pObj);
+        Seq_NtkShareLatches_rec( pNtkNew, pFanin->pCopy, Seq_NodeGetRing(pObj,0), Seq_NodeCountLats(pObj,0), tLatchMap );
+        pFanin = Abc_ObjFanin1(pObj);
+        Seq_NtkShareLatches_rec( pNtkNew, pFanin->pCopy, Seq_NodeGetRing(pObj,1), Seq_NodeCountLats(pObj,1), tLatchMap );
     }
     Abc_NtkForEachPo( pNtk, pObj, i )
         Seq_NtkShareLatches_rec( pNtkNew, Abc_ObjFanin0(pObj)->pCopy, Seq_NodeGetRing(pObj,0), Seq_NodeCountLats(pObj,0), tLatchMap );
@@ -303,22 +305,36 @@ void Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds )
+void Seq_NtkShareLatchesMapping( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds, int fFpga )
 { 
+    Seq_Match_t * pMatch;
     Abc_Obj_t * pObj, * pFanout;
     stmm_table * tLatchMap;
-    int i, k, nOldNodes;
+    Vec_Ptr_t * vNodes;
+    int i, k;
     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) );
+
+    // create the array of all nodes with sharable fanouts
+    vNodes = Vec_PtrAlloc( 100 );
+    Vec_PtrPush( vNodes, Abc_NtkConst1(pNtk) );
     Abc_NtkForEachPi( pNtk, pObj, i )
-        Vec_PtrPush( vMapAnds, pObj );
+        Vec_PtrPush( vNodes, pObj );
+    if ( fFpga )
+    {
+        Vec_PtrForEachEntry( vMapAnds, pObj, i )
+            Vec_PtrPush( vNodes, pObj );
+    }
+    else 
+    {
+        Vec_PtrForEachEntry( vMapAnds, pMatch, i )
+            Vec_PtrPush( vNodes, pMatch->pAnd );
+    }
+
     // process nodes used in the mapping
-    Vec_PtrForEachEntry( vMapAnds, pObj, i )
+    Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         // make sure the label is clean
         Abc_ObjForEachFanout( pObj, pFanout, k )
@@ -339,7 +355,7 @@ void Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t *
     }
     stmm_free_table( tLatchMap );
     // return to the old array
-    Vec_PtrShrink( vMapAnds, nOldNodes );
+    Vec_PtrFree( vNodes );
 }
 
 /**Function*************************************************************
diff --git a/src/base/seq/seqUtil.c b/src/base/seq/seqUtil.c
index a3b8bc84..d9fad0ea 100644
--- a/src/base/seq/seqUtil.c
+++ b/src/base/seq/seqUtil.c
@@ -417,6 +417,50 @@ int Seq_NtkCountNodesAboveLimit( Abc_Ntk_t * pNtk, int Limit )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes area flows.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_MapComputeAreaFlows( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Seq_t * p = pNtk->pManFunc;
+    Abc_Obj_t * pObj;
+    float AFlow;
+    int i, c;
+
+    assert( Abc_NtkIsSeq(pNtk) );
+
+    Vec_IntFill( p->vAFlows, p->nSize, Abc_Float2Int( (float)0.0 ) );
+
+    // update all values iteratively
+    for ( c = 0; c < 7; c++ )
+    {
+        Abc_AigForEachAnd( pNtk, pObj, i )
+        {
+            AFlow = (float)1.0 + Seq_NodeGetFlow( Abc_ObjFanin0(pObj) ) + Seq_NodeGetFlow( Abc_ObjFanin1(pObj) );
+            AFlow /= Abc_ObjFanoutNum(pObj);
+            pObj->pNext = (void *)Abc_Float2Int( AFlow );
+        }
+        Abc_AigForEachAnd( pNtk, pObj, i )
+        {
+            AFlow = Abc_Int2Float( (int)pObj->pNext );
+            pObj->pNext = NULL;
+            Seq_NodeSetFlow( pObj, AFlow );
+
+//            printf( "%5d : %6.1f\n", pObj->Id, Seq_NodeGetFlow(pObj) );
+        }
+//        printf( "\n" );
+    }
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////