Version abc51121

21 files changed, 417 insertions, 171 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 58c9c65b..1985f4c8 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -312,11 +312,6 @@ static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj )      { return (A
 static inline bool        Abc_ObjFaninC( Abc_Obj_t * pObj, int i )   { return pObj->vFanins.pArray[i].fCompl;                               }
 static inline bool        Abc_ObjFaninC0( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[0].fCompl;                               }
 static inline bool        Abc_ObjFaninC1( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[1].fCompl;                               }
-static inline int         Abc_ObjFaninL( Abc_Obj_t * pObj, int i )   { return pObj->vFanins.pArray[i].nLats;                                }
-static inline int         Abc_ObjFaninL0( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[0].nLats;                                }
-static inline int         Abc_ObjFaninL1( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[1].nLats;                                }
-static inline int         Abc_ObjFaninLMin( Abc_Obj_t * pObj )       {  assert( Abc_ObjIsNode(pObj) ); return ABC_MIN( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
-static inline int         Abc_ObjFaninLMax( Abc_Obj_t * pObj )       {  assert( Abc_ObjIsNode(pObj) ); return ABC_MAX( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
 static inline Abc_Obj_t * Abc_ObjChild( Abc_Obj_t * pObj, int i )    { return Abc_ObjNotCond( Abc_ObjFanin(pObj,i), Abc_ObjFaninC(pObj,i) );}
 static inline Abc_Obj_t * Abc_ObjChild0( Abc_Obj_t * pObj )          { return Abc_ObjNotCond( Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );  }
 static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj )          { return Abc_ObjNotCond( Abc_ObjFanin1(pObj), Abc_ObjFaninC1(pObj) );  }
@@ -325,15 +320,6 @@ static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj )      { return Ab
 static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) );  }
 static inline void        Abc_ObjSetFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl = 1;                               }
 static inline void        Abc_ObjXorFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl ^= 1;                              }
-static inline void        Abc_ObjSetFaninL( Abc_Obj_t * pObj, int i, int nLats )  { pObj->vFanins.pArray[i].nLats = nLats;               }
-static inline void        Abc_ObjSetFaninL0( Abc_Obj_t * pObj, int nLats )        { pObj->vFanins.pArray[0].nLats = nLats;               }
-static inline void        Abc_ObjSetFaninL1( Abc_Obj_t * pObj, int nLats )        { pObj->vFanins.pArray[1].nLats = nLats;               }
-static inline void        Abc_ObjAddFaninL( Abc_Obj_t * pObj, int i, int nLats )  { pObj->vFanins.pArray[i].nLats += nLats;              }
-static inline void        Abc_ObjAddFaninL0( Abc_Obj_t * pObj, int nLats )        { pObj->vFanins.pArray[0].nLats += nLats;              }
-static inline void        Abc_ObjAddFaninL1( Abc_Obj_t * pObj, int nLats )        { pObj->vFanins.pArray[1].nLats += nLats;              }
-static inline int         Abc_ObjFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout )               {  return Abc_ObjFaninL( pFanout, Abc_ObjFanoutEdgeNum(pObj,pFanout) );     }
-static inline void        Abc_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats ) {  Abc_ObjSetFaninL( pFanout, Abc_ObjFanoutEdgeNum(pObj,pFanout), nLats );  }
-static inline void        Abc_ObjAddFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats ) {  Abc_ObjAddFaninL( pFanout, Abc_ObjFanoutEdgeNum(pObj,pFanout), nLats );  }
 
 // checking the node type
 static inline bool        Abc_NodeIsAigAnd( Abc_Obj_t * pNode )      { assert(Abc_NtkHasAig(pNode->pNtk));           return Abc_ObjFaninNum(pNode) == 2;                         }
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 4f718bbf..983d41e4 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "seqInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -146,14 +147,13 @@ void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFa
     }
     // remember the attributes of the old fanin
     fCompl = Abc_ObjFaninC(pObj, iFanin);
-    nLats  = Abc_ObjFaninL(pObj, iFanin);
     // replace the old fanin entry by the new fanin entry (removes attributes)
     Vec_FanWriteEntry( &pObj->vFanins, iFanin, Vec_Int2Fan(pFaninNewR->Id) );
     // set the attributes of the new fanin
     if ( fCompl ^ Abc_ObjIsComplement(pFaninNew) )
         Abc_ObjSetFaninC( pObj, iFanin );
-    if ( nLats )
-        Abc_ObjSetFaninL( pObj, iFanin, nLats );
+    if ( Abc_NtkIsSeq(pObj->pNtk) && (nLats = Seq_ObjFaninL(pObj, iFanin)) )
+        Seq_ObjSetFaninL( pObj, iFanin, nLats );
     // update the fanout of the fanin
     if ( !Vec_FanDeleteEntry( &pFaninOld->vFanouts, pObj->Id ) )
     {
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 1afc2038..9d649f6f 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -22,7 +22,7 @@
 #include "abcInt.h"
 #include "main.h"
 #include "mio.h"
-#include "seq.h"
+#include "seqInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -322,7 +322,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
                 Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
                 if ( Abc_ObjFaninC(pObj, k) )
                     Abc_ObjSetFaninC( pObj->pCopy, k );
-                if ( Abc_ObjFaninL(pObj, k) > 0 )
+                if ( Seq_ObjFaninL(pObj, k) )
                     Seq_NodeDupLats( pObj->pCopy, pObj, k );
             }
         }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8c939083..f7e7f763 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -901,7 +901,7 @@ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsBddLogic(pNtk) )
     {
-        fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks (run \"bdd\").\n" );
+        fprintf( pErr, "Visualizing Karnaugh map works for BDD logic networks (run \"bdd\").\n" );
         return 1;
     }
     if ( argc > util_optind + 1 )
@@ -1388,6 +1388,11 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Balancing cannot be applied to a sequential AIG.\n" );
+        return 1;
+    }
 
     // get the new network
     if ( Abc_NtkIsStrash(pNtk) )
@@ -2731,7 +2736,7 @@ int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( stdout, "This command works only for AIGs (run \"strash\").\n" );
+        fprintf( stdout, "Extracting sequential don't-cares works only for AIGs (run \"strash\").\n" );
         return 0;
     }
     if ( !Abc_NtkExtractSequentialDcs( pNtk, fVerbose ) )
@@ -4279,7 +4284,7 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Works only for the AIG representation (run \"strash\").\n" );
+        fprintf( pErr, "Superchoicing works only for the AIG representation (run \"strash\").\n" );
         return 1;
     }
 
@@ -4736,7 +4741,7 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c;
+    int c, nLoops;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -4769,14 +4774,14 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Works only for AIG (run \"strash\").\n" );
+        fprintf( pErr, "Conversion to sequential AIG works only for combinational AIGs (run \"strash\").\n" );
         return 1;
     }
 
-    if ( Abc_NtkCountSelfFeedLatches(pNtk) )
+    if ( nLoops = Abc_NtkCountSelfFeedLatches(pNtk) )
     {
-        fprintf( pErr, "Sequential AIG cannot be created for designs with self-feeding latches.\n" );
-        return 1;
+        fprintf( pErr, "Cannot create sequential AIG because the network contains %d self-feeding latches.\n", nLoops );
+        return 0;
     }
 
     // get the new network
@@ -4844,7 +4849,7 @@ int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsSeq(pNtk) )
     {
-        fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
+        fprintf( pErr, "Conversion to combinational AIG works only for sequential AIG (run \"seq\").\n" );
         return 1;
     }
 
@@ -4891,6 +4896,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fBackward;
     int fInitial;
     int fVerbose;
+    int nLoops;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -4933,8 +4939,14 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsSeq(pNtk) )
     {
-        fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
-        return 1;
+        fprintf( pErr, "Retiming works only for sequential AIG (run \"seq\").\n" );
+        return 0;
+    }
+
+    if ( nLoops = Abc_NtkCountSelfFeedLatches(pNtk) )
+    {
+        fprintf( pErr, "Cannot retime because the network contains %d self-feeding latches.\n", nLoops );
+        return 0;
     }
 
     // get the new network
