Version abc61209

29 files changed, 931 insertions, 305 deletions

diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 12bb8341..3ee39955 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -218,9 +218,9 @@ int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
-        if ( Abc_NodeIsConst(pNode) )
+        if ( Abc_ObjFaninNum(pNode) < 2 )
             continue;
-        nNodes += pNode->pData? Cudd_DagSize( pNode->pData ) : 0;
+        nNodes += pNode->pData? -1 + Cudd_DagSize( pNode->pData ) : 0;
     }
     return nNodes;
 }
@@ -244,7 +244,7 @@ int Abc_NtkGetAigNodeNum( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
-        if ( Abc_NodeIsConst(pNode) )
+        if ( Abc_ObjFaninNum(pNode) < 2 )
             continue;
         nNodes += pNode->pData? Hop_DagSize( pNode->pData ) : 0;
     }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 901e1df4..115e9bb8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2034,24 +2034,26 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int nFaninMax, nCubeMax, c;
+    int nLutSize, nCutsMax, c;
+    int fArea;
     int fUseBdds;
     int fUseSops;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fUseBdds, int fUseSops, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nLutSize, int nCutsMax, int fArea, int fUseBdds, int fUseSops, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFaninMax =  5;
-    nCubeMax  =  5;
+    nLutSize  =  8;
+    nCutsMax  =  5;
+    fArea     =  0;
     fUseBdds  =  0;
     fUseSops  =  0;
     fVerbose  =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCbsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCabsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2061,9 +2063,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nFaninMax = atoi(argv[globalUtilOptind]);
+            nLutSize = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFaninMax < 0 ) 
+            if ( nLutSize < 0 ) 
                 goto usage;
             break;
         case 'C':
@@ -2072,11 +2074,14 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nCubeMax = atoi(argv[globalUtilOptind]);
+            nCutsMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nCubeMax < 0 ) 
+            if ( nCutsMax < 0 ) 
                 goto usage;
             break;
+        case 'a':
+            fArea ^= 1;
+            break;
         case 'b':
             fUseBdds ^= 1;
             break;
@@ -2096,7 +2101,19 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( fUseBdds && fUseSops )
     {
         fprintf( pErr, "Cannot optimize both BDDs and SOPs at the same time.\n" );
-        goto usage;
+        return 1;
+    }
+
+    if ( nLutSize < 3 || nLutSize > IF_MAX_FUNC_LUTSIZE )
+    {
+        fprintf( pErr, "Incorrect LUT size (%d).\n", nLutSize );
+        return 1;
+    }
+
+    if ( nCutsMax < 2 || nCutsMax >= (1<<12) )
+    {
+        fprintf( pErr, "Incorrect number of cuts.\n" );
+        return 1;
     }
 
     if ( pNtk == NULL )
@@ -2111,7 +2128,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkRenode( pNtk, nFaninMax, nCubeMax, fUseBdds, fUseSops, fVerbose );
+    pNtkRes = Abc_NtkRenode( pNtk, nLutSize, nCutsMax, fArea, fUseBdds, fUseSops, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Renoding has failed.\n" );
@@ -2122,13 +2139,14 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: renode [-K num] [-C num] [-bsv]\n" );
+    fprintf( pErr, "usage: renode [-K num] [-C num] [-sbav]\n" );
     fprintf( pErr, "\t          transforms the AIG into a logic network with larger nodes\n" );
     fprintf( pErr, "\t          while minimizing the number of FF literals of the node SOPs\n" );
-    fprintf( pErr, "\t-K num  : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
-    fprintf( pErr, "\t-C num  : the maximum number of cubes used at a node [default = %d]\n", nCubeMax );
-    fprintf( pErr, "\t-b      : toggles minimizing the number of BDD nodes [default = %s]\n", fUseBdds? "yes": "no" );
-    fprintf( pErr, "\t-s      : toggles minimizing the number of SOP cubes [default = %s]\n", fUseSops? "yes": "no" );
+    fprintf( pErr, "\t-K num  : the max cut size for renoding (2 < num < %d) [default = %d]\n", IF_MAX_FUNC_LUTSIZE+1, nLutSize );
+    fprintf( pErr, "\t-C num  : the max number of cuts used at a node (1 < num < 2^12) [default = %d]\n", nCutsMax );
+    fprintf( pErr, "\t-s      : toggles minimizing SOP cubes instead of FF lits [default = %s]\n", fUseSops? "yes": "no" );
+    fprintf( pErr, "\t-b      : toggles minimizing BDD nodes instead of FF lits [default = %s]\n", fUseBdds? "yes": "no" );
+    fprintf( pErr, "\t-a      : toggles area-oriented mapping [default = %s]\n", fArea? "yes": "no" );
     fprintf( pErr, "\t-v      : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
     fprintf( pErr, "\t-h      : print the command usage\n");
     return 1;
@@ -2731,18 +2749,18 @@ int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
-    int nCutMax;
+    int nCutsMax;
     bool fUpdateLevel;
     bool fUseZeros;
     bool fVerbose;
-    extern int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose );
+    extern int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutsMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nCutMax      =  5;
+    nCutsMax      =  5;
     fUpdateLevel =  0;
     fUseZeros    =  0;
     fVerbose     =  0;
@@ -2757,9 +2775,9 @@ int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nCutMax = atoi(argv[globalUtilOptind]);
+            nCutsMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nCutMax < 0 ) 
+            if ( nCutsMax < 0 ) 
                 goto usage;
             break;
         case 'l':
@@ -2783,7 +2801,7 @@ int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( nCutMax < 4 || nCutMax > CUT_SIZE_MAX )
+    if ( nCutsMax < 4 || nCutsMax > CUT_SIZE_MAX )
     {
         fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", 4, CUT_SIZE_MAX );
         return 1;
@@ -2800,7 +2818,7 @@ int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    if ( !Abc_NtkRestructure( pNtk, nCutMax, fUpdateLevel, fUseZeros, fVerbose ) )
+    if ( !Abc_NtkRestructure( pNtk, nCutsMax, fUpdateLevel, fUseZeros, fVerbose ) )
     {
         fprintf( pErr, "Refactoring has failed.\n" );
         return 1;
@@ -2810,7 +2828,7 @@ int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: restructure [-K num] [-lzvh]\n" );
     fprintf( pErr, "\t         performs technology-independent restructuring of the AIG\n" );
-    fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n",   CUT_SIZE_MIN, CUT_SIZE_MAX, nCutMax );  
+    fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n",   CUT_SIZE_MIN, CUT_SIZE_MAX, nCutsMax );  
     fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
     fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
@@ -2836,19 +2854,19 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
     int RS_CUT_MIN =  4;
     int RS_CUT_MAX = 16;
     int c;
-    int nCutMax;
+    int nCutsMax;
     int nNodesMax;
     bool fUpdateLevel;
     bool fUseZeros;
     bool fVerbose;
-    extern int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nNodesMax, bool fUpdateLevel, bool fVerbose );
+    extern int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutsMax, int nNodesMax, bool fUpdateLevel, bool fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nCutMax      =  8;
+    nCutsMax      =  8;
     nNodesMax    =  1;
     fUpdateLevel =  1;
     fUseZeros    =  0;
@@ -2864,9 +2882,9 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nCutMax = atoi(argv[globalUtilOptind]);
+            nCutsMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nCutMax < 0 ) 
+            if ( nCutsMax < 0 ) 
                 goto usage;
             break;
         case 'N':
@@ -2901,7 +2919,7 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( nCutMax < RS_CUT_MIN || nCutMax > RS_CUT_MAX )
+    if ( nCutsMax < RS_CUT_MIN || nCutsMax > RS_CUT_MAX )
     {
         fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", RS_CUT_MIN, RS_CUT_MAX );
         return 1;
@@ -2918,7 +2936,7 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    if ( !Abc_NtkResubstitute( pNtk, nCutMax, nNodesMax, fUpdateLevel, fVerbose ) )
+    if ( !Abc_NtkResubstitute( pNtk, nCutsMax, nNodesMax, fUpdateLevel, fVerbose ) )
     {
         fprintf( pErr, "Refactoring has failed.\n" );
         return 1;
@@ -2928,7 +2946,7 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: resub [-K num] [-N num] [-lzvh]\n" );
     fprintf( pErr, "\t         performs technology-independent restructuring of the AIG\n" );
-    fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n", RS_CUT_MIN, RS_CUT_MAX, nCutMax );  
+    fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n", RS_CUT_MIN, RS_CUT_MAX, nCutsMax );  
     fprintf( pErr, "\t-N num : the max number of nodes to add [default = %d]\n", nNodesMax );  
     fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
     fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
@@ -7510,9 +7528,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     memset( pPars, 0, sizeof(If_Par_t) );
     // user-controlable paramters
-    pPars->Mode        =  0;
     pPars->nLutSize    =  4;
-    pPars->nCutsMax    = 20;
+    pPars->nCutsMax    = 10;
     pPars->DelayTarget = -1;
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
@@ -7522,7 +7539,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->fSeq        =  0;
     pPars->fVerbose    =  0;
     // internal parameters
-    pPars->fTruth      =  1;
+    pPars->fTruth      =  0;
     pPars->nLatches    =  pNtk? Abc_NtkLatchNum(pNtk) : 0;
     pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
     pPars->pTimesArr   =  NULL; 
@@ -7530,21 +7547,10 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->pFuncCost   =  NULL;   
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MKCDpaflrsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCDpaflrsvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'M':
-            if ( globalUtilOptind >= argc )
-            {
-                fprintf( pErr, "Command line switch \"-M\" should be followed by a positive integer.\n" );
-                goto usage;
-            }
-            pPars->Mode = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->Mode < 0 ) 
-                goto usage;
-            break;
         case 'K':
             if ( globalUtilOptind >= argc )
             {
@@ -7614,19 +7620,33 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pPars->fSeq )
     {
         fprintf( pErr, "Sequential mapping is currently being implemented.\n" );
-        goto usage;
+        return 1;
     }
 
-    if ( pPars->Mode < 0 || pPars->Mode > 4 )
+    if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE )
     {
-        fprintf( pErr, "Incorrect mapping mode.\n" );
-        goto usage;
+        fprintf( pErr, "Incorrect LUT size (%d).\n", pPars->nLutSize );
+        return 1;
     }
 
     if ( pPars->nCutsMax < 2 || pPars->nCutsMax >= (1<<12) )
     {
         fprintf( pErr, "Incorrect number of cuts.\n" );
-        goto usage;
+        return 1;
+    }
+
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+    {
+        printf( "Performing FPGA mapping with choices.\n" );
+//        printf( "Currently mapping with choices is not enabled.\n" );
+        pPars->fTruth = 1;
+//        return 1;
+    }
+
+    if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE )
+    {
+        fprintf( pErr, "Mapping with choices requires computing truth tables. In this case, the LUT size cannot be more than %d.\n", IF_MAX_FUNC_LUTSIZE );
+        return 1;
     }
 
     // set the latch paths
@@ -7686,21 +7706,16 @@ usage:
         sprintf( LutSize, "library" );
     else
         sprintf( LutSize, "%d", pPars->nLutSize );
