Version abc51130

18 files changed, 447 insertions, 878 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 1904a0b6..e43ee31b 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -632,8 +632,9 @@ extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool
 extern Abc_Obj_t *        Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode );
 extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
 /*=== abcSweep.c ==========================================================*/
-extern int                Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
 extern int                Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose );
+extern int                Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
+extern int                Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes );
 /*=== abcTiming.c ==========================================================*/
 extern Abc_Time_t *       Abc_NodeReadArrival( Abc_Obj_t * pNode );
 extern Abc_Time_t *       Abc_NodeReadRequired( Abc_Obj_t * pNode );
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index ef9fd50a..53f8c1e9 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -25,6 +25,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
+static void Abc_NtkAddPoBuffers( Abc_Ntk_t * pNtk );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -280,7 +282,17 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
             else
                 Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
     // connect the COs
-    Abc_NtkFinalize( pNtk, pNtkNew );
+//    Abc_NtkFinalize( pNtk, pNtkNew );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        if ( pFanin->pCopy->pCopy )
+            pNodeNew = Abc_ObjNotCond(pFanin->pCopy->pCopy, Abc_ObjFaninC0(pObj));
+        else
+            pNodeNew = Abc_ObjNotCond(pFanin->pCopy, Abc_ObjFaninC0(pObj));
+        Abc_ObjAddFanin( pObj->pCopy, pNodeNew );
+    }
+
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
     // duplicate the EXDC Ntk
@@ -364,6 +376,31 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
     return pNtkNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Adds buffers for each PO.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAddPoBuffers( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj, * pFanin, * pFaninNew;
+    int i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjChild0(pObj);
+        pFaninNew = Abc_NtkCreateNode(pNtk);
+        Abc_ObjAddFanin( pFaninNew, pFanin );
+        Abc_ObjPatchFanin( pObj, pFanin, pFaninNew );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 91adbabc..9abb75e8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -102,6 +102,7 @@ static int Abc_CommandRetime       ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandSeqFpga      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqMap       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqSweep     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqCleanup   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -195,7 +196,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "sfpga",         Abc_CommandSeqFpga,          1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "smap",          Abc_CommandSeqMap,           1 );
-    Cmd_CommandAdd( pAbc, "Sequential",   "seq_sweep",     Abc_CommandSeqSweep,         1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "ssweep",        Abc_CommandSeqSweep,         1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "scleanup",      Abc_CommandSeqCleanup,       1 );
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
@@ -1299,7 +1301,7 @@ int Abc_CommandShowNtk( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         switch ( c )
         {
-        case 'n':
+        case 'g':
             fGateNames ^= 1;
             break;
         default:
@@ -1716,7 +1718,7 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     // modify the current network
-    Abc_NtkCleanup( pNtk, 0 );
+    Abc_NtkCleanup( pNtk, 1 );
     return 0;
 
 usage:
@@ -5132,7 +5134,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Retiming has failed.\n" );
-        return 1;
+        return 0;
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -5208,12 +5210,14 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Abc_NtkHasAig(pNtk) )
     {
+/*
         // quit if there are choice nodes
         if ( Abc_NtkGetChoiceNum(pNtk) )
         {
             fprintf( pErr, "Currently cannot map/retime networks with choice nodes.\n" );
             return 0;
         }
+*/
         if ( Abc_NtkIsStrash(pNtk) )
             pNtkNew = Abc_NtkAigToSeq(pNtk);
         else
@@ -5330,12 +5334,14 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Abc_NtkHasAig(pNtk) )
     {
+/*
         // quit if there are choice nodes
         if ( Abc_NtkGetChoiceNum(pNtk) )
         {
             fprintf( pErr, "Currently cannot map/retime networks with choice nodes.\n" );
             return 0;
         }
+*/
         if ( Abc_NtkIsStrash(pNtk) )
             pNtkNew = Abc_NtkAigToSeq(pNtk);
         else
@@ -5377,7 +5383,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
         Abc_NtkDelete( pNtkNew );
-        return 1;
+        return 0;
     }
     Abc_NtkDelete( pNtkNew );
 
@@ -5497,7 +5503,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: seq_sweep [-F num] [-eivh]\n" );
+    fprintf( pErr, "usage: ssweep [-F num] [-eivh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using van Eijk's method\n" );
     fprintf( pErr, "\t-F num : number of time frames in the base case [default = %d]\n", nFrames );
     fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
@@ -5507,6 +5513,60 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Only works for sequential AIGs.\n" );
+        return 1;
+    }
+    // modify the current network
+    Seq_NtkCleanup( pNtk, 1 );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: scleanup [-h]\n" );
+    fprintf( pErr, "\t         performs sequential cleanup\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 4b4c01ae..dc79208e 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -96,6 +96,57 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         fprintf( pFile, "  lev = %3d", Abc_NtkGetLevelNum(pNtk) );
 
     fprintf( pFile, "\n" );
+    // print the statistic into a file
+/*
+    {
+        FILE * pTable;
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s  ",  pNtk->pName );
+        fprintf( pTable, "%4d ", Abc_NtkPiNum(pNtk) );
+        fprintf( pTable, "%4d ", Abc_NtkPoNum(pNtk) );
+//        fprintf( pTable, "%4d ", Abc_NtkLatchNum(pNtk) );
+        fprintf( pTable, "%6d ", Abc_NtkNodeNum(pNtk) );
+        fprintf( pTable, "%6d ", Abc_AigGetLevelNum(pNtk) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+    }
+*/
+/*
+    // print the statistic into a file
+    {
+        FILE * pTable;
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  pNtk->pSpec );
+        fprintf( pTable, "%.0f ", Abc_NtkGetMappedArea(pNtk) );
+        fprintf( pTable, "%.2f ", Abc_NtkDelayTrace(pNtk) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+    }
+*/
+
+/*
+    // print the statistic into a file
+    {
+        FILE * pTable;
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  pNtk->pName );
+        fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
+        fprintf( pTable, "%d ", Abc_AigGetLevelNum(pNtk) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+    }
+*/
+/*
+    // print the statistic into a file
+    {
+        FILE * pTable;
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  pNtk->pName );
+        fprintf( pTable, "%d ", Abc_NtkLatchNum(pNtk) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+    }
+*/
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 1841ba8c..228e27eb 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -447,17 +447,40 @@ int Abc_NodeDroppingCost( Abc_Obj_t * pNode )
 int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode;
-    int i, Counter;
+    int Counter;
     assert( !Abc_NtkHasAig(pNtk) );
     // mark the nodes reachable from the POs
     vNodes = Abc_NtkDfs( pNtk, 0 );
+    Counter = Abc_NtkReduceNodes( pNtk, vNodes );
+    if ( fVerbose )
+        printf( "Cleanup removed %d dangling nodes.\n", Counter );
+    Vec_PtrFree( vNodes );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Preserves the nodes collected in the array.]
+
+  Description [Returns the number of nodes removed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pNode;
+    int i, Counter;
+    assert( !Abc_NtkIsStrash(pNtk) );
+    // mark the nodes reachable from the POs
     for ( i = 0; i < vNodes->nSize; i++ )
     {
         pNode = vNodes->pArray[i];
+        assert( Abc_ObjIsNode(pNode) );
         pNode->fMarkA = 1;
     }
-    Vec_PtrFree( vNodes );
     // if it is an AIG, also mark the constant 1 node
     if ( Abc_NtkConst1(pNtk) )
         Abc_NtkConst1(pNtk)->fMarkA = 1;
@@ -472,14 +495,9 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
     // unmark the remaining nodes
     Abc_NtkForEachNode( pNtk, pNode, i )
         pNode->fMarkA = 0;
-    if ( fVerbose )
-        printf( "Cleanup removed %d dangling nodes.\n", Counter );
     // check
     if ( !Abc_NtkCheck( pNtk ) )
-    {
         printf( "Abc_NtkCleanup: The network check has failed.\n" );
-        return -1;
-    }
     return Counter;
 }
 
