Version abc80402

8 files changed, 449 insertions, 148 deletions

diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index 295b3a9e..191ca3e5 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -131,6 +131,7 @@ static inline Nwk_Obj_t * Nwk_ObjFanout0( Nwk_Obj_t * p )         { return p->pF
 static inline Nwk_Obj_t * Nwk_ObjFanin( Nwk_Obj_t * p, int i )    { return p->pFanio[i];                        } 
 static inline Nwk_Obj_t * Nwk_ObjFanout( Nwk_Obj_t * p, int i )   { return p->pFanio[p->nFanins+1];             } 
 
+static inline int         Nwk_ObjIsNone( Nwk_Obj_t * p )          { return p->Type == NWK_OBJ_NONE;             } 
 static inline int         Nwk_ObjIsCi( Nwk_Obj_t * p )            { return p->Type == NWK_OBJ_CI;               } 
 static inline int         Nwk_ObjIsCo( Nwk_Obj_t * p )            { return p->Type == NWK_OBJ_CO;               } 
 static inline int         Nwk_ObjIsNode( Nwk_Obj_t * p )          { return p->Type == NWK_OBJ_NODE;             } 
@@ -154,6 +155,10 @@ static inline void        Nwk_ObjSetTravIdPrevious( Nwk_Obj_t * pObj )       { p
 static inline int         Nwk_ObjIsTravIdCurrent( Nwk_Obj_t * pObj )         { return pObj->TravId == pObj->pMan->nTravIds;     }
 static inline int         Nwk_ObjIsTravIdPrevious( Nwk_Obj_t * pObj )        { return pObj->TravId == pObj->pMan->nTravIds - 1; }
 
+static inline int         Nwk_ManTimeEqual( float f1, float f2, float Eps )  { return (f1 < f2 + Eps) && (f2 < f1 + Eps);  }
+static inline int         Nwk_ManTimeLess( float f1, float f2, float Eps )   { return (f1 < f2 + Eps);                     }
+static inline int         Nwk_ManTimeMore( float f1, float f2, float Eps )   { return (f1 + Eps > f2);                     }
+
 ////////////////////////////////////////////////////////////////////////
 ///                         ITERATORS                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -191,8 +196,10 @@ static inline int         Nwk_ObjIsTravIdPrevious( Nwk_Obj_t * pObj )        { r
 extern void            Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose );
 extern Hop_Obj_t *     Nwk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
 /*=== nwkDfs.c ==========================================================*/
+extern int             Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk );
+extern int             Nwk_ManLevelBackup( Nwk_Man_t * pNtk );
 extern int             Nwk_ManLevel( Nwk_Man_t * pNtk );
-extern int             Nwk_ManLevel2( Nwk_Man_t * pNtk );
+extern int             Nwk_ManLevelMax( Nwk_Man_t * pNtk );
 extern Vec_Vec_t *     Nwk_ManLevelize( Nwk_Man_t * pNtk );
 extern Vec_Ptr_t *     Nwk_ManDfs( Nwk_Man_t * pNtk );
 extern Vec_Ptr_t *     Nwk_ManDfsNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes );
@@ -203,9 +210,12 @@ extern int             Nwk_ObjMffcLabel( Nwk_Obj_t * pNode );
 /*=== nwkFanio.c ==========================================================*/
 extern void            Nwk_ObjCollectFanins( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
 extern void            Nwk_ObjCollectFanouts( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern int             Nwk_ObjFindFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
+extern int             Nwk_ObjFindFanout( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanout );
 extern void            Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
 extern void            Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
 extern void            Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew );
+extern void            Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo );
 extern void            Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew );
 /*=== nwkMan.c ============================================================*/
 extern Nwk_Man_t *     Nwk_ManAlloc();
@@ -222,10 +232,11 @@ extern Nwk_Obj_t *     Nwk_ManCreateLatch( Nwk_Man_t * pMan );
 extern void            Nwk_ManDeleteNode( Nwk_Obj_t * pObj );
 extern void            Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj );
 /*=== nwkTiming.c ============================================================*/
-extern float           Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib );
-extern void            Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk, If_Lib_t * pLutLib );
+extern int             Nwk_ManVerifyTiming(  Nwk_Man_t * pNtk );
+extern float           Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk );
+extern void            Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk );
 extern void            Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels );
-extern void            Nwk_ManVerifyLevel( Nwk_Man_t * pNtk );
+extern int             Nwk_ManVerifyLevel( Nwk_Man_t * pNtk );
 /*=== nwkUtil.c ============================================================*/
 extern void            Nwk_ManIncrementTravId( Nwk_Man_t * pNtk );
 extern int             Nwk_ManGetFaninMax( Nwk_Man_t * pNtk );
@@ -235,6 +246,7 @@ extern int             Nwk_ManPoNum( Nwk_Man_t * pNtk );
 extern int             Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk );
 extern int             Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
 extern int             Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
