Version abc51127

19 files changed, 1021 insertions, 131 deletions

diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 0211e9f8..2e596d12 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "main.h"
+#include "seq.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -151,6 +152,8 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
     {
         if ( Abc_NtkIsStrash(pNtk) ) 
             Abc_AigCheck( pNtk->pManFunc );
+        else
+            Abc_NtkSeqCheck( pNtk );
     }
     else
     {
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 158edf65..9701c0e2 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -464,6 +464,9 @@ int Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk )
     int i, LevelsMax;
     // set the traversal ID for this traversal
     Abc_NtkIncrementTravId( pNtk );
+    // set the CI levels to zero
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->Level = 0;
     // perform the traversal
     LevelsMax = 0;
     Abc_NtkForEachNode( pNtk, pNode, i )
@@ -508,7 +511,8 @@ int Abc_NtkGetLevelNum_rec( Abc_Obj_t * pNode )
         if ( pNode->Level < (unsigned)Level )
             pNode->Level = Level;
     }
-    pNode->Level++;
+    if ( Abc_ObjFaninNum(pNode) > 0 )
+        pNode->Level++;
     return pNode->Level;
 }
 
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 39184e01..6fae871d 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -330,6 +330,9 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
         Abc_AigForEachAnd( pNtk, pObj, i )
             if ( pObj->pData )
                 pObj->pCopy->pData = ((Abc_Obj_t *)pObj->pData)->pCopy;
+        // copy the cutset
+        Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+            Vec_PtrPush( pNtkNew->vCutSet, pObj->pCopy );
     }
     else
     {
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index e68a5cb2..ed76f396 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -112,7 +112,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
     Abc_NtkForEachObj( pNtk, pNode, i )
         Vec_PtrPush( vNodes, pNode );
     // write the DOT file
-    Io_WriteDot( pNtk, vNodes, NULL, FileNameDot, 0 );
+    Io_WriteDotAig( pNtk, vNodes, NULL, FileNameDot, 0 );
     Vec_PtrFree( vNodes );
 
     // visualize the file 
@@ -168,7 +168,7 @@ void Abc_NtkShowMulti( Abc_Ntk_t * pNtk )
         Vec_PtrPush( vNodes, pNode );
 
     // write the DOT file
-    Io_WriteDot( pNtk, vNodes, NULL, FileNameDot, 1 );
+    Io_WriteDotAig( pNtk, vNodes, NULL, FileNameDot, 1 );
     Vec_PtrFree( vNodes );
 
     // undo the supergates
@@ -232,7 +232,7 @@ void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax )
     // add the root node to the cone (for visualization)
     Vec_PtrPush( vCutSmall, pNode );
     // write the DOT file
-    Io_WriteDot( pNode->pNtk, vInside, vCutSmall, FileNameDot, 0 );
+    Io_WriteDotAig( pNode->pNtk, vInside, vCutSmall, FileNameDot, 0 );
     // stop the cut computation manager
     Abc_NtkManCutStop( p );
 
@@ -240,6 +240,48 @@ void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax )
     Abc_ShowFile( FileNameDot );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Visualizes AIG with choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames )
+{
+    FILE * pFile;
+    Abc_Obj_t * pNode;
+    Vec_Ptr_t * vNodes;
+    char FileNameDot[200];
+    int i;
+
+    assert( !Abc_NtkHasAig(pNtk) );
+    // create the file name
+    Abc_ShowGetFileName( pNtk->pName, FileNameDot );
+    // check that the file can be opened
+    if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+        return;
+    }
+    fclose( pFile );
+
+    // collect all nodes in the network
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        Vec_PtrPush( vNodes, pNode );
+    // write the DOT file
+    Io_WriteDotNtk( pNtk, vNodes, NULL, FileNameDot, fGateNames );
+    Vec_PtrFree( vNodes );
+
+    // visualize the file 
+    Abc_ShowFile( FileNameDot );
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0b24b3ff..db2d08a7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -41,10 +41,12 @@ static int Abc_CommandPrintLevel   ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintSymms   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintKMap    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintGates   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandShowBdd      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShowCut      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShowAig      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowNtk      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCollapse     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandStrash       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -133,10 +135,12 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Printing",     "print_supp",    Abc_CommandPrintSupport,     0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_symm",    Abc_CommandPrintSymms,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_kmap",    Abc_CommandPrintKMap,        0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_gates",   Abc_CommandPrintGates,       0 );
 
     Cmd_CommandAdd( pAbc, "Printing",     "show_bdd",      Abc_CommandShowBdd,          0 );
     Cmd_CommandAdd( pAbc, "Printing",     "show_cut",      Abc_CommandShowCut,          0 );
     Cmd_CommandAdd( pAbc, "Printing",     "show_aig",      Abc_CommandShowAig,          0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "show_ntk",      Abc_CommandShowNtk,          0 );
 
     Cmd_CommandAdd( pAbc, "Synthesis",    "collapse",      Abc_CommandCollapse,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "strash",        Abc_CommandStrash,           1 );
@@ -950,6 +954,69 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandPrintGates( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fUseLibrary;
+
+    extern void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUseLibrary = 1;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "lh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'l':
+            fUseLibrary ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkHasAig(pNtk) )
+    {
+        fprintf( pErr, "Printing gates does not work for AIGs and sequential AIGs.\n" );
+        return 1;
+    }
+
+    Abc_NtkPrintGates( pNtk, fUseLibrary );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: print_gates [-lh]\n" );
+    fprintf( pErr, "\t        prints statistics about gates used in the network\n" );
+    fprintf( pErr, "\t-l    : used library gate names (if mapped) [default = %s]\n", fUseLibrary? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -1174,9 +1241,10 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkHasAig(pNtk) )
     {
-        fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\" or \"seq\").\n" );
+        fprintf( pErr, "Visualizing networks other than AIGs can be done using command \"show_ntk\".\n" );
         return 1;
     }
+
     if ( fMulti && !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Visualizing multi-input ANDs cannot be done for sequential network (run \"unseq\").\n" );
@@ -1201,6 +1269,70 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandShowNtk( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fGateNames;
+    extern void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fGateNames = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "gh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'n':
+            fGateNames ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkHasAig(pNtk) )
+    {
+        fprintf( pErr, "Visualizing AIG can only be done using command \"show_aig\".\n" );
+        return 1;
+    }
+    Abc_NtkShow( pNtk, fGateNames );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: show_ntk [-gh]\n" );
+    fprintf( pErr, "       visualizes the network structure using DOT and GSVIEW\n" );
+#ifdef WIN32
+    fprintf( pErr, "       \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
+    fprintf( pErr, "       (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
+#endif
+    fprintf( pErr, "\t-g    : toggles printing gate names for mapped network [default = %s].\n", fGateNames? "yes": "no" );  
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -4056,6 +4188,12 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Cannot map a sequential AIG.\n" );
+        return 1;
+    }
+
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         pNtk = Abc_NtkStrash( pNtk, 0, 0 );
@@ -4364,6 +4502,12 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Cannot FPGA map a sequential AIG.\n" );
+        return 1;
+    }
+
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         // strash and balance the network
@@ -4741,7 +4885,7 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c;//, nLoops;
+    int c;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -4772,18 +4916,18 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( Abc_NtkLatchNum(pNtk) == 0 )
+    {
+        fprintf( pErr, "The network has no latches.\n" );
+        return 0;
+    }
+
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Conversion to sequential AIG works only for combinational AIGs (run \"strash\").\n" );
         return 1;
     }
 
