Version abc80327

11 files changed, 829 insertions, 200 deletions

diff --git a/src/aig/ntk/module.make b/src/aig/ntk/module.make
new file mode 100644
index 00000000..b668de2f
--- /dev/null
+++ b/src/aig/ntk/module.make
@@ -0,0 +1,9 @@
+SRC +=    src/aig/ntk/ntkCheck.c \
+    src/aig/ntk/ntkBidec.c \
+    src/aig/ntk/ntkDfs.c \
+    src/aig/ntk/ntkFanio.c \
+    src/aig/ntk/ntkMan.c \
+    src/aig/ntk/ntkMap.c \
+    src/aig/ntk/ntkObj.c \
+    src/aig/ntk/ntkTiming.c \
+    src/aig/ntk/ntkUtil.c
diff --git a/src/aig/ntk/ntk.h b/src/aig/ntk/ntk.h
index 6ddfac81..2fcb6ddc 100644
--- a/src/aig/ntk/ntk.h
+++ b/src/aig/ntk/ntk.h
@@ -30,7 +30,9 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 #include "aig.h"
+#include "hop.h"
 #include "tim.h"
+#include "if.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -66,7 +68,7 @@ struct Ntk_Man_t_
     int                nObjs[NTK_OBJ_VOID]; // counter of objects of each type
     int                nFanioPlus;     // the number of extra fanins/fanouts alloc by default
     // functionality, timing, memory, etc
-    Aig_Man_t *        pAig;           // the functionality representation
+    Hop_Man_t *        pManHop;        // the functionality representation
     Tim_Man_t *        pManTime;       // the timing manager
     Aig_MmFlex_t *     pMemObjs;       // memory for objects
     Vec_Ptr_t *        vTemp;          // array used for incremental updates
@@ -77,9 +79,10 @@ struct Ntk_Obj_t_
 {
     Ntk_Man_t *        pMan;           // the manager  
     void *             pCopy;          // temporary pointer
-    void *             pFunc;          // functionality
+    Hop_Obj_t *        pFunc;          // functionality
     // node information
     int                Id;             // unique ID
+    int                PioId;          // number of this node in the PI/PO list
     unsigned           Type     :  3;  // object type
     unsigned           fCompl   :  1;  // complemented attribute
     unsigned           MarkA    :  1;  // temporary mark  
@@ -113,6 +116,10 @@ static inline int         Ntk_ManLatchNum( Ntk_Man_t * p )        { return p->nO
 static inline int         Ntk_ManBoxNum( Ntk_Man_t * p )          { return p->nObjs[NTK_OBJ_BOX];               } 
 static inline int         Ntk_ManObjNumMax( Ntk_Man_t * p )       { return Vec_PtrSize(p->vObjs);               }
 
+static inline Ntk_Obj_t * Ntk_ManCi( Ntk_Man_t * p, int i )       { return Vec_PtrEntry( p->vCis, i );          } 
+static inline Ntk_Obj_t * Ntk_ManCo( Ntk_Man_t * p, int i )       { return Vec_PtrEntry( p->vCos, i );          } 
+static inline Ntk_Obj_t * Ntk_ManObj( Ntk_Man_t * p, int i )      { return Vec_PtrEntry( p->vObjs, i );         } 
+
 static inline int         Ntk_ObjFaninNum( Ntk_Obj_t * p )        { return p->nFanins;                          } 
 static inline int         Ntk_ObjFanoutNum( Ntk_Obj_t * p )       { return p->nFanouts;                         } 
 
@@ -126,8 +133,8 @@ static inline int         Ntk_ObjIsCo( Ntk_Obj_t * p )            { return p->Ty
 static inline int         Ntk_ObjIsNode( Ntk_Obj_t * p )          { return p->Type == NTK_OBJ_NODE;             } 
 static inline int         Ntk_ObjIsLatch( Ntk_Obj_t * p )         { return p->Type == NTK_OBJ_LATCH;            } 
 static inline int         Ntk_ObjIsBox( Ntk_Obj_t * p )           { return p->Type == NTK_OBJ_BOX;              } 
-static inline int         Ntk_ObjIsPi( Ntk_Obj_t * p )            { return Ntk_ObjFaninNum(p) == 0 || (Ntk_ObjFaninNum(p) == 1 && Ntk_ObjIsLatch(Ntk_ObjFanin0(p)));   } 
-static inline int         Ntk_ObjIsPo( Ntk_Obj_t * p )            { return Ntk_ObjFanoutNum(p)== 0 || (Ntk_ObjFanoutNum(p)== 1 && Ntk_ObjIsLatch(Ntk_ObjFanout0(p)));  } 
+static inline int         Ntk_ObjIsPi( Ntk_Obj_t * p )            { return Ntk_ObjIsCi(p) && Tim_ManBoxForCi(p->pMan->pManTime, p->PioId) == -1; } 
+static inline int         Ntk_ObjIsPo( Ntk_Obj_t * p )            { return Ntk_ObjIsCo(p) && Tim_ManBoxForCo(p->pMan->pManTime, p->PioId) == -1;  }
 
 static inline float       Ntk_ObjArrival( Ntk_Obj_t * pObj )                 { return pObj->tArrival;           }
 static inline float       Ntk_ObjRequired( Ntk_Obj_t * pObj )                { return pObj->tRequired;          }
@@ -181,42 +188,41 @@ static inline int         Ntk_ObjIsTravIdPrevious( Ntk_Obj_t * pObj )        { r
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== ntlDfs.c ==========================================================*/
+/*=== ntkDfs.c ==========================================================*/
+extern int             Ntk_ManLevel( Ntk_Man_t * pNtk );
+extern int             Ntk_ManLevel2( Ntk_Man_t * pNtk );
 extern Vec_Ptr_t *     Ntk_ManDfs( Ntk_Man_t * pNtk );
 extern Vec_Ptr_t *     Ntk_ManDfsReverse( Ntk_Man_t * pNtk );
-/*=== ntlFanio.c ==========================================================*/
+/*=== ntkFanio.c ==========================================================*/
 extern void            Ntk_ObjCollectFanins( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes );
 extern void            Ntk_ObjCollectFanouts( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes );
 extern void            Ntk_ObjAddFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanin );
 extern void            Ntk_ObjDeleteFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanin );
 extern void            Ntk_ObjPatchFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFaninOld, Ntk_Obj_t * pFaninNew );
 extern void            Ntk_ObjReplace( Ntk_Obj_t * pNodeOld, Ntk_Obj_t * pNodeNew );
-/*=== ntlMan.c ============================================================*/
+/*=== ntkMan.c ============================================================*/
 extern Ntk_Man_t *     Ntk_ManAlloc();
 extern void            Ntk_ManFree( Ntk_Man_t * p );
-extern void            Ntk_ManPrintStats( Ntk_Man_t * p );
-/*=== ntlMap.c ============================================================*/
-extern Ntk_Man_t *     Ntk_MappingIf( Aig_Man_t * p, void * pPars );
-/*=== ntlObj.c ============================================================*/
-extern Ntk_Obj_t *     Ntk_ManCreatePi( Ntk_Man_t * pMan );
-extern Ntk_Obj_t *     Ntk_ManCreatePo( Ntk_Man_t * pMan );
+extern void            Ntk_ManPrintStats( Ntk_Man_t * p, If_Lib_t * pLutLib );
+/*=== ntkMap.c ============================================================*/
+/*=== ntkObj.c ============================================================*/
+extern Ntk_Obj_t *     Ntk_ManCreateCi( Ntk_Man_t * pMan, int nFanouts );
+extern Ntk_Obj_t *     Ntk_ManCreateCo( Ntk_Man_t * pMan );
 extern Ntk_Obj_t *     Ntk_ManCreateNode( Ntk_Man_t * pMan, int nFanins, int nFanouts );
 extern Ntk_Obj_t *     Ntk_ManCreateBox( Ntk_Man_t * pMan, int nFanins, int nFanouts );
 extern Ntk_Obj_t *     Ntk_ManCreateLatch( Ntk_Man_t * pMan );
 extern void            Ntk_ManDeleteNode( Ntk_Obj_t * pObj );
 extern void            Ntk_ManDeleteNode_rec( Ntk_Obj_t * pObj );
-/*=== ntlUtil.c ============================================================*/
+/*=== ntkTiming.c ============================================================*/
+extern float           Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, If_Lib_t * pLutLib );
+extern void            Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, If_Lib_t * pLutLib );
+/*=== ntkUtil.c ============================================================*/
 extern void            Ntk_ManIncrementTravId( Ntk_Man_t * pNtk );
 extern int             Ntk_ManGetFaninMax( Ntk_Man_t * pNtk );
 extern int             Ntk_ManGetTotalFanins( Ntk_Man_t * pNtk );
