Version abc80326

34 files changed, 2699 insertions, 662 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 33f7b2a0..8901e8bb 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -47,6 +47,7 @@ extern "C" {
 
 typedef struct Aig_Man_t_            Aig_Man_t;
 typedef struct Aig_Obj_t_            Aig_Obj_t;
+typedef struct Aig_Box_t_            Aig_Box_t;
 typedef struct Aig_MmFixed_t_        Aig_MmFixed_t;    
 typedef struct Aig_MmFlex_t_         Aig_MmFlex_t;     
 typedef struct Aig_MmStep_t_         Aig_MmStep_t;     
@@ -61,7 +62,8 @@ typedef enum {
     AIG_OBJ_AND,                     // 5: AND node
     AIG_OBJ_EXOR,                    // 6: EXOR node
     AIG_OBJ_LATCH,                   // 7: latch
-    AIG_OBJ_VOID                     // 8: unused object
+    AIG_OBJ_BOX,                     // 8: latch
+    AIG_OBJ_VOID                     // 9: unused object
 } Aig_Type_t;
 
 // the AIG node
@@ -71,11 +73,11 @@ struct Aig_Obj_t_  // 8 words
     Aig_Obj_t *      pFanin0;        // fanin
     Aig_Obj_t *      pFanin1;        // fanin
     Aig_Obj_t *      pHaig;          // pointer to the HAIG node
-    unsigned int     Type    :  3;   // object type
+    unsigned int     Type    :  4;   // object type
     unsigned int     fPhase  :  1;   // value under 000...0 pattern
     unsigned int     fMarkA  :  1;   // multipurpose mask
     unsigned int     fMarkB  :  1;   // multipurpose mask
-    unsigned int     nRefs   : 26;   // reference count 
+    unsigned int     nRefs   : 25;   // reference count 
     unsigned         Level   : 24;   // the level of this node
     unsigned         nCuts   :  8;   // the number of cuts
     int              TravId;         // unique ID of last traversal involving the node
@@ -87,6 +89,16 @@ struct Aig_Obj_t_  // 8 words
     };
 };
 
+// the AIG box
+struct Aig_Box_t_  
+{
+    int              nInputs;        // the number of box inputs (POs)
+    int              i1Input;        // the first PO of the interval
+    int              nOutputs;       // the number of box outputs (PIs)
+    int              i1Output;       // the first PI of the interval
+    float **         pTable;         // the delay table of the box
+};
+
 // the AIG manager
 struct Aig_Man_t_
 {
@@ -317,6 +329,7 @@ static inline void         Aig_ObjClean( Aig_Obj_t * pObj )       { memset( pObj
 static inline Aig_Obj_t *  Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj )  { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } 
 static inline Aig_Obj_t *  Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj )    { return p->pEquivs? p->pEquivs[pObj->Id] : NULL;             } 
 static inline Aig_Obj_t *  Aig_ObjHaig( Aig_Obj_t * pObj )        { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); } 
+static inline int          Aig_ObjPioNum( Aig_Obj_t * pObj )      { assert( !Aig_ObjIsNode(pObj) ); return (int)pObj->pNext;                                                    }
 static inline int          Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )    
 { 
     if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; 
@@ -597,6 +610,9 @@ extern void            Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
 extern void            Aig_ManDump( Aig_Man_t * p );
 extern void            Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern void            Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
+extern void            Aig_ManSetPioNumbers( Aig_Man_t * p );
+extern void            Aig_ManCleanPioNumbers( Aig_Man_t * p );
+
 /*=== aigWin.c =========================================================*/
 extern void            Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
  
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 12f2e702..062173e6 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -85,7 +85,7 @@ Aig_Man_t * Aig_ManStart( int nNodesMax )
 Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
 {
     Aig_Man_t * pNew;
-    Aig_Obj_t * pObj;
+    Aig_Obj_t * pObj, * pObjNew;
     int i;
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
@@ -93,7 +93,11 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
     // create the PIs
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
     Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = Aig_ObjCreatePi(pNew);
+    {
+        pObjNew = Aig_ObjCreatePi( pNew );
+        pObjNew->Level = pObj->Level;
+        pObj->pData = pObjNew;
+    }
     return pNew;
 }
 
@@ -154,17 +158,11 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
     Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
-    Aig_ManForEachPi( p, pObj, i )
-    {
-        pObjNew = Aig_ObjCreatePi( pNew );
-        pObjNew->pHaig = pObj->pHaig;
-        pObjNew->Level = pObj->Level;
-        pObj->pData = pObjNew;
-    }
     // duplicate internal nodes
     if ( fOrdered )
     {
         Aig_ManForEachObj( p, pObj, i )
+        {
             if ( Aig_ObjIsBuf(pObj) )
             {
                 if ( pNew->pManHaig == NULL )
@@ -187,28 +185,70 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
                     pObj->pData = pObjNew;
                 }
             }
+            else if ( Aig_ObjIsPi(pObj) )
+            {
+                pObjNew = Aig_ObjCreatePi( pNew );
+                pObjNew->pHaig = pObj->pHaig;
+                pObjNew->Level = pObj->Level;
+                pObj->pData = pObjNew;
+            }
+            else if ( Aig_ObjIsPo(pObj) )
+            {
+                pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+                pObjNew->pHaig = pObj->pHaig;
+                pObj->pData = pObjNew;
+            }
+            else
+                assert( 0 );
+        }
     }
     else
     {
+/*
+        Aig_ManForEachPi( p, pObj, i )
+        {
+            pObjNew = Aig_ObjCreatePi( pNew );
+            pObjNew->pHaig = pObj->pHaig;
+            pObjNew->Level = pObj->Level;
+            pObj->pData = pObjNew;
+        }
+*/
         Aig_ManForEachObj( p, pObj, i )
-            if ( !Aig_ObjIsPo(pObj) )
+        {
+            if ( Aig_ObjIsPi(pObj) )
             {
-                Aig_ManDup_rec( pNew, p, pObj );        
-                assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
+                pObjNew = Aig_ObjCreatePi( pNew );
+                pObjNew->pHaig = pObj->pHaig;
+                pObjNew->Level = pObj->Level;
+                pObj->pData = pObjNew;
             }
+            else if ( Aig_ObjIsPo(pObj) )
+            {
+                Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );        
+//                assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
+                pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+                pObjNew->pHaig = pObj->pHaig;
+                pObj->pData = pObjNew;
+            }
+        }
+/*
+        Aig_ManForEachPo( p, pObj, i )
+        {
+            pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+            pObjNew->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
+        }
+*/
     }
     // add the POs
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-        pObjNew->pHaig = pObj->pHaig;
-        pObj->pData = pObjNew;
-    }
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
     // pass the HAIG to the new AIG
     p->pManHaig = NULL;
     Aig_ManForEachObj( p, pObj, i )
         pObj->pHaig = NULL;
+    // duplicate the timing manager
+    if ( p->pManTime )
+        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDup(): The check has failed.\n" );
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index f6f34de9..7900da51 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -848,6 +848,48 @@ void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName )
     Vec_PtrFree( vNodes );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sets the PI/PO numbers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManSetPioNumbers( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pNext = (Aig_Obj_t *)i;
+    Aig_ManForEachPo( p, pObj, i )
+        pObj->pNext = (Aig_Obj_t *)i;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the PI/PO numbers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCleanPioNumbers( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pNext = NULL;
+    Aig_ManForEachPo( p, pObj, i )
+        pObj->pNext = NULL;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c
index 67b6bcdc..d7811f82 100644
--- a/src/aig/bdc/bdcCore.c
+++ b/src/aig/bdc/bdcCore.c
@@ -212,6 +212,11 @@ int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int n
     p->nWords = Kit_TruthWordNum( nVars );
     p->nNodesMax = nNodesMax;
     Bdc_ManPrepare( p, vDivs );
+    if ( puCare && Kit_TruthIsConst0( puCare, nVars ) )
+    {
+        p->pRoot = Bdc_Not(p->pNodes);
+        return 0;
+    }
     // copy the function
     Bdc_IsfStart( p, pIsf );
     if ( puCare )
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index c4c7db0a..a428f435 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -91,7 +91,7 @@ extern int             Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
 extern Aig_Man_t *     Dar_ManRewriteDefault( Aig_Man_t * pAig );
 extern Aig_Man_t *     Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
 extern Aig_Man_t *     Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
-extern Aig_Man_t *     Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
+extern Aig_Man_t *     Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fVerbose );
 extern Aig_Man_t *     Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose );
 
 #ifdef __cplusplus
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index b3c5d645..01f75e32 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "darInt.h"
+#include "tim.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -62,23 +63,61 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     // map the PI nodes
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = Aig_ObjCreatePi(pNew);
-    // balance the AIG
     vStore = Vec_VecAlloc( 50 );