-    fprintf( pErr, "usage: if [-M num] [-K num] [-C num] [-D float] [-pafrsvh]\n" );
-    fprintf( pErr, "\t           performs FPGA mapping of the network as follows:\n" );
-    fprintf( pErr, "\t               1 - delay only\n" );
-    fprintf( pErr, "\t               2 - area only\n" );
-    fprintf( pErr, "\t               3 - area under delay constraints\n" );
-    fprintf( pErr, "\t               4 - area under delay constraints with area recovery\n" );
-    fprintf( pErr, "\t-M num   : the mapping mode [default = %d]\n", pPars->Mode );
-    fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < 32) [default = %s]\n", LutSize );
+    fprintf( pErr, "usage: if [-K num] [-C num] [-D float] [-pafrsvh]\n" );
+    fprintf( pErr, "\t           performs FPGA technology mapping of the network\n" );
+    fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     fprintf( pErr, "\t-C num   : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
     fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );  
     fprintf( pErr, "\t-p       : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
     fprintf( pErr, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
     fprintf( pErr, "\t-f       : toggles one fancy feature [default = %s]\n", pPars->fFancy? "yes": "no" );
-//    fprintf( pErr, "\t-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
     fprintf( pErr, "\t-r       : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" );
+    fprintf( pErr, "\t-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
     fprintf( pErr, "\t-s       : toggles sequential mapping [default = %s]\n", pPars->fSeq? "yes": "no" );
     fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : prints the command usage\n");
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 948a1d77..d2129e82 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -28,8 +28,9 @@
 
 static If_Man_t *  Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
 static Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk );
-static Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj );
+static Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
 static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj );
+static Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -53,14 +54,6 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
 
     assert( Abc_NtkIsStrash(pNtk) );
 
-    // print a warning about choice nodes
-    if ( Abc_NtkGetChoiceNum( pNtk ) )
-    {
-//        printf( "Performing FPGA mapping with choices.\n" );
-        printf( "Currently mapping with choices is not enabled.\n" );
-        return NULL;
-    }
-
     // get timing information
     pPars->pTimesArr = Abc_NtkGetCiArrivalFloats(pNtk);
     pPars->pTimesReq = NULL;
@@ -111,9 +104,12 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     ProgressBar * pProgress;
     If_Man_t * pIfMan;
     Abc_Obj_t * pNode, * pFanin, * pPrev;
+    Vec_Ptr_t * vNodes;
     int i;
 
     assert( Abc_NtkIsStrash(pNtk) );
+//    vNodes = Abc_NtkFindGoodOrder( pNtk );
+    vNodes = Abc_AigDfs( pNtk, 0, 0 );
 
     // start the mapping manager and set its parameters
     pIfMan = If_ManStart( pPars );
@@ -125,19 +121,24 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
 
     // load the AIG into the mapper
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
-    Abc_AigForEachAnd( pNtk, pNode, i )
+//    Abc_AigForEachAnd( pNtk, pNode, i )
+    Vec_PtrForEachEntry( vNodes, pNode, i )
     {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Extra_ProgressBarUpdate( pProgress, i, "Initial" );
         // add the node to the mapper
         pNode->pCopy = (Abc_Obj_t *)If_ManCreateAnd( pIfMan, 
             (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode), 
             (If_Obj_t *)Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
         // set up the choice node
         if ( Abc_AigNodeIsChoice( pNode ) )
+        {
             for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
                 If_ObjSetChoice( (If_Obj_t *)pPrev->pCopy, (If_Obj_t *)pFanin->pCopy );
+            If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pCopy );
+        }
     }
     Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodes );
 
     // set the primary outputs without copying the phase
     Abc_NtkForEachCo( pNtk, pNode, i )
@@ -161,6 +162,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pNodeNew;
+    Vec_Int_t * vCover;
     int i, nDupGates;
     // create the new network
     if ( pIfMan->pPars->fUseBdds )
@@ -177,15 +179,17 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     Abc_NtkForEachCi( pNtk, pNode, i )
         If_ObjSetCopy( If_ManPi(pIfMan, i), pNode->pCopy );
     // process the nodes in topological order
+    vCover = Vec_IntAlloc( 1 << 16 );
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
-        pNodeNew = Abc_NodeFromIf_rec( pNtkNew, pIfMan, If_ObjFanin0(If_ManPo(pIfMan, i)) );
+        Extra_ProgressBarUpdate( pProgress, i, "Final" );
+        pNodeNew = Abc_NodeFromIf_rec( pNtkNew, pIfMan, If_ObjFanin0(If_ManPo(pIfMan, i)), vCover );
         pNodeNew = Abc_ObjNotCond( pNodeNew, If_ObjFaninC0(If_ManPo(pIfMan, i)) );
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     }
     Extra_ProgressBarStop( pProgress );
+    Vec_IntFree( vCover );
     // remove the constant node if not used
     pNodeNew = (Abc_Obj_t *)If_ObjCopy( If_ManConst1(pIfMan) );
     if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
@@ -208,7 +212,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj )
+Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover )
 {
     Abc_Obj_t * pNodeNew;
     If_Cut_t * pCutBest;
@@ -224,40 +228,60 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
     pNodeNew = Abc_NtkCreateNode( pNtkNew );
     pCutBest = If_ObjCutBest( pIfObj );
     If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i )
-        Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf) );
+        Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) );
     // derive the function of this node
     if ( pIfMan->pPars->fTruth )
     {
         if ( pIfMan->pPars->fUseBdds )
         { 
             extern void Abc_NodeBddReorder( void * p, Abc_Obj_t * pNode );
-            extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars );
             // transform truth table into the BDD 
-            pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), pCutBest->nLimit );
-            // reorder the fanins to minimize the BDD size
-            Abc_NodeBddReorder( pIfMan->pPars->pReoMan, pNodeNew );
+            pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 0 );  Cudd_Ref(pNodeNew->pData); 
+            if ( pNodeNew->pData == Cudd_ReadLogicZero(pNtkNew->pManFunc) || pNodeNew->pData == Cudd_ReadOne(pNtkNew->pManFunc) )
+            {
+                // replace the node by a constant node
+                pNodeNew = pNodeNew->pData == Cudd_ReadOne(pNtkNew->pManFunc) ? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew);
+            }
+            else
+            {
+                // make sure the node is minimum base
+                Abc_NodeMinimumBase( pNodeNew );
+                // reorder the fanins to minimize the BDD size
+                Abc_NodeBddReorder( pIfMan->pPars->pReoMan, pNodeNew );
+            }
         }
         else if ( pIfMan->pPars->fUseSops ) 
         {
-            Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 );
             // transform truth table into the SOP
-            int RetValue = Kit_TruthIsop( If_CutTruth(pCutBest), pCutBest->nLimit, vCover, 0 );
-            assert( RetValue == 0 );
-            // derive the AIG for that tree
-            pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCutBest->nLimit, vCover );
-            Vec_IntFree( vCover );
+            int RetValue = Kit_TruthIsop( If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover, 1 );
+            assert( RetValue == 0 || RetValue == 1 );
+            // check the case of constant cover
+            if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0) )
+            {
+                assert( RetValue == 0 );
+                pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, If_CutLeaveNum(pCutBest), NULL );
+                pNodeNew = (Vec_IntSize(vCover) == 0) ? Abc_NtkCreateNodeConst0(pNtkNew) : Abc_NtkCreateNodeConst1(pNtkNew);
+            }
+            else
+            {
+                // derive the AIG for that tree
+                pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, If_CutLeaveNum(pCutBest), vCover );
+                if ( RetValue )
+                    Abc_SopComplement( pNodeNew->pData );
+            }
         }
         else 
         {
             extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
-            Vec_Int_t * vMemory = Vec_IntAlloc( 1 << 16 );
             // transform truth table into the decomposition tree
-            Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), pCutBest->nLimit, vMemory );
+            Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover );
             // derive the AIG for the decomposition tree
             pNodeNew->pData = Kit_GraphToHop( pNtkNew->pManFunc, pGraph );
             Kit_GraphFree( pGraph );
-            Vec_IntFree( vMemory );
         }
+        // complement the node if the cut was complemented
+        if ( pCutBest->fCompl )
+            Abc_NodeComplement( pNodeNew );
     }
     else
         pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pIfObj );
@@ -333,6 +357,116 @@ Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t *
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Comparison for two nodes with the flow.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjCompareFlow( Abc_Obj_t ** ppNode0, Abc_Obj_t ** ppNode1 )
+{
+    float Flow0 = Abc_Int2Float((int)(*ppNode0)->pCopy);
+    float Flow1 = Abc_Int2Float((int)(*ppNode1)->pCopy);
+    if ( Flow0 > Flow1 )
+        return -1;
+    if ( Flow0 < Flow1 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Orders AIG nodes so that nodes from larger cones go first.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFindGoodOrder_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    if ( !Abc_ObjIsNode(pNode) )
+        return;
+    assert( Abc_ObjIsNode( pNode ) );
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // visit the transitive fanin of the node
+    Abc_NtkFindGoodOrder_rec( Abc_ObjFanin0(pNode), vNodes );
+    Abc_NtkFindGoodOrder_rec( Abc_ObjFanin1(pNode), vNodes );
+    // add the node after the fanins have been added
+    Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Orders AIG nodes so that nodes from larger cones go first.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes, * vCos;
+    Abc_Obj_t * pNode, * pFanin0, * pFanin1;
+    float Flow0, Flow1;
+    int i;
+
+    // initialize the flow
+    Abc_AigConst1(pNtk)->pCopy = NULL;
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pCopy = NULL;
+    // compute the flow
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        pFanin0 = Abc_ObjFanin0(pNode);
+        pFanin1 = Abc_ObjFanin1(pNode);
+        Flow0 = Abc_Int2Float((int)pFanin0->pCopy)/Abc_ObjFanoutNum(pFanin0);
+        Flow1 = Abc_Int2Float((int)pFanin1->pCopy)/Abc_ObjFanoutNum(pFanin1);
+        pNode->pCopy = (Abc_Obj_t *)Abc_Float2Int(Flow0 + Flow1+(float)1.0);
+    }
+    // find the flow of the COs
+    vCos = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pNode->pCopy = Abc_ObjFanin0(pNode)->pCopy;
+//        pNode->pCopy = (Abc_Obj_t *)Abc_Float2Int((float)Abc_ObjFanin0(pNode)->Level);
+        Vec_PtrPush( vCos, pNode );
+    }
+
+    // sort nodes in the increasing order of the flow
+    qsort( (Abc_Obj_t **)Vec_PtrArray(vCos), Abc_NtkCoNum(pNtk), 
+        sizeof(Abc_Obj_t *), (int (*)(const void *, const void *))Abc_ObjCompareFlow );
+    // verify sorting
+    pFanin0 = Vec_PtrEntry(vCos, 0);
+    pFanin1 = Vec_PtrEntryLast(vCos);
+    assert( Abc_Int2Float((int)pFanin0->pCopy) >= Abc_Int2Float((int)pFanin1->pCopy) );
+
+    // collect the nodes in the topological order from the new array
+    Abc_NtkIncrementTravId( pNtk );
+    vNodes = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( vCos, pNode, i )
+    {
+        Abc_NtkFindGoodOrder_rec( Abc_ObjFanin0(pNode), vNodes );
+//        printf( "%.2f ", Abc_Int2Float((int)pNode->pCopy) );
+    }
+    Vec_PtrFree( vCos );
+    return vNodes;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 4f3003a6..b8aa49a4 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -27,9 +27,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars );
-static int Abc_NtkRenodeEvalSop( unsigned * pTruth, int nVars );
-static int Abc_NtkRenodeEvalAig( unsigned * pTruth, int nVars );
+static int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut );
+static int Abc_NtkRenodeEvalSop( If_Cut_t * pCut );
+static int Abc_NtkRenodeEvalAig( If_Cut_t * pCut );
 
 static reo_man * s_pReo      = NULL;
 static DdManager * s_pDd     = NULL;
