Version abc50912

27 files changed, 1463 insertions, 607 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 02b284e6..49dd9943 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -43,7 +43,7 @@
 
 // network types
 typedef enum { 
-    ABC_TYPE_NONE,      // 0:  unknown
+    ABC_TYPE_NONE = 0,  // 0:  unknown
     ABC_TYPE_NETLIST,   // 1:  network with PIs/POs, latches, nodes, and nets
     ABC_TYPE_LOGIC,     // 2:  network with PIs/POs, latches, and nodes
     ABC_TYPE_STRASH,    // 3:  structurally hashed AIG (two input AND gates with c-attributes on edges)
@@ -53,7 +53,7 @@ typedef enum {
 
 // network functionality
 typedef enum { 
-    ABC_FUNC_NONE,      // 0:  unknown
+    ABC_FUNC_NONE = 0,  // 0:  unknown
     ABC_FUNC_SOP,       // 1:  sum-of-products
     ABC_FUNC_BDD,       // 2:  binary decision diagrams
     ABC_FUNC_AIG,       // 3:  and-inverter graphs
@@ -76,7 +76,7 @@ typedef enum {
 
 // object types
 typedef enum { 
-    ABC_OBJ_NONE,       // 0:  unknown
+    ABC_OBJ_NONE = 0,   // 0:  unknown
     ABC_OBJ_NET,        // 1:  net
     ABC_OBJ_NODE,       // 2:  node
     ABC_OBJ_LATCH,      // 3:  latch
@@ -85,6 +85,14 @@ typedef enum {
     ABC_OBJ_OTHER       // 6:  unused
 } Abc_ObjType_t;
 
+// latch initial values
+typedef enum { 
+    ABC_INIT_NONE = 0,  // 0:  unknown
+    ABC_INIT_ZERO,      // 1:  zero
+    ABC_INIT_ONE,       // 2:  one
+    ABC_INIT_DC         // 3:  don't-care
+} Abc_InitType_t;
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -317,13 +325,6 @@ static inline void        Abc_ObjSetFaninL1( Abc_Obj_t * pObj, int 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;              }
-extern int                Abc_ObjFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout );
-extern void               Abc_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats );
-extern void               Abc_ObjAddFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats );  
-extern int                Abc_ObjFanoutLMin( Abc_Obj_t * pObj );
-extern int                Abc_ObjFanoutLMax( Abc_Obj_t * pObj );
-extern int                Abc_ObjFanoutLSum( Abc_Obj_t * pObj );
-extern int                Abc_ObjFaninLSum( Abc_Obj_t * pObj );
 
 // checking the node type
 static inline bool        Abc_NodeIsAigAnd( Abc_Obj_t * pNode )      { assert(Abc_NtkHasAig(pNode->pNtk));           return Abc_ObjFaninNum(pNode) == 2;                         }
@@ -342,12 +343,12 @@ static inline bool        Abc_NodeIsTravIdCurrent( Abc_Obj_t * pNode )       { r
 static inline bool        Abc_NodeIsTravIdPrevious( Abc_Obj_t * pNode )      { return (bool)(pNode->TravId == pNode->pNtk->nTravIds - 1); }
 
 // checking initial state of the latches
-static inline void        Abc_LatchSetInit0( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)0;          }
-static inline void        Abc_LatchSetInit1( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)1;          }
-static inline void        Abc_LatchSetInitDc( Abc_Obj_t * pLatch )  { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)2;          }
-static inline bool        Abc_LatchIsInit0( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)0;  }
-static inline bool        Abc_LatchIsInit1( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)1;  }
-static inline bool        Abc_LatchIsInitDc( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)2;  }
+static inline void        Abc_LatchSetInit0( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_ZERO;         }
+static inline void        Abc_LatchSetInit1( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_ONE;          }
+static inline void        Abc_LatchSetInitDc( Abc_Obj_t * pLatch )  { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_DC;           }
+static inline bool        Abc_LatchIsInit0( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ZERO; }
+static inline bool        Abc_LatchIsInit1( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ONE;  }
+static inline bool        Abc_LatchIsInitDc( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_DC;   }
 static inline int         Abc_LatchInit( Abc_Obj_t * pLatch )       { assert(Abc_ObjIsLatch(pLatch)); return (int)pLatch->pData;          }
 
 // outputs the runtime in seconds
@@ -409,7 +410,6 @@ extern int                Abc_AigCleanup( Abc_Aig_t * pMan );
 extern bool               Abc_AigCheck( Abc_Aig_t * pMan );
 extern int                Abc_AigGetLevelNum( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_AigConst1( Abc_Aig_t * pMan );
-extern Abc_Obj_t *        Abc_AigReset( Abc_Aig_t * pMan );
 extern Abc_Obj_t *        Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
 extern Abc_Obj_t *        Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
 extern Abc_Obj_t *        Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
@@ -515,6 +515,7 @@ extern char *             Abc_NtkRegisterNamePlus( Abc_Ntk_t * pNtk, char * pNam
 extern char *             Abc_ObjName( Abc_Obj_t * pNode );
 extern char *             Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix );
 extern char *             Abc_ObjNameUnique( Abc_Ntk_t * pNtk, char * pName );
+extern char *             Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits );
 extern char *             Abc_NtkLogicStoreName( Abc_Obj_t * pNodeNew, char * pNameOld );
 extern char *             Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pNodeNew, char * pNameOld, char * pSuffix );
 extern void               Abc_NtkCreateCioNamesTable( Abc_Ntk_t * pNtk );
@@ -585,20 +586,6 @@ extern DdNode *           Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pN
 /*=== abcSat.c ==========================================================*/
 extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose );
 extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk );
-
-/*=== abcForBack.c ==========================================================*/
-extern void               Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk );
-/*=== abcLogic.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk );
-/*=== abcRetime.c ==========================================================*/
-extern void               Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk );
-/*=== abcSeq.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkAigToSeq( Abc_Ntk_t * pNtk );
-/*=== abcUtil.c ==========================================================*/
-extern int                Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk );
-
 /*=== abcSop.c ==========================================================*/
 extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
 extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 701fb90f..e1361eb7 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -49,7 +49,7 @@ struct Abc_Aig_t_
 {
     Abc_Ntk_t *       pNtkAig;           // the AIG network
     Abc_Obj_t *       pConst1;           // the constant 1 node
-    Abc_Obj_t *       pReset;            // the sequential reset node
+//    Abc_Obj_t *       pReset;            // the sequential reset node
     Abc_Obj_t **      pBins;             // the table bins
     int               nBins;             // the size of the table
     int               nEntries;          // the total number of entries in the table
@@ -125,9 +125,8 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
     pMan->pNtkAig = pNtkAig;
     // allocate constant nodes
     pMan->pConst1 = Abc_NtkCreateNode( pNtkAig );    
-    pMan->pReset  = Abc_NtkCreateNode( pNtkAig );
     // subtract these nodes from the total number
-    pNtkAig->nNodes -= 2;
+    pNtkAig->nNodes -= 1;
     return pMan;
 }
 
@@ -153,7 +152,6 @@ Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, Abc_Aig_t * pManNew )
     assert( Abc_NtkLatchNum(pMan->pNtkAig) == Abc_NtkLatchNum(pManNew->pNtkAig) );
     // set mapping of the constant nodes
     Abc_AigConst1( pMan )->pCopy = Abc_AigConst1( pManNew );
-    Abc_AigReset( pMan )->pCopy  = Abc_AigReset( pManNew );
     // set the mapping of CIs/COs
     Abc_NtkForEachPi( pMan->pNtkAig, pObj, i )
         pObj->pCopy = Abc_NtkPi( pManNew->pNtkAig, i );
@@ -264,7 +262,7 @@ bool Abc_AigCheck( Abc_Aig_t * pMan )
         nFanins = Abc_ObjFaninNum(pObj);
         if ( nFanins == 0 )
         {
-            if ( pObj != pMan->pConst1 && pObj != pMan->pReset )
+            if ( pObj != pMan->pConst1 )
             {
                 printf( "Abc_AigCheck: The AIG has non-standard constant nodes.\n" );
                 return 0;
@@ -340,22 +338,6 @@ Abc_Obj_t * Abc_AigConst1( Abc_Aig_t * pMan )
     return pMan->pConst1; 
 } 
 
-/**Function*************************************************************
-
-  Synopsis    [Read the reset node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_AigReset( Abc_Aig_t * pMan )  
-{ 
-    return pMan->pReset; 
-} 
-
 
 
 /**Function*************************************************************
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index b91a1291..773096a0 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -565,7 +565,7 @@ bool Abc_NtkCheckLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pLatch )
         Value = 0;
     }
     // make sure the latch has a reasonable return value
-    if ( (int)pLatch->pData < 0 || (int)pLatch->pData > 2 )
+    if ( (int)pLatch->pData < ABC_INIT_ZERO || (int)pLatch->pData > ABC_INIT_DC )
     {
         fprintf( stdout, "NodeCheck: Latch \"%s\" has incorrect reset value (%d).\n", 
             Abc_ObjName(pLatch), (int)pLatch->pData );
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index 2bf6461b..53ac6e07 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -162,6 +162,24 @@ char * Abc_ObjNameUnique( Abc_Ntk_t * pNtk, char * pName )
     return NULL;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the dummy PI name.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits )
+{
+    static char Buffer[100];
+    sprintf( Buffer, "%s%0*d", pPrefix, nDigits, Num );
+    return Buffer;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 08ee93bb..4cda189d 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "abcs.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index dc4dd9e2..e543bf19 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -504,6 +504,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     Vec_PtrFree( pNtk->vPtrTemp );
     Vec_IntFree( pNtk->vIntTemp );
     Vec_StrFree( pNtk->vStrTemp );
+    if ( pNtk->vInits )  Vec_IntFree( pNtk->vInits );
     // free the hash table of Obj name into Obj ID
     stmm_free_table( pNtk->tName2Net );
     stmm_free_table( pNtk->tObj2Name );
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index eddfd8b8..15753f4e 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -196,34 +196,6 @@ Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )
 
 /**Function*************************************************************
 
-  Synopsis    [Creates a new constant node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )  
-{ 
-    Abc_Obj_t * pReset, * pConst1;
-    assert( Abc_NtkHasAig(pNtkAig) );
-    assert( Abc_NtkIsLogic(pNtkNew) );
-    pReset = Abc_AigReset(pNtkAig->pManFunc);
-    if ( Abc_ObjFanoutNum(pReset) > 0 )
-    {
-        // create new latch with reset value 0
-        pReset->pCopy = Abc_NtkCreateLatch( pNtkNew );
-        // add constant node fanin to the latch
-        pConst1 = Abc_NodeCreateConst1( pNtkNew );
-        Abc_ObjAddFanin( pReset->pCopy, pConst1 );
-    }
-    return pReset->pCopy; 
-} 
-
-/**Function*************************************************************
-
   Synopsis    [Deletes the object from the network.]
 
   Description []
@@ -493,6 +465,7 @@ Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
     pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_LATCH );     
+    pObj->pData = (void *)ABC_INIT_NONE;
     Abc_ObjAdd( pObj );
     return pObj;
 }
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 0f7a4ab8..bc71143b 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -22,6 +22,7 @@
 #include "main.h"
 #include "mio.h"
 #include "dec.h"
+#include "abcs.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -931,9 +932,6 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk )
         pConst1 = Abc_AigConst1(pNtk->pManFunc);
         pConst1->Id = Vec_PtrSize( vObjsNew );
         Vec_PtrPush( vObjsNew, pConst1 );
-        pReset = Abc_AigReset(pNtk->pManFunc);
-        pReset->Id = Vec_PtrSize( vObjsNew );
-        Vec_PtrPush( vObjsNew, pReset );
     }
     // put PI nodes next
     Abc_NtkForEachPi( pNtk, pNode, i )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f2cfaaf1..4745273e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -25,6 +25,7 @@
 #include "fpga.h"
 #include "pga.h"
 #include "cut.h"
+#include "abcs.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -3981,6 +3982,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fForward;
     int fBackward;
+    int fInitial;
 
     extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk );
 
@@ -3989,10 +3991,11 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fForward = 0;
+    fForward  = 0;
     fBackward = 0;
+    fInitial  = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "fbh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "fbih" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4002,6 +4005,9 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'b':
             fBackward ^= 1;
             break;
+        case 'i':
+            fInitial ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -4030,15 +4036,18 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_NtkSeqRetimeForward( pNtk );
     else if ( fBackward )
         Abc_NtkSeqRetimeBackward( pNtk );
+    else if ( fInitial )
+        Abc_NtkSeqRetimeInitial( pNtk );
     else
         Abc_NtkSeqRetimeDelay( pNtk );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: retime [-fbh]\n" );
-    fprintf( pErr, "\t        retimes sequential AIG (default is Pan's algorithm)\n" );
+    fprintf( pErr, "usage: retime [-fbih]\n" );
+    fprintf( pErr, "\t        retimes sequential AIG (default is Pan's delay-optimal retiming)\n" );
     fprintf( pErr, "\t-f    : toggle forward retiming [default = %s]\n", fForward? "yes": "no" );
     fprintf( pErr, "\t-b    : toggle backward retiming [default = %s]\n", fBackward? "yes": "no" );
+    fprintf( pErr, "\t-i    : toggle retiming for initial state [default = %s]\n", fInitial? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 7a8eed5d..fe4f0511 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -88,7 +88,7 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
     ProgressBar * pProgress;
     Fraig_Node_t * pNodeFraig;
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode, * pConst1, * pReset;
+    Abc_Obj_t * pNode, * pConst1;
     int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
     int i;
 
@@ -102,7 +102,6 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
     Abc_NtkForEachCi( pNtk, pNode, i )
         pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
     pConst1 = Abc_AigConst1( pNtk->pManFunc );
-    pReset  = Abc_AigReset( pNtk->pManFunc );
 
     // perform strashing
     vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
@@ -114,8 +113,6 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
             Extra_ProgressBarUpdate( pProgress, i, NULL );
         if ( pNode == pConst1 )
             pNodeFraig = Fraig_ManReadConst1(pMan);
-        else if ( pNode == pReset )
-            continue;
         else
             pNodeFraig = Fraig_NodeAnd( pMan, 
                 Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index e4af8e12..26ce3665 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "dec.h"
+#include "abcs.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/base/abcs/abcForBack.c b/src/base/abcs/abcForBack.c
deleted file mode 100644
index 4db162e1..00000000
--- a/src/base/abcs/abcForBack.c
+++ /dev/null
@@ -1,161 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [abcForBack.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Simple forward/backward retiming procedures.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: abcForBack.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Performs forward retiming of the sequential AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk )
-{
-    Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode, * pFanout;
-    int i, k, nLatches;
-    assert( Abc_NtkIsSeq( pNtk ) );
-    // assume that all nodes can be retimed
-    vNodes = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        if ( Abc_NodeIsConst(pNode) )
-            continue;
-        Vec_PtrPush( vNodes, pNode );
-        pNode->fMarkA = 1;
-    }
-    // process the nodes
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-//        printf( "(%d,%d) ", Abc_ObjFaninL0(pNode), Abc_ObjFaninL0(pNode) );
-        // get the number of latches to retime
-        nLatches = Abc_ObjFaninLMin(pNode);
-        if ( nLatches == 0 )
-            continue;
-        assert( nLatches > 0 );
-        // subtract these latches on the fanin side
-        Abc_ObjAddFaninL0( pNode, -nLatches );
-        Abc_ObjAddFaninL1( pNode, -nLatches );
-        // add these latches on the fanout size
-        Abc_ObjForEachFanout( pNode, pFanout, k )
-        {
-            Abc_ObjAddFanoutL( pNode, pFanout, nLatches );
-            if ( pFanout->fMarkA == 0 )
-            {   // schedule the node for updating
-                Vec_PtrPush( vNodes, pFanout );
-                pFanout->fMarkA = 1;
-            }
-        }
-        // unmark the node as processed
-        pNode->fMarkA = 0;
-    }
-    Vec_PtrFree( vNodes );
-    // clean the marks
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        pNode->fMarkA = 0;
-        if ( Abc_NodeIsConst(pNode) )
-            continue;
-        assert( Abc_ObjFaninLMin(pNode) == 0 );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs forward retiming of the sequential AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk )
-{
-    Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode, * pFanin, * pFanout;
-    int i, k, nLatches;
-    assert( Abc_NtkIsSeq( pNtk ) );
-    // assume that all nodes can be retimed
-    vNodes = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        if ( Abc_NodeIsConst(pNode) )
-            continue;
-        Vec_PtrPush( vNodes, pNode );
-        pNode->fMarkA = 1;
-    }
-    // process the nodes
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-        // get the number of latches to retime
-        nLatches = Abc_ObjFanoutLMin(pNode);
-        if ( nLatches == 0 )
-            continue;
-        assert( nLatches > 0 );
-        // subtract these latches on the fanout side
-        Abc_ObjForEachFanout( pNode, pFanout, k )
-            Abc_ObjAddFanoutL( pNode, pFanout, -nLatches );
-        // add these latches on the fanin size
-        Abc_ObjForEachFanin( pNode, pFanin, k )
-        {
-            Abc_ObjAddFaninL( pNode, k, nLatches );
-            if ( Abc_ObjIsPi(pFanin) || Abc_NodeIsConst(pFanin) )
-                continue;
-            if ( pFanin->fMarkA == 0 )
-            {   // schedule the node for updating
-                Vec_PtrPush( vNodes, pFanin );
-                pFanin->fMarkA = 1;
-            }
-        }
-        // unmark the node as processed
-        pNode->fMarkA = 0;
-    }
-    Vec_PtrFree( vNodes );
-    // clean the marks
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        pNode->fMarkA = 0;
-        if ( Abc_NodeIsConst(pNode) )
-            continue;
-//        assert( Abc_ObjFanoutLMin(pNode) == 0 );
-    }
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/base/abcs/abcLogic.c b/src/base/abcs/abcLogic.c
deleted file mode 100644
index f33ed40e..00000000
--- a/src/base/abcs/abcLogic.c
+++ /dev/null
@@ -1,140 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [abcSeq.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: abcSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, int nLatches, int Init );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Converts a sequential AIG into a logic SOP network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
-{
-    Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pObjNew, * pFaninNew;
-    Vec_Ptr_t * vCutset;
-    char Buffer[100];
-    int i, Init, nDigits;
-    assert( Abc_NtkIsSeq(pNtk) );
-    // start the network
-    vCutset = pNtk->vLats;  pNtk->vLats = Vec_PtrAlloc( 0 );
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
-    Vec_PtrFree( pNtk->vLats );  pNtk->vLats = vCutset;
-    // create the constant node
-    Abc_NtkDupConst1( pNtk, pNtkNew );
-    // duplicate the nodes, create node functions and latches
-    Abc_AigForEachAnd( pNtk, pObj, i )
-    {
-        Abc_NtkDupObj(pNtkNew, pObj);
-        pObj->pCopy->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
-    }
-    // connect the objects
-    Abc_AigForEachAnd( pNtk, pObj, i )
-    {
-        // get the initial states of the latches on the fanin edge of this node
-        Init = Vec_IntEntry( pNtk->vInits, pObj->Id );
-        // create the edge
-        pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninL0(pObj), Init & 0xFFFF );
-        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
-        // create the edge
-        pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin1(pObj), Abc_ObjFaninL1(pObj), Init >> 16 );
-        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
-        // the complemented edges are subsumed by node function
-    }
-    // set the complemented attributed of CO edges (to be fixed by making simple COs)
-    Abc_NtkForEachPo( pNtk, pObj, i )
-    {
-        // get the initial states of the latches on the fanin edge of this node
-        Init = Vec_IntEntry( pNtk->vInits, pObj->Id );
-        // create the edge
-        pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninL0(pObj), Init & 0xFFFF );
-        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
-        // create the complemented edge
-        if ( Abc_ObjFaninC0(pObj) )
-            Abc_ObjSetFaninC( pObj->pCopy, 0 );
-    }
-    // count the number of digits in the latch names
-    nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
-    // add the latches and their names
-    Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
-    {
-        // add the latch to the CI/CO arrays
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
-        // create latch name
-        sprintf( Buffer, "L%0*d", nDigits, i );
-        Abc_NtkLogicStoreName( pObjNew, Buffer );
-    }
-    // fix the problem with complemented and duplicated CO edges
-    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
-    // duplicate the EXDC network
-    if ( pNtk->pExdc )
-        fprintf( stdout, "Warning: EXDC network is not copied.\n" );
-    if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkSeqToLogic(): Network check has failed.\n" );
-    return pNtkNew;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Creates latches on one edge.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, int nLatches, int Init )
-{
-    Abc_Obj_t * pLatch;
-    if ( nLatches == 0 )
-        return pFanin->pCopy;
-    pFanin = Abc_NodeSeqToLogic( pNtkNew, pFanin, nLatches - 1, Init >> 2 );
-    pLatch = Abc_NtkCreateLatch( pNtkNew );
-    pLatch->pData = (void *)(Init & 3);
-    Abc_ObjAddFanin( pLatch, pFanin );
-    return pLatch;    
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/base/abcs/abcRetCore.c b/src/base/abcs/abcRetCore.c
new file mode 100644
index 00000000..f6ba0c59
--- /dev/null
+++ b/src/base/abcs/abcRetCore.c
@@ -0,0 +1,145 @@
+/**CFile****************************************************************
+
+  FileName    [abcForBack.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Simple forward/backward retiming procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcForBack.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abcs.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+/* 
+    Retiming can be represented in three equivalent forms:
+    - as a set of integer lags for each node (array of chars by node ID)
+    - as a set of node numbers with lag for each, fwd and bwd (two arrays of Abc_RetStep_t_)
+    - as a set of node moves, fwd and bwd (two arrays arrays of Abc_Obj_t *)
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs most forward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vMoves;
+    Abc_Obj_t * pNode;
+    int i;
+    // get the forward moves
+    vMoves = Abc_NtkUtilRetimingTry( pNtk, 1 );
+    // undo the forward moves
+    Vec_PtrForEachEntryReverse( vMoves, pNode, i )
+        Abc_ObjRetimeBackwardTry( pNode, 1 );
+    // implement this forward retiming
+    Abc_NtkImplementRetimingForward( pNtk, vMoves );
+    Vec_PtrFree( vMoves ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs most backward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vMoves;
+    Abc_Obj_t * pNode;
+    int i, RetValue;
+    // get the backward moves
+    vMoves = Abc_NtkUtilRetimingTry( pNtk, 0 );
+    // undo the backward moves
+    Vec_PtrForEachEntryReverse( vMoves, pNode, i )
+        Abc_ObjRetimeForwardTry( pNode, 1 );
+    // implement this backward retiming
+    RetValue = Abc_NtkImplementRetimingBackward( pNtk, vMoves );
+    Vec_PtrFree( vMoves ); 
+    if ( RetValue == 0 )
+        printf( "Retiming completed but initial state computation has failed.\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs performs optimal delay retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk )
+{
+    Vec_Str_t * vLags;
+    int RetValue;
+    // get the retiming vector
+    vLags = Abc_NtkSeqRetimeDelayLags( pNtk );
+    // implement this retiming
+    RetValue = Abc_NtkImplementRetiming( pNtk, vLags );
+    Vec_StrFree( vLags ); 
+    if ( RetValue == 0 )
+        printf( "Retiming completed but initial state computation has failed.\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs retiming for initial state computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSeqRetimeInitial( Abc_Ntk_t * pNtk )
+{
+    Vec_Str_t * vLags;
+    int RetValue;
+    // get the retiming vector
+    vLags = Abc_NtkSeqRetimeDelayLags( pNtk );
+    // implement this retiming
+    RetValue = Abc_NtkImplementRetiming( pNtk, vLags );
+    Vec_StrFree( vLags ); 
+    if ( RetValue == 0 )
+        printf( "Retiming completed but initial state computation has failed.\n" );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abcs/abcRetime.c b/src/base/abcs/abcRetDelay.c
index 13b8a926..71114171 100644
--- a/src/base/abcs/abcRetime.c
+++ b/src/base/abcs/abcRetDelay.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
+#include "abcs.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -51,9 +51,11 @@ enum { ABC_UPDATE_FAIL, ABC_UPDATE_NO, ABC_UPDATE_YES };
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk )
+Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk )
 {
-    int FiMax, FiBest;
+    Vec_Str_t * vLags;
+    Abc_Obj_t * pNode;
+    int i, FiMax, FiBest;
     assert( Abc_NtkIsSeq( pNtk ) );
 
     // start storage for sequential arrival times
@@ -71,9 +73,15 @@ void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk )
     // print the result
     printf( "The best clock period is %3d.\n", FiBest );
 
+    // convert to lags
+    vLags = Vec_StrStart( Abc_NtkObjNumMax(pNtk) );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        Vec_StrWriteEntry( vLags, i, (char)(Abc_NodeReadLValue(pNode) / FiBest) );
+
     // free storage
     Vec_IntFree( pNtk->pData );
     pNtk->pData = NULL;
+    return vLags;
 }
 
 /**Function*************************************************************
diff --git a/src/base/abcs/abcRetImpl.c b/src/base/abcs/abcRetImpl.c
new file mode 100644
index 00000000..9a28a354
--- /dev/null
+++ b/src/base/abcs/abcRetImpl.c
@@ -0,0 +1,362 @@
+/**CFile****************************************************************
+
+  FileName    [abcRetImpl.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Implementation of retiming.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcRetImpl.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abcs.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_ObjRetimeForward( Abc_Obj_t * pObj );
+static int  Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtk, stmm_table * tTable, Vec_Int_t * vValues );
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the retiming on the sequential AIG.]
+
+  Description [Split the retiming into forward and backward.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags )
+{
+    Vec_Int_t * vSteps;
+    Vec_Ptr_t * vMoves;
+    int RetValue;
+
+    // forward retiming
+    vSteps = Abc_NtkUtilRetimingSplit( vLags, 1 );
+    // translate each set of steps into moves
+    vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 1 );
+    // implement this retiming
+    Abc_NtkImplementRetimingForward( pNtk, vMoves );
+    Vec_IntFree( vSteps );
+    Vec_PtrFree( vMoves );
+
+    // backward retiming
+    vSteps = Abc_NtkUtilRetimingSplit( vLags, 0 );
+    // translate each set of steps into moves
+    vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 0 );
+    // implement this retiming
+    RetValue = Abc_NtkImplementRetimingBackward( pNtk, vMoves );
+    Vec_IntFree( vSteps );
+    Vec_PtrFree( vMoves );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the given retiming on the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    Vec_PtrForEachEntry( vMoves, pNode, i )
+        Abc_ObjRetimeForward( pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the given retiming on the sequential AIG.]
+
+  Description [Returns 0 of initial state computation fails.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
+{
+    Abc_RetEdge_t RetEdge;
+    stmm_table * tTable;
+    stmm_generator * gen;
+    Vec_Int_t * vValues;
+    Abc_Ntk_t * pNtkProb, * pNtkMiter, * pNtkCnf;
+    Abc_Obj_t * pNode, * pNodeNew;
+    int * pModel, Init, nDigits, RetValue, i;
+
+    // return if the retiming is trivial
+    if ( Vec_PtrSize(vMoves) == 0 )
+        return 1;
+
+    // start the table and the array of PO values
+    tTable = stmm_init_table( stmm_numcmp, stmm_numhash );
+    vValues = Vec_IntAlloc( 100 );
+
+    // create the network for the initial state computation
+    pNtkProb = Abc_NtkAlloc( ABC_TYPE_LOGIC, ABC_FUNC_SOP );
+
+    // perform the backward moves and build the network
+    Vec_PtrForEachEntry( vMoves, pNode, i )
+        Abc_ObjRetimeBackward( pNode, pNtkProb, tTable, vValues );
+
+    // add the PIs corresponding to the white spots
+    stmm_foreach_item( tTable, gen, (char **)&RetEdge, (char **)&pNodeNew )
+        Abc_ObjAddFanin( pNodeNew, Abc_NtkCreatePi(pNtkProb) );
+
+    // add the PI/PO names
+    nDigits = Extra_Base10Log( Abc_NtkPiNum(pNtkProb) );
+    Abc_NtkForEachPi( pNtkProb, pNodeNew, i )
+        Abc_NtkLogicStoreName( pNodeNew, Abc_ObjNameDummy("pi", i, nDigits) );
+    nDigits = Extra_Base10Log( Abc_NtkPoNum(pNtkProb) );
+    Abc_NtkForEachPo( pNtkProb, pNodeNew, i )
+        Abc_NtkLogicStoreName( pNodeNew, Abc_ObjNameDummy("po", i, nDigits) );
+
+    // make sure everything is okay with the network structure
+    if ( !Abc_NtkDoCheck( pNtkProb ) )
+    {
+        printf( "Abc_NtkImplementRetimingBackward: The internal network check has failed.\n" );
+        return 0;
+    }
+
+    // get the miter cone
+    pNtkMiter = Abc_NtkCreateCone( pNtkProb, pNtkProb->vCos, vValues );
+    Abc_NtkDelete( pNtkProb );
+    Vec_IntFree( vValues );
+
+    // transform the miter into a logic network for efficient CNF construction
+    pNtkCnf = Abc_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 );
+    Abc_NtkDelete( pNtkMiter );
+
+    // solve the miter
+    RetValue = Abc_NtkMiterSat( pNtkCnf, 30, 0 );
+    pModel = pNtkCnf->pModel;  pNtkCnf->pModel = NULL;
+    Abc_NtkDelete( pNtkCnf );
+
+    // analyze the result
+    if ( RetValue == -1 || RetValue == 1 )
+    {
+        stmm_free_table( tTable );
+        return 0;
+    }
+
+    // set the values of the latches
+    i = 0;
+    stmm_foreach_item( tTable, gen, (char **)&RetEdge, (char **)&pNodeNew )
+    {
+        pNode = Abc_NtkObj( pNtk, RetEdge.iNode );
+        Init = pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO;
+        Abc_ObjFaninLSetInitOne( pNode, RetEdge.iEdge, RetEdge.iLatch, Init );
+        i++;
+    }
+    stmm_free_table( tTable );
+    free( pModel );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retimes node forward by one latch.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjRetimeForward( Abc_Obj_t * pObj )  
+{
+    Abc_Obj_t * pFanout;
+    int Init0, Init1, Init, i;
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    assert( Abc_ObjFaninL0(pObj) >= 1 );
+    assert( Abc_ObjFaninL1(pObj) >= 1 );
+    // remove the init values from the fanins
+    Init0 = Abc_ObjFaninLDeleteFirst( pObj, 0 );
+    Init1 = Abc_ObjFaninLDeleteFirst( pObj, 1 );
+    assert( Init0 != ABC_INIT_NONE );
+    assert( Init1 != ABC_INIT_NONE );
+    // take into account the complements in the node
+    if ( Abc_ObjFaninC0(pObj) )
+    {
+        if ( Init0 == ABC_INIT_ZERO )
+            Init0 = ABC_INIT_ONE;
+        else if ( Init0 == ABC_INIT_ONE )
+            Init0 = ABC_INIT_ZERO;
+    }
+    if ( Abc_ObjFaninC1(pObj) )
+    {
+        if ( Init1 == ABC_INIT_ZERO )
+            Init1 = ABC_INIT_ONE;
+        else if ( Init1 == ABC_INIT_ONE )
+            Init1 = ABC_INIT_ZERO;
+    }
+    // compute the value at the output of the node
+    if ( Init0 == ABC_INIT_ZERO || Init1 == ABC_INIT_ZERO )
+        Init = ABC_INIT_ZERO;
+    else if ( Init0 == ABC_INIT_ONE && Init1 == ABC_INIT_ONE )
+        Init = ABC_INIT_ONE;
+    else
+        Init = ABC_INIT_DC;
+    // add the init values to the fanouts
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        Abc_ObjFaninLInsertLast( pFanout, Abc_ObjEdgeNum(pFanout, pObj), Init );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retimes node backward by one latch.]
+
+  Description [Constructs the problem for initial state computation.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * tTable, Vec_Int_t * vValues )  
+{
+    Abc_Obj_t * pFanout;
+    Abc_InitType_t Init, Value;
+    Abc_RetEdge_t Edge;
+    Abc_Obj_t * pNodeNew, * pFanoutNew, * pBuf;
+    unsigned Entry;
+    int i, fMet0, fMet1, fMetX;
+
+    // make sure the node can be retimed
+    assert( Abc_ObjFanoutLMin(pObj) > 0 );
+    // get the fanout values
+    fMet0 = fMet1 = fMetX = 0;
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        Init = Abc_ObjFaninLGetInitLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout) );
+        if ( Init == ABC_INIT_ZERO )
+            fMet0 = 1;
+        else if ( Init == ABC_INIT_ONE )
+            fMet1 = 1;
+        else if ( Init == ABC_INIT_NONE )
+            fMetX = 1;
+    }
+    // quit if conflict is found
+    if ( fMet0 && fMet1 )
+        return 0;
+
+    // get the new initial value
+    if ( !fMet0 && !fMet1 && !fMetX )
+    {
+        Init = ABC_INIT_DC;
+        // do not add the node
+        pNodeNew = NULL;
+    }
+    else
+    {
+        Init = ABC_INIT_NONE;
+        // add the node to the network
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );
+        pNodeNew->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+    }
+
+    // perform the changes
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        Edge.iNode = pFanout->Id;
+        Edge.iEdge = Abc_ObjEdgeNum(pObj, pFanout);
+        Edge.iLatch = Abc_ObjFaninL( pFanout, Edge.iEdge ) - 1;
+        // try to delete this edge
+        stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew );
+        // delete the entry
+        Value = Abc_ObjFaninLDeleteLast( pFanout, Edge.iEdge );
+        if ( Value == ABC_INIT_NONE )
+            Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+    }
+
+    // update the table for each of the edges
+    Abc_ObjFaninLForEachValue( pObj, 0, Entry, i, Value )
+    {
+        if ( Value != ABC_INIT_NONE )
+            continue;
+        if ( !stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew ) )
+            assert( 0 );
+        Edge.iLatch++;
+        if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pFanoutNew ) )
+            assert( 0 );
+    }
+    Abc_ObjFaninLForEachValue( pObj, 1, Entry, i, Value )
+    {
+        if ( Value != ABC_INIT_NONE )
+            continue;
+        if ( !stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew ) )
+            assert( 0 );
+        Edge.iLatch++;
+        if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pFanoutNew ) )
+            assert( 0 );
+    }
+    Abc_ObjFaninLInsertFirst( pObj, 0, Init );
+    Abc_ObjFaninLInsertFirst( pObj, 1, Init );
+
+    // do not insert the don't-care node into the network
+    if ( Init == ABC_INIT_DC )
+        return 1;
+
+    // add the buffer
+    pBuf = Abc_NtkCreateNode( pNtkNew );
+    pBuf->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+    Abc_ObjAddFanin( pNodeNew, pBuf );
+    // point to it from the table
+    Edge.iNode = pObj->Id;
+    Edge.iEdge = 0;
+    Edge.iLatch = 0;
+    if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pBuf ) )
+        assert( 0 );
+
+    // add the buffer
+    pBuf = Abc_NtkCreateNode( pNtkNew );
+    pBuf->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+    Abc_ObjAddFanin( pNodeNew, pBuf );
+    // point to it from the table
+    Edge.iNode = pObj->Id;
+    Edge.iEdge = 1;
+    Edge.iLatch = 0;
+    if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pBuf ) )
+        assert( 0 );
+
+    // check if the output value is required
+    if ( fMet0 || fMet1 )
+    {
+        // add the PO and the value
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
+        Vec_IntPush( vValues, fMet1 );
+    }
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abcs/abcRetUtil.c b/src/base/abcs/abcRetUtil.c
new file mode 100644
index 00000000..52ea6446
--- /dev/null
+++ b/src/base/abcs/abcRetUtil.c
@@ -0,0 +1,227 @@
+/**CFile****************************************************************
+
+  FileName    [abcRetUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Retiming utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcRetUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abcs.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs forward retiming of the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward )
+{
+    Vec_Ptr_t * vNodes, * vMoves;
+    Abc_Obj_t * pNode, * pFanout, * pFanin;
+    int i, k, nLatches;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    // assume that all nodes can be retimed
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        Vec_PtrPush( vNodes, pNode );
+        pNode->fMarkA = 1;
+    }
+    // process the nodes
+    vMoves = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+//        printf( "(%d,%d) ", Abc_ObjFaninL0(pNode), Abc_ObjFaninL0(pNode) );
+        // unmark the node as processed
+        pNode->fMarkA = 0;
+        // get the number of latches to retime
+        if ( fForward )
+            nLatches = Abc_ObjFaninLMin(pNode);
+        else
+            nLatches = Abc_ObjFanoutLMin(pNode);
+        if ( nLatches == 0 )
+            continue;
+        assert( nLatches > 0 );
+        // retime the latches forward
+        if ( fForward )
+            Abc_ObjRetimeForwardTry( pNode, nLatches );
+        else
+            Abc_ObjRetimeBackwardTry( pNode, nLatches );
+        // write the moves
+        for ( k = 0; k < nLatches; k++ )
+            Vec_PtrPush( vMoves, pNode );
+        // schedule fanouts for updating
+        if ( fForward )
+        {
+            Abc_ObjForEachFanout( pNode, pFanout, k )
+            {
+                if ( Abc_ObjFaninNum(pFanout) != 2 || pFanout->fMarkA )
+                    continue;
+                pFanout->fMarkA = 1;
+                Vec_PtrPush( vNodes, pFanout );
+            }
+        }
+        else
+        {
+            Abc_ObjForEachFanin( pNode, pFanin, k )
+            {
+                if ( Abc_ObjFaninNum(pFanin) != 2 || pFanin->fMarkA )
+                    continue;
+                pFanin->fMarkA = 1;
+                Vec_PtrPush( vNodes, pFanin );
+            }
+        }
+    }
+    Vec_PtrFree( vNodes );
+    // make sure the marks are clean the the retiming is final
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        assert( pNode->fMarkA == 0 );
+        if ( fForward ) 
+            assert( Abc_ObjFaninLMin(pNode) == 0 );
+        else
+            assert( Abc_ObjFanoutLMin(pNode) == 0 );
+    }
+    return vMoves;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Translates retiming steps into retiming moves.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, bool fForward )
+{
+    Abc_RetStep_t RetStep;
+    Vec_Ptr_t * vMoves;
+    Abc_Obj_t * pNode;
+    int i, k, iNode, nLatches, Number;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    // process the nodes
+    vMoves = Vec_PtrAlloc( 100 );
+    while ( Vec_IntSize(vSteps) > 0 )
+    {
+        iNode = 0;
+        Vec_IntForEachEntry( vSteps, Number, i )
+        {
+            // get the retiming step
+            RetStep = Abc_Int2RetStep( Number );
+            // get the node to be retimed
+            pNode = Abc_NtkObj( pNtk, RetStep.iNode );
+            assert( RetStep.nLatches > 0 );
+            // get the number of latches that can be retimed
+            if ( fForward )
+                nLatches = Abc_ObjFaninLMin(pNode);
+            else
+                nLatches = Abc_ObjFanoutLMin(pNode);
+            if ( nLatches == 0 )
+            {
+                Vec_IntWriteEntry( vSteps, iNode++, Abc_RetStep2Int(RetStep) );
+                continue;
+            }
+            assert( nLatches > 0 );
+            // get the number of latches to be retimed over this node
+            nLatches = ABC_MIN( nLatches, (int)RetStep.nLatches );
+            // retime the latches forward
+            if ( fForward )
+                Abc_ObjRetimeForwardTry( pNode, nLatches );
+            else
+                Abc_ObjRetimeBackwardTry( pNode, nLatches );
+            // write the moves
+            for ( k = 0; k < nLatches; k++ )
+                Vec_PtrPush( vMoves, pNode );
+            // subtract the retiming performed
+            RetStep.nLatches -= nLatches;
+            // store the node if it is not retimed completely
+            if ( RetStep.nLatches > 0 )
+                Vec_IntWriteEntry( vSteps, iNode++, Abc_RetStep2Int(RetStep) );
+        }
+        // reduce the array
+        Vec_IntShrink( vSteps, iNode );
+    }
+    // undo the tentative retiming
+    if ( fForward )
+    {
+        Vec_PtrForEachEntryReverse( vMoves, pNode, i )
+            Abc_ObjRetimeBackwardTry( pNode, 1 );
+    }
+    else
+    {
+        Vec_PtrForEachEntryReverse( vMoves, pNode, i )
+            Abc_ObjRetimeForwardTry( pNode, 1 );
+    }
+    return vMoves;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Splits retiming into forward and backward.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward )
+{
+    Vec_Int_t * vNodes;
+    Abc_RetStep_t RetStep;
+    int Value, i;
+    vNodes = Vec_IntAlloc( 100 );
+    Vec_StrForEachEntry( vLags, Value, i )
+    {
+        if ( Value < 0 && fForward )
+        {
+            RetStep.iNode = i;
+            RetStep.nLatches = -Value;
+            Vec_IntPush( vNodes, Abc_RetStep2Int(RetStep) );
+        }
+        else if ( Value > 0 && !fForward )
+        {
+            RetStep.iNode = i;
+            RetStep.nLatches = Value;
+            Vec_IntPush( vNodes, Abc_RetStep2Int(RetStep) );
+        }
+    }
+    return vNodes;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abcs/abcSeq.c b/src/base/abcs/abcSeq.c
index eca337fd..1264a98d 100644
--- a/src/base/abcs/abcSeq.c
+++ b/src/base/abcs/abcSeq.c
@@ -18,20 +18,23 @@
 
 ***********************************************************************/
 
-#include "abc.h"
+#include "abcs.h"
 
 /*
     A sequential network is similar to AIG in that it contains only
     AND gates. However, the AND-gates are currently not hashed. 
-    Const1/PIs/POs remain the same as in the original AIG.
-    Instead of the latches, a new cutset is added, which is currently
-    defined as a set of AND gates that have a latch among their fanouts.
-    The edges of a sequential AIG are labeled with latch attributes
-    in addition to the complementation attibutes. 
-    The attributes contain information about the number of latches 
-    and their initial states. 
-    The number of latches is stored directly on the edges. The initial 
-    states are stored in a special array associated with the network.
+
+    When converting AIG into sequential AIG:
+    - Const1/PIs/POs remain the same as in the original AIG.
+    - Instead of the latches, a new cutset is added, which is currently
+      defined as a set of AND gates that have a latch among their fanouts.
+    - The edges of a sequential AIG are labeled with latch attributes
+      in addition to the complementation attibutes. 
+    - The attributes contain information about the number of latches 
+       and their initial states. 
+    - The number of latches is stored directly on the edges. The initial 
+      states are stored in a special array associated with the network.
+
     The AIG of sequential network is static in the sense that the 
     new AIG nodes are never created.
     The retiming (or retiming/mapping) is performed by moving the
@@ -46,7 +49,8 @@
 ////////////////////////////////////////////////////////////////////////
 
 static Vec_Ptr_t * Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk );
-static Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pAnd, int Num, int * pnLatches, int * pnInit );
+static Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pAnd, int Num, int * pnLatches, unsigned * pnInit );
+static Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, int nLatches, unsigned Init );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -54,11 +58,11 @@ static Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pAnd, int Num, int * pnLatches,
 
 /**Function*************************************************************
 
-  Synopsis    [Converts a normal AIG into a sequential AIG.]
+  Synopsis    [Converts combinational AIG with latches into sequential AIG.]
 
   Description [The const/PI/PO nodes are duplicated. The internal
   nodes are duplicated in the topological order. The dangling nodes
-  are not copies. The choice nodes are copied.]
+  are not duplicated. The choice nodes are duplicated.]
                
   SideEffects []
 
@@ -69,8 +73,8 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew;
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pObj, * pFanin0, * pFanin1;
-    int i, nLatches0, nLatches1, Init0, Init1;
+    Abc_Obj_t * pObj, * pFanin;
+    int i, Init, nLatches;
     // make sure it is an AIG without self-feeding latches
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
@@ -93,32 +97,35 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
     // copy the internal nodes, including choices, excluding dangling
     vNodes = Abc_AigDfs( pNtk, 0, 0 );
     Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
         Abc_NtkDupObj(pNtkNew, pObj);
+        pObj->pCopy->fPhase = pObj->fPhase; // needed for choices
+    }
+    // relink the choice nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( pObj->pData )
+            pObj->pCopy->pData = ((Abc_Obj_t *)pObj->pData)->pCopy;
     Vec_PtrFree( vNodes );
     // start the storage for initial states
-    pNtkNew->vInits = Vec_IntStart( Abc_NtkObjNumMax(pNtkNew) );
+    pNtkNew->vInits = Vec_IntStart( 2 * Abc_NtkObjNumMax(pNtkNew) );
     // reconnect the internal nodes
-    Abc_AigForEachAnd( pNtk, pObj, i )
-    {
-        // process the fanins of the AND gate (pObj)
-        pFanin0 = Abc_NodeAigToSeq( pObj, 0, &nLatches0, &Init0 );
-        pFanin1 = Abc_NodeAigToSeq( pObj, 1, &nLatches1, &Init1 );
-        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin0) );
-        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin1) );
-        Abc_ObjAddFaninL0( pObj->pCopy, nLatches0 );
-        Abc_ObjAddFaninL1( pObj->pCopy, nLatches1 );
-        // add the initial state
-        Vec_IntWriteEntry( pNtkNew->vInits, pObj->pCopy->Id, (Init1 << 16) | Init0 );
-    }
-    // reconnect the POs
-    Abc_NtkForEachPo( pNtk, pObj, i )
+    Abc_NtkForEachObj( pNtk, pObj, i )
     {
-        // process the fanins
-        pFanin0 = Abc_NodeAigToSeq( pObj, 0, &nLatches0, &Init0 );
-        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin0) );
-        Abc_ObjAddFaninL0( pObj->pCopy, nLatches0 );
-        // add the initial state
-        Vec_IntWriteEntry( pNtkNew->vInits, pObj->pCopy->Id, Init0 );
+        // skip the constant and the PIs
+        if ( Abc_ObjFaninNum(pObj) == 0 )
+            continue;
+        // process the first fanin
+        pFanin = Abc_NodeAigToSeq( pObj, 0, &nLatches, &Init );
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin) );
+        Abc_ObjAddFaninL0( pObj->pCopy, nLatches );
+        Vec_IntWriteEntry( pNtkNew->vInits, 2 * i + 0, Init );
+        if ( Abc_ObjFaninNum(pObj) == 1 )
+            continue;
+        // process the second fanin
+        pFanin = Abc_NodeAigToSeq( pObj, 1, &nLatches, &Init );
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin) );
+        Abc_ObjAddFaninL1( pObj->pCopy, nLatches );
+        Vec_IntWriteEntry( pNtkNew->vInits, 2 * i + 1, Init );
     }
     // set the cutset composed of latch drivers
     pNtkNew->vLats = Abc_NtkAigCutsetCopy( pNtk );
@@ -170,24 +177,31 @@ Vec_Ptr_t * Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, int * pnInit )
+Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, unsigned * pnInit )
 {
     Abc_Obj_t * pFanin;
-    int Init;
+    Abc_InitType_t Init;
     // get the given fanin of the node
     pFanin = Abc_ObjFanin( pObj, Num );
     if ( !Abc_ObjIsLatch(pFanin) )
     {
-        *pnLatches = *pnInit = 0;
+        *pnLatches = 0;
+        *pnInit = 0;
         return Abc_ObjChild( pObj, Num );
     }
     pFanin = Abc_NodeAigToSeq( pFanin, 0, pnLatches, pnInit );
     // get the new initial state
     Init = Abc_LatchInit(pObj);
-    assert( Init >= 0 && Init <= 3 );
     // complement the initial state if the inv is retimed over the latch
-    if ( Abc_ObjIsComplement(pFanin) && Init < 2 ) // not a don't-care
-        Init ^= 3;
+    if ( Abc_ObjIsComplement(pFanin) ) 
+    {
+        if ( Init == ABC_INIT_ZERO )
+            Init = ABC_INIT_ONE;
+        else if ( Init == ABC_INIT_ONE )
+            Init = ABC_INIT_ZERO;
+        else if ( Init != ABC_INIT_DC )
+            assert( 0 );
+    }
     // update the latch number and initial state
     (*pnLatches)++;
     (*pnInit) = ((*pnInit) << 2) | Init;
@@ -195,6 +209,120 @@ Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, int *
 }
 
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Converts a sequential AIG into a logic SOP network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pObjNew, * pFaninNew;
+    int i, nCutNodes, nDigits;
+    unsigned Init;
+    assert( Abc_NtkIsSeq(pNtk) );
+    // start the network without latches
+    nCutNodes = pNtk->vLats->nSize; pNtk->vLats->nSize = 0;
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
+    pNtk->vLats->nSize = nCutNodes;
+    // create the constant node
+    Abc_NtkDupConst1( pNtk, pNtkNew );
+    // duplicate the nodes, create node functions
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        // skip the constant
+        if ( Abc_ObjFaninNum(pObj) == 0 )
+            continue;
+        // duplicate the node
+        Abc_NtkDupObj(pNtkNew, pObj);
+        if ( Abc_ObjFaninNum(pObj) == 1 )
+        {
+            assert( !Abc_ObjFaninC0(pObj) );
+            pObj->pCopy->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+            continue;
+        }
+        pObj->pCopy->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+    }
+    // connect the objects
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        // skip PIs and the constant
+        if ( Abc_ObjFaninNum(pObj) == 0 )
+            continue;
+        // get the initial states of the latches on the fanin edge of this node
+        Init = Vec_IntEntry( pNtk->vInits, 2 * pObj->Id );
+        // create the edge
+        pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninL0(pObj), Init );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        if ( Abc_ObjFaninNum(pObj) == 1 )
+        {
+            // create the complemented edge
+            if ( Abc_ObjFaninC0(pObj) )
+                Abc_ObjSetFaninC( pObj->pCopy, 0 );
+            continue;
+        }
+        // get the initial states of the latches on the fanin edge of this node
+        Init = Vec_IntEntry( pNtk->vInits, 2 * pObj->Id + 1 );
+        // create the edge
+        pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin1(pObj), Abc_ObjFaninL1(pObj), Init );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        // the complemented edges are subsumed by the node function
+    }
+    // count the number of digits in the latch names
+    nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
+    // add the latches and their names
+    Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
+    {
+        // add the latch to the CI/CO arrays
+        Vec_PtrPush( pNtkNew->vCis, pObjNew );
+        Vec_PtrPush( pNtkNew->vCos, pObjNew );
+        // create latch name
+        Abc_NtkLogicStoreName( pObjNew, Abc_ObjNameDummy("L", i, nDigits) );
+    }
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
+    // duplicate the EXDC network
+    if ( pNtk->pExdc )
+        fprintf( stdout, "Warning: EXDC network is not copied.\n" );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkSeqToLogic(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates latches on one edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, int nLatches, unsigned Init )
+{
+    Abc_Obj_t * pLatch;
+    if ( nLatches == 0 )
+        return pFanin->pCopy;
+    pFanin = Abc_NodeSeqToLogic( pNtkNew, pFanin, nLatches - 1, Init >> 2 );
+    pLatch = Abc_NtkCreateLatch( pNtkNew );
+    pLatch->pData = (void *)(Init & 3);
+    Abc_ObjAddFanin( pLatch, pFanin );
+    return pLatch;    
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abcs/abcShare.c b/src/base/abcs/abcShare.c
new file mode 100644
index 00000000..4f12b7bc
--- /dev/null
+++ b/src/base/abcs/abcShare.c
@@ -0,0 +1,154 @@
+/**CFile****************************************************************
+
+  FileName    [abcShare.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Procedures for latch sharing on the fanout edges.]
+
+  Synopsis    [Utilities working sequential AIGs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcShare.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abcs.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NodeSeqShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
+static void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, int Init, Vec_Ptr_t * vNodes );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the sequential AIG to take fanout sharing into account.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSeqShareFanouts( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    int i;
+    vNodes = Vec_PtrAlloc( 10 );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Abc_NodeSeqShareFanouts( pObj, vNodes );
+    Vec_PtrFree( vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the node to take fanout sharing into account.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSeqShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pFanout;
+    Abc_InitType_t Type;
+    int nLatches[4], i;
+    // skip the node with only one fanout
+    if ( Abc_ObjFanoutNum(pNode) < 2 )
+        return;
+    // clean the the fanout counters
+    for ( i = 0; i < 4; i++ )
+        nLatches[i] = 0;
+    // find the number of fanouts having latches of each type
+    Abc_ObjForEachFanout( pNode, pFanout, i )  
+    {
+        if ( Abc_ObjFanoutL(pNode, pFanout) == 0 )
+            continue;
+        Type = Abc_ObjFaninLGetInitLast( pFanout, Abc_ObjEdgeNum(pNode, pFanout) );
+        nLatches[Type]++;
+    }
+    // decide what to do
+    if ( nLatches[ABC_INIT_ZERO] > 1 && nLatches[ABC_INIT_ONE] > 1 ) // 0-group and 1-group
+    {
+        Abc_NodeSeqShareOne( pNode, ABC_INIT_ZERO, vNodes );     // shares 0 and DC
+        Abc_NodeSeqShareOne( pNode, ABC_INIT_ONE,  vNodes );     // shares 1 and DC
+    }
+    else if ( nLatches[ABC_INIT_ZERO] > 1 ) // 0-group
+        Abc_NodeSeqShareOne( pNode, ABC_INIT_ZERO, vNodes );     // shares 0 and DC
+    else if ( nLatches[ABC_INIT_ONE] > 1 ) // 1-group
+        Abc_NodeSeqShareOne( pNode, ABC_INIT_ONE,  vNodes );     // shares 1 and DC
+    else if ( nLatches[ABC_INIT_DC] > 1 ) // DC-group
+    {
+        if ( nLatches[ABC_INIT_ZERO] > 0 )
+            Abc_NodeSeqShareOne( pNode, ABC_INIT_ZERO, vNodes ); // shares 0 and DC
+        else 
+            Abc_NodeSeqShareOne( pNode, ABC_INIT_ONE,  vNodes ); // shares 1 and DC
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the node to take fanout sharing into account.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNodes )
+{
+    Vec_Int_t * vInits = pNode->pNtk->vInits;
+    Abc_Obj_t * pFanout, * pBuffer;
+    Abc_InitType_t Type, InitNew;
+    int i;
+    // collect the fanouts that satisfy the property (have initial value Init or DC)
+    InitNew = ABC_INIT_DC;
+    Vec_PtrClear( vNodes );
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+    {
+        Type = Abc_ObjFaninLGetInitLast( pFanout, Abc_ObjEdgeNum(pNode, pFanout) );
+        if ( Type == Init )
+            InitNew = Init;
+        if ( Type == Init || Type == ABC_INIT_DC )
+        {
+            Vec_PtrPush( vNodes, pFanout );
+            Abc_ObjFaninLDeleteLast( pFanout, Abc_ObjEdgeNum(pNode, pFanout) );
+        }
+    }
+    // create the new buffer
+    pBuffer = Abc_NtkCreateNode( pNode->pNtk );
+    Abc_ObjAddFanin( pBuffer, pNode );
+    Abc_ObjSetFaninL( pBuffer, 0, 1 );
+    // add the initial state
+    assert( Vec_IntSize(vInits) == 2 * (int)pBuffer->Id );
+    Vec_IntPush( vInits, InitNew );
+    Vec_IntPush( vInits, 0       );
+    // redirect the fanouts
+    Vec_PtrForEachEntry( vNodes, pFanout, i )
+        Abc_ObjPatchFanin( pFanout, pNode, pBuffer );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abcs/abcUtils.c b/src/base/abcs/abcUtils.c
index 8dccb81d..a9f3254c 100644
--- a/src/base/abcs/abcUtils.c
+++ b/src/base/abcs/abcUtils.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
+#include "abcs.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -30,166 +30,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the latch number of the fanout.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_ObjFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout )
-{
-    assert( Abc_NtkIsSeq(pObj->pNtk) );
-    if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
-        return Abc_ObjFaninL0(pFanout);
-    else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
-        return Abc_ObjFaninL1(pFanout);
-    else 
-        assert( 0 );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the latch number of the fanout.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats )  
-{ 
-    assert( Abc_NtkIsSeq(pObj->pNtk) );
-    if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
-        Abc_ObjSetFaninL0(pFanout, nLats);
-    else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
-        Abc_ObjSetFaninL1(pFanout, nLats);
-    else 
-        assert( 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds to the latch number of the fanout.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_ObjAddFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats )  
-{ 
-    assert( Abc_NtkIsSeq(pObj->pNtk) );
-    if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
-        Abc_ObjAddFaninL0(pFanout, nLats);
-    else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
-        Abc_ObjAddFaninL1(pFanout, nLats);
-    else 
-        assert( 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the latch number of the fanout.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_ObjFanoutLMax( Abc_Obj_t * pObj )
-{
-    Abc_Obj_t * pFanout;
-    int i, nLatchCur, nLatchRes;
-    nLatchRes = 0;
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-    {
-        nLatchCur = Abc_ObjFanoutL(pObj, pFanout);
-        if ( nLatchRes < nLatchCur )
-            nLatchRes = nLatchCur;
-    }
-    assert( nLatchRes >= 0 );
-    return nLatchRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the latch number of the fanout.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_ObjFanoutLMin( Abc_Obj_t * pObj )
-{
-    Abc_Obj_t * pFanout;
-    int i, nLatchCur, nLatchRes;
-    nLatchRes = ABC_INFINITY;
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-    {
-        nLatchCur = Abc_ObjFanoutL(pObj, pFanout);
-        if ( nLatchRes > nLatchCur )
-            nLatchRes = nLatchCur;
-    }
-    assert( nLatchRes < ABC_INFINITY );
-    return nLatchRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the sum of latches on the fanout edges.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_ObjFanoutLSum( Abc_Obj_t * pObj )
-{
-    Abc_Obj_t * pFanout;
-    int i, nSum = 0;
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        nSum += Abc_ObjFanoutL(pObj, pFanout);
-    return nSum;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the sum of latches on the fanin edges.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_ObjFaninLSum( Abc_Obj_t * pObj )
-{
-    Abc_Obj_t * pFanin;
-    int i, nSum = 0;
-    Abc_ObjForEachFanin( pObj, pFanin, i )
-        nSum += Abc_ObjFaninL(pObj, i);
-    return nSum;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counters the number of latches in the sequential AIG.]
+  Synopsis    [Counts the number of latches in the sequential AIG.]
 
   Description []
                
@@ -213,7 +54,7 @@ int Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Counters the number of latches in the sequential AIG.]
+  Synopsis    [Counts the number of latches in the sequential AIG.]
 
   Description []
                
diff --git a/src/base/abcs/abcs.h b/src/base/abcs/abcs.h
new file mode 100644
index 00000000..bfa95f3e
--- /dev/null
+++ b/src/base/abcs/abcs.h
@@ -0,0 +1,315 @@
+/**CFile****************************************************************
+
+  FileName    [abcs.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential synthesis package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __ABCS_H__
+#define __ABCS_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+// the maximum number of latches on the edge
+#define ABC_MAX_EDGE_LATCH   16   
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// representation of latch on the edge
+typedef struct Abc_RetEdge_t_       Abc_RetEdge_t;   
+struct Abc_RetEdge_t_ // 1 word
+{
+    unsigned         iNode    : 24;  // the ID of the node
+    unsigned         iEdge    :  1;  // the edge of the node
+    unsigned         iLatch   :  7;  // the latch number counting from the node
+};
+
+// representation of one retiming step
+typedef struct Abc_RetStep_t_       Abc_RetStep_t;   
+struct Abc_RetStep_t_ // 1 word
+{
+    unsigned         iNode    : 24;  // the ID of the node
+    unsigned         nLatches :  8;  // the number of latches to retime
+};
+
+static inline int            Abc_RetEdge2Int( Abc_RetEdge_t Str )  { return *((int *)&Str);           }
+static inline Abc_RetEdge_t  Abc_Int2RetEdge( int Num )            { return *((Abc_RetEdge_t *)&Num); }
+
+static inline int            Abc_RetStep2Int( Abc_RetStep_t Str )  { return *((int *)&Str);           }
+static inline Abc_RetStep_t  Abc_Int2RetStep( int Num )            { return *((Abc_RetStep_t *)&Num); }
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+// getting the number of the edge for this fanout
+static inline int Abc_ObjEdgeNum( Abc_Obj_t * pObj, Abc_Obj_t * pFanout )  
+{
+    assert( Abc_NtkIsSeq(pObj->pNtk) );
+    if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
+        return 0;
+    else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
+        return 1;
+    assert( 0 );
+    return -1;
+}
+
+// getting the latch number of the fanout
+static inline int Abc_ObjFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout )
+{
+    return Abc_ObjFaninL( pFanout, Abc_ObjEdgeNum(pObj,pFanout) );
+}
+
+// setting the latch number of the fanout
+static inline void Abc_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats )  
+{ 
+    Abc_ObjSetFaninL( pFanout, Abc_ObjEdgeNum(pObj,pFanout), nLats );
+}
+
+// adding to the latch number of the fanout
+static inline void Abc_ObjAddFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats )  
+{ 
+    Abc_ObjAddFaninL( pFanout, Abc_ObjEdgeNum(pObj,pFanout), nLats );
+}
+
+// returns the latch number of the fanout
+static inline int Abc_ObjFanoutLMax( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanout;
+    int i, nLatchCur, nLatchRes;
+    nLatchRes = 0;
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        nLatchCur = Abc_ObjFanoutL(pObj, pFanout);
+        if ( nLatchRes < nLatchCur )
+            nLatchRes = nLatchCur;
+    }
+    assert( nLatchRes >= 0 );
+    return nLatchRes;
+}
+
+// returns the latch number of the fanout
+static inline int Abc_ObjFanoutLMin( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanout;
+    int i, nLatchCur, nLatchRes;
+    nLatchRes = ABC_INFINITY;
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        nLatchCur = Abc_ObjFanoutL(pObj, pFanout);
+        if ( nLatchRes > nLatchCur )
+            nLatchRes = nLatchCur;
+    }
+    assert( nLatchRes < ABC_INFINITY );
+    return nLatchRes;
+}
+
+// returns the sum of latches on the fanout edges
+static inline int Abc_ObjFanoutLSum( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanout;
+    int i, nSum = 0;
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        nSum += Abc_ObjFanoutL(pObj, pFanout);
+    return nSum;
+}
+
+// returns the sum of latches on the fanin edges
+static inline int Abc_ObjFaninLSum( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i, nSum = 0;
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        nSum += Abc_ObjFaninL(pObj, i);
+    return nSum;
+}
+
+
+// getting the bit-string of init values of the edge
+static inline unsigned Abc_ObjFaninLGetInit( Abc_Obj_t * pObj, int Edge )  
+{ 
+    return (unsigned)Vec_IntEntry( pObj->pNtk->vInits, 2 * pObj->Id + Edge );
+}
+
+// setting bit-string of init values of the edge
+static inline void Abc_ObjFaninLSetInit( Abc_Obj_t * pObj, int Edge, unsigned Init )  
+{ 
+    Vec_IntWriteEntry( pObj->pNtk->vInits, 2 * pObj->Id + Edge, Init );
+}
+
+// setting the init value of the given latch on the edge
+static inline void Abc_ObjFaninLSetInitOne( Abc_Obj_t * pObj, int Edge, int iLatch, Abc_InitType_t Init )  
+{
+    unsigned EntryCur = Abc_ObjFaninLGetInit(pObj, Edge);
+    unsigned EntryNew = (EntryCur & ~(0x3 << iLatch)) | (Init << iLatch);
+    assert( iLatch < Abc_ObjFaninL(pObj, Edge) );
+    Abc_ObjFaninLSetInit( pObj, Edge, EntryNew );
+}
+
+// geting the init value of the first latch on the edge
+static inline Abc_InitType_t Abc_ObjFaninLGetInitFirst( Abc_Obj_t * pObj, int Edge )  
+{
+    return 0x3 & Abc_ObjFaninLGetInit( pObj, Edge );
+}
+
+// geting the init value of the last latch on the edge
+static inline Abc_InitType_t Abc_ObjFaninLGetInitLast( Abc_Obj_t * pObj, int Edge )  
+{
+    assert( Abc_ObjFaninL(pObj, Edge) > 0 );
+    return 0x3 & (Abc_ObjFaninLGetInit(pObj, Edge) >> (2 * (Abc_ObjFaninL(pObj, Edge) - 1)));
+}
+
+// insert the first latch on the edge
+static inline void Abc_ObjFaninLInsertFirst( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )  
+{ 
+    unsigned EntryCur = Abc_ObjFaninLGetInit(pObj, Edge);
+    unsigned EntryNew = ((EntryCur << 2) | Init);
+    assert( Init >= 0 && Init < 4 );
+    assert( Abc_ObjFaninL(pObj, Edge) < ABC_MAX_EDGE_LATCH );
+    Abc_ObjFaninLSetInit( pObj, Edge, EntryNew );
+    Abc_ObjAddFaninL( pObj, Edge, 1 );
+}
+
+// insert the last latch on the edge
+static inline void Abc_ObjFaninLInsertLast( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )  
+{ 
+    unsigned EntryCur = Abc_ObjFaninLGetInit(pObj, Edge);
+    unsigned EntryNew = EntryCur | (Init << (2 * Abc_ObjFaninL(pObj, Edge)));
+    assert( Init >= 0 && Init < 4 );
+    assert( Abc_ObjFaninL(pObj, Edge) < ABC_MAX_EDGE_LATCH );
+    Abc_ObjFaninLSetInit( pObj, Edge, EntryNew );
+    Abc_ObjAddFaninL( pObj, Edge, 1 );
+}
+
+// delete the first latch on the edge
+static inline Abc_InitType_t Abc_ObjFaninLDeleteFirst( Abc_Obj_t * pObj, int Edge )  
+{ 
+    unsigned EntryCur = Abc_ObjFaninLGetInit(pObj, Edge);
+    Abc_InitType_t Init = 0x3 & EntryCur;
+    unsigned EntryNew = EntryCur >> 2;
+    assert( Abc_ObjFaninL(pObj, Edge) > 0 );
+    Abc_ObjFaninLSetInit( pObj, Edge, EntryNew );
+    Abc_ObjAddFaninL( pObj, Edge, -1 );
+    return Init;
+}
+
+// delete the last latch on the edge
+static inline Abc_InitType_t Abc_ObjFaninLDeleteLast( Abc_Obj_t * pObj, int Edge )  
+{ 
+    unsigned EntryCur = Abc_ObjFaninLGetInit(pObj, Edge);
+    Abc_InitType_t Init = 0x3 & (EntryCur >> (2 * (Abc_ObjFaninL(pObj, Edge) - 1)));
+    unsigned EntryNew = EntryCur & ~(((unsigned)0x3) << (2 * (Abc_ObjFaninL(pObj, Edge)-1)));
+    assert( Abc_ObjFaninL(pObj, Edge) > 0 );
+    Abc_ObjFaninLSetInit( pObj, Edge, EntryNew );
+    Abc_ObjAddFaninL( pObj, Edge, -1 );
+    return Init;
+}
+
+// retime node forward without initial states
+static inline void Abc_ObjRetimeForwardTry( Abc_Obj_t * pObj, int nLatches )  
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    // make sure it is an AND gate
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    // make sure it has enough latches
+    assert( Abc_ObjFaninL0(pObj) >= nLatches );
+    assert( Abc_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
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        Abc_ObjAddFanoutL( pObj, pFanout, nLatches );
+}
+
+// retime node backward without initial states
+static inline void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches )  
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    // make sure it is an AND gate
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    // subtract these latches on the fanout side
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        assert( Abc_ObjFanoutL(pObj, pFanout) >= nLatches );
+        Abc_ObjAddFanoutL( pObj, pFanout, -nLatches );
+    }
+    // add these latches on the fanin size
+    Abc_ObjAddFaninL0( pObj, nLatches );
+    Abc_ObjAddFaninL1( pObj, nLatches );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                        ITERATORS                                 ///
+////////////////////////////////////////////////////////////////////////
+
+// iterating through the initial values of the edge
+#define Abc_ObjFaninLForEachValue( pObj, Edge, Init, i, Value ) \
+    for ( i = 0, Init = Abc_ObjFaninLGetInit(pObj, Edge); \
+          i < Abc_ObjFaninL(pObj, Edge) && ((Value = ((Init >> i) & 3)), 1); i++ ) 
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== abcRetCore.c ===========================================================*/
+extern void               Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkSeqRetimeInitial( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk );
+/*=== abcRetDelay.c ==========================================================*/
+extern Vec_Str_t *        Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk );
+/*=== abcRetImpl.c ===========================================================*/
+extern int                Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags );
+extern void               Abc_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves );
+extern int                Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves );
+/*=== abcRetUtil.c ===========================================================*/
+extern Vec_Ptr_t *        Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward );
+extern Vec_Ptr_t *        Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vNodes, bool fForward );
+extern Vec_Int_t *        Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward );
+/*=== abcSeq.c ===============================================================*/
+extern Abc_Ntk_t *        Abc_NtkAigToSeq( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *        Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk );
+/*=== abcShare.c =============================================================*/
+extern void               Abc_NtkSeqShareFanouts( Abc_Ntk_t * pNtk );
+/*=== abcUtil.c ==============================================================*/
+extern int                Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk );
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 393b2216..988cabfb 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -114,7 +114,10 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
             // get the node name and the node type
             pType = vTokens->pArray[1];
             if ( strcmp(pType, "DFF") == 0 )
