Version abc80326

8 files changed, 395 insertions, 612 deletions

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 );