+extern void            Nwk_ObjPrint( Nwk_Obj_t * pObj );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/nwk/nwkDfs.c b/src/aig/nwk/nwkDfs.c
index a5f5a660..bf669086 100644
--- a/src/aig/nwk/nwkDfs.c
+++ b/src/aig/nwk/nwkDfs.c
@@ -30,6 +30,63 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Verifies that the objects are in a topo order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pObj, * pNext;
+    int i, k, iBox, iTerm1, nTerms;
+    Nwk_ManIncrementTravId( pNtk );
+    Nwk_ManForEachObj( pNtk, pObj, i )
+    {
+        if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) )
+        {
+            Nwk_ObjForEachFanin( pObj, pNext, k )
+            {
+                if ( !Nwk_ObjIsTravIdCurrent(pNext) )
+                {
+                    printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
+                    return 0;
+                }
+            }
+        }
+        else if ( Nwk_ObjIsCi(pObj) )
+        {
+            if ( pNtk->pManTime )
+            {
+                iBox = Tim_ManBoxForCi( pNtk->pManTime, pObj->PioId );
+                if ( iBox >= 0 ) // this is not a true PI
+                {
+                    iTerm1 = Tim_ManBoxInputFirst( pNtk->pManTime, iBox );
+                    nTerms = Tim_ManBoxInputNum( pNtk->pManTime, iBox );
+                    for ( i = 0; i < nTerms; i++ )
+                    {
+                        pNext = Nwk_ManCo( pNtk, iTerm1 + i );
+                        if ( !Nwk_ObjIsTravIdCurrent(pNext) )
+                        {
+                            printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id );
+                            return 0;
+                        }
+                    }
+                }
+            }
+        }
+        else
+            assert( 0 );
+        Nwk_ObjSetTravIdCurrent( pObj );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes the number of logic levels not counting PIs/POs.]
 
   Description [Assumes that white boxes have unit level.]
@@ -39,11 +96,12 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Nwk_ManLevel( Nwk_Man_t * pNtk )
+int Nwk_ManLevelBackup( Nwk_Man_t * pNtk )
 {
     Tim_Man_t * pManTimeUnit;
     Nwk_Obj_t * pObj, * pFanin;
     int i, k, LevelMax, Level;
+    assert( Nwk_ManVerifyTopoOrder(pNtk) );
     // clean the levels
     Nwk_ManForEachObj( pNtk, pObj, i )
         Nwk_ObjSetLevel( pObj, 0 );
@@ -85,11 +143,9 @@ int Nwk_ManLevel( Nwk_Man_t * pNtk )
     return LevelMax;
 }
 
-
-
 /**Function*************************************************************
 
-  Synopsis    [Performs DFS for one node.]
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
 
   Description []
                
@@ -98,8 +154,9 @@ int Nwk_ManLevel( Nwk_Man_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Nwk_ManLevel2_rec( Nwk_Obj_t * pObj )
+void Nwk_ManLevel_rec( Nwk_Obj_t * pObj )
 {
+    Tim_Man_t * pManTime = pObj->pMan->pManTime;
     Nwk_Obj_t * pNext;
     int i, iBox, iTerm1, nTerms, LevelMax = 0;
     if ( Nwk_ObjIsTravIdCurrent( pObj ) )
@@ -107,30 +164,33 @@ void Nwk_ManLevel2_rec( Nwk_Obj_t * pObj )
     Nwk_ObjSetTravIdCurrent( pObj );
     if ( Nwk_ObjIsCi(pObj) )
     {
-        iBox = Tim_ManBoxForCi( pObj->pMan->pManTime, pObj->PioId );
-        if ( iBox >= 0 ) // this is not a true PI
+        if ( pManTime ) 
         {
-            iTerm1 = Tim_ManBoxInputFirst( pObj->pMan->pManTime, iBox );
-            nTerms = Tim_ManBoxInputNum( pObj->pMan->pManTime, iBox );
-            for ( i = 0; i < nTerms; i++ )
+            iBox = Tim_ManBoxForCi( pManTime, pObj->PioId );
+            if ( iBox >= 0 ) // this is not a true PI
             {
-                pNext = Nwk_ManCo(pObj->pMan, iTerm1 + i);
-                Nwk_ManLevel2_rec( pNext );
-                if ( LevelMax < Nwk_ObjLevel(pNext) )
-                    LevelMax = Nwk_ObjLevel(pNext);
+                iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
+                nTerms = Tim_ManBoxInputNum( pManTime, iBox );
+                for ( i = 0; i < nTerms; i++ )
+                {
+                    pNext = Nwk_ManCo(pObj->pMan, iTerm1 + i);
+                    Nwk_ManLevel_rec( pNext );
+                    if ( LevelMax < Nwk_ObjLevel(pNext) )
+                        LevelMax = Nwk_ObjLevel(pNext);
+                }
+                LevelMax++;
             }
-            LevelMax++;
         }
     }
     else if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) )
     {
         Nwk_ObjForEachFanin( pObj, pNext, i )
         {
-            Nwk_ManLevel2_rec( pNext );
+            Nwk_ManLevel_rec( pNext );
             if ( LevelMax < Nwk_ObjLevel(pNext) )
                 LevelMax = Nwk_ObjLevel(pNext);
         }
-        if ( Nwk_ObjIsNode(pObj) )
+        if ( Nwk_ObjIsNode(pObj) && Nwk_ObjFaninNum(pObj) > 0 )
             LevelMax++;
     }
     else
@@ -140,16 +200,16 @@ void Nwk_ManLevel2_rec( Nwk_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the DFS ordered array of all objects except latches.]
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
 
-  Description []
+  Description [Does not assume that the objects are in a topo order.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Nwk_ManLevel2( Nwk_Man_t * pNtk )
+int Nwk_ManLevel( Nwk_Man_t * pNtk )
 {
     Nwk_Obj_t * pObj;
     int i, LevelMax = 0;
@@ -158,7 +218,7 @@ int Nwk_ManLevel2( Nwk_Man_t * pNtk )
     Nwk_ManIncrementTravId( pNtk );
     Nwk_ManForEachPo( pNtk, pObj, i )
     {
-        Nwk_ManLevel2_rec( pObj );
+        Nwk_ManLevel_rec( pObj );
         if ( LevelMax < Nwk_ObjLevel(pObj) )
             LevelMax = Nwk_ObjLevel(pObj);
     }
@@ -169,6 +229,27 @@ int Nwk_ManLevel2( Nwk_Man_t * pNtk )
 
   Synopsis    [Computes the number of logic levels not counting PIs/POs.]
 
+  Description [Does not assume that the objects are in a topo order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManLevelMax( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pObj;
+    int i, LevelMax = 0;
+    Nwk_ManForEachPo( pNtk, pObj, i )
+        if ( LevelMax < Nwk_ObjLevel(pObj) )
+            LevelMax = Nwk_ObjLevel(pObj);
+    return LevelMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of objects in the AIG manager ordered by level.]
+
   Description []
                
   SideEffects []
@@ -181,7 +262,8 @@ Vec_Vec_t * Nwk_ManLevelize( Nwk_Man_t * pNtk )
     Nwk_Obj_t * pObj;
     Vec_Vec_t * vLevels;
     int nLevels, i;
-    nLevels = Nwk_ManLevel( pNtk );
+    assert( Nwk_ManVerifyLevel(pNtk) );
+    nLevels = Nwk_ManLevelMax( pNtk );
     vLevels = Vec_VecStart( nLevels + 1 );
     Nwk_ManForEachNode( pNtk, pObj, i )
     {
diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c
index d05543e6..2d0254f2 100644
--- a/src/aig/nwk/nwkMan.c
+++ b/src/aig/nwk/nwkMan.c
@@ -93,6 +93,7 @@ void Nwk_ManFree( Nwk_Man_t * p )
 ***********************************************************************/
 void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib )
 {
+    p->pLutLib = pLutLib;
     printf( "%-15s : ",      p->pName );
     printf( "pi = %5d  ",    Nwk_ManPiNum(p) );
     printf( "po = %5d  ",    Nwk_ManPoNum(p) );
@@ -102,8 +103,8 @@ void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib )
     printf( "node = %5d  ",  Nwk_ManNodeNum(p) );
     printf( "aig = %6d  ",   Nwk_ManGetAigNodeNum(p) );
     printf( "lev = %3d  ",   Nwk_ManLevel(p) );
