Version abc71226

15 files changed, 327 insertions, 108 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 28bae70f..d500139d 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -50,7 +50,6 @@ typedef struct Aig_Obj_t_            Aig_Obj_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;     
-typedef struct Aig_TMan_t_           Aig_TMan_t;
 
 // object types
 typedef enum { 
@@ -137,7 +136,7 @@ struct Aig_Man_t_
     Aig_Obj_t **     pObjCopies;     // mapping of AIG nodes into FRAIG nodes
     void (*pImpFunc) (void*, void*); // implication checking precedure
     void *           pImpData;       // implication checking data
-    Aig_TMan_t *     pManTime;       // the timing manager
+    void *           pManTime;       // the timing manager
     Vec_Ptr_t *      vMapped;
     Vec_Int_t *      vFlopNums;      
     void *           pSeqModel;
@@ -553,20 +552,6 @@ extern char *          Aig_MmStepEntryFetch( Aig_MmStep_t * p, int nBytes );
 extern void            Aig_MmStepEntryRecycle( Aig_MmStep_t * p, char * pEntry, int nBytes );
 extern int             Aig_MmStepReadMemUsage( Aig_MmStep_t * p );
 
-/*=== aigTime.c ===========================================================*/
-extern Aig_TMan_t *    Aig_TManStart( int nPis, int nPos );
-extern void            Aig_TManStop( Aig_TMan_t * p );
-extern void            Aig_TManSetDelayTables( Aig_TMan_t * p, Vec_Ptr_t * vDelayTables );
-extern void            Aig_TManCreateBox( Aig_TMan_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable );
-extern void            Aig_TManCreateBoxFirst( Aig_TMan_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable );
-extern void            Aig_TManIncrementTravId( Aig_TMan_t * p );
-extern void            Aig_TManInitPiArrival( Aig_TMan_t * p, int iPi, float Delay );
-extern void            Aig_TManInitPoRequired( Aig_TMan_t * p, int iPo, float Delay );
-extern void            Aig_TManSetPoArrival( Aig_TMan_t * p, int iPo, float Delay );
-extern void            Aig_TManSetPiRequired( Aig_TMan_t * p, int iPi, float Delay );
-extern float           Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi );
-extern float           Aig_TManGetPoRequired( Aig_TMan_t * p, int iPo );
-
 #ifdef __cplusplus
 }
 #endif
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index b915df99..d3fe1412 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "aig.h"
+#include "tim.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -276,7 +277,7 @@ void Aig_ManStop( Aig_Man_t * p )
     if ( p->time2 ) { PRT( "time2", p->time2 ); }
     // delete timing
     if ( p->pManTime )
-        Aig_TManStop( p->pManTime );
+        Tim_ManStop( p->pManTime );
     // delete fanout
     if ( p->pFanData ) 
         Aig_ManFanoutStop( p );
@@ -347,7 +348,7 @@ void Aig_ManPrintStats( Aig_Man_t * p )
     printf( "A = %7d. ",    Aig_ManAndNum(p) );
     if ( Aig_ManExorNum(p) )
         printf( "X = %5d. ",    Aig_ManExorNum(p) );
-//    if ( Aig_ManBufNum(p) )
+    if ( Aig_ManBufNum(p) )
         printf( "B = %5d. ",    Aig_ManBufNum(p) );
 //    printf( "Cre = %6d. ",  p->nCreated );
 //    printf( "Del = %6d. ",  p->nDeleted );
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 48d29115..667ceec1 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -17,7 +17,6 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigSeq.c \
     src/aig/aig/aigShow.c \
     src/aig/aig/aigTable.c \
-    src/aig/aig/aigTime.c \
     src/aig/aig/aigTiming.c \
     src/aig/aig/aigTruth.c \
     src/aig/aig/aigTsim.c \
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index ab93895d..1a3695e8 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -30,6 +30,7 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 #include "aig.h"
+#include "tim.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -70,7 +71,7 @@ struct Ntl_Man_t_
     Vec_Ptr_t *        vCos;           // the primary outputs of the extracted part 
     Vec_Ptr_t *        vNodes;         // the nodes of the abstracted part
     Aig_Man_t *        pAig;           // the extracted AIG
-    Aig_TMan_t *       pManTime;       // the timing manager
+    Tim_Man_t *        pManTime;       // the timing manager
 };
 
 struct Ntl_Mod_t_
