Version abc50911

9 files changed, 690 insertions, 559 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 0e296d64..02b284e6 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -169,6 +169,8 @@ struct Abc_Ntk_t_
     Vec_Ptr_t *      vSupps;
     // the satisfiable assignment of the miter
     int *            pModel;
+    // initial states
+    Vec_Int_t *      vInits; 
     // the external don't-care if given
     Abc_Ntk_t *      pExdc;         // the EXDC network
     // miscellaneous data members
@@ -305,6 +307,7 @@ static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj )          { return Ab
 static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) );}
 static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );  }
 static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) );  }
+static inline Abc_Obj_t * Abc_ObjGetCopy( Abc_Obj_t * pObj )         { return Abc_ObjNotCond( Abc_ObjRegular(pObj)->pCopy, Abc_ObjIsComplement(pObj) );  }
 static inline Abc_Obj_t * Abc_ObjFanoutFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) {  assert( !Abc_NtkIsLogic(pObj->pNtk) ); return (Abc_ObjFaninId0(pFanout) == (int)pObj->Id)? Abc_ObjChild0(pFanout) : Abc_ObjChild1(pFanout);  }
 static inline void        Abc_ObjSetFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl = 1;                               }
 static inline void        Abc_ObjXorFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl ^= 1;                              }
@@ -319,6 +322,8 @@ extern void               Abc_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFano
 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;                         }
@@ -337,12 +342,13 @@ 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 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 int         Abc_LatchInit( Abc_Obj_t * pLatch )       { assert(Abc_ObjIsLatch(pLatch)); return (int)pLatch->pData;          }
 
 // outputs the runtime in seconds
 #define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