-//    printf( "lev2 = %3d  ",  Nwk_ManLevel2(p) );
-    printf( "delay = %5.2f", Nwk_ManDelayTraceLut(p, pLutLib) );
+//    printf( "lev2 = %3d  ",  Nwk_ManLevelBackup(p) );
+    printf( "delay = %5.2f", Nwk_ManDelayTraceLut(p) );
     printf( "\n" );
 //    Nwk_ManDelayTracePrint( p, pLutLib );
     fflush( stdout );
diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c
index ed67966e..eae3bd24 100644
--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -96,50 +96,45 @@ void Nwk_ManSetIfParsDefault( If_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
+If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
 {
     If_Man_t * pIfMan;
-    Aig_Obj_t * pNode;//, * pFanin, * pPrev;
+    If_Obj_t * pIfObj;
+    Aig_Obj_t * pNode, * pFanin, * pPrev;
     int i;
     // start the mapping manager and set its parameters
     pIfMan = If_ManStart( pPars );
-    // print warning about excessive memory usage
-//    if ( 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 )
-//        printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n", 
-//            1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Aig_ManObjNum(p) );
     // load the AIG into the mapper
     Aig_ManForEachObj( p, pNode, i )
     {
         if ( Aig_ObjIsAnd(pNode) )
-            pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan, 
-                If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), 
-                If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
+            pIfObj = If_ManCreateAnd( pIfMan, 
+                If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), 
+                If_NotCond( Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
         else if ( Aig_ObjIsPi(pNode) )
         {
-            pNode->pData = If_ManCreateCi( pIfMan );
-            ((If_Obj_t *)pNode->pData)->Level = pNode->Level;
-            if ( pIfMan->nLevelMax < (int)pNode->Level )
-                pIfMan->nLevelMax = (int)pNode->Level;
+            pIfObj = If_ManCreateCi( pIfMan );
+            If_ObjSetLevel( pIfObj, Aig_ObjLevel(pNode) );
         }
         else if ( Aig_ObjIsPo(pNode) )
-            pNode->pData = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
+            pIfObj = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
         else if ( Aig_ObjIsConst1(pNode) )
-            Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
+            pIfObj = If_ManConst1( pIfMan );
         else // add the node to the mapper
             assert( 0 );
+        // save the result
+        assert( Vec_PtrEntry(vAigToIf, i) == NULL );
+        Vec_PtrWriteEntry( vAigToIf, i, pIfObj );
+        pNode->pData = pIfObj;
         // set up the choice node
-//        if ( Aig_AigNodeIsChoice( pNode ) )
-//        {
-//            pIfMan->nChoices++;
-//            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
-//                If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
-//            If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
-//        }
+        if ( Aig_ObjIsChoice( p, pNode ) )
         {
-            If_Obj_t * pIfObj = pNode->pData;
-            assert( !If_IsComplement(pIfObj) );
-            assert( pIfObj->Id == pNode->Id );
+            pIfMan->nChoices++;
+            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+                If_ObjSetChoice( pPrev->pData, pFanin->pData );
+            If_ManCreateChoice( pIfMan, pNode->pData );
         }
+        assert( If_ObjLevel(pIfObj) == Aig_ObjLevel(pNode) );
     }
     return pIfMan;
 }
@@ -243,7 +238,7 @@ Hop_Obj_t * Nwk_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t *
   SeeAlso     []
 
 ***********************************************************************/
-Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p )
+Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToIf )
 {
     Nwk_Man_t * pNtk;
     Nwk_Obj_t * pObjNew;
@@ -261,7 +256,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p )
     pNtk->pSpec = Aig_UtilStrsav( p->pSpec );
     Aig_ManForEachObj( p, pObj, i )
     {
-        pIfObj = If_ManObj( pIfMan, i );
+        pIfObj = Vec_PtrEntry( vAigToIf, i );
         if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) )
             continue;
         if ( Aig_ObjIsNode(pObj) )