@@ -4979,7 +4991,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fVerbose = 1;
+    fVerbose = 0;
     util_getopt_reset();
     while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
     {
@@ -5003,20 +5015,16 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsSeq(pNtk) )
     {
-        fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
-        return 1;
+        fprintf( pErr, "Sequential FPGA mapping works only for sequential AIG (run \"seq\").\n" );
+        return 0;
     }
 
-//    printf( "This command is not yet implemented.\n" );
-//    return 0;
-
-
     // get the new network
     pNtkRes = Seq_NtkFpgaMapRetime( pNtk, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
-        return 1;
+        return 0;
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -5078,7 +5086,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsSeq(pNtk) )
     {
-        fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
+        fprintf( pErr, "Sequential standard cell mapping works only for sequential AIG (run \"seq\").\n" );
         return 1;
     }
 
@@ -5178,7 +5186,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Abc_NtkIsSeq(pNtk) )
     {
-        fprintf( pErr, "Works only for combinational networks (run \"unseq\").\n" );
+        fprintf( pErr, "Sequential sweep works only for combinational networks (run \"unseq\").\n" );
         return 1;
     }
 
@@ -5190,7 +5198,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Works only for structurally hashed networks (run \"strash\").\n" );
+        fprintf( pErr, "Sequential sweep works only for structurally hashed networks (run \"strash\").\n" );
         return 1;
     }
 
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 8bc2c9b4..f285495c 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "cut.h"
+#include "seqInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -196,7 +197,10 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     pParams->nCutSet = Abc_NtkCutSetNodeNum( pNtk );
     p = Cut_ManStart( pParams );
 
-    // set cuts for PIs
+    // set cuts for the constant node and the PIs
+    pObj = Abc_NtkConst1(pNtk);
+    if ( Abc_ObjFanoutNum(pObj) > 0 )
+        Cut_NodeSetTriv( p, pObj->Id );
     Abc_NtkForEachPi( pNtk, pObj, i )
         Cut_NodeSetTriv( p, pObj->Id );
     // label the cutset nodes and set their number in the array
@@ -240,8 +244,11 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     // unlabel the cutset nodes
     Abc_SeqForEachCutsetNode( pNtk, pObj, i )
         pObj->fMarkC = 0;
+if ( pParams->fVerbose )
+{
 PRT( "Total", clock() - clk );
 printf( "Converged after %d iterations.\n", nIters );
+}
 //Abc_NtkPrintCuts( p, pNtk, 1 );
     return p;
 }