-extern int             Ntk_ManLevel( Ntk_Man_t * pNtk );
 extern int             Ntk_ManPiNum( Ntk_Man_t * pNtk );
 extern int             Ntk_ManPoNum( Ntk_Man_t * pNtk );
-
-/*=== ntlReadBlif.c ==========================================================*/
-extern Ntk_Man_t *     Ioa_ReadBlif( char * pFileName, int fCheck );
-/*=== ntlWriteBlif.c ==========================================================*/
-extern void            Ioa_WriteBlif( Ntk_Man_t * p, char * pFileName );
+extern int             Ntk_ManGetAigNodeNum( Ntk_Man_t * pNtk );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ntk/ntkBidec.c b/src/aig/ntk/ntkBidec.c
new file mode 100644
index 00000000..43426d13
--- /dev/null
+++ b/src/aig/ntk/ntkBidec.c
@@ -0,0 +1,123 @@
+/**CFile****************************************************************
+
+  FileName    [ntkBidec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Bi-decomposition of local functions.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntkBidec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntk.h"
+#include "bdc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj )  { return Hop_NotCond( Bdc_FuncCopy(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) );  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes nodes using bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Ntk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare )
+{
+    unsigned * pTruth;
+    Bdc_Fun_t * pFunc;
+    int nNodes, i;
+    assert( nVars <= 16 );
+    // derive truth table
+    pTruth = Hop_ManConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
+    if ( Hop_IsComplement(pRoot) )
+        for ( i = Aig_TruthWordNum(nVars)-1; i >= 0; i-- )
+            pTruth[i] = ~pTruth[i];
+    // decompose truth table
+    Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 );
+    // convert back into HOP
+    Bdc_FuncSetCopy( Bdc_ManFunc( p, 0 ), Hop_ManConst1( pHop ) );
+    for ( i = 0; i < nVars; i++ )
+        Bdc_FuncSetCopy( Bdc_ManFunc( p, i+1 ), Hop_ManPi( pHop, i ) );
+    nNodes = Bdc_ManNodeNum(p);
+    for ( i = nVars + 1; i < nNodes; i++ )
+    {
+        pFunc = Bdc_ManFunc( p, i );
+        Bdc_FuncSetCopy( pFunc, Hop_And( pHop, Bdc_FunCopyHop(Bdc_FuncFanin0(pFunc)), Bdc_FunCopyHop(Bdc_FuncFanin1(pFunc)) ) );
+    }
+    return Bdc_FunCopyHop( Bdc_ManRoot(p) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes nodes using bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManBidecResyn( Ntk_Man_t * pNtk, int fVerbose )
+{
+    Bdc_Par_t Pars = {0}, * pPars = &Pars;
+    Bdc_Man_t * p;
+    Ntk_Obj_t * pObj;
+    Vec_Int_t * vTruth;
+    int i, nGainTotal = 0, nNodes1, nNodes2;
+    int clk = clock();
+    pPars->nVarsMax = Ntk_ManGetFaninMax( pNtk );
+    pPars->fVerbose = fVerbose;
+    if ( pPars->nVarsMax > 15 )
+    {
+        if ( fVerbose )
+        printf( "Resynthesis is not performed for nodes with more than 15 inputs.\n" );
+        pPars->nVarsMax = 15;
+    }
+    vTruth = Vec_IntAlloc( 0 );
+    p = Bdc_ManAlloc( pPars );
+    Ntk_ManForEachNode( pNtk, pObj, i )
+    {
+        if ( Ntk_ObjFaninNum(pObj) > 15 )
+            continue;
+        nNodes1 = Hop_DagSize(pObj->pFunc);
+        pObj->pFunc = Ntk_NodeIfNodeResyn( p, pNtk->pManHop, pObj->pFunc, Ntk_ObjFaninNum(pObj), vTruth, NULL );
+        nNodes2 = Hop_DagSize(pObj->pFunc);
+        nGainTotal += nNodes1 - nNodes2;
+    }
+    Bdc_ManFree( p );
+    Vec_IntFree( vTruth );
+    if ( fVerbose )
+    {
+    printf( "Total gain in AIG nodes = %d.  ", nGainTotal );
+    PRT( "Total runtime", clock() - clk );
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntk/ntkCheck.c b/src/aig/ntk/ntkCheck.c
new file mode 100644
index 00000000..6bbb67a6
--- /dev/null
+++ b/src/aig/ntk/ntkCheck.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [ntk_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntk_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntk/ntkDfs.c b/src/aig/ntk/ntkDfs.c
index ce176898..263a2740 100644
--- a/src/aig/ntk/ntkDfs.c
+++ b/src/aig/ntk/ntkDfs.c
@@ -30,6 +30,62 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+
+  Description [Assumes that white boxes have unit level.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_ManLevel( Ntk_Man_t * pNtk )
+{
+    Tim_Man_t * pManTimeUnit;
+    Ntk_Obj_t * pObj, * pFanin;
+    int i, k, LevelMax, Level;
+    // clean the levels
+    Ntk_ManForEachObj( pNtk, pObj, i )
+        Ntk_ObjSetLevel( pObj, 0 );
+    // perform level computation
+    LevelMax = 0;
+    pManTimeUnit = Tim_ManDupUnit( pNtk->pManTime );
+    Tim_ManIncrementTravId( pManTimeUnit );
+    Ntk_ManForEachObj( pNtk, pObj, i )
+    {
+        if ( Ntk_ObjIsCi(pObj) )
+        {
+            Level = (int)Tim_ManGetPiArrival( pManTimeUnit, pObj->PioId );
+            Ntk_ObjSetLevel( pObj, Level );
+        }
+        else if ( Ntk_ObjIsCo(pObj) )
+        {
+            Level = Ntk_ObjLevel( Ntk_ObjFanin0(pObj) );
+            Tim_ManSetPoArrival( pManTimeUnit, pObj->PioId, (float)Level );
+            Ntk_ObjSetLevel( pObj, Level );
+            if ( LevelMax < Ntk_ObjLevel(pObj) )
+                LevelMax = Ntk_ObjLevel(pObj);
+        }
+        else if ( Ntk_ObjIsNode(pObj) )
+        {
+            Level = 0;
+            Ntk_ObjForEachFanin( pObj, pFanin, k )
+                if ( Level < Ntk_ObjLevel(pFanin) )
+                    Level = Ntk_ObjLevel(pFanin);
+            Ntk_ObjSetLevel( pObj, Level + 1 );
+        }
+        else
+            assert( 0 );
+    }
+    // set the old timing manager
+    Tim_ManStop( pManTimeUnit );
+    return LevelMax;
+}
+
+
+
+/**Function*************************************************************
+
   Synopsis    [Performs DFS for one node.]
 
   Description []
@@ -39,16 +95,96 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManDfs_rec( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes )
+void Ntk_ManLevel2_rec( Ntk_Obj_t * pObj )
+{
+    Ntk_Obj_t * pNext;
+    int i, iBox, iTerm1, nTerms, LevelMax = 0;
+    if ( Ntk_ObjIsTravIdCurrent( pObj ) )
+        return;
+    Ntk_ObjSetTravIdCurrent( pObj );
+    if ( Ntk_ObjIsCi(pObj) )
+    {
+        iBox = Tim_ManBoxForCi( pObj->pMan->pManTime, pObj->PioId );
+        if ( iBox >= 0 ) // this is not a true PI
+        {
+            iTerm1 = Tim_ManBoxInputFirst( pObj->pMan->pManTime, iBox );
+            nTerms = Tim_ManBoxInputNum( pObj->pMan->pManTime, iBox );
+            for ( i = 0; i < nTerms; i++ )
+            {
+                pNext = Ntk_ManCo(pObj->pMan, iTerm1 + i);
+                Ntk_ManLevel2_rec( pNext );
+                if ( LevelMax < Ntk_ObjLevel(pNext) )
+                    LevelMax = Ntk_ObjLevel(pNext);
+            }
+            LevelMax++;
+        }
+    }
+    else if ( Ntk_ObjIsNode(pObj) || Ntk_ObjIsCo(pObj) )
+    {
+        Ntk_ObjForEachFanin( pObj, pNext, i )
+        {
+            Ntk_ManLevel2_rec( pNext );
+            if ( LevelMax < Ntk_ObjLevel(pNext) )
+                LevelMax = Ntk_ObjLevel(pNext);
+        }
+        if ( Ntk_ObjIsNode(pObj) )
+            LevelMax++;
+    }
+    else
+        assert( 0 );
+    Ntk_ObjSetLevel( pObj, LevelMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the DFS ordered array of all objects except latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_ManLevel2( Ntk_Man_t * pNtk )
+{
+    Ntk_Obj_t * pObj;
+    int i, LevelMax = 0;
+    Ntk_ManForEachObj( pNtk, pObj, i )
+        Ntk_ObjSetLevel( pObj, 0 );
+    Ntk_ManIncrementTravId( pNtk );
+    Ntk_ManForEachPo( pNtk, pObj, i )
+    {
+        Ntk_ManLevel2_rec( pObj );
+        if ( LevelMax < Ntk_ObjLevel(pObj) )
+            LevelMax = Ntk_ObjLevel(pObj);
+    }
+    return LevelMax;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManDfs_rec( Ntk_Obj_t * pObj, Vec_Ptr_t * vNodes )
 {
     Ntk_Obj_t * pNext;
     int i;
-    if ( Ntk_ObjIsTravIdCurrent( pNode ) )
+    if ( Ntk_ObjIsTravIdCurrent( pObj ) )
         return;
-    Ntk_ObjSetTravIdCurrent( pNode );
-    Ntk_ObjForEachFanin( pNode, pNext, i )
+    Ntk_ObjSetTravIdCurrent( pObj );
+    Ntk_ObjForEachFanin( pObj, pNext, i )
         Ntk_ManDfs_rec( pNext, vNodes );
-    Vec_PtrPush( vNodes, pNode );
+    Vec_PtrPush( vNodes, pObj );
 }
 
 /**Function*************************************************************
@@ -69,8 +205,16 @@ Vec_Ptr_t * Ntk_ManDfs( Ntk_Man_t * pNtk )
     int i;
     Ntk_ManIncrementTravId( pNtk );
     vNodes = Vec_PtrAlloc( 100 );
-    Ntk_ManForEachPo( pNtk, pObj, i )
-        Ntk_ManDfs_rec( pObj, vNodes );
+    Ntk_ManForEachObj( pNtk, pObj, i )
+    {
+        if ( Ntk_ObjIsCi(pObj) )
+        {
+            Ntk_ObjSetTravIdCurrent( pObj );
+            Vec_PtrPush( vNodes, pObj );
+        }
+        else if ( Ntk_ObjIsCo(pObj) )
+            Ntk_ManDfs_rec( pObj, vNodes );
+    }
     return vNodes;
 }
 
@@ -85,16 +229,35 @@ Vec_Ptr_t * Ntk_ManDfs( Ntk_Man_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManDfsReverse_rec( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes )
+void Ntk_ManDfsReverse_rec( Ntk_Obj_t * pObj, Vec_Ptr_t * vNodes )
 {
     Ntk_Obj_t * pNext;
-    int i;
-    if ( Ntk_ObjIsTravIdCurrent( pNode ) )
+    int i, iBox, iTerm1, nTerms;
+    if ( Ntk_ObjIsTravIdCurrent( pObj ) )
         return;
-    Ntk_ObjSetTravIdCurrent( pNode );
-    Ntk_ObjForEachFanout( pNode, pNext, i )
-        Ntk_ManDfsReverse_rec( pNext, vNodes );
-    Vec_PtrPush( vNodes, pNode );
+    Ntk_ObjSetTravIdCurrent( pObj );
+    if ( Ntk_ObjIsCo(pObj) )
+    {
+        iBox = Tim_ManBoxForCo( pObj->pMan->pManTime, pObj->PioId );
+        if ( iBox >= 0 ) // this is not a true PO
+        {
+            iTerm1 = Tim_ManBoxOutputFirst( pObj->pMan->pManTime, iBox );
+            nTerms = Tim_ManBoxOutputNum( pObj->pMan->pManTime, iBox );
+            for ( i = 0; i < nTerms; i++ )
+            {
+                pNext = Ntk_ManCi(pObj->pMan, iTerm1 + i);
+                Ntk_ManDfsReverse_rec( pNext, vNodes );
+            }
+        }
+    }
+    else if ( Ntk_ObjIsNode(pObj) || Ntk_ObjIsCi(pObj) )
+    {
+        Ntk_ObjForEachFanout( pObj, pNext, i )
+            Ntk_ManDfsReverse_rec( pNext, vNodes );
+    }
+    else
+        assert( 0 );
+    Vec_PtrPush( vNodes, pObj );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/ntk/ntkFanio.c b/src/aig/ntk/ntkFanio.c
index 73019231..135929af 100644
--- a/src/aig/ntk/ntkFanio.c
+++ b/src/aig/ntk/ntkFanio.c
@@ -279,7 +279,7 @@ void Ntk_ObjTransferFanout( Ntk_Obj_t * pNodeFrom, Ntk_Obj_t * pNodeTo )
     Vec_Ptr_t * vFanouts = pNodeFrom->pMan->vTemp;
     Ntk_Obj_t * pTemp;
     int nFanoutsOld, i;
-    assert( !Ntk_ObjIsPo(pNodeFrom) && !Ntk_ObjIsPo(pNodeTo) );
+    assert( !Ntk_ObjIsCo(pNodeFrom) && !Ntk_ObjIsCo(pNodeTo) );
     assert( pNodeFrom->pMan == pNodeTo->pMan );
     assert( pNodeFrom != pNodeTo );
     assert( Ntk_ObjFanoutNum(pNodeFrom) > 0 );
diff --git a/src/aig/ntk/ntkMan.c b/src/aig/ntk/ntkMan.c
index e302a98c..1a077495 100644
--- a/src/aig/ntk/ntkMan.c
+++ b/src/aig/ntk/ntkMan.c
@@ -50,6 +50,7 @@ Ntk_Man_t * Ntk_ManAlloc()
     p->vTemp = Vec_PtrAlloc( 1000 );
     p->nFanioPlus = 4;
     p->pMemObjs = Aig_MmFlexStart();
+    p->pManHop = Hop_ManStart();
     return p;
 }
 
@@ -72,9 +73,9 @@ void Ntk_ManFree( Ntk_Man_t * p )
     if ( p->vCos )     Vec_PtrFree( p->vCos );
     if ( p->vObjs )    Vec_PtrFree( p->vObjs );
     if ( p->vTemp )    Vec_PtrFree( p->vTemp );
-    if ( p->pAig )     Aig_ManStop( p->pAig );
     if ( p->pManTime ) Tim_ManStop( p->pManTime );
     if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 );
+    if ( p->pManHop )  Hop_ManStop( p->pManHop );
     free( p );
 }
 
@@ -89,7 +90,7 @@ void Ntk_ManFree( Ntk_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManPrintStats( Ntk_Man_t * p )
+void Ntk_ManPrintStats( Ntk_Man_t * p, If_Lib_t * pLutLib )
 {
     printf( "%-15s : ",      p->pName );
     printf( "pi = %5d  ",    Ntk_ManPiNum(p) );
@@ -97,10 +98,15 @@ void Ntk_ManPrintStats( Ntk_Man_t * p )
     printf( "ci = %5d  ",    Ntk_ManCiNum(p) );
     printf( "co = %5d  ",    Ntk_ManCoNum(p) );
     printf( "lat = %5d  ",   Ntk_ManLatchNum(p) );
-    printf( "box = %5d  ",   Ntk_ManBoxNum(p) );
+//    printf( "box = %5d  ",   Ntk_ManBoxNum(p) );
     printf( "node = %5d  ",  Ntk_ManNodeNum(p) );
-    printf( "aig = %6d  ",   Aig_ManNodeNum(p->pAig) );
+    printf( "aig = %6d  ",   Ntk_ManGetAigNodeNum(p) );
+    printf( "lev = %3d  ",   Ntk_ManLevel(p) );
+    printf( "lev2 = %3d  ",  Ntk_ManLevel2(p) );
+    printf( "delay = %5.2f", Ntk_ManDelayTraceLut(p, pLutLib) );
     printf( "\n" );
+
+    Ntk_ManDelayTracePrint( p, pLutLib );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntk/ntkMap.c b/src/aig/ntk/ntkMap.c
index 7700fc63..9c780498 100644
--- a/src/aig/ntk/ntkMap.c
+++ b/src/aig/ntk/ntkMap.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "ntk.h"
+#include "if.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -30,6 +31,209 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Load the network into FPGA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
+{
+//    extern void * Abc_FrameReadLibLut();
+    // set defaults
+    memset( pPars, 0, sizeof(If_Par_t) );
+    // user-controlable paramters
+//    pPars->nLutSize    = -1;
+    pPars->nLutSize    =  6;
+    pPars->nCutsMax    =  8;
+    pPars->nFlowIters  =  1;
+    pPars->nAreaIters  =  2;
+    pPars->DelayTarget = -1;
+    pPars->Epsilon     =  (float)0.01;
+    pPars->fPreprocess =  1;
+    pPars->fArea       =  0;
+    pPars->fFancy      =  0;
+    pPars->fExpRed     =  0;
+    pPars->fLatchPaths =  0;
+    pPars->fEdge       =  1;
+    pPars->fCutMin     =  1;
+    pPars->fSeqMap     =  0;
+    pPars->fVerbose    =  1;
+    // internal parameters
+    pPars->fTruth      =  0;
+    pPars->nLatches    =  0;
+    pPars->fLiftLeaves =  0;
+//    pPars->pLutLib     =  Abc_FrameReadLibLut();
+    pPars->pLutLib     =  NULL;
+    pPars->pTimesArr   =  NULL; 
+    pPars->pTimesArr   =  NULL;   
+    pPars->pFuncCost   =  NULL;   
+/*
+    if ( pPars->nLutSize == -1 )
+    {
+        if ( pPars->pLutLib == NULL )
+        {
+            printf( "The LUT library is not given.\n" );
+            return;
+        }
+        // get LUT size from the library
+        pPars->nLutSize = pPars->pLutLib->LutMax;
+    }
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Load the network into FPGA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
+{
+    If_Man_t * pIfMan;
+    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) ) );
+        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;
+        }
+        else if ( Aig_ObjIsPo(pNode) )
+            pNode->pData = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
+        else if ( Aig_ObjIsConst1(pNode) )
+            Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
+        else // add the node to the mapper
+            assert( 0 );
+        // 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_Obj_t * pIfObj = pNode->pData;
+            assert( !If_IsComplement(pIfObj) );
+            assert( pIfObj->Id == pNode->Id );
+        }
+    }
+    return pIfMan;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively derives the truth table for the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Ntk_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited )
+{
+    If_Cut_t * pCut;
+    If_Obj_t * pTemp;
+    Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
+    // get the best cut
+    pCut = If_ObjCutBest(pIfObj);
+    // if the cut is visited, return the result
+    if ( If_CutData(pCut) )
+        return If_CutData(pCut);
+    // mark the node as visited
+    Vec_PtrPush( vVisited, pCut );
+    // insert the worst case
+    If_CutSetData( pCut, (void *)1 );
+    // skip in case of primary input
+    if ( If_ObjIsCi(pIfObj) )
+        return If_CutData(pCut);
+    // compute the functions of the children
+    for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv )
+    {
+        gFunc0 = Ntk_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin0, vVisited );
+        if ( gFunc0 == (void *)1 )
+            continue;
+        gFunc1 = Ntk_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin1, vVisited );
+        if ( gFunc1 == (void *)1 )
+            continue;
+        // both branches are solved
+        gFunc = Hop_And( pHopMan, Hop_NotCond(gFunc0, pTemp->fCompl0), Hop_NotCond(gFunc1, pTemp->fCompl1) ); 
+        if ( pTemp->fPhase != pIfObj->fPhase )
+            gFunc = Hop_Not(gFunc);
+        If_CutSetData( pCut, gFunc );
+        break;
+    }
+    return If_CutData(pCut);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table for one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Ntk_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj )
+{
+    If_Cut_t * pCut;
+    Hop_Obj_t * gFunc;
+    If_Obj_t * pLeaf;
+    int i;
+    // get the best cut
+    pCut = If_ObjCutBest(pIfObj);
+    assert( pCut->nLeaves > 1 );
+    // set the leaf variables
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetData( If_ObjCutBest(pLeaf), Hop_IthVar(pHopMan, i) );
+    // recursively compute the function while collecting visited cuts
+    Vec_PtrClear( pIfMan->vTemp );
+    gFunc = Ntk_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); 
+    if ( gFunc == (void *)1 )
+    {
+        printf( "Ntk_NodeIfToHop(): Computing local AIG has failed.\n" );
+        return NULL;
+    }
+//    printf( "%d ", Vec_PtrSize(p->vTemp) );
+    // clean the cuts
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetData( If_ObjCutBest(pLeaf), NULL );
+    Vec_PtrForEachEntry( pIfMan->vTemp, pCut, i )
+        If_CutSetData( pCut, NULL );
+    return gFunc;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -39,6 +243,95 @@
   SeeAlso     []
 
 ***********************************************************************/