-    Aig_ManForEachPo( p, pObj, i )
+    if ( p->pManTime != NULL )
     {
-        pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-        pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
-        pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
-        Aig_ObjCreatePo( pNew, pObjNew );
+        float arrTime;
+        Tim_ManIncrementTravId( p->pManTime );
+        Aig_ManSetPioNumbers( p );
+        Aig_ManForEachObj( p, pObj, i )
+        {
+            if ( Aig_ObjIsAnd(pObj) || Aig_ObjIsConst1(pObj) )
+                continue;
+            if ( Aig_ObjIsPi(pObj) )
+            {
+                // copy the PI
+                pObjNew = Aig_ObjCreatePi(pNew); 
+                pObj->pData = pObjNew;
+                // set the arrival time of the new PI
+                arrTime = Tim_ManGetPiArrival( p->pManTime, Aig_ObjPioNum(pObj) );
+                pObjNew->Level = (int)arrTime;
+            }
+            else if ( Aig_ObjIsPo(pObj) )
+            {
+                // perform balancing
+                pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+                pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+                pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
+                Aig_ObjCreatePo( pNew, pObjNew );
+                // save arrival time of the output
+                arrTime = (float)Aig_Regular(pObjNew)->Level;
+                Tim_ManSetPoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime );
+            }
+            else
+                assert( 0 );
+        }
+        Aig_ManCleanPioNumbers( p );
+        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
     }
-    Vec_VecFree( vStore );
-    // remove dangling nodes
-    if ( (i = Aig_ManCleanup( pNew )) )
+    else
     {
-//        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
+        Aig_ManForEachPi( p, pObj, i )
+        {
+            pObjNew = Aig_ObjCreatePi(pNew); 
+            pObjNew->Level = pObj->Level;
+            pObj->pData = pObjNew;
+        }
+        Aig_ManForEachPo( p, pObj, i )
+        {
+            pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+            pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+            pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
+            Aig_ObjCreatePo( pNew, pObjNew );
+        }
     }
+    Vec_VecFree( vStore );
+    // remove dangling nodes
+    Aig_ManCleanup( pNew );
     // check the resulting AIG
     if ( !Aig_ManCheck(pNew) )
         printf( "Dar_ManBalance(): The check has failed.\n" );
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index e690a61b..fad4148c 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -181,6 +181,14 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
+    // balance
+    if ( fBalance )
+    {
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
+    }
+
     return pAig;
 }
 
@@ -195,7 +203,7 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
+Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fVerbose )
 //alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
 {
     Aig_Man_t * pTemp;
@@ -208,6 +216,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
 
     pParsRwr->fUpdateLevel = fUpdateLevel;
     pParsRef->fUpdateLevel = fUpdateLevel;
+    pParsRwr->fFanout = fFanout;
 
     pParsRwr->fVerbose = 0;//fVerbose;
     pParsRef->fVerbose = 0;//fVerbose;
@@ -310,7 +319,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
     Vec_PtrPush( vAigs, pAig );
     pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose);
     Vec_PtrPush( vAigs, pAig );
-    pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, fVerbose);
+    pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose);
     Vec_PtrPush( vAigs, pAig );
     return vAigs;
 }
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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/module.make b/src/aig/ntl/module.make
index f47108a4..aba4fbf2 100644
--- a/src/aig/ntl/module.make
+++ b/src/aig/ntl/module.make
@@ -1,6 +1,7 @@
-SRC +=    src/aig/ntl/ntlAig.c \
-    src/aig/ntl/ntlCheck.c \
-    src/aig/ntl/ntlDfs.c \
+SRC +=    src/aig/ntl/ntlCheck.c \
+    src/aig/ntl/ntlCore.c \
+    src/aig/ntl/ntlExtract.c \
+    src/aig/ntl/ntlInsert.c \
     src/aig/ntl/ntlMan.c \
     src/aig/ntl/ntlMap.c \
     src/aig/ntl/ntlObj.c \
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index dbd8676b..caaa86f8 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -102,8 +102,8 @@ struct Ntl_Obj_t_
     unsigned           Id     : 27;    // object ID
     unsigned           MarkA  :  1;    // temporary mark  
     unsigned           MarkB  :  1;    // temporary mark
-    short              nFanins;        // the number of fanins
-    short              nFanouts;       // the number of fanouts
+    int                nFanins;        // the number of fanins
+    int                nFanouts;       // the number of fanouts
     union {                            // functionality
         Ntl_Mod_t *    pImplem;        // model (for boxes)
         char *         pSop;           // SOP (for logic nodes)
@@ -219,19 +219,18 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== ntlAig.c ==========================================================*/
-extern Aig_Obj_t *     Ntl_ManExtractAigNode( Ntl_Obj_t * pNode );
-extern int             Ntl_ManExtract( Ntl_Man_t * p );
-extern int             Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping );
-extern int             Ntl_ManInsertTest( Ntl_Man_t * p );
-extern int             Ntl_ManInsertTestFpga( Ntl_Man_t * p );
-extern int             Ntl_ManInsertTestIf( Ntl_Man_t * p );
+/*=== ntlCore.c ==========================================================*/
+extern int             Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig );
+extern int             Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig );
+/*=== ntlExtract.c ==========================================================*/
+extern Aig_Man_t *     Ntl_ManExtract( Ntl_Man_t * p );
+extern char *          Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
+/*=== ntlInsert.c ==========================================================*/
+extern int             Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
 /*=== ntlCheck.c ==========================================================*/
 extern int             Ntl_ManCheck( Ntl_Man_t * pMan );
 extern int             Ntl_ModelCheck( Ntl_Mod_t * pModel );
 extern void            Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
-/*=== ntlDfs.c ==========================================================*/
-extern int             Ntl_ManDfs( Ntl_Man_t * p );
 /*=== ntlMan.c ============================================================*/
 extern Ntl_Man_t *     Ntl_ManAlloc( char * pFileName );
 extern void            Ntl_ManFree( Ntl_Man_t * p );