@@ -364,6 +370,12 @@ static inline bool        Abc_LatchIsInitDc( Abc_Obj_t * pLatch )   { assert(Abc
 #define Abc_NtkForEachLatch( pNtk, pObj, i )                             \
     for ( i = 0; i < Vec_PtrSize(pNtk->vLats); i++ )                     \
         if ( pObj = Abc_NtkLatch(pNtk, i) )
+#define Abc_AigForEachAnd( pNtk, pNode, i )                              \
+    for ( i = 0; i < Vec_PtrSize(pNtk->vObjs); i++ )                     \
+        if ( (pNode = Abc_NtkObj(pNtk, i)) && Abc_NodeIsAigAnd(pNode) )
+#define Abc_SeqForEachCutsetNode( pNtk, pNode, i )                       \
+    for ( i = 0; i < Vec_PtrSize(pNtk->vLats); i++ )                     \
+        if ( (pNode = Abc_NtkLatch(pNtk, i)) )
 // inputs and outputs
 #define Abc_NtkForEachPi( pNtk, pPi, i )                                 \
     for ( i = 0; (i < Abc_NtkPiNum(pNtk)) && (((pPi) = Abc_NtkPi(pNtk, i)), 1); i++ )
@@ -529,6 +541,7 @@ extern void               Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk );
 /*=== abcNtk.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
+extern Abc_Ntk_t *        Abc_NtkStartFromSeq( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern void               Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern void               Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk );
@@ -572,13 +585,20 @@ 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 );
-/*=== abcSeq.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkAigToSeq( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkSeqLatchNum( 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/abcCheck.c b/src/base/abc/abcCheck.c
index 356a4eba..b91a1291 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -160,9 +160,10 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
     }
 
     // check the latches
-    Abc_NtkForEachLatch( pNtk, pNode, i )
-        if ( !Abc_NtkCheckLatch( pNtk, pNode ) )
-            return 0;
+    if ( !Abc_NtkIsSeq(pNtk) )
+        Abc_NtkForEachLatch( pNtk, pNode, i )
+            if ( !Abc_NtkCheckLatch( pNtk, pNode ) )
+                return 0;
 
     // finally, check for combinational loops
 //  clk = clock();
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 53ba3568..eddfd8b8 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -186,8 +186,8 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )  
 { 
     Abc_Obj_t * pConst1;
-    assert( Abc_NtkIsStrash(pNtkAig) );
-    assert( Abc_NtkIsSopLogic(pNtkNew) );
+    assert( Abc_NtkHasAig(pNtkAig) );
+    assert( Abc_NtkIsLogic(pNtkNew) );
     pConst1 = Abc_AigConst1(pNtkAig->pManFunc);
     if ( Abc_ObjFanoutNum(pConst1) > 0 )
         pConst1->pCopy = Abc_NodeCreateConst1( pNtkNew );
@@ -208,8 +208,8 @@ Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )
 Abc_Obj_t * Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )  
 { 
     Abc_Obj_t * pReset, * pConst1;
-    assert( Abc_NtkIsStrash(pNtkAig) );
-    assert( Abc_NtkIsSopLogic(pNtkNew) );
+    assert( Abc_NtkHasAig(pNtkAig) );
+    assert( Abc_NtkIsLogic(pNtkNew) );
     pReset = Abc_AigReset(pNtkAig->pManFunc);
     if ( Abc_ObjFanoutNum(pReset) > 0 )
     {
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c4feb7a2..f2cfaaf1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3939,6 +3939,12 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( Abc_NtkCountSelfFeedLatches(pNtk) )
+    {
+        fprintf( pErr, "Works AIG has self-feeding latches. Cannot continue.\n" );
+        return 1;
+    }
+
     // get the new network
     pNtkRes = Abc_NtkAigToSeq( pNtk );
     if ( pNtkRes == NULL )
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 41b9288e..e4af8e12 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -50,7 +50,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     if ( !Abc_NtkIsSeq(pNtk) )
         fprintf( pFile, "  lat = %4d", Abc_NtkLatchNum(pNtk) );
     else
-        fprintf( pFile, "  lat = %4d", Abc_NtkSeqLatchNum(pNtk) );
+        fprintf( pFile, "  lat = %4d(%d)", Abc_NtkSeqLatchNum(pNtk), Abc_NtkSeqLatchNumShared(pNtk) );
 
     if ( Abc_NtkIsNetlist(pNtk) )
     {
diff --git a/src/base/abcs/abcForBack.c b/src/base/abcs/abcForBack.c
new file mode 100644
index 00000000..4db162e1
--- /dev/null
+++ b/src/base/abcs/abcForBack.c
@@ -0,0 +1,161 @@
+/**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
new file mode 100644
index 00000000..f33ed40e
--- /dev/null
+++ b/src/base/abcs/abcLogic.c
@@ -0,0 +1,140 @@
+/**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/abcSeq.c b/src/base/abcs/abcSeq.c
index 344417af..eca337fd 100644
--- a/src/base/abcs/abcSeq.c
+++ b/src/base/abcs/abcSeq.c
@@ -6,7 +6,7 @@
 
   PackageName [Network and node package.]
 
-  Synopsis    []
+  Synopsis    [Procedures to derive sequential AIG from combinational AIG with latches.]
 
   Author      [Alan Mishchenko]
   
@@ -21,27 +21,32 @@
 #include "abc.h"
 
 /*
-    A sequential network is an AIG whose edges have number-of-latches attributes, 
-    in addition to the complemented attibutes. 
-
-    The sets of PIs/POs remain the same as in logic network. 
-    Constant 1 node can only be used as a fanin of a PO node and the reset node.
-    The reset node produces sequence (01111...). It is used to create the
-    initialization logic of all latches.
-    The latches do not have explicit initial state but they are implicitly
-    reset by the reset node.
-
+    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.
+    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
+    latches over the static nodes of the AIG.
+    The new initial state after forward retiming is computed in a
+    straight-forward manner. After backward retiming it is computed
+    by setting up a SAT problem.
 */
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Vec_Int_t * Abc_NtkSeqCountLatches( Abc_Ntk_t * pNtk );
-static void        Abc_NodeSeqCountLatches( Abc_Obj_t * pObj, Vec_Int_t * vNumbers );
-
-static void        Abc_NtkSeqCreateLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-static void        Abc_NodeSeqCreateLatches( Abc_Obj_t * pObj, int nLatches );
+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 );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -51,7 +56,9 @@ static void        Abc_NodeSeqCreateLatches( Abc_Obj_t * pObj, int nLatches );
 
   Synopsis    [Converts a normal AIG into a sequential AIG.]
 