@@ -312,12 +307,13 @@ Nwk_Man_t * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars
 {
     Nwk_Man_t * pNtk;
     If_Man_t * pIfMan;
-    // perform FPGA mapping
+    Vec_Ptr_t * vAigToIf;
     // set the arrival times
     pPars->pTimesArr = ALLOC( float, Aig_ManPiNum(p) );
     memset( pPars->pTimesArr, 0, sizeof(float) * Aig_ManPiNum(p) );
     // translate into the mapper
-    pIfMan = Nwk_ManToIf( p, pPars );    
+    vAigToIf = Vec_PtrStart( Aig_ManObjNumMax(p) );
+    pIfMan = Nwk_ManToIf( p, pPars, vAigToIf );    
     if ( pIfMan == NULL )
         return NULL;
     pIfMan->pManTim = Tim_ManDup( pManTime, 0 );
@@ -327,8 +323,9 @@ Nwk_Man_t * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars
         return NULL;
     }
     // transform the result of mapping into the new network
-    pNtk = Nwk_ManFromIf( pIfMan, p );
+    pNtk = Nwk_ManFromIf( pIfMan, p, vAigToIf );
     If_ManStop( pIfMan );
+    Vec_PtrFree( vAigToIf );
     return pNtk;
 }
 
diff --git a/src/aig/nwk/nwkObj.c b/src/aig/nwk/nwkObj.c
index 0806eecf..6d1f0428 100644
--- a/src/aig/nwk/nwkObj.c
+++ b/src/aig/nwk/nwkObj.c
@@ -194,7 +194,6 @@ void Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj )
     Vec_PtrFree( vNodes );
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/nwk/nwkStrash.c b/src/aig/nwk/nwkStrash.c
index 668889a6..627bfa67 100644
--- a/src/aig/nwk/nwkStrash.c
+++ b/src/aig/nwk/nwkStrash.c
@@ -95,11 +95,13 @@ Aig_Obj_t * Nwk_ManStrashNode( Aig_Man_t * p, Nwk_Obj_t * pObj )
 ***********************************************************************/
 Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
 {
-    Aig_Man_t * pMan;
+    Aig_Man_t * pMan;//, * pTemp;
     Aig_Obj_t * pObjNew;
     Nwk_Obj_t * pObj;
     int i, Level;
     pMan = Aig_ManStart( Nwk_ManGetAigNodeNum(pNtk) );
+    pMan->pName = Aig_UtilStrsav( pNtk->pName );
+    pMan->pSpec = Aig_UtilStrsav( pNtk->pSpec );
     pMan->pManTime = Tim_ManDup( pNtk->pManTime, 1 );
     Tim_ManIncrementTravId( pMan->pManTime );
     Nwk_ManForEachObj( pNtk, pObj, i )
@@ -125,6 +127,8 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
         pObj->pCopy = pObjNew;
     }
     Aig_ManCleanup( pMan );
+//    pMan = Aig_ManDup( pTemp = pMan, 1 );
+//    Aig_ManStop( pTemp );
     return pMan;
 }
 
diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c
index 0cbcb7f8..5e4967da 100644
--- a/src/aig/nwk/nwkTiming.c
+++ b/src/aig/nwk/nwkTiming.c
@@ -24,10 +24,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int   Nwk_ManTimeEqual( float f1, float f2, float Eps )  { return (f1 < f2 + Eps) && (f2 < f1 + Eps);  }
-static inline int   Nwk_ManTimeLess( float f1, float f2, float Eps )   { return (f1 < f2 + Eps);                     }
-static inline int   Nwk_ManTimeMore( float f1, float f2, float Eps )   { return (f1 + Eps > f2);                     }
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -100,7 +96,7 @@ void Nwk_ManDelayTraceSortPins( Nwk_Obj_t * pNode, int * pPinPerm, float * pPinD
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the arrival times for the given node.]
+  Synopsis    [Sorts the pins in the decreasing order of delays.]
 
   Description []
                
