Version abc50813

10 files changed, 1518 insertions, 135 deletions

diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index a02764b1..97d8b56a 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -69,6 +69,9 @@ static int Abc_CommandSuperChoice  ( Abc_Frame_t * pAbc, int argc, char ** argv
 
 static int Abc_CommandFpga         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int Abc_CommandSeq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRetime       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 static int Abc_CommandCec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -130,6 +133,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
 
+    Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
+
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
 
@@ -170,21 +176,26 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     bool fShort;
     int c;
+    int fFactor;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set the defaults
-    fShort = 1;
+    fShort  = 1;
+    fFactor = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "sh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "sfh" ) ) != EOF )
     {
         switch ( c )
         {
         case 's':
             fShort ^= 1;
             break;
+        case 'f':
+            fFactor ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -197,12 +208,13 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( Abc_FrameReadErr(pAbc), "Empty network\n" );
         return 1;
     }
-    Abc_NtkPrintStats( pOut, pNtk );
+    Abc_NtkPrintStats( pOut, pNtk, fFactor );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_stats [-h]\n" );
+    fprintf( pErr, "usage: print_stats [-fh]\n" );
     fprintf( pErr, "\t        prints the network statistics and\n" );
+    fprintf( pErr, "\t-f    : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -2799,6 +2811,147 @@ usage:
 
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsAig(pNtk) )
+    {
+        fprintf( pErr, "Works only for AIG.\n" );
+        return 1;
+    }
+
+    // get the new network
+    pNtkRes = Abc_NtkAigToSeq( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Converting to sequential AIG has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: seq [-h]\n" );
+    fprintf( pErr, "\t        converts AIG into sequential AIG (while sweeping latches)\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fForward;
+    int fBackward;
+
+    extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fForward = 0;
+    fBackward = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "fbh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'f':
+            fForward ^= 1;
+            break;
+        case 'b':
+            fBackward ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Works only for sequential AIG.\n" );
+        return 1;
+    }
+
+    // get the new network
+    if ( fForward )
+        Abc_NtkSeqRetimeForward( pNtk );
+    else if ( fBackward )
+        Abc_NtkSeqRetimeBackward( pNtk );
+    else
+        Abc_NtkSeqRetimeDelay( pNtk );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: retime [-fbh]\n" );
+    fprintf( pErr, "\t        retimes sequential AIG (default is Pan's algorithm)\n" );
+    fprintf( pErr, "\t-f    : toggle forward retiming [default = %s]\n", fForward? "yes": "no" );
+    fprintf( pErr, "\t-b    : toggle backward retiming [default = %s]\n", fBackward? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 99af9ac6..438291d5 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -143,6 +143,7 @@ struct Abc_Ntk_t_
     Vec_Ptr_t *      vPtrTemp;      // the temporary array
     Vec_Int_t *      vIntTemp;      // the temporary array
     Vec_Str_t *      vStrTemp;      // the temporary array
+    void *           pData;         // the temporary pointer
     // the backup network and the step number
     Abc_Ntk_t *      pNetBackup;    // the pointer to the previous backup network
     int              iStep;         // the generation number for the given network
@@ -180,6 +181,11 @@ struct Abc_ManRes_t_
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
 
+// maximum/minimum operators
+#define ABC_MIN(a,b)      (((a) < (b))? (a) : (b))
+#define ABC_MAX(a,b)      (((a) > (b))? (a) : (b))
+#define ABC_INFINITY      (10000000)
+
 // reading data members of the network
 static inline char *      Abc_NtkName( Abc_Ntk_t * pNtk )         { return pNtk->pName;           }
 static inline char *      Abc_NtkSpec( Abc_Ntk_t * pNtk )         { return pNtk->pSpec;           }
@@ -247,31 +253,6 @@ static inline Abc_Obj_t * Abc_ObjRegular( Abc_Obj_t * p )         { return (Abc_
 static inline Abc_Obj_t * Abc_ObjNot( Abc_Obj_t * p )             { return (Abc_Obj_t *)((unsigned)(p) ^  01);  }
 static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c )  { return (Abc_Obj_t *)((unsigned)(p) ^ (c));  }
 
-// working with fanin/fanout edges
-static inline int         Abc_ObjFaninNum( Abc_Obj_t * pObj )     { return pObj->vFanins.nSize;      }
-static inline int         Abc_ObjFanoutNum( Abc_Obj_t * pObj )    { return pObj->vFanouts.nSize;     }
-static inline int         Abc_ObjFaninId( Abc_Obj_t * pObj, int i){ return pObj->vFanins.pArray[i].iFan; }
-static inline int         Abc_ObjFaninId0( Abc_Obj_t * pObj )     { return pObj->vFanins.pArray[0].iFan; }
-static inline int         Abc_ObjFaninId1( Abc_Obj_t * pObj )     { return pObj->vFanins.pArray[1].iFan; }
-static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i ){ return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ]; }
-static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj )      { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ]; }
-static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan  ]; }
-static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj )       { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan  ]; }
-static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj )       { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan  ]; }
-static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )    { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj;   }
-static inline bool        Abc_ObjFaninC( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].fCompl;                             }
-static inline bool        Abc_ObjFaninC0( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[0].fCompl;                             }
-static inline bool        Abc_ObjFaninC1( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[1].fCompl;                             }
-static inline int         Abc_ObjFaninL( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].nLats;                              }
-static inline int         Abc_ObjFaninL0( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[0].nLats;                              }
-static inline int         Abc_ObjFaninL1( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[1].nLats;                              }
-static inline Abc_Obj_t * Abc_ObjChild0( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );}
-static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin1(pObj), Abc_ObjFaninC1(pObj) );}
-static inline void        Abc_ObjSetFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl = 1;                             }
-static inline void        Abc_ObjXorFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl ^= 1;                            }
-static inline void        Abc_ObjSetFaninL( Abc_Obj_t * pObj, int i, int nLats )  { pObj->vFanins.pArray[i].nLats = nLats;             }
-static inline void        Abc_ObjAddFaninL( Abc_Obj_t * pObj, int i, int nLats )  { pObj->vFanins.pArray[i].nLats += nLats;            }
-
 // checking the object type
 static inline bool        Abc_ObjIsNode( Abc_Obj_t * pObj )       { return pObj->Type == ABC_OBJ_NODE;   }
 static inline bool        Abc_ObjIsNet( Abc_Obj_t * pObj )        { return pObj->Type == ABC_OBJ_NET;    }