-  Description []
+  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.]
                
   SideEffects []
 
@@ -61,119 +68,62 @@ static void        Abc_NodeSeqCreateLatches( Abc_Obj_t * pObj, int nLatches );
 Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew;
-    Abc_Aig_t * pManNew;
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pObj, * pConst, * pFanout, * pFaninNew, * pLatch;
-    int i, k, fChange, Counter;
-
+    Abc_Obj_t * pObj, * pFanin0, * pFanin1;
+    int i, nLatches0, nLatches1, Init0, Init1;
+    // make sure it is an AIG without self-feeding latches
     assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
     // start the network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_SEQ, ABC_FUNC_AIG );
-    pManNew = pNtkNew->pManFunc;
-
-    // set mapping of the constant nodes
-    Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1( pManNew );
-    Abc_AigReset(pNtk->pManFunc)->pCopy  = Abc_AigReset( pManNew );
-
-    // get rid of initial states
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-    {
-        pObj->pNext = pObj->pCopy;
-        if ( Abc_LatchIsInit0(pObj) )
-            pObj->pCopy = Abc_AigAnd( pManNew, pObj->pCopy, Abc_AigReset(pManNew) );
-        else if ( Abc_LatchIsInit1(pObj) )
-            pObj->pCopy = Abc_AigOr( pManNew, pObj->pCopy, Abc_ObjNot( Abc_AigReset(pManNew) ) );
-    }
-
-    // copy internal nodes
-    vNodes = Abc_AigDfs( pNtk, 1, 0 );
+    pNtkNew = Abc_NtkAlloc( ABC_TYPE_SEQ, ABC_FUNC_AIG );
+    // duplicate the name and the spec
+    pNtkNew->pName = util_strsav(pNtk->pName);
+    pNtkNew->pSpec = util_strsav(pNtk->pSpec);
+    // clone const/PIs/POs
+    Abc_NtkDupObj(pNtkNew, Abc_AigConst1(pNtk->pManFunc) );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
+    // copy the PI/PO names
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pObj) );
+    Abc_NtkForEachPo( pNtk, pObj, i ) 
+        Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(pObj) );
+    // copy the internal nodes, including choices, excluding dangling
+    vNodes = Abc_AigDfs( pNtk, 0, 0 );
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        if ( Abc_ObjFaninNum(pObj) == 2 )
-            pObj->pCopy = Abc_AigAnd( pManNew, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+        Abc_NtkDupObj(pNtkNew, pObj);
     Vec_PtrFree( vNodes );
-
-    // relink the CO nodes
-    Abc_NtkForEachPo( pNtk, pObj, i )
-        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjChild0Copy(pObj) );
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-        Abc_ObjAddFanin( pObj->pNext, Abc_ObjChild0Copy(pObj) );
-
-    // propagate constant input latches in the new network
-    Counter = 0;
-    fChange = 1;
-    while ( fChange )
+    // start the storage for initial states
+    pNtkNew->vInits = Vec_IntStart( Abc_NtkObjNumMax(pNtkNew) );
+    // reconnect the internal nodes
+    Abc_AigForEachAnd( pNtk, pObj, i )
     {
-        fChange = 0;
-        Abc_NtkForEachLatch( pNtkNew, pLatch, i )
-        {
-            if ( Abc_ObjFanoutNum(pLatch) == 0 )
-                continue;
-            pFaninNew = Abc_ObjFanin0(pLatch);
-            if ( Abc_ObjIsCi(pFaninNew) || !Abc_NodeIsConst(pFaninNew) )
-                continue;
-            pConst = Abc_ObjNotCond( Abc_AigConst1(pManNew), Abc_ObjFaninC0(pLatch) );
-            Abc_AigReplace( pManNew, pLatch, pConst, 0 );
-            fChange = 1;
-            Counter++;
-        }
+        // 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 );
     }