+Ntk_Man_t * Ntk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p )
+{
+    Ntk_Man_t * pNtk;
+    Ntk_Obj_t * pObjNew;
+    Aig_Obj_t * pObj;
+    If_Obj_t * pIfObj;
+    If_Cut_t * pCutBest;
+    int i, k, nLeaves, * ppLeaves;
+    assert( Aig_ManPiNum(p) == If_ManCiNum(pIfMan) );
+    assert( Aig_ManPoNum(p) == If_ManCoNum(pIfMan) );
+    assert( Aig_ManNodeNum(p) == If_ManAndNum(pIfMan) );
+    If_ManCleanCutData( pIfMan );
+    // construct the network
+    pNtk = Ntk_ManAlloc();
+    pNtk->pName = Aig_UtilStrsav( p->pName );
+    pNtk->pSpec = Aig_UtilStrsav( p->pSpec );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        pIfObj = If_ManObj( pIfMan, i );
+        if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) )
+            continue;
+        if ( Aig_ObjIsNode(pObj) )
+        {
+            pCutBest = If_ObjCutBest( pIfObj );
+            nLeaves  = If_CutLeaveNum( pCutBest ); 
+            ppLeaves = If_CutLeaves( pCutBest );
+            // create node
+            pObjNew = Ntk_ManCreateNode( pNtk, nLeaves, pIfObj->nRefs );
+            for ( k = 0; k < nLeaves; k++ )
+                Ntk_ObjAddFanin( pObjNew, Aig_ManObj(p, ppLeaves[k])->pData );
+            // get the functionality
+            pObjNew->pFunc = Ntk_NodeIfToHop( pNtk->pManHop, pIfMan, pIfObj );
+        }
+        else if ( Aig_ObjIsPi(pObj) )
+            pObjNew = Ntk_ManCreateCi( pNtk, pIfObj->nRefs );
+        else if ( Aig_ObjIsPo(pObj) )
+        {
+            pObjNew = Ntk_ManCreateCo( pNtk );
+            pObjNew->fCompl = Aig_ObjFaninC0(pObj);
+            Ntk_ObjAddFanin( pObjNew, Aig_ObjFanin0(pObj)->pData );
+        }
+        else if ( Aig_ObjIsConst1(pObj) )
+        {
+            pObjNew = Ntk_ManCreateNode( pNtk, 0, pIfObj->nRefs );
+            pObjNew->pFunc = Hop_ManConst1( pNtk->pManHop );
+        }
+        else
+            assert( 0 );
+        pObj->pData = pObjNew;
+    }
+    pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntk_Man_t * Ntk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars )
+{
+    Ntk_Man_t * pNtk;
+    If_Man_t * pIfMan;
+    // perform FPGA mapping
+    // 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 = Ntk_ManToIf( p, pPars );    
+    if ( pIfMan == NULL )
+        return NULL;
+    pIfMan->pManTim = Tim_ManDup( pManTime, 0 );
+    if ( !If_ManPerformMapping( pIfMan ) )
+    {
+        If_ManStop( pIfMan );
+        return NULL;
+    }
+    // transform the result of mapping into the new network
+    pNtk = Ntk_ManFromIf( pIfMan, p );
+    If_ManStop( pIfMan );
+    return pNtk;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ntk/ntkObj.c b/src/aig/ntk/ntkObj.c
index 259ed79d..7bd2f552 100644
--- a/src/aig/ntk/ntkObj.c
+++ b/src/aig/ntk/ntkObj.c
@@ -63,10 +63,11 @@ Ntk_Obj_t * Ntk_ManCreateObj( Ntk_Man_t * p, int nFanins, int nFanouts )
   SeeAlso     []
 
 ***********************************************************************/
-Ntk_Obj_t * Ntk_ManCreatePi( Ntk_Man_t * p )
+Ntk_Obj_t * Ntk_ManCreateCi( Ntk_Man_t * p, int nFanouts )
 {
     Ntk_Obj_t * pObj;
-    pObj = Ntk_ManCreateObj( p, 1, 1 );
+    pObj = Ntk_ManCreateObj( p, 1, nFanouts );
+    pObj->PioId = Vec_PtrSize( p->vCis );
     Vec_PtrPush( p->vCis, pObj );
     pObj->Type = NTK_OBJ_CI;
     p->nObjs[NTK_OBJ_CI]++;
@@ -84,10 +85,11 @@ Ntk_Obj_t * Ntk_ManCreatePi( Ntk_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Ntk_Obj_t * Ntk_ManCreatePo( Ntk_Man_t * p )
+Ntk_Obj_t * Ntk_ManCreateCo( Ntk_Man_t * p )
 {
     Ntk_Obj_t * pObj;
     pObj = Ntk_ManCreateObj( p, 1, 1 );
+    pObj->PioId = Vec_PtrSize( p->vCos );
     Vec_PtrPush( p->vCos, pObj );
     pObj->Type = NTK_OBJ_CO;
     p->nObjs[NTK_OBJ_CO]++;
@@ -200,7 +202,7 @@ void Ntk_ManDeleteNode_rec( Ntk_Obj_t * pObj )
 {
     Vec_Ptr_t * vNodes;
     int i;
-    assert( !Ntk_ObjIsPi(pObj) );
+    assert( !Ntk_ObjIsCi(pObj) );
     assert( Ntk_ObjFanoutNum(pObj) == 0 );
     vNodes = Vec_PtrAlloc( 100 );
     Ntk_ObjCollectFanins( pObj, vNodes );
diff --git a/src/aig/ntk/ntkTiming.c b/src/aig/ntk/ntkTiming.c
index f57c7987..ff867e02 100644
--- a/src/aig/ntk/ntkTiming.c
+++ b/src/aig/ntk/ntkTiming.c
@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "ntk.h"
-#include "if.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -108,19 +107,17 @@ void Ntk_ManDelayTraceSortPins( Ntk_Obj_t * pNode, int * pPinPerm, float * pPinD
   SeeAlso     []
 
 ***********************************************************************/
-float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, int fUseLutLib )
+float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, If_Lib_t * pLutLib )
 {
     int fUseSorting = 1;
     int pPinPerm[32];
     float pPinDelays[32];
-    If_Lib_t * pLutLib;
-    Ntk_Obj_t * pNode, * pFanin;
+    Ntk_Obj_t * pObj, * pFanin;
     Vec_Ptr_t * vNodes;
     float tArrival, tRequired, tSlack, * pDelays;
     int i, k;
 
     // get the library
-    pLutLib = fUseLutLib?  Abc_FrameReadLibLut() : NULL;
     if ( pLutLib && pLutLib->LutMax < Ntk_ManGetFaninMax(pNtk) )
     {
         printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", 
@@ -128,107 +125,138 @@ float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, int fUseLutLib )
         return -AIG_INFINITY;
     }
 
+    // compute the reverse order of all objects
+    vNodes = Ntk_ManDfsReverse( pNtk );
+
     // initialize the arrival times
     Abc_NtkPrepareTiming( pNtk );
 
     // propagate arrival times
-    vNodes = Ntk_ManDfs( pNtk );
-    Vec_PtrForEachEntry( vNodes, pNode, i )
+    Tim_ManIncrementTravId( pNtk->pManTime );
+    Ntk_ManForEachObj( pNtk, pObj, i )
     {
-        tArrival = -AIG_INFINITY;
-        if ( pLutLib == NULL )
-        {
-            Ntk_ObjForEachFanin( pNode, pFanin, k )
-                if ( tArrival < Ntk_ObjArrival(pFanin) + 1.0 )
-                    tArrival = Ntk_ObjArrival(pFanin) + 1.0;
-        }
-        else if ( !pLutLib->fVarPinDelays )
+        if ( Ntk_ObjIsNode(pObj) )
         {
-            pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-            Ntk_ObjForEachFanin( pNode, pFanin, k )
-                if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[0] )
-                    tArrival = Ntk_ObjArrival(pFanin) + pDelays[0];
-        }
-        else
-        {
-            pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-            if ( fUseSorting )
+            tArrival = -AIG_INFINITY;
+            if ( pLutLib == NULL )
             {
-                Ntk_ManDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
-                Ntk_ObjForEachFanin( pNode, pFanin, k ) 
-                    if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] )
-                        tArrival = Ntk_ObjArrival(Ntk_ObjFanin(pNode,pPinPerm[k])) + pDelays[k];
+                Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    if ( tArrival < Ntk_ObjArrival(pFanin) + 1.0 )
+                        tArrival = Ntk_ObjArrival(pFanin) + 1.0;
+            }
+            else if ( !pLutLib->fVarPinDelays )
+            {
+                pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)];
+                Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[0] )
+                        tArrival = Ntk_ObjArrival(pFanin) + pDelays[0];
             }
             else
             {
-                Ntk_ObjForEachFanin( pNode, pFanin, k )
-                    if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[k] )
-                        tArrival = Ntk_ObjArrival(pFanin) + pDelays[k];
+                pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)];
+                if ( fUseSorting )
+                {
+                    Ntk_ManDelayTraceSortPins( pObj, pPinPerm, pPinDelays );
+                    Ntk_ObjForEachFanin( pObj, pFanin, k ) 
+                        if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin(pObj,pPinPerm[k])) + pDelays[k] )
+                            tArrival = Ntk_ObjArrival(Ntk_ObjFanin(pObj,pPinPerm[k])) + pDelays[k];
+                }
+                else
+                {
+                    Ntk_ObjForEachFanin( pObj, pFanin, k )
+                        if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[k] )
+                            tArrival = Ntk_ObjArrival(pFanin) + pDelays[k];
+                }
             }