@@ -109,14 +105,39 @@ void Nwk_ManDelayTraceSortPins( Nwk_Obj_t * pNode, int * pPinPerm, float * pPinD
   SeeAlso     []
 
 ***********************************************************************/
-float Nwk_NodeComputeArrival( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSorting )
+int Nwk_ManWhereIsPin( Nwk_Obj_t * pFanout, Nwk_Obj_t * pFanin, int * pPinPerm )
 {
+    int i;
+    for ( i = 0; i < Nwk_ObjFaninNum(pFanout); i++ )
+        if ( Nwk_ObjFanin(pFanout, pPinPerm[i]) == pFanin )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the arrival times for the given object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Nwk_NodeComputeArrival( Nwk_Obj_t * pObj, int fUseSorting )
+{
+    If_Lib_t * pLutLib = pObj->pMan->pLutLib;
     int pPinPerm[32];
     float pPinDelays[32];
     Nwk_Obj_t * pFanin;
     float tArrival, * pDelays;
     int k;
-    assert( Nwk_ObjIsNode(pObj) );
+    assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) || Nwk_ObjIsCo(pObj) );
+    if ( Nwk_ObjIsCi(pObj) )
+        return Nwk_ObjArrival(pObj);
+    if ( Nwk_ObjIsCo(pObj) )
+        return Nwk_ObjArrival( Nwk_ObjFanin0(pObj) );
     tArrival = -AIG_INFINITY;
     if ( pLutLib == NULL )
     {
@@ -164,28 +185,35 @@ float Nwk_NodeComputeArrival( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSort
   SeeAlso     []
 
 ***********************************************************************/
-float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSorting )
+float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, int fUseSorting )
 {
+    If_Lib_t * pLutLib = pObj->pMan->pLutLib;
     int pPinPerm[32];
     float pPinDelays[32];
     Nwk_Obj_t * pFanout;
-    float tRequired, * pDelays;
-    int k;
-    assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) );
+    float tRequired, tDelay, * pDelays;
+    int k, iFanin;
+    assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) || Nwk_ObjIsCo(pObj) );
+    if ( Nwk_ObjIsCo(pObj) )
+        return Nwk_ObjRequired(pObj);
     tRequired = AIG_INFINITY;
     if ( pLutLib == NULL )
     {
         Nwk_ObjForEachFanout( pObj, pFanout, k )
-            if ( tRequired > Nwk_ObjRequired(pFanout) - 1.0 )
-                tRequired = Nwk_ObjRequired(pFanout) - 1.0;
+        {
+            tDelay = Nwk_ObjIsCo(pFanout)? 0.0 : 1.0;
+            if ( tRequired > Nwk_ObjRequired(pFanout) - tDelay )
+                tRequired = Nwk_ObjRequired(pFanout) - tDelay;
+        }
     }
     else if ( !pLutLib->fVarPinDelays )
     {
         Nwk_ObjForEachFanout( pObj, pFanout, k )
         {
             pDelays = pLutLib->pLutDelays[Nwk_ObjFaninNum(pFanout)];
-            if ( tRequired > Nwk_ObjRequired(pFanout) - pDelays[0] )
-                tRequired = Nwk_ObjRequired(pFanout) - pDelays[0];
+            tDelay = Nwk_ObjIsCo(pFanout)? 0.0 : pDelays[0];
+            if ( tRequired > Nwk_ObjRequired(pFanout) - tDelay )
+                tRequired = Nwk_ObjRequired(pFanout) - tDelay;
         }
     }
     else
@@ -196,8 +224,11 @@ float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSor
             {
                 pDelays = pLutLib->pLutDelays[Nwk_ObjFaninNum(pFanout)];
                 Nwk_ManDelayTraceSortPins( pFanout, pPinPerm, pPinDelays );
-                if ( tRequired > Nwk_ObjRequired(Nwk_ObjFanout(pObj,pPinPerm[k])) - pDelays[k] )
-                    tRequired = Nwk_ObjRequired(Nwk_ObjFanout(pObj,pPinPerm[k])) - pDelays[k];
+                iFanin = Nwk_ManWhereIsPin( pFanout, pObj, pPinPerm );
+                assert( Nwk_ObjFanin(pFanout,pPinPerm[iFanin]) == pObj );
+                tDelay = Nwk_ObjIsCo(pFanout)? 0.0 : pDelays[iFanin];
+                if ( tRequired > Nwk_ObjRequired(pFanout) - tDelay )
+                    tRequired = Nwk_ObjRequired(pFanout) - tDelay;
             }
         }
         else
@@ -205,8 +236,11 @@ float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSor
             Nwk_ObjForEachFanout( pObj, pFanout, k )
             {
                 pDelays = pLutLib->pLutDelays[Nwk_ObjFaninNum(pFanout)];
-                if ( tRequired > Nwk_ObjRequired(pFanout) - pDelays[k] )
-                    tRequired = Nwk_ObjRequired(pFanout) - pDelays[k];
+                iFanin = Nwk_ObjFindFanin( pFanout, pObj );
+                assert( Nwk_ObjFanin(pFanout,iFanin) == pObj );
+                tDelay = Nwk_ObjIsCo(pFanout)? 0.0 : pDelays[iFanin];
+                if ( tRequired > Nwk_ObjRequired(pFanout) - tDelay )
+                    tRequired = Nwk_ObjRequired(pFanout) - tDelay;
             }
         }
     }
@@ -224,8 +258,9 @@ float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSor
   SeeAlso     []
 
 ***********************************************************************/
-float Nwk_NodePropagateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSorting )
+float Nwk_NodePropagateRequired( Nwk_Obj_t * pObj, int fUseSorting )
 {
+    If_Lib_t * pLutLib = pObj->pMan->pLutLib;
     int pPinPerm[32];
     float pPinDelays[32];
     Nwk_Obj_t * pFanin;
@@ -284,9 +319,10 @@ float Nwk_NodePropagateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseS
   SeeAlso     []
 
 ***********************************************************************/
-float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
+float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk )
 {
     int fUseSorting = 1;
+    If_Lib_t * pLutLib = pNtk->pLutLib;
     Vec_Ptr_t * vNodes;
     Nwk_Obj_t * pObj;
     float tArrival, tRequired, tSlack;
@@ -311,22 +347,11 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
         Tim_ManIncrementTravId( pNtk->pManTime );
     Nwk_ManForEachObj( pNtk, pObj, i )
     {
-        if ( Nwk_ObjIsNode(pObj) )
-        {
-            tArrival = Nwk_NodeComputeArrival( pObj, pLutLib, fUseSorting );
-        }
-        else if ( Nwk_ObjIsCi(pObj) )
-        {
-            tArrival = pNtk->pManTime? Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId ) : (float)0.0;
-        }
-        else if ( Nwk_ObjIsCo(pObj) )
-        {
-            tArrival = Nwk_ObjArrival( Nwk_ObjFanin0(pObj) );
-            if ( pNtk->pManTime )
-                Tim_ManSetPoArrival( pNtk->pManTime, pObj->PioId, tArrival );
-        }
-        else
-            assert( 0 );
+        tArrival = Nwk_NodeComputeArrival( pObj, fUseSorting );
+        if ( Nwk_ObjIsCo(pObj) && pNtk->pManTime )
+            Tim_ManSetPoArrival( pNtk->pManTime, pObj->PioId, tArrival );
+        if ( Nwk_ObjIsCi(pObj) && pNtk->pManTime )
+            tArrival = Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId );
         Nwk_ObjSetArrival( pObj, tArrival );
     }
 