@@ -219,6 +220,8 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
 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 );
 /*=== ntlCheck.c ==========================================================*/
 extern int             Ntl_ManCheck( Ntl_Man_t * pMan );
 extern int             Ntl_ModelCheck( Ntl_Mod_t * pModel );
@@ -235,6 +238,8 @@ extern void            Ntl_ModelFree( Ntl_Mod_t * p );
 /*=== ntlMap.c ============================================================*/
 extern Vec_Ptr_t *     Ntl_MappingAlloc( int nLuts, int nVars );
 extern Vec_Ptr_t *     Ntl_MappingFromAig( Aig_Man_t * p );
+extern Vec_Ptr_t *     Ntl_MappingFpga( Aig_Man_t * p );
+extern Vec_Ptr_t *     Ntl_MappingIf( Aig_Man_t * p );
 /*=== ntlObj.c ============================================================*/
 extern Ntl_Obj_t *     Ntl_ModelCreatePi( Ntl_Mod_t * pModel );
 extern Ntl_Obj_t *     Ntl_ModelCreatePo( Ntl_Mod_t * pModel, Ntl_Net_t * pNet );
diff --git a/src/aig/ntl/ntlAig.c b/src/aig/ntl/ntlAig.c
index bc8a8c35..c81280d7 100644
--- a/src/aig/ntl/ntlAig.c
+++ b/src/aig/ntl/ntlAig.c
@@ -413,27 +413,33 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping )
     Ntl_Net_t * pNet, * pNetCo;
     Ntl_Lut_t * pLut;
     int i, k, nDigits;
-    nDigits = Aig_Base10Log( Vec_PtrSize(vMapping) );
+    // 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(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 );
-    pRoot = Vec_PtrEntry( p->vModels, 0 );
+    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 );
-        for ( k = 0; k < pLut->nFanins; k++ )
+        if ( !Kit_TruthIsConst0(pLut->pTruth, pLut->nFanins) && !Kit_TruthIsConst1(pLut->pTruth, pLut->nFanins) )
         {
-            pNet = Vec_PtrEntry( vCopies, pLut->pFanins[k] );
-            if ( pNet == NULL )
+            for ( k = 0; k < pLut->nFanins; k++ )
             {
-                printf( "Ntl_ManInsert(): Internal error: Net not found.\n" );
-                return 0;
+                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 );
             }
-            Ntl_ObjSetFanin( pNode, pNet, k );
         }
         sprintf( Buffer, "lut%0*d", nDigits, i );
         if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
@@ -450,15 +456,18 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping )
         Vec_PtrWriteEntry( vCopies, pLut->Id, pNet );
     }
     Vec_IntFree( vCover );
-    // remove old nodes
-    Ntl_ManForEachNode( p, pNode, i )
-        Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
+    // 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" );
-        pNet = Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pFunc)->Id );
         Ntl_ObjSetFanin( pNode, pNet, 0 );
         // update the CO driver net
         pNetCo->pDriver = NULL;