@@ -50,7 +50,7 @@ static Vec_Int_t * s_vMemory = NULL;
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fUseBdds, int fUseSops, int fVerbose )
+Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fArea, int fUseBdds, int fUseSops, int fVerbose )
 {
     extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
     If_Par_t Pars, * pPars = &Pars;
@@ -59,19 +59,19 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fU
     // set defaults
     memset( pPars, 0, sizeof(If_Par_t) );
     // user-controlable paramters
-    pPars->Mode        =  0;
     pPars->nLutSize    =  nFaninMax;
-    pPars->nCutsMax    = 10;
+    pPars->nCutsMax    =  nCubeMax;
     pPars->DelayTarget = -1;
     pPars->fPreprocess =  1;
-    pPars->fArea       =  0;
+    pPars->fArea       =  fArea;
     pPars->fFancy      =  0;
     pPars->fExpRed     =  0; //
     pPars->fLatchPaths =  0;
     pPars->fSeq        =  0;
-    pPars->fVerbose    =  0;
+    pPars->fVerbose    =  fVerbose;
     // internal parameters
     pPars->fTruth      =  1;
+    pPars->fUsePerm    =  1; //!fUseSops;
     pPars->nLatches    =  0;
     pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
     pPars->pTimesArr   =  NULL; 
@@ -130,18 +130,22 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fU
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars )
+int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut )
 {
+    int pOrder[IF_MAX_LUTSIZE];
     DdNode * bFunc, * bFuncNew;
-    int nNodes, nSupport;
-    bFunc = Kit_TruthToBdd( s_pDd, pTruth, nVars );           Cudd_Ref( bFunc );
-    bFuncNew = Extra_Reorder( s_pReo, s_pDd, bFunc, NULL );   Cudd_Ref( bFuncNew );
-//    nSupport = Cudd_SupportSize( s_pDd, bFuncNew );
-    nSupport = 1;
-    nNodes = Cudd_DagSize( bFuncNew );
+    int i, k, nNodes;
+    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+        pCut->pPerm[i] = pOrder[i] = -100;
+    bFunc = Kit_TruthToBdd( s_pDd, If_CutTruth(pCut), If_CutLeaveNum(pCut), 0 );  Cudd_Ref( bFunc );
+    bFuncNew = Extra_Reorder( s_pReo, s_pDd, bFunc, pOrder );                     Cudd_Ref( bFuncNew );
+    for ( i = k = 0; i < If_CutLeaveNum(pCut); i++ )
+        if ( pOrder[i] >= 0 )
+            pCut->pPerm[pOrder[i]] = ++k; // double-check this!
+    nNodes = -1 + Cudd_DagSize( bFuncNew );
     Cudd_RecursiveDeref( s_pDd, bFuncNew );
     Cudd_RecursiveDeref( s_pDd, bFunc );
-    return (nSupport << 16) | nNodes;
+    return nNodes; 
 }
 
 /**Function*************************************************************
@@ -155,13 +159,16 @@ int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRenodeEvalSop( unsigned * pTruth, int nVars )
+int Abc_NtkRenodeEvalSop( If_Cut_t * pCut )
 {
-    int nCubes, RetValue;
-    RetValue = Kit_TruthIsop( pTruth, nVars, s_vMemory, 0 );
-    assert( RetValue == 0 );
-    nCubes = Vec_IntSize( s_vMemory );
-    return (1 << 16) | nCubes;
+    int i, RetValue;
+    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+        pCut->pPerm[i] = 1;
+    RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 1 );
+    if ( RetValue == -1 )
+        return ABC_INFINITY;
+    assert( RetValue == 0 || RetValue == 1 );
+    return Vec_IntSize( s_vMemory );
 }
 
 /**Function*************************************************************
@@ -175,16 +182,22 @@ int Abc_NtkRenodeEvalSop( unsigned * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRenodeEvalAig( unsigned * pTruth, int nVars )
+int Abc_NtkRenodeEvalAig( If_Cut_t * pCut )
 {
     Kit_Graph_t * pGraph;
-    int nNodes, nDepth;
-    pGraph = Kit_TruthToGraph( pTruth, nVars, s_vMemory );
+    int i, nNodes;
+    pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory );
+    if ( pGraph == NULL )
+    {
+        for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+            pCut->pPerm[i] = 100;
+        return ABC_INFINITY;
+    }
     nNodes = Kit_GraphNodeNum( pGraph );
-//    nDepth = Kit_GraphLevelNum( pGraph );
-    nDepth = 1;
+    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+        pCut->pPerm[i] = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeLast(pGraph), Kit_GraphNode(pGraph, i) );
     Kit_GraphFree( pGraph );
-    return (nDepth << 16) | nNodes;
+    return nNodes;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/fpga/fpga.c b/src/map/fpga/fpga.c
index d04c9910..40423f4f 100644
--- a/src/map/fpga/fpga.c
+++ b/src/map/fpga/fpga.c
@@ -56,10 +56,10 @@ static int Fpga_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
 void Fpga_Init( Abc_Frame_t * pAbc )
 {
     // set the default library
-    //Fpga_LutLib_t s_LutLib = { "lutlib", 6, {0,1,2,4,8,16,32}, {0,1,2,3,4,5,6} };
-//    Fpga_LutLib_t s_LutLib = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} };
-    Fpga_LutLib_t s_LutLib = { "lutlib", 4, {0,1,1,1,1}, {0,1,1,1,1} };
-    //Fpga_LutLib_t s_LutLib = { "lutlib", 3, {0,1,1,1}, {0,1,1,1} };
+    //Fpga_LutLib_t s_LutLib = { "lutlib", 6, 0, {0,1,2,4,8,16,32}, {{0},{1},{2},{3},{4},{5},{6}} };
+//    Fpga_LutLib_t s_LutLib = { "lutlib", 5, 0, {0,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1}} };
+    Fpga_LutLib_t s_LutLib = { "lutlib", 4, 0, {0,1,1,1,1}, {{0},{1},{1},{1},{1}} };
+    //Fpga_LutLib_t s_LutLib = { "lutlib", 3, 0, {0,1,1,1}, {{0},{1},{1},{1}} };
 
     Abc_FrameSetLibLut( Fpga_LutLibDup(&s_LutLib) );
 
@@ -248,14 +248,14 @@ usage:
 ***********************************************************************/
 void Fpga_SetSimpleLutLib( int nLutSize )
 {
-    Fpga_LutLib_t s_LutLib10= { "lutlib",10, {0,1,1,1,1,1,1,1,1,1,1}, {0,1,1,1,1,1,1,1,1,1,1} };
-    Fpga_LutLib_t s_LutLib9 = { "lutlib", 9, {0,1,1,1,1,1,1,1,1,1}, {0,1,1,1,1,1,1,1,1,1} };
-    Fpga_LutLib_t s_LutLib8 = { "lutlib", 8, {0,1,1,1,1,1,1,1,1}, {0,1,1,1,1,1,1,1,1} };
-    Fpga_LutLib_t s_LutLib7 = { "lutlib", 7, {0,1,1,1,1,1,1,1}, {0,1,1,1,1,1,1,1} };
-    Fpga_LutLib_t s_LutLib6 = { "lutlib", 6, {0,1,1,1,1,1,1}, {0,1,1,1,1,1,1} };
-    Fpga_LutLib_t s_LutLib5 = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} };
-    Fpga_LutLib_t s_LutLib4 = { "lutlib", 4, {0,1,1,1,1}, {0,1,1,1,1} };
-    Fpga_LutLib_t s_LutLib3 = { "lutlib", 3, {0,1,1,1}, {0,1,1,1} };
+    Fpga_LutLib_t s_LutLib10= { "lutlib",10, 0, {0,1,1,1,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1},{1},{1},{1}} };
+    Fpga_LutLib_t s_LutLib9 = { "lutlib", 9, 0, {0,1,1,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1},{1},{1}} };
+    Fpga_LutLib_t s_LutLib8 = { "lutlib", 8, 0, {0,1,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1},{1}} };
+    Fpga_LutLib_t s_LutLib7 = { "lutlib", 7, 0, {0,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1}} };
+    Fpga_LutLib_t s_LutLib6 = { "lutlib", 6, 0, {0,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1}} };
+    Fpga_LutLib_t s_LutLib5 = { "lutlib", 5, 0, {0,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1}} };
+    Fpga_LutLib_t s_LutLib4 = { "lutlib", 4, 0, {0,1,1,1,1}, {{0},{1},{1},{1},{1}} };
+    Fpga_LutLib_t s_LutLib3 = { "lutlib", 3, 0, {0,1,1,1}, {{0},{1},{1},{1}} };
     Fpga_LutLib_t * pLutLib;
     assert( nLutSize >= 3 && nLutSize <= 10 );
     switch ( nLutSize )
diff --git a/src/map/fpga/fpgaCutUtils.c b/src/map/fpga/fpgaCutUtils.c
index 658ea172..7779be1e 100644
--- a/src/map/fpga/fpgaCutUtils.c
+++ b/src/map/fpga/fpgaCutUtils.c
@@ -290,7 +290,9 @@ void Fpga_CutGetParameters( Fpga_Man_t * pMan, Fpga_Cut_t * pCut )
 //            pCut->aFlow += pFaninCut->aFlow / pCut->ppLeaves[i]->nRefs;
             pCut->aFlow += pFaninCut->aFlow / pCut->ppLeaves[i]->aEstFanouts;
     }
-    pCut->tArrival += pMan->pLutLib->pLutDelays[pCut->nLeaves];
+    // use the first pin to compute the delay of the LUT 
+    // (this mapper does not support the variable pin delay model)
+    pCut->tArrival += pMan->pLutLib->pLutDelays[pCut->nLeaves][0];
 }
 
 
diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h
index 9085baa2..14c2cbdb 100644
--- a/src/map/fpga/fpgaInt.h
+++ b/src/map/fpga/fpgaInt.h
@@ -46,7 +46,7 @@
 #endif
 
 // the maximum number of cut leaves (currently does not work for 7)
-#define FPGA_MAX_LEAVES           10   
+#define FPGA_MAX_LEAVES           6   
 
 // the bit masks
 #define FPGA_MASK(n)             ((~((unsigned)0)) >> (32-(n)))
@@ -171,8 +171,9 @@ struct Fpga_LutLibStruct_t_
 {
     char *              pName;         // the name of the LUT library
     int                 LutMax;        // the maximum LUT size 
+    int                 fVarPinDelays; // set to 1 if variable pin delays are specified
     float               pLutAreas[FPGA_MAX_LUTSIZE+1]; // the areas of LUTs
-    float               pLutDelays[FPGA_MAX_LUTSIZE+1];// the delays of LUTs
+    float               pLutDelays[FPGA_MAX_LUTSIZE+1][FPGA_MAX_LUTSIZE+1];// the delays of LUTs
 };
 
 // the mapping node
diff --git a/src/map/fpga/fpgaLib.c b/src/map/fpga/fpgaLib.c
index 00832bce..8ac66cdc 100644
--- a/src/map/fpga/fpgaLib.c
+++ b/src/map/fpga/fpgaLib.c
@@ -39,9 +39,7 @@
 ***********************************************************************/
 int         Fpga_LutLibReadVarMax( Fpga_LutLib_t * p )               { return p->LutMax;     }
 float *     Fpga_LutLibReadLutAreas( Fpga_LutLib_t * p )             { return p->pLutAreas;  }
-float *     Fpga_LutLibReadLutDelays( Fpga_LutLib_t * p )            { return p->pLutDelays; }
 float       Fpga_LutLibReadLutArea( Fpga_LutLib_t * p, int Size )    { assert( Size <= p->LutMax ); return p->pLutAreas[Size];  }