diff --git a/src/base/seq/seq.h b/src/base/seq/seq.h
index 323466a0..cba15e47 100644
--- a/src/base/seq/seq.h
+++ b/src/base/seq/seq.h
@@ -79,6 +79,8 @@ extern void            Seq_NtkLatchGetInitNums( Abc_Ntk_t * pNtk, int * pInits )
 extern int             Seq_NtkLatchGetEqualFaninNum( Abc_Ntk_t * pNtk );
 extern int             Seq_NtkCountNodesAboveLimit( Abc_Ntk_t * pNtk, int Limit );
 extern int             Seq_MapComputeAreaFlows( Abc_Ntk_t * pNtk, int fVerbose );
+extern Vec_Ptr_t *     Seq_NtkReachNodes( Abc_Ntk_t * pNtk, int fFromPos );
+extern int             Seq_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c
index 9b1e69a5..b1f66721 100644
--- a/src/base/seq/seqAigCore.c
+++ b/src/base/seq/seqAigCore.c
@@ -73,7 +73,8 @@ void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int f
         Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC );
     // get the retiming lags
     p->nMaxIters = nMaxIters;
-    Seq_AigRetimeDelayLags( pNtk, fVerbose );
+    if ( !Seq_AigRetimeDelayLags( pNtk, fVerbose ) )
+        return;
     // implement this retiming
     RetValue = Seq_NtkImplementRetiming( pNtk, p->vLags, fVerbose );
     if ( RetValue == 0 )
diff --git a/src/base/seq/seqAigIter.c b/src/base/seq/seqAigIter.c
index 9b423d32..683c0093 100644
--- a/src/base/seq/seqAigIter.c
+++ b/src/base/seq/seqAigIter.c
@@ -44,11 +44,11 @@ static int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_AigRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
+int Seq_AigRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
     Abc_Obj_t * pNode;
-    int i, FiMax, FiBest, RetValue;
+    int i, FiMax, FiBest, RetValue, clk, clkIter;
     char NodeLag;
 
     assert( Abc_NtkIsSeq( pNtk ) );
@@ -57,15 +57,29 @@ void Seq_AigRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
     FiMax = 2 + Seq_NtkLevelMax(pNtk);
 
     // make sure this clock period is feasible
-    assert( Seq_RetimeForPeriod( pNtk, FiMax, fVerbose ) );
+    if ( !Seq_RetimeForPeriod( pNtk, FiMax, fVerbose ) )
+    {
+        Vec_StrFill( p->vLags, p->nSize, 0 );
+        printf( "Error: The upper bound on the clock period cannot be computed.\n" );
+        printf( "The reason for this error may be the presence in the circuit of logic\n" );
+        printf( "that is not reachable from the PIs. Mapping/retiming is not performed.\n" );
+        return 0;
+    }
 
     // search for the optimal clock period between 0 and nLevelMax
+clk = clock();
     FiBest = Seq_RetimeSearch_rec( pNtk, 0, FiMax, fVerbose );
+clkIter = clock() - clk;
 
     // recompute the best l-values
     RetValue = Seq_RetimeForPeriod( pNtk, FiBest, fVerbose );
     assert( RetValue );
 
+    // fix the problem with non-converged delays
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        if ( Seq_NodeGetLValue(pNode) < -ABC_INFINITY/2 )
+            Seq_NodeSetLValue( pNode, 0 );
+
     // write the retiming lags
     Vec_StrFill( p->vLags, p->nSize, 0 );
     Abc_AigForEachAnd( pNtk, pNode, i )
@@ -73,39 +87,39 @@ void Seq_AigRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
         NodeLag = Seq_NodeComputeLag( Seq_NodeGetLValue(pNode), FiBest );
         Seq_NodeSetLag( pNode, NodeLag );
     }