@@ -474,6 +483,39 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping )
 
 /**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;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Testing procedure for insertion of mapping into the netlist.]
 
   Description []
@@ -490,12 +532,38 @@ int Ntl_ManInsertTest( Ntl_Man_t * p )
     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.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManInsertTestIf( 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_MappingIf( p->pAig );
+    RetValue = Ntl_ManInsert( p, vMapping );
+    Vec_PtrFree( vMapping );
+    return RetValue;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ntl/ntlMap.c b/src/aig/ntl/ntlMap.c
index 7ee0fba0..d4c7d81b 100644
--- a/src/aig/ntl/ntlMap.c
+++ b/src/aig/ntl/ntlMap.c
@@ -246,7 +246,7 @@ Vec_Ptr_t * Ntl_ManFromFpga( Aig_Man_t * p, Fpga_Man_t * pMan )
     Aig_Obj_t * pObj;
     Ntl_Lut_t * pLut;
     unsigned * pTruth;
-    int i, k = 0, nLeaves, nWords, nVarsMax;
+    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 );
@@ -254,18 +254,26 @@ Vec_Ptr_t * Ntl_ManFromFpga( Aig_Man_t * p, Fpga_Man_t * pMan )
     {
         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, k++ );
+        pLut = Vec_PtrEntry( vMapping, nLuts++ );
         pLut->Id = 0;
         pLut->nFanins = 0;
         memset( pLut->pTruth, 0xFF, 4 * nWords );
@@ -281,7 +289,7 @@ Vec_Ptr_t * Ntl_ManFromFpga( Aig_Man_t * p, Fpga_Man_t * pMan )
         nLeaves  = Fpga_CutReadLeavesNum( pCutBest ); 
         ppLeaves = Fpga_CutReadLeaves( pCutBest );
         // fill the LUT
-        pLut = Vec_PtrEntry( vMapping, k++ );
+        pLut = Vec_PtrEntry( vMapping, nLuts++ );
         pLut->Id = Vec_IntEntry( vFpgaToAig, Fpga_NodeReadNum(pNode) );
         pLut->nFanins = nLeaves;
         for ( k = 0; k < nLeaves; k++ )
@@ -290,7 +298,7 @@ Vec_Ptr_t * Ntl_ManFromFpga( Aig_Man_t * p, Fpga_Man_t * pMan )
         pTruth = Ntl_FpgaComputeTruth( pCutBest, vTruthElem, vTruthStore, vVisited, nVarsMax );
         memcpy( pLut->pTruth, pTruth, 4 * nWords );
     }
-    assert( k == Vec_PtrSize(vMapping) );
+    assert( nLuts == Vec_PtrSize(vMapping) );
     Vec_IntFree( vFpgaToAig );
     Vec_PtrFree( vVisited );
     Vec_PtrFree( vTruthElem );
@@ -309,13 +317,13 @@ Vec_Ptr_t * Ntl_ManFromFpga( Aig_Man_t * p, Fpga_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Ntl_ManFpga( Aig_Man_t * p )
+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_ManFpga(): Performing FPGA mapping with choices.\n" );
+        printf( "Ntl_MappingFpga(): Performing FPGA mapping with choices.\n" );
     // perform FPGA mapping
     pMan = Ntl_ManToFpga( p );    
     if ( pMan == NULL )
@@ -351,11 +359,12 @@ Vec_Ptr_t * Ntl_ManFpga( Aig_Man_t * p )
 ***********************************************************************/
 void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
 {
-    extern void * Abc_FrameReadLibLut();
+//    extern void * Abc_FrameReadLibLut();
     // set defaults
     memset( pPars, 0, sizeof(If_Par_t) );
     // user-controlable paramters
-    pPars->nLutSize    = -1;
+//    pPars->nLutSize    = -1;
+    pPars->nLutSize    =  6;
     pPars->nCutsMax    =  8;
     pPars->nFlowIters  =  1;
     pPars->nAreaIters  =  2;
@@ -363,21 +372,22 @@ void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
-    pPars->fExpRed     =  1;
+    pPars->fExpRed     =  0;
     pPars->fLatchPaths =  0;
     pPars->fEdge       =  1;
     pPars->fCutMin     =  1;
     pPars->fSeqMap     =  0;
-    pPars->fVerbose    =  0;
+    pPars->fVerbose    =  1;
     // internal parameters
     pPars->fTruth      =  1;
     pPars->nLatches    =  0;
     pPars->fLiftLeaves =  0;
-    pPars->pLutLib     =  Abc_FrameReadLibLut();
+//    pPars->pLutLib     =  Abc_FrameReadLibLut();
+    pPars->pLutLib     =  NULL;
     pPars->pTimesArr   =  NULL; 
     pPars->pTimesArr   =  NULL;   
     pPars->pFuncCost   =  NULL;   
-
+/*
     if ( pPars->nLutSize == -1 )
     {
         if ( pPars->pLutLib == NULL )
@@ -388,6 +398,7 @@ void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
         // get LUT size from the library
         pPars->nLutSize = pPars->pLutLib->LutMax;
     }
+*/
 }
 
 /**Function*************************************************************
@@ -417,16 +428,18 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
     vNodes = Aig_ManDfsPio( p );
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
-        if ( Aig_ObjIsConst1(pNode) )
-            Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
+        if ( Aig_ObjIsAnd(pNode) )
+            pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan, 
+                If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), 
+                If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
         else if ( Aig_ObjIsPi(pNode) )
             pNode->pData = If_ManCreateCi( pIfMan );
         else if ( Aig_ObjIsPo(pNode) )
             If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
+        else if ( Aig_ObjIsConst1(pNode) )
+            Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
         else // add the node to the mapper
-            pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan, 
-                If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), 
-                If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
+            assert( 0 );
         // set up the choice node
 //        if ( Aig_AigNodeIsChoice( pNode ) )
 //        {
@@ -461,7 +474,7 @@ Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
     Aig_Obj_t * pObj;
     Ntl_Lut_t * pLut;
     int * ppLeaves;
-    int i, k = 0, nLeaves, nWords, nVarsMax;
+    int i, k, nLuts, nLeaves, nWords, nVarsMax;
     // create mapping of If nodes into AIG nodes
     vIfToAig = Vec_IntStart( Aig_ManObjNumMax(p) );
     Vec_IntFill( vIfToAig, Aig_ManObjNumMax(p), -1 );
@@ -469,18 +482,24 @@ Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
     {
         if ( Aig_ObjIsPo(pObj) )
             continue;
+        if ( Aig_ObjIsConst1(pObj) && pObj->pData == NULL )
+            continue;
+        if ( Aig_ObjIsPi(pObj) && pObj->pData == NULL )
+            continue;
         pNode = pObj->pData;
         assert( pNode != NULL );
         Vec_IntWriteEntry( vIfToAig, pNode->Id, pObj->Id );
     }
     // create the mapping
+    If_ManScanMappingDirect( pMan );
     nVarsMax = pMan->pPars->nLutSize;
     nWords   = Aig_TruthWordNum( nVarsMax );
     vIfMap   = pMan->vMapped;
     vMapping = Ntl_MappingAlloc( Vec_PtrSize(vIfMap) + (int)(Aig_ManConst1(p)->nRefs > 0), nVarsMax );
+    nLuts    = 0;
     if ( Aig_ManConst1(p)->nRefs > 0 )
     {
-        pLut = Vec_PtrEntry( vMapping, k++ );
+        pLut = Vec_PtrEntry( vMapping, nLuts++ );
         pLut->Id = 0;
         pLut->nFanins = 0;
         memset( pLut->pTruth, 0xFF, 4 * nWords );
@@ -492,7 +511,7 @@ Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
         nLeaves  = If_CutLeaveNum( pCutBest ); 
         ppLeaves = If_CutLeaves( pCutBest );
         // fill the LUT
-        pLut = Vec_PtrEntry( vMapping, k++ );
+        pLut = Vec_PtrEntry( vMapping, nLuts++ );
         pLut->Id = Vec_IntEntry( vIfToAig, pNode->Id );
         pLut->nFanins = nLeaves;
         If_CutForEachLeaf( pMan, pCutBest, pLeaf, k )
@@ -500,7 +519,7 @@ Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
         // compute the truth table
         memcpy( pLut->pTruth, If_CutTruth(pCutBest), 4 * nWords );
     }
-    assert( k == Vec_PtrSize(vMapping) );
+    assert( nLuts == Vec_PtrSize(vMapping) );
     Vec_IntFree( vIfToAig );
     return vMapping;
 }
@@ -516,13 +535,17 @@ Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Ntk_ManIf( Aig_Man_t * p )
+Vec_Ptr_t * Ntl_MappingIf( Aig_Man_t * p )
 {
     Vec_Ptr_t * vMapping;
     If_Par_t Pars, * pPars = &Pars;
     If_Man_t * pIfMan;
     // perform FPGA mapping
     Ntk_ManSetIfParsDefault( pPars );
+    // set the arrival times
+    pPars->pTimesArr = ALLOC( float, Aig_ManPiNum(p) );
+    memset( pPars->pTimesArr, 0, sizeof(float) * Aig_ManPiNum(p) );
+    // translate into the mapper
     pIfMan = Ntk_ManToIf( p, pPars );    
     if ( pIfMan == NULL )
         return NULL;
diff --git a/src/aig/ntl/ntlTime.c b/src/aig/ntl/ntlTime.c
index d4bd1375..c81686fa 100644
--- a/src/aig/ntl/ntlTime.c
+++ b/src/aig/ntl/ntlTime.c
@@ -76,32 +76,32 @@ float * Ntl_ManCreateDelayTable( Vec_Int_t * vDelays, int nIns, int nOuts )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_TMan_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
+Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
 {
-    Aig_TMan_t * pMan;
+    Tim_Man_t * pMan;
     Vec_Ptr_t * vDelayTables;
     Ntl_Mod_t * pRoot, * pModel;
     Ntl_Obj_t * pObj;
     int i, curPi, curPo, Entry;
     assert( p->pAig != NULL );
     // start the timing manager
-    pMan = Aig_TManStart( Aig_ManPiNum(p->pAig), Aig_ManPoNum(p->pAig) );
+    pMan = Tim_ManStart( Aig_ManPiNum(p->pAig), Aig_ManPoNum(p->pAig) );
     // add arrival time info for the true PIs
     pRoot = Vec_PtrEntry( p->vModels, 0 );
     Ntl_ModelForEachPi( pRoot, pObj, i )
-        Aig_TManInitPiArrival( pMan, i, 0.0 );
+        Tim_ManInitPiArrival( pMan, i, 0.0 );
     // unpack the data in the arrival times
     if ( pRoot->vArrivals )
         Vec_IntForEachEntry( pRoot->vArrivals, Entry, i )
-            Aig_TManInitPiArrival( pMan, Entry, Vec_IntEntry(pRoot->vArrivals,++i) );
+            Tim_ManInitPiArrival( pMan, Entry, Vec_IntEntry(pRoot->vArrivals,++i) );
     // add the required time into for the true POs
     pRoot = Vec_PtrEntry( p->vModels, 0 );
     Ntl_ModelForEachPo( pRoot, pObj, i )
-        Aig_TManInitPoRequired( pMan, i, AIG_INFINITY );
+        Tim_ManInitPoRequired( pMan, i, AIG_INFINITY );
     // unpack the data in the required times
     if ( pRoot->vRequireds )
         Vec_IntForEachEntry( pRoot->vRequireds, Entry, i )
-            Aig_TManInitPoRequired( pMan, Entry, Vec_IntEntry(pRoot->vRequireds,++i) );
+            Tim_ManInitPoRequired( pMan, Entry, Vec_IntEntry(pRoot->vRequireds,++i) );
     // derive timing tables
     vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vModels) );
     Ntl_ManForEachModel( p, pModel, i )
@@ -110,13 +110,13 @@ Aig_TMan_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
             pModel->pDelayTable = Ntl_ManCreateDelayTable( pModel->vDelays, Ntl_ModelPiNum(pModel), Ntl_ModelPoNum(pModel) );
         Vec_PtrPush( vDelayTables, pModel->pDelayTable );
     }
-    Aig_TManSetDelayTables( pMan, vDelayTables );
+    Tim_ManSetDelayTables( pMan, vDelayTables );
     // set up the boxes
     curPi = Ntl_ModelPiNum(pRoot);
     curPo = Ntl_ModelPoNum(pRoot);
     Ntl_ManForEachBox( p, pObj, i )
     {
-        Aig_TManCreateBoxFirst( pMan, curPo, Ntl_ObjFanoutNum(pObj), curPi, Ntl_ObjFaninNum(pObj), pObj->pImplem->pDelayTable );
+        Tim_ManCreateBoxFirst( pMan, curPo, Ntl_ObjFanoutNum(pObj), curPi, Ntl_ObjFaninNum(pObj), pObj->pImplem->pDelayTable );
         curPo += Ntl_ObjFanoutNum(pObj);
         curPi += Ntl_ObjFaninNum(pObj);
     }
diff --git a/src/aig/tim/module.make b/src/aig/tim/module.make
new file mode 100644
index 00000000..81079346
--- /dev/null
+++ b/src/aig/tim/module.make
@@ -0,0 +1 @@
+SRC +=    src/aig/tim/tim.c
diff --git a/src/aig/aig/aigTime.c b/src/aig/tim/tim.c
index 1544a15b..364f7d20 100644
--- a/src/aig/aig/aigTime.c
+++ b/src/aig/tim/tim.c
@@ -1,10 +1,10 @@
 /**CFile****************************************************************
 
-  FileName    [aigTime.c]
+  FileName    [tim.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [AIG package.]
+  PackageName [A timing manager.]
 
   Synopsis    [Representation of timing information.]
 
@@ -14,34 +14,47 @@
 
   Date        [Ver. 1.0. Started - April 28, 2007.]
 
-  Revision    [$Id: aigTime.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+  Revision    [$Id: tim.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
-#include "aig.h"
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+
+#include "vec.h"
+#include "mem.h"
+#include "tim.h"
+
+#define AIG_MIN(a,b)       (((a) < (b))? (a) : (b))
+#define AIG_MAX(a,b)       (((a) > (b))? (a) : (b))
+#define AIG_ABS(a)         (((a) >= 0)?  (a) :-(a))
+#define AIG_INFINITY       (100000000)
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Aig_TBox_t_           Aig_TBox_t;
-typedef struct Aig_TObj_t_           Aig_TObj_t;
+typedef struct Tim_Box_t_           Tim_Box_t;
+typedef struct Tim_Obj_t_           Tim_Obj_t;
 
 // timing manager
-struct Aig_TMan_t_
+struct Tim_Man_t_
 {
     Vec_Ptr_t *      vBoxes;         // the timing boxes
     Vec_Ptr_t *      vDelayTables;   // pointers to the delay tables
-    Aig_MmFlex_t *   pMemObj;        // memory manager for boxes
+    Mem_Flex_t *   pMemObj;        // memory manager for boxes
     int              nTravIds;       // traversal ID of the manager
     int              nPis;           // the number of PIs
     int              nPos;           // the number of POs
-    Aig_TObj_t *     pPis;           // timing info for the PIs
-    Aig_TObj_t *     pPos;           // timing info for the POs
+    Tim_Obj_t *      pPis;           // timing info for the PIs
+    Tim_Obj_t *      pPos;           // timing info for the POs
 };
 
 // timing box
-struct Aig_TBox_t_
+struct Tim_Box_t_
 {
     int              iBox;           // the unique ID of this box
     int              TravId;         // traversal ID of this box
@@ -52,7 +65,7 @@ struct Aig_TBox_t_
 };
 
 // timing object
-struct Aig_TObj_t_
+struct Tim_Obj_t_
 {
     int              TravId;         // traversal ID of this object
     int              iObj2Box;       // mapping of the object into its box
@@ -76,21 +89,21 @@ struct Aig_TObj_t_
   SeeAlso     []
 
 ***********************************************************************/
-Aig_TMan_t * Aig_TManStart( int nPis, int nPos )
+Tim_Man_t * Tim_ManStart( int nPis, int nPos )
 {
-    Aig_TMan_t * p;
+    Tim_Man_t * p;
     int i;
-    p = ALLOC( Aig_TMan_t, 1 );
-    memset( p, 0, sizeof(Aig_TMan_t) );
-    p->pMemObj = Aig_MmFlexStart();
+    p = ALLOC( Tim_Man_t, 1 );
+    memset( p, 0, sizeof(Tim_Man_t) );
+    p->pMemObj = Mem_FlexStart();
     p->vBoxes  = Vec_PtrAlloc( 100 );
     Vec_PtrPush( p->vBoxes, NULL );
     p->nPis = nPis;
     p->nPos = nPos;
-    p->pPis = ALLOC( Aig_TObj_t, nPis );
-    memset( p->pPis, 0, sizeof(Aig_TObj_t) * nPis );
-    p->pPos = ALLOC( Aig_TObj_t, nPos );
-    memset( p->pPos, 0, sizeof(Aig_TObj_t) * nPos );
+    p->pPis = ALLOC( Tim_Obj_t, nPis );
+    memset( p->pPis, 0, sizeof(Tim_Obj_t) * nPis );
+    p->pPos = ALLOC( Tim_Obj_t, nPos );
+    memset( p->pPos, 0, sizeof(Tim_Obj_t) * nPos );
     for ( i = 0; i < nPis; i++ )
         p->pPis[i].iObj2Box = p->pPis[i].iObj2Num = -1;
     for ( i = 0; i < nPos; i++ )
@@ -109,7 +122,7 @@ Aig_TMan_t * Aig_TManStart( int nPis, int nPos )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManStop( Aig_TMan_t * p )
+void Tim_ManStop( Tim_Man_t * p )
 {
     float * pTable;
     int i;
@@ -120,7 +133,7 @@ void Aig_TManStop( Aig_TMan_t * p )
         Vec_PtrFree( p->vDelayTables );
     }
     Vec_PtrFree( p->vBoxes );
-    Aig_MmFlexStop( p->pMemObj, 0 );
+    Mem_FlexStop( p->pMemObj, 0 );
     free( p->pPis );
     free( p->pPos );
     free( p );
@@ -137,7 +150,7 @@ void Aig_TManStop( Aig_TMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManSetDelayTables( Aig_TMan_t * p, Vec_Ptr_t * vDelayTables )
+void Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables )
 {
     assert( p->vDelayTables == NULL );
     p->vDelayTables = vDelayTables;
@@ -154,12 +167,12 @@ void Aig_TManSetDelayTables( Aig_TMan_t * p, Vec_Ptr_t * vDelayTables )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManCreateBox( Aig_TMan_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable )
+void Tim_ManCreateBox( Tim_Man_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable )
 {
-    Aig_TBox_t * pBox;
+    Tim_Box_t * pBox;
     int i;
-    pBox = (Aig_TBox_t *)Aig_MmFlexEntryFetch( p->pMemObj, sizeof(Aig_TBox_t) + sizeof(int) * (nIns+nOuts) );
-    memset( pBox, 0, sizeof(Aig_TBox_t) );
+    pBox = (Tim_Box_t *)Mem_FlexEntryFetch( p->pMemObj, sizeof(Tim_Box_t) + sizeof(int) * (nIns+nOuts) );
+    memset( pBox, 0, sizeof(Tim_Box_t) );
     pBox->iBox = Vec_PtrSize( p->vBoxes );
     Vec_PtrPush( p->vBoxes, pBox );
     pBox->pDelayTable = pDelayTable;
@@ -192,12 +205,12 @@ void Aig_TManCreateBox( Aig_TMan_t * p, int * pIns, int nIns, int * pOuts, int n
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManCreateBoxFirst( Aig_TMan_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable )
+void Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable )
 {
-    Aig_TBox_t * pBox;
+    Tim_Box_t * pBox;
     int i;
-    pBox = (Aig_TBox_t *)Aig_MmFlexEntryFetch( p->pMemObj, sizeof(Aig_TBox_t) + sizeof(int) * (nIns+nOuts) );
-    memset( pBox, 0, sizeof(Aig_TBox_t) );
+    pBox = (Tim_Box_t *)Mem_FlexEntryFetch( p->pMemObj, sizeof(Tim_Box_t) + sizeof(int) * (nIns+nOuts) );
+    memset( pBox, 0, sizeof(Tim_Box_t) );
     pBox->iBox = Vec_PtrSize( p->vBoxes );
     Vec_PtrPush( p->vBoxes, pBox );
     pBox->pDelayTable = pDelayTable;
@@ -232,7 +245,7 @@ void Aig_TManCreateBoxFirst( Aig_TMan_t * p, int firstIn, int nIns, int firstOut
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManIncrementTravId( Aig_TMan_t * p )
+void Tim_ManIncrementTravId( Tim_Man_t * p )
 {
     p->nTravIds++;
 }
@@ -248,7 +261,7 @@ void Aig_TManIncrementTravId( Aig_TMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManInitPiArrival( Aig_TMan_t * p, int iPi, float Delay )
+void Tim_ManInitPiArrival( Tim_Man_t * p, int iPi, float Delay )
 {
     assert( iPi < p->nPis );
     p->pPis[iPi].timeArr = Delay;
@@ -265,7 +278,7 @@ void Aig_TManInitPiArrival( Aig_TMan_t * p, int iPi, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManInitPoRequired( Aig_TMan_t * p, int iPo, float Delay )
+void Tim_ManInitPoRequired( Tim_Man_t * p, int iPo, float Delay )
 {
     assert( iPo < p->nPos );
     p->pPos[iPo].timeArr = Delay;
@@ -282,7 +295,7 @@ void Aig_TManInitPoRequired( Aig_TMan_t * p, int iPo, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManSetPoArrival( Aig_TMan_t * p, int iPo, float Delay )
+void Tim_ManSetPoArrival( Tim_Man_t * p, int iPo, float Delay )
 {
     assert( iPo < p->nPos );
     assert( p->pPos[iPo].TravId != p->nTravIds );
@@ -301,10 +314,10 @@ void Aig_TManSetPoArrival( Aig_TMan_t * p, int iPo, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-float Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi )
+float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
 {
-    Aig_TBox_t * pBox;
-    Aig_TObj_t * pObj;
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj;
     float * pDelays;
     float DelayMax;
     int i, k;
@@ -325,7 +338,7 @@ float Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi )
     {
         pObj = p->pPos + pBox->Inouts[i];
         if ( pObj->TravId != p->nTravIds )
-            printf( "Aig_TManGetPiArrival(): PO arrival times of the box are not up to date!\n" );
+            printf( "Tim_ManGetPiArrival(): PO arrival times of the box are not up to date!\n" );
     }
     // compute the required times for each output of the box (PIs)
     for ( i = 0; i < pBox->nOutputs; i++ )
@@ -355,7 +368,7 @@ float Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManSetPiRequired( Aig_TMan_t * p, int iPi, float Delay )
+void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay )
 {
     assert( iPi < p->nPis );
     assert( p->pPis[iPi].TravId != p->nTravIds );
@@ -374,7 +387,7 @@ void Aig_TManSetPiRequired( Aig_TMan_t * p, int iPi, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-float Aig_TManGetPoRequired( Aig_TMan_t * p, int iPo )
+float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo )
 {
     return 0.0;
 }
diff --git a/src/aig/tim/tim.h b/src/aig/tim/tim.h
new file mode 100644
index 00000000..8b11ca02
--- /dev/null
+++ b/src/aig/tim/tim.h
@@ -0,0 +1,82 @@
+/**CFile****************************************************************
+
+  FileName    [tim.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [A timing manager.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: tim.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __TIM_H__
+#define __TIM_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Tim_Man_t_           Tim_Man_t;
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                             ITERATORS                            ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     SEQUENTIAL ITERATORS                         ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== time.c ===========================================================*/
+extern Tim_Man_t *     Tim_ManStart( int nPis, int nPos );
+extern void            Tim_ManStop( Tim_Man_t * p );
+extern void            Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables );
+extern void            Tim_ManCreateBox( Tim_Man_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable );
+extern void            Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable );
+extern void            Tim_ManIncrementTravId( Tim_Man_t * p );
+extern void            Tim_ManInitPiArrival( Tim_Man_t * p, int iPi, float Delay );
+extern void            Tim_ManInitPoRequired( Tim_Man_t * p, int iPo, float Delay );
+extern void            Tim_ManSetPoArrival( Tim_Man_t * p, int iPo, float Delay );
+extern void            Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay );
+extern float           Tim_ManGetPiArrival( Tim_Man_t * p, int iPi );
+extern float           Tim_ManGetPoRequired( Tim_Man_t * p, int iPo );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 29b1ea14..439c3383 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1507,13 +1507,12 @@ void Abc_NtkDarTestBlif( char * pFileName )
         return;
     }
     Ntl_ManPrintStats( p );
-/*
-    if ( !Ntl_ManInsertTest( p ) )
+//    if ( !Ntl_ManInsertTest( p ) )
+    if ( !Ntl_ManInsertTestIf( p ) )
     {
         printf( "Abc_NtkDarTestBlif(): Tranformation of the netlist has failed.\n" );
         return;
     }
-*/
 //    sprintf( Buffer, "%s_.blif", p->pName );
     sprintf( Buffer, "test_.blif", p->pName );
     Ioa_WriteBlif( p, Buffer );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 1b82f9a0..17040742 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -381,6 +381,7 @@ extern void            If_ManCleanMarkV( If_Man_t * p );
 extern float           If_ManDelayMax( If_Man_t * p, int fSeq );
 extern void            If_ManComputeRequired( If_Man_t * p );
 extern float           If_ManScanMapping( If_Man_t * p );
+extern float           If_ManScanMappingDirect( If_Man_t * p );
 extern float           If_ManScanMappingSeq( If_Man_t * p );
 extern void            If_ManResetOriginalRefs( If_Man_t * p );
 extern int             If_ManCrossCut( If_Man_t * p );
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index f3fa049e..f4fcf94a 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -290,6 +290,48 @@ float If_ManScanMapping( If_Man_t * p )
 
   Synopsis    [Computes area, references, and nodes used in the mapping.]
 
+  Description [Collects the nodes in reverse topological order in array 
+  p->vMapping.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_ManScanMappingDirect( If_Man_t * p )
+{
+    If_Obj_t * pObj, ** ppStore;
+    float aArea;
+    int i;
+    assert( !p->pPars->fLiftLeaves );
+    // clean all references
+    If_ManForEachObj( p, pObj, i )
+    {
+        pObj->Required = IF_FLOAT_LARGE;
+        pObj->nVisits  = pObj->nVisitsCopy;
+        pObj->nRefs    = 0;
+    }
+    // allocate place to store the nodes
+    ppStore = ALLOC( If_Obj_t *, p->nLevelMax + 1 );
+    memset( ppStore, 0, sizeof(If_Obj_t *) * (p->nLevelMax + 1) );
+    // collect nodes reachable from POs in the DFS order through the best cuts
+    aArea = 0;
+    If_ManForEachCo( p, pObj, i )
+        aArea += If_ManScanMapping_rec( p, If_ObjFanin0(pObj), ppStore );
+    // reconnect the nodes in reverse topological order
+    Vec_PtrClear( p->vMapped );
+//    for ( i = p->nLevelMax; i >= 0; i-- )
+    for ( i = 0; i <= p->nLevelMax; i++ )
+        for ( pObj = ppStore[i]; pObj; pObj = pObj->pCopy )
+            Vec_PtrPush( p->vMapped, pObj );
+    free( ppStore );
+    return aArea;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area, references, and nodes used in the mapping.]
+
   Description []
                
   SideEffects []
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/pcm/module.make
+++ /dev/null
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/ply/module.make
+++ /dev/null