Other changes to enable new features in the mapper.

7 files changed, 440 insertions, 28 deletions

diff --git a/src/map/if/if.h b/src/map/if/if.h
index 86d504bc..52cd0c2b 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -99,6 +99,7 @@ struct If_Par_t_
     int                fEnableCheck07;// enable additional checking
     int                fEnableCheck08;// enable additional checking
     int                fEnableCheck10;// enable additional checking
+    int                fEnableRealPos;// enable additional feature
     int                fVerbose;      // the verbosity flag
     // internal parameters
     int                fDelayOpt;     // special delay optimization
@@ -449,8 +450,8 @@ extern int             If_ManPerformMappingSeq( If_Man_t * p );
 /*=== ifTime.c ============================================================*/
 extern int             If_CutDelaySopCost( If_Man_t * p, If_Cut_t * pCut );
 extern Vec_Wrd_t *     If_CutDelaySopArray( If_Man_t * p, If_Cut_t * pCut );
-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 );
+extern float           If_CutDelay( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut );
+extern void            If_CutPropagateRequired( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut, float Required );
 extern void            If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut );
 /*=== ifTruth.c ===========================================================*/
 extern int             If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
diff --git a/src/map/if/ifDec10f.c b/src/map/if/ifDec10f.c
new file mode 100644
index 00000000..9f30cf96
--- /dev/null
+++ b/src/map/if/ifDec10f.c
@@ -0,0 +1,384 @@
+/**CFile****************************************************************
+
+  FileName    [ifDec10f.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapping based on priority cuts.]
+
+  Synopsis    [Fast checking procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 21, 2006.]
+
+  Revision    [$Id: ifDec10f.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "if.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the bit count for the first 256 integer numbers
+static int BitCount8[256] = {
+    0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
+    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+    3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
+};
+// variable swapping code
+static word PMasks[5][3] = {
+    { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
+    { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
+    { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
+    { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 },
+    { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 }
+};
+// elementary truth tables
+static word Truth6[6] = {
+    0xAAAAAAAAAAAAAAAA,
+    0xCCCCCCCCCCCCCCCC,
+    0xF0F0F0F0F0F0F0F0,
+    0xFF00FF00FF00FF00,
+    0xFFFF0000FFFF0000,
+    0xFFFFFFFF00000000
+};
+static word Truth10[10][16] = {
+    0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,
+    0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,
+    0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,
+    0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,
+    0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,
+    0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,
+    0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,
+    0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,
+    0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,
+    0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF
+};
+
+extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
+extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
+
+//  vars are numbered starting from MSB
+//  moving down means moving from MSB -> LSB
+//  moving up means moving from LSB -> MSB
+//  groups list vars indices from MSB to LSB
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+// variable permutation for large functions
+static inline int If_CluWordNum( int nVars )
+{
+    return nVars <= 6 ? 1 : 1 << (nVars-6);
+}
+static inline void If_CluCopy( word * pOut, word * pIn, int nVars )
+{
+    int w, nWords = If_CluWordNum( nVars );
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] = pIn[w];
+}
+static inline void If_CluSwapAdjacent( word * pOut, word * pIn, int iVar, int nVars )
+{
+    int i, k, nWords = If_CluWordNum( nVars );
+    assert( iVar < nVars - 1 );
+    if ( iVar < 5 )
+    {
+        int Shift = (1 << iVar);
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
+    }
+    else if ( iVar > 5 )
+    {
+        int Step = (1 << (iVar - 6));
+        for ( k = 0; k < nWords; k += 4*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+                pOut[i] = pIn[i];
+            for ( i = 0; i < Step; i++ )
+                pOut[Step+i] = pIn[2*Step+i];
+            for ( i = 0; i < Step; i++ )
+                pOut[2*Step+i] = pIn[Step+i];
+            for ( i = 0; i < Step; i++ )
+                pOut[3*Step+i] = pIn[3*Step+i];
+            pIn  += 4*Step;
+            pOut += 4*Step;
+        }
+    }
+    else // if ( iVar == 5 )
+    {
+        for ( i = 0; i < nWords; i += 2 )
+        {
+            pOut[i]   = (pIn[i]   & 0x00000000FFFFFFFF) | ((pIn[i+1] & 0x00000000FFFFFFFF) << 32);
+            pOut[i+1] = (pIn[i+1] & 0xFFFFFFFF00000000) | ((pIn[i]   & 0xFFFFFFFF00000000) >> 32);
+        }
+    }
+}
+
+// moves one var (v) to the given position (p)
+void If_CluMoveVarOneUp( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int v, int p )
+{
+    word pG[16], * pIn = pF, * pOut = pG, * pTemp;
+    int iPlace0, iPlace1, Count = 0;
+    assert( v >= 0 && v < nVars );
+    assert( Var2Pla[v] >= p );
+    while ( Var2Pla[v] > p )
+    {
+        iPlace0 = Var2Pla[v]-1;
+        iPlace1 = Var2Pla[v];
+        If_CluSwapAdjacent( pOut, pIn, iPlace0, nVars );
+        pTemp = pIn; pIn = pOut, pOut = pTemp;
+        Var2Pla[Pla2Var[iPlace0]]++;
+        Var2Pla[Pla2Var[iPlace1]]--;
+        Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
+        Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
+        Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
+        Count++;
+    }
+    if ( Count & 1 )
+        If_CluCopy( pF, pIn, nVars );
+    assert( Pla2Var[p] == v );
+}
+
+// moves one var (v) to the given position (p)
+void If_CluMoveVarOneDown( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int v, int p )
+{
+    word pG[16], * pIn = pF, * pOut = pG, * pTemp;
+    int iPlace0, iPlace1, Count = 0;
+    assert( v >= 0 && v < nVars );
+    assert( Var2Pla[v] <= p );
+    while ( Var2Pla[v] < p )
+    {
+        iPlace0 = Var2Pla[v];
+        iPlace1 = Var2Pla[v]+1;
+        If_CluSwapAdjacent( pOut, pIn, iPlace0, nVars );
+        pTemp = pIn; pIn = pOut, pOut = pTemp;
+        Var2Pla[Pla2Var[iPlace0]]++;
+        Var2Pla[Pla2Var[iPlace1]]--;
+        Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
+        Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
+        Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
+        Count++;
+    }
+    if ( Count & 1 )
+        If_CluCopy( pF, pIn, nVars );
+    assert( Pla2Var[p] == v );
+}
+
+// moves vars to be the most signiticant ones (Group[0] is MSB)
+void If_CluMoveVars( word * pF, int * V2P, int * P2V, int nVars, int Group )
+{
+    int v;
+    for ( v = 0; v < 4; v++ )
+        If_CluMoveVarOneUp( pF, V2P, P2V, nVars, (Group >> (8*v)) & 0xFF, v );
+}
+
+// return the number of cofactors w.r.t. the topmost vars (nBSsize)
+int If_CluCountCofs( word * pF, int * V2P, int * P2V, int nVars, int nBSsize )
+{
+    int nShift = (1 << (nVars - nBSsize));
+    word Mask  = (((word)1) << nShift) - 1;
+    word iCofs[16], iCof;
+    int i, c, nMints = (1 << nBSsize), nCofs = 1;
+    assert( nBSsize >= 3 && nBSsize <= 5 );
+    assert( nVars - nBSsize >= 0 && nVars - nBSsize <= 6 );
+    if ( nVars - nBSsize == 6 )
+        Mask = ~0;
+    iCofs[0] = pF[0] & Mask;
+    for ( i = 1; i < nMints; i++ )
+    {
+        iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask;
+        for ( c = 0; c < nCofs; c++ )
+            if ( iCof == iCofs[c] )
+                break;
+        if ( c == nCofs )
+            iCofs[nCofs++] = iCof;
+        if ( nCofs == 5 )
+            break;
+    }
+    assert( nCofs >= 2 && nCofs <= 5 );
+    return nCofs;
+}
+
+// finds a good var group (cof count < 6; vars are MSBs)
+int If_CluFindGroup( word * pF, int * V2P, int * P2V, int nVars, int GroupEx )
+{
+/*
+    int i, Excl[10];
+    if ( GroupEx )
+    {
+        for ( i = 0; i < nVars; i++ )
+            Excl[i] = 0;
+        for ( i = 0; i < 4; i++ )
+            Excl[(GroupEx >> (8*i)) & 0xFF] = 1;
+    }
+*/
+    int nRounds = 3;
+    int GroupBest, nCofsBest;
+    int VarBest, nCofsBest2;
+    int i, r, v, nCofs;
+    assert( nVars > 4 );
+    // start with the default group
+    nCofsBest = If_CluCountCofs( pF, V2P, P2V, nVars, 4 );
+    GroupBest = 0;
+    for ( i = 0; i < 4; i++ )
+        GroupBest |= ( P2V[i] << (8*i) );
+    // try to find better group
+    for ( r = 0; r < nRounds && nCofsBest > 2; r++ )
+    {
+        // find the best var to add
+        VarBest = P2V[4];
+        nCofsBest2 = If_CluCountCofs( pF, V2P, P2V, nVars, 5 );
+        for ( v = 5; v < nVars; v++ )
+        {
+            If_CluMoveVarOneUp( pF, V2P, P2V, nVars, P2V[v], 4 );
+            nCofs = If_CluCountCofs( pF, V2P, P2V, nVars, 5 );
+            if ( nCofsBest2 > nCofs )
+            {
+                nCofsBest2 = nCofs;
+                VarBest = P2V[4];
+            }
+        }
+        // go back
+        If_CluMoveVarOneUp( pF, V2P, P2V, nVars, VarBest, 4 );
+
+        // find the best var to remove
+        VarBest = P2V[4];
+        nCofsBest2 = If_CluCountCofs( pF, V2P, P2V, nVars, 4 );
+        for ( v = 3; v >= 0; v-- )
+        {
+            If_CluMoveVarOneDown( pF, V2P, P2V, nVars, v, 4 );
+            nCofs = If_CluCountCofs( pF, V2P, P2V, nVars, 4 );
+            if ( nCofsBest2 > nCofs )
+            {
+                nCofsBest2 = nCofs;
+                VarBest = P2V[4];
+            }
+        }
+        // go back
+        If_CluMoveVarOneDown( pF, V2P, P2V, nVars, VarBest, 4 );
+
+        // update best bound set
+        nCofs = If_CluCountCofs( pF, V2P, P2V, nVars, 4 );
+        assert( nCofs == nCofsBest2 );
+        if ( nCofsBest > nCofs )
+        {
+            nCofsBest = nCofs;
+            for ( i = 0; i < 4; i++ )
+                GroupBest |= ( P2V[i] << (8*i) );
+        }
+    }
+    if ( nCofsBest <= 4 )
+        return GroupBest;
+    assert( r == nRounds );
+    return 0;
+}
+
+static inline int If_CluSuppIsMinBase( int Supp )
+{
+    return (Supp & (Supp+1)) == 0;
+}
+static inline int If_CluHasVar( word * t, int nVars, int iVar )
+{
+    int nWords = If_CluWordNum( nVars );
+    assert( iVar < nVars );
+    if ( iVar < 6 )
+    {
+        int i, Shift = (1 << iVar);
+        for ( i = 0; i < nWords; i++ )
+            if ( (t[i] & ~Truth6[iVar]) != ((t[i] & Truth6[iVar]) >> Shift) )
+                return 1;
+        return 0;
+    }
+    else
+    {
+        int i, k, Step = (1 << (iVar - 6));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+                if ( t[i] != t[Step+i] )
+                    return 1;
+            t += 2*Step;
+        }
+        return 0;
+    }
+}
+static inline int If_CluSupport( word * t, int nVars )
+{
+    int v, Supp = 0;
+    for ( v = 0; v < nVars; v++ )
+        if ( If_CluHasVar( t, nVars, v ) )
+            Supp |= (1 << v);
+    return Supp;
+}
+
+
+
+// returns the number of nodes and conf bits in vConf
+int If_CluCheck( word * pTruth, int nVars, Vec_Int_t * vConf )
+{
+    int fDerive = 0;
+    int V2P[10], P2V[10];
+    int i, nSupp, nNodes, Group1, Group2, nCofs1, nCofs2;
+    word pF[16];
+    assert( nVars <= 10 );
+    if ( nVars <= 5 )
+        return 1;
+
+    // check minnimum base
+    If_CluCopy( pF, pTruth, nVars );
+    nSupp = If_CluSupport( pF, nVars );
+    if ( !nSupp || !If_CluSuppIsMinBase(nSupp) )
+        return 0;
+
+    // perform testing
+    for ( i = 0; i < nVars; i++ )
+        V2P[i] = P2V[i] = i;
+    Group1 = If_CluFindGroup( pF, V2P, P2V, nVars, 0 );
+    if ( Group1 == 0 )
+        return 0;
+    nCofs1 = If_CluCountCofs( pF, V2P, P2V, nVars, 4 );
+    assert( nCofs1 >= 2 && nCofs1 <= 4 );
+    if ( nVars <= 6 )
+        return 1;
+    if ( nCofs1 == 2 && nVars == 7 )
+        return 1;
+    if ( nCofs1 > 2 && nVars == 10 )
+        return 0;
+
+    // perform testing
+    Group2 = If_CluFindGroup( pF, V2P, P2V, nVars, Group1 );
+    if ( Group2 == 0 )
+        return 0;
+    nCofs2 = If_CluCountCofs( pF, V2P, P2V, nVars, 4 );
+    assert( nCofs2 >= 2 && nCofs2 <= 4 );
+    if ( nVars - 6 + (nCofs1 > 2) + (nCofs2 > 2) <= 4 )
+        return 1;
+    return 0;
+
+    // compute conf bits
+
+    return nNodes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index f2dbe3f7..fb8e763c 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -105,7 +105,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         else if ( Mode == 1 )
             pObj->EstRefs = (float)((2.0 * pObj->EstRefs + pObj->nRefs) / 3.0);
     }
-
+/*
     // process special cut
     if ( p->pDriverCuts && p->pDriverCuts[pObj->Id] )
     {
@@ -137,7 +137,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         assert( pCutSet->nCuts == 2 );
         return;
     }
-
+*/
     // deref the selected cut
     if ( Mode && pObj->nRefs > 0 )
         If_CutAreaDeref( p, If_ObjCutBest(pObj) );
@@ -153,7 +153,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         if ( p->pPars->fDelayOpt )
             pCut->Delay = If_CutDelaySopCost( p, pCut );
         else
-            pCut->Delay = If_CutDelay( p, pCut );
+            pCut->Delay = If_CutDelay( p, pObj, pCut );
 //        assert( pCut->Delay <= pObj->Required + p->fEpsilon );
         if ( pCut->Delay > pObj->Required + 2*p->fEpsilon )
             Abc_Print( 1, "If_ObjPerformMappingAnd(): Warning! Delay of node %d (%f) exceeds the required times (%f).\n", 
@@ -215,7 +215,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         if ( p->pPars->fDelayOpt )
             pCut->Delay = If_CutDelaySopCost( p, pCut );
         else
-            pCut->Delay = If_CutDelay( p, pCut );
+            pCut->Delay = If_CutDelay( p, pObj, pCut );
 //        Abc_Print( 1, "%.2f ", pCut->Delay );
         if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
             continue;
@@ -305,7 +305,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
             if ( If_CutFilter( pCutSet, pCut ) )
                 continue;
             // check if the cut satisfies the required times
-            assert( pCut->Delay == If_CutDelay( p, pCut ) );
+            assert( pCut->Delay == If_CutDelay( p, pObj, pCut ) );
             if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
                 continue;
             // set the phase attribute
diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c
index 622688e7..b45a9b25 100644
--- a/src/map/if/ifReduce.c
+++ b/src/map/if/ifReduce.c
@@ -153,7 +153,7 @@ void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr
     int CostBef, CostAft, i;
     float DelayOld, AreaBef, AreaAft;
     pCut = If_ObjCutBest(pObj);
-    pCut->Delay = If_CutDelay( p, pCut );
+    pCut->Delay = If_CutDelay( p, pObj, pCut );
     assert( pCut->Delay <= pObj->Required + p->fEpsilon );
     if ( pObj->nRefs == 0 )
         return;
@@ -177,7 +177,7 @@ void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr
         pFanin->fMark = 0;
     // update the node
     If_ManImproveNodeUpdate( p, pObj, vFront );
-    pCut->Delay = If_CutDelay( p, pCut );
+    pCut->Delay = If_CutDelay( p, pObj, pCut );
     // get the new area
     AreaAft = If_CutAreaRefed( p, pCut );
     if ( AreaAft > AreaBef || pCut->Delay > pObj->Required + p->fEpsilon )
@@ -539,14 +539,14 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
     }
     if ( RetValue )
     {
-        pCutR->Delay = If_CutDelay( p, pCutR );
+        pCutR->Delay = If_CutDelay( p, pObj, pCutR );
         AreaAft = If_CutAreaDerefed( p, pCutR );
         // update the best cut
         if ( AreaAft < AreaBef - p->fEpsilon && pCutR->Delay < pObj->Required + p->fEpsilon )
             If_CutCopy( p, pCut, pCutR );
     }
     // recompute the delay of the best cut
-    pCut->Delay = If_CutDelay( p, pCut );
+    pCut->Delay = If_CutDelay( p, pObj, pCut );
     // ref the cut if the node is refed
     if ( pObj->nRefs > 0 )
         If_CutRef( p, pCut );
diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c
index e6cf99d5..5dd57efc 100644
--- a/src/map/if/ifTime.c
+++ b/src/map/if/ifTime.c
@@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START
 
 #define IF_BIG_CHAR 120
 
+static float s_ExtraDel[2][3] = { {1.0, 1.0, 1.0}, {1.0, 1.0, 0.0} };
+
 static void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float * pPinDelays );
 
 ////////////////////////////////////////////////////////////////////////
@@ -386,7 +388,7 @@ int If_CutDelaySopCost( If_Man_t * p, If_Cut_t * pCut )
     }
 //    Vec_WrdFree( vAnds );
     // verify the delay
-//    Delay = If_CutDelay( p, pCut );
+//    Delay = If_CutDelay( p, pObj, pCut );
 //    assert( (int)Leaf.Delay == Delay );
     return Leaf.Delay;
 }
@@ -407,14 +409,14 @@ int If_CutDelaySopCost( If_Man_t * p, If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-float If_CutDelay( If_Man_t * p, If_Cut_t * pCut )
+float If_CutDelay( If_Man_t * p, If_Obj_t * pObj, 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, Shift, Pin2PinDelay;
+    int i, Shift, Pin2PinDelay, iLeaf;
     assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
     Delay = -IF_FLOAT_LARGE;
     if ( p->pPars->pLutLib )
@@ -435,7 +437,10 @@ float If_CutDelay( If_Man_t * p, If_Cut_t * pCut )
         {
             If_CutForEachLeaf( p, pCut, pLeaf, i )
             {
-                DelayCur = If_ObjCutBest(pLeaf)->Delay + pLutDelays[0];
+                if ( p->pDriverCuts && p->pDriverCuts[pObj->Id] && (iLeaf = Vec_IntFind(p->pDriverCuts[pObj->Id], pLeaf->Id)) >= 0 )
+                    DelayCur = If_ObjCutBest(pLeaf)->Delay + s_ExtraDel[pObj->fDriver][iLeaf];
+                else
+                    DelayCur = If_ObjCutBest(pLeaf)->Delay + pLutDelays[0];
                 Delay = IF_MAX( Delay, DelayCur );
             }
         }
@@ -459,18 +464,20 @@ float If_CutDelay( If_Man_t * p, If_Cut_t * pCut )
                 If_CutForEachLeafSeq( p, pCut, pLeaf, Shift, i )
                 {
                     DelayCur = If_ObjCutBest(pLeaf)->Delay - Shift * p->Period;
-                    Delay = IF_MAX( Delay, DelayCur );
+                    Delay = IF_MAX( Delay, DelayCur + 1.0 );
                 }
             }
             else
             {
                 If_CutForEachLeaf( p, pCut, pLeaf, i )
                 {
-                    DelayCur = If_ObjCutBest(pLeaf)->Delay;
+                    if ( p->pDriverCuts && p->pDriverCuts[pObj->Id] && (iLeaf = Vec_IntFind(p->pDriverCuts[pObj->Id], pLeaf->Id)) >= 0 )
+                        DelayCur = If_ObjCutBest(pLeaf)->Delay + ((pObj->fDriver && iLeaf == 2) ? 0.0 : 1.0);
+                    else
+                        DelayCur = If_ObjCutBest(pLeaf)->Delay + 1.0;
                     Delay = IF_MAX( Delay, DelayCur );
                 }
             }
-            Delay += 1.0;
         }
     }
     return Delay;
@@ -487,14 +494,14 @@ float If_CutDelay( If_Man_t * p, If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-void If_CutPropagateRequired( If_Man_t * p, If_Cut_t * pCut, float ObjRequired )
+void If_CutPropagateRequired( If_Man_t * p, If_Obj_t * pObj, 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, Pin2PinDelay;
+    int i, Pin2PinDelay, iLeaf;
     assert( !p->pPars->fLiftLeaves );
     // compute the pins
     if ( p->pPars->pLutLib )
@@ -513,9 +520,14 @@ void If_CutPropagateRequired( If_Man_t * p, If_Cut_t * pCut, float ObjRequired )
         }
         else
         {
-            Required = ObjRequired - pLutDelays[0];
+            Required = ObjRequired;
             If_CutForEachLeaf( p, pCut, pLeaf, i )
-                pLeaf->Required = IF_MIN( pLeaf->Required, Required );
+            {
+                if ( p->pDriverCuts && p->pDriverCuts[pObj->Id] && (iLeaf = Vec_IntFind(p->pDriverCuts[pObj->Id], pLeaf->Id)) >= 0 )
+                    pLeaf->Required = IF_MIN( pLeaf->Required, Required - s_ExtraDel[pObj->fDriver][iLeaf] );
+                else
+                    pLeaf->Required = IF_MIN( pLeaf->Required, Required - pLutDelays[0] );
+            }
         }
     }
     else
