Version abc50912

10 files changed, 1387 insertions, 508 deletions

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
+