@@ -306,7 +313,7 @@ void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fTriv )
     fTriv     = pObj->fMarkC ? 0 : fTriv;
     CutSetNum = pObj->fMarkC ? (int)pObj->pCopy : -1;
     Cut_NodeComputeCutsSeq( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
-        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj), fTriv, CutSetNum );  
+        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), Seq_ObjFaninL0(pObj), Seq_ObjFaninL1(pObj), fTriv, CutSetNum );  
 }
 
 /**Function*************************************************************
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 06f32f38..7343582b 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "io.h"
-#include "seq.h"
+#include "seqInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -315,7 +315,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
             fprintf( pFile, "Node%d%s",  Abc_ObjFaninId0(pNode), (Abc_ObjIsLatch(Abc_ObjFanin0(pNode))? "_out":"") );
             fprintf( pFile, " [" );
             fprintf( pFile, "style = %s", Abc_ObjFaninC0(pNode)? "dotted" : "bold" );
-            if ( Abc_ObjFaninL0(pNode) > 0 )
+            if ( Seq_ObjFaninL0(pNode) > 0 )
             fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) );
             fprintf( pFile, "]" );
             fprintf( pFile, ";\n" );
@@ -330,7 +330,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
             fprintf( pFile, "Node%d%s",  Abc_ObjFaninId1(pNode), (Abc_ObjIsLatch(Abc_ObjFanin1(pNode))? "_out":"") );
             fprintf( pFile, " [" );
             fprintf( pFile, "style = %s", Abc_ObjFaninC1(pNode)? "dotted" : "bold" );
-            if ( Abc_ObjFaninL1(pNode) > 0 )
+            if ( Seq_ObjFaninL1(pNode) > 0 )
             fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) );
             fprintf( pFile, "]" );
             fprintf( pFile, ";\n" );
diff --git a/src/base/io/ioWriteList.c b/src/base/io/ioWriteList.c
index fefe9b0e..ab216eb3 100644
--- a/src/base/io/ioWriteList.c
+++ b/src/base/io/ioWriteList.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "io.h"
+#include "seqInt.h"
 
 /*
 -------- Original Message --------
@@ -156,7 +157,7 @@ void Io_WriteListEdge( FILE * pFile, Abc_Obj_t * pObj )
     fprintf( pFile, "%-10s >    ", Abc_ObjName(pObj) );
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
-        fprintf( pFile, " %s ([%s_to_%s] = %d)", Abc_ObjName(pFanout), Abc_ObjName(pObj), Abc_ObjName(pFanout), Abc_ObjFanoutL(pObj, pFanout) );
+        fprintf( pFile, " %s ([%s_to_%s] = %d)", Abc_ObjName(pFanout), Abc_ObjName(pObj), Abc_ObjName(pFanout), Seq_ObjFanoutL(pObj, pFanout) );
         if ( i == Abc_ObjFanoutNum(pObj) - 1 )
             fprintf( pFile, "." );
         else
diff --git a/src/base/seq/seq.h b/src/base/seq/seq.h
index cbffe0bd..2e1fef91 100644
--- a/src/base/seq/seq.h
+++ b/src/base/seq/seq.h
@@ -17,7 +17,7 @@
   Revision    [$Id: seq.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
- 
+
 #ifndef __SEQ_H__
 #define __SEQ_H__
 
@@ -68,6 +68,7 @@ extern int             Seq_NtkLatchNum( Abc_Ntk_t * pNtk );
 extern int             Seq_NtkLatchNumMax( Abc_Ntk_t * pNtk );
 extern int             Seq_NtkLatchNumShared( Abc_Ntk_t * pNtk );
 extern void            Seq_NtkLatchGetInitNums( Abc_Ntk_t * pNtk, int * pInits );
+extern int             Seq_NtkLatchGetEqualFaninNum( Abc_Ntk_t * pNtk );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c
index 0816c673..05eebe15 100644
--- a/src/base/seq/seqCreate.c
+++ b/src/base/seq/seqCreate.c
@@ -158,6 +158,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
 
     // set the cutset composed of latch drivers
     Abc_NtkAigCutsetCopy( pNtk );
+    Seq_NtkLatchGetEqualFaninNum( pNtkNew );
 
     // copy EXDC and check correctness
     if ( pNtkNew->pExdc )
@@ -280,7 +281,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
         if ( Abc_ObjFaninNum(pObj) == 0 )
             continue;
         // create the edge
-        pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin0(pObj), Seq_NodeGetRing(pObj,0), Abc_ObjFaninL0(pObj) );
+        pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin0(pObj), Seq_NodeGetRing(pObj,0), Seq_ObjFaninL0(pObj) );
         Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
         if ( Abc_ObjFaninNum(pObj) == 1 )
         {
@@ -290,7 +291,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
             continue;
         }
         // create the edge
-        pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin1(pObj), Seq_NodeGetRing(pObj,1), Abc_ObjFaninL1(pObj) );
+        pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin1(pObj), Seq_NodeGetRing(pObj,1), Seq_ObjFaninL1(pObj) );
         Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
         // the complemented edges are subsumed by the node function
     }
diff --git a/src/base/seq/seqFpgaCore.c b/src/base/seq/seqFpgaCore.c
index a40caf34..cb000ab9 100644
--- a/src/base/seq/seqFpgaCore.c
+++ b/src/base/seq/seqFpgaCore.c
@@ -25,13 +25,13 @@
 ////////////////////////////////////////////////////////////////////////
 
 static Abc_Ntk_t *  Seq_NtkFpgaDup( Abc_Ntk_t * pNtk );
-static int          Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk );
+static int          Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk, int fVerbose );
 static Abc_Ntk_t *  Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtkNew );
 static int          Seq_FpgaMappingCount( Abc_Ntk_t * pNtk );
 static int          Seq_FpgaMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
 static DdNode *     Seq_FpgaMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
 static void         Seq_FpgaMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges );
-static Abc_Obj_t *  Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, Vec_Ptr_t * vLeaves );
+static Abc_Obj_t *  Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -57,12 +57,16 @@ Abc_Ntk_t * Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int fVerbose )
     Seq_FpgaMappingDelays( pNtk, fVerbose );
     // duplicate the nodes contained in multiple cuts
     pNtkNew = Seq_NtkFpgaDup( 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_NtkFpgaInitCompatible( pNtkNew ) )
+    if ( RetValue = Seq_NtkFpgaInitCompatible( pNtkNew, fVerbose ) )
     {
         printf( "The number of LUTs with incompatible edges = %d.\n", RetValue );
         Abc_NtkDelete( pNtkNew );
@@ -93,7 +97,7 @@ Abc_Ntk_t * Seq_NtkFpgaDup( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj, * pLeaf;
     Vec_Ptr_t * vLeaves;
     unsigned SeqEdge;
-    int i, k, nObjsNew;
+    int i, k, nObjsNew, Lag;
     
     assert( Abc_NtkIsSeq(pNtk) );
 
@@ -112,13 +116,15 @@ Abc_Ntk_t * Seq_NtkFpgaDup( Abc_Ntk_t * pNtk )
     Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
     {
         vLeaves = Vec_VecEntry( p->vMapCuts, i );
-        Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, pObj->Id << 8, 1, vLeaves );
+        Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, pObj->Id << 8, 1, Seq_NodeGetLag(pObj), vLeaves );
     }
     assert( nObjsNew == pNtkNew->nObjs );
 
     // set the POs
     Abc_NtkFinalize( pNtk, pNtkNew );
-
+    // duplicate the latches on the PO edges
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_NodeDupLats( pObj->pCopy, pObj, 0 );
 //Abc_NtkShowAig( pNtkNew );
 
     // transfer the mapping info to the new manager
@@ -133,8 +139,11 @@ 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) | (SeqEdge & 255)) );
+            Vec_PtrWriteEntry( vLeaves, k, (void *)((pLeaf->pCopy->Id << 8) | Lag) );
 //            printf( "%d -> %d\n", pLeaf->Id, pLeaf->pCopy->Id );
         }
     }
@@ -163,15 +172,15 @@ Abc_Ntk_t * Seq_NtkFpgaDup( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk )
+int Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
     Abc_Obj_t * pAnd, * pLeaf, * pFanout0, * pFanout1;
     Vec_Vec_t * vTotalEdges;
     Vec_Ptr_t * vLeaves, * vEdges;
-    int i, k, m, Edge0, Edge1, nLatchBefore, nLatchAfter, nLatches1, nLatches2;
+    int i, k, m, Edge0, Edge1, nLatchAfter, nLatches1, nLatches2;
     unsigned SeqEdge;
-    int CountBad = 0;
+    int CountBad = 0, CountAll = 0;
 
     vTotalEdges = Vec_VecStart( p->nVarsMax );
     // go through all the nodes (cuts) used in the mapping
@@ -191,11 +200,7 @@ int Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk )
         {
             SeqEdge = (unsigned)pLeaf;
             pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
-            nLatchBefore = SeqEdge & 255;
-
-            // get the resulting lag of this node
-            nLatchAfter = nLatchBefore + Seq_NodeGetLag(pAnd) - Seq_NodeGetLag(pLeaf);
-            assert( nLatchAfter >= 0 );
+            nLatchAfter = SeqEdge & 255;
             if ( nLatchAfter == 0 )
                 continue;
 
@@ -226,6 +231,7 @@ int Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk )
                 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
@@ -234,9 +240,12 @@ int Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk )
                     CountBad++;
                     break;
                 }
+                CountAll++;
             }
         }
     }
+    if ( fVerbose )
+        printf( "The number of pairs of edges checked = %d.\n", CountAll );
     Vec_VecFree( vTotalEdges );
     return CountBad;
 }
@@ -260,7 +269,7 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
     Vec_Vec_t * vTotalEdges;
     Vec_Ptr_t * vLeaves, * vMapEdges;
     Abc_Obj_t * pObj, * pAnd, * pLeaf, * pFanout, * pFanin, * pLatch;
-    int i, k, m, Edge, nLatches, nLatchBefore, nLatchAfter;
+    int i, k, m, Edge, nLatches, nLatchAfter;
     unsigned SeqEdge;
 
     assert( Abc_NtkIsSeq(pNtk) );
@@ -293,11 +302,7 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
         {
             SeqEdge = (unsigned)pLeaf;
             pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
-            nLatchBefore = SeqEdge & 255;
-
-            // get the resulting lag of this node
-            nLatchAfter = nLatchBefore + Seq_NodeGetLag(pAnd) - Seq_NodeGetLag(pLeaf);
-            assert( nLatchAfter >= 0 );
+            nLatchAfter = SeqEdge & 255;
             if ( nLatchAfter == 0 )
             {
                 // add the fanin
@@ -316,6 +321,7 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
             else
                 assert( pLeaf == Abc_ObjFanin0(pFanout) );
             nLatches = Seq_NodeCountLats(pFanout, Edge);
+            assert( nLatches == nLatchAfter );
             assert( nLatches > 0 );
 
             // for each implicit latch add the real latch
@@ -338,7 +344,9 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
     Abc_NtkForEachPo( pNtk, pObj, i )
     {
         pFanin = Abc_ObjFanin0(pObj)->pCopy;
-        if ( Abc_ObjFaninL0(pObj) > 0 )
+        nLatches = Seq_NodeCountLats(pObj, 0);
+        assert( nLatches == Seq_ObjFaninL0(pObj) );
+        if ( nLatches > 0 )
         {
             pRing = Seq_NodeGetRing(pObj, 0);
             for ( m = 0, pLat = Seq_LatPrev(pRing); m < nLatches; m++, pLat = Seq_LatPrev(pLat) )
@@ -421,10 +429,10 @@ int Seq_FpgaMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vL
     // continue unfolding
     assert( Abc_NodeIsAigAnd(pObj) );
     // get new sequential edges
-    assert( Lag + Abc_ObjFaninL0(pObj) < 255 );
-    assert( Lag + Abc_ObjFaninL1(pObj) < 255 );
-    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Abc_ObjFaninL0(pObj);
-    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Abc_ObjFaninL1(pObj);
+    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_FpgaMappingCount_rec( pNtk, SeqEdge0, vLeaves ) + 
         Seq_FpgaMappingCount_rec( pNtk, SeqEdge1, vLeaves );
@@ -457,17 +465,21 @@ DdNode * Seq_FpgaMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqE
     // continue unfolding
     assert( Abc_NodeIsAigAnd(pObj) );
     // get new sequential edges
-    assert( Lag + Abc_ObjFaninL0(pObj) < 255 );
-    assert( Lag + Abc_ObjFaninL1(pObj) < 255 );
-    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Abc_ObjFaninL0(pObj);
-    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Abc_ObjFaninL1(pObj);
+    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_FpgaMappingBdd_rec( dd, pNtk, SeqEdge0, vLeaves );    Cudd_Ref( bFunc0 );
     bFunc1 = Seq_FpgaMappingBdd_rec( dd, pNtk, SeqEdge1, 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, Cudd_NotCond(bFunc0, Abc_ObjFaninC0(pObj)), Cudd_NotCond(bFunc1, Abc_ObjFaninC1(pObj)) );  Cudd_Ref( bFunc );
+    bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );  Cudd_Ref( bFunc );
     Cudd_RecursiveDeref( dd, bFunc0 );
     Cudd_RecursiveDeref( dd, bFunc1 );
+    // complement the function if the node is created from the complimented cut
+    // ...
     // return the BDD
     Cudd_Deref( bFunc );
     return bFunc;
@@ -505,10 +517,10 @@ void Seq_FpgaMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * p
     // continue unfolding
     assert( Abc_NodeIsAigAnd(pObj) );
     // get new sequential edges
-    assert( Lag + Abc_ObjFaninL0(pObj) < 255 );
-    assert( Lag + Abc_ObjFaninL1(pObj) < 255 );
-    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Abc_ObjFaninL0(pObj);
-    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Abc_ObjFaninL1(pObj);
+    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_FpgaMappingEdges_rec( pNtk, SeqEdge0, pObj            , vLeaves, vMapEdges );
     Seq_FpgaMappingEdges_rec( pNtk, SeqEdge1, Abc_ObjNot(pObj), vLeaves, vMapEdges );
@@ -525,11 +537,11 @@ void Seq_FpgaMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * p
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, Vec_Ptr_t * vLeaves )
+Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves )
 {
     Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1;
     unsigned SeqEdge0, SeqEdge1;
-    int TotalLag, Lag, i;
+    int Lag, i;
     // get the object and the lag
     pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
     Lag  = SeqEdge & 255;
@@ -540,23 +552,23 @@ Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, uns
     // continue unfolding
     assert( Abc_NodeIsAigAnd(pObj) );
     // get new sequential edges
-    assert( Lag + Abc_ObjFaninL0(pObj) < 255 );
-    assert( Lag + Abc_ObjFaninL1(pObj) < 255 );
-    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Abc_ObjFaninL0(pObj);
-    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Abc_ObjFaninL1(pObj);
+    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
+    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
+    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
+    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
     // call for the children    
     pObjNew = fTop? pObj->pCopy : Abc_NtkCreateNode( pNtkNew );
     // solve subproblems
-    pFaninNew0 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, vLeaves );
-    pFaninNew1 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, vLeaves );
+    pFaninNew0 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, LagCut, vLeaves );
+    pFaninNew1 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, LagCut, vLeaves );
     // add the fanins to the node
     Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) );
     Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) );
     Seq_NodeDupLats( pObjNew, pObj, 0 );
     Seq_NodeDupLats( pObjNew, pObj, 1 );
     // set the lag of the new node equal to the internal lag plus mapping/retiming lag
-    TotalLag = Lag + Seq_NodeGetLag(pObj);
-    Seq_NodeSetLag( pObjNew, (char)TotalLag );
+    Seq_NodeSetLag( pObjNew, (char)(Lag + LagCut) );
+//    Seq_NodeSetLag( pObjNew, (char)(Lag) );
     return pObjNew;
 }
 
diff --git a/src/base/seq/seqFpgaIter.c b/src/base/seq/seqFpgaIter.c
index c2777606..fc521158 100644
--- a/src/base/seq/seqFpgaIter.c
+++ b/src/base/seq/seqFpgaIter.c
@@ -63,7 +63,7 @@ void Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose )
     pParams->fTruth    = 0;     // compute truth tables
     pParams->fFilter   = 1;     // filter dominated cuts
     pParams->fSeq      = 1;     // compute sequential cuts
-    pParams->fVerbose  = 0;     // the verbosiness flag
+    pParams->fVerbose  = fVerbose;     // the verbosiness flag
 
     // compute the cuts
 clk = clock();
@@ -84,7 +84,8 @@ p->timeDelay = clock() - clk;
     Abc_NtkForEachPo( pNtk, pObj, i )
         Seq_FpgaMappingCollectNode_rec( Abc_ObjFanin0(pObj), p->vMapAnds, p->vMapCuts );
 
-printf( "The number of LUTs = %d.\n", Vec_PtrSize(p->vMapAnds) );
+    if ( fVerbose )
+    printf( "The number of LUTs = %d.\n", Vec_PtrSize(p->vMapAnds) );
 
     // remove the cuts
     Cut_ManStop( p->pCutMan );
@@ -151,7 +152,7 @@ Cut_Cut_t * Seq_FpgaMappingSelectCut( Abc_Obj_t * pAnd )
     int ArrivalCut, ArrivalMin, i;
     // get the arrival time of the best non-trivial cut
     ArrivalMin = Seq_NodeGetLValue( pAnd );
-    // iterate through the cuts and with the one with the minimum cost
+    // iterate through the cuts and select the one with the minimum cost
     pList = Abc_NodeReadCuts( Seq_NodeCutMan(pAnd), pAnd );
     CostMin = ABC_INFINITY;
     pCutBest = NULL;
@@ -231,7 +232,7 @@ int Seq_FpgaNodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
     assert( Abc_ObjFaninNum(pObj) > 0 );
     if ( Abc_ObjIsPo(pObj) )
     {
-        lValueNew = Seq_NodeGetLValue(Abc_ObjFanin0(pObj)) - Fi * Abc_ObjFaninL0(pObj);
+        lValueNew = Seq_NodeGetLValue(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj);
         return (lValueNew > Fi)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO;
     }
     // get the arrival time of the best non-trivial cut
diff --git a/src/base/seq/seqInt.h b/src/base/seq/seqInt.h
index 6cb1fecc..a39a6d69 100644
--- a/src/base/seq/seqInt.h
+++ b/src/base/seq/seqInt.h
@@ -48,6 +48,7 @@ struct Abc_Seq_t_
     // sequential information
     Abc_Ntk_t *         pNtk;           // the network
     int                 nSize;          // the number of entries in all internal arrays
+    Vec_Int_t *         vNums;          // the number of latches on each edge in the AIG
     Vec_Ptr_t *         vInits;         // the initial states for each edge in the AIG
     Extra_MmFixed_t *   pMmInits;       // memory manager for latch structures used to remember init states
     int                 fVerbose;       // the verbose flag
@@ -104,17 +105,28 @@ static inline Seq_RetEdge_t  Seq_Int2RetEdge( int Num )            { return *((S
 static inline int            Seq_RetStep2Int( Seq_RetStep_t Val )  { return *((int *)&Val);           }
 static inline Seq_RetStep_t  Seq_Int2RetStep( int Num )            { return *((Seq_RetStep_t *)&Num); }
 
-// reading l-values and lags
-static inline Vec_Int_t *    Seq_NodeLValues( Abc_Obj_t * pNode )               { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLValues;           }
-static inline int            Seq_NodeGetLValue( Abc_Obj_t * pNode )             { return Vec_IntEntry( Seq_NodeLValues(pNode), (pNode)->Id );        }
-static inline void           Seq_NodeSetLValue( Abc_Obj_t * pNode, int Value )  { Vec_IntWriteEntry( Seq_NodeLValues(pNode), (pNode)->Id, Value );   }
-static inline int            Seq_NodeComputeLag( int LValue, int Fi )           { return (LValue + 1024*Fi)/Fi - 1024 - (int)(LValue % Fi == 0);     }
+// manipulating the number of latches on each edge
+static inline Vec_Int_t *    Seq_ObjLNums( Abc_Obj_t * pObj )                        { return ((Abc_Seq_t*)pObj->pNtk->pManFunc)->vNums;                    }
+static inline int            Seq_ObjFaninL( Abc_Obj_t * pObj, int i )                { return Vec_IntEntry(Seq_ObjLNums(pObj), 2*pObj->Id + i);             }
+static inline int            Seq_ObjFaninL0( Abc_Obj_t * pObj )                      { return Vec_IntEntry(Seq_ObjLNums(pObj), 2*pObj->Id + 0);             }
+static inline int            Seq_ObjFaninL1( Abc_Obj_t * pObj )                      { return Vec_IntEntry(Seq_ObjLNums(pObj), 2*pObj->Id + 1);             }
+static inline void           Seq_ObjSetFaninL( Abc_Obj_t * pObj, int i, int nLats )  { Vec_IntWriteEntry(Seq_ObjLNums(pObj), 2*pObj->Id + i, nLats);        }
+static inline void           Seq_ObjSetFaninL0( Abc_Obj_t * pObj, int nLats )        { Vec_IntWriteEntry(Seq_ObjLNums(pObj), 2*pObj->Id + 0, nLats);        }
+static inline void           Seq_ObjSetFaninL1( Abc_Obj_t * pObj, int nLats )        { Vec_IntWriteEntry(Seq_ObjLNums(pObj), 2*pObj->Id + 1, nLats);        }
+static inline void           Seq_ObjAddFaninL( Abc_Obj_t * pObj, int i, int nLats )  { Vec_IntAddToEntry(Seq_ObjLNums(pObj), 2*pObj->Id + i, nLats);        }
+static inline void           Seq_ObjAddFaninL0( Abc_Obj_t * pObj, int nLats )        { Vec_IntAddToEntry(Seq_ObjLNums(pObj), 2*pObj->Id + 0, nLats);        }
+static inline void           Seq_ObjAddFaninL1( Abc_Obj_t * pObj, int nLats )        { Vec_IntAddToEntry(Seq_ObjLNums(pObj), 2*pObj->Id + 1, nLats);        }
+static inline int            Seq_ObjFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) { return Seq_ObjFaninL( pFanout, Abc_ObjFanoutEdgeNum(pObj,pFanout) ); }
+static inline void           Seq_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats ) {  Seq_ObjSetFaninL( pFanout, Abc_ObjFanoutEdgeNum(pObj,pFanout), nLats );  }
+static inline void           Seq_ObjAddFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats ) {  Seq_ObjAddFaninL( pFanout, Abc_ObjFanoutEdgeNum(pObj,pFanout), nLats );  }
+static inline int            Seq_ObjFaninLMin( Abc_Obj_t * pObj )                    {  assert( Abc_ObjIsNode(pObj) ); return ABC_MIN( Seq_ObjFaninL0(pObj), Seq_ObjFaninL1(pObj) ); }
+static inline int            Seq_ObjFaninLMax( Abc_Obj_t * pObj )                    {  assert( Abc_ObjIsNode(pObj) ); return ABC_MAX( Seq_ObjFaninL0(pObj), Seq_ObjFaninL1(pObj) ); }
 
-// reading best cuts at each node
-static inline Cut_Man_t *    Seq_NodeCutMan( Abc_Obj_t * pNode )                { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->pCutMan;                 }
-//static inline Vec_Ptr_t *    Seq_NodeCutBests( Abc_Obj_t * pNode )              { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vBestCuts;               }
-//static inline Cut_Cut_t *    Seq_NodeGetCutBest( Abc_Obj_t * pNode )            { return Vec_PtrEntry( Seq_NodeCutBests(pNode), (pNode)->Id );            }
-//static inline void           Seq_NodeSetCutBest( Abc_Obj_t * pNode, Cut_Cut_t * pCut ) { Vec_PtrWriteEntry( Seq_NodeCutBests(pNode), (pNode)->Id, pCut ); }
+// reading l-values and lags
+static inline Vec_Int_t *    Seq_NodeLValues( Abc_Obj_t * pNode )                    { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLValues;           }
+static inline int            Seq_NodeGetLValue( Abc_Obj_t * pNode )                  { return Vec_IntEntry( Seq_NodeLValues(pNode), (pNode)->Id );        }
+static inline void           Seq_NodeSetLValue( Abc_Obj_t * pNode, int Value )       { Vec_IntWriteEntry( Seq_NodeLValues(pNode), (pNode)->Id, Value );   }
+static inline int            Seq_NodeComputeLag( int LValue, int Fi )                { return (LValue + 1024*Fi)/Fi - 1024 - (int)(LValue % Fi == 0);     }
 
 // reading the contents of the lat
 static inline Abc_InitType_t Seq_LatInit( Seq_Lat_t * pLat )  { return ((unsigned)pLat->pPrev) & 3;                                 }
@@ -127,6 +139,7 @@ static inline void           Seq_LatSetNext( Seq_Lat_t * pLat, Seq_Lat_t * pNext
 static inline void           Seq_LatSetPrev( Seq_Lat_t * pLat, Seq_Lat_t * pPrev )    { Abc_InitType_t Init = Seq_LatInit(pLat);  pLat->pPrev = pPrev;  Seq_LatSetInit(pLat, Init); }
 
 // accessing retiming lags
+static inline Cut_Man_t *    Seq_NodeCutMan( Abc_Obj_t * pNode )                      { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->pCutMan;                 }
 static inline Vec_Str_t *    Seq_NodeLags( Abc_Obj_t * pNode )                        { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLags;            }
 static inline char           Seq_NodeGetLag( Abc_Obj_t * pNode )                      { return Vec_StrEntry( Seq_NodeLags(pNode), (pNode)->Id );         }
 static inline void           Seq_NodeSetLag( Abc_Obj_t * pNode, char Value )          { Vec_StrWriteEntry( Seq_NodeLags(pNode), (pNode)->Id, (Value) );  }
diff --git a/src/base/seq/seqLatch.c b/src/base/seq/seqLatch.c
index f5106b24..8f861004 100644
--- a/src/base/seq/seqLatch.c
+++ b/src/base/seq/seqLatch.c
@@ -60,7 +60,7 @@ void Seq_NodeInsertFirst( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )
         Seq_NodeSetRing( pObj, Edge, pLat );  // rotate the ring to make pLat the first
     }
     Seq_LatSetInit( pLat, Init );
-    Abc_ObjAddFaninL( pObj, Edge, 1 );
+    Seq_ObjAddFaninL( pObj, Edge, 1 );
 }
 
 /**Function*************************************************************
@@ -94,7 +94,7 @@ void Seq_NodeInsertLast( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )
         Seq_LatSetNext( pLat, pRing );
     }
     Seq_LatSetInit( pLat, Init );
-    Abc_ObjAddFaninL( pObj, Edge, 1 );
+    Seq_ObjAddFaninL( pObj, Edge, 1 );
 }
 
 /**Function*************************************************************
@@ -126,7 +126,7 @@ Abc_InitType_t Seq_NodeDeleteFirst( Abc_Obj_t * pObj, int Edge )
     }
     Init = Seq_LatInit( pLat );
     Seq_NodeRecycleLat( pObj, pLat );
-    Abc_ObjAddFaninL( pObj, Edge, -1 );
+    Seq_ObjAddFaninL( pObj, Edge, -1 );
     return Init;
 }
 
@@ -158,7 +158,7 @@ Abc_InitType_t Seq_NodeDeleteLast( Abc_Obj_t * pObj, int Edge )
     }
     Init = Seq_LatInit( pLat );
     Seq_NodeRecycleLat( pObj, pLat ); 
-    Abc_ObjAddFaninL( pObj, Edge, -1 );
+    Seq_ObjAddFaninL( pObj, Edge, -1 );
     return Init;
 }
 
diff --git a/src/base/seq/seqMan.c b/src/base/seq/seqMan.c
index 7074f28d..109199fe 100644
--- a/src/base/seq/seqMan.c
+++ b/src/base/seq/seqMan.c
@@ -51,6 +51,7 @@ Abc_Seq_t * Seq_Create( Abc_Ntk_t * pNtk )
     p->nSize = 1000;
     p->pMmInits = Extra_MmFixedStart( sizeof(Seq_Lat_t) );
     // create internal data structures
+    p->vNums    = Vec_IntStart( 2 * p->nSize ); 
     p->vInits   = Vec_PtrStart( 2 * p->nSize ); 
     p->vLValues = Vec_IntStart( p->nSize ); 
     p->vLags    = Vec_StrStart( p->nSize ); 
@@ -73,6 +74,7 @@ void Seq_Resize( Abc_Seq_t * p, int nMaxId )
     if ( p->nSize > nMaxId )
         return;
     p->nSize = nMaxId + 1;
+    Vec_IntFill( p->vNums,     2 * p->nSize, 0 ); 
     Vec_PtrFill( p->vInits,    2 * p->nSize, NULL ); 
     Vec_IntFill( p->vLValues,  p->nSize, 0 ); 
     Vec_StrFill( p->vLags,     p->nSize, 0 ); 
@@ -97,6 +99,7 @@ void Seq_Delete( Abc_Seq_t * p )
     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->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/seqRetCore.c b/src/base/seq/seqRetCore.c
index 03b86451..373e77bd 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -220,8 +220,8 @@ void Abc_ObjRetimeForward( Abc_Obj_t * pObj )
     Abc_Obj_t * pFanout;
     int Init0, Init1, Init, i;
     assert( Abc_ObjFaninNum(pObj) == 2 );
-    assert( Abc_ObjFaninL0(pObj) >= 1 );
-    assert( Abc_ObjFaninL1(pObj) >= 1 );
+    assert( Seq_ObjFaninL0(pObj) >= 1 );
+    assert( Seq_ObjFaninL1(pObj) >= 1 );
     // remove the init values from the fanins
     Init0 = Seq_NodeDeleteFirst( pObj, 0 ); 
     Init1 = Seq_NodeDeleteFirst( pObj, 1 );
@@ -249,13 +249,31 @@ void Abc_ObjRetimeForward( Abc_Obj_t * pObj )
         Init = ABC_INIT_ONE;
     else
         Init = ABC_INIT_DC;
+
+    // make sure the label is clean
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        assert( pFanout->fMarkC == 0 );
     // add the init values to the fanouts
     Abc_ObjForEachFanout( pObj, pFanout, i )
-        Seq_NodeInsertLast( pFanout, Abc_ObjFanoutEdgeNum(pObj, pFanout), Init );
+    {
+        if ( pFanout->fMarkC )
+            continue;
+        pFanout->fMarkC = 1;
+        if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) )
+            Seq_NodeInsertLast( pFanout, Abc_ObjFanoutEdgeNum(pObj, pFanout), Init );
+        else
+        {
+            assert( Abc_ObjFanin0(pFanout) == pObj );
+            Seq_NodeInsertLast( pFanout, 0, Init );
+            Seq_NodeInsertLast( pFanout, 1, Init );
+        }
+    }
+    // clean the label
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        pFanout->fMarkC = 0;
 }
 
 
-
 /**Function*************************************************************
 
   Synopsis    [Implements the given retiming on the sequential AIG.]
@@ -390,22 +408,49 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t
     fMet0 = fMet1 = fMetN = 0;
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
-        Init = Seq_NodeGetInitLast( pFanout, Abc_ObjFanoutEdgeNum(pObj, pFanout) );
-        if ( Init == ABC_INIT_ZERO )
-            fMet0 = 1;
-        else if ( Init == ABC_INIT_ONE )
-            fMet1 = 1;
-        else if ( Init == ABC_INIT_NONE )
-            fMetN = 1;
+        if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
+        {
+            Init = Seq_NodeGetInitLast( pFanout, 0 );
+            if ( Init == ABC_INIT_ZERO )
+                fMet0 = 1;
+            else if ( Init == ABC_INIT_ONE )
+                fMet1 = 1;
+            else if ( Init == ABC_INIT_NONE )
+                fMetN = 1;
+        }
+        if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
+        {
+            Init = Seq_NodeGetInitLast( pFanout, 1 );
+            if ( Init == ABC_INIT_ZERO )
+                fMet0 = 1;
+            else if ( Init == ABC_INIT_ONE )
+                fMet1 = 1;
+            else if ( Init == ABC_INIT_NONE )
+                fMetN = 1;
+        }
     }
 
-    // consider the case when all fanout latchs have don't-care values
+    // consider the case when all fanout latches have don't-care values
     // the new values on the fanin edges will be don't-cares
     if ( !fMet0 && !fMet1 && !fMetN )
     {
+        // make sure the label is clean
+        Abc_ObjForEachFanout( pObj, pFanout, i )
+            assert( pFanout->fMarkC == 0 );
         // update the fanout edges
         Abc_ObjForEachFanout( pObj, pFanout, i )
-            Seq_NodeDeleteLast( pFanout, Abc_ObjFanoutEdgeNum(pObj, pFanout) );
+        {
+            if ( pFanout->fMarkC )
+                continue;
+            pFanout->fMarkC = 1;
+            if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
+                Seq_NodeDeleteLast( pFanout, 0 );
+            if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
+                Seq_NodeDeleteLast( pFanout, 1 );
+        }
+        // clean the label
+        Abc_ObjForEachFanout( pObj, pFanout, i )
+            pFanout->fMarkC = 0;
         // update the fanin edges
         Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable );
         Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable );
@@ -432,22 +477,49 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t
         Vec_IntPush( vValues, 1 );
     }
 
+    // make sure the label is clean
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        assert( pFanout->fMarkC == 0 );
     // perform the changes
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
-        Edge = Abc_ObjFanoutEdgeNum( pObj, pFanout );
-        Value = Seq_NodeDeleteLast( pFanout, Edge );
-        if ( Value != ABC_INIT_NONE )
+        if ( pFanout->fMarkC )
             continue;
-        // value is unknown, remove it from the table
-        RetEdge.iNode  = pFanout->Id;
-        RetEdge.iEdge  = Edge;
-        RetEdge.iLatch = Abc_ObjFaninL( pFanout, Edge ); // after edge is removed
-        if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
-            assert( 0 );
-        // create the fanout of the AND gate
-        Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+        pFanout->fMarkC = 1;
+        if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
+        {
+            Edge = 0;
+            Value = Seq_NodeDeleteLast( pFanout, Edge );
+            if ( Value != ABC_INIT_NONE )
+                continue;
+            // value is unknown, remove it from the table
+            RetEdge.iNode  = pFanout->Id;
+            RetEdge.iEdge  = Edge;
+            RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed
+            if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
+                assert( 0 );
+            // create the fanout of the AND gate
+            Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+        }
+        if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
+        {
+            Edge = 1;
+            Value = Seq_NodeDeleteLast( pFanout, Edge );
+            if ( Value != ABC_INIT_NONE )
+                continue;
+            // value is unknown, remove it from the table
+            RetEdge.iNode  = pFanout->Id;
+            RetEdge.iEdge  = Edge;
+            RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed
+            if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
+                assert( 0 );
+            // create the fanout of the AND gate
+            Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+        }
     }
+    // clean the label
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        pFanout->fMarkC = 0;
 
     // update the fanin edges
     Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable );
@@ -500,7 +572,7 @@ void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * t
     int nLatches, i;
 
     // get the number of latches on the edge
-    nLatches = Abc_ObjFaninL( pObj, Edge );
+    nLatches = Seq_ObjFaninL( pObj, Edge );
     for ( i = nLatches - 1; i >= 0; i-- )
     {
         // get the value of this latch
@@ -579,12 +651,12 @@ Vec_Ptr_t * Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward )
     vMoves = Vec_PtrAlloc( 100 );
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
-//        printf( "(%d,%d) ", Abc_ObjFaninL0(pNode), Abc_ObjFaninL0(pNode) );
+//        printf( "(%d,%d) ", Seq_ObjFaninL0(pNode), Seq_ObjFaninL0(pNode) );
         // unmark the node as processed
         pNode->fMarkA = 0;
         // get the number of latches to retime
         if ( fForward )
-            nLatches = Abc_ObjFaninLMin(pNode);
+            nLatches = Seq_ObjFaninLMin(pNode);
         else
             nLatches = Seq_ObjFanoutLMin(pNode);
         if ( nLatches == 0 )
@@ -626,7 +698,7 @@ Vec_Ptr_t * Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward )
     {
         assert( pNode->fMarkA == 0 );
         if ( fForward ) 
-            assert( Abc_ObjFaninLMin(pNode) == 0 );
+            assert( Seq_ObjFaninLMin(pNode) == 0 );
         else
             assert( Seq_ObjFanoutLMin(pNode) == 0 );
     }
@@ -652,6 +724,48 @@ Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, b
     int i, k, iNode, nLatches, Number;
     int fChange;
     assert( Abc_NtkIsSeq( pNtk ) );
+
+/*
+    // try implementing all the moves at once
+    Vec_IntForEachEntry( vSteps, Number, i )
+    {
+        // get the retiming step
+        RetStep = Seq_Int2RetStep( Number );
+        // get the node to be retimed
+        pNode = Abc_NtkObj( pNtk, RetStep.iNode );
+        assert( RetStep.nLatches > 0 );
+        nLatches = RetStep.nLatches;
+
+        if ( fForward )
+            Abc_ObjRetimeForwardTry( pNode, nLatches );
+        else
+            Abc_ObjRetimeBackwardTry( pNode, nLatches );
+    }
+    // now look if any node has wrong number of latches
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        if ( Seq_ObjFaninL0(pNode) < 0 )
+            printf( "Wrong 0node %d.\n", pNode->Id );
+        if ( Seq_ObjFaninL1(pNode) < 0 )
+            printf( "Wrong 1node %d.\n", pNode->Id );
+    }
+    // try implementing all the moves at once
+    Vec_IntForEachEntry( vSteps, Number, i )
+    {
+        // get the retiming step
+        RetStep = Seq_Int2RetStep( Number );
+        // get the node to be retimed
+        pNode = Abc_NtkObj( pNtk, RetStep.iNode );
+        assert( RetStep.nLatches > 0 );
+        nLatches = RetStep.nLatches;
+
+        if ( !fForward )
+            Abc_ObjRetimeForwardTry( pNode, nLatches );
+        else
+            Abc_ObjRetimeBackwardTry( pNode, nLatches );
+    }
+*/
+
     // process the nodes
     vMoves = Vec_PtrAlloc( 100 );
     while ( Vec_IntSize(vSteps) > 0 )