@@ -531,9 +543,14 @@ void If_CutPropagateRequired( If_Man_t * p, If_Cut_t * pCut, float ObjRequired )
         }
         else
         {
-            Required = ObjRequired - (float)1.0;
+            Required = ObjRequired;
             If_CutForEachLeaf( p, pCut, pLeaf, i )
-                pLeaf->Required = IF_MIN( pLeaf->Required, Required );
+            {
+                if ( p->pDriverCuts && p->pDriverCuts[pObj->Id] && (iLeaf = Vec_IntFind(p->pDriverCuts[pObj->Id], pLeaf->Id)) >= 0 )
+                    pLeaf->Required = IF_MIN( pLeaf->Required, Required - (float)((pObj->fDriver && iLeaf == 2) ? 0.0 : 1.0) );
+                else
+                    pLeaf->Required = IF_MIN( pLeaf->Required, Required - (float)1.0 );
+            }
         }
     }
 }
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index 5adf96fb..fe3bf8fc 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -344,6 +344,8 @@ static inline unsigned If_CutTruthPhase( If_Cut_t * pCut, If_Cut_t * pCut1 )
     return uPhase;
 }
 
+//static FILE * pTruths;
+
 /**Function*************************************************************
 
   Synopsis    [Performs truth table computation.]
@@ -377,7 +379,15 @@ int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_
         If_TruthNand( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
     else
         If_TruthAnd( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
-
+/*
+    if ( pCut->nLeaves == 5 )
+    {
+        if ( pTruths == NULL )
+            pTruths = fopen( "fun5var.txt", "w" );
+        Extra_PrintHex( pTruths, If_CutTruth(pCut), pCut->nLeaves );
+        fprintf( pTruths, "\n" );
+    }
+*/
     // minimize the support of the cut
     if ( p->pPars->fCutMin )
         return If_CutTruthMinimize( p, pCut );
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index f752baef..b1ec7169 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -223,12 +223,12 @@ void If_ManComputeRequired( If_Man_t * p )
         }
         // go through the nodes in the reverse topological order
     //    Vec_PtrForEachEntry( If_Obj_t *, p->vMapped, pObj, i )
-    //        If_CutPropagateRequired( p, If_ObjCutBest(pObj), pObj->Required );
+    //        If_CutPropagateRequired( p, pObj, If_ObjCutBest(pObj), pObj->Required );
         If_ManForEachObjReverse( p, pObj, i )
         {
             if ( pObj->nRefs == 0 )
                 continue;
-            If_CutPropagateRequired( p, If_ObjCutBest(pObj), pObj->Required );
+            If_CutPropagateRequired( p, pObj, If_ObjCutBest(pObj), pObj->Required );
         }
     }
     else
@@ -298,7 +298,7 @@ void If_ManComputeRequired( If_Man_t * p )
             {
                 if ( pObj->nRefs == 0 )
                     continue;
-                If_CutPropagateRequired( p, If_ObjCutBest(pObj), pObj->Required );
+                If_CutPropagateRequired( p, pObj, If_ObjCutBest(pObj), pObj->Required );
             }
             else if ( If_ObjIsCi(pObj) )
             {