@@ -343,15 +368,17 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
         Tim_ManSetPoRequiredAll( pNtk->pManTime, tArrival );
     }
     else
-        Nwk_ManForEachPo( pNtk, pObj, i )
+    {
+        Nwk_ManForEachCo( pNtk, pObj, i )
             Nwk_ObjSetRequired( pObj, tArrival );
+    }
 
     // propagate the required times
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         if ( Nwk_ObjIsNode(pObj) )
         {
-            Nwk_NodePropagateRequired( pObj, pLutLib, fUseSorting );
+            Nwk_NodePropagateRequired( pObj, fUseSorting );
         }
         else if ( Nwk_ObjIsCi(pObj) )
         {
@@ -370,7 +397,7 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
 
         // set slack for this object
         tSlack = Nwk_ObjRequired(pObj) - Nwk_ObjArrival(pObj);
-        assert( tSlack + 0.001 > 0.0 );
+        assert( tSlack + 0.01 > 0.0 );
         Nwk_ObjSetSlack( pObj, tSlack < 0.0 ? 0.0 : tSlack );
     }
     Vec_PtrFree( vNodes );
@@ -379,6 +406,38 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the arrival times for the given node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManVerifyTiming(  Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pObj;
+    float tArrival, tRequired;
+    int i;
+    Nwk_ManForEachObj( pNtk, pObj, i )
+    {
+        tArrival = Nwk_NodeComputeArrival( pObj, 1 );
+        tRequired = Nwk_NodeComputeRequired( pObj, 1 );
+        if ( Nwk_ObjIsCi(pObj) && pNtk->pManTime )
+            tArrival = Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId );
+        if ( Nwk_ObjIsCo(pObj) && pNtk->pManTime )
+            tArrival = Tim_ManGetPoRequired( pNtk->pManTime, pObj->PioId );
+        if ( !Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pObj), (float)0.01 ) )
+            printf( "Nwk_ManVerifyTiming(): Arrival time of object %d is incorrect.\n", pObj->Id );
+        if ( !Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.01 ) )
+            printf( "Nwk_ManVerifyTiming(): Required time of object %d is incorrect.\n", pObj->Id );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prints the delay trace for the given network.]
 
   Description []
@@ -388,8 +447,9 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
   SeeAlso     []
 
 ***********************************************************************/
-void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
+void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk )
 {
+    If_Lib_t * pLutLib = pNtk->pLutLib;
     Nwk_Obj_t * pNode;
     int i, Nodes, * pCounters;
     float tArrival, tDelta, nSteps, Num;
@@ -401,11 +461,11 @@ void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
         return;
     }
     // decide how many steps
-    nSteps = pLutLib ? 20 : Nwk_ManLevel(pNtk);
+    nSteps = pLutLib ? 20 : Nwk_ManLevelMax(pNtk);
     pCounters = ALLOC( int, nSteps + 1 );
     memset( pCounters, 0, sizeof(int)*(nSteps + 1) );
     // perform delay trace
-    tArrival = Nwk_ManDelayTraceLut( pNtk, pLutLib );
+    tArrival = Nwk_ManDelayTraceLut( pNtk );
     tDelta = tArrival / nSteps;
     // count how many nodes have slack in the corresponding intervals
     Nwk_ManForEachNode( pNtk, pNode, i )
@@ -491,39 +551,66 @@ void Nwk_NodeUpdateAddToQueue( Vec_Ptr_t * vQueue, Nwk_Obj_t * pObj, int iCurren
   SeeAlso     []
 
 ***********************************************************************/
-void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj, If_Lib_t * pLutLib )
+void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj )
 {
+    If_Lib_t * pLutLib = pObj->pMan->pLutLib;
     Tim_Man_t * pManTime = pObj->pMan->pManTime;
     Vec_Ptr_t * vQueue = pObj->pMan->vTemp;
     Nwk_Obj_t * pTemp, * pNext;
     float tArrival;
-    int i, k;
+    int i, k, iBox, iTerm1, nTerms;
     assert( Nwk_ObjIsNode(pObj) );
+    // verify the arrival time
+    tArrival = Nwk_NodeComputeArrival( pObj, 1 );
+    assert( Nwk_ManTimeLess( tArrival, Nwk_ObjRequired(pObj), (float)0.01 ) );
     // initialize the queue with the node
     Vec_PtrClear( vQueue );
     Vec_PtrPush( vQueue, pObj );
     pObj->MarkA = 1;
     // process objects
-    Tim_ManTravIdDisable( pManTime );
+    if ( pManTime )
+        Tim_ManIncrementTravId( pManTime );
     Vec_PtrForEachEntry( vQueue, pTemp, i )
     {
         pTemp->MarkA = 0;
-        tArrival = Nwk_NodeComputeArrival( pTemp, pLutLib, 1 );
-        if ( Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pTemp), (float)0.001 ) )
+        tArrival = Nwk_NodeComputeArrival( pTemp, 1 );
+        if ( Nwk_ObjIsCi(pTemp) && pManTime )
+            tArrival = Tim_ManGetPiArrival( pManTime, pTemp->PioId );
+        if ( Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pTemp), (float)0.01 ) )
             continue;
         Nwk_ObjSetArrival( pTemp, tArrival );
         // add the fanouts to the queue