-/*
-    {
-        Abc_Obj_t * pFanin, * pFanout;
-        pNode = Abc_NtkObj( pNtk, 823 );
-        printf( "Node  %d.  Lag = %d. LValue = %d. Latches = (%d,%d) (%d,%d).\n", pNode->Id, Seq_NodeGetLag(pNode), Seq_NodeGetLValue(pNode), 
-            Seq_ObjFaninL0(pNode), Seq_ObjFaninL1(pNode), Seq_ObjFanoutL(pNode, Abc_NtkObj(pNtk, 826)), Seq_ObjFanoutL(pNode, Abc_NtkObj(pNtk, 1210)) );
-        pFanin = Abc_ObjFanin0( pNode );
-        printf( "Fanin %d.  Lag = %d. LValue = %d. Latches = (%d,%d)\n", pFanin->Id, Seq_NodeGetLag(pFanin), Seq_NodeGetLValue(pFanin),
-            Seq_ObjFaninL0(pFanin), Seq_ObjFaninL1(pFanin) );
-        pFanin = Abc_ObjFanin1( pNode );
-        printf( "Fanin %d.  Lag = %d. LValue = %d.\n", pFanin->Id, Seq_NodeGetLag(pFanin), Seq_NodeGetLValue(pFanin) );
-        Abc_ObjForEachFanout( pNode, pFanout, i )
-            printf( "Fanout %d.  Lag = %d. LValue = %d.\n", pFanout->Id, Seq_NodeGetLag(pFanout), Seq_NodeGetLValue(pFanout) );
-        Abc_ObjForEachFanout( Abc_ObjFanin0(pNode), pFanout, i )
-            printf( "Fanout %d.  Lag = %d. LValue = %d.\n", pFanout->Id, Seq_NodeGetLag(pFanout), Seq_NodeGetLValue(pFanout) );
-    }
-*/
 
     // print the result
     if ( fVerbose )
     printf( "The best clock period is %3d.\n", FiBest );
-
 /*
-    printf( "LValues : " );
+    printf( "lvalues and lags : " );
     Abc_AigForEachAnd( pNtk, pNode, i )
-        printf( "%d=%d ", i, Seq_NodeGetLValue(pNode) );
-    printf( "\n" );
-    printf( "Lags : " );
-    Abc_AigForEachAnd( pNtk, pNode, i )
-        if ( Vec_StrEntry(p->vLags,i) != 0 )
-            printf( "%d=%d(%d)(%d) ", i, Vec_StrEntry(p->vLags,i), Seq_NodeGetLValue(pNode), Seq_NodeGetLValue(pNode) - FiBest * Vec_StrEntry(p->vLags,i) );
+        printf( "%d=%d(%d) ", pNode->Id, Seq_NodeGetLValue(pNode), Seq_NodeGetLag(pNode) );
     printf( "\n" );
 */
+/*
+    {
+        FILE * pTable;
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  pNtk->pName );
+        fprintf( pTable, "%d ", FiBest );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+    }
+*/
+/*
+    {
+        FILE * pTable;
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  pNtk->pName );
+        fprintf( pTable, "%.2f ", (float)(p->timeCuts)/(float)(CLOCKS_PER_SEC) );
+        fprintf( pTable, "%.2f ", (float)(clkIter)/(float)(CLOCKS_PER_SEC) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+    }
+*/
+    return 1;
+
 }
 
 /**Function*************************************************************
@@ -203,6 +217,14 @@ int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose )
         else
             printf( "Period = %3d.  Iterations = %3d.  Updates = %10d.      Feasible\n",    Fi, c, Counter );
     }
+/*
+    // check if any AND gates have infinite delay
+    Counter = 0;
+    Abc_AigForEachAnd( pNtk, pObj, i )
+        Counter += (Seq_NodeGetLValue(pObj) < -ABC_INFINITY/2);
+    if ( Counter > 0 )
+        printf( "Warning: %d internal nodes have wrong l-values!\n", Counter );
+*/
     return RetValue != SEQ_UPDATE_FAIL;
 }
 
diff --git a/src/base/seq/seqFpgaCore.c b/src/base/seq/seqFpgaCore.c
index 705f553d..2afb5332 100644
--- a/src/base/seq/seqFpgaCore.c
+++ b/src/base/seq/seqFpgaCore.c
@@ -62,7 +62,8 @@ Abc_Ntk_t * Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose
     p->nMaxIters = nMaxIters;
 
     // find the best mapping and retiming for all nodes (p->vLValues, p->vBestCuts, p->vLags)
-    Seq_FpgaMappingDelays( pNtk, fVerbose );
+    if ( !Seq_FpgaMappingDelays( pNtk, fVerbose ) )
+        return NULL;
     if ( RetValue = Abc_NtkGetChoiceNum(pNtk) )
     {
         printf( "The network has %d choices. Deriving the resulting network is skipped.\n", RetValue );
diff --git a/src/base/seq/seqFpgaIter.c b/src/base/seq/seqFpgaIter.c
index 96874db3..ae411881 100644
--- a/src/base/seq/seqFpgaIter.c
+++ b/src/base/seq/seqFpgaIter.c
@@ -47,7 +47,7 @@ extern Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose )
+int Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
     Cut_Params_t Params, * pParams = &Params;
@@ -78,8 +78,9 @@ p->timeCuts = clock() - clk;
 
     // compute the delays
 clk = clock();
-    Seq_AigRetimeDelayLags( pNtk, fVerbose );
-p->timeDelay = clock() - clk;
+    if ( !Seq_AigRetimeDelayLags( pNtk, fVerbose ) )
+        return 0;
+    p->timeDelay = clock() - clk;
 
     // collect the nodes and cuts used in the mapping
     p->vMapAnds = Vec_PtrAlloc( 1000 );
@@ -94,6 +95,7 @@ p->timeDelay = clock() - clk;
     // remove the cuts
     Cut_ManStop( p->pCutMan );
     p->pCutMan = NULL;
