Version abc50916

15 files changed, 1080 insertions, 269 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index db66c49b..50787d9b 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -343,13 +343,15 @@ 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 *)ABC_INIT_ZERO;         }
-static inline void        Abc_LatchSetInit1( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_ONE;          }
-static inline void        Abc_LatchSetInitDc( Abc_Obj_t * pLatch )  { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_DC;           }
-static inline bool        Abc_LatchIsInit0( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ZERO; }
-static inline bool        Abc_LatchIsInit1( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ONE;  }
-static inline bool        Abc_LatchIsInitDc( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_DC;   }
-static inline int         Abc_LatchInit( Abc_Obj_t * pLatch )       { assert(Abc_ObjIsLatch(pLatch)); return (int)pLatch->pData;          }
+static inline void        Abc_LatchSetInitNone( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_NONE;         }
+static inline void        Abc_LatchSetInit0( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_ZERO;         }
+static inline void        Abc_LatchSetInit1( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_ONE;          }
+static inline void        Abc_LatchSetInitDc( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_DC;           }
+static inline bool        Abc_LatchIsInitNone( Abc_Obj_t * pLatch )  { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_NONE; }
+static inline bool        Abc_LatchIsInit0( Abc_Obj_t * pLatch )     { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ZERO; }
+static inline bool        Abc_LatchIsInit1( Abc_Obj_t * pLatch )     { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ONE;  }
+static inline bool        Abc_LatchIsInitDc( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_DC;   }
+static inline int         Abc_LatchInit( Abc_Obj_t * pLatch )        { assert(Abc_ObjIsLatch(pLatch)); return (int)pLatch->pData;          }
 
 // outputs the runtime in seconds
 #define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
@@ -528,6 +530,9 @@ extern void               Abc_NodeFreeNames( Vec_Ptr_t * vNames );
 extern char **            Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos );
 extern int                Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
 extern void               Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb );
+extern void               Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
 /*=== abcNetlist.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index d804601e..3e50b972 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -93,6 +93,50 @@ int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Pipelines the network with latches.]
+
+  Description []
+               
+  SideEffects [Does not check the names of the added latches!!!]
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pLatch, * pFanin, * pFanout;
+    int i, k, nTotal, nDigits;
+    if ( nLatches < 1 )
+        return;
+    nTotal = nLatches * Abc_NtkPiNum(pNtk);
+    nDigits = Extra_Base10Log( nTotal );
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        // remember current fanins of the PI
+        Abc_NodeCollectFanouts( pObj, vNodes );
+        // create the latches
+        for ( pFanin = pObj, k = 0; k < nLatches; k++, pFanin = pLatch )
+        {
+            pLatch = Abc_NtkCreateLatch( pNtk );
+            Abc_ObjAddFanin( pLatch, pFanin );
+            Abc_LatchSetInitDc( pLatch );
+            // add the latch to the CI/CO lists
+            Vec_PtrPush( pNtk->vCis, pLatch );
+            Vec_PtrPush( pNtk->vCos, pLatch );
+            // create the name of the new latch
+            Abc_NtkLogicStoreName( pLatch, Abc_ObjNameDummy("LL", i*nLatches + k, nDigits) );
+        }
+        // patch the PI fanouts
+        Vec_PtrForEachEntry( vNodes, pFanout, k )
+            Abc_ObjPatchFanin( pFanout, pObj, pFanin );
+    }
+    Vec_PtrFree( vNodes );
+    Abc_NtkLogicMakeSimpleCos( pNtk, 0 );
+}
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index 619cce23..0abccd0a 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -469,7 +469,7 @@ void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Adds dummy names.]
 
   Description []
                
@@ -478,41 +478,73 @@ void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkShortNames( Abc_Ntk_t * pNtk )
+void Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk )
 {
-    stmm_table * tObj2NameNew;
     Abc_Obj_t * pObj;
-    char Buffer[100];
-    char * pNameNew;
-    int Length, i;
-
-    tObj2NameNew = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
-    // create new names and add them to the table
-    Length = Extra_Base10Log( Abc_NtkPiNum(pNtk) );
+    int nDigits, i;
+    nDigits = Extra_Base10Log( Abc_NtkPiNum(pNtk) );
     Abc_NtkForEachPi( pNtk, pObj, i )
-    {
-        sprintf( Buffer, "pi%0*d", Length, i );
-        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
-        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
-    }
-    // create new names and add them to the table
-    Length = Extra_Base10Log( Abc_NtkPoNum(pNtk) );
+        Abc_NtkLogicStoreName( pObj, Abc_ObjNameDummy("pi", i, nDigits) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds dummy names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int nDigits, i;
+    nDigits = Extra_Base10Log( Abc_NtkPoNum(pNtk) );
     Abc_NtkForEachPo( pNtk, pObj, i )
-    {
-        sprintf( Buffer, "po%0*d", Length, i );
-        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
-        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
-    }
-    // create new names and add them to the table
-    Length = Extra_Base10Log( Abc_NtkLatchNum(pNtk) );
+        Abc_NtkLogicStoreName( pObj, Abc_ObjNameDummy("po", i, nDigits) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds dummy names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int nDigits, i;
+    nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtk) );
     Abc_NtkForEachLatch( pNtk, pObj, i )
-    {
-        sprintf( Buffer, "lat%0*d", Length, i );
-        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
-        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
-    }
+        Abc_NtkLogicStoreName( pObj, Abc_ObjNameDummy("L", i, nDigits) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces names by short names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkShortNames( Abc_Ntk_t * pNtk )
+{
     stmm_free_table( pNtk->tObj2Name );
-    pNtk->tObj2Name = tObj2NameNew;
+    pNtk->tObj2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
+    Abc_NtkAddDummyPiNames( pNtk );
+    Abc_NtkAddDummyPoNames( pNtk );
+    Abc_NtkAddDummyLatchNames( pNtk );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index bc71143b..a5605d4e 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -771,7 +771,7 @@ void Abc_NodeCollectFanins( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 {
     Abc_Obj_t * pFanin;
     int i;
-    vNodes->nSize = 0;
+    Vec_PtrClear(vNodes);
     Abc_ObjForEachFanin( pNode, pFanin, i )
         Vec_PtrPush( vNodes, pFanin );
 }
@@ -791,7 +791,7 @@ void Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 {
     Abc_Obj_t * pFanout;
     int i;
-    vNodes->nSize = 0;
+    Vec_PtrClear(vNodes);
     Abc_ObjForEachFanout( pNode, pFanout, i )
         Vec_PtrPush( vNodes, pFanout );
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 16be21fd..38472a0c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -85,6 +85,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_CommandPga          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int Abc_CommandScut         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInit         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPipe         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUnseq        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRetime       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -163,6 +166,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
     Cmd_CommandAdd( pAbc, "FPGA mapping", "pga",           Abc_CommandPga,              1 );
 
+    Cmd_CommandAdd( pAbc, "Sequential",   "scut",          Abc_CommandScut,             0 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "init",          Abc_CommandInit,             1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "pipe",          Abc_CommandPipe,             1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "unseq",         Abc_CommandUnseq,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
@@ -2725,15 +2731,15 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    memset( pParams, 0, sizeof(Cut_Params_t) );
     pParams->nVarsMax  = 5;     // the max cut size ("k" of the k-feasible cuts)
     pParams->nKeepMax  = 250;   // the max number of cuts kept at a node
     pParams->fTruth    = 0;     // compute truth tables
     pParams->fFilter   = 1;     // filter dominated cuts
-    pParams->fSeq      = 0;     // compute sequential cuts
     pParams->fDrop     = 0;     // drop cuts on the fly
     pParams->fVerbose  = 0;     // the verbosiness flag
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "KMtfsdvh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "KMtfdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2765,9 +2771,6 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             pParams->fFilter ^= 1;
             break;
-        case 's':
-            pParams->fSeq ^= 1;
-            break;
         case 'd':
             pParams->fDrop ^= 1;
             break;
@@ -2797,13 +2800,12 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfsdvh]\n" );
+    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdvh]\n" );
     fprintf( pErr, "\t         computes k-feasible cuts for the AIG\n" );
     fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n",     pParams->nVarsMax );
     fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",      pParams->nKeepMax );
     fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",           pParams->fTruth? "yes": "no" );
     fprintf( pErr, "\t-f     : toggle filtering of duplicated/dominated [default = %s]\n", pParams->fFilter? "yes": "no" );
-    fprintf( pErr, "\t-s     : toggle sequential cut computation [default = %s]\n",        pParams->fSeq? "yes": "no" );
     fprintf( pErr, "\t-d     : toggle dropping when fanouts are done [default = %s]\n",    pParams->fDrop? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",      pParams->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -2821,6 +2823,104 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandScut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cut_Params_t Params, * pParams = &Params;
+    Cut_Man_t * pCutMan;
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    extern Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    memset( pParams, 0, sizeof(Cut_Params_t) );
+    pParams->nVarsMax  = 5;     // the max cut size ("k" of the k-feasible cuts)
+    pParams->nKeepMax  = 250;   // the max number of cuts kept at a node
+    pParams->fTruth    = 0;     // compute truth tables
+    pParams->fFilter   = 0;     // filter dominated cuts
+    pParams->fSeq      = 1;     // compute sequential cuts
+    pParams->fVerbose  = 0;     // the verbosiness flag
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "KMtvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pParams->nVarsMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( pParams->nVarsMax < 0 ) 
+                goto usage;
+            break;
+        case 'M':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pParams->nKeepMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( pParams->nKeepMax < 0 ) 
+                goto usage;
+            break;
+        case 't':
+            pParams->fTruth ^= 1;
+            break;
+        case 'v':
+            pParams->fVerbose ^= 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, "Sequential cuts can be computed for sequential AIGs (run \"seq\").\n" );
+        return 1;
+    }
+    pCutMan = Abc_NtkSeqCuts( pNtk, pParams );
+    Cut_ManPrintStats( pCutMan );
+    Cut_ManStop( pCutMan );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: scut [-K num] [-M num] [-tvh]\n" );
+    fprintf( pErr, "\t         computes k-feasible cuts for the sequential AIG\n" );
+    fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n",     pParams->nVarsMax );
+    fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",      pParams->nKeepMax );
+    fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",           pParams->fTruth? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",      pParams->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -3903,6 +4003,195 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObj;
+    int c, i;
+    int fZeros;
+    int fOnes;
+    int fRandom;
+    int fDontCare;
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fZeros    = 0;
+    fOnes     = 0;
+    fRandom   = 0;
+    fDontCare = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "zordh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'z':
+            fZeros ^= 1;
+            break;
+        case 'o':
+            fOnes ^= 1;
+            break;
+        case 'r':
+            fRandom ^= 1;
+            break;
+        case 'd':
+            fDontCare ^= 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, "Does not work for a sequentail AIG (run \"unseq\").\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "The current network is combinational.\n" );
+        return 1;
+    }
+
+    if ( fZeros )
+    {
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_LatchSetInit0( pObj );
+    }
+    else if ( fOnes )
+    {
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_LatchSetInit1( pObj );
+    }
+    else if ( fRandom )
+    {
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            if ( rand() & 1 )
+                Abc_LatchSetInit1( pObj );
+            else
+                Abc_LatchSetInit0( pObj );
+    }
+    else if ( fDontCare )
+    {
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_LatchSetInitDc( pObj );
+    }
+    else
+        printf( "The initial states remain unchanged.\n" );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: init [-zordh]\n" );
+    fprintf( pErr, "\t        resets initial states of all latches\n" );
+    fprintf( pErr, "\t-z    : set zeros initial states [default = %s]\n", fZeros? "yes": "no" );
+    fprintf( pErr, "\t-o    : set ones initial states [default = %s]\n", fOnes? "yes": "no" );
+    fprintf( pErr, "\t-d    : set don't-care initial states [default = %s]\n", fDontCare? "yes": "no" );
+    fprintf( pErr, "\t-r    : set random initial states [default = %s]\n", fRandom? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nLatches;
+    extern void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nLatches = 5;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "Lh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'L':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-L\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nLatches = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nLatches < 0 ) 
+                goto usage;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Does not work for a sequentail AIG (run \"unseq\").\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "The current network is combinational.\n" );
+        return 1;
+    }
+
+    // update the network
+    Abc_NtkLatchPipe( pNtk, nLatches );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: pipe [-L num] [-h]\n" );
+    fprintf( pErr, "\t         inserts the given number of latches at the PIs\n" );
+    fprintf( pErr, "\t-L num : the number of latches to insert [default = %d]\n", nLatches );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -4066,7 +4355,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fForward  = 1;
+    fForward  = 0;
     fBackward = 0;
     fInitial  = 0;
     util_getopt_reset();
@@ -4098,7 +4387,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsSeq(pNtk) )
     {
-        fprintf( pErr, "Works only for sequential AIG.\n" );
+        fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
         return 1;
     }
 
@@ -4114,11 +4403,11 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: retime [-fbih]\n" );
+    fprintf( pErr, "usage: retime [-fbh]\n" );
     fprintf( pErr, "\t        retimes sequential AIG (default is Pan's delay-optimal retiming)\n" );
     fprintf( pErr, "\t-f    : toggle forward retiming [default = %s]\n", fForward? "yes": "no" );
     fprintf( pErr, "\t-b    : toggle backward retiming [default = %s]\n", fBackward? "yes": "no" );
-    fprintf( pErr, "\t-i    : toggle retiming for initial state [default = %s]\n", fInitial? "yes": "no" );
+//    fprintf( pErr, "\t-i    : toggle retiming for initial state [default = %s]\n", fInitial? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index e7309a59..64dec4a4 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -43,7 +43,7 @@
 Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
 {
     Cut_Man_t *  p;
-    Abc_Obj_t * pObj, * pDriver, * pNode;
+    Abc_Obj_t * pObj, * pNode;
     Vec_Ptr_t * vNodes;
     Vec_Int_t * vChoices;
     int i;
@@ -86,30 +86,26 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
             Cut_NodeUnionCuts( p, vChoices );
         }
     }
-    if ( !pParams->fSeq )
-    {
-        Vec_PtrFree( vNodes );
-        Vec_IntFree( vChoices );
+    Vec_PtrFree( vNodes );
+    Vec_IntFree( vChoices );
 PRT( "Total", clock() - clk );
-        return p;
-    }
-    assert( 0 );
+    return p;
+}
 
-    // compute sequential cuts
-    Abc_NtkIncrementTravId( pNtk );
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-    {
-        pDriver = Abc_ObjFanin0(pObj);
-        if ( !Abc_ObjIsNode(pDriver) )
-            continue;
-        if ( Abc_NodeIsTravIdCurrent(pDriver) )
-            continue;
-        Abc_NodeSetTravIdCurrent(pDriver);
-    }
-    // compute as long as new cuts appear
+/**Function*************************************************************
 
+  Synopsis    [Computes the cuts for the network.]
 
-    return p;
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
+{
+    return NULL;
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 01317d1d..c5a9f5f3 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -491,7 +491,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
         Counter = 0;
         Abc_NtkForEachLatch( pNtk, pLatch, i )
         {
-            if ( Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI
+            if ( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI
             {
                 pLatch->pCopy = Abc_NtkCreatePi(pNtkFrames);
                 Abc_NtkLogicStoreName( pLatch->pCopy, Abc_ObjName(pLatch) );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 26ce3665..2e9c3cc8 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -145,7 +145,17 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pLatch, * pFanin;
     int i, Counter0, Counter1, Counter2;
-    int Init0, Init1, Init2;
+    int InitNums[4], Init;
+
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        Abc_NtkSeqLatchGetInitNums( pNtk, InitNums );
+        fprintf( pFile, "%-15s:  ", pNtk->pName );
+        fprintf( pFile, "Latch = %6d. No = %4d. Zero = %4d. One = %4d. DC = %4d.\n", 
+            Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] );
+        return;
+    }
 
     if ( Abc_NtkLatchNum(pNtk) == 0 )
     {
@@ -153,21 +163,14 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
         return;
     }
 
-    assert( !Abc_NtkIsNetlist(pNtk) );
-
-    Init0 = Init1 = Init2 = 0;
+    for ( i = 0; i < 4; i++ )    
+        InitNums[i] = 0;
     Counter0 = Counter1 = Counter2 = 0;
-
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
-        if ( Abc_LatchIsInit0(pLatch) )
-            Init0++;
-        else if ( Abc_LatchIsInit1(pLatch) )
-            Init1++;
-        else if ( Abc_LatchIsInitDc(pLatch) )
-            Init2++;
-        else
-            assert( 0 );
+        Init = Abc_LatchInit( pLatch );
+        assert( Init < 4 );
+        InitNums[Init]++;
 
         pFanin = Abc_ObjFanin0(pLatch);
         if ( !Abc_ObjIsNode(pFanin) || !Abc_NodeIsConst(pFanin) )
@@ -192,14 +195,11 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
                 Counter2++;
         }
     }
-//    fprintf( pFile, "%-15s: ", pNtk->pName );
-//    fprintf( pFile, "L = %5d: 0 = %4d. 1 = %3d. DC = %4d. ", Abc_NtkLatchNum(pNtk), Init0, Init1, Init2 );
-//    fprintf( pFile, "Con = %3d. DC = %3d. Mat = %3d. ", Counter0, Counter1, Counter2 );
-//    fprintf( pFile, "SFeed = %2d.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
     fprintf( pFile, "%-15s:  ", pNtk->pName );
-    fprintf( pFile, "Lat = %5d: 0 = %4d. 1 = %3d. DC = %4d. \n", Abc_NtkLatchNum(pNtk), Init0, Init1, Init2 );
-    fprintf( pFile, "Con = %3d. DC = %3d. Mat = %3d. ", Counter0, Counter1, Counter2 );
-    fprintf( pFile, "SFeed = %2d.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
+    fprintf( pFile, "Latch = %6d. No = %4d. Zero = %4d. One = %4d. DC = %4d.\n", 
+        Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] );
+    fprintf( pFile, "Const fanin = %3d. DC init = %3d. Matching init = %3d. ", Counter0, Counter1, Counter2 );
+    fprintf( pFile, "Self-feed latches = %2d.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abcs/abcRetDelay.c b/src/base/abcs/abcRetDelay.c
index 71114171..277e7750 100644
--- a/src/base/abcs/abcRetDelay.c
+++ b/src/base/abcs/abcRetDelay.c
@@ -25,8 +25,10 @@
 ////////////////////////////////////////////////////////////////////////
 
 // 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) ); }
+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) );    }
+//static inline int  Abc_NodeGetLag( int LValue, int Fi )               { return LValue/Fi - (int)(LValue % Fi == 0); }
+static inline int  Abc_NodeGetLag( int LValue, int Fi )               { return (LValue + 256*Fi)/Fi - 256 - (int)(LValue % Fi == 0); }
 
 // the internal procedures
 static int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax );
@@ -36,6 +38,8 @@ 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 };
 
+static void Abc_RetimingExperiment( Abc_Ntk_t * pNtk, Vec_Str_t * vLags );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -59,11 +63,16 @@ Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsSeq( pNtk ) );
 
     // start storage for sequential arrival times
-    assert( pNtk->pData == NULL );
+//    assert( pNtk->pData == NULL );
     pNtk->pData = Vec_IntAlloc( 0 );
 
-    // get the maximum possible clock
-    FiMax = Abc_NtkNodeNum(pNtk);
+    // get the upper bound on the clock period
+//    FiMax = Abc_NtkNodeNum(pNtk);
+    FiMax = 0;
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        if ( FiMax < (int)pNode->Level )
+            FiMax = pNode->Level;
+    FiMax += 2;
 
     // make sure this clock period is feasible
     assert( Abc_NtkRetimeForPeriod( pNtk, FiMax ) );
@@ -76,7 +85,23 @@ Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk )
     // convert to lags
     vLags = Vec_StrStart( Abc_NtkObjNumMax(pNtk) );
     Abc_AigForEachAnd( pNtk, pNode, i )
-        Vec_StrWriteEntry( vLags, i, (char)(Abc_NodeReadLValue(pNode) / FiBest) );
+        Vec_StrWriteEntry( vLags, i, (char)Abc_NodeGetLag(Abc_NodeReadLValue(pNode), FiBest) );
+/*
+    printf( "LValues : " );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        printf( "%d=%d ", i, Abc_NodeReadLValue(pNode) );
+    printf( "\n" );
+*/
+
+/*
+    printf( "Lags : " );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        if ( Vec_StrEntry(vLags,i) != 0 )
+            printf( "%d=%d(%d)(%d) ", i, Vec_StrEntry(vLags,i), Abc_NodeReadLValue(pNode), Abc_NodeReadLValue(pNode) - FiBest * Vec_StrEntry(vLags,i) );
+    printf( "\n" );
+*/
+
+//    Abc_RetimingExperiment( pNtk, vLags );
 
     // free storage
     Vec_IntFree( pNtk->pData );