-float       Fpga_LutLibReadLutDelay( Fpga_LutLib_t * p, int Size )   { assert( Size <= p->LutMax ); return p->pLutDelays[Size]; }
 
 /**Function*************************************************************
 
@@ -59,7 +57,7 @@ Fpga_LutLib_t * Fpga_LutLibCreate( char * FileName, int fVerbose )
     char pBuffer[1000], * pToken;
     Fpga_LutLib_t * p;
     FILE * pFile;
-    int i;
+    int i, k;
 
     pFile = fopen( FileName, "r" );
     if ( pFile == NULL )
@@ -87,16 +85,30 @@ Fpga_LutLib_t * Fpga_LutLibCreate( char * FileName, int fVerbose )
             return NULL;
         }
 
+        // read area
         pToken = strtok( NULL, " \t\n" );
         p->pLutAreas[i] = (float)atof(pToken);
 
-        pToken = strtok( NULL, " \t\n" );
-        p->pLutDelays[i] = (float)atof(pToken);
+        // read delays
+        k = 0;
+        while ( pToken = strtok( NULL, " \t\n" ) )
+            p->pLutDelays[i][k++] = (float)atof(pToken);
+
+        // check for out-of-bound
+        if ( k > i )
+        {
+            printf( "LUT %d has too many pins (%d). Max allowed is %d.\n", i, k, i );
+            return NULL;
+        }
+
+        // check if var delays are specifies
+        if ( k > 1 )
+            p->fVarPinDelays = 1;
 
         if ( i == FPGA_MAX_LUTSIZE )
         {
             printf( "Skipping LUTs of size more than %d.\n", i );
-            break;
+            return NULL;
         }
         i++;
     }
@@ -106,6 +118,32 @@ Fpga_LutLib_t * Fpga_LutLibCreate( char * FileName, int fVerbose )
         p->LutMax = FPGA_MAX_LEAVES;
         printf( "Warning: LUTs with more than %d input will not be used.\n", FPGA_MAX_LEAVES );
     }
+
+    // check the library
+    if ( p->fVarPinDelays )
+    {
+        for ( i = 1; i <= p->LutMax; i++ )
+            for ( k = 0; k < i; k++ )
+            {
+                if ( p->pLutDelays[i][k] <= 0.0 )
+                    printf( "Warning: Pin %d of LUT %d has delay %f. Pin delays should be non-negative numbers. Technology mapping may not work correctly.\n", 
+                        k, i, p->pLutDelays[i][k] );
+                if ( k && p->pLutDelays[i][k-1] > p->pLutDelays[i][k] )
+                    printf( "Warning: Pin %d of LUT %d has delay %f. Pin %d of LUT %d has delay %f. Pin delays should be in non-degreasing order. Technology mapping may not work correctly.\n", 
+                        k-1, i, p->pLutDelays[i][k-1], 
+                        k, i, p->pLutDelays[i][k] );
+            }
+    }
+    else
+    {
+        for ( i = 1; i <= p->LutMax; i++ )
+        {
+            if ( p->pLutDelays[i][0] <= 0.0 )
+                printf( "Warning: LUT %d has delay %f. Pin delays should be non-negative numbers. Technology mapping may not work correctly.\n", 
+                    k, i, p->pLutDelays[i][0] );
+        }
+    }
+
     return p;
 }
 
@@ -162,11 +200,22 @@ void Fpga_LutLibFree( Fpga_LutLib_t * pLutLib )
 ***********************************************************************/
 void Fpga_LutLibPrint( Fpga_LutLib_t * pLutLib )
 {
-    int i;
+    int i, k;
     printf( "# The area/delay of k-variable LUTs:\n" );
     printf( "# k    area     delay\n" );
-    for ( i = 1; i <= pLutLib->LutMax; i++ )
-        printf( "%d   %7.2f   %7.2f\n", i, pLutLib->pLutAreas[i], pLutLib->pLutDelays[i] );
+    if ( pLutLib->fVarPinDelays )
+    {
+        for ( i = 1; i <= pLutLib->LutMax; i++ )
+        {
+            printf( "%d   %7.2f  ", i, pLutLib->pLutAreas[i] );
+            for ( k = 0; k < i; k++ )
+                printf( " %7.2f", pLutLib->pLutDelays[i][k] );
+            printf( "\n" );
+        }
+    }
+    else
+        for ( i = 1; i <= pLutLib->LutMax; i++ )
+            printf( "%d   %7.2f   %7.2f\n", i, pLutLib->pLutAreas[i], pLutLib->pLutDelays[i][0] );
 }
 
 /**Function*************************************************************
@@ -186,7 +235,7 @@ int Fpga_LutLibDelaysAreDiscrete( Fpga_LutLib_t * pLutLib )
     int i;
     for ( i = 1; i <= pLutLib->LutMax; i++ )
     {
-        Delay = pLutLib->pLutDelays[i];
+        Delay = pLutLib->pLutDelays[i][0];
         if ( ((float)((int)Delay)) != Delay )
             return 0;
     }
diff --git a/src/map/fpga/fpgaMatch.c b/src/map/fpga/fpgaMatch.c
index d413a067..9557494c 100644
--- a/src/map/fpga/fpgaMatch.c
+++ b/src/map/fpga/fpgaMatch.c
@@ -323,7 +323,7 @@ clk = clock();
     if ( pNode->nRefs ) 
     {
         pNode->pCutBest->aFlow = Fpga_CutRef( p, pNode, pNode->pCutBest, 0 );
-        assert( pNode->pCutBest->aFlow <= aAreaCutBest );
+//        assert( pNode->pCutBest->aFlow <= aAreaCutBest );
 //        assert( pNode->tRequired < FPGA_FLOAT_LARGE );
     }
     return 1;
diff --git a/src/map/fpga/fpgaTime.c b/src/map/fpga/fpgaTime.c
index 380ff592..879cad4d 100644
--- a/src/map/fpga/fpgaTime.c
+++ b/src/map/fpga/fpgaTime.c
@@ -46,7 +46,7 @@ float Fpga_TimeCutComputeArrival( Fpga_Man_t * pMan, Fpga_Cut_t * pCut )
     for ( i = 0; i < pCut->nLeaves; i++ )
         if ( tArrival < pCut->ppLeaves[i]->pCutBest->tArrival )
             tArrival = pCut->ppLeaves[i]->pCutBest->tArrival;
-    tArrival += pMan->pLutLib->pLutDelays[pCut->nLeaves];
+    tArrival += pMan->pLutLib->pLutDelays[pCut->nLeaves][0];
     return tArrival;
 }
 
@@ -216,7 +216,7 @@ void Fpga_TimePropagateRequired( Fpga_Man_t * p, Fpga_NodeVec_t * vNodes )
         if ( !Fpga_NodeIsAnd(pNode) )
             continue;
         // get the required time for children
-        fRequired = pNode->tRequired - p->pLutLib->pLutDelays[pNode->pCutBest->nLeaves];
+        fRequired = pNode->tRequired - p->pLutLib->pLutDelays[pNode->pCutBest->nLeaves][0];
         // update the required time of the children
         for ( i = 0; i < pNode->pCutBest->nLeaves; i++ )
         {
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 12769eb6..f867e85e 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -40,9 +40,11 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
-
+ 
 // the maximum size of LUTs used for mapping (should be the same as FPGA_MAX_LUTSIZE defined in "fpga.h"!!!)
-#define IF_MAX_LUTSIZE   32
+#define IF_MAX_LUTSIZE       32
+// the largest possible number of LUT inputs when funtionality of the LUTs are computed
+#define IF_MAX_FUNC_LUTSIZE  15
 
 // object types
 typedef enum { 
@@ -71,7 +73,6 @@ typedef struct If_Cut_t_     If_Cut_t;
 struct If_Par_t_
 {
     // user-controlable paramters
-    int                Mode;          // the mapping mode
     int                nLutSize;      // the LUT size
     int                nCutsMax;      // the max number of cuts
     float              DelayTarget;   // delay target
@@ -84,13 +85,14 @@ struct If_Par_t_
     int                fVerbose;      // the verbosity flag
     // internal parameters
     int                fTruth;        // truth table computation enabled
+    int                fUsePerm;      // use permutation (delay info)
     int                fUseBdds;      // sets local BDDs at the nodes
     int                fUseSops;      // sets local SOPs at the nodes
     int                nLatches;      // the number of latches in seq mapping
     If_Lib_t *         pLutLib;       // the LUT library
     float *            pTimesArr;     // arrival times
     float *            pTimesReq;     // required times
-    int(*pFuncCost)(unsigned *, int); // procedure the user's cost of a cut
+    int (* pFuncCost)  (If_Cut_t *);  // procedure to compute the user's cost of a cut
     void *             pReoMan;       // reordering manager
 };
 
@@ -99,8 +101,9 @@ struct If_Lib_t_
 {
     char *             pName;         // the name of the LUT library
     int                LutMax;        // the maximum LUT size 
+    int                fVarPinDelays; // set to 1 if variable pin delays are specified
     float              pLutAreas[IF_MAX_LUTSIZE+1]; // the areas of LUTs
-    float              pLutDelays[IF_MAX_LUTSIZE+1];// the delays of LUTs
+    float              pLutDelays[IF_MAX_LUTSIZE+1][IF_MAX_LUTSIZE+1];// the delays of LUTs
 };
 
 // manager
@@ -123,6 +126,7 @@ struct If_Man_t_
     float              AreaGlo;       // global area
     int                nCutsUsed;     // the number of cuts currently used
     int                nCutsMerged;   // the total number of cuts merged
+    int                nCutsSaved;    // the total number of cuts saved
     int                nCutsMax;      // the maximum number of cuts at a node
     float              Fi;            // the current value of the clock period (for seq mapping)
     unsigned *         puTemp[4];     // used for the truth table computation
@@ -131,6 +135,7 @@ struct If_Man_t_
     int                nEntrySize;    // the size of the entry
     int                nEntryBase;    // the size of the entry minus cut leaf arrays
     int                nTruthSize;    // the size of the truth table if allocated
+    int                nPermSize;     // the size of the permutation array (in words)
     int                nCutSize;      // the size of the cut
     // temporary cut storage
     int                nCuts;         // the number of cuts used
@@ -142,13 +147,15 @@ struct If_Cut_t_
 {
     float              Delay;         // delay of the cut
     float              Area;          // area (or area-flow) of the cut
+    float              AveRefs;       // the average number of leaf references
     unsigned           uSign;         // cut signature
-    unsigned           Cost    : 10;  // the user's cost of the cut
-    unsigned           Depth   :  9;  // the user's depth of the cut
+    unsigned           Cost    : 14;  // the user's cost of the cut
     unsigned           fCompl  :  1;  // the complemented attribute 
-    unsigned           nLimit  :  6;  // the maximum number of leaves
-    unsigned           nLeaves :  6;  // the number of leaves
+    unsigned           fUser   :  1;  // using the user's area and delay
+    unsigned           nLimit  :  8;  // the maximum number of leaves
+    unsigned           nLeaves :  8;  // the number of leaves
     int *              pLeaves;       // array of fanins
+    char *             pPerm;         // permutation
     unsigned *         pTruth;        // the truth table
 };
 
@@ -159,8 +166,9 @@ struct If_Obj_t_
     unsigned           fCompl0 :  1;  // complemented attribute
     unsigned           fCompl1 :  1;  // complemented attribute
     unsigned           fPhase  :  1;  // phase of the node
+    unsigned           fRepr   :  1;  // representative of the equivalence class
     unsigned           fMark   :  1;  // multipurpose mark
-    unsigned           Level   : 24;  // logic level of the node
+    unsigned           Level   : 23;  // logic level of the node
     int                Id;            // integer ID
     int                nRefs;         // the number of references
     int                nCuts;         // the number of cuts
@@ -182,6 +190,7 @@ static inline If_Cut_t * If_ManCut( If_Man_t * p, int i )                    { r
 static inline int        If_ManPiNum( If_Man_t * p )                         { return p->nObjs[IF_PI];               }
 static inline int        If_ManPoNum( If_Man_t * p )                         { return p->nObjs[IF_PO];               }
 static inline int        If_ManAndNum( If_Man_t * p )                        { return p->nObjs[IF_AND];              }
+static inline int        If_ManObjNum( If_Man_t * p )                        { return Vec_PtrSize(p->vObjs);         }
 
 static inline int        If_ObjIsConst1( If_Obj_t * pObj )                   { return pObj->Type == IF_CONST1;       }
 static inline int        If_ObjIsPi( If_Obj_t * pObj )                       { return pObj->Type == IF_PI;           }
@@ -207,11 +216,12 @@ static inline unsigned   If_ObjCutSign( unsigned ObjId )                     { r
 static inline void *     If_CutData( If_Cut_t * pCut )                       { return *(void **)pCut;                }
 static inline void       If_CutSetData( If_Cut_t * pCut, void * pData )      { *(void **)pCut = pData;               }
 
-static inline int        If_CutTruthWords( int nVarsMax )                    { return nVarsMax <= 5 ? 1 : (1 << (nVarsMax - 5)); }
+static inline int        If_CutLeaveNum( If_Cut_t * pCut )                   { return pCut->nLeaves;                             }
 static inline unsigned * If_CutTruth( If_Cut_t * pCut )                      { return pCut->pTruth;                              }
+static inline int        If_CutTruthWords( int nVarsMax )                    { return nVarsMax <= 5 ? 1 : (1 << (nVarsMax - 5)); }
+static inline int        If_CutPermWords( int nVarsMax )                     { return nVarsMax / sizeof(int) + ((nVarsMax % sizeof(int)) > 0); }
 
-static inline float      If_CutLutDelay( If_Man_t * p, If_Cut_t * pCut )     { return pCut->Depth? (float)pCut->Depth : (p->pPars->pLutLib? p->pPars->pLutLib->pLutDelays[pCut->nLeaves] : (float)1.0);  }
-static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { return pCut->Cost?  (float)pCut->Cost  : (p->pPars->pLutLib? p->pPars->pLutLib->pLutAreas[pCut->nLeaves]  : (float)1.0);  }
+static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { return pCut->fUser? (float)pCut->Cost : (p->pPars->pLutLib? p->pPars->pLutLib->pLutAreas[pCut->nLeaves] : (float)1.0); }
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
@@ -233,7 +243,7 @@ static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { r
     Vec_PtrForEachEntry( p->vPos, pObj, i )
 // iterator over the latches 
 #define If_ManForEachLatch( p, pObj, i )                                       \
-    Vec_PtrForEachEntryStart( p->vPos, pObj, i, p->pPars->nLatches )
+    Vec_PtrForEachEntryStart( p->vPos, pObj, i, If_ManPoNum(p) - p->pPars->nLatches )
 // iterator over all objects, including those currently not used
 #define If_ManForEachObj( p, pObj, i )                                         \
     Vec_PtrForEachEntry( p->vObjs, pObj, i )
@@ -256,27 +266,32 @@ static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { r
 
 /*=== ifCore.c ==========================================================*/
 extern int             If_ManPerformMapping( If_Man_t * p );