-        Nwk_ObjForEachFanout( pTemp, pNext, k )
+        if ( Nwk_ObjIsCo(pTemp) )
+        {
+            if ( pManTime )
+            {
+                Tim_ManSetPoArrival( pManTime, pTemp->PioId, tArrival );
+                iBox = Tim_ManBoxForCo( pManTime, pNext->PioId );
+                Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
+                if ( iBox >= 0 ) // this is not a true PO
+                {
+                    iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox );
+                    nTerms = Tim_ManBoxOutputNum( pManTime, iBox );
+                    for ( i = 0; i < nTerms; i++ )
+                    {
+                        pNext = Nwk_ManCi(pNext->pMan, iTerm1 + i);
+                        if ( pNext->MarkA )
+                            continue;
+                        Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
+                        pNext->MarkA = 1;
+                    }
+                }
+            }
+        }
+        else
         {
-            if ( Nwk_ObjIsCo(pNext) )
+            Nwk_ObjForEachFanout( pTemp, pNext, k )
             {
-                Nwk_ObjSetArrival( pNext, tArrival );
-                continue;
+                if ( pNext->MarkA )
+                    continue;
+                Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
+                pNext->MarkA = 1;
             }
-            if ( pNext->MarkA )
-                continue;
-            Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
-            pNext->MarkA = 1;
         }
     }
 }
@@ -539,18 +626,27 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj, If_Lib_t * pLutLib )
   SeeAlso     []
 
 ***********************************************************************/
-void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib )
+void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj )
 {
+    If_Lib_t * pLutLib = pObj->pMan->pLutLib;
     Tim_Man_t * pManTime = pObj->pMan->pManTime;
     Vec_Ptr_t * vQueue = pObj->pMan->vTemp;
     Nwk_Obj_t * pTemp, * pNext;
     float tRequired;
-    int i, k; 
+    int i, k, iBox, iTerm1, nTerms;
     assert( Nwk_ObjIsNode(pObj) );
+
+if ( pObj->Id == 1384 )
+{
+    int x = 0;
+//    Nwk_ObjPrint( Nwk_ManObj(pObj->pMan, 1384) );
+//    Nwk_ObjPrint( Nwk_ManObj(pObj->pMan, 422) );
+}
+
     // make sure the node's required time remained the same
-    tRequired = Nwk_NodeComputeRequired( pObj, pLutLib, 1 );
-    assert( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.001 ) );
-    // initialize the queue with the node's fanins
+    tRequired = Nwk_NodeComputeRequired( pObj, 1 );
+    assert( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.01 ) );
+    // initialize the queue with the node's faninsa and the old node's fanins
     Vec_PtrClear( vQueue );
     Nwk_ObjForEachFanin( pObj, pNext, k )
     {
@@ -560,21 +656,49 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib )
         pNext->MarkA = 1;
     }
     // process objects
-    Tim_ManTravIdDisable( pManTime );
+    if ( pManTime )
+        Tim_ManIncrementTravId( pManTime );
     Vec_PtrForEachEntry( vQueue, pTemp, i )
     {
         pTemp->MarkA = 0;
-        tRequired = Nwk_NodeComputeRequired( pTemp, pLutLib, 1 );
-        if ( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pTemp), (float)0.001 ) )
+        tRequired = Nwk_NodeComputeRequired( pTemp, 1 );
+        if ( Nwk_ObjIsCo(pTemp) && pManTime )
+            tRequired = Tim_ManGetPoRequired( pManTime, pTemp->PioId );
+        if ( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pTemp), (float)0.01 ) )
             continue;
         Nwk_ObjSetRequired( pTemp, tRequired );
-        // schedule fanins of the node
-        Nwk_ObjForEachFanin( pTemp, pNext, k )
+        // add the fanouts to the queue
+        if ( Nwk_ObjIsCi(pTemp) )
         {
-            if ( pNext->MarkA )
-                continue;
-            Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 0 );
-            pNext->MarkA = 1;
+            if ( pManTime )
+            {
+                Tim_ManSetPiRequired( pManTime, pTemp->PioId, tRequired );
+                iBox = Tim_ManBoxForCi( pManTime, pNext->PioId );
+                Tim_ManSetCurrentTravIdBoxOutputs( pManTime, iBox );
+                if ( iBox >= 0 ) // this is not a true PO
+                {
+                    iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
+                    nTerms = Tim_ManBoxInputNum( pManTime, iBox );
+                    for ( i = 0; i < nTerms; i++ )
+                    {
+                        pNext = Nwk_ManCo(pNext->pMan, iTerm1 + i);
+                        if ( pNext->MarkA )
+                            continue;
+                        Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 0 );
+                        pNext->MarkA = 1;
+                    }
+                }
+            }
+        }
+        else
+        {
+            Nwk_ObjForEachFanin( pTemp, pNext, k )
+            {
+                if ( pNext->MarkA )
+                    continue;
+                Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 0 );
+                pNext->MarkA = 1;
+            }
         }
     }
 }
@@ -592,10 +716,28 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib )
 ***********************************************************************/
 int Nwk_ObjLevelNew( Nwk_Obj_t * pObj )
 {
+    Tim_Man_t * pManTime = pObj->pMan->pManTime;
     Nwk_Obj_t * pFanin;
-    int i, Level = 0;
+    int i, iBox, iTerm1, nTerms, Level = 0;
     if ( Nwk_ObjIsCi(pObj) || Nwk_ObjIsLatch(pObj) )
-        return 0;
+    {
+        if ( pManTime )
+        {
+            iBox = Tim_ManBoxForCi( pManTime, pObj->PioId );
+            if ( iBox >= 0 ) // this is not a true PI
+            {
+                iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
+                nTerms = Tim_ManBoxInputNum( pManTime, iBox );
+                for ( i = 0; i < nTerms; i++ )
+                {
+                    pFanin = Nwk_ManCo(pObj->pMan, iTerm1 + i);
+                    Level = AIG_MAX( Level, Nwk_ObjLevel(pFanin) );
+                }
+                Level++;
+            }
+        }
+        return Level;
+    }
     assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) );
     Nwk_ObjForEachFanin( pObj, pFanin, i )
         Level = AIG_MAX( Level, Nwk_ObjLevel(pFanin) );