@@ -98,13 +123,10 @@ Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk )
 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 
@@ -122,17 +144,30 @@ int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
+int Abc_NtkRetimeForPeriod2( Abc_Ntk_t * pNtk, int Fi )
 {
     Vec_Ptr_t * vFrontier;
     Abc_Obj_t * pObj, * pFanout;
+    char * pReason = "";
     int RetValue, i, k;
+    int Limit;
 
     // set l-values of all nodes to be minus infinity
     Vec_IntFill( pNtk->pData, Abc_NtkObjNumMax(pNtk), -ABC_INFINITY );
 
-    // start the frontier by including PI fanouts
+    // start the frontier by setting PI l-values to 0 and including PI fanouts
     vFrontier = Vec_PtrAlloc( 100 );
+    pObj = Abc_NtkObj( pNtk, 0 );
+    if ( Abc_ObjFanoutNum(pObj) > 0 )
+    {
+        Abc_NodeSetLValue( pObj, 0 );
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            if ( pFanout->fMarkA == 0 )
+            {   
+                Vec_PtrPush( vFrontier, pFanout );
+                pFanout->fMarkA = 1;
+            }
+    }
     Abc_NtkForEachPi( pNtk, pObj, i )
     {
         Abc_NodeSetLValue( pObj, 0 );
@@ -145,19 +180,25 @@ int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
     }
 
     // iterate until convergence
+    Limit = Abc_NtkObjNumMax(pNtk) * 20;
     Vec_PtrForEachEntry( vFrontier, pObj, i )
     {
+        pObj->fMarkA = 0;
         RetValue = Abc_NodeUpdateLValue( pObj, Fi );
         if ( RetValue == ABC_UPDATE_FAIL )
             break;
-        // unmark the node as processed
-        pObj->fMarkA = 0;
+        if ( i == Limit )
+        {
+            RetValue = ABC_UPDATE_FAIL;
+            pReason = "(timeout)";
+            break;
+        }
         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 )
+            if ( pFanout->fMarkA == 0 && pFanout != pObj )
             {   
                 Vec_PtrPush( vFrontier, pFanout );
                 pFanout->fMarkA = 1;
@@ -167,18 +208,18 @@ int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
     Vec_PtrForEachEntryStart( vFrontier, pObj, k, i )
         pObj->fMarkA = 0;
 
-    // report the results
+  // report the results
     if ( RetValue == ABC_UPDATE_FAIL )
-        printf( "Period = %3d.  Updated nodes = %6d.    Infeasible\n", Fi, vFrontier->nSize );
+        printf( "Period = %3d.  Updated nodes = %6d.    Infeasible %s\n", Fi, vFrontier->nSize, pReason );
     else
         printf( "Period = %3d.  Updated nodes = %6d.    Feasible\n",   Fi, vFrontier->nSize );
-    Vec_PtrFree( vFrontier );
+//    Vec_PtrFree( vFrontier );
     return RetValue != ABC_UPDATE_FAIL;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the l-value of the node.]
+  Synopsis    [Returns 1 if retiming with this clock period is feasible.]
 
   Description []
                
@@ -187,24 +228,276 @@ int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
+{
+    Abc_Obj_t * pObj;
+    int i, c, RetValue, fChange, Counter;
+    char * pReason = "";
+
+    // set l-values of all nodes to be minus infinity
+    Vec_IntFill( pNtk->pData, Abc_NtkObjNumMax(pNtk), -ABC_INFINITY );
+
+    pObj = Abc_NtkObj( pNtk, 0 );
+    Abc_NodeSetLValue( pObj, 0 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NodeSetLValue( pObj, 0 );
+
+    Counter = 0;
+    for ( c = 0; c < 20; c++ )
+    {
+        fChange = 0;
+        Abc_NtkForEachObj( pNtk, pObj, i )
+        {
+            if ( Abc_ObjIsPi(pObj) )
+                continue;
+            if ( Abc_ObjFaninNum(pObj) == 0 )
+                continue;
+            RetValue = Abc_NodeUpdateLValue( pObj, Fi );
+            Counter++;
+            if ( RetValue == ABC_UPDATE_FAIL )
+                break;
+            if ( RetValue == ABC_UPDATE_NO ) 
+                continue;
+            fChange = 1;
+        }
+        if ( RetValue == ABC_UPDATE_FAIL )
+            break;
+        if ( fChange == 0 )
+            break;
+    }
+    if ( c == 20 )
+    {
+        RetValue = ABC_UPDATE_FAIL;
+        pReason = "(timeout)";
+    }
+
+    // report the results
+    if ( RetValue == ABC_UPDATE_FAIL )
+        printf( "Period = %3d.  Iterations = %3d.  Updates = %6d.  Infeasible %s\n", Fi, c, Counter, pReason );
+    else
+        printf( "Period = %3d.  Iterations = %3d.  Updates = %6d.  Feasible\n",   Fi, c, Counter );
+    return RetValue != ABC_UPDATE_FAIL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the l-value of the node.]
+
+  Description [The node can be internal or a PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_NodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
 {
-    int lValueNew, lValue0, lValue1;
+    int lValueNew, lValueOld, lValue0, lValue1;
     assert( !Abc_ObjIsPi(pObj) );
+    assert( Abc_ObjFaninNum(pObj) > 0 );
     lValue0 = Abc_NodeReadLValue(Abc_ObjFanin0(pObj)) - Fi * Abc_ObjFaninL0(pObj);
+    if ( Abc_ObjIsPo(pObj) )
+        return (lValue0 > Fi)? ABC_UPDATE_FAIL : ABC_UPDATE_NO;
     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) )
+    lValueOld = Abc_NodeReadLValue(pObj);
+//    if ( lValueNew == lValueOld )
+    if ( lValueNew <= lValueOld )
         return ABC_UPDATE_NO;
     Abc_NodeSetLValue( pObj, lValueNew );
     return ABC_UPDATE_YES;
 }
 
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_RetimingPrint_rec( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin0, * pFanin1;
+    int Depth0, Depth1;
+
+    if ( Abc_ObjIsPi(pObj) )
+    {
+        printf( "%d -> ", pObj->Id );
+        return 0;
+    }
+    
+    pFanin0 = Abc_ObjFanin0(pObj);
+    pFanin1 = Abc_ObjFanin1(pObj);
+
+    if ( Abc_ObjFaninL0(pObj) == 0 && Abc_ObjFaninL1(pObj) > 0 )
+        Abc_RetimingPrint_rec( pFanin0 );
+    else if ( Abc_ObjFaninL1(pObj) == 0 && Abc_ObjFaninL0(pObj) > 0 )
+        Abc_RetimingPrint_rec( pFanin1 );
+    else if ( Abc_ObjFaninL0(pObj) == 0 && Abc_ObjFaninL1(pObj) == 0 )
+    {
+        Depth0 = (int)pFanin0->pCopy;
+        Depth1 = (int)pFanin1->pCopy;
+
+        if ( Depth0 > Depth1 )
+            Abc_RetimingPrint_rec( pFanin0 );
+        else
+            Abc_RetimingPrint_rec( pFanin1 );
+    }
+
+    printf( "%d (%d) -> ", pObj->Id, (int)pObj->pCopy );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_Retiming_rec( Abc_Obj_t * pObj )
+{
+    int Depth0, Depth1, Depth;
+    if ( Abc_ObjIsPi(pObj) )
+    {
+        pObj->pCopy = 0;
+        return 0;
+    }
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pObj ) )
+        return (int)pObj->pCopy;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pObj );
+    if ( Abc_ObjFaninL0(pObj) == 0 )
+        Depth0 = Abc_Retiming_rec( Abc_ObjFanin0(pObj) );
+    else
+        Depth0 = 0;
+    if ( Abc_ObjFaninL1(pObj) == 0 )
+        Depth1 = Abc_Retiming_rec( Abc_ObjFanin1(pObj) );
+    else
+        Depth1 = 0;
+    Depth = 1 + ABC_MAX( Depth0, Depth1 );
+    pObj->pCopy = (void *)Depth;
+    return Depth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRetiming( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, Depth;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) != 2 )
+            continue;
+        if ( Abc_ObjFaninL0(pObj) > 0 )
+        {
+            Abc_NtkIncrementTravId(pNtk);
+            Depth = Abc_Retiming_rec( Abc_ObjFanin0(pObj) );
+            if ( Depth > 30 )
+            {
+                printf( "Depth is %d.   ", Depth );
+                Abc_RetimingPrint_rec( Abc_ObjFanin0(pObj) );
+                printf( "\n\n" );
+            }
+        }
+        if ( Abc_ObjFaninL1(pObj) > 0 )
+        {
+            Abc_NtkIncrementTravId(pNtk);
+            Depth = Abc_Retiming_rec( Abc_ObjFanin1(pObj) );
+            if ( Depth > 30 )
+            {
+                printf( "Depth is %d.   ", Depth );
+                Abc_RetimingPrint_rec( Abc_ObjFanin1(pObj) );
+                printf( "\n\n" );
+            }
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_RetimingExperiment( Abc_Ntk_t * pNtk, Vec_Str_t * vLags )
+{
+    Abc_Obj_t * pObj;
+    char Lag;
+    int i;
+
+    Vec_StrForEachEntry( vLags, Lag, i )
+    {
+        if ( Lag == 0 )
+            continue;
+        pObj = Abc_NtkObj( pNtk, i );
+        if ( Lag < 0 )
+            Abc_ObjRetimeForwardTry( pObj, -Lag );
+        else
+            Abc_ObjRetimeBackwardTry( pObj, Lag );
+    }
+
+    // make sure there are no negative latches
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) == 0 )
+            continue;
+        assert( Abc_ObjFaninL0(pObj) >= 0 );
+        if ( Abc_ObjFaninNum(pObj) == 1 )
+            continue;
+        assert( Abc_ObjFaninL1(pObj) >= 0 );
+//        printf( "%d=(%d,%d) ", i, Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) );
+    }
+//    printf( "\n" );
+
+    Abc_NtkRetiming( pNtk );
+
+    Vec_StrForEachEntry( vLags, Lag, i )
+    {
+        if ( Lag == 0 )
+            continue;
+        pObj = Abc_NtkObj( pNtk, i );
+        if ( Lag < 0 )
+            Abc_ObjRetimeBackwardTry( pObj, -Lag );
+        else
+            Abc_ObjRetimeForwardTry( pObj, Lag );
+    }
+
+//    Abc_NtkSeqRetimeDelayLags( pNtk );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abcs/abcRetImpl.c b/src/base/abcs/abcRetImpl.c
index ea849c1c..0082ff22 100644
--- a/src/base/abcs/abcRetImpl.c
+++ b/src/base/abcs/abcRetImpl.c
@@ -26,6 +26,8 @@
 
 static void Abc_ObjRetimeForward( Abc_Obj_t * pObj );
 static int  Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtk, stmm_table * tTable, Vec_Int_t * vValues );