+            if ( Ntk_ObjFaninNum(pObj) == 0 )
+                tArrival = 0.0;
         }
-        if ( Ntk_ObjFaninNum(pNode) == 0 )
-            tArrival = 0.0;
-        Ntk_ObjSetArrival( pNode, tArrival );
+        else if ( Ntk_ObjIsCi(pObj) )
+        {
+            tArrival = Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId );
+        }
+        else if ( Ntk_ObjIsCo(pObj) )
+        {
+            tArrival = Ntk_ObjArrival( Ntk_ObjFanin0(pObj) );
+            Tim_ManSetPoArrival( pNtk->pManTime, pObj->PioId, tArrival );
+        }
+        else
+            assert( 0 );
+        Ntk_ObjSetArrival( pObj, tArrival );
     }
-    Vec_PtrFree( vNodes );
 
     // get the latest arrival times
     tArrival = -AIG_INFINITY;
-    Ntk_ManForEachPo( pNtk, pNode, i )
-        if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin0(pNode)) )
-            tArrival = Ntk_ObjArrival(Ntk_ObjFanin0(pNode));
+    Ntk_ManForEachPo( pNtk, pObj, i )
+        if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin0(pObj)) )
+            tArrival = Ntk_ObjArrival(Ntk_ObjFanin0(pObj));
 
     // initialize the required times