@@ -615,9 +757,10 @@ int Nwk_ObjLevelNew( Nwk_Obj_t * pObj )
 ***********************************************************************/
 void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj )
 {
+    Tim_Man_t * pManTime = pObj->pMan->pManTime;
     Vec_Ptr_t * vQueue = pObj->pMan->vTemp;
     Nwk_Obj_t * pTemp, * pNext;
-    int LevelNew, i, k;
+    int LevelNew, i, k, iBox, iTerm1, nTerms;
     assert( Nwk_ObjIsNode(pObj) );
     // initialize the queue with the node
     Vec_PtrClear( vQueue );
@@ -632,17 +775,36 @@ void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj )
             continue;
         Nwk_ObjSetLevel( pTemp, LevelNew );
         // add the fanouts to the queue
-        Nwk_ObjForEachFanout( pTemp, pNext, k )
+        if ( Nwk_ObjIsCo(pTemp) )
+        {
+            if ( pManTime )
+            {
+                iBox = Tim_ManBoxForCo( pManTime, pNext->PioId );
+                Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
+                if ( iBox >= 0 ) // this is not a true PO
+                {
+                    iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox );
+                    nTerms = Tim_ManBoxOutputNum( pManTime, iBox );
+                    for ( i = 0; i < nTerms; i++ )
+                    {
+                        pNext = Nwk_ManCi(pNext->pMan, iTerm1 + i);
+                        if ( pNext->MarkA )
+                            continue;
+                        Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
+                        pNext->MarkA = 1;
+                    }
+                }
+            }
+        }
+        else
         {
-            if ( Nwk_ObjIsCo(pNext) )
+            Nwk_ObjForEachFanout( pTemp, pNext, k )
             {
-                Nwk_ObjSetLevel( pNext, LevelNew );
-                continue;
+                if ( pNext->MarkA )
+                    continue;
+                Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
+                pNext->MarkA = 1;
             }
-            if ( pNext->MarkA )
-                continue;
-            Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
-            pNext->MarkA = 1;
         }
     }
 }
@@ -658,7 +820,7 @@ void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Nwk_ManVerifyLevel( Nwk_Man_t * pNtk )
+int Nwk_ManVerifyLevel( Nwk_Man_t * pNtk )
 {
     Nwk_Obj_t * pObj;
     int LevelNew, i;
@@ -672,6 +834,7 @@ void Nwk_ManVerifyLevel( Nwk_Man_t * pNtk )
                 i, Nwk_ObjLevel(pObj), LevelNew );
         }
     }
+    return 1;
 }
 
 /**Function*************************************************************
@@ -687,6 +850,14 @@ void Nwk_ManVerifyLevel( Nwk_Man_t * pNtk )
 ***********************************************************************/
 void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels )
 {
+//    float Temp;
+    assert( pObj->pMan == pObjNew->pMan );
+    assert( pObj != pObjNew );
+    assert( Nwk_ObjFanoutNum(pObj) > 0 );
+    assert( Nwk_ObjIsNode(pObj) && !Nwk_ObjIsCo(pObjNew) );
+//    Temp = Nwk_NodeComputeRequired( pObj, 1 );
+    // transfer fanouts to the old node
+    Nwk_ObjTransferFanout( pObj, pObjNew );
     // transfer the timing information
     // (this is needed because updating level happens if the level has changed;
     // when we set the old level, it will be recomputed by the level updating
@@ -694,13 +865,16 @@ void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels )
     pObjNew->Level = pObj->Level;
     pObjNew->tArrival = pObj->tArrival;
     pObjNew->tRequired = pObj->tRequired;
-    // replace the old node by the new node
-    Nwk_ObjReplace( pObj, pObjNew );
-    // update the level of the node
+    // update required times of the old fanins
+    pObj->tRequired = AIG_INFINITY;
+    Nwk_NodeUpdateRequired( pObj );
+    // remove the old node
+    Nwk_ManDeleteNode_rec( pObj );
+    // update the information of the new node
     Nwk_ManUpdateLevel( pObjNew );
-//Nwk_ManVerifyLevel( pObjNew->pMan );
-//    Nwk_NodeUpdateArrival( pObjNew, pObj->pMan->pLutLib );
-//    Nwk_NodeUpdateRequired( pObjNew, pObj->pMan->pLutLib );
+    Nwk_NodeUpdateArrival( pObjNew );
+    Nwk_NodeUpdateRequired( pObjNew );
+//Nwk_ManVerifyTiming( pObjNew->pMan );
 }
 
 
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index 47e76844..b25fd68a 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -207,6 +207,38 @@ int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 )
     return 0; 
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ObjPrint( Nwk_Obj_t * pObj )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    printf( "ObjId = %5d.  ", pObj->Id );
+    if ( Nwk_ObjIsPi(pObj) )
+        printf( "PI" );
+    if ( Nwk_ObjIsPo(pObj) )
+        printf( "PO" );
+    if ( Nwk_ObjIsNode(pObj) )
+        printf( "Node" );
+    printf( "   Fanins = " );
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        printf( "%d ", pNext->Id );
+    printf( "   Fanouts = " );
+    Nwk_ObjForEachFanout( pObj, pNext, i )
+        printf( "%d ", pNext->Id );
+    printf( "\n" );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////