-    if ( Counter )
-        fprintf( stdout, "Latch sweeping removed %d latches (out of %d).\n", Counter, Abc_NtkLatchNum(pNtk) );
-
-    // redirect fanouts of each latch to the latch fanins
-    vNodes = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachLatch( pNtkNew, pLatch, i )
+    // reconnect the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
     {
-//printf( "Latch %s. Fanouts = %d.\n", Abc_ObjName(pLatch), Abc_ObjFanoutNum(pLatch) );
-
-        Abc_NodeCollectFanouts( pLatch, vNodes );
-        Vec_PtrForEachEntry( vNodes, pFanout, k )
-        {
-            if ( Abc_ObjFaninId0(pFanout) == Abc_ObjFaninId1(pFanout))
-                printf( " ******* Identical fanins!!! ******* \n" );
-
-            if ( Abc_ObjFaninId0(pFanout) == (int)pLatch->Id )
-            {
-//                pFaninNew = Abc_ObjNotCond( Abc_ObjChild0(pLatch), Abc_ObjFaninC0(pFanout) );
-                pFaninNew = Abc_ObjChild0(pLatch);
-                Abc_ObjPatchFanin( pFanout, pLatch, pFaninNew );
-                Abc_ObjAddFaninL0( pFanout, 1 );
-            }
-            else if ( Abc_ObjFaninId1(pFanout) == (int)pLatch->Id )
-            {
-//                pFaninNew = Abc_ObjNotCond( Abc_ObjChild0(pLatch), Abc_ObjFaninC1(pFanout) );
-                pFaninNew = Abc_ObjChild0(pLatch);
-                Abc_ObjPatchFanin( pFanout, pLatch, pFaninNew );
-                Abc_ObjAddFaninL1( pFanout, 1 );
-            }
-            else
-                assert( 0 );
-        }
-        assert( Abc_ObjFanoutNum(pLatch) == 0 );
-        Abc_NtkDeleteObj( pLatch );
+        // 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 );
     }