-    Ntk_ManForEachPo( pNtk, pNode, i )
-        if ( Ntk_ObjRequired(Ntk_ObjFanin0(pNode)) > tArrival )
-            Ntk_ObjSetRequired( Ntk_ObjFanin0(pNode), tArrival );
+    Ntk_ManForEachPo( pNtk, pObj, i )
+        if ( Ntk_ObjRequired(Ntk_ObjFanin0(pObj)) > tArrival )
+            Ntk_ObjSetRequired( Ntk_ObjFanin0(pObj), tArrival );
 
     // propagate the required times
-    vNodes = Ntk_ManDfsReverse( pNtk );
-    Vec_PtrForEachEntry( vNodes, pNode, i )
+    Tim_ManIncrementTravId( pNtk->pManTime );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
     {
-        if ( pLutLib == NULL )
-        {
-            tRequired = Ntk_ObjRequired(pNode) - (float)1.0;
-            Ntk_ObjForEachFanin( pNode, pFanin, k )
-                if ( Ntk_ObjRequired(pFanin) > tRequired )
-                    Ntk_ObjSetRequired( pFanin, tRequired );
-        }
-        else if ( !pLutLib->fVarPinDelays )
-        {
-            pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-            tRequired = Ntk_ObjRequired(pNode) - pDelays[0];
-            Ntk_ObjForEachFanin( pNode, pFanin, k )
-                if ( Ntk_ObjRequired(pFanin) > tRequired )
-                    Ntk_ObjSetRequired( pFanin, tRequired );
-        }
-        else 
+        if ( Ntk_ObjIsNode(pObj) )
         {
-            pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-            if ( fUseSorting )
+            if ( pLutLib == NULL )
             {
-                Ntk_ManDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
-                Ntk_ObjForEachFanin( pNode, pFanin, k )
-                {
-                    tRequired = Ntk_ObjRequired(pNode) - pDelays[k];
-                    if ( Ntk_ObjRequired(Ntk_ObjFanin(pNode,pPinPerm[k])) > tRequired )
-                        Ntk_ObjSetRequired( Ntk_ObjFanin(pNode,pPinPerm[k]), tRequired );
-                }
+                tRequired = Ntk_ObjRequired(pObj) - (float)1.0;
+                Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    if ( Ntk_ObjRequired(pFanin) > tRequired )
+                        Ntk_ObjSetRequired( pFanin, tRequired );
             }
-            else
+            else if ( !pLutLib->fVarPinDelays )
             {
-                Ntk_ObjForEachFanin( pNode, pFanin, k )
-                {
-                    tRequired = Ntk_ObjRequired(pNode) - pDelays[k];
+                pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)];
+                tRequired = Ntk_ObjRequired(pObj) - pDelays[0];
+                Ntk_ObjForEachFanin( pObj, pFanin, k )
                     if ( Ntk_ObjRequired(pFanin) > tRequired )
                         Ntk_ObjSetRequired( pFanin, tRequired );
+            }
+            else 
+            {
+                pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)];
+                if ( fUseSorting )
+                {
+                    Ntk_ManDelayTraceSortPins( pObj, pPinPerm, pPinDelays );
+                    Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    {
+                        tRequired = Ntk_ObjRequired(pObj) - pDelays[k];
+                        if ( Ntk_ObjRequired(Ntk_ObjFanin(pObj,pPinPerm[k])) > tRequired )
+                            Ntk_ObjSetRequired( Ntk_ObjFanin(pObj,pPinPerm[k]), tRequired );
+                    }
+                }
+                else
+                {
+                    Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    {
+                        tRequired = Ntk_ObjRequired(pObj) - pDelays[k];
+                        if ( Ntk_ObjRequired(pFanin) > tRequired )
+                            Ntk_ObjSetRequired( pFanin, tRequired );
+                    }
                 }
             }
         }