-                Io_ReadCreateLatch( pNtk, vTokens->pArray[2], vTokens->pArray[0] );
+            {
+                pNode = Io_ReadCreateLatch( pNtk, vTokens->pArray[2], vTokens->pArray[0] );
+                Abc_LatchSetInit0( pNode );
+            }
             else
             {
                 // create a new node and add it to the network
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 7adec714..1cae68e7 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -395,7 +395,6 @@ int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
     Abc_Ntk_t * pNtk = p->pNtk;
     Abc_Obj_t * pLatch;
     int ResetValue;
-
     if ( vTokens->nSize < 3 )
     {
         p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
@@ -407,7 +406,7 @@ int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
     pLatch = Io_ReadCreateLatch( pNtk, vTokens->pArray[1], vTokens->pArray[2] );
     // get the latch reset value
     if ( vTokens->nSize == 3 )
-        ResetValue = 2;
+        Abc_LatchSetInitDc( pLatch );
     else
     {
         ResetValue = atoi(vTokens->pArray[3]);
@@ -418,8 +417,13 @@ int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
             Io_ReadBlifPrintErrorMessage( p );
             return 1;
         }
+        if ( ResetValue == 0 )
+            Abc_LatchSetInit0( pLatch );
+        else if ( ResetValue == 1 )
+            Abc_LatchSetInit1( pLatch );
+        else if ( ResetValue == 2 )
+            Abc_LatchSetInitDc( pLatch );
     }
-    Abc_ObjSetData( pLatch, (void *)ResetValue );
     return 0;
 }
 
diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c
index 48a1722b..d94b46c7 100644
--- a/src/base/io/ioReadEdif.c
+++ b/src/base/io/ioReadEdif.c
@@ -114,7 +114,10 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p )
             vTokens = Extra_FileReaderGetTokens(p);
             pGateName = vTokens->pArray[1];
             if ( strncmp( pGateName, "Flip", 4 ) == 0 )
+            {
                 pObj = Abc_NtkCreateLatch( pNtk );
+                Abc_LatchSetInit0( pObj );
+            }
             else
             {
                 pObj = Abc_NtkCreateNode( pNtk );
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 132684cc..e3e9c59a 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -82,7 +82,7 @@ Abc_Obj_t * Io_ReadCreatePo( Abc_Ntk_t * pNtk, char * pName )
 
   Synopsis    [Create a latch with the given input/output.]
 
-  Description []
+  Description [By default, the latch value is unknown (ABC_INIT_NONE).]
                
   SideEffects []
 
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 7d6815b9..84fedc34 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -300,7 +300,7 @@ void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch )
     fprintf( pFile, ".latch" );
     fprintf( pFile, " %10s",    Abc_ObjName(pNetLi) );
     fprintf( pFile, " %10s",    Abc_ObjName(pNetLo) );
-    fprintf( pFile, "  %d\n",   Reset );
+    fprintf( pFile, "  %d\n",   Reset-1 );
 }
 
 
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 4481297a..37822383 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -515,7 +515,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
 
     if ( mng->mode == 0 ) // brute-force SAT
     {
-        // transfor the AIG into a logic network for efficient CNF construction
+        // transform the AIG into a logic network for efficient CNF construction
         pCnf = Abc_NtkRenode( mng->pTarget, 0, 100, 1, 0, 0 );
         RetValue = Abc_NtkMiterSat( pCnf, mng->nSeconds, 0 );