-extern int             If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequired );
 /*=== ifCut.c ==========================================================*/
 extern float           If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels );
 extern float           If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels );
 extern float           If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels );
 extern float           If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels );
 extern void            If_CutPrint( If_Man_t * p, If_Cut_t * pCut );
-extern float           If_CutDelay( If_Man_t * p, If_Cut_t * pCut );
+extern void            If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutFlow( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutAverageRefs( If_Man_t * p, If_Cut_t * pCut );
 extern int             If_CutFilter( If_Man_t * p, If_Cut_t * pCut );
 extern int             If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut );
 extern void            If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
 extern void            If_ManSortCuts( If_Man_t * p, int Mode );
+/*=== ifLib.c ==========================================================*/
+extern float           If_CutDelay( If_Man_t * p, If_Cut_t * pCut );
+extern void            If_CutPropagateRequired( If_Man_t * p, If_Cut_t * pCut, float Required );
 /*=== ifMan.c ==========================================================*/
 extern If_Man_t *      If_ManStart( If_Par_t * pPars );
 extern void            If_ManStop( If_Man_t * p );
 extern If_Obj_t *      If_ManCreatePi( If_Man_t * p );
 extern If_Obj_t *      If_ManCreatePo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 );
 extern If_Obj_t *      If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 );
+extern void            If_ManCreateChoice( If_Man_t * p, If_Obj_t * pRepr );
 /*=== ifMap.c ==========================================================*/
 extern void            If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode );
+extern int             If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequired, char * pLabel );
 /*=== ifPrepro.c ==========================================================*/
 extern void            If_ManPerformMappingPreprocess( If_Man_t * p );
 /*=== ifReduce.c ==========================================================*/
diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c
index c5000dbe..c40ed893 100644
--- a/src/map/if/ifCore.c
+++ b/src/map/if/ifCore.c
@@ -43,7 +43,7 @@ int If_ManPerformMapping( If_Man_t * p )
 {
     If_Obj_t * pObj;
     int nItersFlow = 1;
-    int nItersArea = 1;
+    int nItersArea = 2;
     int clkTotal = clock();
     int i;
     // set arrival times and trivial cuts at const 1 and PIs
@@ -57,21 +57,21 @@ int If_ManPerformMapping( If_Man_t * p )
     if ( p->pPars->fPreprocess && !p->pPars->fArea && p->pPars->nCutsMax >= 4  )
         If_ManPerformMappingPreprocess( p );
     else
-        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1 );
+        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1, "Delay" );
     // try to improve area by expanding and reducing the cuts
     if ( p->pPars->fExpRed && !p->pPars->fTruth )
         If_ManImproveMapping( p );
     // area flow oriented mapping
     for ( i = 0; i < nItersFlow; i++ )
     {
-        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 1 );
+        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 1, "Flow" );
         if ( p->pPars->fExpRed && !p->pPars->fTruth )
             If_ManImproveMapping( p );
     }
     // area oriented mapping
     for ( i = 0; i < nItersArea; i++ )
     {
-        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 1 );
+        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 1, "Area" );
         if ( p->pPars->fExpRed && !p->pPars->fTruth )
             If_ManImproveMapping( p );
     }