-//    if ( nLoops = Abc_NtkCountSelfFeedLatches(pNtk) )
-//    {
-//        fprintf( pErr, "Cannot create sequential AIG because the network contains %d self-feeding latches.\n", nLoops );
-//        return 0;
-//    }
-
     // get the new network
     pNtkRes = Abc_NtkAigToSeq( pNtk );
     if ( pNtkRes == NULL )
@@ -4890,13 +5034,12 @@ usage:
 int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;
-    int c;
+    Abc_Ntk_t * pNtk, * pNtkRes, * pNtkTemp;
+    int c, nMaxIters;
     int fForward;
     int fBackward;
     int fInitial;
     int fVerbose;
-    int nLoops;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -4907,11 +5050,23 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     fBackward = 0;
     fInitial  = 1;
     fVerbose  = 0;
+    nMaxIters = 15;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "fbivh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "Ifbivh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'I':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nMaxIters = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nMaxIters < 0 ) 
+                goto usage;
+            break;
         case 'f':
             fForward ^= 1;
             break;
@@ -4937,34 +5092,59 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsSeq(pNtk) )
+    if ( !Abc_NtkIsSeq(pNtk) && Abc_NtkLatchNum(pNtk) == 0 )
     {
-        fprintf( pErr, "Retiming works only for sequential AIG (run \"seq\").\n" );
+        fprintf( pErr, "The network has no latches. Retiming is not performed.\n" );
         return 0;
     }
 
-    if ( nLoops = Abc_NtkCountSelfFeedLatches(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
     {
-        fprintf( pErr, "Cannot retime because the network contains %d self-feeding latches.\n", nLoops );
-        return 0;
+        if ( Abc_NtkIsStrash(pNtk) )
+            pNtkRes = Abc_NtkAigToSeq(pNtk);
+        else
+        {
+            if ( Abc_NtkGetChoiceNum(pNtk) )
+            {
+                fprintf( pErr, "Currently cannot retime networks with choice nodes.\n" );
+                return 0;
+            }
+            pNtkRes = Abc_NtkDup(pNtk);
+        }
+        // retime the network
+        if ( fForward )
+            Seq_NtkSeqRetimeForward( pNtkRes, fInitial, fVerbose );
+        else if ( fBackward )
+            Seq_NtkSeqRetimeBackward( pNtkRes, fInitial, fVerbose );
+        else
+            Seq_NtkSeqRetimeDelay( pNtkRes, nMaxIters, fInitial, fVerbose );
+        // convert from the sequential AIG
+        if ( Abc_NtkIsStrash(pNtk) )
+        {
+            pNtkRes = Abc_NtkSeqToLogicSop( pNtkTemp = pNtkRes );
+            Abc_NtkDelete( pNtkTemp );
+        }
     }
-
-    // get the new network
-    if ( fForward )
-        Seq_NtkSeqRetimeForward( pNtk, fInitial, fVerbose );
-    else if ( fBackward )
-        Seq_NtkSeqRetimeBackward( pNtk, fInitial, fVerbose );
     else
-        Seq_NtkSeqRetimeDelay( pNtk, fInitial, fVerbose );
+        pNtkRes = Seq_NtkRetime( pNtk, nMaxIters, fInitial, fVerbose );
+    // replace the network
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Retiming has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: retime [-fbih]\n" );
-    fprintf( pErr, "\t        retimes sequential AIG (default is Pan's delay-optimal retiming)\n" );
-    fprintf( pErr, "\t-f    : toggle forward retiming [default = %s]\n", fForward? "yes": "no" );
-    fprintf( pErr, "\t-b    : toggle backward retiming [default = %s]\n", fBackward? "yes": "no" );
-    fprintf( pErr, "\t-i    : toggle computation of initial state [default = %s]\n", fInitial? "yes": "no" );
-    fprintf( pErr, "\t-h    : print the command usage\n");
+    fprintf( pErr, "usage: retime [-I num] [-fbih]\n" );
+    fprintf( pErr, "\t         retimes the current network using Pan's delay-optimal retiming\n" );
+    fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters );
+    fprintf( pErr, "\t-f     : toggle forward retiming (for AIGs) [default = %s]\n", fForward? "yes": "no" );
+    fprintf( pErr, "\t-b     : toggle backward retiming (for AIGs) [default = %s]\n", fBackward? "yes": "no" );
+    fprintf( pErr, "\t-i     : toggle computation of 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/abcPrint.c b/src/base/abci/abcPrint.c
index e96825bb..4b4c01ae 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -20,6 +20,8 @@
 
 #include "abc.h"
 #include "dec.h"
+#include "main.h"
+#include "mio.h"
 #include "seq.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -524,6 +526,96 @@ void Abc_NodePrintKMap( Abc_Obj_t * pNode, int fUseRealNames )
 
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints statistics about gates used in the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary )
+{
+    Abc_Obj_t * pObj;
+    int fHasBdds, i;
+    int CountConst, CountBuf, CountInv, CountAnd, CountOr, CountOther, CounterTotal;
+    char * pSop;
+
+    if ( fUseLibrary && Abc_NtkHasMapping(pNtk) )
+    {
+        stmm_table * tTable;
+        stmm_generator * gen;
+        char * pName;
+        int * pCounter, Counter;
+        double Area, AreaTotal;
+
+        // count the gates by name
+        CounterTotal = 0;
+        tTable = stmm_init_table(strcmp, stmm_strhash);
+        Abc_NtkForEachNode( pNtk, pObj, i )
+        {
+            if ( i == 0 ) continue;
+            if ( !stmm_find_or_add( tTable, Mio_GateReadName(pObj->pData), (char ***)&pCounter ) )
+                *pCounter = 0;
+            (*pCounter)++;
+            CounterTotal++;
+        }
+        // print the gates
+        AreaTotal = Abc_NtkGetMappedArea(pNtk);
+        stmm_foreach_item( tTable, gen, (char **)&pName, (char **)&Counter )
+        {
+            Area = Counter * Mio_GateReadArea(Mio_LibraryReadGateByName(pNtk->pManFunc,pName));
+            printf( "%-12s = %8d   %10.2f    %6.2f %%\n", pName, Counter, Area, 100.0 * Area / AreaTotal );
+        }
+        printf( "%-12s = %8d   %10.2f    %6.2f %%\n", "TOTAL", CounterTotal, AreaTotal, 100.0 );
+        stmm_free_table( tTable );
+        return;
+    }
+
+    // transform logic functions from BDD to SOP
+    if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
+        Abc_NtkBddToSop(pNtk);
+
+    // get hold of the SOP of the node
+    CountConst = CountBuf = CountInv = CountAnd = CountOr = CountOther = CounterTotal = 0;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( i == 0 ) continue;
+        if ( Abc_NtkHasMapping(pNtk) )
+            pSop = Mio_GateReadSop(pObj->pData);
+        else
+            pSop = pObj->pData;
+        // collect the stats
+        if ( Abc_SopIsConst0(pSop) || Abc_SopIsConst1(pSop) )
+            CountConst++;
+        else if ( Abc_SopIsBuf(pSop) )
+            CountBuf++;
+        else if ( Abc_SopIsInv(pSop) )
+            CountInv++;
+        else if ( !Abc_SopIsComplement(pSop) && Abc_SopIsAndType(pSop) ||  Abc_SopIsComplement(pSop) && Abc_SopIsOrType(pSop) )
+            CountAnd++;
+        else if (  Abc_SopIsComplement(pSop) && Abc_SopIsAndType(pSop) || !Abc_SopIsComplement(pSop) && Abc_SopIsOrType(pSop) )
+            CountOr++;
+        else
+            CountOther++;
+        CounterTotal++;
+    }
+    printf( "Const        = %8d    %6.2f %%\n", CountConst  ,  100.0 * CountConst   / CounterTotal );
+    printf( "Buffer       = %8d    %6.2f %%\n", CountBuf    ,  100.0 * CountBuf     / CounterTotal );
+    printf( "Inverter     = %8d    %6.2f %%\n", CountInv    ,  100.0 * CountInv     / CounterTotal );
+    printf( "And          = %8d    %6.2f %%\n", CountAnd    ,  100.0 * CountAnd     / CounterTotal );
+    printf( "Or           = %8d    %6.2f %%\n", CountOr     ,  100.0 * CountOr      / CounterTotal );
+    printf( "Other        = %8d    %6.2f %%\n", CountOther  ,  100.0 * CountOther   / CounterTotal );
+    printf( "TOTAL        = %8d    %6.2f %%\n", CounterTotal,  100.0 * CounterTotal / CounterTotal );
+
+    // convert the network back into BDDs if this is how it was
+    if ( fHasBdds )
+        Abc_NtkSopToBdd(pNtk);
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 9fe5bea0..1841ba8c 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -449,6 +449,7 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode;
     int i, Counter;
+    assert( !Abc_NtkHasAig(pNtk) );
     // mark the nodes reachable from the POs
     vNodes = Abc_NtkDfs( pNtk, 0 );
     for ( i = 0; i < vNodes->nSize; i++ )
@@ -458,7 +459,7 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
     }
     Vec_PtrFree( vNodes );
     // if it is an AIG, also mark the constant 1 node