@@ -667,7 +781,7 @@ Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, b
             assert( RetStep.nLatches > 0 );
             // get the number of latches that can be retimed
             if ( fForward )
-                nLatches = Abc_ObjFaninLMin(pNode);
+                nLatches = Seq_ObjFaninLMin(pNode);
             else
                 nLatches = Seq_ObjFanoutLMin(pNode);
             if ( nLatches == 0 )
@@ -698,14 +812,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;
         }
     }
@@ -777,14 +891,32 @@ void Abc_ObjRetimeForwardTry( Abc_Obj_t * pObj, int nLatches )
     // make sure it is an AND gate
     assert( Abc_ObjFaninNum(pObj) == 2 );
     // make sure it has enough latches
-//    assert( Abc_ObjFaninL0(pObj) >= nLatches );
-//    assert( Abc_ObjFaninL1(pObj) >= nLatches );
+//    assert( Seq_ObjFaninL0(pObj) >= nLatches );
+//    assert( Seq_ObjFaninL1(pObj) >= nLatches );
     // subtract these latches on the fanin side
-    Abc_ObjAddFaninL0( pObj, -nLatches );
-    Abc_ObjAddFaninL1( pObj, -nLatches );
-    // add these latches on the fanout size
+    Seq_ObjAddFaninL0( pObj, -nLatches );
+    Seq_ObjAddFaninL1( pObj, -nLatches );
+    // make sure the label is clean
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        assert( pFanout->fMarkC == 0 );
+    // add these latches on the fanout side
     Abc_ObjForEachFanout( pObj, pFanout, i )