+    return 1;
 }
 
 /**Function*************************************************************
@@ -161,7 +163,7 @@ Cut_Cut_t * Seq_FpgaMappingSelectCut( Abc_Obj_t * pAnd )
     for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
     {
         ArrivalCut = *((int *)&pCut->uSign);
-        assert( ArrivalCut >= ArrivalMin );
+//        assert( ArrivalCut >= ArrivalMin );
         if ( ArrivalCut > ArrivalMin )
             continue;
         CostCur = 0.0;
diff --git a/src/base/seq/seqInt.h b/src/base/seq/seqInt.h
index 5532b490..e571272c 100644
--- a/src/base/seq/seqInt.h
+++ b/src/base/seq/seqInt.h
@@ -217,15 +217,15 @@ static inline void           Seq_NodeSetInitOne( Abc_Obj_t * pObj, int Edge, int
 ////////////////////////////////////////////////////////////////////////
 
 /*=== seqAigIter.c =============================================================*/
-extern void                  Seq_AigRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose );
+extern int                   Seq_AigRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose );
 extern int                   Seq_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags, int fVerbose );
 /*=== seqFpgaIter.c ============================================================*/
-extern void                  Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose );
+extern int                   Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose );
 extern int                   Seq_FpgaNodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
 /*=== seqMapIter.c ============================================================*/
-extern void                  Seq_MapRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose );
+extern int                   Seq_MapRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose );
 /*=== seqRetIter.c =============================================================*/
-extern void                  Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose );
+extern int                   Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose );
 /*=== seqLatch.c ===============================================================*/
 extern void                  Seq_NodeInsertFirst( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init );  
 extern void                  Seq_NodeInsertLast( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init );  
diff --git a/src/base/seq/seqMapCore.c b/src/base/seq/seqMapCore.c
index bbcc9a7c..fee31287 100644
--- a/src/base/seq/seqMapCore.c
+++ b/src/base/seq/seqMapCore.c
@@ -74,12 +74,14 @@ Abc_Ntk_t * Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
     p->fStandCells = 1;
 
     // find the best mapping and retiming for all nodes (p->vLValues, p->vBestCuts, p->vLags)
-    Seq_MapRetimeDelayLags( pNtk, fVerbose );
+    if ( !Seq_MapRetimeDelayLags( pNtk, fVerbose ) )
+        return NULL;
     if ( RetValue = Abc_NtkGetChoiceNum(pNtk) )
     {
         printf( "The network has %d choices. Deriving the resulting network is skipped.\n", RetValue );
         return NULL;
     }
+    return NULL;
 
     // duplicate the nodes contained in multiple cuts
     pNtkNew = Seq_NtkMapDup( pNtk );