+        else if ( Ntk_ObjIsCi(pObj) )
+        {
+            tRequired = Ntk_ObjRequired(pObj);
+            Tim_ManSetPiRequired( pNtk->pManTime, pObj->PioId, tRequired );
+        }
+        else if ( Ntk_ObjIsCo(pObj) )
+        {
+            tRequired = Tim_ManGetPoRequired( pNtk->pManTime, pObj->PioId );
+            if ( Ntk_ObjRequired(Ntk_ObjFanin0(pObj)) > tRequired )
+                Ntk_ObjSetRequired( Ntk_ObjFanin0(pObj), tRequired );
+        }
+
         // set slack for this object
-        tSlack = Ntk_ObjRequired(pNode) - Ntk_ObjArrival(pNode);
+        tSlack = Ntk_ObjRequired(pObj) - Ntk_ObjArrival(pObj);
         assert( tSlack + 0.001 > 0.0 );
-        Ntk_ObjSetSlack( pNode, tSlack < 0.0 ? 0.0 : tSlack );
+        Ntk_ObjSetSlack( pObj, tSlack < 0.0 ? 0.0 : tSlack );
     }
     Vec_PtrFree( vNodes );
     return tArrival;
@@ -236,52 +264,6 @@ float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, int fUseLutLib )
 
 /**Function*************************************************************
 
-  Synopsis    [Determines timing-critical edges of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Ntk_ManDelayTraceTCEdges( Ntk_Man_t * pNtk, Ntk_Obj_t * pNode, float tDelta, int fUseLutLib )
-{
-    int pPinPerm[32];
-    float pPinDelays[32];
-    If_Lib_t * pLutLib;
-    Ntk_Obj_t * pFanin;
-    unsigned uResult = 0;
-    float tRequired, * pDelays;
-    int k;
-    pLutLib = fUseLutLib?  Abc_FrameReadLibLut() : NULL;
-    tRequired = Ntk_ObjRequired(pNode);
-    if ( pLutLib == NULL )
-    {
-        Ntk_ObjForEachFanin( pNode, pFanin, k )
-            if ( tRequired < Ntk_ObjArrival(pFanin) + 1.0 + tDelta )
-                uResult |= (1 << k);
-    }
-    else if ( !pLutLib->fVarPinDelays )
-    {
-        pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-        Ntk_ObjForEachFanin( pNode, pFanin, k )
-            if ( tRequired < Ntk_ObjArrival(pFanin) + pDelays[0] + tDelta )
-                uResult |= (1 << k);
-    }
-    else
-    {
-        pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-        Ntk_ManDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
-        Ntk_ObjForEachFanin( pNode, pFanin, k )
-            if ( tRequired < Ntk_ObjArrival(Ntk_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] + tDelta )
-                uResult |= (1 << pPinPerm[k]);
-    }
-    return uResult;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Delay tracing of the LUT mapped network.]
 
   Description []
@@ -291,14 +273,12 @@ unsigned Ntk_ManDelayTraceTCEdges( Ntk_Man_t * pNtk, Ntk_Obj_t * pNode, float tD
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, int fUseLutLib, int fVerbose )
+void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, If_Lib_t * pLutLib )
 {
     Ntk_Obj_t * pNode;
-    If_Lib_t * pLutLib;
     int i, Nodes, * pCounters;
     float tArrival, tDelta, nSteps, Num;
     // get the library
-    pLutLib = fUseLutLib?  Abc_FrameReadLibLut() : NULL;
     if ( pLutLib && pLutLib->LutMax < Ntk_ManGetFaninMax(pNtk) )
     {
         printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", 
@@ -306,11 +286,11 @@ void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, int fUseLutLib, int fVerbose )
         return;
     }
     // decide how many steps
-    nSteps = fUseLutLib ? 20 : Ntk_ManLevel(pNtk);
+    nSteps = pLutLib ? 20 : Ntk_ManLevel(pNtk);
     pCounters = ALLOC( int, nSteps + 1 );
     memset( pCounters, 0, sizeof(int)*(nSteps + 1) );
     // perform delay trace
-    tArrival = Ntk_ManDelayTraceLut( pNtk, fUseLutLib );
+    tArrival = Ntk_ManDelayTraceLut( pNtk, pLutLib );
     tDelta = tArrival / nSteps;
     // count how many nodes have slack in the corresponding intervals
     Ntk_ManForEachNode( pNtk, pNode, i )
@@ -318,17 +298,19 @@ void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, int fUseLutLib, int fVerbose )
         if ( Ntk_ObjFaninNum(pNode) == 0 )
             continue;
         Num = Ntk_ObjSlack(pNode) / tDelta;
+        if ( Num > nSteps )
+            continue;
         assert( Num >=0 && Num <= nSteps );
         pCounters[(int)Num]++;
     }
     // print the results
-    printf( "Max delay = %6.2f. Delay trace using %s model:\n", tArrival, fUseLutLib? "LUT library" : "unit-delay" );
+    printf( "Max delay = %6.2f. Delay trace using %s model:\n", tArrival, pLutLib? "LUT library" : "unit-delay" );
     Nodes = 0;
     for ( i = 0; i < nSteps; i++ )
     {
         Nodes += pCounters[i];
-        printf( "%3d %s : %5d  (%6.2f %%)\n", fUseLutLib? 5*(i+1) : i+1, 
-            fUseLutLib? "%":"lev", Nodes, 100.0*Nodes/Ntk_ManNodeNum(pNtk) );
+        printf( "%3d %s : %5d  (%6.2f %%)\n", pLutLib? 5*(i+1) : i+1, 
+            pLutLib? "%":"lev", Nodes, 100.0*Nodes/Ntk_ManNodeNum(pNtk) );
     }
     free( pCounters );
 }
diff --git a/src/aig/ntk/ntkUtil.c b/src/aig/ntk/ntkUtil.c
index 543d1a60..931a26ee 100644
--- a/src/aig/ntk/ntkUtil.c
+++ b/src/aig/ntk/ntkUtil.c
@@ -95,36 +95,25 @@ int Ntk_ManGetTotalFanins( Ntk_Man_t * pNtk )
     return nFanins;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+  Synopsis    []
 
-  Description [Assumes topological ordering of the nodes.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_ManLevel( Ntk_Man_t * pNtk )
+int Ntk_ManPiNum( Ntk_Man_t * pNtk )
 {
-    Ntk_Obj_t * pObj, * pFanin;
-    int i, k, LevelMax;
-    Ntk_ManForEachPi( pNtk, pObj, i )
-        Ntk_ObjSetLevel( pObj, 0 );
-    Ntk_ManForEachNode( pNtk, pObj, i )
-    {
-        LevelMax = 0;
-        Ntk_ObjForEachFanin( pObj, pFanin, k )
-            if ( LevelMax < Ntk_ObjLevel(pFanin) )
-                LevelMax = Ntk_ObjLevel(pFanin);
-        Ntk_ObjSetLevel( pFanin, LevelMax+1 );
-    }
-    LevelMax = 0;
-    Ntk_ManForEachPo( pNtk, pObj, i )
-        if ( LevelMax < Ntk_ObjLevel(pObj) )
-            LevelMax = Ntk_ObjLevel(pObj);
-    return LevelMax;
+    Ntk_Obj_t * pNode;
+    int i, Counter = 0;
+    Ntk_ManForEachCi( pNtk, pNode, i )
+        Counter += Ntk_ObjIsPi( pNode );
+    return Counter;
 }
 
 /**Function*************************************************************
@@ -138,18 +127,18 @@ int Ntk_ManLevel( Ntk_Man_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_ManPiNum( Ntk_Man_t * pNtk )
+int Ntk_ManPoNum( Ntk_Man_t * pNtk )
 {
     Ntk_Obj_t * pNode;
     int i, Counter = 0;
-    Ntk_ManForEachPi( pNtk, pNode, i )
-        Counter++;
+    Ntk_ManForEachCo( pNtk, pNode, i )
+        Counter += Ntk_ObjIsPo( pNode );
     return Counter;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Reads the number of BDD nodes.]
 
   Description []
                
@@ -158,13 +147,22 @@ int Ntk_ManPiNum( Ntk_Man_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_ManPoNum( Ntk_Man_t * pNtk )
+int Ntk_ManGetAigNodeNum( Ntk_Man_t * pNtk )
 {
     Ntk_Obj_t * pNode;
-    int i, Counter = 0;
-    Ntk_ManForEachPo( pNtk, pNode, i )
-        Counter++;
-    return Counter;
+    int i, nNodes = 0;
+    Ntk_ManForEachNode( pNtk, pNode, i )
+    {
+        if ( pNode->pFunc == NULL )
+        {
+            printf( "Ntk_ManGetAigNodeNum(): Local AIG of node %d is not assigned.\n", pNode->Id );
+            continue;
+        }
+        if ( Ntk_ObjFaninNum(pNode) < 2 )
+            continue;
+        nNodes += Hop_DagSize( pNode->pFunc );
+    }
+    return nNodes;
 }
 
 ////////////////////////////////////////////////////////////////////////