@@ -82,47 +82,6 @@ int If_ManPerformMapping( If_Man_t * p )
     return 1;
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequired )
-{
-    If_Obj_t * pObj;
-    int i, clk = clock();
-    assert( Mode >= 0 && Mode <= 2 );
-    // set the cut number
-    p->nCutsUsed   = nCutsUsed;
-    p->nCutsMerged = 0;
-    p->nCutsMax    = 0;
-    // map the internal nodes
-    If_ManForEachNode( p, pObj, i )
-        If_ObjPerformMapping( p, pObj, Mode );
-    // compute required times and stats
-    if ( fRequired )
-    {
-        If_ManComputeRequired( p, Mode==0 );
-        if ( p->pPars->fVerbose )
-        {
-            char Symb = (Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A');
-            printf( "%c:  Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", 
-                Symb, p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
-            PRT( "T", clock() - clk );
-//    printf( "Max number of cuts = %d. Average number of cuts = %5.2f.\n", 
-//        p->nCutsMax, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
-        }
-    }
-    return 1;
-}
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 56e354ce..06a020a6 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -96,7 +96,9 @@ int If_CutFilter( If_Man_t * p, If_Cut_t * pCut )
         pTemp = p->ppCuts[i];
         if ( pTemp->nLeaves > pCut->nLeaves )
         {
-//            continue;
+            // do not fiter the first cut
+            if ( i == 0 )
+                continue;
             // skip the non-contained cuts
             if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
                 continue;
@@ -368,6 +370,10 @@ int If_CutCompareArea( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
         return -1;
     if ( pC0->Area > pC1->Area + 0.0001 )
         return 1;
+    if ( pC0->AveRefs > pC1->AveRefs )
+        return -1;
+    if ( pC0->AveRefs < pC1->AveRefs )
+        return 1;
     if ( pC0->nLeaves < pC1->nLeaves )
         return -1;
     if ( pC0->nLeaves > pC1->nLeaves )
@@ -403,7 +409,7 @@ void If_ManSortCuts( If_Man_t * p, int Mode )
 
 /**Function*************************************************************
 
-  Synopsis    [Computes delay.]
+  Synopsis    [Computes area flow.]
 
   Description []
                
@@ -412,21 +418,29 @@ void If_ManSortCuts( If_Man_t * p, int Mode )
   SeeAlso     []
 
 ***********************************************************************/
-float If_CutDelay( If_Man_t * p, If_Cut_t * pCut )
+float If_CutFlow( If_Man_t * p, If_Cut_t * pCut )
 {
     If_Obj_t * pLeaf;
-    float Delay;
+    float Flow;
     int i;
     assert( pCut->nLeaves > 1 );
-    Delay = -IF_FLOAT_LARGE;
+    Flow = If_CutLutArea(p, pCut);
     If_CutForEachLeaf( p, pCut, pLeaf, i )
-        Delay = IF_MAX( Delay, If_ObjCutBest(pLeaf)->Delay );
-    return Delay + If_CutLutDelay(p, pCut);
+    {
+        if ( pLeaf->nRefs == 0 )
+            Flow += If_ObjCutBest(pLeaf)->Area;
+        else
+        {
+            assert( pLeaf->EstRefs > p->fEpsilon );
+            Flow += If_ObjCutBest(pLeaf)->Area / pLeaf->EstRefs;
+        }
+    }
+    return Flow;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes area flow.]
+  Synopsis    [Average number of references of the leaves.]
 
   Description []
                
@@ -435,24 +449,15 @@ float If_CutDelay( If_Man_t * p, If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-float If_CutFlow( If_Man_t * p, If_Cut_t * pCut )
+float If_CutAverageRefs( If_Man_t * p, If_Cut_t * pCut )
 {
     If_Obj_t * pLeaf;
-    float Flow;
-    int i;
+    int nRefsTotal, i;
     assert( pCut->nLeaves > 1 );
-    Flow = If_CutLutArea(p, pCut);
+    nRefsTotal = 0;
     If_CutForEachLeaf( p, pCut, pLeaf, i )
-    {
-        if ( pLeaf->nRefs == 0 )
-            Flow += If_ObjCutBest(pLeaf)->Area;
-        else
-        {
-            assert( pLeaf->EstRefs > p->fEpsilon );
-            Flow += If_ObjCutBest(pLeaf)->Area / pLeaf->EstRefs;
-        }
-    }
-    return Flow;
+        nRefsTotal += pLeaf->nRefs;
+    return ((float)nRefsTotal)/pCut->nLeaves;
 }
 
 /**Function*************************************************************
@@ -531,6 +536,27 @@ void If_CutPrint( If_Man_t * p, If_Cut_t * pCut )
 
 /**Function*************************************************************
 
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut )
+{
+    If_Obj_t * pLeaf;
+    unsigned i;
+    printf( "{" );
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+        printf( " %d(%.2f/%.2f)", pLeaf->Id, If_ObjCutBest(pLeaf)->Delay, pLeaf->Required );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes area of the first level.]
 
   Description [The cut need to be derefed.]
@@ -585,15 +611,24 @@ float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
 void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
 {
     int * pLeaves;
+    char * pPerm;
     unsigned * pTruth;
+    // save old arrays
     pLeaves = pCutDest->pLeaves;
+    pPerm   = pCutDest->pPerm;
     pTruth  = pCutDest->pTruth;
+    // copy the cut info
     *pCutDest = *pCutSrc;
+    // restore the arrays
     pCutDest->pLeaves = pLeaves;
+    pCutDest->pPerm   = pPerm;
     pCutDest->pTruth  = pTruth;
+    // copy the array data
     memcpy( pCutDest->pLeaves, pCutSrc->pLeaves, sizeof(int) * pCutSrc->nLeaves );
+    if ( pCutSrc->pPerm )
+        memcpy( pCutDest->pPerm, pCutSrc->pPerm, sizeof(unsigned) * If_CutPermWords(pCutSrc->nLimit) );
     if ( pCutSrc->pTruth )
-    memcpy( pCutDest->pTruth,  pCutSrc->pTruth,  sizeof(unsigned) * If_CutTruthWords(pCutSrc->nLimit) );
+        memcpy( pCutDest->pTruth, pCutSrc->pTruth, sizeof(unsigned) * If_CutTruthWords(pCutSrc->nLimit) );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifLib.c b/src/map/if/ifLib.c
new file mode 100644
index 00000000..85747b8e
--- /dev/null
+++ b/src/map/if/ifLib.c
@@ -0,0 +1,203 @@
+/**CFile****************************************************************
+
+  FileName    [ifLib.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapping based on priority cuts.]
+
+  Synopsis    [Computation of LUT paramters depending on the library.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 21, 2006.]
+
+  Revision    [$Id: ifLib.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "if.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float * pPinDelays );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes delay.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutDelay( If_Man_t * p, If_Cut_t * pCut )
+{
+    static int pPinPerm[IF_MAX_LUTSIZE];
+    static float pPinDelays[IF_MAX_LUTSIZE];
+    If_Obj_t * pLeaf;
+    float Delay, DelayCur;
+    float * pLutDelays;
+    int i;
+    assert( pCut->nLeaves > 1 );
+    Delay = -IF_FLOAT_LARGE;
+    if ( p->pPars->pLutLib )
+    {
+        pLutDelays = p->pPars->pLutLib->pLutDelays[pCut->nLeaves];
+        if ( p->pPars->pLutLib->fVarPinDelays )
+        {
+            // compute the delay using sorted pins
+            If_CutSortInputPins( p, pCut, pPinPerm, pPinDelays );
+            for ( i = 0; i < (int)pCut->nLeaves; i++ )
+            {
+                DelayCur = pPinDelays[pPinPerm[i]] + pLutDelays[i];
+                Delay = IF_MAX( Delay, DelayCur );
+            }
+        }
+        else
+        {
+            If_CutForEachLeaf( p, pCut, pLeaf, i )
+            {
+                DelayCur = If_ObjCutBest(pLeaf)->Delay + pLutDelays[0];
+                Delay = IF_MAX( Delay, DelayCur );
+            }
+        }
+    }
+    else
+    {
+        if ( pCut->fUser )
+        {
+            If_CutForEachLeaf( p, pCut, pLeaf, i )
+            {
+                DelayCur = If_ObjCutBest(pLeaf)->Delay + (float)pCut->pPerm[i];
+                Delay = IF_MAX( Delay, DelayCur );
+            }
+        }
+        else
+        {
+            If_CutForEachLeaf( p, pCut, pLeaf, i )
+            {
+                DelayCur = If_ObjCutBest(pLeaf)->Delay;
+                Delay = IF_MAX( Delay, DelayCur );
+            }
+            Delay += 1.0;
+        }
+    }
+    return Delay;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutPropagateRequired( If_Man_t * p, If_Cut_t * pCut, float ObjRequired )
+{
+    static int pPinPerm[IF_MAX_LUTSIZE];
+    static float pPinDelays[IF_MAX_LUTSIZE];
+    If_Obj_t * pLeaf;
+    float * pLutDelays;
+    float Required;
+    int i;
+    // compute the pins
+    if ( p->pPars->pLutLib )
+    {
+        pLutDelays = p->pPars->pLutLib->pLutDelays[pCut->nLeaves];
+        if ( p->pPars->pLutLib->fVarPinDelays )
+        {
+            // compute the delay using sorted pins
+            If_CutSortInputPins( p, pCut, pPinPerm, pPinDelays );
+            for ( i = 0; i < (int)pCut->nLeaves; i++ )
+            {
+                Required = ObjRequired - pLutDelays[i];
+                pLeaf = If_ManObj( p, pCut->pLeaves[pPinPerm[i]] );
+                pLeaf->Required = IF_MIN( pLeaf->Required, Required );
+            }
+        }
+        else
+        {
+            Required = ObjRequired - pLutDelays[0];
+            If_CutForEachLeaf( p, pCut, pLeaf, i )
+                pLeaf->Required = IF_MIN( pLeaf->Required, Required );
+        }
+    }
+    else
+    {
+        if ( pCut->fUser )
+        {
+            If_CutForEachLeaf( p, pCut, pLeaf, i )
+            {
+                Required = ObjRequired - (float)pCut->pPerm[i];
+                pLeaf->Required = IF_MIN( pLeaf->Required, Required );
+            }
+        }
+        else
+        {
+            Required = ObjRequired - (float)1.0;
+            If_CutForEachLeaf( p, pCut, pLeaf, i )
+                pLeaf->Required = IF_MIN( pLeaf->Required, Required );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the pins in the degreasing order of delays.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float * pPinDelays )
+{
+    If_Obj_t * pLeaf;
+    int i, j, best_i, temp;
+    // start the trivial permutation and collect pin delays
+    If_CutForEachLeaf( p, pCut, pLeaf, i );
+    {
+        pPinPerm[i] = i;
+        pPinDelays[i] = If_ObjCutBest(pLeaf)->Delay;
+    }
+    // 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 < (int)pCut->nLeaves-1; i++ )
+    {
+        best_i = i;
+        for ( j = i+1; j < (int)pCut->nLeaves; 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
+    for ( i = 1; i < (int)pCut->nLeaves; i++ )
+        assert( pPinDelays[pPinPerm[i-1]] >= pPinDelays[pPinPerm[i]] );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 46ca1b5b..040b0e4f 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -58,7 +58,8 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     p->vTemp   = Vec_PtrAlloc( 100 );
     // prepare the memory manager
     p->nTruthSize = p->pPars->fTruth? If_CutTruthWords( p->pPars->nLutSize ) : 0;
-    p->nCutSize   = sizeof(If_Cut_t) + sizeof(int) * p->pPars->nLutSize + sizeof(unsigned) * p->nTruthSize;
+    p->nPermSize  = p->pPars->fUsePerm? If_CutPermWords( p->pPars->nLutSize ) : 0;
+    p->nCutSize   = sizeof(If_Cut_t) + sizeof(int) * (p->pPars->nLutSize + p->nPermSize + p->nTruthSize);
     p->nEntrySize = sizeof(If_Obj_t) + p->pPars->nCutsMax * p->nCutSize;
     p->nEntryBase = sizeof(If_Obj_t) + p->pPars->nCutsMax * sizeof(If_Cut_t);
     p->pMem = Mem_FixedStart( p->nEntrySize );
@@ -182,7 +183,7 @@ If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_
     pObj->fCompl1 = fCompl1;
     pObj->pFanin0 = pFan0; pFan0->nRefs++;
     pObj->pFanin1 = pFan1; pFan1->nRefs++;
-    pObj->fPhase  = (fCompl0? !pFan0->fPhase : pFan0->fPhase) & (fCompl1? !pFan1->fPhase : pFan1->fPhase);
+    pObj->fPhase  = (fCompl0 ^ pFan0->fPhase) & (fCompl1 ^ pFan1->fPhase);
     pObj->Level   = 1 + IF_MAX( pFan0->Level, pFan1->Level );
     if ( p->nLevelMax < (int)pObj->Level )
         p->nLevelMax = (int)pObj->Level;
@@ -192,6 +193,31 @@ If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_
 
 /**Function*************************************************************
 
+  Synopsis    [Creates the choice node.]
+
+  Description [Should be called after the equivalence class nodes are linked.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManCreateChoice( If_Man_t * p, If_Obj_t * pObj )
+{
+    If_Obj_t * pTemp;
+    // mark the node as a representative if its class
+    assert( pObj->fRepr == 0 );
+    pObj->fRepr = 1;
+    // update the level of this node (needed for correct required time computation)
+    for ( pTemp = pObj->pEquiv; pTemp; pTemp = pTemp->pEquiv )
+        pObj->Level = IF_MAX( pObj->Level, pTemp->Level );
+    // mark the largest level
+    if ( p->nLevelMax < (int)pObj->Level )
+        p->nLevelMax = (int)pObj->Level;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prepares memory for the node with cuts.]
 
   Description []
@@ -216,7 +242,8 @@ If_Obj_t * If_ManSetupObj( If_Man_t * p )
         pCut = pObj->Cuts + i;
         pCut->nLimit  = p->pPars->nLutSize;
         pCut->pLeaves = pArrays + i * p->pPars->nLutSize;
-        pCut->pTruth  = pArrays + p->pPars->nCutsMax * p->pPars->nLutSize + i * p->nTruthSize;
+        pCut->pPerm   = (char *)(p->pPars->fUsePerm? pArrays + p->pPars->nCutsMax * p->pPars->nLutSize + i * p->nPermSize : NULL);
+        pCut->pTruth  = p->pPars->fTruth? pArrays + p->pPars->nCutsMax * (p->pPars->nLutSize + p->nPermSize) + i * p->nTruthSize : NULL;
     }
     // assign ID and save 
     pObj->Id = Vec_PtrSize(p->vObjs);
@@ -270,7 +297,8 @@ If_Cut_t ** If_ManSetupCuts( If_Man_t * p )
         pCutStore[i] = (If_Cut_t *)((char *)pCutStore[0] + sizeof(If_Cut_t) * i);
         pCutStore[i]->nLimit  = p->pPars->nLutSize;
         pCutStore[i]->pLeaves = pArrays + i * p->pPars->nLutSize;
-        pCutStore[i]->pTruth  = pArrays + nCutsTotal * p->pPars->nLutSize + i * p->nTruthSize;
+        pCutStore[i]->pPerm   = (char *)(p->pPars->fUsePerm? pArrays + nCutsTotal * p->pPars->nLutSize + i * p->nPermSize : NULL);
+        pCutStore[i]->pTruth  = p->pPars->fTruth? pArrays + nCutsTotal * (p->pPars->nLutSize + p->nPermSize) + i * p->nTruthSize : NULL;
     }
     return pCutStore;
 }
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 76c524ee..743662b0 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -30,6 +30,7 @@
   - ordering of the outputs by size
   - merging Delay, Delay2, and Area
   - expand/reduce area recovery
+  - use average nrefs for tie-breaking
 
 */
 
@@ -59,7 +60,7 @@ static inline int If_WordCountOnes( unsigned uWord )
 
 /**Function*************************************************************
 
-  Synopsis    [Finds the best cut.]
+  Synopsis    [Finds the best cut for the given node.]
 
   Description [Mapping modes: delay (0), area flow (1), area (2).]
                
@@ -71,7 +72,10 @@ static inline int If_WordCountOnes( unsigned uWord )
 void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode )
 {
     If_Cut_t * pCut0, * pCut1, * pCut;
-    int i, k, iCut, Temp;
+    int i, k, iCut;
+
+    assert( !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->nCuts > 1 );
+    assert( !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->nCuts > 1 );
 
     // prepare
     if ( Mode == 0 )
@@ -105,29 +109,30 @@ void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode )
         // make sure K-feasible cut exists
         if ( If_WordCountOnes(pCut0->uSign | pCut1->uSign) > p->pPars->nLutSize )
             continue;
-        // prefilter using arrival times
-        if ( Mode && (pCut0->Delay > pObj->Required + p->fEpsilon || pCut1->Delay > pObj->Required + p->fEpsilon) )
-            continue;
         // merge the nodes
         if ( !If_CutMerge( pCut0, pCut1, pCut ) )
             continue;
         // check if this cut is contained in any of the available cuts
         pCut->uSign = pCut0->uSign | pCut1->uSign;
+        pCut->fCompl = 0;
+//        if ( p->pPars->pFuncCost == NULL && If_CutFilter( p, pCut ) ) // do not filter functionality cuts
         if ( If_CutFilter( p, pCut ) )
             continue;
-        // check if the cut satisfies the required times
-        pCut->Delay = If_CutDelay( p, pCut );
-        if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
-            continue;
         // the cuts have been successfully merged
         // compute the truth table
         if ( p->pPars->fTruth )
             If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
         // compute the application-specific cost and depth
-        Temp = p->pPars->pFuncCost? p->pPars->pFuncCost(If_CutTruth(pCut), pCut->nLimit) : 0;
-        pCut->Cost = (Temp & 0xffff); pCut->Depth = (Temp >> 16);
+        pCut->fUser = (p->pPars->pFuncCost != NULL);
+        pCut->Cost = p->pPars->pFuncCost? p->pPars->pFuncCost(pCut) : 0;
+        // check if the cut satisfies the required times
+        pCut->Delay = If_CutDelay( p, pCut );
+//        printf( "%.2f ", pCut->Delay );
+        if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
+            continue;
         // compute area of the cut (this area may depend on the application specific cost)
         pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
+        pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
         // make sure the cut is the last one (after filtering it may not be so)
         assert( pCut == p->ppCuts[iCut] );
         p->ppCuts[iCut] = p->ppCuts[p->nCuts];
@@ -139,7 +144,6 @@ void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode )
         iCut = p->nCuts;
         pCut = p->ppCuts[iCut];
     } 
-//printf( "%d  ", p->nCuts );
     assert( p->nCuts > 0 );
     // sort if we have more cuts
     If_ManSortCuts( p, Mode );
@@ -149,10 +153,6 @@ void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode )
     If_ObjForEachCutStart( pObj, pCut, i, 1 )
         If_CutCopy( pCut, p->ppCuts[i-1] );
     assert( If_ObjCutBest(pObj)->nLeaves > 1 );
-    // assign delay of the trivial cut
-    If_ObjCutTriv(pObj)->Delay = If_ObjCutBest(pObj)->Delay;
-//printf( "%d %d   ", pObj->Id, (int)If_ObjCutBest(pObj)->Delay );
-//printf( "%d %d   ", pObj->Id, pObj->nCuts );
     // ref the selected cut
     if ( Mode == 2 && pObj->nRefs > 0 )
         If_CutRef( p, If_ObjCutBest(pObj), 100 );
@@ -161,6 +161,132 @@ void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode )
         p->nCutsMax = pObj->nCuts;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Finds the best cut for the choice node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ObjMergeChoice( If_Man_t * p, If_Obj_t * pObj, int Mode )
+{
+    If_Obj_t * pTemp;
+    If_Cut_t * pCutTemp, * pCut;
+    int i, iCut;
+    assert( pObj->pEquiv != NULL );
+    // prepare
+    if ( Mode == 2 && pObj->nRefs > 0 )
+        If_CutDeref( p, If_ObjCutBest(pObj), 100 );
+    // prepare room for the next cut
+    p->nCuts = 0;
+    iCut = p->nCuts;
+    pCut = p->ppCuts[iCut];
+    // generate cuts
+    for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
+    If_ObjForEachCutStart( pTemp, pCutTemp, i, 1 )
+    {
+        assert( pTemp->nCuts > 1 );
+        assert( pTemp == pObj || pTemp->nRefs == 0 );
+        // copy the cut into storage
+        If_CutCopy( pCut, pCutTemp );
+        // check if this cut is contained in any of the available cuts
+        if ( If_CutFilter( p, pCut ) )
+            continue;
+        // the cuts have been successfully merged
+        // check if the cut satisfies the required times
+        assert( pCut->Delay == If_CutDelay( p, pCut ) );
+        if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
+            continue;
+        // set the phase attribute
+        pCut->fCompl ^= (pObj->fPhase ^ pTemp->fPhase);
+        // compute area of the cut (this area may depend on the application specific cost)
+        pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
+        pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
+        // make sure the cut is the last one (after filtering it may not be so)
+        assert( pCut == p->ppCuts[iCut] );
+        p->ppCuts[iCut] = p->ppCuts[p->nCuts];
+        p->ppCuts[p->nCuts] = pCut;
+        // count the cut
+        p->nCuts++;
+        // prepare room for the next cut
+        iCut = p->nCuts;
+        pCut = p->ppCuts[iCut];
+        // quit if we exceeded the number of cuts
+        if ( p->nCuts >= p->pPars->nCutsMax * p->pPars->nCutsMax )
+            break;
+    } 
+    assert( p->nCuts > 0 );
+    // sort if we have more cuts
+    If_ManSortCuts( p, Mode );
+    // decide how many cuts to use
+    pObj->nCuts = IF_MIN( p->nCuts + 1, p->nCutsUsed );
+    // take the first
+    If_ObjForEachCutStart( pObj, pCut, i, 1 )
+        If_CutCopy( pCut, p->ppCuts[i-1] );
+    assert( If_ObjCutBest(pObj)->nLeaves > 1 );
+    // ref the selected cut
+    if ( Mode == 2 && pObj->nRefs > 0 )
+        If_CutRef( p, If_ObjCutBest(pObj), 100 );
+    // find the largest cut
+    if ( p->nCutsMax < pObj->nCuts )
+        p->nCutsMax = pObj->nCuts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one mapping pass over all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequired, char * pLabel )
+{
+    ProgressBar * pProgress;
+    If_Obj_t * pObj;
+    int i, clk = clock();
+    assert( Mode >= 0 && Mode <= 2 );
+    // set the cut number
+    p->nCutsUsed   = nCutsUsed;
+    p->nCutsMerged = 0;
+    p->nCutsSaved  = 0;
+    p->nCutsMax    = 0;
+    // map the internal nodes
+    pProgress = Extra_ProgressBarStart( stdout, If_ManObjNum(p) );
+    If_ManForEachNode( p, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, pLabel );
+        If_ObjPerformMapping( p, pObj, Mode );
+        if ( pObj->fRepr )
+            If_ObjMergeChoice( p, pObj, Mode );
+    }
+    Extra_ProgressBarStop( pProgress );
+    // compute required times and stats
+    if ( fRequired )
+    {
+        If_ManComputeRequired( p, Mode==0 );
+        if ( p->pPars->fVerbose )
+        {
+            char Symb = (Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A');
+            printf( "%c:  Del = %6.2f. Area = %8.2f. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
+                Symb, p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+            PRT( "T", clock() - clk );
+//            printf( "Saved cuts = %d.\n", p->nCutsSaved );
+//    printf( "Max number of cuts = %d. Average number of cuts = %5.2f.\n", 
+//        p->nCutsMax, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+        }
+    }
+    return 1;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifPrepro.c b/src/map/if/ifPrepro.c
index 797e8727..7aec8f53 100644
--- a/src/map/if/ifPrepro.c
+++ b/src/map/if/ifPrepro.c
@@ -50,7 +50,7 @@ void If_ManPerformMappingPreprocess( If_Man_t * p )
 
     // perform min-area mapping and move the cut to the end
     p->pPars->fArea = 1;
-    If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0 );
+    If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0, "Start delay" );
     p->pPars->fArea = 0;
     delayArea = If_ManDelayMax( p );
     if ( p->pPars->DelayTarget != -1 && delayArea < p->pPars->DelayTarget - p->fEpsilon )
@@ -59,15 +59,15 @@ void If_ManPerformMappingPreprocess( If_Man_t * p )
 
     // perfrom min-delay mapping and move the cut to the end
     p->pPars->fFancy = 1;
-    If_ManPerformMappingRound( p, p->pPars->nCutsMax - 1, 0, 0 );
+    If_ManPerformMappingRound( p, p->pPars->nCutsMax - 1, 0, 0, "Start delay-2" );
     p->pPars->fFancy = 0;
     delayDelay = If_ManDelayMax( p );
     if ( p->pPars->DelayTarget != -1 && delayDelay < p->pPars->DelayTarget - p->fEpsilon )
         delayDelay = p->pPars->DelayTarget;
     If_ManPerformMappingMoveBestCut( p, p->pPars->nCutsMax - 2, 1 );
 
-    // perform min-area mapping 
-    If_ManPerformMappingRound( p, p->pPars->nCutsMax - 2, 0, 0 );
+    // perform min-delay mapping
+    If_ManPerformMappingRound( p, p->pPars->nCutsMax - 2, 0, 0, "Start flow" );
     delayPure = If_ManDelayMax( p );
     if ( p->pPars->DelayTarget != -1 && delayPure < p->pPars->DelayTarget - p->fEpsilon )
         delayPure = p->pPars->DelayTarget;
@@ -100,7 +100,7 @@ void If_ManPerformMappingPreprocess( If_Man_t * p )
     If_ManComputeRequired( p, 1 );
     if ( p->pPars->fVerbose )
     {
-        printf( "S:  Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", 
+        printf( "S:  Del = %6.2f. Area = %8.2f. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
             p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
         PRT( "T", clock() - clk );
     }
diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c
index 0b3cf9c2..69312c5b 100644
--- a/src/map/if/ifReduce.c
+++ b/src/map/if/ifReduce.c
@@ -55,7 +55,7 @@ void If_ManImproveMapping( If_Man_t * p )
     If_ManComputeRequired( p, 0 );
     if ( p->pPars->fVerbose )
     {
-        printf( "E:  Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", 
+        printf( "E:  Del = %6.2f. Area = %8.2f. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
             p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
         PRT( "T", clock() - clk );
     }
@@ -65,7 +65,7 @@ void If_ManImproveMapping( If_Man_t * p )
     If_ManComputeRequired( p, 0 );
     if ( p->pPars->fVerbose )
     {
-        printf( "R:  Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", 
+        printf( "R:  Del = %6.2f. Area = %8.2f. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
             p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
         PRT( "T", clock() - clk );
     }
@@ -75,7 +75,7 @@ void If_ManImproveMapping( If_Man_t * p )
     If_ManComputeRequired( p, 0 );
     if ( p->pPars->fVerbose )
     {
-        printf( "E:  Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", 
+        printf( "E:  Del = %6.2f. Area = %8.2f. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
             p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
         PRT( "T", clock() - clk );
     }
diff --git a/src/map/if/ifSeq.c b/src/map/if/ifSeq.c
index bc4ab806..ac2754c0 100644
--- a/src/map/if/ifSeq.c
+++ b/src/map/if/ifSeq.c
@@ -58,7 +58,7 @@ int If_ManPerformMappingSeq( If_Man_t * p )
         pObj->EstRefs = (float)1.0;
     // delay oriented mapping
     p->pPars->fFancy = 1;
-    If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0 );
+    If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0, NULL );
     p->pPars->fFancy = 0;
 
     // perform iterations over the circuit
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index 3f9f9f14..c2f3196b 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -72,18 +72,19 @@ void If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut
     extern void Kit_FactorTest( unsigned * pTruth, int nVars );
 
     // permute the first table
-    if ( fCompl0 ) 
+    if ( fCompl0 ^ pCut0->fCompl ) 
         Extra_TruthNot( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit );
     else
         Extra_TruthCopy( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit );
     Extra_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nLeaves, pCut->nLimit, Cut_TruthPhase(pCut, pCut0) );
     // permute the second table
-    if ( fCompl1 ) 
+    if ( fCompl1 ^ pCut1->fCompl ) 
         Extra_TruthNot( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit );
     else
         Extra_TruthCopy( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit );
     Extra_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nLeaves, pCut->nLimit, Cut_TruthPhase(pCut, pCut1) );
     // produce the resulting table
+    assert( pCut->fCompl == 0 );
     if ( pCut->fCompl )
         Extra_TruthNand( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
     else
@@ -91,6 +92,7 @@ void If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut
 
     // perform 
 //    Kit_FactorTest( If_CutTruth(pCut), pCut->nLimit );
+//    printf( "%d ", If_CutLeaveNum(pCut) - Kit_TruthSupportSize(If_CutTruth(pCut), If_CutLeaveNum(pCut)) );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index 1144fa3f..bb8e3dee 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -44,10 +44,24 @@ float If_ManDelayMax( If_Man_t * p )
     If_Obj_t * pObj;
     float DelayBest;
     int i;
+    if ( p->pPars->fLatchPaths && p->pPars->nLatches == 0 )
+    {
+        printf( "Delay optimization of latch path is not performed because there is no latches.\n" );
+        p->pPars->fLatchPaths = 0;
+    }
     DelayBest = -IF_FLOAT_LARGE;
-    If_ManForEachPo( p, pObj, i )
-        if ( DelayBest < If_ObjCutBest( If_ObjFanin0(pObj) )->Delay )
-             DelayBest = If_ObjCutBest( If_ObjFanin0(pObj) )->Delay;
+    if ( p->pPars->fLatchPaths )
+    {
+        If_ManForEachLatch( p, pObj, i )
+            if ( DelayBest < If_ObjCutBest( If_ObjFanin0(pObj) )->Delay )
+                 DelayBest = If_ObjCutBest( If_ObjFanin0(pObj) )->Delay;
+    }
+    else
+    {
+        If_ManForEachPo( p, pObj, i )
+            if ( DelayBest < If_ObjCutBest( If_ObjFanin0(pObj) )->Delay )
+                 DelayBest = If_ObjCutBest( If_ObjFanin0(pObj) )->Delay;
+    }
     return DelayBest;
 }
 
@@ -174,10 +188,8 @@ float If_ManScanMapping( If_Man_t * p )
 ***********************************************************************/
 void If_ManComputeRequired( If_Man_t * p, int fFirstTime )
 {
-    If_Obj_t * pObj, * pLeaf;
-    If_Cut_t * pCutBest;
-    float Required;
-    int i, k;
+    If_Obj_t * pObj;
+    int i;
     // compute area, clean required times, collect nodes used in the mapping
     p->AreaGlo = If_ManScanMapping( p );
     // get the global required times
@@ -209,16 +221,8 @@ void If_ManComputeRequired( If_Man_t * p, int fFirstTime )
             If_ObjFanin0(pObj)->Required = p->RequiredGlo;
     }
     // go through the nodes in the reverse topological order
-    Vec_PtrForEachEntry( p->vMapped, pObj, k )
-    {
-        // get the best cut of the node
-        pCutBest = If_ObjCutBest(pObj);
-        // get the required times for the leaves of the cut
-        Required = pObj->Required - If_CutLutDelay( p, pCutBest );
-        // update the required time of the leaves
-        If_CutForEachLeaf( p, pCutBest, pLeaf, i )
-            pLeaf->Required = IF_MIN( pLeaf->Required, Required );
-    }
+    Vec_PtrForEachEntry( p->vMapped, pObj, i )
+        If_CutPropagateRequired( p, If_ObjCutBest(pObj), pObj->Required );
 }
 
 
diff --git a/src/map/if/module.make b/src/map/if/module.make
index b7d3185f..20586ed8 100644
--- a/src/map/if/module.make
+++ b/src/map/if/module.make
@@ -1,5 +1,6 @@
 SRC +=  src/map/if/ifCore.c \
     src/map/if/ifCut.c \
+    src/map/if/ifLib.c \
     src/map/if/ifMan.c \
     src/map/if/ifMap.c \
     src/map/if/ifPrepro.c \
diff --git a/src/map/mapper/mapperCut.c b/src/map/mapper/mapperCut.c
index 91ef6562..b05e9d0c 100644
--- a/src/map/mapper/mapperCut.c
+++ b/src/map/mapper/mapperCut.c
@@ -149,7 +149,7 @@ void Map_MappingCuts( Map_Man_t * p )
     if ( p->fVerbose )
     {
         nCuts = Map_MappingCountAllCuts(p);
-        printf( "Nodes = %6d. Total %d-feasible cuts = %d. Per node = %.1f. ", 
+        printf( "Nodes = %6d.  Total %d-feasible cuts = %10d.  Per node = %.1f. ", 
                p->nNodes, p->nVarsMax, nCuts, ((float)nCuts)/p->nNodes );
         PRT( "Time", clock() - clk );
     }
diff --git a/src/misc/st/st.c b/src/misc/st/st.c
index 892a33af..c0965a41 100644
--- a/src/misc/st/st.c
+++ b/src/misc/st/st.c
@@ -8,7 +8,7 @@
  *
  */
 #include <stdio.h>
-//#include "extra.h"
+#include <stdlib.h>
 #include "st.h"
 
 #ifndef ABS
diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index d97fca58..58c55cd2 100644
--- a/src/opt/kit/kit.h
+++ b/src/opt/kit/kit.h
@@ -91,6 +91,9 @@ struct Kit_Graph_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
+#define KIT_MIN(a,b)       (((a) < (b))? (a) : (b))
+#define KIT_MAX(a,b)       (((a) > (b))? (a) : (b))
+
 #ifndef ALLOC
 #define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
 #endif
@@ -143,8 +146,10 @@ static inline Kit_Node_t * Kit_GraphNode( Kit_Graph_t * pGraph, int i )
 static inline Kit_Node_t * Kit_GraphNodeLast( Kit_Graph_t * pGraph )                      { return pGraph->pNodes + pGraph->nSize - 1;          }
 static inline int          Kit_GraphNodeInt( Kit_Graph_t * pGraph, Kit_Node_t * pNode )   { return pNode - pGraph->pNodes;                      }
 static inline int          Kit_GraphNodeIsVar( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return Kit_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; }
-static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph )                           { assert( Kit_GraphIsVar( pGraph ) );    return Kit_GraphNode( pGraph, pGraph->eRoot.Node ); }
-static inline int          Kit_GraphVarInt( Kit_Graph_t * pGraph )                        { assert( Kit_GraphIsVar( pGraph ) );    return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) );}
+static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph )                           { assert( Kit_GraphIsVar( pGraph ) );    return Kit_GraphNode( pGraph, pGraph->eRoot.Node );      }
+static inline int          Kit_GraphVarInt( Kit_Graph_t * pGraph )                        { assert( Kit_GraphIsVar( pGraph ) );    return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); }
+static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.Node);     }
+static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node);     }
 
 static inline int          Kit_Float2Int( float Val )     { return *((int *)&Val);               }
 static inline float        Kit_Int2Float( int Num )       { return *((float *)&Num);             }