@@ -283,6 +264,43 @@ static inline bool        Abc_ObjIsCi( Abc_Obj_t * pObj )         { return pObj-
 static inline bool        Abc_ObjIsCo( Abc_Obj_t * pObj )         { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
 static inline bool        Abc_ObjIsCio( Abc_Obj_t * pObj )        { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
 
+// working with fanin/fanout edges
+static inline int         Abc_ObjFaninNum( Abc_Obj_t * pObj )     { return pObj->vFanins.nSize;      }
+static inline int         Abc_ObjFanoutNum( Abc_Obj_t * pObj )    { return pObj->vFanouts.nSize;     }
+static inline int         Abc_ObjFaninId( Abc_Obj_t * pObj, int i){ return pObj->vFanins.pArray[i].iFan; }
+static inline int         Abc_ObjFaninId0( Abc_Obj_t * pObj )     { return pObj->vFanins.pArray[0].iFan; }
+static inline int         Abc_ObjFaninId1( Abc_Obj_t * pObj )     { return pObj->vFanins.pArray[1].iFan; }
+static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i ){ return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ];   }
+static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj )      { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ];   }
+static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan  ];   }
+static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj )       { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan  ];   }
+static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj )       { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan  ];   }
+static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )    { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj;     }
+static inline bool        Abc_ObjFaninC( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].fCompl;                               }
+static inline bool        Abc_ObjFaninC0( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[0].fCompl;                               }
+static inline bool        Abc_ObjFaninC1( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[1].fCompl;                               }
+static inline int         Abc_ObjFaninL( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].nLats;                                }
+static inline int         Abc_ObjFaninL0( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[0].nLats;                                }
+static inline int         Abc_ObjFaninL1( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[1].nLats;                                }
+static inline int         Abc_ObjFaninLMin( Abc_Obj_t * pObj )   {  assert( Abc_ObjIsNode(pObj) ); return ABC_MIN( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
+static inline int         Abc_ObjFaninLMax( Abc_Obj_t * pObj )   {  assert( Abc_ObjIsNode(pObj) ); return ABC_MAX( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
+static inline Abc_Obj_t * Abc_ObjChild( Abc_Obj_t * pObj, int i ) { return Abc_ObjNotCond( Abc_ObjFanin(pObj,i), Abc_ObjFaninC(pObj,i) );}
+static inline Abc_Obj_t * Abc_ObjChild0( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );  }
+static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin1(pObj), Abc_ObjFaninC1(pObj) );  }
+static inline void        Abc_ObjSetFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl = 1;                               }
+static inline void        Abc_ObjXorFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl ^= 1;                              }
+static inline void        Abc_ObjSetFaninL( Abc_Obj_t * pObj, int i, int nLats )  { pObj->vFanins.pArray[i].nLats = nLats;               }
+static inline void        Abc_ObjSetFaninL0( Abc_Obj_t * pObj, int nLats )        { pObj->vFanins.pArray[0].nLats = nLats;               }
+static inline void        Abc_ObjSetFaninL1( Abc_Obj_t * pObj, int nLats )        { pObj->vFanins.pArray[1].nLats = nLats;               }
+static inline void        Abc_ObjAddFaninL( Abc_Obj_t * pObj, int i, int nLats )  { pObj->vFanins.pArray[i].nLats += nLats;              }
+static inline void        Abc_ObjAddFaninL0( Abc_Obj_t * pObj, int nLats )        { pObj->vFanins.pArray[0].nLats += nLats;              }
+static inline void        Abc_ObjAddFaninL1( Abc_Obj_t * pObj, int nLats )        { pObj->vFanins.pArray[1].nLats += nLats;              }
+extern int                Abc_ObjFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout );
+extern void               Abc_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats );
+extern void               Abc_ObjAddFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats );  
+extern int                Abc_ObjFanoutLMin( Abc_Obj_t * pObj );
+extern int                Abc_ObjFanoutLMax( Abc_Obj_t * pObj );
+
 // checking the node type
 static inline bool        Abc_NodeIsAigAnd( Abc_Obj_t * pNode )   { assert(Abc_NtkIsAig(pNode->pNtk));            return Abc_ObjFaninNum(pNode) == 2;                         }
 static inline bool        Abc_NodeIsAigChoice( Abc_Obj_t * pNode ){ assert(Abc_NtkIsAig(pNode->pNtk));            return pNode->pData != NULL && Abc_ObjFanoutNum(pNode) > 0; }
@@ -299,11 +317,6 @@ static inline void        Abc_NodeSetTravIdPrevious( Abc_Obj_t * pNode )     { p
 static inline bool        Abc_NodeIsTravIdCurrent( Abc_Obj_t * pNode )       { return (bool)(pNode->TravId == pNode->pNtk->nTravIds);     }
 static inline bool        Abc_NodeIsTravIdPrevious( Abc_Obj_t * pNode )      { return (bool)(pNode->TravId == pNode->pNtk->nTravIds - 1); }
 
-// maximum/minimum operators
-#define ABC_MIN(a,b)      (((a) < (b))? (a) : (b))
-#define ABC_MAX(a,b)      (((a) > (b))? (a) : (b))
-#define ABC_INFINITY      (10000000)
-
 // outputs the runtime in seconds
 #define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
 
@@ -356,13 +369,18 @@ static inline bool        Abc_NodeIsTravIdPrevious( Abc_Obj_t * pNode )      { r
 ////////////////////////////////////////////////////////////////////////
 
 /*=== abcAig.c ==========================================================*/
-extern Abc_Aig_t *        Abc_AigAlloc( Abc_Ntk_t * pNtk );
+extern Abc_Aig_t *        Abc_AigAlloc( Abc_Ntk_t * pNtk, bool fSeq );
+extern Abc_Aig_t *        Abc_AigDup( Abc_Aig_t * pMan, bool fSeq );
 extern void               Abc_AigFree( Abc_Aig_t * pMan );
+extern int                Abc_AigCleanup( Abc_Aig_t * pMan );
+extern bool               Abc_AigCheck( Abc_Aig_t * pMan );
 extern Abc_Obj_t *        Abc_AigConst1( Abc_Aig_t * pMan );
+extern Abc_Obj_t *        Abc_AigReset( Abc_Aig_t * pMan );
 extern Abc_Obj_t *        Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
 extern Abc_Obj_t *        Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
 extern Abc_Obj_t *        Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
 extern Abc_Obj_t *        Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs );
+extern void               Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew );
 extern bool               Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
 extern bool               Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
 /*=== abcAttach.c ==========================================================*/
@@ -378,6 +396,7 @@ extern void               Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNt
 extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type );
 extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type );
 extern void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+extern void               Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkStartRead( char * pName );
 extern void               Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
@@ -385,6 +404,8 @@ extern Abc_Ntk_t *        Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNod
 extern void               Abc_NtkDelete( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
+extern Abc_Obj_t *        Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew );
+extern Abc_Obj_t *        Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew );
 extern void               Abc_NtkDeleteObj( Abc_Obj_t * pObj );
 extern Abc_Obj_t *        Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