diff --git a/src/aig/ntl/ntlCore.c b/src/aig/ntl/ntlCore.c
new file mode 100644
index 00000000..ed0f057b
--- /dev/null
+++ b/src/aig/ntl/ntlCore.c
@@ -0,0 +1,104 @@
+/**CFile****************************************************************
+
+  FileName    [ntlCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [DFS traversal.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts AIG from the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig )
+{
+    extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * pAig, int fUpdateLevel );
+    extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
+    Aig_Man_t * pTemp;
+    // perform synthesis
+//printf( "Pre-synthesis AIG:  " );
+//Aig_ManPrintStats( pAig );
+//    pTemp = Dar_ManBalance( pAig, 1 );
+    pTemp = Dar_ManCompress( pAig, 1, 1, 0 );
+//printf( "Post-synthesis AIG: " );
+//Aig_ManPrintStats( pTemp );
+    return pTemp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testing procedure for insertion of mapping into the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig )
+{
+    Vec_Ptr_t * vMapping;
+    int RetValue;
+    vMapping = Ntl_MappingFromAig( pAig );
+    RetValue = Ntl_ManInsert( p, vMapping, pAig );
+    Vec_PtrFree( vMapping );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testing procedure for insertion of mapping into the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig )
+{
+    Vec_Ptr_t * vMapping;
+    int RetValue;
+    vMapping = Ntl_MappingIf( p, pAig );
+    RetValue = Ntl_ManInsert( p, vMapping, pAig );
+    Vec_PtrFree( vMapping );
+    return RetValue;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlDfs.c b/src/aig/ntl/ntlDfs.c
deleted file mode 100644
index 1e9503a4..00000000
--- a/src/aig/ntl/ntlDfs.c
+++ /dev/null
@@ -1,184 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ntlDfs.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Netlist representation.]
-
-  Synopsis    [DFS traversal.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: ntlDfs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "ntl.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the nodes in a topological order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_ManDfs_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
-{
-    Ntl_Obj_t * pObj;
-    Ntl_Net_t * pNetFanin;
-    int i;
-    // skip visited
-    if ( pNet->nVisits == 2 ) 
-        return 1;
-    // if the node is on the path, this is a combinational loop
-    if ( pNet->nVisits == 1 )
-        return 0; 
-    // mark the node as the one on the path
-    pNet->nVisits = 1;
-    // derive the box
-    pObj = pNet->pDriver;
-    assert( Ntl_ObjIsNode(pObj) || Ntl_ObjIsBox(pObj) );
-    // visit the input nets of the box
-    Ntl_ObjForEachFanin( pObj, pNetFanin, i )
-        if ( !Ntl_ManDfs_rec( p, pNetFanin ) )
-            return 0;
-    // add box inputs/outputs to COs/CIs
-    if ( Ntl_ObjIsBox(pObj) )
-    {
-        int LevelCur, LevelMax = -AIG_INFINITY;
-        Vec_IntPush( p->vBox1Cos, Aig_ManPoNum(p->pAig) );
-        Ntl_ObjForEachFanin( pObj, pNetFanin, i )
-        {
-            LevelCur = Aig_ObjLevel( Aig_Regular(pNetFanin->pFunc) );
-            LevelMax = AIG_MAX( LevelMax, LevelCur );
-            Vec_PtrPush( p->vCos, pNetFanin );
-            Aig_ObjCreatePo( p->pAig, pNetFanin->pFunc );
-        }
-        Ntl_ObjForEachFanout( pObj, pNetFanin, i )
-        {
-            Vec_PtrPush( p->vCis, pNetFanin );
-            pNetFanin->pFunc = Aig_ObjCreatePi( p->pAig );
-            Aig_ObjSetLevel( pNetFanin->pFunc, LevelMax + 1 );
-        }
-//printf( "Creating fake PO with ID = %d.\n", Aig_ManPo(p->pAig, Vec_IntEntryLast(p->vBox1Cos))->Id );
-    }
-    // store the node
-    Vec_PtrPush( p->vNodes, pObj );
-    if ( Ntl_ObjIsNode(pObj) )
-        pNet->pFunc = Ntl_ManExtractAigNode( pObj );
-    pNet->nVisits = 2;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs DFS.]
-
-  Description [Checks for combinational loops. Collects PI/PO nets.
-  Collects nodes in the topological order.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_ManDfs( Ntl_Man_t * p )
-{
-    Ntl_Mod_t * pRoot;
-    Ntl_Obj_t * pObj;
-    Ntl_Net_t * pNet;
-    int i, nUselessObjects;
-    assert( Vec_PtrSize(p->vCis) == 0 );
-    assert( Vec_PtrSize(p->vCos) == 0 );
-    assert( Vec_PtrSize(p->vNodes) == 0 );
-    assert( Vec_IntSize(p->vBox1Cos) == 0 );
-    // get the root model
-    pRoot = Vec_PtrEntry( p->vModels, 0 );
-    // collect primary inputs
-    Ntl_ModelForEachPi( pRoot, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        Vec_PtrPush( p->vCis, pNet );
-        pNet->pFunc = Aig_ObjCreatePi( p->pAig );
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManDfs(): Primary input appears twice in the list.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // collect latch outputs
-    Ntl_ModelForEachLatch( pRoot, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        Vec_PtrPush( p->vCis, pNet );
-        pNet->pFunc = Aig_ObjCreatePi( p->pAig );
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManDfs(): Latch output is duplicated or defined as a primary input.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // visit the nodes starting from primary outputs
-    Ntl_ModelForEachPo( pRoot, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManDfs_rec( p, pNet ) )
-        {
-            printf( "Ntl_ManDfs(): Error: Combinational loop is detected.\n" );
-            Vec_PtrClear( p->vCis );
-            Vec_PtrClear( p->vCos );
-            Vec_PtrClear( p->vNodes );
-            return 0;
-        }
-        Vec_PtrPush( p->vCos, pNet );
-        Aig_ObjCreatePo( p->pAig, pNet->pFunc );
-    }
-    // visit the nodes starting from latch inputs outputs
-    Ntl_ModelForEachLatch( pRoot, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManDfs_rec( p, pNet ) )
-        {
-            printf( "Ntl_ManDfs(): Error: Combinational loop is detected.\n" );
-            Vec_PtrClear( p->vCis );
-            Vec_PtrClear( p->vCos );
-            Vec_PtrClear( p->vNodes );
-            return 0;
-        }
-        Vec_PtrPush( p->vCos, pNet );
-        Aig_ObjCreatePo( p->pAig, pNet->pFunc );
-    }
-    // report the number of dangling objects
-    nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
-    if ( nUselessObjects )
-        printf( "The number of nodes that do not feed into POs = %d.\n", nUselessObjects );
-    return 1;    
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/ntl/ntlAig.c b/src/aig/ntl/ntlExtract.c
index c0a122d3..72a8bc40 100644
--- a/src/aig/ntl/ntlAig.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [ntlAig.c]
+  FileName    [ntlExtract.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: ntlAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: ntlExtract.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -353,12 +353,9 @@ Aig_Obj_t * Ntl_ManExtractAigNode( Ntl_Obj_t * pNode )
     return Ntl_ConvertSopToAigInternal( pMan, pNode, pNode->pSop );
 }
 
-
-
-
 /**Function*************************************************************
 
-  Synopsis    [Extracts AIG from the netlist.]
+  Synopsis    [Collects the nodes in a topological order.]
 
   Description []
                
@@ -367,205 +364,163 @@ Aig_Obj_t * Ntl_ManExtractAigNode( Ntl_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ManExtract_old( Ntl_Man_t * p )
+int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
 {
-    Ntl_Obj_t * pNode;
-    Ntl_Net_t * pNet;
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNetFanin;
     int i;
-    // check the DFS traversal
-    if ( !Ntl_ManDfs( p ) )
-        return 0;
-    // start the AIG manager
-    assert( p->pAig == NULL );
-    p->pAig = Aig_ManStart( 10000 );
-    // create the primary inputs
-    Ntl_ManForEachCiNet( p, pNet, i )
-        pNet->pFunc = Aig_ObjCreatePi( p->pAig );
-    // convert internal nodes to AIGs
-    Ntl_ManForEachNode( p, pNode, i )
-        Ntl_ObjFanout0(pNode)->pFunc = Ntl_ManExtractAigNode( pNode );
-    // create the primary outputs
-    Ntl_ManForEachCoNet( p, pNet, i )
-        Aig_ObjCreatePo( p->pAig, pNet->pFunc );
-    // cleanup the AIG
-    Aig_ManCleanup( p->pAig );
+    // skip visited
+    if ( pNet->nVisits == 2 ) 
+        return 1;
+    // if the node is on the path, this is a combinational loop
+    if ( pNet->nVisits == 1 )
+        return 0; 
+    // mark the node as the one on the path
+    pNet->nVisits = 1;
+    // derive the box
+    pObj = pNet->pDriver;
+    assert( Ntl_ObjIsNode(pObj) || Ntl_ObjIsBox(pObj) );
+    // visit the input nets of the box
+    Ntl_ObjForEachFanin( pObj, pNetFanin, i )
+        if ( !Ntl_ManExtract_rec( p, pNetFanin ) )
+            return 0;
+    // add box inputs/outputs to COs/CIs
+    if ( Ntl_ObjIsBox(pObj) )
+    {
+        int LevelCur, LevelMax = -AIG_INFINITY;
+        Vec_IntPush( p->vBox1Cos, Aig_ManPoNum(p->pAig) );
+        Ntl_ObjForEachFanin( pObj, pNetFanin, i )
+        {
+            LevelCur = Aig_ObjLevel( Aig_Regular(pNetFanin->pFunc) );
+            LevelMax = AIG_MAX( LevelMax, LevelCur );
+            Vec_PtrPush( p->vCos, pNetFanin );
+            Aig_ObjCreatePo( p->pAig, pNetFanin->pFunc );
+        }
+        Ntl_ObjForEachFanout( pObj, pNetFanin, i )
+        {
+            Vec_PtrPush( p->vCis, pNetFanin );
+            pNetFanin->pFunc = Aig_ObjCreatePi( p->pAig );
+            Aig_ObjSetLevel( pNetFanin->pFunc, LevelMax + 1 );
+        }
+//printf( "Creating fake PO with ID = %d.\n", Aig_ManPo(p->pAig, Vec_IntEntryLast(p->vBox1Cos))->Id );
+    }
+    // store the node
+    Vec_PtrPush( p->vNodes, pObj );
+    if ( Ntl_ObjIsNode(pObj) )
+        pNet->pFunc = Ntl_ManExtractAigNode( pObj );
+    pNet->nVisits = 2;
     return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Extracts AIG from the netlist.]
+  Synopsis    [Performs DFS.]
 
-  Description []
+  Description [Checks for combinational loops. Collects PI/PO nets.
+  Collects nodes in the topological order.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ManExtract( Ntl_Man_t * p )
+Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
 {
+    Aig_Man_t * pAig;
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNet;
+    int i, nUselessObjects;
+    assert( Vec_PtrSize(p->vCis) == 0 );
+    assert( Vec_PtrSize(p->vCos) == 0 );
+    assert( Vec_PtrSize(p->vNodes) == 0 );
+    assert( Vec_IntSize(p->vBox1Cos) == 0 );
     // start the AIG manager
     assert( p->pAig == NULL );
     p->pAig = Aig_ManStart( 10000 );
-    // check the DFS traversal
-    if ( !Ntl_ManDfs( p ) )
-        return 0;
-    // cleanup the AIG
-    Aig_ManCleanup( p->pAig );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Inserts the given mapping into the netlist.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping )
-{
-    char Buffer[100];
-    Vec_Ptr_t * vCopies;
-    Vec_Int_t * vCover;
-    Ntl_Mod_t * pRoot;
-    Ntl_Obj_t * pNode;
-    Ntl_Net_t * pNet, * pNetCo;
-    Ntl_Lut_t * pLut;
-    int i, k, nDigits;
-    // remove old nodes
+    // get the root model
     pRoot = Vec_PtrEntry( p->vModels, 0 );
-    Ntl_ModelForEachNode( pRoot, pNode, i )
-        Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
-    // start mapping of AIG nodes into their copies
-    vCopies = Vec_PtrStart( Aig_ManObjNumMax(p->pAig) );
-    Ntl_ManForEachCiNet( p, pNet, i )
-        Vec_PtrWriteEntry( vCopies, pNet->pFunc->Id, pNet );
-    // create a new node for each LUT
-    vCover = Vec_IntAlloc( 1 << 16 );
-    nDigits = Aig_Base10Log( Vec_PtrSize(vMapping) );
-    Vec_PtrForEachEntry( vMapping, pLut, i )
+    // collect primary inputs
+    Ntl_ModelForEachPi( pRoot, pObj, i )
     {
-        pNode = Ntl_ModelCreateNode( pRoot, pLut->nFanins );
-        pNode->pSop = Ntl_SopFromTruth( p, pLut->pTruth, pLut->nFanins, vCover );
-        if ( !Kit_TruthIsConst0(pLut->pTruth, pLut->nFanins) && !Kit_TruthIsConst1(pLut->pTruth, pLut->nFanins) )
+        assert( Ntl_ObjFanoutNum(pObj) == 1 );
+        pNet = Ntl_ObjFanout0(pObj);
+        Vec_PtrPush( p->vCis, pNet );
+        pNet->pFunc = Aig_ObjCreatePi( p->pAig );
+        if ( pNet->nVisits )
         {
-            for ( k = 0; k < pLut->nFanins; k++ )
-            {
-                pNet = Vec_PtrEntry( vCopies, pLut->pFanins[k] );
-                if ( pNet == NULL )
-                {
-                    printf( "Ntl_ManInsert(): Internal error: Net not found.\n" );
-                    return 0;
-                }
-                Ntl_ObjSetFanin( pNode, pNet, k );
-            }
+            printf( "Ntl_ManExtract(): Primary input appears twice in the list.\n" );
+            return 0;
         }
-        sprintf( Buffer, "lut%0*d", nDigits, i );
-        if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
+        pNet->nVisits = 2;
+    }
+    // collect latch outputs
+    Ntl_ModelForEachLatch( pRoot, pObj, i )
+    {
+        assert( Ntl_ObjFanoutNum(pObj) == 1 );
+        pNet = Ntl_ObjFanout0(pObj);
+        Vec_PtrPush( p->vCis, pNet );
+        pNet->pFunc = Aig_ObjCreatePi( p->pAig );
+        if ( pNet->nVisits )
         {
-            printf( "Ntl_ManInsert(): Internal error: Intermediate net name is not unique.\n" );
+            printf( "Ntl_ManExtract(): Latch output is duplicated or defined as a primary input.\n" );
             return 0;
         }
-        pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
-        if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
+        pNet->nVisits = 2;
+    }
+    // visit the nodes starting from primary outputs
+    Ntl_ModelForEachPo( pRoot, pObj, i )
+    {
+        pNet = Ntl_ObjFanin0(pObj);
+        if ( !Ntl_ManExtract_rec( p, pNet ) )
         {
-            printf( "Ntl_ManInsert(): Internal error: Net has more than one fanin.\n" );
+            printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
+            Vec_PtrClear( p->vCis );
+            Vec_PtrClear( p->vCos );
+            Vec_PtrClear( p->vNodes );
             return 0;
         }
-        Vec_PtrWriteEntry( vCopies, pLut->Id, pNet );
+        Vec_PtrPush( p->vCos, pNet );
+        Aig_ObjCreatePo( p->pAig, pNet->pFunc );
     }
-    Vec_IntFree( vCover );
-    // mark CIs and outputs of the registers
-    Ntl_ManForEachCiNet( p, pNetCo, i )
-        pNetCo->nVisits = 101;
-    // update the CO pointers
-    Ntl_ManForEachCoNet( p, pNetCo, i )
+    // visit the nodes starting from latch inputs outputs
+    Ntl_ModelForEachLatch( pRoot, pObj, i )
     {
-        if ( pNetCo->nVisits == 101 )
-            continue;
-        pNetCo->nVisits = 101;
-        pNet = Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pFunc)->Id );
-        pNode = Ntl_ModelCreateNode( pRoot, 1 );
-        pNode->pSop = Aig_IsComplement(pNetCo->pFunc)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
-        Ntl_ObjSetFanin( pNode, pNet, 0 );
-        // update the CO driver net
-        pNetCo->pDriver = NULL;
-        if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
+        pNet = Ntl_ObjFanin0(pObj);
+        if ( !Ntl_ManExtract_rec( p, pNet ) )
         {
-            printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
+            printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
+            Vec_PtrClear( p->vCis );
+            Vec_PtrClear( p->vCos );
+            Vec_PtrClear( p->vNodes );
             return 0;
         }
+        Vec_PtrPush( p->vCos, pNet );
+        Aig_ObjCreatePo( p->pAig, pNet->pFunc );
     }
-    Vec_PtrFree( vCopies );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Extracts AIG from the netlist.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_ManPerformSynthesis( Ntl_Man_t * p )
-{
-    extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
-    extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
-    Aig_Man_t * pTemp;
-    Ntl_Net_t * pNet;
-    int i;
-    // perform synthesis
-printf( "Pre-synthesis AIG:  " );
-Aig_ManPrintStats( p->pAig );
-//    p->pAig = Dar_ManBalance( pTemp = p->pAig, 1 );
-    p->pAig = Dar_ManCompress( pTemp = p->pAig, 1, 1, 0 );
-    Ntl_ManForEachCiNet( p, pNet, i )
-        pNet->pFunc = Aig_ManPi( p->pAig, i );
-    Ntl_ManForEachCoNet( p, pNet, i )
-        pNet->pFunc = Aig_ObjChild0( Aig_ManPo( p->pAig, i ) );
-    Aig_ManStop( pTemp );
-printf( "Post-synthesis AIG: " );
-Aig_ManPrintStats( p->pAig );
-    return 1;
+    // report the number of dangling objects
+    nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
+    if ( nUselessObjects )
+        printf( "The number of nodes that do not feed into POs = %d.\n", nUselessObjects );
+    // cleanup the AIG
+    Aig_ManCleanup( p->pAig );
+    // extract the timing manager
+    assert( p->pManTime == NULL );
+    p->pManTime = Ntl_ManCreateTiming( p );
+    // discretize timing info
+    p->pAig->pManTime = Tim_ManDup( p->pManTime, 1 );
+    pAig = p->pAig; p->pAig = NULL;
+    return pAig;    
 }
 
-/**Function*************************************************************
 
-  Synopsis    [Testing procedure for insertion of mapping into the netlist.]
 
-  Description []
-               
-  SideEffects []
 
-  SeeAlso     []
 
-***********************************************************************/
-int Ntl_ManInsertTest( Ntl_Man_t * p )
-{
-    Vec_Ptr_t * vMapping;
-    int RetValue;
-    if ( !Ntl_ManExtract( p ) )
-        return 0;
-    assert( p->pAig != NULL );
-    Ntl_ManPerformSynthesis( p );
-    vMapping = Ntl_MappingFromAig( p->pAig );
-    RetValue = Ntl_ManInsert( p, vMapping );
-    Vec_PtrFree( vMapping );
-    return RetValue;
-}
 
 /**Function*************************************************************
 
-  Synopsis    [Testing procedure for insertion of mapping into the netlist.]
+  Synopsis    [Extracts AIG from the netlist.]
 
   Description []
                
@@ -574,19 +529,32 @@ int Ntl_ManInsertTest( Ntl_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ManInsertTestIf( Ntl_Man_t * p )
+/*
+int Ntl_ManExtract_old( Ntl_Man_t * p )
 {
-    Vec_Ptr_t * vMapping;
-    int RetValue;
-    if ( !Ntl_ManExtract( p ) )
+    Ntl_Obj_t * pNode;
+    Ntl_Net_t * pNet;
+    int i;
+    // check the DFS traversal
+    if ( !Ntl_ManDfs( p ) )
         return 0;
-    assert( p->pAig != NULL );
-//    Ntl_ManPerformSynthesis( p );
-    vMapping = Ntl_MappingIf( p, p->pAig );
-    RetValue = Ntl_ManInsert( p, vMapping );
-    Vec_PtrFree( vMapping );
-    return RetValue;
+    // start the AIG manager
+    assert( p->pAig == NULL );
+    p->pAig = Aig_ManStart( 10000 );
+    // create the primary inputs
+    Ntl_ManForEachCiNet( p, pNet, i )
+        pNet->pFunc = Aig_ObjCreatePi( p->pAig );
+    // convert internal nodes to AIGs
+    Ntl_ManForEachNode( p, pNode, i )
+        Ntl_ObjFanout0(pNode)->pFunc = Ntl_ManExtractAigNode( pNode );
+    // create the primary outputs
+    Ntl_ManForEachCoNet( p, pNet, i )
+        Aig_ObjCreatePo( p->pAig, pNet->pFunc );
+    // cleanup the AIG
+    Aig_ManCleanup( p->pAig );
+    return 1;
 }
+*/
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
new file mode 100644
index 00000000..971d1278
--- /dev/null
+++ b/src/aig/ntl/ntlInsert.c
@@ -0,0 +1,131 @@
+/**CFile****************************************************************
+
+  FileName    [ntlInsert.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Procedures to insert mapping into a design.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlInsert.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the given mapping into the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
+{
+    char Buffer[100];
+    Vec_Ptr_t * vCopies;
+    Vec_Int_t * vCover;
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pNode;
+    Ntl_Net_t * pNet, * pNetCo;
+    Ntl_Lut_t * pLut;
+    int i, k, nDigits;
+    // map the AIG back onto the design
+    Ntl_ManForEachCiNet( p, pNet, i )
+        pNet->pFunc = Aig_ManPi( pAig, i );
+    Ntl_ManForEachCoNet( p, pNet, i )
+        pNet->pFunc = Aig_ObjChild0( Aig_ManPo( pAig, i ) );
+    // remove old nodes
+    pRoot = Vec_PtrEntry( p->vModels, 0 );
+    Ntl_ModelForEachNode( pRoot, pNode, i )
+        Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
+    // start mapping of AIG nodes into their copies
+    vCopies = Vec_PtrStart( Aig_ManObjNumMax(pAig) );
+    Ntl_ManForEachCiNet( p, pNet, i )
+        Vec_PtrWriteEntry( vCopies, pNet->pFunc->Id, pNet );
+    // create a new node for each LUT
+    vCover = Vec_IntAlloc( 1 << 16 );
+    nDigits = Aig_Base10Log( Vec_PtrSize(vMapping) );
+    Vec_PtrForEachEntry( vMapping, pLut, i )
+    {
+        pNode = Ntl_ModelCreateNode( pRoot, pLut->nFanins );
+        pNode->pSop = Ntl_SopFromTruth( p, pLut->pTruth, pLut->nFanins, vCover );
+        if ( !Kit_TruthIsConst0(pLut->pTruth, pLut->nFanins) && !Kit_TruthIsConst1(pLut->pTruth, pLut->nFanins) )
+        {
+            for ( k = 0; k < pLut->nFanins; k++ )
+            {
+                pNet = Vec_PtrEntry( vCopies, pLut->pFanins[k] );
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManInsert(): Internal error: Net not found.\n" );
+                    return 0;
+                }
+                Ntl_ObjSetFanin( pNode, pNet, k );
+            }
+        }
+        sprintf( Buffer, "lut%0*d", nDigits, i );
+        if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: Intermediate net name is not unique.\n" );
+            return 0;
+        }
+        pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
+        if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: Net has more than one fanin.\n" );
+            return 0;
+        }
+        Vec_PtrWriteEntry( vCopies, pLut->Id, pNet );
+    }
+    Vec_IntFree( vCover );
+    // mark CIs and outputs of the registers
+    Ntl_ManForEachCiNet( p, pNetCo, i )
+        pNetCo->nVisits = 101;
+    // update the CO pointers
+    Ntl_ManForEachCoNet( p, pNetCo, i )
+    {
+        if ( pNetCo->nVisits == 101 )
+            continue;
+        pNetCo->nVisits = 101;
+        pNet = Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pFunc)->Id );
+        pNode = Ntl_ModelCreateNode( pRoot, 1 );
+        pNode->pSop = Aig_IsComplement(pNetCo->pFunc)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
+        Ntl_ObjSetFanin( pNode, pNet, 0 );
+        // update the CO driver net
+        pNetCo->pDriver = NULL;
+        if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
+            return 0;
+        }
+    }
+    Vec_PtrFree( vCopies );
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index 9b4aff5f..b5331ae2 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -87,6 +87,7 @@ void Ntl_ManFree( Ntl_Man_t * p )
     if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 );
     if ( p->pMemSops ) Aig_MmFlexStop( p->pMemSops, 0 );
     if ( p->pAig )     Aig_ManStop( p->pAig );
+    if ( p->pManTime ) Tim_ManStop( p->pManTime );
     free( p );
 }
 
diff --git a/src/aig/ntl/ntlMap.c b/src/aig/ntl/ntlMap.c
index 59c40453..3de74200 100644
--- a/src/aig/ntl/ntlMap.c
+++ b/src/aig/ntl/ntlMap.c
@@ -20,6 +20,7 @@
 
 #include "ntl.h"
 #include "kit.h"
+#include "if.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -105,247 +106,6 @@ Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p )
 }
 
 
-#include "fpgaInt.h"
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively derives the truth table for the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Ntl_FpgaComputeTruth_rec( Fpga_Cut_t * pCut, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore, Vec_Ptr_t * vVisited, int nVars, int * pnCounter )
-{
-    unsigned * pTruth, * pTruth0, * pTruth1;
-    assert( !Fpga_IsComplement(pCut) );
-    // if the cut is visited, return the result
-    if ( pCut->pRoot )
-        return (unsigned *)pCut->pRoot;
-    // compute the functions of the children
-    pTruth0 = Ntl_FpgaComputeTruth_rec( Fpga_CutRegular(pCut->pOne), vTruthElem, vTruthStore, vVisited, nVars, pnCounter );  
-    if ( Fpga_CutIsComplement(pCut->pOne) )
-        Kit_TruthNot( pTruth0, pTruth0, nVars );
-    pTruth1 = Ntl_FpgaComputeTruth_rec( Fpga_CutRegular(pCut->pTwo), vTruthElem, vTruthStore, vVisited, nVars, pnCounter );   
-    if ( Fpga_CutIsComplement(pCut->pTwo) )
-        Kit_TruthNot( pTruth1, pTruth1, nVars );
-    // get the function of the cut
-    pTruth = Vec_PtrEntry( vTruthStore, (*pnCounter)++ );
-    Kit_TruthAnd( pTruth, pTruth0, pTruth1, nVars );
-    if ( pCut->Phase )
-        Kit_TruthNot( pTruth, pTruth, nVars );
-    assert( pCut->pRoot == NULL );
-    pCut->pRoot = (Fpga_Node_t *)pTruth;
-    // add this cut to the visited list
-    Vec_PtrPush( vVisited, pCut );
-    return pTruth;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the truth table for one cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Ntl_FpgaComputeTruth( Fpga_Cut_t * pCut, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore, Vec_Ptr_t * vVisited, int nVars )
-{
-    unsigned * pTruth;
-    int i, nCounter = 0;
-    assert( pCut->nLeaves > 1 );
-    // set the leaf variables
-    for ( i = 0; i < pCut->nLeaves; i++ )
-        pCut->ppLeaves[i]->pCuts->pRoot = (Fpga_Node_t *)Vec_PtrEntry( vTruthElem, i );
-    // recursively compute the function
-    Vec_PtrClear( vVisited );
-    pTruth = Ntl_FpgaComputeTruth_rec( pCut, vTruthElem, vTruthStore, vVisited, nVars, &nCounter ); 
-    // clean the intermediate BDDs
-    for ( i = 0; i < pCut->nLeaves; i++ )
-        pCut->ppLeaves[i]->pCuts->pRoot = NULL;
-    Vec_PtrForEachEntry( vVisited, pCut, i )
-        pCut->pRoot = NULL;
-    return pTruth;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Load the network into FPGA manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fpga_Man_t * Ntl_ManToFpga( Aig_Man_t * p )
-{
-    Fpga_Man_t * pMan;
-    Aig_Obj_t * pNode;//, * pFanin, * pPrev;
-    float * pfArrivals;
-    int i;
-    // start the mapping manager and set its parameters
-    pMan = Fpga_ManCreate( Aig_ManPiNum(p), Aig_ManPoNum(p), 0 );
-    if ( pMan == NULL )
-        return NULL;
-    // set the arrival times
-    pfArrivals = ALLOC( float, Aig_ManPiNum(p) );
-    memset( pfArrivals, 0, sizeof(float) * Aig_ManPiNum(p) );
-    Fpga_ManSetInputArrivals( pMan, pfArrivals );
-    // create PIs and remember them in the old nodes
-    Aig_ManConst1(p)->pData = Fpga_ManReadConst1(pMan);
-    Aig_ManForEachPi( p, pNode, i )
-        pNode->pData = Fpga_ManReadInputs(pMan)[i];
-    // load the AIG into the mapper
-    Aig_ManForEachNode( p, pNode, i )
-    {
-        pNode->pData = Fpga_NodeAnd( pMan, 
-            Fpga_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ),
-            Fpga_NotCond( Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
-        // set up the choice node
-//        if ( Aig_AigNodeIsChoice( pNode ) )
-//            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
-//            {
-//                Fpga_NodeSetNextE( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
-//                Fpga_NodeSetRepr( (If_Obj_t *)pFanin->pData, (If_Obj_t *)pNode->pData );
-//            }
-    }
-    // set the primary outputs while copying the phase
-    Aig_ManForEachPo( p, pNode, i )
-        Fpga_ManReadOutputs(pMan)[i] = Fpga_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) );
-    assert( Fpga_NodeVecReadSize(pMan->vAnds) == Aig_ManNodeNum(p) );
-    return pMan;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the mapped network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Ntl_ManFromFpga( Aig_Man_t * p, Fpga_Man_t * pMan )
-{
-    Fpga_NodeVec_t * vFpgaMap;
-    Fpga_Node_t ** ppLeaves, * pNode; 
-    Fpga_Cut_t * pCutBest;
-    Vec_Ptr_t * vTruthElem, * vTruthStore, * vVisited, * vMapping;
-    Vec_Int_t * vFpgaToAig;
-    Aig_Obj_t * pObj;
-    Ntl_Lut_t * pLut;
-    unsigned * pTruth;
-    int i, k, nLuts, nLeaves, nWords, nVarsMax;
-    // create mapping of FPGA nodes into AIG nodes
-    vFpgaToAig = Vec_IntStart( Aig_ManObjNumMax(p) );
-    Vec_IntFill( vFpgaToAig, Aig_ManObjNumMax(p), -1 );
-    Aig_ManForEachObj( p, pObj, i )
-    {
-        if ( Aig_ObjIsPo(pObj) )
-            continue;
-        if ( Aig_ObjIsConst1(pObj) && pObj->pData == NULL )
-            continue;
-        pNode = pObj->pData;
-        assert( pNode != NULL );
-        Vec_IntWriteEntry( vFpgaToAig, Fpga_NodeReadNum(pNode), pObj->Id );
-    }
-    // create the mapping
-
-
-    // make sure nodes are in the top order!!!
-
-
-    nVarsMax = Fpga_ManReadVarMax( pMan );
-    nWords   = Aig_TruthWordNum( nVarsMax );
-    vFpgaMap = Fpga_ManReadMapping( pMan );
-    vMapping = Ntl_MappingAlloc( vFpgaMap->nSize + (int)(Aig_ManConst1(p)->nRefs > 0), nVarsMax );
-    nLuts    = 0;
-    if ( Aig_ManConst1(p)->nRefs > 0 )
-    {
-        pLut = Vec_PtrEntry( vMapping, nLuts++ );
-        pLut->Id = 0;
-        pLut->nFanins = 0;
-        memset( pLut->pTruth, 0xFF, 4 * nWords );
-    }
-    vVisited    = Vec_PtrAlloc( 1000 );
-    vTruthElem  = Vec_PtrAllocTruthTables( nVarsMax );
-    vTruthStore = Vec_PtrAllocSimInfo( 256, nWords );
-    for ( i = 0; i < vFpgaMap->nSize; i++ )
-    {
-        // get the best cut
-        pNode    = vFpgaMap->pArray[i];
-        pCutBest = Fpga_NodeReadCutBest( pNode );
-        nLeaves  = Fpga_CutReadLeavesNum( pCutBest ); 
-        ppLeaves = Fpga_CutReadLeaves( pCutBest );
-        // fill the LUT
-        pLut = Vec_PtrEntry( vMapping, nLuts++ );
-        pLut->Id = Vec_IntEntry( vFpgaToAig, Fpga_NodeReadNum(pNode) );
-        pLut->nFanins = nLeaves;
-        for ( k = 0; k < nLeaves; k++ )
-            pLut->pFanins[k] = Vec_IntEntry( vFpgaToAig, Fpga_NodeReadNum(ppLeaves[k]) );
-        // compute the truth table
-        pTruth = Ntl_FpgaComputeTruth( pCutBest, vTruthElem, vTruthStore, vVisited, nVarsMax );
-        memcpy( pLut->pTruth, pTruth, 4 * nWords );
-    }
-    assert( nLuts == Vec_PtrSize(vMapping) );
-    Vec_IntFree( vFpgaToAig );
-    Vec_PtrFree( vVisited );
-    Vec_PtrFree( vTruthElem );
-    Vec_PtrFree( vTruthStore );
-    return vMapping;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Interface with the FPGA mapping package.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Ntl_MappingFpga( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vMapping;
-    Fpga_Man_t * pMan;
-    // print a warning about choice nodes
-    if ( p->pEquivs )
-        printf( "Ntl_MappingFpga(): Performing FPGA mapping with choices.\n" );
-    // perform FPGA mapping
-    pMan = Ntl_ManToFpga( p );    
-    if ( pMan == NULL )
-        return NULL;
-    if ( !Fpga_Mapping( pMan ) )
-    {
-        Fpga_ManFree( pMan );
-        return NULL;
-    }
-    // transform the result of mapping into a BDD network
-    vMapping = Ntl_ManFromFpga( p, pMan );
-    Fpga_ManFree( pMan );
-    if ( vMapping == NULL )
-        return NULL;
-    return vMapping;
-}
-
-
-
-
-#include "if.h"
-
 /**Function*************************************************************
 
   Synopsis    [Load the network into FPGA manager.]
@@ -369,6 +129,7 @@ void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
     pPars->nFlowIters  =  1;
     pPars->nAreaIters  =  2;
     pPars->DelayTarget = -1;
+    pPars->Epsilon     =  (float)0.001;
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
@@ -486,6 +247,8 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
         {
             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) )
             If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
@@ -601,7 +364,7 @@ Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p )
     pIfMan = Ntk_ManToIf( p, pPars );    
     if ( pIfMan == NULL )
         return NULL;
-    pIfMan->pManTim = Ntl_ManCreateTiming( pMan );
+    pIfMan->pManTim = Tim_ManDup( pMan->pManTime, 0 );
     if ( !If_ManPerformMapping( pIfMan ) )
     {
         If_ManStop( pIfMan );
diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c
index 8d312dba..a71e1497 100644
--- a/src/aig/tim/tim.c
+++ b/src/aig/tim/tim.c
@@ -148,6 +148,49 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the timing manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fDiscrete )
+{
+    Tim_Man_t * pNew;
+    Tim_Box_t * pBox;
+    float * pDelayTableNew;
+    int i, k;
+    pNew = Tim_ManStart( p->nPis, p->nPos );
+    memcpy( pNew->pPis, p->pPis, sizeof(Tim_Obj_t) * p->nPis );
+    memcpy( pNew->pPos, p->pPos, sizeof(Tim_Obj_t) * p->nPos );
+    for ( k = 0; k < p->nPis; k++ )
+        pNew->pPis[k].TravId = 0;
+    for ( k = 0; k < p->nPos; k++ )
+        pNew->pPos[k].TravId = 0;
+    if ( fDiscrete )
+        for ( k = 0; k < p->nPis; k++ )
+            pNew->pPis[k].timeArr = 0.0; // modify here
+    pNew->vDelayTables = Vec_PtrAlloc( 100 );
+    Tim_ManForEachBox( p, pBox, i )
+    {
+        pDelayTableNew = ALLOC( float, pBox->nInputs * pBox->nOutputs );
+        Vec_PtrPush( pNew->vDelayTables, pDelayTableNew );
+        if ( fDiscrete )
+            for ( k = 0; k < pBox->nInputs * pBox->nOutputs; k++ )
+                pDelayTableNew[k] = 1.0; // modify here
+        else
+            memcpy( pDelayTableNew, pBox->pDelayTable, sizeof(float) * pBox->nInputs * pBox->nOutputs );
+        Tim_ManCreateBoxFirst( pNew, pBox->Inouts[0], pBox->nInputs, 
+            pBox->Inouts[pBox->nInputs], pBox->nOutputs, pDelayTableNew );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Stops the timing manager.]
 
   Description []
diff --git a/src/aig/tim/tim.h b/src/aig/tim/tim.h
index d7544169..f1fb992c 100644
--- a/src/aig/tim/tim.h
+++ b/src/aig/tim/tim.h
@@ -58,6 +58,7 @@ typedef struct Tim_Man_t_           Tim_Man_t;
 
 /*=== time.c ===========================================================*/
 extern Tim_Man_t *     Tim_ManStart( int nPis, int nPos );