-    Vec_PtrFree( vNodes );
-    // get rid of latches altogether 
-//    Abc_NtkForEachLatch( pNtkNew, pObj, i )
-//        Abc_NtkDeleteObj( pObj );
-    assert( pNtkNew->nLatches == 0 );
-    Vec_PtrClear( pNtkNew->vLats );
-    Vec_PtrShrink( pNtkNew->vCis, pNtk->nPis );
-    Vec_PtrShrink( pNtkNew->vCos, pNtk->nPos );
-
-/*
-/////////////////////////////////////////////
-Abc_NtkForEachNode( pNtkNew, pObj, i )
-    if ( !Abc_NodeIsConst(pObj) )
-        if ( Abc_ObjFaninL0(pObj) + Abc_ObjFaninL1(pObj) > 20 )
-            printf( "(%d,%d) ", Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) );
-Abc_NtkForEachCo( pNtkNew, pObj, i )
-    printf( "(%d) ", Abc_ObjFaninL0(pObj) );
-/////////////////////////////////////////////
-printf( "\n" );
-*/
-
-    if ( pNtk->pExdc )
+    // set the cutset composed of latch drivers
+    pNtkNew->vLats = Abc_NtkAigCutsetCopy( pNtk );
+    // copy EXDC and check correctness
+    if ( pNtkNew->pExdc )
         fprintf( stdout, "Warning: EXDC is dropped when converting to sequential AIG.\n" );
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkAigToSeq(): Network check has failed.\n" );
@@ -182,282 +132,36 @@ printf( "\n" );
 
 /**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, * pFanin, * pFaninNew;
-    int i, k, c;
-    assert( Abc_NtkIsSeq(pNtk) );
-    // start the network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
-    // create the constant and reset nodes
-    Abc_NtkDupConst1( pNtk, pNtkNew );
-    Abc_NtkDupReset( pNtk, pNtkNew );
-    // duplicate the nodes, create node functions and latches
-    Abc_NtkForEachNode( pNtk, pObj, i )
-    {
-        if ( Abc_NodeIsConst(pObj) )
-            continue;
-        Abc_NtkDupObj(pNtkNew, pObj);
-        pObj->pCopy->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
-    }
-    // create latches for the new nodes
-    Abc_NtkSeqCreateLatches( pNtk, pNtkNew );
-    // connect the objects
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-        {
-            // find the fanin
-            pFaninNew = pFanin->pCopy;
-            for ( c = 0; c < Abc_ObjFaninL(pObj, k); c++ )
-                pFaninNew = pFaninNew->pCopy;
-            Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
-        }
-    // set the complemented attributed of CO edges (to be fixed by making simple COs)
-    Abc_NtkForEachPo( pNtk, pObj, i )
-        if ( Abc_ObjFaninC0(pObj) )
-            Abc_ObjSetFaninC( pObj->pCopy, 0 );
-    // 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    [Finds max number of latches on the fanout edges of each node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Abc_NtkSeqCountLatches( Abc_Ntk_t * pNtk )
-{
-    Vec_Int_t * vNumbers;
-    Abc_Obj_t * pObj;
-    int i;
-    assert( Abc_NtkIsSeq( pNtk ) );
-    // start the array of counters
-    vNumbers = Vec_IntAlloc( 0 );
-    Vec_IntFill( vNumbers, Abc_NtkObjNumMax(pNtk), 0 );
-    // count for each edge
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        Abc_NodeSeqCountLatches( pObj, vNumbers );
-    return vNumbers;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Countes the latch numbers due to the fanins edges of the given node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeSeqCountLatches( Abc_Obj_t * pObj, Vec_Int_t * vNumbers )
-{
-    Abc_Obj_t * pFanin;
-    int k, nLatches;
-    // go through each fanin edge
-    Abc_ObjForEachFanin( pObj, pFanin, k )
-    {
-        nLatches = Abc_ObjFaninL( pObj, k );
-        if ( nLatches == 0 )
-            continue;
-        if ( Vec_IntEntry( vNumbers, pFanin->Id ) < nLatches )
-            Vec_IntWriteEntry( vNumbers, pFanin->Id, nLatches );
-    }
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Creates latches.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkSeqCreateLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
-{
-    Vec_Int_t * vNumbers;
-    Abc_Obj_t * pObj;
-    int i;
-    assert( Abc_NtkIsSeq( pNtk ) );
-    // create latches for each new object according to the counters
-    vNumbers = Abc_NtkSeqCountLatches( pNtk );
-    Abc_NtkForEachObj( pNtk, pObj, i )
-    {
-        if ( pObj->pCopy == NULL )
-            continue;
-        Abc_NodeSeqCreateLatches( pObj->pCopy, Vec_IntEntry(vNumbers, (int)pObj->Id) );
-    }
-    Vec_IntFree( vNumbers );
-    // add latch to the PI/PO lists, create latch names
-    Abc_NtkFinalizeLatches( pNtkNew );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the given number of latches for this object.]
+  Synopsis    [Collects the cut set nodes.]
 
-  Description [The latches are attached to the node and to each other
-  through the pCopy field.]
+  Description [These are internal AND gates that fanins into latches.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeSeqCreateLatches( Abc_Obj_t * pObj, int nLatches )
-{
-    Abc_Ntk_t * pNtk = pObj->pNtk;
-    Abc_Obj_t * pLatch, * pFanin;
-    int i;
-    pFanin = pObj;
-    for ( i = 0, pFanin = pObj; i < nLatches; pFanin = pLatch, i++ )
-    {
-        pLatch = Abc_NtkCreateLatch( pNtk );
-        Abc_LatchSetInitDc(pLatch);
-        Abc_ObjAddFanin( pLatch, pFanin );
-        pFanin->pCopy = pLatch;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counters the number of latches in the sequential AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk )
-{
-    Vec_Int_t * vNumbers;
-    Abc_Obj_t * pObj;
-    int i, Counter;
-    assert( Abc_NtkIsSeq( pNtk ) );
-    // create latches for each new object according to the counters
-    Counter = 0;
-    vNumbers = Abc_NtkSeqCountLatches( pNtk );
-    Abc_NtkForEachPi( pNtk, pObj, i )
-    {
-        assert( Abc_ObjFanoutLMax(pObj) == Vec_IntEntry(vNumbers, (int)pObj->Id) );
-        Counter += Vec_IntEntry(vNumbers, (int)pObj->Id);
-    }
-    Abc_NtkForEachNode( pNtk, pObj, i )
-    {
-        if ( Abc_NodeIsConst(pObj) )
-            continue;
-        assert( Abc_ObjFanoutLMax(pObj) == Vec_IntEntry(vNumbers, (int)pObj->Id) );
-        Counter += Vec_IntEntry(vNumbers, (int)pObj->Id);
-    }
-    Vec_IntFree( vNumbers );
-    if ( Abc_ObjFanoutNum( Abc_AigReset(pNtk->pManFunc) ) > 0 )
-        Counter++;
-    return Counter;
-}
-
-
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Performs forward retiming of the sequential AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Abc_NtkAigCutsetCopy( 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 )
+    Abc_Obj_t * pLatch, * pDriver;
+    int i;
+    vNodes = Vec_PtrAlloc( Abc_NtkLatchNum(pNtk) );
+    Abc_NtkIncrementTravId(pNtk);
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
-        pNode->fMarkA = 0;
-        if ( Abc_NodeIsConst(pNode) )
+        pDriver = Abc_ObjFanin0(pLatch);
+        if ( Abc_NodeIsTravIdCurrent(pDriver) || !Abc_NodeIsAigAnd(pDriver) )
             continue;
-        assert( Abc_ObjFaninLMin(pNode) == 0 );
+        Abc_NodeSetTravIdCurrent(pDriver);
+        Vec_PtrPush( vNodes, pDriver->pCopy );
     }
+    return vNodes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Performs forward retiming of the sequential AIG.]
+  Synopsis    [Determines the fanin that is transparent for latches.]
 
   Description []
                
@@ -466,172 +170,28 @@ void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk )
+Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, int * pnInit )
 {
-    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 )
+    Abc_Obj_t * pFanin;
+    int Init;
+    // get the given fanin of the node
+    pFanin = Abc_ObjFanin( pObj, Num );
+    if ( !Abc_ObjIsLatch(pFanin) )
     {
-        pNode->fMarkA = 0;
-        if ( Abc_NodeIsConst(pNode) )
-            continue;
-//        assert( Abc_ObjFanoutLMin(pNode) == 0 );
+        *pnLatches = *pnInit = 0;
+        return Abc_ObjChild( pObj, Num );
     }
-}
-
-
-
-
-/**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, nLatch, nLatchRes;
-    nLatchRes = 0;
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        if ( nLatchRes < (nLatch = Abc_ObjFanoutL(pObj, pFanout)) )
-            nLatchRes = nLatch;
-    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, nLatch, nLatchRes;
-    nLatchRes = ABC_INFINITY;
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        if ( nLatchRes > (nLatch = Abc_ObjFanoutL(pObj, pFanout)) )
-            nLatchRes = nLatch;
-    assert( nLatchRes < ABC_INFINITY );
-    return nLatchRes;
+    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;
+    // update the latch number and initial state
+    (*pnLatches)++;
+    (*pnInit) = ((*pnInit) << 2) | Init;
+    return Abc_ObjNotCond( pFanin, Abc_ObjFaninC(pObj,Num) );
 }
 
 
diff --git a/src/base/abcs/abcUtils.c b/src/base/abcs/abcUtils.c
new file mode 100644
index 00000000..8dccb81d
--- /dev/null
+++ b/src/base/abcs/abcUtils.c
@@ -0,0 +1,243 @@
+/**CFile****************************************************************
+
+  FileName    [abcUtils.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Utilities working sequential AIGs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcUtils.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, Counter;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    Counter = 0;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Counter += Abc_ObjFaninLSum( pObj );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Counter += Abc_ObjFaninLSum( pObj );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counters the number of latches in the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, Counter;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    Counter = 0;
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Counter += Abc_ObjFanoutLMax( pObj );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Counter += Abc_ObjFanoutLMax( pObj );
+    return Counter;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+