-    if ( Abc_NtkIsStrash(pNtk) )
+    if ( Abc_NtkConst1(pNtk) )
         Abc_NtkConst1(pNtk)->fMarkA = 1;
     // remove the non-marked nodes
     Counter = 0;
@@ -514,7 +515,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
     {
         // sweep constants and single-input nodes
         Abc_NtkForEachNode( pNtk, pNode, i )
-            if ( Abc_ObjFaninNum(pNode) < 2 )
+            if ( i && Abc_ObjFaninNum(pNode) < 2 )
                 Abc_NodeSweep( pNode, fVerbose );
         // make the network minimum base
         Abc_NtkRemoveDupFanins(pNtk);
diff --git a/src/base/io/io.c b/src/base/io/io.c
index e5f8b9a1..1330d114 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1101,7 +1101,7 @@ int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv )
     FileName = argv[util_optind];
     // write the file
     vNodes = Abc_NtkCollectObjects( pAbc->pNtkCur );
-    Io_WriteDot( pAbc->pNtkCur, vNodes, NULL, FileName, 0 );
+    Io_WriteDotAig( pAbc->pNtkCur, vNodes, NULL, FileName, 0 );
     Vec_PtrFree( vNodes );
     return 0;
 
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 21bb9214..cb8678b3 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -80,7 +80,8 @@ extern int                Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteCnf.c ==========================================================*/
 extern int                Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteDot.c ==========================================================*/
-extern void               Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fMulti );
+extern void               Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fMulti );
+extern void               Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames );
 /*=== abcWriteEqn.c ==========================================================*/
 extern void               Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName );
 /*=== abcWriteGml.c ==========================================================*/
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 7bece42e..d00b265a 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -25,6 +25,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static char * Abc_NtkPrintSop( char * pSop );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -41,13 +43,15 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fMulti )
+void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fMulti )
 {
     FILE * pFile;
     Abc_Obj_t * pNode, * pTemp, * pPrev;
     int LevelMin, LevelMax, fHasCos, Level, i;
     int Limit = 300;
 
+    assert( Abc_NtkHasAig(pNtk) );
+
     if ( vNodes->nSize < 1 )
     {
         printf( "The set has no nodes. DOT file is not written.\n" );
@@ -103,7 +107,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
     }
 
     // write the DOT header
-    fprintf( pFile, "# %s\n",  "AIG generated by ABC" );
+    fprintf( pFile, "# %s\n",  "AIG structure generated by ABC" );
     fprintf( pFile, "\n" );
     fprintf( pFile, "digraph AIG {\n" );
     fprintf( pFile, "size = \"7.5,10\";\n" );
@@ -159,7 +163,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
     fprintf( pFile, "          fontsize=20,\n" );
     fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
     fprintf( pFile, "          label=\"" );
-    fprintf( pFile, "%s", "AIG generated by ABC" );
+    fprintf( pFile, "%s", "AIG structure visualized by ABC" );
     fprintf( pFile, "\\n" );
     fprintf( pFile, "Benchmark \\\"%s\\\". ", pNtk->pName );
     fprintf( pFile, "Time was %s. ",  Extra_TimeStamp() );
@@ -364,6 +368,339 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
             pNode->fMarkB = 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the graph structure of network for DOT.]
+
+  Description [Useful for graph visualization using tools such as GraphViz: 
+  http://www.graphviz.org/]
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames )
+{
+    FILE * pFile;
+    Abc_Obj_t * pNode, * pFanin;
+    char * pSopString;
+    int LevelMin, LevelMax, fHasCos, Level, i, k, fHasBdds;
+    int Limit = 300;
+
+    assert( !Abc_NtkHasAig(pNtk) );
+
+    if ( vNodes->nSize < 1 )
+    {
+        printf( "The set has no nodes. DOT file is not written.\n" );
+        return;
+    }
+
+    if ( vNodes->nSize > Limit )
+    {
+        printf( "The set has more than %d nodes. DOT file is not written.\n", Limit );
+        return;
+    }
+
+    // start the stream
+    if ( (pFile = fopen( pFileName, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
+        return;
+    }
+
+    // transform logic functions from BDD to SOP
+    if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
+        Abc_NtkBddToSop(pNtk);
+
+    // mark the nodes from the set
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+        pNode->fMarkC = 1;
+    if ( vNodesShow )
+        Vec_PtrForEachEntry( vNodesShow, pNode, i )
+            pNode->fMarkB = 1;
+
+    // get the levels of nodes
+    Abc_NtkGetLevelNum( pNtk );
+
+    // find the largest and the smallest levels
+    LevelMin = 10000;
+    LevelMax = -1;
+    fHasCos  = 0;
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( Abc_ObjIsCo(pNode) )
+        {
+            fHasCos = 1;
+            continue;
+        }
+        if ( LevelMin > (int)pNode->Level )
+            LevelMin = pNode->Level;
+        if ( LevelMax < (int)pNode->Level )
+            LevelMax = pNode->Level;
+    }
+
+    // set the level of the CO nodes
+    if ( fHasCos )
+    {
+        LevelMax++;
+        Vec_PtrForEachEntry( vNodes, pNode, i )
+        {
+            if ( Abc_ObjIsCo(pNode) )
+                pNode->Level = LevelMax;
+        }
+    }
+
+    // write the DOT header
+    fprintf( pFile, "# %s\n",  "Network structure generated by ABC" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "digraph AIG {\n" );
+    fprintf( pFile, "size = \"7.5,10\";\n" );
+//  fprintf( pFile, "ranksep = 0.5;\n" );
+//  fprintf( pFile, "nodesep = 0.5;\n" );
+    fprintf( pFile, "center = true;\n" );
+//  fprintf( pFile, "orientation = landscape;\n" );
+//  fprintf( pFile, "edge [fontsize = 10];\n" );
+//  fprintf( pFile, "edge [dir = none];\n" );
+    fprintf( pFile, "edge [dir = back];\n" );
+    fprintf( pFile, "\n" );
+
+    // labels on the left of the picture
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  node [shape = plaintext];\n" );
+    fprintf( pFile, "  edge [style = invis];\n" );
+    fprintf( pFile, "  LevelTitle1 [label=\"\"];\n" );
+    fprintf( pFile, "  LevelTitle2 [label=\"\"];\n" );
+    // generate node names with labels
+    for ( Level = LevelMax; Level >= LevelMin; Level-- )
+    {
+        // the visible node name
+        fprintf( pFile, "  Level%d", Level );
+        fprintf( pFile, " [label = " );
+        // label name
+        fprintf( pFile, "\"" );
+        fprintf( pFile, "\"" );
+        fprintf( pFile, "];\n" );
+    }
+
+    // genetate the sequence of visible/invisible nodes to mark levels
+    fprintf( pFile, "  LevelTitle1 ->  LevelTitle2 ->" );
+    for ( Level = LevelMax; Level >= LevelMin; Level-- )
+    {
+        // the visible node name
+        fprintf( pFile, "  Level%d",  Level );
+        // the connector
+        if ( Level != LevelMin )
+            fprintf( pFile, " ->" );
+        else
+            fprintf( pFile, ";" );
+    }
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate title box on top
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  rank = same;\n" );
+    fprintf( pFile, "  LevelTitle1;\n" );
+    fprintf( pFile, "  title1 [shape=plaintext,\n" );
+    fprintf( pFile, "          fontsize=20,\n" );
+    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
+    fprintf( pFile, "          label=\"" );
+    fprintf( pFile, "%s", "Network structure visualized by ABC" );
+    fprintf( pFile, "\\n" );
+    fprintf( pFile, "Benchmark \\\"%s\\\". ", pNtk->pName );
+    fprintf( pFile, "Time was %s. ",  Extra_TimeStamp() );
+    fprintf( pFile, "\"\n" );
+    fprintf( pFile, "         ];\n" );
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate statistics box
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  rank = same;\n" );
+    fprintf( pFile, "  LevelTitle2;\n" );
+    fprintf( pFile, "  title2 [shape=plaintext,\n" );
+    fprintf( pFile, "          fontsize=18,\n" );
+    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
+    fprintf( pFile, "          label=\"" );
+    fprintf( pFile, "The set contains %d nodes and spans %d levels.", vNodes->nSize, LevelMax - LevelMin + 1 );
+    fprintf( pFile, "\\n" );
+    fprintf( pFile, "\"\n" );
+    fprintf( pFile, "         ];\n" );
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate the POs
+    if ( fHasCos )
+    {
+        fprintf( pFile, "{\n" );
+        fprintf( pFile, "  rank = same;\n" );
+        // the labeling node of this level
+        fprintf( pFile, "  Level%d;\n",  LevelMax );
+        // generate the PO nodes
+        Vec_PtrForEachEntry( vNodes, pNode, i )
+        {
+            if ( !Abc_ObjIsCo(pNode) )
+                continue;
+            fprintf( pFile, "  Node%d%s [label = \"%s%s\"", pNode->Id, 
+                (Abc_ObjIsLatch(pNode)? "_in":""), Abc_ObjName(pNode), (Abc_ObjIsLatch(pNode)? "_in":"") );
+            fprintf( pFile, ", shape = %s", (Abc_ObjIsLatch(pNode)? "box":"invtriangle") );
+            if ( pNode->fMarkB )
+                fprintf( pFile, ", style = filled" );
+            fprintf( pFile, ", color = coral, fillcolor = coral" );
+            fprintf( pFile, "];\n" );
+        }
+        fprintf( pFile, "}" );
+        fprintf( pFile, "\n" );
+        fprintf( pFile, "\n" );
+    }
+
+    // generate nodes of each rank
+    for ( Level = LevelMax - fHasCos; Level >= LevelMin && Level > 0; Level-- )
+    {
+        fprintf( pFile, "{\n" );
+        fprintf( pFile, "  rank = same;\n" );
+        // the labeling node of this level
+        fprintf( pFile, "  Level%d;\n",  Level );
+        Vec_PtrForEachEntry( vNodes, pNode, i )
+        {
+            if ( (int)pNode->Level != Level )
+                continue;
+//            fprintf( pFile, "  Node%d [label = \"%d\"", pNode->Id, pNode->Id );
+            if ( Abc_NtkHasMapping(pNtk) && fGateNames )
+                pSopString = Mio_GateReadName(pNode->pData);
+            else if ( Abc_NtkHasMapping(pNtk) )
+                pSopString = Abc_NtkPrintSop(Mio_GateReadSop(pNode->pData));
+            else
+                pSopString = Abc_NtkPrintSop(pNode->pData);
+            fprintf( pFile, "  Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString );
+
+            fprintf( pFile, ", shape = ellipse" );
+            if ( pNode->fMarkB )
+                fprintf( pFile, ", style = filled" );
+            fprintf( pFile, "];\n" );
+        }
+        fprintf( pFile, "}" );
+        fprintf( pFile, "\n" );
+        fprintf( pFile, "\n" );
+    }
+
+    // generate the PI nodes if any
+    if ( LevelMin == 0 )
+    {
+        fprintf( pFile, "{\n" );
+        fprintf( pFile, "  rank = same;\n" );
+        // the labeling node of this level
+        fprintf( pFile, "  Level%d;\n",  LevelMin );
+        // generat the PO nodes
+        Vec_PtrForEachEntry( vNodes, pNode, i )
+        {
+            if ( !Abc_ObjIsCi(pNode) )
+            {
+                // check if the costant node is present
+                if ( Abc_ObjFaninNum(pNode) == 0 && Abc_ObjFanoutNum(pNode) > 0 )
+                {
+                    fprintf( pFile, "  Node%d [label = \"Const1\"", pNode->Id );
+                    fprintf( pFile, ", shape = ellipse" );
+                    if ( pNode->fMarkB )
+                        fprintf( pFile, ", style = filled" );
+                    fprintf( pFile, ", color = coral, fillcolor = coral" );
+                    fprintf( pFile, "];\n" );
+                }
+                continue;
+            }
+            fprintf( pFile, "  Node%d%s [label = \"%s%s\"", pNode->Id, 
+                (Abc_ObjIsLatch(pNode)? "_out":""), Abc_ObjName(pNode), (Abc_ObjIsLatch(pNode)? "_out":"") );
+            fprintf( pFile, ", shape = %s", (Abc_ObjIsLatch(pNode)? "box":"triangle") );
+            if ( pNode->fMarkB )
+                fprintf( pFile, ", style = filled" );
+            fprintf( pFile, ", color = coral, fillcolor = coral" );
+            fprintf( pFile, "];\n" );
+        }
+        fprintf( pFile, "}" );
+        fprintf( pFile, "\n" );
+        fprintf( pFile, "\n" );
+    }
+
+    // generate invisible edges from the square down
+    fprintf( pFile, "title1 -> title2 [style = invis];\n" );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( (int)pNode->Level != LevelMax )
+            continue;
+        fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id, 
+            (Abc_ObjIsLatch(pNode)? "_in":"") );
+    }
+
+    // generate edges
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+        {
+            if ( !Abc_ObjFanin0(pNode)->fMarkC )
+                continue;
+            // generate the edge from this node to the next
+            fprintf( pFile, "Node%d%s",  pNode->Id, (Abc_ObjIsLatch(pNode)? "_in":"") );
+            fprintf( pFile, " -> " );
+            fprintf( pFile, "Node%d%s",  Abc_ObjFaninId(pNode,k), (Abc_ObjIsLatch(Abc_ObjFanin(pNode,k))? "_out":"") );
+            fprintf( pFile, " [style = bold" );
+            fprintf( pFile, ", label = \"%c\"", 'a' + k );
+            fprintf( pFile, "]" );
+            fprintf( pFile, ";\n" );
+        }
+    }
+
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+
+    // unmark the nodes from the set
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+        pNode->fMarkC = 0;
+    if ( vNodesShow )
+        Vec_PtrForEachEntry( vNodesShow, pNode, i )
+            pNode->fMarkB = 0;
+
+    // convert the network back into BDDs if this is how it was
+    if ( fHasBdds )
+        Abc_NtkSopToBdd(pNtk);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the printable SOP form.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_NtkPrintSop( char * pSop ) 
+{
+    static char Buffer[1000];
+    char * pGet, * pSet;
+    pSet = Buffer;
+    for ( pGet = pSop; *pGet; pGet++ )
+    {        
+        if ( *pGet == '\n' )
+        {
+            *pSet++ = '\\';
+            *pSet++ = 'n';
+        }
+        else
+            *pSet++ = *pGet;
+    }
+    *(pSet-2) = 0;
+    return Buffer;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seq.h b/src/base/seq/seq.h
index 368f8afc..a644303f 100644
--- a/src/base/seq/seq.h
+++ b/src/base/seq/seq.h
@@ -44,7 +44,7 @@ typedef struct Abc_Seq_t_  Abc_Seq_t;
 ////////////////////////////////////////////////////////////////////////
 
 /*=== seqAigCore.c ===========================================================*/
-extern void            Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fInitial, int fVerbose );
+extern void            Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose );
 extern void            Seq_NtkSeqRetimeForward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose );
 extern void            Seq_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose );
 /*=== seqFpgaCore.c ===============================================================*/
@@ -52,7 +52,7 @@ extern Abc_Ntk_t *     Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int nMaxIters, in
 /*=== seqMapCore.c ===============================================================*/
 extern Abc_Ntk_t *     Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
 /*=== seqRetCore.c ===========================================================*/
-extern Abc_Ntk_t *     Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
+extern Abc_Ntk_t *     Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose );
 /*=== seqLatch.c ===============================================================*/
 extern void            Seq_NodeDupLats( Abc_Obj_t * pObjNew, Abc_Obj_t * pObj, int Edge );
 extern int             Seq_NodeCompareLats( Abc_Obj_t * pObj1, int Edge1, Abc_Obj_t * pObj2, int Edge2 );
@@ -63,10 +63,12 @@ extern void            Seq_Delete( Abc_Seq_t * p );
 /*=== abcSeq.c ===============================================================*/
 extern Abc_Ntk_t *     Abc_NtkAigToSeq( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *     Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk );
+extern bool            Abc_NtkSeqCheck( Abc_Ntk_t * pNtk ); 
 /*=== seqShare.c =============================================================*/
 extern void            Seq_NtkShareFanouts( Abc_Ntk_t * pNtk );
 extern void            Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk );
 extern void            Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds );
+extern void            Seq_NtkShareLatchesClean( Abc_Ntk_t * pNtk );
 /*=== seqUtil.c ==============================================================*/
 extern char *          Seq_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge );
 extern void            Seq_NtkLatchSetValues( Abc_Ntk_t * pNtk, Abc_InitType_t Init );
diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c
index d347d53e..5dca2e86 100644
--- a/src/base/seq/seqAigCore.c
+++ b/src/base/seq/seqAigCore.c
@@ -65,13 +65,14 @@ static void        Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches );
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fInitial, int fVerbose )
+void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
     int RetValue;
     if ( !fInitial )
         Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC );
     // get the retiming lags
+    p->nMaxIters = nMaxIters;
     Seq_AigRetimeDelayLags( pNtk, fVerbose );
     // implement this retiming
     RetValue = Seq_NtkImplementRetiming( pNtk, p->vLags, fVerbose );
@@ -490,31 +491,33 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t
         {
             Edge = 0;
             Value = Seq_NodeDeleteLast( pFanout, Edge );
-            if ( Value != ABC_INIT_NONE )
-                continue;
-            // value is unknown, remove it from the table
-            RetEdge.iNode  = pFanout->Id;
-            RetEdge.iEdge  = Edge;
-            RetEdge.iLatch = Seq_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 );
+            if ( Value == ABC_INIT_NONE )
+            {
+                // value is unknown, remove it from the table
+                RetEdge.iNode  = pFanout->Id;
+                RetEdge.iEdge  = Edge;
+                RetEdge.iLatch = Seq_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 );
+            }
         }
         if ( Abc_ObjFaninId1(pFanout) == pObj->Id )
         {
             Edge = 1;
             Value = Seq_NodeDeleteLast( pFanout, Edge );
-            if ( Value != ABC_INIT_NONE )
-                continue;
-            // value is unknown, remove it from the table
-            RetEdge.iNode  = pFanout->Id;
-            RetEdge.iEdge  = Edge;
-            RetEdge.iLatch = Seq_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 );
+            if ( Value == ABC_INIT_NONE )
+            {
+                // value is unknown, remove it from the table
+                RetEdge.iNode  = pFanout->Id;
+                RetEdge.iEdge  = Edge;
+                RetEdge.iLatch = Seq_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 );
+            }
         }
     }
     // clean the label
diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c
index d293b946..d94e8e82 100644
--- a/src/base/seq/seqCreate.c
+++ b/src/base/seq/seqCreate.c
@@ -164,7 +164,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
     Seq_NtkLatchGetEqualFaninNum( pNtkNew );
 
     // copy EXDC and check correctness
-    if ( pNtkNew->pExdc )
+    if ( pNtk->pExdc )
         fprintf( stdout, "Warning: EXDC is not copied when converting to sequential AIG.\n" );
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkAigToSeq(): Network check has failed.\n" );
@@ -292,6 +292,8 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
         pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
         Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
     }
+    // clean the latch pointers
+    Seq_NtkShareLatchesClean( pNtk );
 
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkNew );
@@ -408,6 +410,73 @@ Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, Seq_Lat
     return pLatch;    
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Makes sure that every node in the table is in the network and vice versa.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkSeqCheck( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, nFanins;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+        {
+            if ( pObj != Abc_NtkConst1(pNtk) )
+            {
+                printf( "Abc_SeqCheck: The AIG has non-standard constant nodes.\n" );
+                return 0;
+            }
+            continue;
+        }
+        if ( nFanins == 1 )
+        {
+            printf( "Abc_SeqCheck: The AIG has single input nodes.\n" );
+            return 0;
+        }
+        if ( nFanins > 2 )
+        {
+            printf( "Abc_SeqCheck: The AIG has non-standard nodes.\n" );
+            return 0;
+        }
+    }
+    // check the correctness of the internal representation of the initial states
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+            continue;
+        if ( nFanins == 1 )
+        {
+            if ( Seq_NodeCountLats(pObj, 0) != Seq_ObjFaninL0(pObj) )
+            {
+                printf( "Abc_SeqCheck: Node %d has mismatch in the number of latches.\n", Abc_ObjName(pObj) );
+                return 0;
+            }
+        }
+        // look at both inputs
+        if ( Seq_NodeCountLats(pObj, 0) != Seq_ObjFaninL0(pObj) )
+        {
+            printf( "Abc_SeqCheck: The first fanin of node %d has mismatch in the number of latches.\n", Abc_ObjName(pObj) );
+            return 0;
+        }
+        if ( Seq_NodeCountLats(pObj, 1) != Seq_ObjFaninL1(pObj) )
+        {
+            printf( "Abc_SeqCheck: The second fanin of node %d has mismatch in the number of latches.\n", Abc_ObjName(pObj) );
+            return 0;
+        }
+    }
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqInt.h b/src/base/seq/seqInt.h
index 4503cef8..c0f3e907 100644
--- a/src/base/seq/seqInt.h
+++ b/src/base/seq/seqInt.h
@@ -195,7 +195,8 @@ static inline void           Seq_NodeRecycleLat( Abc_Obj_t * pObj, Seq_Lat_t * p
 static inline Seq_Lat_t *    Seq_NodeGetLatFirst( Abc_Obj_t * pObj, int Edge )               { return Seq_NodeGetRing(pObj, Edge);                      }
 static inline Seq_Lat_t *    Seq_NodeGetLatLast( Abc_Obj_t * pObj, int Edge )                { return Seq_LatPrev( Seq_NodeGetRing(pObj, Edge) );       }
 static inline Seq_Lat_t *    Seq_NodeGetLat( Abc_Obj_t * pObj, int Edge, int iLat )          { int c; Seq_Lat_t * pLat = Seq_NodeGetRing(pObj, Edge); for ( c = 0; c != iLat; c++ ) pLat = pLat->pNext; return pLat; }
-static inline int            Seq_NodeCountLats( Abc_Obj_t * pObj, int Edge )                 { int c; Seq_Lat_t * pLat, * pRing = Seq_NodeGetRing(pObj, Edge); if ( pRing == NULL ) return 0; for ( c = 0, pLat = pRing; !c || pLat != pRing; c++ )      pLat = pLat->pNext; return c; }
+static inline int            Seq_NodeCountLats( Abc_Obj_t * pObj, int Edge )                 { int c; Seq_Lat_t * pLat, * pRing = Seq_NodeGetRing(pObj, Edge); if ( pRing == NULL ) return 0; for ( c = 0, pLat = pRing; !c || pLat != pRing; c++ )  pLat = pLat->pNext; return c; }
+static inline void           Seq_NodeCleanLats( Abc_Obj_t * pObj, int Edge )                 { int c; Seq_Lat_t * pLat, * pRing = Seq_NodeGetRing(pObj, Edge); if ( pRing == NULL ) return  ; for ( c = 0, pLat = pRing; !c || pLat != pRing; c++ )  pLat->pLatch = NULL, pLat = pLat->pNext; return;  }
 
 // getting/setting initial states of the latches
 static inline Abc_InitType_t Seq_NodeGetInitOne( Abc_Obj_t * pObj, int Edge, int iLat )      { return Seq_LatInit( Seq_NodeGetLat(pObj, Edge, iLat) );  }
diff --git a/src/base/seq/seqLatch.c b/src/base/seq/seqLatch.c
index 8f861004..cb3e1e36 100644
--- a/src/base/seq/seqLatch.c
+++ b/src/base/seq/seqLatch.c
@@ -61,6 +61,7 @@ void Seq_NodeInsertFirst( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )
     }
     Seq_LatSetInit( pLat, Init );
     Seq_ObjAddFaninL( pObj, Edge, 1 );