@@ -272,7 +277,7 @@ static inline void Kit_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * p
 /*=== kitBdd.c ==========================================================*/
 extern DdNode *        Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars );
 extern DdNode *        Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph );
-extern DdNode *        Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars );
+extern DdNode *        Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop );
 /*=== kitFactor.c ==========================================================*/
 extern Kit_Graph_t *   Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_t * vMemory );
 /*=== kitGraph.c ==========================================================*/
@@ -288,6 +293,7 @@ extern Kit_Edge_t      Kit_GraphAddNodeXor( Kit_Graph_t * pGraph, Kit_Edge_t eEd
 extern Kit_Edge_t      Kit_GraphAddNodeMux( Kit_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edge_t eEdgeT, Kit_Edge_t eEdgeE, int Type );
 extern unsigned        Kit_GraphToTruth( Kit_Graph_t * pGraph );
 extern Kit_Graph_t *   Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
+extern int             Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t * pLeaf );
 /*=== kitHop.c ==========================================================*/
 /*=== kitIsop.c ==========================================================*/
 extern int             Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
diff --git a/src/opt/kit/kitBdd.c b/src/opt/kit/kitBdd.c
index ed978740..9c8d4f7a 100644
--- a/src/opt/kit/kitBdd.c
+++ b/src/opt/kit/kitBdd.c
@@ -135,26 +135,26 @@ DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph )
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Kit_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nVars, int nVarsTotal )
+DdNode * Kit_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nVars, int nVarsTotal, int fMSBonTop )
 {
     DdNode * bF0, * bF1, * bF;
-    if ( nVars == 0 )
+    int Var;
+    if ( nVars <= 5 )
     {
-        if ( pTruth[iBit>>5] & (1 << iBit&31) )
-            return b1;
-        return b0;
-    }
-    if ( nVars == 5 )
-    {
-        if ( pTruth[iBit>>5] == 0xFFFFFFFF )
-            return b1;
-        if ( pTruth[iBit>>5] == 0 )
+        unsigned uTruth, uMask;
+        uMask = ((~(unsigned)0) >> (32 - (1<<nVars)));
+        uTruth = (pTruth[iBit>>5] >> (iBit&31)) & uMask;
+        if ( uTruth == 0 )
             return b0;
+        if ( uTruth == uMask )
+            return b1;        
     }
+    // find the variable to use
+    Var = fMSBonTop? nVarsTotal-nVars : nVars-1;
     // other special cases can be added
-    bF0 = Kit_TruthToBdd_rec( dd, pTruth, iBit,                nVars-1, nVarsTotal );  Cudd_Ref( bF0 );
-    bF1 = Kit_TruthToBdd_rec( dd, pTruth, iBit+(1<<(nVars-1)), nVars-1, nVarsTotal );  Cudd_Ref( bF1 );
-    bF  = Cudd_bddIte( dd, dd->vars[nVarsTotal-nVars], bF1, bF0 );                     Cudd_Ref( bF );
+    bF0 = Kit_TruthToBdd_rec( dd, pTruth, iBit,                nVars-1, nVarsTotal, fMSBonTop );  Cudd_Ref( bF0 );
+    bF1 = Kit_TruthToBdd_rec( dd, pTruth, iBit+(1<<(nVars-1)), nVars-1, nVarsTotal, fMSBonTop );  Cudd_Ref( bF1 );
+    bF  = Cudd_bddIte( dd, dd->vars[Var], bF1, bF0 );                     Cudd_Ref( bF );
     Cudd_RecursiveDeref( dd, bF0 );
     Cudd_RecursiveDeref( dd, bF1 );
     Cudd_Deref( bF );
@@ -176,9 +176,9 @@ DdNode * Kit_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nV
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars )
+DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop )
 {
-    return Kit_TruthToBdd_rec( dd, pTruth, 0, nVars, nVars );
+    return Kit_TruthToBdd_rec( dd, pTruth, 0, nVars, nVars, fMSBonTop );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/kit/kitFactor.c b/src/opt/kit/kitFactor.c
index 618a4272..cbac918d 100644
--- a/src/opt/kit/kitFactor.c
+++ b/src/opt/kit/kitFactor.c
@@ -197,6 +197,7 @@ Kit_Edge_t Kit_SopFactorTrivialCube_rec( Kit_Graph_t * pFForm, unsigned uCube, i
 {
     Kit_Edge_t eNode1, eNode2;
     int i, iLit, nLits, nLits1, nLits2;
+    assert( uCube );
     // count the number of literals in this interval
     nLits = 0;
     for ( i = nStart; i < nFinish; i++ )
diff --git a/src/opt/kit/kitGraph.c b/src/opt/kit/kitGraph.c
index e2172ca3..1123b90e 100644
--- a/src/opt/kit/kitGraph.c
+++ b/src/opt/kit/kitGraph.c
@@ -354,13 +354,40 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor
     Kit_Graph_t * pGraph;
     int RetValue;
     // derive SOP
-    RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 0 );
-    assert( RetValue == 0 );
+    RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 0 ); // tried 1 and found not useful in "renode"
+    if ( RetValue == -1 )
+        return NULL;
+    assert( RetValue == 0 || RetValue == 1 );
     // derive factored form
-    pGraph = Kit_SopFactor( vMemory, 0, nVars, vMemory );
+    pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory );
     return pGraph;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Derives the maximum depth from the leaf to the root.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t * pLeaf )
+{
+    int Depth0, Depth1, Depth;
+    if ( pNode == pLeaf )
+        return 0;
+    if ( Kit_GraphNodeIsVar(pGraph, pNode) )
+        return -100;
+    Depth0 = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeFanin0(pGraph, pNode), pLeaf );
+    Depth1 = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeFanin1(pGraph, pNode), pLeaf );
+    Depth = KIT_MAX( Depth0, Depth1 );
+    Depth = (Depth == -100) ? -100 : Depth + 1;
+    return Depth;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/kit/kitIsop.c b/src/opt/kit/kitIsop.c
index 420cb16f..d54932ee 100644
--- a/src/opt/kit/kitIsop.c
+++ b/src/opt/kit/kitIsop.c
@@ -67,9 +67,14 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB
     if ( pcRes->nCubes == -1 )
     {
         vMemory->nSize = -1;
-        return 0;
+        return -1;
     }
     assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
+    if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
+    {
+        Vec_IntShrink( vMemory, pcRes->nCubes );
+        return 0;
+    }
     if ( fTryBoth )
     {
         // compute ISOP for the complemented polarity