-        Abc_ObjAddFanoutL( pObj, pFanout, nLatches );
+    {
+        if ( pFanout->fMarkC )
+            continue;
+        pFanout->fMarkC = 1;
+        if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) )
+            Seq_ObjAddFanoutL( pObj, pFanout, nLatches );
+        else
+        {
+            assert( Abc_ObjFanin0(pFanout) == pObj );
+            Seq_ObjAddFaninL0( pFanout, nLatches );
+            Seq_ObjAddFaninL1( pFanout, nLatches );
+        }
+    }
+    // clean the label
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        pFanout->fMarkC = 0;
 }
 
 /**Function*************************************************************
@@ -804,15 +936,31 @@ void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches )
     int i;
     // make sure it is an AND gate
     assert( Abc_ObjFaninNum(pObj) == 2 );
+    // make sure the label is clean
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        assert( pFanout->fMarkC == 0 );
     // subtract these latches on the fanout side
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
+        if ( pFanout->fMarkC )
+            continue;
+        pFanout->fMarkC = 1;
 //        assert( Abc_ObjFanoutL(pObj, pFanout) >= nLatches );
-        Abc_ObjAddFanoutL( pObj, pFanout, -nLatches );
+        if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) )
+            Seq_ObjAddFanoutL( pObj, pFanout, -nLatches );
+        else
+        {
+            assert( Abc_ObjFanin0(pFanout) == pObj );
+            Seq_ObjAddFaninL0( pFanout, -nLatches );
+            Seq_ObjAddFaninL1( pFanout, -nLatches );
+        }
     }
-    // add these latches on the fanin size
-    Abc_ObjAddFaninL0( pObj, nLatches );
-    Abc_ObjAddFaninL1( pObj, nLatches );
+    // clean the label
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        pFanout->fMarkC = 0;
+    // add these latches on the fanin side
+    Seq_ObjAddFaninL0( pObj, nLatches );
+    Seq_ObjAddFaninL1( pObj, nLatches );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqRetIter.c b/src/base/seq/seqRetIter.c
index af239f81..6f7a320a 100644
--- a/src/base/seq/seqRetIter.c
+++ b/src/base/seq/seqRetIter.c
@@ -78,6 +78,23 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
         NodeLag = Seq_NodeComputeLag( Seq_NodeGetLValue(pNode), FiBest );
         Seq_NodeSetLag( pNode, NodeLag );
     }
+/*
+    {
+        Abc_Obj_t * pFanin, * pFanout;
+        pNode = Abc_NtkObj( pNtk, 823 );
+        printf( "Node  %d.  Lag = %d. LValue = %d. Latches = (%d,%d) (%d,%d).\n", pNode->Id, Seq_NodeGetLag(pNode), Seq_NodeGetLValue(pNode), 
+            Seq_ObjFaninL0(pNode), Seq_ObjFaninL1(pNode), Seq_ObjFanoutL(pNode, Abc_NtkObj(pNtk, 826)), Seq_ObjFanoutL(pNode, Abc_NtkObj(pNtk, 1210)) );
+        pFanin = Abc_ObjFanin0( pNode );
+        printf( "Fanin %d.  Lag = %d. LValue = %d. Latches = (%d,%d)\n", pFanin->Id, Seq_NodeGetLag(pFanin), Seq_NodeGetLValue(pFanin),
+            Seq_ObjFaninL0(pFanin), Seq_ObjFaninL1(pFanin) );
+        pFanin = Abc_ObjFanin1( pNode );
+        printf( "Fanin %d.  Lag = %d. LValue = %d.\n", pFanin->Id, Seq_NodeGetLag(pFanin), Seq_NodeGetLValue(pFanin) );
+        Abc_ObjForEachFanout( pNode, pFanout, i )
+            printf( "Fanout %d.  Lag = %d. LValue = %d.\n", pFanout->Id, Seq_NodeGetLag(pFanout), Seq_NodeGetLValue(pFanout) );
+        Abc_ObjForEachFanout( Abc_ObjFanin0(pNode), pFanout, i )
+            printf( "Fanout %d.  Lag = %d. LValue = %d.\n", pFanout->Id, Seq_NodeGetLag(pFanout), Seq_NodeGetLValue(pFanout) );
+    }
+*/
 
     // print the result
     if ( fVerbose )