+static void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable );
+static void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -51,7 +53,9 @@ int Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags )
     // forward retiming
     vSteps = Abc_NtkUtilRetimingSplit( vLags, 1 );
     // translate each set of steps into moves
+    printf( "The number of forward steps  = %6d.\n", Vec_IntSize(vSteps) );
     vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 1 );
+    printf( "The number of forward moves  = %6d.\n", Vec_PtrSize(vMoves) );
     // implement this retiming
     Abc_NtkImplementRetimingForward( pNtk, vMoves );
     Vec_IntFree( vSteps );
@@ -60,7 +64,9 @@ int Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags )
     // backward retiming
     vSteps = Abc_NtkUtilRetimingSplit( vLags, 0 );
     // translate each set of steps into moves
+    printf( "The number of backward steps = %6d.\n", Vec_IntSize(vSteps) );
     vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 0 );
+    printf( "The number of backward moves = %6d.\n", Vec_PtrSize(vMoves) );
     // implement this retiming
     RetValue = Abc_NtkImplementRetimingBackward( pNtk, vMoves );
     Vec_IntFree( vSteps );
@@ -89,6 +95,58 @@ void Abc_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
 
 /**Function*************************************************************
 
+  Synopsis    [Retimes node forward by one latch.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjRetimeForward( Abc_Obj_t * pObj )  
+{
+    Abc_Obj_t * pFanout;
+    int Init0, Init1, Init, i;
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    assert( Abc_ObjFaninL0(pObj) >= 1 );
+    assert( Abc_ObjFaninL1(pObj) >= 1 );
+    // remove the init values from the fanins
+    Init0 = Abc_ObjFaninLDeleteFirst( pObj, 0 );
+    Init1 = Abc_ObjFaninLDeleteFirst( pObj, 1 );
+    assert( Init0 != ABC_INIT_NONE );
+    assert( Init1 != ABC_INIT_NONE );
+    // take into account the complements in the node
+    if ( Abc_ObjFaninC0(pObj) )
+    {
+        if ( Init0 == ABC_INIT_ZERO )
+            Init0 = ABC_INIT_ONE;
+        else if ( Init0 == ABC_INIT_ONE )
+            Init0 = ABC_INIT_ZERO;
+    }
+    if ( Abc_ObjFaninC1(pObj) )
+    {
+        if ( Init1 == ABC_INIT_ZERO )
+            Init1 = ABC_INIT_ONE;
+        else if ( Init1 == ABC_INIT_ONE )
+            Init1 = ABC_INIT_ZERO;
+    }
+    // compute the value at the output of the node
+    if ( Init0 == ABC_INIT_ZERO || Init1 == ABC_INIT_ZERO )
+        Init = ABC_INIT_ZERO;
+    else if ( Init0 == ABC_INIT_ONE && Init1 == ABC_INIT_ONE )
+        Init = ABC_INIT_ONE;
+    else
+        Init = ABC_INIT_DC;
+    // add the init values to the fanouts
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        Abc_ObjFaninLInsertLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout), Init );
+}
+
+
+
+/**Function*************************************************************
+
   Synopsis    [Implements the given retiming on the sequential AIG.]
 
   Description [Returns 0 of initial state computation fails.]
@@ -106,39 +164,50 @@ int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
     Vec_Int_t * vValues;
     Abc_Ntk_t * pNtkProb, * pNtkMiter, * pNtkCnf;
     Abc_Obj_t * pNode, * pNodeNew;
-    int * pModel, Init, nDigits, RetValue, i;
+    int * pModel, RetValue, i, clk;
 
     // return if the retiming is trivial
     if ( Vec_PtrSize(vMoves) == 0 )
         return 1;
 
-    // start the table and the array of PO values
-    tTable = stmm_init_table( stmm_numcmp, stmm_numhash );
-    vValues = Vec_IntAlloc( 100 );
-
     // create the network for the initial state computation
+    // start the table and the array of PO values
     pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    tTable   = stmm_init_table( stmm_numcmp, stmm_numhash );
+    vValues  = Vec_IntAlloc( 100 );
 
-    // perform the backward moves and build the network
+    // perform the backward moves and build the network for initial state computation
+    RetValue = 0;
     Vec_PtrForEachEntry( vMoves, pNode, i )
-        Abc_ObjRetimeBackward( pNode, pNtkProb, tTable, vValues );
+        RetValue |= Abc_ObjRetimeBackward( pNode, pNtkProb, tTable, vValues );
 
     // add the PIs corresponding to the white spots
     stmm_foreach_item( tTable, gen, (char **)&RetEdge, (char **)&pNodeNew )
         Abc_ObjAddFanin( pNodeNew, Abc_NtkCreatePi(pNtkProb) );
 
     // add the PI/PO names
-    nDigits = Extra_Base10Log( Abc_NtkPiNum(pNtkProb) );
-    Abc_NtkForEachPi( pNtkProb, pNodeNew, i )
-        Abc_NtkLogicStoreName( pNodeNew, Abc_ObjNameDummy("pi", i, nDigits) );
-    nDigits = Extra_Base10Log( Abc_NtkPoNum(pNtkProb) );
-    Abc_NtkForEachPo( pNtkProb, pNodeNew, i )
-        Abc_NtkLogicStoreName( pNodeNew, Abc_ObjNameDummy("po", i, nDigits) );
+    Abc_NtkAddDummyPiNames( pNtkProb );
+    Abc_NtkAddDummyPoNames( pNtkProb );
 
     // make sure everything is okay with the network structure
     if ( !Abc_NtkDoCheck( pNtkProb ) )
     {
         printf( "Abc_NtkImplementRetimingBackward: The internal network check has failed.\n" );
+        Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL );
+        Abc_NtkDelete( pNtkProb );
+        stmm_free_table( tTable );
+        Vec_IntFree( vValues );
+        return 0;
+    }
+
+    // check if conflict is found
+    if ( RetValue )
+    {
+        printf( "Abc_NtkImplementRetimingBackward: A top level conflict is detected. DC latch values are used.\n" );
+        Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL );
+        Abc_NtkDelete( pNtkProb );
+        stmm_free_table( tTable );
+        Vec_IntFree( vValues );
         return 0;
     }
 
@@ -147,31 +216,36 @@ int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
     Abc_NtkDelete( pNtkProb );
     Vec_IntFree( vValues );
 
+    printf( "The number of ANDs in the AIG = %5d.\n", Abc_NtkNodeNum(pNtkMiter) );
+
     // transform the miter into a logic network for efficient CNF construction
     pNtkCnf = Abc_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 );
     Abc_NtkDelete( pNtkMiter );
 
     // solve the miter
+clk = clock();
     RetValue = Abc_NtkMiterSat( pNtkCnf, 30, 0 );
+if ( clock() - clk > 500 )
+{
+PRT( "SAT solving time", clock() - clk );
+}
     pModel = pNtkCnf->pModel;  pNtkCnf->pModel = NULL;
     Abc_NtkDelete( pNtkCnf );
 
     // analyze the result
     if ( RetValue == -1 || RetValue == 1 )
     {
+        Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL );
+        if ( RetValue == 1 )
+            printf( "Abc_NtkImplementRetimingBackward: The problem is unsatisfiable. DC latch values are used.\n" );
+        else
+            printf( "Abc_NtkImplementRetimingBackward: The SAT problem timed out. DC latch values are used.\n" );
         stmm_free_table( tTable );
         return 0;
     }
 
     // set the values of the latches
-    i = 0;
-    stmm_foreach_item( tTable, gen, (char **)&RetEdge, (char **)&pNodeNew )
-    {
-        pNode = Abc_NtkObj( pNtk, RetEdge.iNode );
-        Init = pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO;
-        Abc_ObjFaninLSetInitOne( pNode, RetEdge.iEdge, RetEdge.iLatch, Init );
-        i++;
-    }
+    Abc_NtkRetimeSetInitialValues( pNtk, tTable, pModel );
     stmm_free_table( tTable );
     free( pModel );
     return 1;
@@ -179,59 +253,10 @@ int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
 
 /**Function*************************************************************
 
-  Synopsis    [Retimes node forward by one latch.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_ObjRetimeForward( Abc_Obj_t * pObj )  
-{
-    Abc_Obj_t * pFanout;
-    int Init0, Init1, Init, i;
-    assert( Abc_ObjFaninNum(pObj) == 2 );
-    assert( Abc_ObjFaninL0(pObj) >= 1 );
-    assert( Abc_ObjFaninL1(pObj) >= 1 );
-    // remove the init values from the fanins
-    Init0 = Abc_ObjFaninLDeleteFirst( pObj, 0 );
-    Init1 = Abc_ObjFaninLDeleteFirst( pObj, 1 );
-    assert( Init0 != ABC_INIT_NONE );
-    assert( Init1 != ABC_INIT_NONE );
-    // take into account the complements in the node
-    if ( Abc_ObjFaninC0(pObj) )
-    {
-        if ( Init0 == ABC_INIT_ZERO )
-            Init0 = ABC_INIT_ONE;
-        else if ( Init0 == ABC_INIT_ONE )
-            Init0 = ABC_INIT_ZERO;
-    }
-    if ( Abc_ObjFaninC1(pObj) )
-    {
-        if ( Init1 == ABC_INIT_ZERO )
-            Init1 = ABC_INIT_ONE;
-        else if ( Init1 == ABC_INIT_ONE )
-            Init1 = ABC_INIT_ZERO;
-    }
-    // compute the value at the output of the node
-    if ( Init0 == ABC_INIT_ZERO || Init1 == ABC_INIT_ZERO )
-        Init = ABC_INIT_ZERO;
-    else if ( Init0 == ABC_INIT_ONE && Init1 == ABC_INIT_ONE )
-        Init = ABC_INIT_ONE;
-    else
-        Init = ABC_INIT_DC;
-    // add the init values to the fanouts
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        Abc_ObjFaninLInsertLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout), Init );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Retimes node backward by one latch.]
 
-  Description [Constructs the problem for initial state computation.]
+  Description [Constructs the problem for initial state computation.
+  Returns 1 if the conflict is found.]
                
   SideEffects []
 
@@ -242,15 +267,14 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t
 {
     Abc_Obj_t * pFanout;
     Abc_InitType_t Init, Value;
-    Abc_RetEdge_t Edge;
-    Abc_Obj_t * pNodeNew, * pFanoutNew, * pBuf;
-    unsigned Entry;
-    int i, fMet0, fMet1, fMetX;
+    Abc_RetEdge_t RetEdge;
+    Abc_Obj_t * pNodeNew, * pFanoutNew, * pBuffer;
+    int i, Edge, fMet0, fMet1, fMetN;
 
     // make sure the node can be retimed
     assert( Abc_ObjFanoutLMin(pObj) > 0 );
     // get the fanout values
-    fMet0 = fMet1 = fMetX = 0;
+    fMet0 = fMet1 = fMetN = 0;
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
         Init = Abc_ObjFaninLGetInitLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout) );
@@ -259,101 +283,159 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t
         else if ( Init == ABC_INIT_ONE )
             fMet1 = 1;
         else if ( Init == ABC_INIT_NONE )
-            fMetX = 1;
+            fMetN = 1;
     }
-    // quit if conflict is found
-    if ( fMet0 && fMet1 )
+
+    // consider the case when all fanout latchs have don't-care values
+    // the new values on the fanin edges will be don't-cares
+    if ( !fMet0 && !fMet1 && !fMetN )
+   {
+        // update the fanout edges
+        Abc_ObjForEachFanout( pObj, pFanout, i )
+            Abc_ObjFaninLDeleteLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout) );
+        // update the fanin edges
+        Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable );
+        Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable );
+        Abc_ObjFaninLInsertFirst( pObj, 0, ABC_INIT_DC );
+        Abc_ObjFaninLInsertFirst( pObj, 1, ABC_INIT_DC );
         return 0;
+    }
+    // the initial values on the fanout edges contain 0, 1, or unknown
+    // the new values on the fanin edges will be unknown
 
-    // get the new initial value
-    if ( !fMet0 && !fMet1 && !fMetX )
+    // add new AND-gate to the network
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    pNodeNew->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+
+    // add PO fanouts if any
+    if ( fMet0 )
     {
-        Init = ABC_INIT_DC;
-        // do not add the node
-        pNodeNew = NULL;
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
+        Vec_IntPush( vValues, 0 );
     }
-    else
+    if ( fMet1 )
     {
-        Init = ABC_INIT_NONE;
-        // add the node to the network
-        pNodeNew = Abc_NtkCreateNode( pNtkNew );
-        pNodeNew->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
+        Vec_IntPush( vValues, 1 );
     }
 
     // perform the changes
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
-        Edge.iNode = pFanout->Id;
-        Edge.iEdge = Abc_ObjEdgeNum(pObj, pFanout);
-        Edge.iLatch = Abc_ObjFaninL( pFanout, Edge.iEdge ) - 1;
-        // try to delete this edge
-        stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew );
-        // delete the entry
-        Value = Abc_ObjFaninLDeleteLast( pFanout, Edge.iEdge );
-        if ( Value == ABC_INIT_NONE )
-            Abc_ObjAddFanin( pFanoutNew, pNodeNew );
-    }
-
-    // update the table for each of the edges
-    Abc_ObjFaninLForEachValue( pObj, 0, Entry, i, Value )
-    {
+        Edge = Abc_ObjEdgeNum( pObj, pFanout );
+        Value = Abc_ObjFaninLDeleteLast( pFanout, Edge );
         if ( Value != ABC_INIT_NONE )
             continue;
-        if ( !stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew ) )
-            assert( 0 );
-        Edge.iLatch++;
-        if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pFanoutNew ) )
+        // value is unknown, remove it from the table
+        RetEdge.iNode  = pFanout->Id;
+        RetEdge.iEdge  = Edge;
+        RetEdge.iLatch = Abc_ObjFaninL( pFanout, Edge ); // after edge is removed
+        if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
             assert( 0 );
+        // create the fanout of the AND gate
+        Abc_ObjAddFanin( pFanoutNew, pNodeNew );
     }
-    Abc_ObjFaninLForEachValue( pObj, 1, Entry, i, Value )
-    {
-        if ( Value != ABC_INIT_NONE )
-            continue;
-        if ( !stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew ) )
-            assert( 0 );
-        Edge.iLatch++;
-        if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pFanoutNew ) )
-            assert( 0 );
-    }
-    Abc_ObjFaninLInsertFirst( pObj, 0, Init );
-    Abc_ObjFaninLInsertFirst( pObj, 1, Init );
 
-    // do not insert the don't-care node into the network
-    if ( Init == ABC_INIT_DC )
-        return 1;
+    // update the fanin edges
+    Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable );
+    Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable );
+    Abc_ObjFaninLInsertFirst( pObj, 0, ABC_INIT_NONE );
+    Abc_ObjFaninLInsertFirst( pObj, 1, ABC_INIT_NONE );
 
     // add the buffer
-    pBuf = Abc_NtkCreateNode( pNtkNew );
-    pBuf->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
-    Abc_ObjAddFanin( pNodeNew, pBuf );
+    pBuffer = Abc_NtkCreateNode( pNtkNew );
+    pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+    Abc_ObjAddFanin( pNodeNew, pBuffer );
     // point to it from the table
-    Edge.iNode = pObj->Id;
-    Edge.iEdge = 0;
-    Edge.iLatch = 0;
-    if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pBuf ) )
+    RetEdge.iNode  = pObj->Id;
+    RetEdge.iEdge  = 0;
+    RetEdge.iLatch = 0;
+    if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(RetEdge), (char *)pBuffer ) )
         assert( 0 );
 
     // add the buffer
-    pBuf = Abc_NtkCreateNode( pNtkNew );
-    pBuf->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
-    Abc_ObjAddFanin( pNodeNew, pBuf );
+    pBuffer = Abc_NtkCreateNode( pNtkNew );
+    pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+    Abc_ObjAddFanin( pNodeNew, pBuffer );
     // point to it from the table
-    Edge.iNode = pObj->Id;
-    Edge.iEdge = 1;
-    Edge.iLatch = 0;
-    if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pBuf ) )
+    RetEdge.iNode  = pObj->Id;
+    RetEdge.iEdge  = 1;
+    RetEdge.iLatch = 0;
+    if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(RetEdge), (char *)pBuffer ) )
         assert( 0 );
 
-    // check if the output value is required
-    if ( fMet0 || fMet1 )
+    // report conflict is found
+    return fMet0 && fMet1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generates the printable edge label with the initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable )
+{
+    Abc_Obj_t * pFanoutNew;
+    Abc_RetEdge_t RetEdge;
+    Abc_InitType_t Init;
+    int nLatches, i;
+
+    // get the number of latches on the edge
+    nLatches = Abc_ObjFaninL( pObj, Edge );
+    assert( nLatches <= ABC_MAX_EDGE_LATCH );
+    for ( i = nLatches - 1; i >= 0; i-- )
     {
-        // add the PO and the value
-        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
-        Vec_IntPush( vValues, fMet1 );
+        // get the value of this latch
+        Init = Abc_ObjFaninLGetInitOne( pObj, Edge, i );
+        if ( Init != ABC_INIT_NONE )
+            continue;
+        // get the retiming edge
+        RetEdge.iNode  = pObj->Id;
+        RetEdge.iEdge  = Edge;
+        RetEdge.iLatch = i;
+        // remove entry from table and add it with a different key
+        if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
+            assert( 0 );
+        RetEdge.iLatch++;
+        if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(RetEdge), (char *)pFanoutNew ) )
+            assert( 0 );
     }
-    return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sets the initial values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel )
+{
+    Abc_Obj_t * pNode;
+    stmm_generator * gen;
+    Abc_RetEdge_t RetEdge;
+    Abc_InitType_t Init;
+    int i;
+
+    i = 0;
+    stmm_foreach_item( tTable, gen, (char **)&RetEdge, NULL )
+    {
+        pNode = Abc_NtkObj( pNtk, RetEdge.iNode );
+        Init = pModel? (pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC;
+        Abc_ObjFaninLSetInitOne( pNode, RetEdge.iEdge, RetEdge.iLatch, Init );
+        i++;
+    }
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abcs/abcRetUtil.c b/src/base/abcs/abcRetUtil.c
index 52ea6446..b8f2cf25 100644
--- a/src/base/abcs/abcRetUtil.c
+++ b/src/base/abcs/abcRetUtil.c
@@ -127,12 +127,14 @@ Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, b
     Vec_Ptr_t * vMoves;
     Abc_Obj_t * pNode;
     int i, k, iNode, nLatches, Number;
+    int fChange;
     assert( Abc_NtkIsSeq( pNtk ) );
     // process the nodes
     vMoves = Vec_PtrAlloc( 100 );
     while ( Vec_IntSize(vSteps) > 0 )
     {
         iNode = 0;
+        fChange = 0;
         Vec_IntForEachEntry( vSteps, Number, i )
         {
             // get the retiming step
@@ -151,6 +153,7 @@ Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, b
                 continue;
             }
             assert( nLatches > 0 );
+            fChange = 1;
             // get the number of latches to be retimed over this node
             nLatches = ABC_MIN( nLatches, (int)RetStep.nLatches );
             // retime the latches forward
@@ -169,6 +172,11 @@ Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, b
         }
         // reduce the array
         Vec_IntShrink( vSteps, iNode );
+        if ( !fChange )
+        {
+            printf( "Warning: %d strange steps.\n", Vec_IntSize(vSteps) );
+            break;
+        }
     }
     // undo the tentative retiming
     if ( fForward )
@@ -204,6 +212,7 @@ Vec_Int_t * Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward )
     vNodes = Vec_IntAlloc( 100 );
     Vec_StrForEachEntry( vLags, Value, i )
     {
+//        assert( Value <= ABC_MAX_EDGE_LATCH );
         if ( Value < 0 && fForward )
         {
             RetStep.iNode = i;
diff --git a/src/base/abcs/abcSeq.c b/src/base/abcs/abcSeq.c
index 4a29fe0e..53e6dd90 100644
--- a/src/base/abcs/abcSeq.c
+++ b/src/base/abcs/abcSeq.c
@@ -31,7 +31,7 @@
     - 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. 
+      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.
 
@@ -92,6 +92,8 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
         Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachPo( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
+//    Abc_NtkForEachLatch( pNtk, pObj, i )
+//        Vec_PtrPush( pNtkNew->vObjs, NULL );
     // copy the PI/PO names
     Abc_NtkForEachPi( pNtk, pObj, i )
         Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pObj) );
@@ -104,6 +106,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
         if ( Abc_ObjFaninNum(pObj) != 2 )
             continue;
         Abc_NtkDupObj(pNtkNew, pObj);
+//        assert( pObj->Id == pObj->pCopy->Id );
         pObj->pCopy->fPhase = pObj->fPhase; // needed for choices
         pObj->pCopy->Level = pObj->Level; 
     }
@@ -248,7 +251,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pConst1;
-    int i, nCutNodes, nDigits;
+    int i, nCutNodes;
     unsigned Init;
     int nLatchMax = 0;
 
@@ -311,17 +314,13 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
         Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
         // the complemented edges are subsumed by the node function
     }
-    printf( "The max edge latch num = %d.\n", nLatchMax );
-    // count the number of digits in the latch names
-    nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
+//    printf( "The max edge latch num = %d.\n", nLatchMax );
     // add the latches and their names
+    Abc_NtkAddDummyLatchNames( pNtkNew );
     Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
     {
-        // add the latch to the CI/CO arrays
         Vec_PtrPush( pNtkNew->vCis, pObjNew );
         Vec_PtrPush( pNtkNew->vCos, pObjNew );
-        // create latch name
-        Abc_NtkLogicStoreName( pObjNew, Abc_ObjNameDummy("L", i, nDigits) );
     }
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
diff --git a/src/base/abcs/abcShare.c b/src/base/abcs/abcShare.c
index d74d2577..05a306b8 100644
--- a/src/base/abcs/abcShare.c
+++ b/src/base/abcs/abcShare.c
@@ -48,6 +48,10 @@ void Abc_NtkSeqShareFanouts( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj;
     int i;
     vNodes = Vec_PtrAlloc( 10 );
+    // share the PI latches
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NodeSeqShareFanouts( pObj, vNodes );
+    // share the node latches
     Abc_NtkForEachNode( pNtk, pObj, i )
         Abc_NodeSeqShareFanouts( pObj, vNodes );
     Vec_PtrFree( vNodes );
diff --git a/src/base/abcs/abcUtils.c b/src/base/abcs/abcUtils.c
index 6b42b9a9..5bd0f1da 100644
--- a/src/base/abcs/abcUtils.c
+++ b/src/base/abcs/abcUtils.c
@@ -78,6 +78,59 @@ int Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the number of latches in the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjLatchGetInitNums( Abc_Obj_t * pObj, int Edge, int * pInits )
+{
+    Abc_InitType_t Init;
+    int nLatches, i;
+    nLatches = Abc_ObjFaninL( pObj, Edge );
+    assert( nLatches <= ABC_MAX_EDGE_LATCH );
+    for ( i = 0; i < nLatches; i++ )
+    {
+        Init = Abc_ObjFaninLGetInitOne( pObj, Edge, i );
+        pInits[Init]++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of latches in the sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSeqLatchGetInitNums( Abc_Ntk_t * pNtk, int * pInits )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    for ( i = 0; i < 4; i++ )    
+        pInits[i] = 0;
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_ObjLatchGetInitNums( pObj, 0, pInits );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) > 0 )
+            Abc_ObjLatchGetInitNums( pObj, 0, pInits );
+        if ( Abc_ObjFaninNum(pObj) > 1 )
+            Abc_ObjLatchGetInitNums( pObj, 1, pInits );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Generates the printable edge label with the initial state.]
 
   Description []
diff --git a/src/base/abcs/abcs.h b/src/base/abcs/abcs.h
index 024fe57a..9e0669d4 100644
--- a/src/base/abcs/abcs.h
+++ b/src/base/abcs/abcs.h
@@ -104,6 +104,8 @@ static inline int Abc_ObjFanoutLMax( Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanout;
     int i, nLatchCur, nLatchRes;
+    if ( Abc_ObjFanoutNum(pObj) == 0 )
+        return 0;
     nLatchRes = 0;
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
@@ -120,6 +122,8 @@ static inline int Abc_ObjFanoutLMin( Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanout;
     int i, nLatchCur, nLatchRes;
+    if ( Abc_ObjFanoutNum(pObj) == 0 )
+        return 0;
     nLatchRes = ABC_INFINITY;
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
@@ -246,8 +250,8 @@ static inline void Abc_ObjRetimeForwardTry( Abc_Obj_t * pObj, int nLatches )
     // make sure it is an AND gate
     assert( Abc_ObjFaninNum(pObj) == 2 );
     // make sure it has enough latches
-    assert( Abc_ObjFaninL0(pObj) >= nLatches );
-    assert( Abc_ObjFaninL1(pObj) >= nLatches );
+//    assert( Abc_ObjFaninL0(pObj) >= nLatches );
+//    assert( Abc_ObjFaninL1(pObj) >= nLatches );
     // subtract these latches on the fanin side
     Abc_ObjAddFaninL0( pObj, -nLatches );
     Abc_ObjAddFaninL1( pObj, -nLatches );
@@ -266,7 +270,7 @@ static inline void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches )
     // subtract these latches on the fanout side
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
-        assert( Abc_ObjFanoutL(pObj, pFanout) >= nLatches );
+//        assert( Abc_ObjFanoutL(pObj, pFanout) >= nLatches );
         Abc_ObjAddFanoutL( pObj, pFanout, -nLatches );
     }
     // add these latches on the fanin size
@@ -282,7 +286,7 @@ static inline void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches )
 // iterating through the initial values of the edge
 #define Abc_ObjFaninLForEachValue( pObj, Edge, Init, i, Value ) \
     for ( i = 0, Init = Abc_ObjFaninLGetInit(pObj, Edge); \
-          i < Abc_ObjFaninL(pObj, Edge) && ((Value = ((Init >> i) & 3)), 1); i++ ) 
+          i < Abc_ObjFaninL(pObj, Edge) && ((Value = ((Init >> (2*i)) & 0x3)), 1); i++ ) 
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -311,6 +315,7 @@ extern void               Abc_NtkSeqShareFanouts( Abc_Ntk_t * pNtk );
 /*=== abcUtil.c ==============================================================*/
 extern int                Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkSeqLatchGetInitNums( Abc_Ntk_t * pNtk, int * pInits );
 extern char *             Abc_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge );
 
 ////////////////////////////////////////////////////////////////////////