@@ -462,7 +483,7 @@ extern Abc_Ntk_t *        Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk );
 /*=== abcPrint.c ==========================================================*/
-extern void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk );
+extern void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored );
 extern void               Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
@@ -481,6 +502,13 @@ extern void               Abc_NtkManResStop( Abc_ManRes_t * p );
 /*=== abcSat.c ==========================================================*/
 extern bool               Abc_NtkMiterSat( Abc_Ntk_t * pNtk, 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 );
+extern void               Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk );
 /*=== abcSop.c ==========================================================*/
 extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
 extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 590bc4d2..67f19ba7 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -20,6 +20,23 @@
 
 #include "abc.h"
 
+/*
+    AIG is an And-Inv Graph with structural hashing.
+    It is always structurally hashed. It means that at any time:
+    - the constants are propagated
+    - there is no single-input nodes (inverters/buffers)
+    - for each AND gate, there are no other AND gates with the same children.
+    The operations that are performed on AIG:
+    - building new nodes (Abc_AigAnd)
+    - elementary Boolean operations (Abc_AigOr, Abc_AigXor, etc)
+    - propagation of constants (Abc_AigReplace)
+    - variable substitution (Abc_AigReplace)
+
+    When AIG is duplicated, the new graph is struturally hashed too.
+    If this repeated hashing leads to fewer nodes, it means the original
+    AIG was not strictly hashed (using the three criteria above).
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -27,12 +44,16 @@
 // the simple AIG manager
 struct Abc_Aig_t_
 {
-    Abc_Ntk_t *       pAig;          // the AIG network
-    Abc_Obj_t *       pConst1;       // the constant 1 node
-    Abc_Obj_t **      pBins;         // the table bins
-    int               nBins;         // the size of the table
-    int               nEntries;      // the total number of entries in the table
-    Vec_Ptr_t *       vNodes;        // the temporary array of nodes
+    Abc_Ntk_t *       pNtkAig;           // the AIG network
+    Abc_Obj_t *       pConst1;           // the constant 1 node
+    Abc_Obj_t *       pReset;            // the sequential reset node
+    Abc_Obj_t **      pBins;             // the table bins
+    int               nBins;             // the size of the table
+    int               nEntries;          // the total number of entries in the table
+    Vec_Ptr_t *       vNodes;            // the temporary array of nodes
+    Vec_Ptr_t *       vStackDelete;      // the nodes to be deleted
+    Vec_Ptr_t *       vStackReplaceOld;  // the nodes to be replaced
+    Vec_Ptr_t *       vStackReplaceNew;  // the nodes to be used for replacement
 };
 
 // iterators through the entries in the linked lists of nodes
@@ -51,8 +72,15 @@ struct Abc_Aig_t_
 static inline unsigned Abc_HashKey2( Abc_Obj_t * p0, Abc_Obj_t * p1, int TableSize ) { return ((unsigned)(p0) + (unsigned)(p1) * 12582917) % TableSize; }
 //static inline unsigned Abc_HashKey2( Abc_Obj_t * p0, Abc_Obj_t * p1, int TableSize ) { return ((unsigned)((a)->Id + (b)->Id) * ((a)->Id + (b)->Id + 1) / 2) % TableSize; }
 
-// static hash table procedures
-static void Abc_AigResize( Abc_Aig_t * pMan );
+// structural hash table procedures
+static Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
+static Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, Abc_Obj_t * pAnd );
+static Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
+static void        Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis );
+static void        Abc_AigResize( Abc_Aig_t * pMan );
+// incremental AIG procedures
+static void        Abc_AigReplace_int( Abc_Aig_t * pMan );
+static void        Abc_AigDelete_int( Abc_Aig_t * pMan );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -69,7 +97,7 @@ static void Abc_AigResize( Abc_Aig_t * pMan );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
+Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig, bool fSeq )
 {
     Abc_Aig_t * pMan;
     // start the manager
@@ -80,14 +108,38 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
     pMan->pBins    = ALLOC( Abc_Obj_t *, pMan->nBins );
     memset( pMan->pBins, 0, sizeof(Abc_Obj_t *) * pMan->nBins );
     pMan->vNodes   = Vec_PtrAlloc( 100 );
+    pMan->vStackDelete     = Vec_PtrAlloc( 100 );
+    pMan->vStackReplaceOld = Vec_PtrAlloc( 100 );
+    pMan->vStackReplaceNew = Vec_PtrAlloc( 100 );
     // save the current network
-    pMan->pAig     = pNtkAig;
-    pMan->pConst1  = Abc_NtkCreateNode( pNtkAig );    
+    pMan->pNtkAig = pNtkAig;
+    pMan->pConst1 = Abc_NtkCreateNode( pNtkAig );    
+    pMan->pReset  = fSeq? Abc_NtkCreateNode( pNtkAig ) : NULL;    
     return pMan;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicated the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, bool fSeq )
+{
+    Abc_Aig_t * pManNew;
+    pManNew = Abc_AigAlloc( pMan->pNtkAig, fSeq );
+
+
+    return pManNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Deallocates the local AIG manager.]
 
   Description []
@@ -99,7 +151,13 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
 ***********************************************************************/
 void Abc_AigFree( Abc_Aig_t * pMan )
 {
+    assert( Vec_PtrSize( pMan->vStackDelete )     == 0 );
+    assert( Vec_PtrSize( pMan->vStackReplaceOld ) == 0 );
+    assert( Vec_PtrSize( pMan->vStackReplaceNew ) == 0 );
     // free the table
+    Vec_PtrFree( pMan->vStackDelete );
+    Vec_PtrFree( pMan->vStackReplaceOld );
+    Vec_PtrFree( pMan->vStackReplaceNew );
     Vec_PtrFree( pMan->vNodes );
     free( pMan->pBins );
     free( pMan );
@@ -107,6 +165,90 @@ void Abc_AigFree( Abc_Aig_t * pMan )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_AigCleanup( Abc_Aig_t * pMan )
+{
+    Abc_Obj_t * pAnd;
+    int i, Counter;
+    // collect the AND nodes that do not fanout
+    assert( Vec_PtrSize( pMan->vStackDelete ) == 0 );
+    for ( i = 0; i < pMan->nBins; i++ )
+        Abc_AigBinForEachEntry( pMan->pBins[i], pAnd )
+            if ( Abc_ObjFanoutNum(pAnd) == 0 )
+                Vec_PtrPush( pMan->vStackDelete, pAnd );
+    // process the dangling nodes and their MFFCs
+    for ( Counter = 0; Vec_PtrSize(pMan->vStackDelete) > 0; Counter++ )
+        Abc_AigDelete_int( pMan );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Makes sure that every node in the table is in the network and vice versa.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_AigCheck( Abc_Aig_t * pMan )
+{
+    Abc_Obj_t * pObj, * pAnd;
+    int i, nFanins, Counter;
+    Abc_NtkForEachNode( pMan->pNtkAig, pObj, i )
+    {
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+        {
+            if ( pObj != pMan->pConst1 && pObj != pMan->pReset )
+            {
+                printf( "Abc_AigCheck: The AIG has non-standard constant nodes.\n" );
+                return 0;
+            }
+            continue;
+        }
+        if ( nFanins == 1 )
+        {
+            printf( "Abc_AigCheck: The AIG has single input nodes.\n" );
+            return 0;
+        }
+        if ( nFanins > 2 )
+        {
+            printf( "Abc_AigCheck: The AIG has non-standard nodes.\n" );
+            return 0;
+        }
+        pAnd = Abc_AigAndLookup( pMan, Abc_ObjChild0(pObj), Abc_ObjChild1(pObj) );
+        if ( pAnd != pObj )
+        {
+            printf( "Abc_AigCheck: Node \"%s\" is not in the structural hashing table.\n", Abc_ObjName(pObj) );
+            return 0;
+        }
+    }
+    // count the number of nodes in the table
+    Counter = 0;
+    for ( i = 0; i < pMan->nBins; i++ )
+        Abc_AigBinForEachEntry( pMan->pBins[i], pAnd )
+            Counter++;
+    if ( Counter + 1 + Abc_NtkIsSeq(pMan->pNtkAig) != Abc_NtkNodeNum(pMan->pNtkAig) )
+    {
+        printf( "Abc_AigCheck: The number of nodes in the structural hashing table is wrong.\n", Counter );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Read the constant 1 node.]
 
   Description []
@@ -123,6 +265,24 @@ Abc_Obj_t * Abc_AigConst1( Abc_Aig_t * pMan )
 
 /**Function*************************************************************
 
+  Synopsis    [Read the reset node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_AigReset( Abc_Aig_t * pMan )  
+{ 
+    return pMan->pReset; 
+} 
+
+
+
+/**Function*************************************************************
+
   Synopsis    [Performs canonicization step.]
 
   Description [The argument nodes can be complemented.]
@@ -132,7 +292,71 @@ Abc_Obj_t * Abc_AigConst1( Abc_Aig_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
+Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
+{
+    Abc_Obj_t * pAnd;
+    unsigned Key;
+    // check if it is a good time for table resizing
+    if ( pMan->nEntries > 2 * pMan->nBins )
+        Abc_AigResize( pMan );
+    // order the arguments
+    if ( Abc_ObjRegular(p0)->Id > Abc_ObjRegular(p1)->Id )
+        pAnd = p0, p0 = p1, p1 = pAnd;
+    // create the new node
+    pAnd = Abc_NtkCreateNode( pMan->pNtkAig );
+    Abc_ObjAddFanin( pAnd, p0 );
+    Abc_ObjAddFanin( pAnd, p1 );
+    // set the level of the new node
+    pAnd->Level      = 1 + ABC_MAX( Abc_ObjRegular(p0)->Level, Abc_ObjRegular(p1)->Level ); 
+    // add the node to the corresponding linked list in the table
+    Key = Abc_HashKey2( p0, p1, pMan->nBins );
+    pAnd->pNext      = pMan->pBins[Key];
+    pMan->pBins[Key] = pAnd;
+    pMan->nEntries++;
+    return pAnd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description [The argument nodes can be complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, Abc_Obj_t * pAnd )
+{
+    unsigned Key;
+    // order the arguments
+    if ( Abc_ObjRegular(p0)->Id > Abc_ObjRegular(p1)->Id )
+        pAnd = p0, p0 = p1, p1 = pAnd;
+    // create the new node
+    Abc_ObjAddFanin( pAnd, p0 );
+    Abc_ObjAddFanin( pAnd, p1 );
+    // set the level of the new node
+    pAnd->Level      = 1 + ABC_MAX( Abc_ObjRegular(p0)->Level, Abc_ObjRegular(p1)->Level ); 
+    // add the node to the corresponding linked list in the table
+    Key = Abc_HashKey2( p0, p1, pMan->nBins );
+    pAnd->pNext      = pMan->pBins[Key];
+    pMan->pBins[Key] = pAnd;
+    return pAnd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description [The argument nodes can be complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
 {
     Abc_Obj_t * pAnd;
     unsigned Key;
@@ -165,23 +389,106 @@ Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
              Abc_ObjFaninC0(pAnd) == Abc_ObjIsComplement(p0) && 
              Abc_ObjFaninC1(pAnd) == Abc_ObjIsComplement(p1) )
              return pAnd;
-    // check if it is a good time for table resizing
-    if ( pMan->nEntries > 2 * pMan->nBins )
-    {
-        Abc_AigResize( pMan );
-        Key = Abc_HashKey2( p0, p1, pMan->nBins );
-    }
-    // create the new node
-    pAnd = Abc_NtkCreateNode( pMan->pAig );
-    Abc_ObjAddFanin( pAnd, p0 );
-    Abc_ObjAddFanin( pAnd, p1 );
-    // set the level of the new node
-    pAnd->Level      = 1 + ABC_MAX( Abc_ObjRegular(p0)->Level, Abc_ObjRegular(p1)->Level ); 
-    // add the node to the corresponding linked list in the table
-    pAnd->pNext      = pMan->pBins[Key];
-    pMan->pBins[Key] = pAnd;
-    pMan->nEntries++;
-    return pAnd;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes an AIG node from the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis )
+{
+    Abc_Obj_t * pAnd, ** ppPlace;
+    unsigned Key;
+    assert( !Abc_ObjIsComplement(pThis) );
+    assert( Abc_ObjFanoutNum(pThis) == 0 );
+    assert( pMan->pNtkAig == pThis->pNtk );
+    // get the hash key for these two nodes
+    Key = Abc_HashKey2( Abc_ObjChild0(pThis), Abc_ObjChild1(pThis), pMan->nBins );
+    // find the mataching node in the table
+    ppPlace = pMan->pBins + Key;
+    Abc_AigBinForEachEntry( pMan->pBins[Key], pAnd )
+        if ( pAnd != pThis )
+            ppPlace = &pAnd->pNext;
+        else
+        {
+            *ppPlace = pAnd->pNext;
+            break;
+        }
+    assert( pAnd == pThis );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_AigResize( Abc_Aig_t * pMan )
+{
+    Abc_Obj_t ** pBinsNew;
+    Abc_Obj_t * pEnt, * pEnt2;
+    int nBinsNew, Counter, i, clk;
+    unsigned Key;
+
+clk = clock();
+    // get the new table size
+    nBinsNew = Cudd_PrimeCopy(2 * pMan->nBins); 
+    // allocate a new array
+    pBinsNew = ALLOC( Abc_Obj_t *, nBinsNew );
+    memset( pBinsNew, 0, sizeof(Abc_Obj_t *) * nBinsNew );
+    // rehash the entries from the old table
+    Counter = 0;
+    for ( i = 0; i < pMan->nBins; i++ )
+        Abc_AigBinForEachEntrySafe( pMan->pBins[i], pEnt, pEnt2 )
+        {
+            Key = Abc_HashKey2( Abc_ObjFanin(pEnt,0), Abc_ObjFanin(pEnt,1), nBinsNew );
+            pEnt->pNext   = pBinsNew[Key];
+            pBinsNew[Key] = pEnt;
+            Counter++;
+        }
+    assert( Counter == pMan->nEntries );
+//    printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew );
+//    PRT( "Time", clock() - clk );
+    // replace the table and the parameters
+    free( pMan->pBins );
+    pMan->pBins = pBinsNew;
+    pMan->nBins = nBinsNew;
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description [The argument nodes can be complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
+{
+    Abc_Obj_t * pAnd;
+    if ( pAnd = Abc_AigAndLookup( pMan, p0, p1 ) )
+        return pAnd;
+    return Abc_AigAndCreate( pMan, p0, p1 );
 }
 
 /**Function*************************************************************
@@ -243,6 +550,131 @@ Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
     return pMiter;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces one AIG node by the other.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew )
+{
+    assert( Vec_PtrSize(pMan->vStackReplaceOld) == 0 );
+    assert( Vec_PtrSize(pMan->vStackReplaceNew) == 0 );
+    assert( Vec_PtrSize(pMan->vStackDelete)     == 0 );
+    Vec_PtrPush( pMan->vStackReplaceOld, pOld );
+    Vec_PtrPush( pMan->vStackReplaceNew, pNew );
+    while ( Vec_PtrSize(pMan->vStackReplaceOld) )
+        Abc_AigReplace_int( pMan );
+    while ( Vec_PtrSize(pMan->vStackDelete) )
+        Abc_AigDelete_int( pMan );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs internal replacement step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_AigReplace_int( Abc_Aig_t * pMan )
+{
+    Abc_Obj_t * pOld, * pNew, * pFanin1, * pFanin2, * pFanout, * pFanoutNew;
+    int k, iFanin;
+    // get the pair of nodes to replace
+    assert( Vec_PtrSize(pMan->vStackReplaceOld) > 0 );
+    pOld = Vec_PtrPop( pMan->vStackReplaceOld );
+    pNew = Vec_PtrPop( pMan->vStackReplaceNew );
+    // make sure the old node is regular and has fanouts
+    // the new node can be complemented and can have fanouts
+    assert( !Abc_ObjIsComplement(pOld) == 0 );
+    assert( Abc_ObjFanoutNum(pOld) > 0 );
+    // look at the fanouts of old node
+    Abc_NodeCollectFanouts( pOld, pMan->vNodes );
+    Vec_PtrForEachEntry( pMan->vNodes, pFanout, k )
+    {
+        if ( Abc_ObjIsCo(pFanout) )
+        {
+            Abc_ObjPatchFanin( pFanout, pOld, pNew );
+            continue;
+        }
+        // find the old node as a fanin of this fanout
+        iFanin = Vec_FanFindEntry( &pFanout->vFanins, pOld->Id );
+        assert( iFanin == 0 || iFanin == 1 );
+        // get the new fanin
+        pFanin1 = Abc_ObjNotCond( pNew, Abc_ObjFaninC(pFanout, iFanin) );
+        // get another fanin
+        pFanin2 = Abc_ObjChild( pFanout, iFanin ^ 1 );
+        // check if the node with these fanins exists
+        if ( pFanoutNew = Abc_AigAndLookup( pMan, pFanin1, pFanin2 ) )
+        { // such node exists (it may be a constant)
+            // schedule replacement of the old fanout by the new fanout
+            Vec_PtrPush( pMan->vStackReplaceOld, pFanout );
+            Vec_PtrPush( pMan->vStackReplaceNew, pFanoutNew );
+            continue;
+        }
+        // such node does not exist - modify the old fanout 
+        // remove the old fanout from the table
+        Abc_AigAndDelete( pMan, pFanout );
+        // remove its old fanins
+        Abc_ObjRemoveFanins( pFanout );
+        // update the old fanout with new fanins and add it to the table
+        Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
+    }
+    // schedule deletion of the old node
+    Vec_PtrPush( pMan->vStackDelete, pOld );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs internal deletion step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_AigDelete_int( Abc_Aig_t * pMan )
+{
+    Abc_Obj_t * pNode, * pFanin;
+    int k;
+    // get the node to delete
+    assert( Vec_PtrSize(pMan->vStackDelete) > 0 );
+    pNode = Vec_PtrPop( pMan->vStackDelete );
+    // make sure the node is regular and dangling
+    assert( !Abc_ObjIsComplement(pNode) == 0 );
+    assert( Abc_ObjFanoutNum(pNode) == 0 );
+    // skip the constant node
+    if ( pNode == pMan->pConst1 )
+        return;
+    // schedule fanins for deletion if they dangle
+    Abc_ObjForEachFanin( pNode, pFanin, k )
+    {
+        assert( Abc_ObjFanoutNum(pFanin) > 0 );
+        if ( Abc_ObjFanoutNum(pFanin) == 1 )
+            Vec_PtrPush( pMan->vStackDelete, pFanin );
+    }
+    // remove the node from the table
+    Abc_AigAndDelete( pMan, pNode );
+    // remove the node fro the network
+    Abc_NtkDeleteObj( pNode );
+}
+
+
+
+
 /**Function*************************************************************
 
   Synopsis    [Returns 1 if the node has at least one complemented fanout.]
@@ -298,51 +730,6 @@ bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode )
     return 0;
 }
 
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_AigResize( Abc_Aig_t * pMan )
-{
-    Abc_Obj_t ** pBinsNew;
-    Abc_Obj_t * pEnt, * pEnt2;
-    int nBinsNew, Counter, i, clk;
-    unsigned Key;
-
-clk = clock();
-    // get the new table size
-    nBinsNew = Cudd_PrimeCopy(2 * pMan->nBins); 
-    // allocate a new array
-    pBinsNew = ALLOC( Abc_Obj_t *, nBinsNew );
-    memset( pBinsNew, 0, sizeof(Abc_Obj_t *) * nBinsNew );
-    // rehash the entries from the old table
-    Counter = 0;
-    for ( i = 0; i < pMan->nBins; i++ )
-        Abc_AigBinForEachEntrySafe( pMan->pBins[i], pEnt, pEnt2 )
-        {
-            Key = Abc_HashKey2( Abc_ObjFanin(pEnt,0), Abc_ObjFanin(pEnt,1), nBinsNew );
-            pEnt->pNext   = pBinsNew[Key];
-            pBinsNew[Key] = pEnt;
-            Counter++;
-        }
-    assert( Counter == pMan->nEntries );
-//    printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew );
-//    PRT( "Time", clock() - clk );
-    // replace the table and the parameters
-    free( pMan->pBins );
-    pMan->pBins = pBinsNew;
-    pMan->nBins = nBinsNew;
-}
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c
index c530f3f6..9412305b 100644
--- a/src/base/abc/abcCreate.c
+++ b/src/base/abc/abcCreate.c
@@ -32,8 +32,6 @@ static Abc_Obj_t *   Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
 static void          Abc_ObjRecycle( Abc_Obj_t * pObj );
 static void          Abc_ObjAdd( Abc_Obj_t * pObj );
 
-extern void          Extra_StopManager( DdManager * dd );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -78,7 +76,9 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type )
     else if ( Abc_NtkIsLogicBdd(pNtk) )
         pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     else if ( Abc_NtkIsAig(pNtk) )
-        pNtk->pManFunc = Abc_AigAlloc( pNtk );
+        pNtk->pManFunc = Abc_AigAlloc( pNtk, 0 );
+    else if ( Abc_NtkIsSeq(pNtk) )
+        pNtk->pManFunc = Abc_AigAlloc( pNtk, 1 );
     else if ( Abc_NtkIsMapped(pNtk) )
         pNtk->pManFunc = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
     else
@@ -155,6 +155,30 @@ void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 
 /**Function*************************************************************
 
+  Synopsis    [Finalizes the network adding latches to CI/CO lists and creates their names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch;
+    int i;
+    // set the COs of the strashed network
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        Vec_PtrPush( pNtk->vCis, pLatch );
+        Vec_PtrPush( pNtk->vCos, pLatch );
+        Abc_NtkLogicStoreName( pLatch, Abc_ObjNameSuffix(pLatch, "L") );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Starts a new network using existing network as a model.]
 
   Description []
@@ -564,16 +588,19 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pObjNew;
     pObjNew = Abc_ObjAlloc( pNtkNew, pObj->Type );
-    if ( Abc_ObjIsNode(pObj) ) // copy the function
+    if ( Abc_ObjIsNode(pObj) ) // copy the function if network is the same type
     {
-        if ( Abc_NtkIsSop(pNtkNew) )
-            pObjNew->pData = Abc_SopRegister( pNtkNew->pManFunc, pObj->pData );
-        else if ( Abc_NtkIsLogicBdd(pNtkNew) )
-            pObjNew->pData = Cudd_bddTransfer(pObj->pNtk->pManFunc, pNtkNew->pManFunc, pObj->pData), Cudd_Ref(pObjNew->pData);
-        else if ( Abc_NtkIsMapped(pNtkNew) )
-            pObjNew->pData = pObj->pData;
-        else if ( !Abc_NtkIsAig(pNtkNew) )
-            assert( 0 );
+        if ( pNtkNew->Type == pObj->pNtk->Type || Abc_NtkIsNetlist(pObj->pNtk) || Abc_NtkIsNetlist(pNtkNew) ) 
+        {
+            if ( Abc_NtkIsSop(pNtkNew) )
+                pObjNew->pData = Abc_SopRegister( pNtkNew->pManFunc, pObj->pData );
+            else if ( Abc_NtkIsLogicBdd(pNtkNew) )
+                pObjNew->pData = Cudd_bddTransfer(pObj->pNtk->pManFunc, pNtkNew->pManFunc, pObj->pData), Cudd_Ref(pObjNew->pData);
+            else if ( Abc_NtkIsMapped(pNtkNew) )
+                pObjNew->pData = pObj->pData;
+            else if ( !Abc_NtkIsAig(pNtkNew) )
+                assert( 0 );
+        }
     }
     else if ( Abc_ObjIsNet(pObj) ) // copy the name
         pObjNew->pData = Abc_NtkRegisterName( pNtkNew, pObj->pData );
@@ -587,6 +614,55 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 
 /**Function*************************************************************
 
+  Synopsis    [Creates a new constant node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )  
+{ 
+    Abc_Obj_t * pConst1;
+    assert( Abc_NtkIsAig(pNtkAig) );
+    pConst1 = Abc_AigConst1(pNtkAig->pManFunc);
+    if ( Abc_ObjFanoutNum( pConst1 ) > 0 )
+        pConst1->pCopy = Abc_NodeCreateConst1( pNtkNew );
+    return pConst1->pCopy; 
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new constant node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )  
+{ 
+    Abc_Obj_t * pReset, * pConst1;
+    assert( Abc_NtkIsAig(pNtkAig) );
+    assert( Abc_NtkIsLogicSop(pNtkNew) );
+    pReset = Abc_AigReset(pNtkAig->pManFunc);
+    if ( Abc_ObjFanoutNum( pReset ) > 0 )
+    {
+        // create new latch with reset value 0
+        pReset->pCopy = Abc_NtkCreateLatch( pNtkNew );
+        // add constant node fanin to the latch
+        pConst1 = Abc_AigConst1(pNtkAig->pManFunc);
+        Abc_ObjAddFanin( pReset->pCopy, pConst1->pCopy );
+    }
+    return pReset->pCopy; 
+} 
+
+/**Function*************************************************************
+
   Synopsis    [Deletes the object from the network.]
 
   Description []
@@ -614,6 +690,7 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
 
     // remove from the list of objects
     Vec_PtrWriteEntry( pNtk->vObjs, pObj->Id, NULL );
+    pObj->Id = (1<<26)-1;
     pNtk->nObjs--;
 
     // perform specialized operations depending on the object type
@@ -625,8 +702,8 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
             printf( "Error: The net is not in the table...\n" );
             assert( 0 );
         }
+        pObj->pData = NULL;
         pNtk->nNets--;
-        assert( !Abc_ObjIsPi(pObj) && !Abc_ObjIsPo(pObj) );
     }
     else if ( Abc_ObjIsNode(pObj) )
     {
@@ -898,6 +975,8 @@ Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
 Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
+    if ( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) )
+        return Abc_AigConst1(pNtk->pManFunc);
     pNode = Abc_NtkCreateNode( pNtk );   
     if ( Abc_NtkIsSop(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, " 1\n" );
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 5a4b7447..3f7fae2b 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -230,15 +230,21 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsAig(pNtk) );
     // start the network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_SOP );
+    // create the constant node
+    Abc_NtkDupConst1( pNtk, pNtkNew );
     // duplicate the nodes and create node functions
     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 the choice nodes
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
+        if ( Abc_NodeIsConst(pObj) )
+            continue;
         if ( !Abc_NodeIsAigChoice(pObj) )
             continue;
         // create an OR gate
@@ -255,12 +261,10 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
         // set the new node
         pObj->pCopy = pNodeNew;
     }
-    // connect the objects
+    // connect the objects, including the COs
     Abc_NtkForEachObj( pNtk, pObj, i )
         Abc_ObjForEachFanin( pObj, pFanin, k )
             Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
-    // connect the COs
-    Abc_NtkFinalize( pNtk, pNtkNew );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
     // duplicate the EXDC Ntk
@@ -299,6 +303,8 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
         printf( "Warning: Choice nodes are skipped.\n" );
     // start the network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_SOP );
+    // create the constant node
+    Abc_NtkDupConst1( pNtk, pNtkNew );
     // collect the nodes to be used (marks all nodes with current TravId)
     vNodes = Abc_NtkDfs( pNtk );
     // create inverters for the CI and remember them
@@ -308,8 +314,11 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
     // duplicate the nodes, create node functions, and inverters
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
-        Abc_NtkDupObj( pNtkNew, pObj );
-        pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2 );
+        if ( !Abc_NodeIsConst(pObj) )
+        {
+            Abc_NtkDupObj( pNtkNew, pObj );
+            pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2 );
+        }
         if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) )
             pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
     }
@@ -324,7 +333,14 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
         }
     Vec_PtrFree( vNodes );
     // connect the COs
-    Abc_NtkFinalize( pNtk, pNtkNew );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        if ( Abc_ObjFaninC0( pObj ) )
+            Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy->pCopy );
+        else
+            Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+    }
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
     // duplicate the EXDC Ntk
diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c
index 1eac5333..f4833a11 100644
--- a/src/base/abc/abcPrint.c
+++ b/src/base/abc/abcPrint.c
@@ -40,11 +40,15 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
+void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 {
     fprintf( pFile, "%-15s:",       pNtk->pName );
     fprintf( pFile, "  i/o = %3d/%3d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
-    fprintf( pFile, "  lat = %4d", Abc_NtkLatchNum(pNtk) );
+
+    if ( !Abc_NtkIsSeq(pNtk) )
+        fprintf( pFile, "  lat = %4d", Abc_NtkLatchNum(pNtk) );
+    else
+        fprintf( pFile, "  lat = %4d", Abc_NtkSeqLatchNum(pNtk) );
 
     if ( Abc_NtkIsNetlist(pNtk) )
     {
@@ -56,14 +60,17 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
         fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
         fprintf( pFile, "  choice = %5d", Abc_NtkCountChoiceNodes(pNtk) );
     }
+    else if ( Abc_NtkIsSeq(pNtk) )
+        fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
     else 
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
 
     if ( Abc_NtkIsLogicSop(pNtk) )   
     {
         fprintf( pFile, "  cube = %5d",  Abc_NtkGetCubeNum(pNtk) );
-        fprintf( pFile, "  lit(sop) = %5d",  Abc_NtkGetLitNum(pNtk) );
-        fprintf( pFile, "  lit(fac) = %5d",  Abc_NtkGetLitFactNum(pNtk) );
+//        fprintf( pFile, "  lit(sop) = %5d",  Abc_NtkGetLitNum(pNtk) );
+        if ( fFactored )
+            fprintf( pFile, "  lit(fac) = %5d",  Abc_NtkGetLitFactNum(pNtk) );
     }
     else if ( Abc_NtkIsLogicBdd(pNtk) )
         fprintf( pFile, "  bdd = %5d",  Abc_NtkGetBddNodeNum(pNtk) );
@@ -72,11 +79,14 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
         fprintf( pFile, "  area = %5.2f", Abc_NtkGetMappedArea(pNtk) );
         fprintf( pFile, "  delay = %5.2f", Abc_NtkDelayTrace(pNtk) );
     }
-    else if ( !Abc_NtkIsAig(pNtk) )
+    else if ( !Abc_NtkIsAig(pNtk) && !Abc_NtkIsSeq(pNtk) )
     {
         assert( 0 );
     }
-    fprintf( pFile, "  lev = %2d", Abc_NtkGetLevelNum(pNtk) );
+
+    if ( !Abc_NtkIsSeq(pNtk) )
+        fprintf( pFile, "  lev = %2d", Abc_NtkGetLevelNum(pNtk) );
+
     fprintf( pFile, "\n" );
 }
 
diff --git a/src/base/abc/abcSeq.c b/src/base/abc/abcSeq.c
new file mode 100644
index 00000000..9d4658ce
--- /dev/null
+++ b/src/base/abc/abcSeq.c
@@ -0,0 +1,502 @@
+/**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"
+
+/*
+    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 reset node.
+    The reset node producing sequence (01111...) 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.
+
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                        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 );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Converts a normal AIG into a sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew;
+    assert( Abc_NtkIsAig(pNtk) );
+    // start the network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_SEQ );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts a sequential AIG into a logic SOP network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
+{
+    int fCheck = 1;
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pFanin, * pFaninNew;
+    int i, k;
+    assert( Abc_NtkIsSeq(pNtk) );
+    // start the network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_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 ( i = 0; i < Abc_ObjFaninL(pObj, k); i++ )
+                pFaninNew = pFaninNew->pCopy;
+            Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        }
+    // 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 ( fCheck && !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_NtkObjNum(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 )
+        Abc_NodeSeqCreateLatches( pObj->pCopy, Vec_IntEntry(vNumbers, 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.]
+
+  Description [The latches are attached to the node and to each other
+  through the pCopy field.]
+               
+  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_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_NtkForEachObj( pNtk, pObj, i )
+    {
+        assert( Abc_ObjFanoutLMax(pObj) == Vec_IntEntry(vNumbers, pObj->Id) );
+        Counter += Vec_IntEntry(vNumbers, pObj->Id);
+    }
+    Vec_IntFree( vNumbers );
+    return Counter;
+}
+
+
+
+
+
+
+/**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 )
+    {
+        Vec_PtrPush( vNodes, pNode );
+        pNode->fMarkA = 1;
+    }
+    // process the nodes
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        // 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;
+        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 )
+    {
+        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 ( 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;
+        assert( Abc_ObjFanoutLMin(pNode) == 0 );
+    }
+}
+
+
+
+
+/**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_ObjFanin0(pFanout) == pObj )
+        return Abc_ObjFaninL0(pFanout);
+    else if ( Abc_ObjFanin1(pFanout) == pObj )
+        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_ObjFanin0(pFanout) == pObj )
+        Abc_ObjSetFaninL0(pFanout, nLats);
+    else if ( Abc_ObjFanin1(pFanout) == pObj )
+        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_ObjFanin0(pFanout) == pObj )
+        Abc_ObjAddFaninL0(pFanout, nLats);
+    else if ( Abc_ObjFanin1(pFanout) == pObj )
+        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 = -1;
+    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;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcSeqRetime.c b/src/base/abc/abcSeqRetime.c
new file mode 100644
index 00000000..ecd8b3d7
--- /dev/null
+++ b/src/base/abc/abcSeqRetime.c
@@ -0,0 +1,203 @@
+/**CFile****************************************************************
+
+  FileName    [abcSeqRetime.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Peforms retiming for optimal clock cycle.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcSeqRetime.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// storing arrival times in the nodes
+static inline int  Abc_NodeReadLValue( Abc_Obj_t * pNode )            { return Vec_IntEntry( (pNode)->pNtk->pData, (pNode)->Id );        }
+static inline void Abc_NodeSetLValue( Abc_Obj_t * pNode, int Value )  { Vec_IntWriteEntry( (pNode)->pNtk->pData, (pNode)->Id, (Value) ); }
+
+// the internal procedures
+static int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax );
+static int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi );
+static int Abc_NodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
+
+// node status after updating its arrival time
+enum { ABC_UPDATE_FAIL, ABC_UPDATE_NO, ABC_UPDATE_YES };
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Retimes AIG for optimal delay.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk )
+{
+    int FiMax, FiBest;
+    assert( Abc_NtkIsSeq( pNtk ) );
+
+    // start storage for sequential arrival times
+    assert( pNtk->pData == NULL );
+    pNtk->pData = Vec_IntAlloc( 0 );
+
+    // get the maximum possible clock
+    FiMax = Abc_NtkNodeNum(pNtk);
+
+    // make sure this clock period is feasible
+    assert( Abc_NtkRetimeForPeriod( pNtk, FiMax ) );
+
+    // search for the optimal clock period between 0 and nLevelMax
+    FiBest = Abc_NtkRetimeSearch_rec( pNtk, 0, FiMax );
+    // print the result
+    printf( "The best clock period is %3d.\n", FiBest );
+
+    // free storage
+    Vec_IntFree( pNtk->pData );
+    pNtk->pData = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs binary search for the optimal clock period.]
+
+  Description [Assumes that FiMin is infeasible while FiMax is feasible.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax )
+{
+    int Median;
+
+    assert( FiMin < FiMax );
+    if ( FiMin + 1 == FiMax )
+        return FiMax;
+
+    Median = FiMin + (FiMax - FiMin)/2;
+
+    if ( Abc_NtkRetimeForPeriod( pNtk, Median ) )
+        return Abc_NtkRetimeSearch_rec( pNtk, FiMin, Median ); // Median is feasible
+    else 
+        return Abc_NtkRetimeSearch_rec( pNtk, Median, FiMax ); // Median is infeasible
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if retiming with this clock period is feasible.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
+{
+    Vec_Ptr_t * vFrontier;
+    Abc_Obj_t * pObj, * pFanout;
+    int RetValue, i, k;
+
+    // set l-values of all nodes to be minus infinity
+    Vec_IntFill( pNtk->pData, Abc_NtkObjNum(pNtk), -ABC_INFINITY );
+
+    // start the frontier by including PI fanouts
+    vFrontier = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        Abc_NodeSetLValue( pObj, 0 );
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            if ( pFanout->fMarkA == 0 )
+            {   
+                Vec_PtrPush( vFrontier, pFanout );
+                pFanout->fMarkA = 1;
+            }
+    }
+
+    // iterate until convergence
+    Vec_PtrForEachEntry( vFrontier, pObj, i )
+    {
+        RetValue = Abc_NodeUpdateLValue( pObj, Fi );
+        if ( RetValue == ABC_UPDATE_FAIL )
+            break;
+        // unmark the node as processed
+        pObj->fMarkA = 0;
+        if ( RetValue == ABC_UPDATE_NO ) 
+            continue;
+        assert( RetValue == ABC_UPDATE_YES );
+        // arrival times have changed - add fanouts to the frontier
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            if ( pFanout->fMarkA == 0 )
+            {   
+                Vec_PtrPush( vFrontier, pFanout );
+                pFanout->fMarkA = 1;
+            }
+    }
+    // clean the nodes
+    Vec_PtrForEachEntryStart( vFrontier, pObj, k, i )
+        pObj->fMarkA = 0;
+
+    // report the results
+    if ( RetValue == ABC_UPDATE_FAIL )
+        printf( "Period = %3d.  Updated nodes = %6d.    Infeasible\n", Fi, vFrontier->nSize );
+    else
+        printf( "Period = %3d.  Updated nodes = %6d.    Feasible\n",   Fi, vFrontier->nSize );
+    Vec_PtrFree( vFrontier );
+    return RetValue != ABC_UPDATE_FAIL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
+{
+    int lValueNew, lValue0, lValue1;
+    assert( !Abc_ObjIsPi(pObj) );
+    lValue0 = Abc_NodeReadLValue(Abc_ObjFanin0(pObj)) - Fi * Abc_ObjFaninL0(pObj);
+    if ( Abc_ObjFaninNum(pObj) == 2 )
+        lValue1 = Abc_NodeReadLValue(Abc_ObjFanin1(pObj)) - Fi * Abc_ObjFaninL1(pObj);
+    else
+        lValue1 = -ABC_INFINITY;
+    lValueNew = 1 + ABC_MAX( lValue0, lValue1 );
+    if ( Abc_ObjIsPo(pObj) && lValueNew > Fi )
+        return ABC_UPDATE_FAIL;
+    if ( lValueNew == Abc_NodeReadLValue(pObj) )
+        return ABC_UPDATE_NO;
+    Abc_NodeSetLValue( pObj, lValueNew );
+    return ABC_UPDATE_YES;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/abc/module.make b/src/base/abc/module.make
index f698d167..ee494926 100644
--- a/src/base/abc/module.make
+++ b/src/base/abc/module.make
@@ -22,6 +22,8 @@ SRC +=    src/base/abc/abc.c \
     src/base/abc/abcRenode.c \
     src/base/abc/abcRes.c \
     src/base/abc/abcSat.c \
+    src/base/abc/abcSeq.c \
+    src/base/abc/abcSeqRetime.c \
     src/base/abc/abcShow.c \
     src/base/abc/abcSop.c \
     src/base/abc/abcStrash.c \
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 3914cf99..e7584feb 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -51,6 +51,9 @@ struct Vec_Ptr_t_
 #define Vec_PtrForEachEntry( vVec, pEntry, i )                                               \
     for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
 
+#define Vec_PtrForEachEntryStart( vVec, pEntry, i, Start )                                   \
+    for ( i = Start; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
+
 #define Vec_PtrForEachEntryByLevel( vVec, pEntry, i, k )                                     \
     for ( i = 0; i < Vec_PtrSize(vVec); i++ )                                                \
         Vec_PtrForEachEntry( ((Vec_Ptr_t *)Vec_PtrEntry(vVec, i)), pEntry, k )