@@ -135,6 +152,7 @@ int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
     Abc_Obj_t * pObj;
+    int nMaxSteps = 10;
     int i, c, RetValue, fChange, Counter;
     char * pReason = "";
 
@@ -149,7 +167,7 @@ int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose )
 
     // update all values iteratively
     Counter = 0;
-    for ( c = 0; c < 20; c++ )
+    for ( c = 0; c < nMaxSteps; c++ )
     {
         fChange = 0;
         Abc_AigForEachAnd( pNtk, pObj, i )
@@ -185,7 +203,7 @@ int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose )
         if ( fChange == 0 )
             break;
     }
-    if ( c == 20 )
+    if ( c == nMaxSteps )
     {
         RetValue = SEQ_UPDATE_FAIL;
         pReason = "(timeout)";
@@ -222,11 +240,11 @@ int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
     int lValueNew, lValueOld, lValue0, lValue1;
     assert( !Abc_ObjIsPi(pObj) );
     assert( Abc_ObjFaninNum(pObj) > 0 );
-    lValue0 = Seq_NodeGetLValue(Abc_ObjFanin0(pObj)) - Fi * Abc_ObjFaninL0(pObj);
+    lValue0 = Seq_NodeGetLValue(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj);
     if ( Abc_ObjIsPo(pObj) )
         return (lValue0 > Fi)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO;
     if ( Abc_ObjFaninNum(pObj) == 2 )
-        lValue1 = Seq_NodeGetLValue(Abc_ObjFanin1(pObj)) - Fi * Abc_ObjFaninL1(pObj);
+        lValue1 = Seq_NodeGetLValue(Abc_ObjFanin1(pObj)) - Fi * Seq_ObjFaninL1(pObj);
     else
         lValue1 = -ABC_INFINITY;
     lValueNew = 1 + ABC_MAX( lValue0, lValue1 );
diff --git a/src/base/seq/seqShare.c b/src/base/seq/seqShare.c
index aafc7dc5..818dca23 100644
--- a/src/base/seq/seqShare.c
+++ b/src/base/seq/seqShare.c
@@ -82,7 +82,7 @@ void Seq_NodeShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
     // find the number of fanouts having latches of each type
     Abc_ObjForEachFanout( pNode, pFanout, i )  
     {
-        if ( Abc_ObjFanoutL(pNode, pFanout) == 0 )
+        if ( Seq_ObjFanoutL(pNode, pFanout) == 0 )
             continue;
         Type = Seq_NodeGetInitLast( pFanout, Abc_ObjFanoutEdgeNum(pNode, pFanout) );
         nLatches[Type]++;
@@ -119,6 +119,7 @@ void Seq_NodeShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 ***********************************************************************/
 void Seq_NodeShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNodes )
 {
+    Vec_Int_t * vNums  = Seq_ObjLNums( pNode );
     Vec_Ptr_t * vInits = Seq_NodeLats( pNode );
     Abc_Obj_t * pFanout, * pBuffer;
     Abc_InitType_t Type, InitNew;
@@ -128,7 +129,7 @@ void Seq_NodeShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNode
     Vec_PtrClear( vNodes );
     Abc_ObjForEachFanout( pNode, pFanout, i )
     {
-        if ( Abc_ObjFanoutL(pNode, pFanout) == 0 )
+        if ( Seq_ObjFanoutL(pNode, pFanout) == 0 )
             continue;
         Type = Seq_NodeGetInitLast( pFanout, Abc_ObjFanoutEdgeNum(pNode, pFanout) );
         if ( Type == Init )
@@ -147,6 +148,11 @@ void Seq_NodeShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNode
     Vec_PtrGrow( vInits, 2 * pBuffer->Id + 2 );
     for ( i = Vec_PtrSize(vInits); i < 2 * (int)pBuffer->Id + 2; i++ )
         Vec_PtrPush( vInits, NULL );
+    // grow storage for numbers of latches
+    Vec_IntGrow( vNums, 2 * pBuffer->Id + 2 );
+    for ( i = Vec_IntSize(vNums); i < 2 * (int)pBuffer->Id + 2; i++ )
+        Vec_IntPush( vNums, 0 );
+    // insert the new latch
     Seq_NodeInsertFirst( pBuffer, 0, InitNew );
 
     // redirect the fanouts
diff --git a/src/base/seq/seqUtil.c b/src/base/seq/seqUtil.c
index 3a80bd3c..b126b043 100644
--- a/src/base/seq/seqUtil.c
+++ b/src/base/seq/seqUtil.c
@@ -48,7 +48,7 @@ int Seq_ObjFanoutLMax( Abc_Obj_t * pObj )
     nLatchRes = 0;
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
-        nLatchCur = Abc_ObjFanoutL(pObj, pFanout);
+        nLatchCur = Seq_ObjFanoutL(pObj, pFanout);
         if ( nLatchRes < nLatchCur )
             nLatchRes = nLatchCur;
     }
@@ -76,7 +76,7 @@ int Seq_ObjFanoutLMin( Abc_Obj_t * pObj )
     nLatchRes = ABC_INFINITY;
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
-        nLatchCur = Abc_ObjFanoutL(pObj, pFanout);
+        nLatchCur = Seq_ObjFanoutL(pObj, pFanout);
         if ( nLatchRes > nLatchCur )
             nLatchRes = nLatchCur;
     }
@@ -100,7 +100,7 @@ int Seq_ObjFanoutLSum( Abc_Obj_t * pObj )
     Abc_Obj_t * pFanout;
     int i, nSum = 0;
     Abc_ObjForEachFanout( pObj, pFanout, i )
-        nSum += Abc_ObjFanoutL(pObj, pFanout);
+        nSum += Seq_ObjFanoutL(pObj, pFanout);
     return nSum;
 }
 