diff --git a/src/base/seq/seqMapCore_old.c b/src/base/seq/seqMapCore_old.c
deleted file mode 100644
index cc31de10..00000000
--- a/src/base/seq/seqMapCore_old.c
+++ /dev/null
@@ -1,361 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [seqMapCore.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Construction and manipulation of sequential AIGs.]
-
-  Synopsis    [The core of SC mapping/retiming package.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: seqMapCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "seqInt.h"
-#include "main.h"
-#include "mio.h"
-#include "mapper.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-extern Abc_Ntk_t *  Seq_NtkMapDup( Abc_Ntk_t * pNtk );
-extern int          Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose );
-extern Abc_Ntk_t *  Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk );
-
-static int          Seq_MapMappingCount( Abc_Ntk_t * pNtk );
-static int          Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
-static Abc_Obj_t *  Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int fCompl, int LagCut, Vec_Ptr_t * vLeaves, unsigned uPhase );
-static DdNode *     Seq_MapMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves );
-static void         Seq_MapMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges );
-static void         Seq_MapMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
-static DdNode *     Seq_MapMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
-
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Performs Map mapping and retiming.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
-{
-    Abc_Seq_t * p = pNtk->pManFunc;
-    Abc_Ntk_t * pNtkNew;
-    Abc_Ntk_t * pNtkMap;
-    int RetValue;
-
-    // derive the supergate library
-    if ( Abc_FrameReadLibSuper() == NULL && Abc_FrameReadLibGen() )
-    {
-        printf( "A simple supergate library is derived from gate library \"%s\".\n", 
-            Mio_LibraryReadName(Abc_FrameReadLibGen()) );
-        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen() );
-    }
-    p->pSuperLib   = Abc_FrameReadLibSuper();
-    p->nVarsMax    = Map_SuperLibReadVarsMax(p->pSuperLib);
-    p->nMaxIters   = nMaxIters;
-    p->fStandCells = 1;
-
-    // find the best mapping and retiming for all nodes (p->vLValues, p->vBestCuts, p->vLags)
-    Seq_MapRetimeDelayLags( pNtk, fVerbose );
-    if ( RetValue = Abc_NtkGetChoiceNum(pNtk) )
-    {
-        printf( "The network has %d choices. Deriving the resulting network is skipped.\n", RetValue );
-        return NULL;
-    }
-
-    // duplicate the nodes contained in multiple cuts
-    pNtkNew = Seq_NtkMapDup( pNtk );
-    return pNtkNew;
-    
-    // implement the retiming
-    RetValue = Seq_NtkImplementRetiming( pNtkNew, ((Abc_Seq_t *)pNtkNew->pManFunc)->vLags, fVerbose );
-    if ( RetValue == 0 )
-        printf( "Retiming completed but initial state computation has failed.\n" );
-//    return pNtkNew;
-
-    // check the compatibility of initial states computed
-    if ( RetValue = Seq_NtkMapInitCompatible( pNtkNew, fVerbose ) )
-    {
-        printf( "The number of LUTs with incompatible edges = %d.\n", RetValue );
-        Abc_NtkDelete( pNtkNew );
-        return NULL;
-    }
-
-    // create the final mapped network
-    pNtkMap = Seq_NtkSeqMapMapped( pNtkNew );
-    Abc_NtkDelete( pNtkNew );
-    return pNtkMap;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the network by duplicating some of the nodes.]
-
-  Description [Information about mapping is given as mapping nodes (p->vMapAnds)
-  and best cuts for each node (p->vMapCuts).]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk )
-{
-    Abc_Seq_t * pNew, * p = pNtk->pManFunc;
-    Seq_Match_t * pMatch;
-    Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pFanin, * pFaninNew, * pLeaf;
-    Vec_Ptr_t * vLeaves;
-    unsigned SeqEdge;
-    int i, k, nObjsNew, Lag;
-    
-    assert( Abc_NtkIsSeq(pNtk) );
-
-    // start the expanded network
-    pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
-    Abc_NtkCleanNext(pNtk);
-
-    // start the new sequential AIG manager
-    nObjsNew = 1 + Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk) + Seq_MapMappingCount(pNtk);
-    Seq_Resize( pNtkNew->pManFunc, nObjsNew );
-
-    // duplicate the nodes in the mapping
-    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
-    {
-//        Abc_NtkDupObj( pNtkNew, pMatch->pAnd );
-        if ( !pMatch->fCompl )
-            pMatch->pAnd->pCopy = Abc_NtkCreateNode( pNtkNew );
-        else
-            pMatch->pAnd->pNext = Abc_NtkCreateNode( pNtkNew );
-    }
-
-    // recursively construct the internals of each node
-    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
-    {
-        vLeaves = Vec_VecEntry( p->vMapCuts, i );
-        Seq_MapMappingBuild_rec( pNtkNew, pNtk, pMatch->pAnd->Id << 8, 1, pMatch->fCompl, Seq_NodeGetLag(pMatch->pAnd), vLeaves, pMatch->uPhase );
-    }
-    assert( nObjsNew == pNtkNew->nObjs );
-
-    // set the POs
-//    Abc_NtkFinalize( pNtk, pNtkNew );
-    Abc_NtkForEachPo( pNtk, pObj, i )
-    {
-        pFanin = Abc_ObjFanin0(pObj);
-        if ( Abc_ObjFaninC0(pObj) )
-            pFaninNew = pFanin->pNext ? pFanin->pNext : Abc_ObjNot(pFanin->pCopy);
-        else
-            pFaninNew = pFanin->pCopy ? pFanin->pCopy : Abc_ObjNot(pFanin->pNext);
-        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
-    }
-
-    // duplicate the latches on the PO edges
-    Abc_NtkForEachPo( pNtk, pObj, i )
-        Seq_NodeDupLats( pObj->pCopy, pObj, 0 );
-
-    // transfer the mapping info to the new manager
-    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
-    {
-        // get the leaves of the cut
-        vLeaves = Vec_VecEntry( p->vMapCuts, i );
-        // convert the leaf nodes
-        Vec_PtrForEachEntry( vLeaves, pLeaf, k )
-        {
-            SeqEdge = (unsigned)pLeaf;
-            pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 );
-            Lag = (SeqEdge & 255) + Seq_NodeGetLag(pMatch->pAnd) - Seq_NodeGetLag(pLeaf);
-            assert( Lag >= 0 );
-            // translate the old leaf into the leaf in the new network
-//            Vec_PtrWriteEntry( vLeaves, k, (void *)((pLeaf->pCopy->Id << 8) | Lag) );
-
-//            printf( "%d -> %d\n", pLeaf->Id, pLeaf->pCopy->Id );
-        }
-        // convert the root node
-//        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
-        pMatch->pAnd = pMatch->pAnd->pCopy;
-    }
-    pNew = pNtkNew->pManFunc;
-    pNew->nVarsMax  = p->nVarsMax;
-    pNew->vMapAnds  = p->vMapAnds;   p->vMapAnds  = NULL;
-    pNew->vMapCuts  = p->vMapCuts;   p->vMapCuts  = NULL;
-
-    if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Seq_NtkMapDup(): Network check has failed.\n" );
-    return pNtkNew;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if the initial states are compatible.]
-
-  Description [Checks of all the initial states on the fanins edges
-  of the cut have compatible number of latches and initial states.
-  If this is not true, then the mapped network with the does not have initial 
-  state. Returns the number of LUTs with incompatible edges.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose )
-{
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the final mapped network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk )
-{
-    return NULL;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of nodes in the bag.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Seq_MapMappingCount( Abc_Ntk_t * pNtk )
-{
-    Abc_Seq_t * p = pNtk->pManFunc;
-    Vec_Ptr_t * vLeaves;
-    Seq_Match_t * pMatch;
-    int i, Counter = 0;
-    Vec_PtrForEachEntry( p->vMapAnds, pMatch, i )
-    {
-        vLeaves = Vec_VecEntry( p->vMapCuts, i );
-        Counter += Seq_MapMappingCount_rec( pNtk, pMatch->pAnd->Id << 8, vLeaves );
-    }
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of nodes in the bag.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves )
-{
-    Abc_Obj_t * pObj, * pLeaf;
-    unsigned SeqEdge0, SeqEdge1;
-    int Lag, i;
-    // get the object and the lag
-    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
-    Lag  = SeqEdge & 255;
-    // if the node is the fanin of the cut, return
-    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
-        if ( SeqEdge == (unsigned)pLeaf )
-            return 0;
-    // continue unfolding
-    assert( Abc_NodeIsAigAnd(pObj) );
-    // get new sequential edges
-    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
-    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
-    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
-    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
-    // call for the children
-    return 1 + Seq_MapMappingCount_rec( pNtk, SeqEdge0, vLeaves ) + 
-        Seq_MapMappingCount_rec( pNtk, SeqEdge1, vLeaves );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the edges pointing to the leaves of the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int fCompl, int LagCut, Vec_Ptr_t * vLeaves, unsigned uPhase )
-{
-    Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1;
-    unsigned SeqEdge0, SeqEdge1;
-    int Lag, i;
-    // get the object and the lag
-    pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 );
-    Lag  = SeqEdge & 255;
-    // if the node is the fanin of the cut, return
-    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
-        if ( SeqEdge == (unsigned)pLeaf )
-        {
-//            if ( uPhase & (1 << i) ) // negative phase is required
-//                return pObj->pNext? pObj->pNext : Abc_ObjNot(pObj->pCopy);
-//            else // positive phase is required
-//                return pObj->pCopy? pObj->pCopy : Abc_ObjNot(pObj->pNext);
-            return pObj->pCopy? pObj->pCopy : Abc_ObjNot(pObj->pNext);
-        }
-    // continue unfolding
-    assert( Abc_NodeIsAigAnd(pObj) );
-    // get new sequential edges
-    assert( Lag + Seq_ObjFaninL0(pObj) < 255 );
-    assert( Lag + Seq_ObjFaninL1(pObj) < 255 );
-    SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj);
-    SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj);
-    // call for the children    
-    pObjNew = fTop? (fCompl? pObj->pNext : pObj->pCopy) : Abc_NtkCreateNode( pNtkNew );
-    // solve subproblems
-    pFaninNew0 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, fCompl, LagCut, vLeaves, uPhase );
-    pFaninNew1 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, fCompl, LagCut, vLeaves, uPhase );
-    // add the fanins to the node
-    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) );
-    Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) );
-    Seq_NodeDupLats( pObjNew, pObj, 0 );
-    Seq_NodeDupLats( pObjNew, pObj, 1 );
-    // set the lag of the new node equal to the internal lag plus mapping/retiming lag
-    Seq_NodeSetLag( pObjNew, (char)(Lag + LagCut) );
-//    Seq_NodeSetLag( pObjNew, (char)(Lag) );
-    return pObjNew;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/base/seq/seqMapIter.c b/src/base/seq/seqMapIter.c
index b93e5dbe..1ff8effd 100644
--- a/src/base/seq/seqMapIter.c
+++ b/src/base/seq/seqMapIter.c
@@ -48,7 +48,7 @@ extern Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_MapRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
+int Seq_MapRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
     Cut_Params_t Params, * pParams = &Params;
@@ -81,8 +81,21 @@ p->timeCuts = clock() - clk;
     // compute the delays
 clk = clock();
     FiBest = Seq_MapRetimeDelayLagsInternal( pNtk, fVerbose );
+    if ( FiBest == 0.0 )
+        return 0;
 p->timeDelay = clock() - clk;
-
+/*
+    {
+        FILE * pTable;
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  pNtk->pName );
+        fprintf( pTable, "%.2f ", FiBest );
+        fprintf( pTable, "%.2f ", (float)(p->timeCuts)/(float)(CLOCKS_PER_SEC) );
+        fprintf( pTable, "%.2f ", (float)(p->timeDelay)/(float)(CLOCKS_PER_SEC) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+    }
+*/
     // clean the marks
     Abc_NtkForEachObj( pNtk, pObj, i )
         assert( !pObj->fMarkA && !pObj->fMarkB );
@@ -104,6 +117,7 @@ p->timeDelay = clock() - clk;
     // remove the cuts
     Cut_ManStop( p->pCutMan );
     p->pCutMan = NULL;
+    return 1;
 }
 
 /**Function*************************************************************
@@ -144,7 +158,15 @@ float Seq_MapRetimeDelayLagsInternal( Abc_Ntk_t * pNtk, int fVerbose )
     Delta /= 2;
 
     // make sure this clock period is feasible
-    assert( Seq_MapRetimeForPeriod( pNtk, FiMax, fVerbose ) );
+    if ( !Seq_MapRetimeForPeriod( pNtk, FiMax, fVerbose ) )
+    {
+        Vec_StrFill( p->vLags, p->nSize, 0 );
+        Vec_StrFill( p->vLagsN, p->nSize, 0 );
+        printf( "Error: The upper bound on the clock period cannot be computed.\n" );
+        printf( "The reason for this error may be the presence in the circuit of logic\n" );
+        printf( "that is not reachable from the PIs. Mapping/retiming is not performed.\n" );
+        return 0;
+    }
 
     // search for the optimal clock period between 0 and nLevelMax
     FiBest = Seq_MapRetimeSearch_rec( pNtk, 0.0, FiMax, Delta, fVerbose );
@@ -153,6 +175,15 @@ float Seq_MapRetimeDelayLagsInternal( Abc_Ntk_t * pNtk, int fVerbose )
     RetValue = Seq_MapRetimeForPeriod( pNtk, FiBest, fVerbose );
     assert( RetValue );
 
+    // fix the problem with non-converged delays
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        if ( Seq_NodeGetLValueP(pNode) < -ABC_INFINITY/2 )
+            Seq_NodeSetLValueP( pNode, 0 );
+        if ( Seq_NodeGetLValueN(pNode) < -ABC_INFINITY/2 )
+            Seq_NodeSetLValueN( pNode, 0 );
+    }
+
     // write the retiming lags for both phases of each node
     Vec_StrFill( p->vLags,  p->nSize, 0 );
     Vec_StrFill( p->vLagsN, p->nSize, 0 );
@@ -579,6 +610,8 @@ void Seq_MapCanonicizeTruthTables( Abc_Ntk_t * pNtk )
     Abc_AigForEachAnd( pNtk, pObj, i )
     {
         pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj );
+        if ( pList == NULL )
+            continue;
         for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
             Cut_TruthCanonicize( pCut );
     }
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index f989eefb..08da5b39 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -60,7 +60,11 @@ Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fV
     if ( !fInitial )
         Seq_NtkLatchSetValues( pNtkSeq, ABC_INIT_DC );
     // find the best mapping and retiming 
-    Seq_NtkRetimeDelayLags( pNtk, pNtkSeq, fVerbose );
+    if ( !Seq_NtkRetimeDelayLags( pNtk, pNtkSeq, fVerbose ) )
+        return NULL;
+    return NULL;
+
+
     // implement the retiming
     RetValue = Seq_NtkImplementRetiming( pNtkSeq, p->vLags, fVerbose );
     if ( RetValue == 0 )
diff --git a/src/base/seq/seqRetCore_old.c b/src/base/seq/seqRetCore_old.c
deleted file mode 100644
index 154f8dad..00000000
--- a/src/base/seq/seqRetCore_old.c
+++ /dev/null
@@ -1,453 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [seqRetCore.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Construction and manipulation of sequential AIGs.]
-
-  Synopsis    [The core of FPGA mapping/retiming package.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: seqRetCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "seqInt.h"
-#include "dec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-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 * 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                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Performs FPGA mapping and retiming.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose )
-{
-    Abc_Seq_t * p;
-    Abc_Ntk_t * pNtkSeq, * pNtkNew;
-    int RetValue;
-    assert( !Abc_NtkHasAig(pNtk) );
-    // derive the isomorphic seq AIG
-    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, pNtkSeq, fVerbose );
-    // implement the retiming
-    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, pNtkSeq );
-    Abc_NtkDelete( pNtkSeq );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the isomorphic seq AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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, fHasBdds;
-    char * pSop;
-
-    // make sure it is an AIG without self-feeding latches
-    assert( !Abc_NtkHasAig(pNtk) );
-    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) )
-        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
-    assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
-
-    // 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_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_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);
-        else
-            pSop = pObj->pData;
-        pFanin = Seq_NodeRetimeDerive( pNtkNew, pObj, pSop );
-        Abc_ObjAddFanin( pObj->pCopy, pFanin );
-        Abc_ObjAddFanin( pObj->pCopy, pFanin );
-    }
-    // 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;
-    Seq_Resize( p, Abc_NtkObjNumMax(pNtkNew) );
-
-    // add the sequential edges
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-        Abc_ObjForEachFanout( pObj, pFanout, k )
-        {
-            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 );
-    p->vMapCuts   = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
-    p->vMapDelays = Vec_VecStart( Vec_PtrSize(p->vMapAnds) );
-    Vec_PtrForEachEntry( p->vMapAnds, pObj, i )
-    {
-        // change the node to be the new one
-        Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy );
-        // collect the new fanins of this node
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-            Vec_VecPush( p->vMapCuts, i, (void *)( (pFanin->pCopy->Id << 8) | Abc_ObjIsLatch(pFanin) ) );
-        // collect the delay info
-        if ( !Abc_NtkHasMapping(pNtk) )
-        {
-            Abc_ObjForEachFanin( pObj, pFanin, k )
-                Vec_VecPush( p->vMapDelays, i, (void *)Abc_Float2Int(1.0) );
-        }
-        else
-        {
-            Mio_Pin_t * pPin = Mio_GateReadPins(pObj->pData);
-            float Max, tDelayBlockRise, tDelayBlockFall;
-            Abc_ObjForEachFanin( pObj, pFanin, k )
-            {
-                tDelayBlockRise = (float)Mio_PinReadDelayBlockRise( pPin );  
-                tDelayBlockFall = (float)Mio_PinReadDelayBlockFall( pPin ); 
-                Max = ABC_MAX( tDelayBlockRise, tDelayBlockFall );
-                Vec_VecPush( p->vMapDelays, i, (void *)Abc_Float2Int(Max) );
-                pPin = Mio_PinReadNext(pPin);
-            }
-        }
-    }
-
-    // set the cutset composed of latch drivers
-//    Abc_NtkAigCutsetCopy( pNtk );
-//    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 ( 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" );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Add sequential edges.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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
-        Seq_NodeAddEdges_rec( pGoal, pFanin, Init );
-    else if ( pFanin == pGoal )
-        Seq_NodeInsertFirst( pNode, 0, Init );
-    // consider the second fanin
-    pFanin = Abc_ObjFanin1(pNode);
-    if ( pFanin->pCopy == NULL ) // internal node
-        Seq_NodeAddEdges_rec( pGoal, pFanin, Init );
-    else if ( pFanin == pGoal )
-        Seq_NodeInsertFirst( pNode, 1, Init );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Strashes one logic node using its SOP.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop )
-{
-    Dec_Graph_t * pFForm;
-    Dec_Node_t * pNode;
-    Abc_Obj_t * pAnd;
-    int i, nFanins;
-
-    // get the number of node's fanins
-    nFanins = Abc_ObjFaninNum( pRoot );
-    assert( nFanins == Abc_SopGetVarNum(pSop) );
-    if ( nFanins < 2 )
-    {
-        if ( Abc_SopIsConst1(pSop) )
-            return Abc_NtkConst1(pNtkNew);
-        else if ( Abc_SopIsConst0(pSop) )
-            return Abc_ObjNot( Abc_NtkConst1(pNtkNew) );
-        else if ( Abc_SopIsBuf(pSop) )
-            return Abc_ObjFanin0(pRoot)->pCopy;
-        else if ( Abc_SopIsInv(pSop) )
-            return Abc_ObjNot( Abc_ObjFanin0(pRoot)->pCopy );
-        assert( 0 );
-        return NULL;
-    }
-
-    // perform factoring
-    pFForm = Dec_Factor( pSop );
-    // collect the fanins
-    Dec_GraphForEachLeaf( pFForm, pNode, i )
-        pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy;
-    // perform strashing
-    pAnd = Dec_GraphToNetworkNoStrash( pNtkNew, pFForm );
-    Dec_GraphFree( pFForm );
-    return pAnd;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Reconstructs the network after retiming.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
-{
-    Abc_Seq_t * p = pNtkSeq->pManFunc;
-    Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj, * pObjNew, * pFanin, * pFaninNew;
-    int i, k;
-
-    assert( !Abc_NtkIsSeq(pNtkOld) );
-    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( pNtkSeq, pNtkOld->ntkType, pNtkOld->ntkFunc );
-
-    // 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, pNtkSeq );
-
-    // connect the objects
-    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 );
-        }
-
-    // connect the POs
-    Abc_NtkForEachPo( pNtkOld, pObj, i )
-    {
-        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 )
-    {
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
-    }
-    // fix the problem with complemented and duplicated CO edges
-    Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
-    if ( !Abc_NtkCheck( pNtkNew ) )
-        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 6fe571f0..9c28c097 100644
--- a/src/base/seq/seqRetIter.c
+++ b/src/base/seq/seqRetIter.c
@@ -49,7 +49,7 @@ static void  Seq_NodePrintInfoPlus( Abc_Obj_t * pNode );
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose )
+int Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
     Abc_Obj_t * pNode;
@@ -76,7 +76,7 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
             if ( Delta == 0.0 )
             {
                 printf( "Cannot retime/map if the library does not have NAND2 or AND2.\n" );
-                return;
+                return 0;
             }
         }
         // get the upper bound on the clock period
@@ -90,8 +90,14 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
     }
 
     // make sure this clock period is feasible
-    assert( Seq_NtkMappingForPeriod( pNtk, FiMax, fVerbose ) );
-
+    if ( !Seq_NtkMappingForPeriod( pNtk, FiMax, fVerbose ) )
+    {
+        printf( "Error: The upper bound on the clock period cannot be computed.\n" );
+        printf( "The reason for this error may be the presence in the circuit of logic\n" );
+        printf( "that is not reachable from the PIs. Mapping/retiming is not performed.\n" );
+        return 0;
+    }
+ 
     // search for the optimal clock period between 0 and nLevelMax
     FiBest = Seq_NtkMappingSearch_rec( pNtk, 0.0, FiMax, Delta, fVerbose );
 
@@ -99,6 +105,11 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
     RetValue = Seq_NtkMappingForPeriod( pNtk, FiBest, fVerbose );
     assert( RetValue );
 
+    // fix the problem with non-converged delays
+    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+        if ( Seq_NodeGetLValueP(pNode) < -ABC_INFINITY/2 )
+            Seq_NodeSetLValueP( pNode, 0 );
+
     // experiment by adding an epsilon to all LValues
 //    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
 //        Seq_NodeSetLValueP( pNode, Seq_NodeGetLValueP(pNode) - p->fEpsilon );
@@ -126,8 +137,18 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
     // print the result
     if ( fVerbose )
         printf( "The best clock period is %6.2f.\n", FiBest );
-
+/*
+    {
+        FILE * pTable;
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  pNtk->pName );
+        fprintf( pTable, "%.2f ", FiBest );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+    }
+*/
 //    Seq_NodePrintInfo( Abc_NtkObj(pNtk, 847) );