+    assert( pLat->pLatch == NULL );
 }
 
 /**Function*************************************************************
diff --git a/src/base/seq/seqMapIter.c b/src/base/seq/seqMapIter.c
index 5a8b57bd..284fd27d 100644
--- a/src/base/seq/seqMapIter.c
+++ b/src/base/seq/seqMapIter.c
@@ -207,8 +207,8 @@ int Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
     char * pReason = "";
 
     // set l-values of all nodes to be minus infinity
-    Vec_IntFill( p->vLValues,  p->nSize, -ABC_INFINITY );
-    Vec_IntFill( p->vLValuesN, p->nSize, -ABC_INFINITY );
+    Vec_IntFill( p->vLValues,  p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
+    Vec_IntFill( p->vLValuesN, p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
     Vec_StrFill( p->vUses,     p->nSize, 0             );
 
     // set l-values of constants and PIs
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index c746f9a4..154f8dad 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -25,11 +25,12 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose );
 static Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
 static void        Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init );
-static Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk );
-
+static Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq );
+static Abc_Obj_t * Seq_EdgeReconstruct_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode );
+static Abc_Obj_t * Seq_EdgeReconstructPO( Abc_Obj_t * pNode );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -46,25 +47,31 @@ static Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pN
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
+Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose )
 {
     Abc_Seq_t * p;
-    Abc_Ntk_t * pNtkAig, * pNtkNew;
+    Abc_Ntk_t * pNtkSeq, * pNtkNew;
     int RetValue;
     assert( !Abc_NtkHasAig(pNtk) );
     // derive the isomorphic seq AIG
-    pNtkAig = Seq_NtkRetimeDerive( pNtk );
-    p = pNtkAig->pManFunc;
+    pNtkSeq = Seq_NtkRetimeDerive( pNtk, fVerbose );
+    p = pNtkSeq->pManFunc;
     p->nMaxIters = nMaxIters;
+
+    if ( !fInitial )
+        Seq_NtkLatchSetValues( pNtkSeq, ABC_INIT_DC );
     // find the best mapping and retiming 
-    Seq_NtkRetimeDelayLags( pNtk, pNtkAig, fVerbose );
+    Seq_NtkRetimeDelayLags( pNtk, pNtkSeq, fVerbose );
     // implement the retiming
-    RetValue = Seq_NtkImplementRetiming( pNtkAig, p->vLags, fVerbose );
+    RetValue = Seq_NtkImplementRetiming( pNtkSeq, p->vLags, fVerbose );
     if ( RetValue == 0 )
         printf( "Retiming completed but initial state computation has failed.\n" );
+
+//return pNtkSeq;
+
     // create the final mapped network
-    pNtkNew = Seq_NtkRetimeReconstruct( pNtk, pNtkAig );
-    Abc_NtkDelete( pNtkAig );
+    pNtkNew = Seq_NtkRetimeReconstruct( pNtk, pNtkSeq );
+    Abc_NtkDelete( pNtkSeq );
     return pNtkNew;
 }
 
@@ -79,12 +86,12 @@ Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Abc_Seq_t * p;
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pObj, * pFanin, * pFanout;
-    int i, k, RetValue;
+    int i, k, RetValue, fHasBdds;
     char * pSop;
 
     // make sure it is an AIG without self-feeding latches
@@ -93,35 +100,52 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
         printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
     assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
 
-    if ( Abc_NtkIsBddLogic(pNtk) )
+    // remove the dangling nodes
+    Abc_NtkCleanup( pNtk, fVerbose );
+
+    // transform logic functions from BDD to SOP
+    if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
         Abc_NtkBddToSop(pNtk);
 
     // start the network
     pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );
-
     // duplicate the name and the spec
     pNtkNew->pName = util_strsav(pNtk->pName);
     pNtkNew->pSpec = util_strsav(pNtk->pSpec);
+
     // map the constant nodes
     Abc_NtkCleanCopy( pNtk );
     // clone the PIs/POs/latches
     Abc_NtkForEachPi( pNtk, pObj, i )
-        Abc_NtkDupObj(pNtkNew, pObj);
+        Abc_NtkDupObj( pNtkNew, pObj );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj );
+    // copy the names
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
     Abc_NtkForEachPo( pNtk, pObj, i )
-        Abc_NtkDupObj(pNtkNew, pObj);
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
 
     // create one AND for each logic node
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
+        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
+            continue;
         pObj->pCopy = Abc_NtkCreateNode( pNtkNew );
         pObj->pCopy->pCopy = pObj;
     }
+    // make latches point to the latch fanins
     Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        assert( !Abc_ObjIsLatch(Abc_ObjFanin0(pObj)) );
         pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
+    }
 
     // create internal AND nodes w/o strashing for each logic node (including constants)
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
+        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
+            continue;
         // get the SOP of the node
         if ( Abc_NtkHasMapping(pNtk) )
             pSop = Mio_GateReadSop(pObj->pData);
@@ -131,9 +155,9 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
         Abc_ObjAddFanin( pObj->pCopy, pFanin );
         Abc_ObjAddFanin( pObj->pCopy, pFanin );
     }
-
-    // connect the POs...
-
+    // connect the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
     
     // start the storage for initial states
     p = pNtkNew->pManFunc;
@@ -142,7 +166,15 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
     // add the sequential edges
     Abc_NtkForEachLatch( pNtk, pObj, i )
         Abc_ObjForEachFanout( pObj, pFanout, k )
-            Seq_NodeAddEdges_rec( Abc_ObjFanin0(pObj)->pCopy, pFanout->pCopy, Abc_LatchInit(pObj) );
+        {
+            if ( pObj->pCopy == Abc_ObjFanin0(pFanout->pCopy) )
+            {
+                Seq_NodeInsertFirst( pFanout->pCopy, 0, Abc_LatchInit(pObj) );
+                Seq_NodeInsertFirst( pFanout->pCopy, 1, Abc_LatchInit(pObj) );
+                continue;
+            }
+            Seq_NodeAddEdges_rec( pObj->pCopy, Abc_ObjFanin0(pFanout->pCopy), Abc_LatchInit(pObj) );
+        }
 
     // collect the nodes in the topological order
     p->vMapAnds   = Abc_NtkDfs( pNtk, 0 );
@@ -154,7 +186,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
         Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
         // collect the new fanins of this node
         Abc_ObjForEachFanin( pObj, pFanin, k )
-            Vec_VecPush( p->vMapCuts, i, pFanin->pCopy );
+            Vec_VecPush( p->vMapCuts, i, (void *)( (pFanin->pCopy->Id << 8) | Abc_ObjIsLatch(pFanin) ) );
         // collect the delay info
         if ( !Abc_NtkHasMapping(pNtk) )
         {
@@ -178,10 +210,14 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
 
     // set the cutset composed of latch drivers
 //    Abc_NtkAigCutsetCopy( pNtk );
-    Seq_NtkLatchGetEqualFaninNum( pNtkNew );
+//    Seq_NtkLatchGetEqualFaninNum( pNtkNew );
+
+    // convert the network back into BDDs if this is how it was
+    if ( fHasBdds )
+        Abc_NtkSopToBdd(pNtk);
 
     // copy EXDC and check correctness
-    if ( pNtkNew->pExdc )
+    if ( pNtk->pExdc )
         fprintf( stdout, "Warning: EXDC is not copied when converting to sequential AIG.\n" );
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Seq_NtkRetimeDerive(): Network check has failed.\n" );
@@ -202,6 +238,9 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk )
 void Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init )
 {
     Abc_Obj_t * pFanin;
+    assert( !Abc_ObjIsLatch(pNode) );
+    if ( !Abc_NodeIsAigAnd(pNode) )
+        return;
     // consider the first fanin
     pFanin = Abc_ObjFanin0(pNode);
     if ( pFanin->pCopy == NULL ) // internal node
@@ -275,53 +314,55 @@ Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char *
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
 {
-    Abc_Seq_t * p = pNtk->pManFunc;
-    Seq_Lat_t * pRing;
+    Abc_Seq_t * p = pNtkSeq->pManFunc;
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj, * pFaninNew, * pObjNew;
-    int i;
+    Abc_Obj_t * pObj, * pObjNew, * pFanin, * pFaninNew;
+    int i, k;
 
     assert( !Abc_NtkIsSeq(pNtkOld) );
-    assert( Abc_NtkIsSeq(pNtk) );
+    assert( Abc_NtkIsSeq(pNtkSeq) );
+
+    // transfer the pointers pNtkOld->pNtkSeq from pCopy to pNext
+    Abc_NtkForEachObj( pNtkOld, pObj, i )
+        pObj->pNext = pObj->pCopy;
 
     // start the final network
-    pNtkNew = Abc_NtkStartFrom( pNtk, pNtkOld->ntkType, pNtkOld->ntkFunc );
+    pNtkNew = Abc_NtkStartFrom( pNtkSeq, pNtkOld->ntkType, pNtkOld->ntkFunc );
 
-    // copy the internal nodes
-    Abc_NtkForEachNode( pNtk, pObj, i )
+    // copy the internal nodes of the old network into the new network
+    // transfer the pointers pNktOld->pNtkNew to pNtkSeq->pNtkNew
+    Abc_NtkForEachNode( pNtkOld, pObj, i )
+    {
+        if ( i == 0 ) continue;
         Abc_NtkDupObj( pNtkNew, pObj );
+        pObj->pNext->pCopy = pObj->pCopy;
+    }
 
     // share the latches
-    Seq_NtkShareLatches( pNtkNew, pNtk );
+    Seq_NtkShareLatches( pNtkNew, pNtkSeq );
 
     // connect the objects
-    Abc_AigForEachAnd( pNtk, pObj, i )
-    {
-        if ( pRing = Seq_NodeGetRing(pObj,0) )
-            pFaninNew = pRing->pLatch;
-        else
-            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
-        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    Abc_NtkForEachNode( pNtkOld, pObj, i )
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            pFaninNew = Seq_EdgeReconstruct_rec( pFanin->pNext, pObj->pNext );
+            assert( pFaninNew != NULL );
+            Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        }
 
-        if ( pRing = Seq_NodeGetRing(pObj,1) )
-            pFaninNew = pRing->pLatch;
-        else
-            pFaninNew = Abc_ObjFanin1(pObj)->pCopy;
-        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
-    }
     // connect the POs
-    Abc_NtkForEachPo( pNtk, pObj, i )
+    Abc_NtkForEachPo( pNtkOld, pObj, i )
     {
-        if ( pRing = Seq_NodeGetRing(pObj,0) )
-            pFaninNew = pRing->pLatch;
-        else
-            pFaninNew = Abc_ObjFanin0(pObj)->pCopy;
-        pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
-        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+        pFaninNew = Seq_EdgeReconstructPO( pObj->pNext );
+        assert( pFaninNew != NULL );
+        Abc_ObjAddFanin( pObj->pNext->pCopy, pFaninNew );
     }
 
+    // clean the result of latch sharing
+    Seq_NtkShareLatchesClean( pNtkSeq );
+
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkNew );
     Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
@@ -330,13 +371,81 @@ Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk )
         Vec_PtrPush( pNtkNew->vCos, pObjNew );
     }
     // fix the problem with complemented and duplicated CO edges
-    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkSeqToLogicSop(): Network check has failed.\n" );
+        fprintf( stdout, "Seq_NtkRetimeReconstruct(): Network check has failed.\n" );
     return pNtkNew;
 
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the network after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_EdgeReconstruct_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode )
+{
+    Seq_Lat_t * pRing;
+    Abc_Obj_t * pFanin, * pRes = NULL;
+
+    if ( !Abc_NodeIsAigAnd(pNode) )
+        return NULL;
+
+    // consider the first fanin
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        pRes = Seq_EdgeReconstruct_rec( pGoal, pFanin );
+    else if ( pFanin == pGoal )
+    {
+        if ( pRing = Seq_NodeGetRing( pNode, 0 ) )
+            pRes = pRing->pLatch;
+        else
+            pRes = pFanin->pCopy;
+    }
+    if ( pRes != NULL )
+        return pRes;
+
+    // consider the second fanin
+    pFanin = Abc_ObjFanin1(pNode);
+    if ( pFanin->pCopy == NULL ) // internal node
+        pRes = Seq_EdgeReconstruct_rec( pGoal, pFanin );
+    else if ( pFanin == pGoal )
+    {
+        if ( pRing = Seq_NodeGetRing( pNode, 1 ) )
+            pRes = pRing->pLatch;
+        else
+            pRes = pFanin->pCopy;
+    }
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the network after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Seq_EdgeReconstructPO( Abc_Obj_t * pNode )
+{
+    Seq_Lat_t * pRing;
+    assert( Abc_ObjIsPo(pNode) );
+    if ( pRing = Seq_NodeGetRing( pNode, 0 ) )
+        return pRing->pLatch;
+    else
+        return Abc_ObjFanin0(pNode)->pCopy;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/seq/seqRetIter.c b/src/base/seq/seqRetIter.c
index 5c65e72e..1b8ac71c 100644
--- a/src/base/seq/seqRetIter.c
+++ b/src/base/seq/seqRetIter.c
@@ -76,7 +76,7 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
             }
         }
         // get the upper bound on the clock period
-        FiMax = Delta * (2 + Seq_NtkLevelMax(pNtk));
+        FiMax = Delta * 2 + Abc_NtkDelayTrace(pNtkOld);
         Delta /= 2;
     }
     else
@@ -95,14 +95,24 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
     RetValue = Seq_NtkMappingForPeriod( pNtk, FiBest, fVerbose );
     assert( RetValue );
 
-    // write the retiming lags for both phases of each node
+    // experiment by adding an epsilon to all LValues
+//    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+//        Seq_NodeSetLValueP( pNode, Seq_NodeGetLValueP(pNode) - p->fEpsilon );
+
+    // save the retiming lags
+    // mark the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+        pNode->fMarkA = 1;
+    // process the nodes
     Vec_StrFill( p->vLags,  p->nSize, 0 );
     Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
     {
         NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueP(pNode), FiBest );
-//        Seq_NodeSetLag( pNode, NodeLag );
         Seq_NodeRetimeSetLag_rec( pNode, NodeLag );
     }
+    // unmark the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+        pNode->fMarkA = 0;
 
     // print the result
     if ( fVerbose )
@@ -153,7 +163,7 @@ int Seq_NtkMappingForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
     char * pReason = "";
 
     // set l-values of all nodes to be minus infinity
-    Vec_IntFill( p->vLValues,  p->nSize, -ABC_INFINITY );
+    Vec_IntFill( p->vLValues,  p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
 
     // set l-values of constants and PIs
     pObj = Abc_NtkObj( pNtk, 0 );
@@ -268,11 +278,18 @@ int Seq_NtkNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, Vec_Ptr_t * vLeaves, Ve
 ***********************************************************************/
 void Seq_NodeRetimeSetLag_rec( Abc_Obj_t * pNode, char Lag )
 {
-    if ( pNode->pCopy )
+    Abc_Obj_t * pFanin;
+    if ( !Abc_NodeIsAigAnd(pNode) )
         return;
-    Seq_NodeRetimeSetLag_rec( Abc_ObjFanin0(pNode), Lag );
-    Seq_NodeRetimeSetLag_rec( Abc_ObjFanin1(pNode), Lag );
     Seq_NodeSetLag( pNode, Lag );
+    // consider the first fanin
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( pFanin->fMarkA == 0 ) // internal node
+        Seq_NodeRetimeSetLag_rec( pFanin, Lag );
+    // consider the second fanin
+    pFanin = Abc_ObjFanin1(pNode);
+    if ( pFanin->fMarkA == 0 ) // internal node
+        Seq_NodeRetimeSetLag_rec( pFanin, Lag );
 }
 
 
diff --git a/src/base/seq/seqShare.c b/src/base/seq/seqShare.c
index 5f5f1731..417dcc83 100644
--- a/src/base/seq/seqShare.c
+++ b/src/base/seq/seqShare.c
@@ -342,6 +342,31 @@ void Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t *
     Vec_PtrShrink( vMapAnds, nOldNodes );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Clean the latches after sharing them.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkShareLatchesClean( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        Seq_NodeCleanLats( pObj, 0 );
+        Seq_NodeCleanLats( pObj, 1 );
+    }
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_NodeCleanLats( pObj, 0 );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////