@@ -120,7 +120,7 @@ int Seq_ObjFaninLSum( Abc_Obj_t * pObj )
     Abc_Obj_t * pFanin;
     int i, nSum = 0;
     Abc_ObjForEachFanin( pObj, pFanin, i )
-        nSum += Abc_ObjFaninL(pObj, i);
+        nSum += Seq_ObjFaninL(pObj, i);
     return nSum;
 }
 
@@ -140,7 +140,7 @@ char * Seq_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge )
     static char Buffer[1000];
     Abc_InitType_t Init;
     int nLatches, i;
-    nLatches = Abc_ObjFaninL( pObj, Edge );
+    nLatches = Seq_ObjFaninL( pObj, Edge );
     for ( i = 0; i < nLatches; i++ )
     {
         Init = Seq_LatInit( Seq_NodeGetLat(pObj, Edge, i) );
@@ -249,13 +249,13 @@ int Seq_NtkLatchNumMax( Abc_Ntk_t * pNtk )
     Max = 0;
     Abc_AigForEachAnd( pNtk, pObj, i )
     {
-        Cur = Abc_ObjFaninLMax( pObj );
+        Cur = Seq_ObjFaninLMax( pObj );
         if ( Max < Cur )
             Max = Cur;
     }
     Abc_NtkForEachPo( pNtk, pObj, i )
     {
-        Cur = Abc_ObjFaninL0( pObj );
+        Cur = Seq_ObjFaninL0( pObj );
         if ( Max < Cur )
             Max = Cur;
     }
@@ -301,7 +301,7 @@ void Seq_ObjLatchGetInitNums( Abc_Obj_t * pObj, int Edge, int * pInits )
 {
     Abc_InitType_t Init;
     int nLatches, i;
-    nLatches = Abc_ObjFaninL( pObj, Edge );
+    nLatches = Seq_ObjFaninL( pObj, Edge );
     for ( i = 0; i < nLatches; i++ )
     {
         Init = Seq_NodeGetInitOne( pObj, Edge, i );
@@ -338,6 +338,31 @@ void Seq_NtkLatchGetInitNums( Abc_Ntk_t * pNtk, int * pInits )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Report nodes with equal fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkLatchGetEqualFaninNum( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, Counter;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    Counter = 0;
+    Abc_AigForEachAnd( pNtk, pObj, i )
+        if ( Abc_ObjFaninId0(pObj) == Abc_ObjFaninId1(pObj) )
+            Counter++;
+    if ( Counter )
+        printf( "The number of nodes with equal fanins = %d.\n", Counter );
+    return Counter;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/fpga/fpgaCore.c b/src/map/fpga/fpgaCore.c
index 2e5529f2..2de8b73a 100644
--- a/src/map/fpga/fpgaCore.c
+++ b/src/map/fpga/fpgaCore.c
@@ -46,7 +46,7 @@ static int  Fpga_MappingPostProcess( Fpga_Man_t * p );
 int Fpga_Mapping( Fpga_Man_t * p )
 {
     int clk, clkTotal = clock();
-
+ 
     // collect the nodes reachable from POs in the DFS order (including the choices)
     p->vAnds = Fpga_MappingDfs( p, 1 );
     Fpga_ManReportChoices( p ); // recomputes levels
diff --git a/src/misc/vec/vecFan.h b/src/misc/vec/vecFan.h
index a42f6aa1..1493014a 100644
--- a/src/misc/vec/vecFan.h
+++ b/src/misc/vec/vecFan.h
@@ -39,8 +39,7 @@
 typedef struct Abc_Fan_t_       Abc_Fan_t;
 struct Abc_Fan_t_ // 1 word
 {
-    unsigned         iFan    : 24;  // the ID of the object
-    unsigned         nLats   :  7;  // the number of latches (up to 127)
+    unsigned         iFan    : 31;  // the ID of the object
     unsigned         fCompl  :  1;  // the complemented attribute
 };
 
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index c46db454..3c767f20 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -307,6 +307,23 @@ static inline void Vec_IntWriteEntry( Vec_Int_t * p, int i, int Entry )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Vec_IntAddToEntry( Vec_Int_t * p, int i, int Addition )
+{
+    assert( i >= 0 && i < p->nSize );
+    p->pArray[i] += Addition;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline int Vec_IntEntryLast( Vec_Int_t * p )
 {
     return p->pArray[p->nSize-1];