+    return 1;
 }
 
 /**Function*************************************************************
diff --git a/src/base/seq/seqUtil.c b/src/base/seq/seqUtil.c
index d9fad0ea..39fde28e 100644
--- a/src/base/seq/seqUtil.c
+++ b/src/base/seq/seqUtil.c
@@ -461,6 +461,134 @@ int Seq_MapComputeAreaFlows( Abc_Ntk_t * pNtk, int fVerbose )
     return 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Collects all the internal nodes reachable from POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkReachNodesFromPos_rec( Abc_Obj_t * pAnd, Vec_Ptr_t * vNodes )
+{
+    // skip if this is a non-PI node
+    if ( !Abc_NodeIsAigAnd(pAnd) )
+        return;
+    // skip a visited node
+    if ( Abc_NodeIsTravIdCurrent(pAnd) )
+        return;
+    Abc_NodeSetTravIdCurrent(pAnd);
+    // visit the fanin nodes
+    Seq_NtkReachNodesFromPos_rec( Abc_ObjFanin0(pAnd), vNodes );
+    Seq_NtkReachNodesFromPos_rec( Abc_ObjFanin1(pAnd), vNodes );
+    // add this node
+    Vec_PtrPush( vNodes, pAnd );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects all the internal nodes reachable from POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkReachNodesFromPis_rec( Abc_Obj_t * pAnd, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pFanout;
+    int k;
+    // skip if this is a non-PI node
+    if ( !Abc_NodeIsAigAnd(pAnd) )
+        return;
+    // skip a visited node
+    if ( Abc_NodeIsTravIdCurrent(pAnd) )
+        return;
+    Abc_NodeSetTravIdCurrent(pAnd);
+    // visit the fanin nodes
+    Abc_ObjForEachFanout( pAnd, pFanout, k )
+        Seq_NtkReachNodesFromPis_rec( pFanout, vNodes );
+    // add this node
+    Vec_PtrPush( vNodes, pAnd );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects all the internal nodes reachable from POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Seq_NtkReachNodes( Abc_Ntk_t * pNtk, int fFromPos )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pFanout;
+    int i, k;
+    assert( Abc_NtkIsSeq(pNtk) );
+    vNodes = Vec_PtrAlloc( 1000 );
+    Abc_NtkIncrementTravId( pNtk );
+    if ( fFromPos )
+    {
+        // traverse the cone of each PO
+        Abc_NtkForEachPo( pNtk, pObj, i )
+            Seq_NtkReachNodesFromPos_rec( Abc_ObjFanin0(pObj), vNodes );
+    }
+    else
+    {
+        // tranvers the reverse cone of the constant node
+        pObj = Abc_NtkConst1( pNtk );
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            Seq_NtkReachNodesFromPis_rec( pFanout, vNodes );
+        // tranvers the reverse cone of the PIs
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            Abc_ObjForEachFanout( pObj, pFanout, k )
+                Seq_NtkReachNodesFromPis_rec( pFanout, vNodes );
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform sequential cleanup.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Seq_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Vec_Ptr_t * vNodesPo, * vNodesPi;
+    int Counter = 0;
+    assert( Abc_NtkIsSeq(pNtk) );
+    // collect the nodes reachable from POs and PIs
+    vNodesPo = Seq_NtkReachNodes( pNtk, 1 );
+    vNodesPi = Seq_NtkReachNodes( pNtk, 0 );
+    printf( "Total nodes = %6d. Reachable from POs = %6d. Reachable from PIs = %6d.\n", 
+        Abc_NtkNodeNum(pNtk), Vec_PtrSize(vNodesPo), Vec_PtrSize(vNodesPi) );
+    if ( Abc_NtkNodeNum(pNtk) > Vec_PtrSize(vNodesPo) )
+    {
+        Counter = Abc_NtkReduceNodes( pNtk, vNodesPo );
+        if ( fVerbose )
+            printf( "Cleanup removed %d nodes that are not reachable from the POs.\n", Counter );
+    }
+    Vec_PtrFree( vNodesPo );
+    Vec_PtrFree( vNodesPi );
+    return Counter;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////