Version abc80326

9 files changed, 1630 insertions, 0 deletions

diff --git a/src/aig/ntk/ntk.h b/src/aig/ntk/ntk.h
new file mode 100644
index 00000000..6ddfac81
--- /dev/null
+++ b/src/aig/ntk/ntk.h
@@ -0,0 +1,230 @@
+/**CFile****************************************************************
+
+  FileName    [ntk.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntk.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __NTK_H__
+#define __NTK_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig.h"
+#include "tim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ntk_Man_t_    Ntk_Man_t;
+typedef struct Ntk_Obj_t_    Ntk_Obj_t;
+
+// object types
+typedef enum { 
+    NTK_OBJ_NONE,                      // 0: non-existant object
+    NTK_OBJ_CI,                        // 1: combinational input
+    NTK_OBJ_CO,                        // 2: combinational output
+    NTK_OBJ_NODE,                      // 3: logic node
+    NTK_OBJ_BOX,                       // 4: white box
+    NTK_OBJ_LATCH,                     // 5: register
+    NTK_OBJ_VOID                       // 6: unused object
+} Ntk_Type_t;
+
+struct Ntk_Man_t_
+{
+    // models of this design
+    char *             pName;          // the name of this design
+    char *             pSpec;          // the name of input file
+    // node representation
+    Vec_Ptr_t *        vCis;           // the primary inputs of the extracted part
+    Vec_Ptr_t *        vCos;           // the primary outputs of the extracted part 
+    Vec_Ptr_t *        vObjs;          // the objects in the topological order
+    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
+    Tim_Man_t *        pManTime;       // the timing manager
+    Aig_MmFlex_t *     pMemObjs;       // memory for objects
+    Vec_Ptr_t *        vTemp;          // array used for incremental updates
+    unsigned           nTravIds;       // the counter of traversal IDs
+};
+
+struct Ntk_Obj_t_
+{
+    Ntk_Man_t *        pMan;           // the manager  
+    void *             pCopy;          // temporary pointer
+    void *             pFunc;          // functionality
+    // node information
+    int                Id;             // unique ID
+    unsigned           Type     :  3;  // object type
+    unsigned           fCompl   :  1;  // complemented attribute
+    unsigned           MarkA    :  1;  // temporary mark  
+    unsigned           MarkB    :  1;  // temporary mark
+    unsigned           TravId   : 26;  // traversal ID
+    // timing information
+    float              tArrival;       // the arrival time
+    float              tRequired;      // the required time
+    float              tSlack;         // the slack
+    // fanin/fanout representation
+    unsigned           nFanins  :  6;  // the number of fanins
+    unsigned           nFanouts : 26;  // the number of fanouts
+    int                nFanioAlloc;    // the number of allocated fanins/fanouts
+    Ntk_Obj_t *        pFanio[0];      // fanins/fanouts
+};
+
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                      INLINED FUNCTIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int         Ntk_ManCiNum( Ntk_Man_t * p )           { return p->nObjs[NTK_OBJ_CI];                } 
+static inline int         Ntk_ManCoNum( Ntk_Man_t * p )           { return p->nObjs[NTK_OBJ_CO];                } 
+static inline int         Ntk_ManNodeNum( Ntk_Man_t * p )         { return p->nObjs[NTK_OBJ_NODE];              } 
+static inline int         Ntk_ManLatchNum( Ntk_Man_t * p )        { return p->nObjs[NTK_OBJ_LATCH];             } 
+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 int         Ntk_ObjFaninNum( Ntk_Obj_t * p )        { return p->nFanins;                          } 
+static inline int         Ntk_ObjFanoutNum( Ntk_Obj_t * p )       { return p->nFanouts;                         } 
+
+static inline Ntk_Obj_t * Ntk_ObjFanin0( Ntk_Obj_t * p )          { return p->pFanio[0];                        } 
+static inline Ntk_Obj_t * Ntk_ObjFanout0( Ntk_Obj_t * p )         { return p->pFanio[p->nFanins];               } 
+static inline Ntk_Obj_t * Ntk_ObjFanin( Ntk_Obj_t * p, int i )    { return p->pFanio[i];                        } 
+static inline Ntk_Obj_t * Ntk_ObjFanout( Ntk_Obj_t * p, int i )   { return p->pFanio[p->nFanins+1];             } 
+
+static inline int         Ntk_ObjIsCi( Ntk_Obj_t * p )            { return p->Type == NTK_OBJ_CI;               } 
+static inline int         Ntk_ObjIsCo( Ntk_Obj_t * p )            { return p->Type == NTK_OBJ_CO;               } 
+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 float       Ntk_ObjArrival( Ntk_Obj_t * pObj )                 { return pObj->tArrival;           }
+static inline float       Ntk_ObjRequired( Ntk_Obj_t * pObj )                { return pObj->tRequired;          }
+static inline float       Ntk_ObjSlack( Ntk_Obj_t * pObj )                   { return pObj->tSlack;             }
+static inline void        Ntk_ObjSetArrival( Ntk_Obj_t * pObj, float Time )  { pObj->tArrival   = Time;         }
+static inline void        Ntk_ObjSetRequired( Ntk_Obj_t * pObj, float Time ) { pObj->tRequired  = Time;         }
+static inline void        Ntk_ObjSetSlack( Ntk_Obj_t * pObj, float Time )    { pObj->tSlack     = Time;         }
+
+static inline int         Ntk_ObjLevel( Ntk_Obj_t * pObj )                   { return (int)pObj->tArrival;      }
+static inline void        Ntk_ObjSetLevel( Ntk_Obj_t * pObj, int Lev )       { pObj->tArrival = (float)Lev;     }
+
+static inline void        Ntk_ObjSetTravId( Ntk_Obj_t * pObj, int TravId )   { pObj->TravId = TravId;                           }
+static inline void        Ntk_ObjSetTravIdCurrent( Ntk_Obj_t * pObj )        { pObj->TravId = pObj->pMan->nTravIds;             }
+static inline void        Ntk_ObjSetTravIdPrevious( Ntk_Obj_t * pObj )       { pObj->TravId = pObj->pMan->nTravIds - 1;         }
+static inline int         Ntk_ObjIsTravIdCurrent( Ntk_Obj_t * pObj )         { return pObj->TravId == pObj->pMan->nTravIds;     }
+static inline int         Ntk_ObjIsTravIdPrevious( Ntk_Obj_t * pObj )        { return pObj->TravId == pObj->pMan->nTravIds - 1; }
+
+////////////////////////////////////////////////////////////////////////
+///                         ITERATORS                                ///
+////////////////////////////////////////////////////////////////////////
+
+#define Ntk_ManForEachCi( p, pObj, i )                                     \
+    Vec_PtrForEachEntry( p->vCis, pObj, i )
+#define Ntk_ManForEachCo( p, pObj, i )                                     \
+    Vec_PtrForEachEntry( p->vCos, pObj, i )
+#define Ntk_ManForEachPi( p, pObj, i )                                     \
+    Vec_PtrForEachEntry( p->vCis, pObj, i )                                \
+        if ( !Ntk_ObjIsPi(pObj) ) {} else
+#define Ntk_ManForEachPo( p, pObj, i )                                     \
+    Vec_PtrForEachEntry( p->vCos, pObj, i )                                \
+        if ( !Ntk_ObjIsPo(pObj) ) {} else
+#define Ntk_ManForEachObj( p, pObj, i )                                    \
+    for ( i = 0; (i < Vec_PtrSize(p->vObjs)) && (((pObj) = Vec_PtrEntry(p->vObjs, i)), 1); i++ ) \
+        if ( pObj == NULL ) {} else
+#define Ntk_ManForEachNode( p, pObj, i )                                   \
+    for ( i = 0; (i < Vec_PtrSize(p->vObjs)) && (((pObj) = Vec_PtrEntry(p->vObjs, i)), 1); i++ ) \
+        if ( !Ntk_ObjIsNode(pObj) ) {} else
+#define Ntk_ManForEachBox( p, pObj, i )                                    \
+    for ( i = 0; (i < Vec_PtrSize(p->vObjs)) && (((pObj) = Vec_PtrEntry(p->vObjs, i)), 1); i++ ) \
+        if ( !Ntk_ObjIsBox(pObj) ) {} else
+#define Ntk_ManForEachLatch( p, pObj, i )                                  \
+    for ( i = 0; (i < Vec_PtrSize(p->vObjs)) && (((pObj) = Vec_PtrEntry(p->vObjs, i)), 1); i++ ) \
+        if ( !Ntk_ObjIsLatch(pObj) ) {} else
+
+#define Ntk_ObjForEachFanin( pObj, pFanin, i )                                  \
+    for ( i = 0; (i < (int)(pObj)->nFanins) && ((pFanin) = (pObj)->pFanio[i]); i++ )
+#define Ntk_ObjForEachFanout( pObj, pFanout, i )                                \
+    for ( i = 0; (i < (int)(pObj)->nFanouts) && ((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== ntlDfs.c ==========================================================*/
+extern Vec_Ptr_t *     Ntk_ManDfs( Ntk_Man_t * pNtk );
+extern Vec_Ptr_t *     Ntk_ManDfsReverse( Ntk_Man_t * pNtk );
+/*=== ntlFanio.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 ============================================================*/
+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 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 ============================================================*/
+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 );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/ntk/ntkDfs.c b/src/aig/ntk/ntkDfs.c
new file mode 100644
index 00000000..ce176898
--- /dev/null
+++ b/src/aig/ntk/ntkDfs.c
@@ -0,0 +1,127 @@
+/**CFile****************************************************************
+
+  FileName    [ntkDfs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [DFS traversals.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntkDfs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManDfs_rec( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Ntk_Obj_t * pNext;
+    int i;
+    if ( Ntk_ObjIsTravIdCurrent( pNode ) )
+        return;
+    Ntk_ObjSetTravIdCurrent( pNode );
+    Ntk_ObjForEachFanin( pNode, pNext, i )
+        Ntk_ManDfs_rec( pNext, vNodes );
+    Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the DFS ordered array of all objects except latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntk_ManDfs( Ntk_Man_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Ntk_Obj_t * pObj;
+    int i;
+    Ntk_ManIncrementTravId( pNtk );
+    vNodes = Vec_PtrAlloc( 100 );
+    Ntk_ManForEachPo( pNtk, pObj, i )
+        Ntk_ManDfs_rec( pObj, vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManDfsReverse_rec( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Ntk_Obj_t * pNext;
+    int i;
+    if ( Ntk_ObjIsTravIdCurrent( pNode ) )
+        return;
+    Ntk_ObjSetTravIdCurrent( pNode );
+    Ntk_ObjForEachFanout( pNode, pNext, i )
+        Ntk_ManDfsReverse_rec( pNext, vNodes );
+    Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the DFS ordered array of all objects except latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntk_ManDfsReverse( Ntk_Man_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Ntk_Obj_t * pObj;
+    int i;
+    Ntk_ManIncrementTravId( pNtk );
+    vNodes = Vec_PtrAlloc( 100 );
+    Ntk_ManForEachPi( pNtk, pObj, i )
+        Ntk_ManDfsReverse_rec( pObj, vNodes );
+    return vNodes;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntk/ntkFanio.c b/src/aig/ntk/ntkFanio.c
new file mode 100644
index 00000000..73019231
--- /dev/null
+++ b/src/aig/ntk/ntkFanio.c
@@ -0,0 +1,323 @@
+/**CFile****************************************************************
+
+  FileName    [ntkFanio.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Manipulation of fanins/fanouts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntkFanio.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if it is an AIG with choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ObjCollectFanins( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Ntk_Obj_t * pFanin;
+    int i;
+    Vec_PtrClear(vNodes);
+    Ntk_ObjForEachFanin( pNode, pFanin, i )
+        Vec_PtrPush( vNodes, pFanin );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if it is an AIG with choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ObjCollectFanouts( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Ntk_Obj_t * pFanout;
+    int i;
+    Vec_PtrClear(vNodes);
+    Ntk_ObjForEachFanout( pNode, pFanout, i )
+        Vec_PtrPush( vNodes, pFanout );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of the fanin of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_ObjFindFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanin )
+{  
+    Ntk_Obj_t * pTemp;
+    int i;
+    Ntk_ObjForEachFanin( pObj, pTemp, i )
+        if ( pTemp == pFanin )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of the fanin of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_ObjFindFanout( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanout )
+{  
+    Ntk_Obj_t * pTemp;
+    int i;
+    Ntk_ObjForEachFanout( pObj, pTemp, i )
+        if ( pTemp == pFanout )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the object has to be reallocated.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ntk_ObjReallocIsNeeded( Ntk_Obj_t * pObj )
+{  
+    return pObj->nFanins + pObj->nFanouts == (unsigned)pObj->nFanioAlloc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Ntk_Obj_t * Ntk_ManReallocNode( Ntk_Obj_t * pObj )
+{  
+    Ntk_Obj_t * pObjNew, * pTemp;
+    int i, iNum;
+    assert( Ntk_ObjReallocIsNeeded(pObj) );
+    pObjNew = (Ntk_Obj_t *)Aig_MmFlexEntryFetch( pObj->pMan->pMemObjs, sizeof(Ntk_Obj_t) + 2 * pObj->nFanioAlloc * sizeof(Ntk_Obj_t *) );
+    memmove( pObjNew, pObj, sizeof(Ntk_Obj_t) + pObj->nFanioAlloc * sizeof(Ntk_Obj_t *) );
+    pObjNew->nFanioAlloc = pObj->nFanioAlloc;
+    // update the fanouts' fanins
+    Ntk_ObjForEachFanout( pObj, pTemp, i )
+    {
+        iNum = Ntk_ObjFindFanin( pTemp, pObj );
+        if ( iNum == -1 )
+            printf( "Ntk_ManReallocNode(): Error! Fanin cannot be found.\n" );
+        pTemp->pFanio[iNum] = pObjNew;
+    }
+    // update the fanins' fanouts
+    Ntk_ObjForEachFanin( pObj, pTemp, i )
+    {
+        iNum = Ntk_ObjFindFanout( pTemp, pObj );
+        if ( iNum == -1 )
+            printf( "Ntk_ManReallocNode(): Error! Fanout cannot be found.\n" );
+        pTemp->pFanio[pTemp->nFanins+iNum] = pObjNew;
+    }
+    return pObjNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates fanout/fanin relationship between the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ObjAddFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanin )
+{
+    int i;
+    assert( pObj->pMan == pFanin->pMan );
+    assert( pObj->Id >= 0 && pFanin->Id >= 0 );
+    if ( Ntk_ObjReallocIsNeeded(pObj) )
+        Ntk_ManReallocNode( pObj );
+    if ( Ntk_ObjReallocIsNeeded(pFanin) )
+        Ntk_ManReallocNode( pFanin );
+    for ( i = pObj->nFanins + pObj->nFanouts; i > (int)pObj->nFanins; i-- )
+        pObj->pFanio[i] = pObj->pFanio[i-1];
+    pObj->pFanio[pObj->nFanins++] = pFanin;
+    pFanin->pFanio[pFanin->nFanins + pFanin->nFanouts++] = pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes fanout/fanin relationship between the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ObjDeleteFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanin )
+{
+    int i, k, Limit;
+    // remove pFanin from the fanin list of pObj
+    Limit = pObj->nFanins + pObj->nFanouts;
+    for ( k = i = 0; i < Limit; i++ )
+        if ( pObj->pFanio[i] != pFanin )
+            pObj->pFanio[k++] = pObj->pFanio[i];
+    pObj->nFanins--;
+    // remove pObj from the fanout list of pFanin
+    Limit = pFanin->nFanins + pFanin->nFanouts;
+    for ( k = i = pFanin->nFanins; i < Limit; i++ )
+        if ( pFanin->pFanio[i] != pObj )
+            pFanin->pFanio[k++] = pFanin->pFanio[i];
+    pFanin->nFanouts--;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces a fanin of the node.]
+
+  Description [The node is pObj. An old fanin of this node (pFaninOld) has to be
+  replaced by a new fanin (pFaninNew). Assumes that the node and the old fanin 
+  are not complemented. The new fanin can be complemented. In this case, the
+  polarity of the new fanin will change, compared to the polarity of the old fanin.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ObjPatchFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFaninOld, Ntk_Obj_t * pFaninNew )
+{
+    int i, k, iFanin, Limit;
+    assert( pFaninOld != pFaninNew );
+    assert( pObj != pFaninOld );
+    assert( pObj != pFaninNew );
+    assert( pObj->pMan == pFaninOld->pMan );
+    assert( pObj->pMan == pFaninNew->pMan );
+    // update the fanin
+    iFanin = Ntk_ObjFindFanin( pObj, pFaninOld );
+    if ( iFanin == -1 )
+    {
+        printf( "Ntk_ObjPatchFanin(); Error! Node %d is not among", pFaninOld->Id );
+        printf( " the fanins of node %s...\n", pObj->Id );
+        return;
+    }
+    pObj->pFanio[iFanin] = pFaninNew;
+    // remove pObj from the fanout list of pFaninOld
+    Limit = pFaninOld->nFanins + pFaninOld->nFanouts;
+    for ( k = i = pFaninOld->nFanins; i < Limit; i++ )
+        if ( pFaninOld->pFanio[i] != pObj )
+            pFaninOld->pFanio[k++] = pFaninOld->pFanio[i];
+    pFaninOld->nFanouts--;
+    // add pObj to the fanout list of pFaninNew
+    if ( Ntk_ObjReallocIsNeeded(pFaninNew) )
+        Ntk_ManReallocNode( pFaninNew );
+    pFaninNew->pFanio[pFaninNew->nFanins + pFaninNew->nFanouts++] = pObj;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers fanout from the old node to the new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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( pNodeFrom->pMan == pNodeTo->pMan );
+    assert( pNodeFrom != pNodeTo );
+    assert( Ntk_ObjFanoutNum(pNodeFrom) > 0 );
+    // get the fanouts of the old node
+    nFanoutsOld = Ntk_ObjFanoutNum(pNodeTo);
+    Ntk_ObjCollectFanouts( pNodeFrom, vFanouts );
+    // patch the fanin of each of them
+    Vec_PtrForEachEntry( vFanouts, pTemp, i )
+        Ntk_ObjPatchFanin( pTemp, pNodeFrom, pNodeTo );
+    assert( Ntk_ObjFanoutNum(pNodeFrom) == 0 );
+    assert( Ntk_ObjFanoutNum(pNodeTo) == nFanoutsOld + Vec_PtrSize(vFanouts) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces the node by a new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ObjReplace( Ntk_Obj_t * pNodeOld, Ntk_Obj_t * pNodeNew )
+{
+    assert( pNodeOld->pMan == pNodeNew->pMan );
+    assert( pNodeOld != pNodeNew );
+    assert( Ntk_ObjFanoutNum(pNodeOld) > 0 );
+    // transfer the fanouts to the old node
+    Ntk_ObjTransferFanout( pNodeOld, pNodeNew );
+    // remove the old node
+    Ntk_ManDeleteNode_rec( pNodeOld );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntk/ntkMan.c b/src/aig/ntk/ntkMan.c
new file mode 100644
index 00000000..e302a98c
--- /dev/null
+++ b/src/aig/ntk/ntkMan.c
@@ -0,0 +1,110 @@
+/**CFile****************************************************************
+
+  FileName    [ntkMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Network manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntkMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the netlist manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntk_Man_t * Ntk_ManAlloc()
+{
+    Ntk_Man_t * p;
+    p = ALLOC( Ntk_Man_t, 1 );
+    memset( p, 0, sizeof(Ntk_Man_t) );
+    p->vCis = Vec_PtrAlloc( 1000 );
+    p->vCos = Vec_PtrAlloc( 1000 );
+    p->vObjs = Vec_PtrAlloc( 1000 );
+    p->vTemp = Vec_PtrAlloc( 1000 );
+    p->nFanioPlus = 4;
+    p->pMemObjs = Aig_MmFlexStart();
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the netlist manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManFree( Ntk_Man_t * p )
+{
+    if ( p->pName )    free( p->pName );
+    if ( p->pSpec )    free( p->pSpec );
+    if ( p->vCis )     Vec_PtrFree( p->vCis );
+    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 );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the netlist manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManPrintStats( Ntk_Man_t * p )
+{
+    printf( "%-15s : ",      p->pName );
+    printf( "pi = %5d  ",    Ntk_ManPiNum(p) );
+    printf( "po = %5d  ",    Ntk_ManPoNum(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( "node = %5d  ",  Ntk_ManNodeNum(p) );
+    printf( "aig = %6d  ",   Aig_ManNodeNum(p->pAig) );
+    printf( "\n" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntk/ntkMap.c b/src/aig/ntk/ntkMap.c
new file mode 100644
index 00000000..7700fc63
--- /dev/null
+++ b/src/aig/ntk/ntkMap.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [ntkMap.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Interface to technology mapping.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntkMap.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/ntkObj.c b/src/aig/ntk/ntkObj.c
new file mode 100644
index 00000000..259ed79d
--- /dev/null
+++ b/src/aig/ntk/ntkObj.c
@@ -0,0 +1,219 @@
+/**CFile****************************************************************
+
+  FileName    [ntkObj.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Manipulation of objects.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntkObj.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates an object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntk_Obj_t * Ntk_ManCreateObj( Ntk_Man_t * p, int nFanins, int nFanouts )
+{
+    Ntk_Obj_t * pObj;
+    pObj = (Ntk_Obj_t *)Aig_MmFlexEntryFetch( p->pMemObjs, sizeof(Ntk_Obj_t) + (nFanins + nFanouts + p->nFanioPlus) * sizeof(Ntk_Obj_t *) );
+    memset( pObj, 0, sizeof(Ntk_Obj_t) );
+    pObj->Id = Vec_PtrSize( p->vObjs );
+    Vec_PtrPush( p->vObjs, pObj );
+    pObj->pMan        = p;
+    pObj->nFanioAlloc = nFanins + nFanouts + p->nFanioPlus;
+    return pObj;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a primary input.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntk_Obj_t * Ntk_ManCreatePi( Ntk_Man_t * p )
+{
+    Ntk_Obj_t * pObj;
+    pObj = Ntk_ManCreateObj( p, 1, 1 );
+    Vec_PtrPush( p->vCis, pObj );
+    pObj->Type = NTK_OBJ_CI;
+    p->nObjs[NTK_OBJ_CI]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a primary output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntk_Obj_t * Ntk_ManCreatePo( Ntk_Man_t * p )
+{
+    Ntk_Obj_t * pObj;
+    pObj = Ntk_ManCreateObj( p, 1, 1 );
+    Vec_PtrPush( p->vCos, pObj );
+    pObj->Type = NTK_OBJ_CO;
+    p->nObjs[NTK_OBJ_CO]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a latch.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntk_Obj_t * Ntk_ManCreateLatch( Ntk_Man_t * p )
+{
+    Ntk_Obj_t * pObj;
+    pObj = Ntk_ManCreateObj( p, 1, 1 );
+    pObj->Type = NTK_OBJ_LATCH;
+    p->nObjs[NTK_OBJ_LATCH]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntk_Obj_t * Ntk_ManCreateNode( Ntk_Man_t * p, int nFanins, int nFanouts )
+{
+    Ntk_Obj_t * pObj;
+    pObj = Ntk_ManCreateObj( p, nFanins, nFanouts );
+    pObj->Type = NTK_OBJ_NODE;
+    p->nObjs[NTK_OBJ_NODE]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntk_Obj_t * Ntk_ManCreateBox( Ntk_Man_t * p, int nFanins, int nFanouts )
+{
+    Ntk_Obj_t * pObj;
+    pObj = Ntk_ManCreateObj( p, nFanins, nFanouts );
+    pObj->Type = NTK_OBJ_BOX;
+    p->nObjs[NTK_OBJ_BOX]++;
+    return pObj;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManDeleteNode( Ntk_Obj_t * pObj )
+{
+    Vec_Ptr_t * vNodes = pObj->pMan->vTemp;
+    Ntk_Obj_t * pTemp;
+    int i;
+    // delete fanins and fanouts
+    Ntk_ObjCollectFanouts( pObj, vNodes );
+    Vec_PtrForEachEntry( vNodes, pTemp, i )
+        Ntk_ObjDeleteFanin( pTemp, pObj );
+    Ntk_ObjCollectFanins( pObj, vNodes );
+    Vec_PtrForEachEntry( vNodes, pTemp, i )
+        Ntk_ObjDeleteFanin( pObj, pTemp );
+    // remove from the list of objects
+    Vec_PtrWriteEntry( pObj->pMan->vObjs, pObj->Id, NULL );
+    pObj->pMan->nObjs[pObj->Type]--;
+    memset( pObj, 0, sizeof(Ntk_Obj_t) );
+    pObj->Id = -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node and MFFC of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManDeleteNode_rec( Ntk_Obj_t * pObj )
+{
+    Vec_Ptr_t * vNodes;
+    int i;
+    assert( !Ntk_ObjIsPi(pObj) );
+    assert( Ntk_ObjFanoutNum(pObj) == 0 );
+    vNodes = Vec_PtrAlloc( 100 );
+    Ntk_ObjCollectFanins( pObj, vNodes );
+    Ntk_ManDeleteNode( pObj );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( Ntk_ObjIsNode(pObj) && Ntk_ObjFanoutNum(pObj) == 0 )
+            Ntk_ManDeleteNode_rec( pObj );
+    Vec_PtrFree( vNodes );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntk/ntkTiming.c b/src/aig/ntk/ntkTiming.c
new file mode 100644
index 00000000..f57c7987
--- /dev/null
+++ b/src/aig/ntk/ntkTiming.c
@@ -0,0 +1,353 @@
+/**CFile****************************************************************
+
+  FileName    [ntkTiming.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Manipulation of timing information.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntkTiming.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntk.h"
+#include "if.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern void * Abc_FrameReadLibLut();   
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrepareTiming( Ntk_Man_t * pNtk )
+{
+    Ntk_Obj_t * pObj;
+    int i;
+    Ntk_ManForEachObj( pNtk, pObj, i )
+    {
+        pObj->tArrival = pObj->tSlack = 0.0;
+        pObj->tRequired = AIG_INFINITY;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the pins in the decreasing order of delays.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManDelayTraceSortPins( Ntk_Obj_t * pNode, int * pPinPerm, float * pPinDelays )
+{
+    Ntk_Obj_t * pFanin;
+    int i, j, best_i, temp;
+    // start the trivial permutation and collect pin delays
+    Ntk_ObjForEachFanin( pNode, pFanin, i )
+    {
+        pPinPerm[i] = i;
+        pPinDelays[i] = Ntk_ObjArrival(pFanin);
+    }
+    // selection sort the pins in the decreasible order of delays
+    // this order will match the increasing order of LUT input pins
+    for ( i = 0; i < Ntk_ObjFaninNum(pNode)-1; i++ )
+    {
+        best_i = i;
+        for ( j = i+1; j < Ntk_ObjFaninNum(pNode); j++ )
+            if ( pPinDelays[pPinPerm[j]] > pPinDelays[pPinPerm[best_i]] )
+                best_i = j;
+        if ( best_i == i )
+            continue;
+        temp = pPinPerm[i]; 
+        pPinPerm[i] = pPinPerm[best_i]; 
+        pPinPerm[best_i] = temp;
+    }
+    // verify
+    assert( Ntk_ObjFaninNum(pNode) == 0 || pPinPerm[0] < Ntk_ObjFaninNum(pNode) );
+    for ( i = 1; i < Ntk_ObjFaninNum(pNode); i++ )
+    {
+        assert( pPinPerm[i] < Ntk_ObjFaninNum(pNode) );
+        assert( pPinDelays[pPinPerm[i-1]] >= pPinDelays[pPinPerm[i]] );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, int fUseLutLib )
+{
+    int fUseSorting = 1;
+    int pPinPerm[32];
+    float pPinDelays[32];
+    If_Lib_t * pLutLib;
+    Ntk_Obj_t * pNode, * 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", 
+            pLutLib->LutMax, Ntk_ManGetFaninMax(pNtk) );
+        return -AIG_INFINITY;
+    }
+
+    // initialize the arrival times
+    Abc_NtkPrepareTiming( pNtk );
+
+    // propagate arrival times
+    vNodes = Ntk_ManDfs( pNtk );
+    Vec_PtrForEachEntry( vNodes, pNode, 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 )
+        {
+            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 )
+            {
+                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];
+            }
+            else
+            {
+                Ntk_ObjForEachFanin( pNode, pFanin, k )
+                    if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[k] )
+                        tArrival = Ntk_ObjArrival(pFanin) + pDelays[k];
+            }
+        }
+        if ( Ntk_ObjFaninNum(pNode) == 0 )
+            tArrival = 0.0;
+        Ntk_ObjSetArrival( pNode, 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));
+
+    // initialize the required times
+    Ntk_ManForEachPo( pNtk, pNode, i )
+        if ( Ntk_ObjRequired(Ntk_ObjFanin0(pNode)) > tArrival )
+            Ntk_ObjSetRequired( Ntk_ObjFanin0(pNode), tArrival );
+
+    // propagate the required times
+    vNodes = Ntk_ManDfsReverse( pNtk );
+    Vec_PtrForEachEntry( vNodes, pNode, 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 
+        {
+            pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
+            if ( fUseSorting )
+            {
+                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 );
+                }
+            }
+            else
+            {
+                Ntk_ObjForEachFanin( pNode, pFanin, k )
+                {
+                    tRequired = Ntk_ObjRequired(pNode) - pDelays[k];
+                    if ( Ntk_ObjRequired(pFanin) > tRequired )
+                        Ntk_ObjSetRequired( pFanin, tRequired );
+                }
+            }
+        }
+        // set slack for this object
+        tSlack = Ntk_ObjRequired(pNode) - Ntk_ObjArrival(pNode);
+        assert( tSlack + 0.001 > 0.0 );
+        Ntk_ObjSetSlack( pNode, tSlack < 0.0 ? 0.0 : tSlack );
+    }
+    Vec_PtrFree( vNodes );
+    return tArrival;
+}
+
+/**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 []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, int fUseLutLib, int fVerbose )
+{
+    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", 
+            pLutLib->LutMax, Ntk_ManGetFaninMax(pNtk) );
+        return;
+    }
+    // decide how many steps
+    nSteps = fUseLutLib ? 20 : Ntk_ManLevel(pNtk);
+    pCounters = ALLOC( int, nSteps + 1 );
+    memset( pCounters, 0, sizeof(int)*(nSteps + 1) );
+    // perform delay trace
+    tArrival = Ntk_ManDelayTraceLut( pNtk, fUseLutLib );
+    tDelta = tArrival / nSteps;
+    // count how many nodes have slack in the corresponding intervals
+    Ntk_ManForEachNode( pNtk, pNode, i )
+    {
+        if ( Ntk_ObjFaninNum(pNode) == 0 )
+            continue;
+        Num = Ntk_ObjSlack(pNode) / tDelta;
+        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" );
+    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) );
+    }
+    free( pCounters );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntk/ntkUtil.c b/src/aig/ntk/ntkUtil.c
new file mode 100644
index 00000000..543d1a60
--- /dev/null
+++ b/src/aig/ntk/ntkUtil.c
@@ -0,0 +1,174 @@
+/**CFile****************************************************************
+
+  FileName    [ntkUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Various utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntkUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Increments the current traversal ID of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManIncrementTravId( Ntk_Man_t * pNtk )
+{
+    Ntk_Obj_t * pObj;
+    int i;
+    if ( pNtk->nTravIds >= (1<<26)-1 )
+    {
+        pNtk->nTravIds = 0;
+        Ntk_ManForEachObj( pNtk, pObj, i )
+            pObj->TravId = 0;
+    }
+    pNtk->nTravIds++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the maximum number of fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_ManGetFaninMax( Ntk_Man_t * pNtk )
+{
+    Ntk_Obj_t * pNode;
+    int i, nFaninsMax = 0;
+    Ntk_ManForEachNode( pNtk, pNode, i )
+    {
+        if ( nFaninsMax < Ntk_ObjFaninNum(pNode) )
+            nFaninsMax = Ntk_ObjFaninNum(pNode);
+    }
+    return nFaninsMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the total number of all fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_ManGetTotalFanins( Ntk_Man_t * pNtk )
+{
+    Ntk_Obj_t * pNode;
+    int i, nFanins = 0;
+    Ntk_ManForEachNode( pNtk, pNode, i )
+        nFanins += Ntk_ObjFaninNum(pNode);
+    return nFanins;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+
+  Description [Assumes topological ordering of the nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_ManLevel( 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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_ManPiNum( Ntk_Man_t * pNtk )
+{
+    Ntk_Obj_t * pNode;
+    int i, Counter = 0;
+    Ntk_ManForEachPi( pNtk, pNode, i )
+        Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_ManPoNum( Ntk_Man_t * pNtk )
+{
+    Ntk_Obj_t * pNode;
+    int i, Counter = 0;
+    Ntk_ManForEachPo( pNtk, pNode, i )
+        Counter++;
+    return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntk/ntk_.c b/src/aig/ntk/ntk_.c
new file mode 100644
index 00000000..6bbb67a6
--- /dev/null
+++ b/src/aig/ntk/ntk_.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                                ///
+////////////////////////////////////////////////////////////////////////
+
+