+extern Tim_Man_t *     Tim_ManDup( Tim_Man_t * p, int fDiscrete );
 extern void            Tim_ManStop( Tim_Man_t * p );
 extern void            Tim_ManPrint( Tim_Man_t * p );
 extern void            Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7178cc0a..d9c68bc4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -200,6 +200,18 @@ static int Abc_CommandEnlarge        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandTraceStart     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTraceCheck     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int Abc_CommandAbc8Read       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Write      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Ps         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8If         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8DChoice    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Scl        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Lcorr      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Ssw        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Cec        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8DSec       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -215,6 +227,42 @@ static int Abc_CommandTraceCheck     ( Abc_Frame_t * pAbc, int argc, char ** arg
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_FrameClearDesign()
+{
+    extern Abc_Frame_t * Abc_FrameGetGlobalFrame();
+    extern void Ntl_ManFree( void * );
+    extern void Ntk_ManFree( void * );
+    Abc_Frame_t * pAbc;
+
+    pAbc = Abc_FrameGetGlobalFrame();
+    if ( pAbc->pAbc8Ntl )
+    {
+        Ntl_ManFree( pAbc->pAbc8Ntl );
+        pAbc->pAbc8Ntl = NULL;
+    }
+    if ( pAbc->pAbc8Aig )
+    {
+        Aig_ManStop( pAbc->pAbc8Aig );
+        pAbc->pAbc8Aig = NULL;
+    }
+    if ( pAbc->pAbc8Ntk )
+    {
+        Ntk_ManFree( pAbc->pAbc8Ntk );
+        pAbc->pAbc8Ntk = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_Init( Abc_Frame_t * pAbc )
 {
 //    Abc_NtkBddImplicationTest();
@@ -378,6 +426,18 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "indcut",        Abc_CommandIndcut,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "enlarge",       Abc_CommandEnlarge,          1 );
 
+    Cmd_CommandAdd( pAbc, "ABC8",         "*read",         Abc_CommandAbc8Read,         0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*write",        Abc_CommandAbc8Write,        0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*ps",           Abc_CommandAbc8Ps,           0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*if",           Abc_CommandAbc8If,           0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*dchoice",      Abc_CommandAbc8DChoice,      0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*scl",          Abc_CommandAbc8Scl,          0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*lcorr",        Abc_CommandAbc8Lcorr,        0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*ssw",          Abc_CommandAbc8Ssw,          0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*cec",          Abc_CommandAbc8Cec,          0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*dsec",         Abc_CommandAbc8DSec,         0 );
+
+
 //    Cmd_CommandAdd( pAbc, "Verification", "trace_start",   Abc_CommandTraceStart,       0 );
 //    Cmd_CommandAdd( pAbc, "Verification", "trace_check",   Abc_CommandTraceCheck,       0 );
 
@@ -412,6 +472,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
 ***********************************************************************/
 void Abc_End()
 {
+    Abc_FrameClearDesign(); 
+
 //    Dar_LibDumpPriorities();
     {
         extern int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk );
@@ -7813,12 +7875,12 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: drw [-C num] [-N num] [-flzvwh]\n" );
+    fprintf( pErr, "usage: drw [-C num] [-N num] [-lfzvwh]\n" );
     fprintf( pErr, "\t         performs combinational AIG rewriting\n" );
     fprintf( pErr, "\t-C num : the max number of cuts at a node [default = %d]\n", pPars->nCutsMax );
     fprintf( pErr, "\t-N num : the max number of subgraphs tried [default = %d]\n", pPars->nSubgMax );
-    fprintf( pErr, "\t-f     : toggle representing fanouts [default = %s]\n", pPars->fFanout? "yes": "no" );
     fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", pPars->fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "\t-f     : toggle representing fanouts [default = %s]\n", pPars->fFanout? "yes": "no" );
     fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", pPars->fUseZeros? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w     : toggle very verbose printout [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
@@ -7966,20 +8028,21 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int fBalance, fVerbose, fUpdateLevel, c;
+    int fBalance, fVerbose, fUpdateLevel, fFanout, c;
 
-    extern Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fFanout, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fBalance = 0;
-    fVerbose = 0;
+    fBalance     = 0;
+    fVerbose     = 0;
     fUpdateLevel = 0;
+    fFanout      = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "blvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "blfvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7989,6 +8052,9 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'l':
             fUpdateLevel ^= 1;
             break;
+        case 'f':
+            fFanout ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -8008,7 +8074,7 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "This command works only for strashed networks.\n" );
         return 1;
     }
-    pNtkRes = Abc_NtkDCompress2( pNtk, fBalance, fUpdateLevel, fVerbose );
+    pNtkRes = Abc_NtkDCompress2( pNtk, fBalance, fUpdateLevel, fFanout, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -8019,10 +8085,11 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dcompress2 [-blvh]\n" );
+    fprintf( pErr, "usage: dcompress2 [-blfvh]\n" );
     fprintf( pErr, "\t         performs combinational AIG optimization\n" );
     fprintf( pErr, "\t-b     : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
     fprintf( pErr, "\t-l     : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "\t-f     : toggle representing fanouts [default = %s]\n", fFanout? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -14599,6 +14666,356 @@ usage:
     return 1;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pFile;
+    char * pFileName;
+    int c;
+    extern void * Ioa_ReadBlif( char * pFileName, int fCheck );
+    extern Aig_Man_t * Ntl_ManExtract( void * p );
+
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    // get the input file name
+    pFileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( pFileName, "r" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open input file \"%s\". ", pFileName );
+        if ( pFileName = Extra_FileGetSimilarName( pFileName, ".blif", NULL, NULL, NULL, NULL ) )
+            fprintf( stdout, "Did you mean \"%s\"?", pFileName );
+        fprintf( stdout, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    Abc_FrameClearDesign(); 
+    pAbc->pAbc8Ntl = Ioa_ReadBlif( pFileName, 1 );
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Read(): Reading BLIF has failed.\n" );
+        return 1;
+    }
+    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Read(): AIG extraction has failed.\n" );
+        return 1;
+    }
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *read [-h]\n" );
+    fprintf( stdout, "\t        reads the design with whiteboxes\n" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    char * pFileName;
+    int c;
+    extern void Ioa_WriteBlif( void * p, char * pFileName );
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Write(): There is no design to write.\n" );
+        return 1;
+    }
+
+    // get the input file name
+    pFileName = argv[globalUtilOptind];
+    Ioa_WriteBlif( pAbc->pAbc8Ntl, pFileName );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *write [-h]\n" );
+    fprintf( stdout, "\t        write the design with whiteboxes\n" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    extern void Ntl_ManPrintStats( void * p );
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Write(): There is no design to show.\n" );
+        return 1;
+    }
+
+    // get the input file name
+    if ( pAbc->pAbc8Ntl )
+        Ntl_ManPrintStats( pAbc->pAbc8Ntl );
+    if ( pAbc->pAbc8Aig )
+        Aig_ManPrintStats( pAbc->pAbc8Aig );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *ps [-h]\n" );
+    fprintf( stdout, "\t        prints design statistics\n" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    extern int Ntl_ManInsertTest( void * p, Aig_Man_t * pAig );
+    extern int Ntl_ManInsertTestIf( void * p, Aig_Man_t * pAig );
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Write(): There is no AIG to map.\n" );
+        return 1;
+    }
+
+    // get the input file name
+    if ( !Ntl_ManInsertTestIf( pAbc->pAbc8Ntl, pAbc->pAbc8Aig ) )
+//    if ( !Ntl_ManInsertTest( pAbc->pAbc8Ntl, pAbc->pAbc8Aig ) )
+    {
+        printf( "Abc_CommandAbc8Write(): Tranformation of the netlist has failed.\n" );
+        return 1;
+    }
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *if [-h]\n" );
+    fprintf( stdout, "\t        performs mapping for logic extraced from the design\n" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8DChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Aig_Man_t * pAigNew;
+    int c;
+    extern Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig );
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8DChoice(): There is no AIG to synthesize.\n" );
+        return 1;
+    }
+
+    // get the input file name
+    pAigNew = Ntl_ManPerformSynthesis( pAbc->pAbc8Aig );
+    if ( pAigNew == NULL )
+    {
+        printf( "Abc_CommandAbc8DChoice(): Tranformation of the AIG has failed.\n" );
+        return 1;
+    }
+    Aig_ManStop( pAbc->pAbc8Aig );
+    pAbc->pAbc8Aig = pAigNew;
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *dchoice [-h]\n" );
+    fprintf( stdout, "\t        performs AIG-based synthesis\n" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    return 0;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index e1b3828e..94b6c52b 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -736,7 +736,7 @@ clk = clock();
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
+Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fFanout, int fVerbose )
 {
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
@@ -748,7 +748,7 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel,
 //    Aig_ManPrintStats( pMan );
 
 clk = clock();
-    pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fVerbose ); 
+    pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fFanout, fVerbose ); 
     Aig_ManStop( pTemp );
 //PRT( "time", clock() - clk );
 
@@ -1744,6 +1744,7 @@ void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
 ***********************************************************************/
 void Abc_NtkDarTestBlif( char * pFileName )
 {
+/*
     char Buffer[1000];
     Ntl_Man_t * p;
     p = Ioa_ReadBlif( pFileName, 1 );
@@ -1763,6 +1764,7 @@ void Abc_NtkDarTestBlif( char * pFileName )
     sprintf( Buffer, "test_.blif", p->pName );
     Ioa_WriteBlif( p, Buffer );
     Ntl_ManFree( p );
+*/
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index 967e4617..be16da95 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -795,6 +795,7 @@ void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
 {
     Abc_Obj_t * pFanout, * pTemp;
     int LevelOld, Lev, k, m;
+//    int Counter = 0, CounterMax = 0;
     // check if level has changed
     LevelOld = Abc_ObjLevel(pObjNew);
     if ( LevelOld == Abc_ObjLevelNew(pObjNew) )
@@ -808,6 +809,7 @@ void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
     // recursively update level
     Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, LevelOld )
     {
+//        Counter--;
         pTemp->fMarkA = 0;
         assert( Abc_ObjLevel(pTemp) == Lev );
         Abc_ObjSetLevel( pTemp, Abc_ObjLevelNew(pTemp) );
@@ -821,10 +823,13 @@ void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
             {
                 assert( Abc_ObjLevel(pFanout) >= Lev );
                 Vec_VecPush( vLevels, Abc_ObjLevel(pFanout), pFanout );
+//                Counter++;
+//                CounterMax = ABC_MAX( CounterMax, Counter );
                 pFanout->fMarkA = 1;
             }
         }
     }
+//    printf( "%d ", CounterMax );
 }
 
 /**Function*************************************************************
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index f82e12d6..0261d7da 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -73,6 +73,11 @@ struct Abc_Frame_t_
     void *          pLibGen;     // the current genlib
     void *          pLibSuper;   // the current supergate library
     void *          pLibVer;     // the current Verilog library
+
+    // new code
+    void *          pAbc8Ntl;    // the current design
+    void *          pAbc8Ntk;    // the current mapped network
+    void *          pAbc8Aig;    // the current AIG
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/pcm/module.make
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/ply/module.make
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index a3320ad3..e4790325 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -220,7 +220,7 @@ void Extra_StopManager( DdManager * dd )
     int RetValue;
     // check for remaining references in the package
     RetValue = Cudd_CheckZeroRef( dd );
-    if ( RetValue > 0 )
+    if ( RetValue > 10 )
         printf( "\nThe number of referenced nodes = %d\n\n", RetValue );
 //  Cudd_PrintInfo( dd, stdout );
     Cudd_Quit( dd );
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index bde2ad42..59ee7488 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -246,8 +246,8 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     if ( !pPars->fResub )
     {
         extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
-        Abc_NtkSweep( pNtk, 0 );
-        Abc_NtkBidecResyn( pNtk, 0 );
+//        Abc_NtkSweep( pNtk, 0 );
+//        Abc_NtkBidecResyn( pNtk, 0 );
     }
 
     p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk);