Implementation of DSD balancing.

9 files changed, 586 insertions, 583 deletions

diff --git a/abclib.dsp b/abclib.dsp
index e1cc7062..f3d810c3 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -2323,6 +2323,10 @@ SOURCE=.\src\map\if\ifCore.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\map\if\ifCount.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\map\if\ifCut.c
 # End Source File
 # Begin Source File
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2e2c4e73..397cee76 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -15102,7 +15102,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->fTruth      =  1;
         pPars->fCutMin     =  1;
         pPars->fExpRed     =  0;
-        pPars->fUsePerm    =  0;
+        pPars->fUsePerm    =  pPars->fDsdBalance;
+        pPars->fUseDsd     =  pPars->fDsdBalance;
         pPars->pLutLib     =  NULL;
     }
     // modify for delay optimization
@@ -29855,7 +29856,8 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->fTruth      =  1;
         pPars->fCutMin     =  1;
         pPars->fExpRed     =  0;
-        pPars->fUsePerm    =  0;
+        pPars->fUsePerm    =  pPars->fDsdBalance;
+        pPars->fUseDsd     =  pPars->fDsdBalance;
         pPars->pLutLib     =  NULL;
     }
     // modify for delay optimization
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 0e86ff2b..b4d98598 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -540,7 +540,7 @@ extern int             If_DsdManLutSize( If_DsdMan_t * p );
 extern int             If_DsdManSuppSize( If_DsdMan_t * p, int iDsd );
 extern int             If_DsdManCheckDec( If_DsdMan_t * p, int iDsd );
 extern unsigned        If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fHighEffort, int fVerbose );
-extern int             If_CutDsdBalanceEval( If_Man_t * pIfMan, If_Cut_t * pCut, Vec_Int_t * vAig );
+extern int             If_CutDsdBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig );
 extern int             If_CutDsdBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm );
 /*=== ifLib.c =============================================================*/
 extern If_LibLut_t *   If_LibLutRead( char * FileName );
diff --git a/src/map/if/ifCount.h b/src/map/if/ifCount.h
new file mode 100644
index 00000000..478f1e9a
--- /dev/null
+++ b/src/map/if/ifCount.h
@@ -0,0 +1,490 @@
+/**CFile****************************************************************
+
+  FileName    [ifCount.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapping based on priority cuts.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 21, 2006.]
+
+  Revision    [$Id: ifCount.h,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__map__if__if_Count_h
+#define ABC__map__if__if_Count_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_LogCreateAnd( Vec_Int_t * vAig, int iLit0, int iLit1, int nSuppAll )
+{
+    int iObjId = Vec_IntSize(vAig)/2 + nSuppAll;
+    Vec_IntPush( vAig, iLit0 );
+    Vec_IntPush( vAig, iLit1 );
+    return Abc_Var2Lit( iObjId, 0 );
+}
+static inline int If_LogCreateMux( Vec_Int_t * vAig, int iLitC, int iLit1, int iLit0, int nSuppAll )
+{
+    int iFanLit0 = If_LogCreateAnd( vAig, iLitC, iLit1, nSuppAll );
+    int iFanLit1 = If_LogCreateAnd( vAig, Abc_LitNot(iLitC), iLit0, nSuppAll );
+    int iResLit  = If_LogCreateAnd( vAig, Abc_LitNot(iFanLit0), Abc_LitNot(iFanLit1), nSuppAll );
+    return Abc_LitNot(iResLit);
+}
+static inline int If_LogCreateXor( Vec_Int_t * vAig, int iLit0, int iLit1, int nSuppAll )
+{
+    return If_LogCreateMux( vAig, iLit0, Abc_LitNot(iLit1), iLit1, nSuppAll );
+}
+static inline int If_LogCreateAndXor( Vec_Int_t * vAig, int iLit0, int iLit1, int nSuppAll, int fXor )
+{
+    return fXor ? If_LogCreateXor(vAig, iLit0, iLit1, nSuppAll) : If_LogCreateAnd(vAig, iLit0, iLit1, nSuppAll);
+}
+static inline int If_LogCreateAndXorMulti( Vec_Int_t * vAig, int * pFaninLits, int nFanins, int nSuppAll, int fXor )
+{
+    int i;
+    assert( nFanins > 0 );
+    for ( i = nFanins - 1; i > 0; i-- )
+        pFaninLits[i-1] = If_LogCreateAndXor( vAig, pFaninLits[i], pFaninLits[i-1], nSuppAll, fXor );
+    return pFaninLits[0];
+}
+static inline int If_LogCounterAddAig( int * pTimes, int * pnTimes, int * pFaninLits, int Num, int iLit, Vec_Int_t * vAig, int nSuppAll, int fXor )
+{
+    int nTimes = *pnTimes;
+    if ( vAig )
+        pFaninLits[nTimes] = iLit;
+    pTimes[nTimes++] = Num;
+    if ( nTimes > 1 )
+    {
+        int i, k;
+        for ( k = nTimes-1; k > 0; k-- )
+        {
+            if ( pTimes[k] < pTimes[k-1] )
+                break;
+            if ( pTimes[k] > pTimes[k-1] )
+            { 
+                ABC_SWAP( int, pTimes[k], pTimes[k-1] ); 
+                if ( vAig )
+                    ABC_SWAP( int, pFaninLits[k], pFaninLits[k-1] ); 
+                continue; 
+            }
+            pTimes[k-1] += 1 + fXor;
+            if ( vAig )
+                pFaninLits[k-1] = If_LogCreateAndXor( vAig, pFaninLits[k], pFaninLits[k-1], nSuppAll, fXor );
+            for ( nTimes--, i = k; i < nTimes; i++ )
+            {
+                pTimes[i] = pTimes[i+1];
+                if ( vAig )
+                    pFaninLits[i] = pFaninLits[i+1];
+            }
+        }
+    }
+    assert( nTimes > 0 );
+    *pnTimes = nTimes;
+    return pTimes[0] + (nTimes > 1 ? 1 + fXor : 0);
+}
+static inline int If_LogCounterDelayXor( int * pTimes, int nTimes )
+{
+    int i;
+    assert( nTimes > 0 );
+    for ( i = nTimes - 1; i > 0; i-- )
+        pTimes[i-1] = 2 + Abc_MaxInt( pTimes[i], pTimes[i-1] );
+    return pTimes[0];
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Compute delay/area profile of the structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int  If_CutPinDelayGet( word D, int v )           { assert(v >= 0 && v < IF_MAX_FUNC_LUTSIZE); return (int)((D >> (v << 2)) & 0xF);                             }
+static inline void If_CutPinDelaySet( word * pD, int v, int d ) { assert(v >= 0 && v < IF_MAX_FUNC_LUTSIZE); assert(d >= 0 && d < IF_MAX_FUNC_LUTSIZE); *pD |= ((word)d << (v << 2)); }
+static inline word If_CutPinDelayInit( int v )                  { assert(v >= 0 && v < IF_MAX_FUNC_LUTSIZE); return (word)1 << (v << 2);                                      }
+static inline word If_CutPinDelayMax( word D1, word D2, int nVars, int AddOn )
+{
+    int v, Max;
+    word D = 0;
+    for ( v = 0; v < nVars; v++ )
+        if ( (Max = Abc_MaxInt(If_CutPinDelayGet(D1, v), If_CutPinDelayGet(D2, v))) )
+            If_CutPinDelaySet( &D, v, Abc_MinInt(Max + AddOn, 15) );
+    return D;
+}
+static inline word If_CutPinDelayDecrement( word D1, int nVars )
+{
+    int v;
+    word D = 0;
+    for ( v = 0; v < nVars; v++ )
+        if ( If_CutPinDelayGet(D1, v) )
+            If_CutPinDelaySet( &D, v, If_CutPinDelayGet(D1, v) - 1 );
+    return D;
+}
+static inline int If_CutPinDelayEqual( word D1, word D2, int nVars ) // returns 1 if D1 has the same delays than D2
+{
+    int v;
+    for ( v = 0; v < nVars; v++ )
+        if ( If_CutPinDelayGet(D1, v) != If_CutPinDelayGet(D2, v) )
+            return 0;
+    return 1;
+}
+static inline int If_CutPinDelayDom( word D1, word D2, int nVars ) // returns 1 if D1 has the same or smaller delays than D2
+{
+    int v;
+    for ( v = 0; v < nVars; v++ )
+        if ( If_CutPinDelayGet(D1, v) > If_CutPinDelayGet(D2, v) )
+            return 0;
+    return 1;
+}
+static inline void If_CutPinDelayTranslate( word D, int nVars, char * pPerm ) 
+{
+    int v, Delay;
+    for ( v = 0; v < nVars; v++ )
+    {
+        Delay = If_CutPinDelayGet(D, v);
+        assert( Delay > 1 );
+        pPerm[v] = Delay - 1;
+    }
+}
+static inline void If_CutPinDelayPrint( word D, int nVars )
+{
+    int v;
+    printf( "Delay profile = {" );
+    for ( v = 0; v < nVars; v++ )
+        printf( " %d", If_CutPinDelayGet(D, v) );
+    printf( " }\n" );
+}
+static inline int If_LogCounterPinDelays( int * pTimes, int * pnTimes, word * pPinDels, int Num, word PinDel, int nSuppAll, int fXor )
+{
+    int nTimes = *pnTimes;
+    pPinDels[nTimes] = PinDel;
+    pTimes[nTimes++] = Num;
+    if ( nTimes > 1 )
+    {
+        int i, k;
+        for ( k = nTimes-1; k > 0; k-- )
+        {
+            if ( pTimes[k] < pTimes[k-1] )
+                break;
+            if ( pTimes[k] > pTimes[k-1] )
+            { 
+                ABC_SWAP( int, pTimes[k], pTimes[k-1] ); 
+                ABC_SWAP( word, pPinDels[k], pPinDels[k-1] ); 
+                continue; 
+            }
+            pTimes[k-1] += 1 + fXor;
+            pPinDels[k-1] = If_CutPinDelayMax( pPinDels[k], pPinDels[k-1], nSuppAll, 1 + fXor );
+            for ( nTimes--, i = k; i < nTimes; i++ )
+            {
+                pTimes[i] = pTimes[i+1];
+                pPinDels[i] = pPinDels[i+1];
+            }
+        }
+    }
+    assert( nTimes > 0 );
+    *pnTimes = nTimes;
+    return pTimes[0] + (nTimes > 1 ? 1 + fXor : 0);
+}
+static inline word If_LogPinDelaysMulti( word * pPinDels, int nFanins, int nSuppAll, int fXor )
+{
+    int i;
+    assert( nFanins > 0 );
+    for ( i = nFanins - 1; i > 0; i-- )
+        pPinDels[i-1] = If_CutPinDelayMax( pPinDels[i], pPinDels[i-1], nSuppAll, 1 + fXor );
+    return pPinDels[0];
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline word If_AigVerifyArray( Vec_Int_t * vAig, int nLeaves )
+{
+    assert( Vec_IntSize(vAig) > 0 );
+    assert( Vec_IntEntryLast(vAig) < 2 );
+    if ( Vec_IntSize(vAig) == 1 ) // const
+        return Vec_IntEntry(vAig, 0) ? ~((word)0) : 0;
+    if ( Vec_IntSize(vAig) == 2 ) // variable
+    {
+        assert( Vec_IntEntry(vAig, 0) == 0 );
+        return Vec_IntEntry(vAig, 1) ? ~s_Truths6[0] : s_Truths6[0];
+    }
+    else
+    {
+        word Truth0 = 0, Truth1 = 0, TruthR;
+        int i, iVar0, iVar1, iLit0, iLit1;
+        assert( Vec_IntSize(vAig) & 1 );
+        Vec_IntForEachEntryDouble( vAig, iLit0, iLit1, i )
+        {
+            iVar0 = Abc_Lit2Var( iLit0 );
+            iVar1 = Abc_Lit2Var( iLit1 );
+            Truth0 = iVar0 < nLeaves ? s_Truths6[iVar0] : Vec_WrdEntry( (Vec_Wrd_t *)vAig, iVar0 - nLeaves );
+            Truth1 = iVar1 < nLeaves ? s_Truths6[iVar1] : Vec_WrdEntry( (Vec_Wrd_t *)vAig, iVar1 - nLeaves );
+            if ( Abc_LitIsCompl(iLit0) )
+                Truth0 = ~Truth0;
+            if ( Abc_LitIsCompl(iLit1) )
+                Truth1 = ~Truth1;
+            assert( (i & 1) == 0 );
+            Vec_WrdWriteEntry( (Vec_Wrd_t *)vAig, Abc_Lit2Var(i), Truth0 & Truth1 );  // overwriting entries
+        }
+        assert( i == Vec_IntSize(vAig) - 1 );
+        TruthR = Truth0 & Truth1;
+        if ( Vec_IntEntry(vAig, i) )
+            TruthR = ~TruthR;
+        Vec_IntClear( vAig ); // useless
+        return TruthR;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Naive implementation of log-counter.]
+
+  Description [Incrementally computes [log2(SUMi(2^di)).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_LogCounter64Eval( word Count )
+{
+    int n = ((Count & (Count - 1)) > 0) ? -1 : 0;
+    assert( Count > 0 );
+    if ( (Count & ABC_CONST(0xFFFFFFFF00000000)) == 0 ) { n += 32; Count <<= 32; }
+    if ( (Count & ABC_CONST(0xFFFF000000000000)) == 0 ) { n += 16; Count <<= 16; }
+    if ( (Count & ABC_CONST(0xFF00000000000000)) == 0 ) { n +=  8; Count <<=  8; }
+    if ( (Count & ABC_CONST(0xF000000000000000)) == 0 ) { n +=  4; Count <<=  4; }
+    if ( (Count & ABC_CONST(0xC000000000000000)) == 0 ) { n +=  2; Count <<=  2; }
+    if ( (Count & ABC_CONST(0x8000000000000000)) == 0 ) { n++; }
+    return 63 - n;
+}
+static word If_LogCounter64Add( word Count, int Num )
+{
+    assert( Num < 48 );
+    return Count + (((word)1) << Num);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implementation of log-counter.]
+
+  Description [Incrementally computes [log2(SUMi(2^di)).
+  Supposed to work correctly up to 16 entries.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int If_LogCounter32Eval( unsigned Count, int Start )
+{
+    int n = (Abc_LitIsCompl(Start) || (Count & (Count - 1)) > 0) ? -1 : 0;
+    assert( Count > 0 );
+    if ( (Count & 0xFFFF0000) == 0 ) { n += 16; Count <<= 16; }
+    if ( (Count & 0xFF000000) == 0 ) { n +=  8; Count <<=  8; }
+    if ( (Count & 0xF0000000) == 0 ) { n +=  4; Count <<=  4; }
+    if ( (Count & 0xC0000000) == 0 ) { n +=  2; Count <<=  2; }
+    if ( (Count & 0x80000000) == 0 ) { n++; }
+    return Abc_Lit2Var(Start) + 31 - n;
+}
+static unsigned If_LogCounter32Add( unsigned Count, int * pStart, int Num )
+{
+    int Start = Abc_Lit2Var(*pStart);
+    if ( Num < Start )
+    {
+        *pStart |= 1;
+        return Count;
+    }
+    if ( Num > Start + 16 )
+    {
+        int Shift = Num - (Start + 16);
+        if ( !Abc_LitIsCompl(*pStart) && (Shift >= 32 ? Count : Count & ~(~0 << Shift)) > 0 )
+            *pStart |= 1;
+        Count >>= Shift;
+        Start += Shift;
+        *pStart = Abc_Var2Lit( Start, Abc_LitIsCompl(*pStart) );
+        assert( Num <= Start + 16 );
+    }
+    return Count + (1 << (Num-Start));
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testing of the counter]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+void If_LogCounterTest2()
+{
+    word Count64 = 0;
+
+    unsigned Count = 0; 
+    int Start = 0;
+
+    int Result, Result64;
+
+    Count = If_LogCounter32Add( Count, &Start, 39 );
+    Count = If_LogCounter32Add( Count, &Start, 35 );
+    Count = If_LogCounter32Add( Count, &Start, 35 );
+    Count = If_LogCounter32Add( Count, &Start, 36 );
+    Count = If_LogCounter32Add( Count, &Start, 37 );
+    Count = If_LogCounter32Add( Count, &Start, 38 );
+    Count = If_LogCounter32Add( Count, &Start, 40 );
+    Count = If_LogCounter32Add( Count, &Start, 1 );
+    Count = If_LogCounter32Add( Count, &Start, 41 );
+    Count = If_LogCounter32Add( Count, &Start, 42 );
+
+    Count64 = If_LogCounter64Add( Count64, 1 );
+    Count64 = If_LogCounter64Add( Count64, 35 );
+    Count64 = If_LogCounter64Add( Count64, 35 );
+    Count64 = If_LogCounter64Add( Count64, 36 );
+    Count64 = If_LogCounter64Add( Count64, 37 );
+    Count64 = If_LogCounter64Add( Count64, 38 );
+    Count64 = If_LogCounter64Add( Count64, 39 );
+    Count64 = If_LogCounter64Add( Count64, 40 );
+    Count64 = If_LogCounter64Add( Count64, 41 );
+    Count64 = If_LogCounter64Add( Count64, 42 );
+
+    Result = If_LogCounter32Eval( Count, Start );
+    Result64 = If_LogCounter64Eval( Count64 );
+
+    printf( "%d  %d\n", Result, Result64 );
+}
+*/
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the number to the numbers stored.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_LogCounterAdd( int * pTimes, int * pnTimes, int Num, int fXor )
+{
+    int nTimes = *pnTimes;
+    pTimes[nTimes++] = Num;
+    if ( nTimes > 1 )
+    {
+        int i, k;
+        for ( k = nTimes-1; k > 0; k-- )
+        {
+            if ( pTimes[k] < pTimes[k-1] )
+                break;
+            if ( pTimes[k] > pTimes[k-1] )
+            { 
+                ABC_SWAP( int, pTimes[k], pTimes[k-1] ); 
+                continue; 
+            }
+            pTimes[k-1] += 1 + fXor;
+            for ( nTimes--, i = k; i < nTimes; i++ )
+                pTimes[i] = pTimes[i+1];
+        }
+    }
+    assert( nTimes > 0 );
+    *pnTimes = nTimes;
+    return pTimes[0] + (nTimes > 1 ? 1 + fXor : 0);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testing of the counter]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+void If_LogCounterTest()
+{
+    int pArray[10] = { 1, 2, 4, 5, 6, 3, 1 };
+    int i, nSize = 4;
+
+    word Count64 = 0;
+    int Result, Result64;
+
+    int pTimes[100];
+    int nTimes = 0;
+
+    for ( i = 0; i < nSize; i++ )
+        Count64 = If_LogCounter64Add( Count64, pArray[i] );
+    Result64 = If_LogCounter64Eval( Count64 );
+
+    for ( i = 0; i < nSize; i++ )
+        Result = If_LogCounterAdd( pTimes, &nTimes, pArray[i], 0 );
+
+    printf( "%d  %d\n", Result64, Result );
+}
+*/
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/map/if/ifDelay.c b/src/map/if/ifDelay.c
index 710941e6..9c5704b7 100644
--- a/src/map/if/ifDelay.c
+++ b/src/map/if/ifDelay.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "if.h"
+#include "ifCount.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -105,165 +106,7 @@ int If_CutDelaySop( If_Man_t * p, If_Cut_t * pCut )
 
 /**Function*************************************************************
 
-  Synopsis    [Naive implementation of log-counter.]
-
-  Description [Incrementally computes [log2(SUMi(2^di)).]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int If_LogCounter64Eval( word Count )
-{
-    int n = ((Count & (Count - 1)) > 0) ? -1 : 0;
-    assert( Count > 0 );
-    if ( (Count & ABC_CONST(0xFFFFFFFF00000000)) == 0 ) { n += 32; Count <<= 32; }
-    if ( (Count & ABC_CONST(0xFFFF000000000000)) == 0 ) { n += 16; Count <<= 16; }
-    if ( (Count & ABC_CONST(0xFF00000000000000)) == 0 ) { n +=  8; Count <<=  8; }
-    if ( (Count & ABC_CONST(0xF000000000000000)) == 0 ) { n +=  4; Count <<=  4; }
-    if ( (Count & ABC_CONST(0xC000000000000000)) == 0 ) { n +=  2; Count <<=  2; }
-    if ( (Count & ABC_CONST(0x8000000000000000)) == 0 ) { n++; }
-    return 63 - n;
-}
-static word If_LogCounter64Add( word Count, int Num )
-{
-    assert( Num < 48 );
-    return Count + (((word)1) << Num);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Implementation of log-counter.]
-
-  Description [Incrementally computes [log2(SUMi(2^di)).
-  Supposed to work correctly up to 16 entries.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static int If_LogCounter32Eval( unsigned Count, int Start )
-{
-    int n = (Abc_LitIsCompl(Start) || (Count & (Count - 1)) > 0) ? -1 : 0;
-    assert( Count > 0 );
-    if ( (Count & 0xFFFF0000) == 0 ) { n += 16; Count <<= 16; }
-    if ( (Count & 0xFF000000) == 0 ) { n +=  8; Count <<=  8; }
-    if ( (Count & 0xF0000000) == 0 ) { n +=  4; Count <<=  4; }
-    if ( (Count & 0xC0000000) == 0 ) { n +=  2; Count <<=  2; }
-    if ( (Count & 0x80000000) == 0 ) { n++; }
-    return Abc_Lit2Var(Start) + 31 - n;
-}
-static unsigned If_LogCounter32Add( unsigned Count, int * pStart, int Num )
-{
-    int Start = Abc_Lit2Var(*pStart);
-    if ( Num < Start )
-    {
-        *pStart |= 1;
-        return Count;
-    }
-    if ( Num > Start + 16 )
-    {
-        int Shift = Num - (Start + 16);
-        if ( !Abc_LitIsCompl(*pStart) && (Shift >= 32 ? Count : Count & ~(~0 << Shift)) > 0 )
-            *pStart |= 1;
-        Count >>= Shift;
-        Start += Shift;
-        *pStart = Abc_Var2Lit( Start, Abc_LitIsCompl(*pStart) );
-        assert( Num <= Start + 16 );
-    }
-    return Count + (1 << (Num-Start));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Testing of the counter]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void If_LogCounterTest2()
-{
-    word Count64 = 0;
-
-    unsigned Count = 0; 
-    int Start = 0;
-
-    int Result, Result64;
-
-    Count = If_LogCounter32Add( Count, &Start, 39 );
-    Count = If_LogCounter32Add( Count, &Start, 35 );
-    Count = If_LogCounter32Add( Count, &Start, 35 );
-    Count = If_LogCounter32Add( Count, &Start, 36 );
-    Count = If_LogCounter32Add( Count, &Start, 37 );
-    Count = If_LogCounter32Add( Count, &Start, 38 );
-    Count = If_LogCounter32Add( Count, &Start, 40 );
-    Count = If_LogCounter32Add( Count, &Start, 1 );
-    Count = If_LogCounter32Add( Count, &Start, 41 );
-    Count = If_LogCounter32Add( Count, &Start, 42 );
-
-    Count64 = If_LogCounter64Add( Count64, 1 );
-    Count64 = If_LogCounter64Add( Count64, 35 );
-    Count64 = If_LogCounter64Add( Count64, 35 );
-    Count64 = If_LogCounter64Add( Count64, 36 );
-    Count64 = If_LogCounter64Add( Count64, 37 );
-    Count64 = If_LogCounter64Add( Count64, 38 );
-    Count64 = If_LogCounter64Add( Count64, 39 );
-    Count64 = If_LogCounter64Add( Count64, 40 );
-    Count64 = If_LogCounter64Add( Count64, 41 );
-    Count64 = If_LogCounter64Add( Count64, 42 );
-
-    Result = If_LogCounter32Eval( Count, Start );
-    Result64 = If_LogCounter64Eval( Count64 );
-
-    printf( "%d  %d\n", Result, Result64 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the number to the numbers stored.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int If_LogCounterAdd( int * pTimes, int * pnTimes, int Num, int fXor )
-{
-    int nTimes = *pnTimes;
-    pTimes[nTimes++] = Num;
-    if ( nTimes > 1 )
-    {
-        int i, k;
-        for ( k = nTimes-1; k > 0; k-- )
-        {
-            if ( pTimes[k] < pTimes[k-1] )
-                break;
-            if ( pTimes[k] > pTimes[k-1] )
-            { 
-                ABC_SWAP( int, pTimes[k], pTimes[k-1] ); 
-                continue; 
-            }
-            pTimes[k-1] += 1 + fXor;
-            for ( nTimes--, i = k; i < nTimes; i++ )
-                pTimes[i] = pTimes[i+1];
-        }
-    }
-    assert( nTimes > 0 );
-    *pnTimes = nTimes;
-    return pTimes[0] + (nTimes > 1 ? 1 + fXor : 0);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Testing of the counter]
+  Synopsis    [Compute pin delays.]
 
   Description []
                
@@ -272,259 +115,6 @@ static inline int If_LogCounterAdd( int * pTimes, int * pnTimes, int Num, int fX
   SeeAlso     []
 
 ***********************************************************************/
-void If_LogCounterTest()
-{
-    int pArray[10] = { 1, 2, 4, 5, 6, 3, 1 };
-    int i, nSize = 4;
-
-    word Count64 = 0;
-    int Result, Result64;
-
-    int pTimes[100];
-    int nTimes = 0;
-
-    for ( i = 0; i < nSize; i++ )
-        Count64 = If_LogCounter64Add( Count64, pArray[i] );
-    Result64 = If_LogCounter64Eval( Count64 );
-
-    for ( i = 0; i < nSize; i++ )
-        Result = If_LogCounterAdd( pTimes, &nTimes, pArray[i], 0 );
-
-    printf( "%d  %d\n", Result64, Result );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Inserts the entry while sorting them by delay.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-word If_AigVerifyArray( Vec_Int_t * vAig, int nLeaves, int fCompl )
-{
-    assert( Vec_IntSize(vAig) > 0 );
-    assert( Vec_IntEntryLast(vAig) < 2 );
-    if ( Vec_IntSize(vAig) == 1 ) // const
-        return Vec_IntEntry(vAig, 0) ? ~((word)0) : 0;
-    if ( Vec_IntSize(vAig) == 2 ) // variable
-    {
-        assert( Vec_IntEntry(vAig, 0) == 0 );
-        return Vec_IntEntry(vAig, 1) ? ~s_Truths6[0] : s_Truths6[0];
-    }
-    else
-    {
-        word Truth0 = 0, Truth1 = 0, TruthR;
-        int i, iVar0, iVar1, iLit0, iLit1;
-        assert( Vec_IntSize(vAig) & 1 );
-        Vec_IntForEachEntryDouble( vAig, iLit0, iLit1, i )
-        {
-            iVar0 = Abc_Lit2Var( iLit0 );
-            iVar1 = Abc_Lit2Var( iLit1 );
-            Truth0 = iVar0 < nLeaves ? s_Truths6[iVar0] : Vec_WrdEntry( (Vec_Wrd_t *)vAig, iVar0 - nLeaves );
-            Truth1 = iVar1 < nLeaves ? s_Truths6[iVar1] : Vec_WrdEntry( (Vec_Wrd_t *)vAig, iVar1 - nLeaves );
-            if ( Abc_LitIsCompl(iLit0) )
-                Truth0 = ~Truth0;
-            if ( Abc_LitIsCompl(iLit1) )
-                Truth1 = ~Truth1;
-            assert( (i & 1) == 0 );
-            Vec_WrdWriteEntry( (Vec_Wrd_t *)vAig, Abc_Lit2Var(i), Truth0 & Truth1 );  // overwriting entries
-        }
-        assert( i == Vec_IntSize(vAig) - 1 );
-        TruthR = Truth0 & Truth1;
-        if ( Vec_IntEntry(vAig, i) ^ fCompl )
-            TruthR = ~TruthR;
-        Vec_IntClear( vAig ); // useless
-        return TruthR;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int If_LogCreateAnd( Vec_Int_t * vAig, int iLit0, int iLit1, int nSuppAll )
-{
-    int iObjId = Vec_IntSize(vAig)/2 + nSuppAll;
-    Vec_IntPush( vAig, iLit0 );
-    Vec_IntPush( vAig, iLit1 );
-    return Abc_Var2Lit( iObjId, 0 );
-}
-static inline int If_LogCreateMux( Vec_Int_t * vAig, int iLitC, int iLit1, int iLit0, int nSuppAll )
-{
-    int iFanLit0 = If_LogCreateAnd( vAig, iLitC, iLit1, nSuppAll );
-    int iFanLit1 = If_LogCreateAnd( vAig, Abc_LitNot(iLitC), iLit0, nSuppAll );
-    int iResLit  = If_LogCreateAnd( vAig, Abc_LitNot(iFanLit0), Abc_LitNot(iFanLit1), nSuppAll );
-    return Abc_LitNot(iResLit);
-}
-static inline int If_LogCreateXor( Vec_Int_t * vAig, int iLit0, int iLit1, int nSuppAll )
-{
-    return If_LogCreateMux( vAig, iLit0, Abc_LitNot(iLit1), iLit1, nSuppAll );
-}
-static inline int If_LogCreateAndXor( Vec_Int_t * vAig, int iLit0, int iLit1, int nSuppAll, int fXor )
-{
-    return fXor ? If_LogCreateXor(vAig, iLit0, iLit1, nSuppAll) : If_LogCreateAnd(vAig, iLit0, iLit1, nSuppAll);
-}
-static inline int If_LogCreateAndXorMulti( Vec_Int_t * vAig, int * pFaninLits, int nFanins, int nSuppAll, int fXor )
-{
-    int i;
-    assert( nFanins > 0 );
-    for ( i = nFanins - 1; i > 0; i-- )
-        pFaninLits[i-1] = If_LogCreateAndXor( vAig, pFaninLits[i], pFaninLits[i-1], nSuppAll, fXor );
-    return pFaninLits[0];
-}
-static inline int If_LogCounterAddAig( int * pTimes, int * pnTimes, int * pFaninLits, int Num, int iLit, Vec_Int_t * vAig, int nSuppAll, int fXor )
-{
-    int nTimes = *pnTimes;
-    if ( vAig )
-        pFaninLits[nTimes] = iLit;
-    pTimes[nTimes++] = Num;
-    if ( nTimes > 1 )
-    {
-        int i, k;
-        for ( k = nTimes-1; k > 0; k-- )
-        {
-            if ( pTimes[k] < pTimes[k-1] )
-                break;
-            if ( pTimes[k] > pTimes[k-1] )
-            { 
-                ABC_SWAP( int, pTimes[k], pTimes[k-1] ); 
-                if ( vAig )
-                    ABC_SWAP( int, pFaninLits[k], pFaninLits[k-1] ); 
-                continue; 
-            }
-            pTimes[k-1] += 1 + fXor;
-            if ( vAig )
-                pFaninLits[k-1] = If_LogCreateAndXor( vAig, pFaninLits[k], pFaninLits[k-1], nSuppAll, fXor );
-            for ( nTimes--, i = k; i < nTimes; i++ )
-            {
-                pTimes[i] = pTimes[i+1];
-                if ( vAig )
-                    pFaninLits[i] = pFaninLits[i+1];
-            }
-        }
-    }
-    assert( nTimes > 0 );
-    *pnTimes = nTimes;
-    return pTimes[0] + (nTimes > 1 ? 1 + fXor : 0);
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Compute delay/area profile of the structure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int  If_CutPinDelayGet( word D, int v )           { assert(v >= 0 && v < IF_MAX_FUNC_LUTSIZE); return (int)((D >> (v << 2)) & 0xF);                             }
-static inline void If_CutPinDelaySet( word * pD, int v, int d ) { assert(v >= 0 && v < IF_MAX_FUNC_LUTSIZE); assert(d >= 0 && d < IF_MAX_FUNC_LUTSIZE); *pD |= ((word)d << (v << 2)); }
-static inline word If_CutPinDelayInit( int v )                  { assert(v >= 0 && v < IF_MAX_FUNC_LUTSIZE); return (word)1 << (v << 2);                                      }
-static inline word If_CutPinDelayMax( word D1, word D2, int nVars, int AddOn )
-{
-    int v, Max;
-    word D = 0;
-    for ( v = 0; v < nVars; v++ )
-        if ( (Max = Abc_MaxInt(If_CutPinDelayGet(D1, v), If_CutPinDelayGet(D2, v))) )
-            If_CutPinDelaySet( &D, v, Abc_MinInt(Max + AddOn, 15) );
-    return D;
-}
-static inline word If_CutPinDelayDecrement( word D1, int nVars )
-{
-    int v;
-    word D = 0;
-    for ( v = 0; v < nVars; v++ )
-        if ( If_CutPinDelayGet(D1, v) )
-            If_CutPinDelaySet( &D, v, If_CutPinDelayGet(D1, v) - 1 );
-    return D;
-}
-static inline int If_CutPinDelayEqual( word D1, word D2, int nVars ) // returns 1 if D1 has the same delays than D2
-{
-    int v;
-    for ( v = 0; v < nVars; v++ )
-        if ( If_CutPinDelayGet(D1, v) != If_CutPinDelayGet(D2, v) )
-            return 0;
-    return 1;
-}
-static inline int If_CutPinDelayDom( word D1, word D2, int nVars ) // returns 1 if D1 has the same or smaller delays than D2
-{
-    int v;
-    for ( v = 0; v < nVars; v++ )
-        if ( If_CutPinDelayGet(D1, v) > If_CutPinDelayGet(D2, v) )
-            return 0;
-    return 1;
-}
-static inline void If_CutPinDelayTranslate( word D, int nVars, char * pPerm ) // fills up the array
-{
-    int v, Delay;
-    for ( v = 0; v < nVars; v++ )
-    {
-        Delay = If_CutPinDelayGet(D, v);
-        assert( Delay > 1 );
-        pPerm[v] = Delay - 1;
-    }
-}
-static inline void If_CutPinDelayPrint( word D, int nVars )
-{
-    int v;
-    printf( "Delay profile = {" );
-    for ( v = 0; v < nVars; v++ )
-        printf( " %d", If_CutPinDelayGet(D, v) );
-    printf( " }\n" );
-}
-static inline int If_LogCounterPinDelays( int * pTimes, int * pnTimes, word * pPinDels, int Num, word PinDel, int nSuppAll, int fXor )
-{
-    int nTimes = *pnTimes;
-    pPinDels[nTimes] = PinDel;
-    pTimes[nTimes++] = Num;
-    if ( nTimes > 1 )
-    {
-        int i, k;
-        for ( k = nTimes-1; k > 0; k-- )
-        {
-            if ( pTimes[k] < pTimes[k-1] )
-                break;
-            if ( pTimes[k] > pTimes[k-1] )
-            { 
-                ABC_SWAP( int, pTimes[k], pTimes[k-1] ); 
-                ABC_SWAP( word, pPinDels[k], pPinDels[k-1] ); 
-                continue; 
-            }
-            pTimes[k-1] += 1 + fXor;
-            pPinDels[k-1] = If_CutPinDelayMax( pPinDels[k], pPinDels[k-1], nSuppAll, 1 + fXor );
-            for ( nTimes--, i = k; i < nTimes; i++ )
-            {
-                pTimes[i] = pTimes[i+1];
-                pPinDels[i] = pPinDels[i+1];
-            }
-        }
-    }
-    assert( nTimes > 0 );
-    *pnTimes = nTimes;
-    return pTimes[0] + (nTimes > 1 ? 1 + fXor : 0);
-}
-static inline word If_LogPinDelaysMulti( word * pPinDels, int nFanins, int nSuppAll, int fXor )
-{
-    int i;
-    assert( nFanins > 0 );
-    for ( i = nFanins - 1; i > 0; i-- )
-        pPinDels[i-1] = If_CutPinDelayMax( pPinDels[i], pPinDels[i-1], nSuppAll, 1 + fXor );
-    return pPinDels[0];
-}
 int If_CutSopBalancePinDelaysInt( Vec_Int_t * vCover, int * pTimes, int nSuppAll, char * pPerm )
 {
     word pPinDelsAnd[IF_MAX_FUNC_LUTSIZE], pPinDelsOr[IF_MAX_CUBES];
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index 6bcc44be..4b1a42e5 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -20,6 +20,7 @@
 
 #include <math.h>
 #include "if.h"
+#include "ifCount.h"
 #include "misc/extra/extra.h"
 #include "sat/bsat/satSolver.h"
 #include "aig/gia/gia.h"
@@ -1838,9 +1839,10 @@ void If_DsdManTest()
     Vec_IntFree( vSets );
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Compute pin delays.]
 
   Description []
                
@@ -1849,174 +1851,71 @@ void If_DsdManTest()
   SeeAlso     []
 
 ***********************************************************************/
-static inline int If_LogCounterAdd( int * pTimes, int * pnTimes, int Num, int fXor )
-{
-    int nTimes = *pnTimes;
-    pTimes[nTimes++] = Num;
-    if ( nTimes > 1 )
-    {
-        int i, k;
-        for ( k = nTimes-1; k > 0; k-- )
-        {
-            if ( pTimes[k] < pTimes[k-1] )
-                break;
-            if ( pTimes[k] > pTimes[k-1] )
-            { 
-                ABC_SWAP( int, pTimes[k], pTimes[k-1] ); 
-                continue; 
-            }
-            pTimes[k-1] += 1 + fXor;
-            for ( nTimes--, i = k; i < nTimes; i++ )
-                pTimes[i] = pTimes[i+1];
-        }
-    }
-    assert( nTimes > 0 );
-    *pnTimes = nTimes;
-    return pTimes[0] + (nTimes > 1 ? 1 + fXor : 0);
-}
-int If_DsdCutBalanceCost_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pArea, int * pnSupp )
+int If_CutDsdBalancePinDelays_rec( If_DsdMan_t * p, int Id, int * pTimes, word * pRes, int * pnSupp, int nSuppAll, char * pPermLits )
 {
     If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Id );
-    if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
-        return -1;
+    assert( If_DsdObjType(pObj) != IF_DSD_PRIME );
     if ( If_DsdObjType(pObj) == IF_DSD_VAR )
-        return pTimes[(*pnSupp)++];
+    {
+        int iCutVar = Abc_Lit2Var(pPermLits[(*pnSupp)++]);
+        *pRes = If_CutPinDelayInit(iCutVar);
+        return pTimes[iCutVar];
+    }
     if ( If_DsdObjType(pObj) == IF_DSD_MUX )
     {
+        word pFaninRes[3], Res0, Res1;
         int i, iFanin, Delay[3];
         If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
-        {
-            Delay[i] = If_DsdCutBalanceCost_rec( p, Abc_Lit2Var(iFanin), pTimes, pArea, pnSupp );
-            if ( Delay[i] == -1 )
-                return -1;
-        }
-        *pArea += 3;
+            Delay[i] = If_CutDsdBalancePinDelays_rec( p, Abc_Lit2Var(iFanin), pTimes, pFaninRes+i, pnSupp, nSuppAll, pPermLits );
+        Res0 = If_CutPinDelayMax( pFaninRes[0], pFaninRes[1], nSuppAll, 1 );
+        Res1 = If_CutPinDelayMax( pFaninRes[0], pFaninRes[2], nSuppAll, 1 );
+        *pRes = If_CutPinDelayMax( Res0, Res1, nSuppAll, 1 );
         return 2 + Abc_MaxInt(Delay[0], Abc_MaxInt(Delay[1], Delay[2]));
     }
-    else
+    assert( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_XOR );
     {
+        word pFaninRes[IF_MAX_FUNC_LUTSIZE];
         int i, iFanin, Delay, Result = 0;
+        int fXor = (If_DsdObjType(pObj) == IF_DSD_XOR);
         int nCounter = 0, pCounter[IF_MAX_FUNC_LUTSIZE];
-        assert( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_XOR );
         If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
         {
-            Delay = If_DsdCutBalanceCost_rec( p, Abc_Lit2Var(iFanin), pTimes, pArea, pnSupp );
-            if ( Delay == -1 )
-                return -1;
-            Result = If_LogCounterAdd( pCounter, &nCounter, Delay, If_DsdObjType(pObj) == IF_DSD_XOR );
+            Delay = If_CutDsdBalancePinDelays_rec( p, Abc_Lit2Var(iFanin), pTimes, pFaninRes+i, pnSupp, nSuppAll, pPermLits );
+            Result = If_LogCounterPinDelays( pCounter, &nCounter, pFaninRes, Delay, pFaninRes[i], nSuppAll, fXor );
         }
-        *pArea += (If_DsdObjType(pObj) == IF_DSD_XOR ? 3 : 1);
+        assert( nCounter > 0 );
+        if ( fXor )
+            Result = If_LogCounterDelayXor( pCounter, nCounter ); // estimation
+        *pRes = If_LogPinDelaysMulti( pFaninRes, nCounter, nSuppAll, fXor );
         return Result;
     }
 }
-int If_DsdCutBalanceCostInt( If_DsdMan_t * p, int iDsd, int * pTimes, int * pArea )
-{
-    int nSupp = 0;
-    int Res = If_DsdCutBalanceCost_rec( p, Abc_Lit2Var(iDsd), pTimes, pArea, &nSupp );
-    assert( nSupp == If_DsdVecLitSuppSize( &p->vObjs, iDsd ) );
-    return Res;
-}
-int If_DsdCutBalanceCost( If_Man_t * pIfMan, If_Cut_t * pCut )
+int If_CutDsdBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm )
 {
-    pCut->fUser = 1;
-    pCut->Cost = 0;
-    if ( pCut->nLeaves == 0 )
+    if ( pCut->nLeaves == 0 ) // const
         return 0;
-    if ( pCut->nLeaves == 1 )
-        return (int)If_ObjCutBest(If_CutLeaf(pIfMan, pCut, 0))->Delay; 
+    if ( pCut->nLeaves == 1 ) // variable
+    {
+        pPerm[0] = 0;
+        return (int)If_ObjCutBest(If_CutLeaf(p, pCut, 0))->Delay;
+    }
     else
     {
-        If_Obj_t * pLeaf;
-        int i, Delay, Area = 0, pTimes[IF_MAX_FUNC_LUTSIZE];
-        If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
-            pTimes[i] = (int)If_ObjCutBest(pLeaf)->Delay; 
-        Delay = If_DsdCutBalanceCostInt( pIfMan->pIfDsdMan, If_CutDsdLit(pCut), pTimes, &Area );
-        pCut->Cost = Area;
+        word Result = 0;
+        int i, Delay, nSupp = 0, pTimes[IF_MAX_FUNC_LUTSIZE];
+        for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+            pTimes[i] = (int)If_ObjCutBest(If_CutLeaf(p, pCut, i))->Delay; 
+        Delay = If_CutDsdBalancePinDelays_rec( p->pIfDsdMan, Abc_Lit2Var(If_CutDsdLit(pCut)), pTimes, &Result, &nSupp, If_CutLeaveNum(pCut), pCut->pPerm );
+        assert( nSupp == If_CutLeaveNum(pCut) );
+        If_CutPinDelayTranslate( Result, If_CutLeaveNum(pCut), pPerm );
         return Delay;
     }
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int If_LogCreateAnd( Vec_Int_t * vAig, int iLit0, int iLit1, int nSuppAll )
-{
-    int iObjId = Vec_IntSize(vAig)/2 + nSuppAll;
-    Vec_IntPush( vAig, iLit0 );
-    Vec_IntPush( vAig, iLit1 );
-    return Abc_Var2Lit( iObjId, 0 );
-}
-static inline int If_LogCreateMux( Vec_Int_t * vAig, int iLitC, int iLit1, int iLit0, int nSuppAll )
-{
-    int iFanLit0 = If_LogCreateAnd( vAig, iLitC, iLit1, nSuppAll );
-    int iFanLit1 = If_LogCreateAnd( vAig, Abc_LitNot(iLitC), iLit0, nSuppAll );
-    int iResLit  = If_LogCreateAnd( vAig, Abc_LitNot(iFanLit0), Abc_LitNot(iFanLit1), nSuppAll );
-    return Abc_LitNot(iResLit);
-}
-static inline int If_LogCreateXor( Vec_Int_t * vAig, int iLit0, int iLit1, int nSuppAll )
-{
-    return If_LogCreateMux( vAig, iLit0, Abc_LitNot(iLit1), iLit1, nSuppAll );
-}
-static inline int If_LogCreateAndXor( Vec_Int_t * vAig, int iLit0, int iLit1, int nSuppAll, int fXor )
-{
-    return fXor ? If_LogCreateXor(vAig, iLit0, iLit1, nSuppAll) : If_LogCreateAnd(vAig, iLit0, iLit1, nSuppAll);
-}
-static inline int If_LogCreateAndXorMulti( Vec_Int_t * vAig, int * pFaninLits, int nFanins, int nSuppAll, int fXor )
-{
-    int i;
-    assert( nFanins > 0 );
-    for ( i = nFanins - 1; i > 0; i-- )
-        pFaninLits[i-1] = If_LogCreateAndXor( vAig, pFaninLits[i], pFaninLits[i-1], nSuppAll, fXor );
-    return pFaninLits[0];
-}
-
-static inline int If_LogCounterAddAig( int * pTimes, int * pnTimes, int * pFaninLits, int Num, int iLit, Vec_Int_t * vAig, int nSuppAll, int fXor )
-{
-    int nTimes = *pnTimes;
-    if ( vAig )
-        pFaninLits[nTimes] = iLit;
-    pTimes[nTimes++] = Num;
-    if ( nTimes > 1 )
-    {
-        int i, k;
-        for ( k = nTimes-1; k > 0; k-- )
-        {
-            if ( pTimes[k] < pTimes[k-1] )
-                break;
-            if ( pTimes[k] > pTimes[k-1] )
-            { 
-                ABC_SWAP( int, pTimes[k], pTimes[k-1] ); 
-                if ( vAig )
-                    ABC_SWAP( int, pFaninLits[k], pFaninLits[k-1] ); 
-                continue; 
-            }
-            pTimes[k-1] += 1 + fXor;
-            if ( vAig )
-                pFaninLits[k-1] = If_LogCreateAndXor( vAig, pFaninLits[k], pFaninLits[k-1], nSuppAll, fXor );
-            for ( nTimes--, i = k; i < nTimes; i++ )
-            {
-                pTimes[i] = pTimes[i+1];
-                if ( vAig )
-                    pFaninLits[i] = pFaninLits[i+1];
-            }
-        }
-    }
-    assert( nTimes > 0 );
-    *pnTimes = nTimes;
-    return pTimes[0] + (nTimes > 1 ? 1 + fXor : 0);
-}
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Evaluate delay using DSD balancing.]
 
   Description []
                
@@ -2025,25 +1924,28 @@ static inline int If_LogCounterAddAig( int * pTimes, int * pnTimes, int * pFanin
   SeeAlso     []
 
 ***********************************************************************/
-int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSupp, Vec_Int_t * vAig, int * piLit, int nSuppAll, int * pArea )
+int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSupp, Vec_Int_t * vAig, int * piLit, int nSuppAll, int * pArea, char * pPermLits )
 {
     If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Id );
     if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
         return -1;
     if ( If_DsdObjType(pObj) == IF_DSD_VAR )
     {
+        int iCutVar = Abc_Lit2Var( pPermLits[*pnSupp] );
         if ( vAig )
-            *piLit = Abc_Var2Lit( *pnSupp, 0 );
-        return pTimes[(*pnSupp)++];
+            *piLit = Abc_Var2Lit( iCutVar, Abc_LitIsCompl(pPermLits[*pnSupp]) );
+        (*pnSupp)++;
+        return pTimes[iCutVar];
     }
     if ( If_DsdObjType(pObj) == IF_DSD_MUX )
     {
         int i, iFanin, Delay[3], pFaninLits[3];
         If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
         {
-            Delay[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea );
+            Delay[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits );
             if ( Delay[i] == -1 )
                 return -1;
+            pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
         }
         if ( vAig )
             *piLit = If_LogCreateMux( vAig, pFaninLits[0], pFaninLits[1], pFaninLits[2], nSuppAll );
@@ -2058,11 +1960,15 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup
         int nCounter = 0, pCounter[IF_MAX_FUNC_LUTSIZE], pFaninLits[IF_MAX_FUNC_LUTSIZE];
         If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
         {
-            Delay = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea );
+            Delay = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits );
             if ( Delay == -1 )
                 return -1;
+            pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
             Result = If_LogCounterAddAig( pCounter, &nCounter, pFaninLits, Delay, pFaninLits[i], vAig, nSuppAll, fXor );
         }
+        assert( nCounter > 0 );
+        if ( fXor )
+            Result = If_LogCounterDelayXor( pCounter, nCounter ); // estimation
         if ( vAig )
             *piLit = If_LogCreateAndXorMulti( vAig, pFaninLits, nCounter, nSuppAll, fXor );
         else
@@ -2070,19 +1976,21 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup
         return Result;
     }
 }
-int If_CutDsdBalanceEvalInt( If_DsdMan_t * p, int iDsd, int * pTimes, Vec_Int_t * vAig, int * pArea )
+int If_CutDsdBalanceEvalInt( If_DsdMan_t * p, int iDsd, int * pTimes, Vec_Int_t * vAig, int * pArea, char * pPermLits )
 {
     int nSupp = 0, iLit = 0;
     int nSuppAll = If_DsdVecLitSuppSize( &p->vObjs, iDsd );
-    int Res = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iDsd), pTimes, &nSupp, vAig, &iLit, nSuppAll, pArea );
+    int Res = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iDsd), pTimes, &nSupp, vAig, &iLit, nSuppAll, pArea, pPermLits );
+    if ( Res == -1 )
+        return -1;
     assert( nSupp == nSuppAll );
     assert( vAig == NULL || Abc_Lit2Var(iLit) == nSupp + Abc_Lit2Var(Vec_IntSize(vAig)) - 1 );
     if ( vAig )
-        Vec_IntPush( vAig, Abc_LitIsCompl(iLit) );
+        Vec_IntPush( vAig, Abc_LitIsCompl(iLit) ^ Abc_LitIsCompl(iDsd) );
     assert( vAig == NULL || (Vec_IntSize(vAig) & 1) );
     return Res;
 }
-int If_CutDsdBalanceEval( If_Man_t * pIfMan, If_Cut_t * pCut, Vec_Int_t * vAig )
+int If_CutDsdBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig )
 {
     pCut->fUser = 1;
     if ( vAig )
@@ -2101,27 +2009,20 @@ int If_CutDsdBalanceEval( If_Man_t * pIfMan, If_Cut_t * pCut, Vec_Int_t * vAig )
             Vec_IntPush( vAig, 0 );
         if ( vAig )
             Vec_IntPush( vAig, Abc_LitIsCompl(If_CutDsdLit(pCut)) );
-        return (int)If_ObjCutBest(If_CutLeaf(pIfMan, pCut, 0))->Delay;
+        return (int)If_ObjCutBest(If_CutLeaf(p, pCut, 0))->Delay;
     }
     else
     {
-        If_Obj_t * pLeaf;
         int i, pTimes[IF_MAX_FUNC_LUTSIZE];
         int Delay, Area = 0;
-        If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
-            pTimes[i] = (int)If_ObjCutBest(pLeaf)->Delay; 
-        Delay = If_CutDsdBalanceEvalInt( pIfMan->pIfDsdMan, If_CutDsdLit(pCut), pTimes, vAig, &Area );
+        for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+            pTimes[i] = (int)If_ObjCutBest(If_CutLeaf(p, pCut, i))->Delay; 
+        Delay = If_CutDsdBalanceEvalInt( p->pIfDsdMan, If_CutDsdLit(pCut), pTimes, vAig, &Area, pCut->pPerm );
         pCut->Cost = Area;
         return Delay;
     }
 }
 
-int If_CutDsdBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm )
-{
-    return 0;
-}
-
-
 /**Function*************************************************************
 
   Synopsis    []
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 9bda135f..61c8df5d 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -72,8 +72,6 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
             p->vTtMem[v] = p->vTtMem[6];
         if ( p->pPars->fDelayOpt )
         {
-            p->vCover = Vec_IntAlloc( 0 );
-            p->vArray = Vec_IntAlloc( 1000 );
             for ( v = 6; v <= Abc_MaxInt(6,p->pPars->nLutSize); v++ )
                 p->vTtIsops[v] = Vec_WecAlloc( 1000 );
             for ( v = 6; v <= Abc_MaxInt(6,p->pPars->nLutSize); v++ )
@@ -81,6 +79,11 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
             for ( v = 0; v < 6; v++ )
                 p->vTtIsops[v] = p->vTtIsops[6];
         }
+        if ( p->pPars->fDelayOpt || p->pPars->fDsdBalance );
+        {
+            p->vCover = Vec_IntAlloc( 0 );
+            p->vArray = Vec_IntAlloc( 1000 );
+        }
     }
     p->nPermWords  = p->pPars->fUsePerm? If_CutPermWords( p->pPars->nLutSize ) : 0;
     p->nObjBytes   = sizeof(If_Obj_t) + sizeof(int) * (p->pPars->nLutSize + p->nPermWords);
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index a497b37e..3226e5ce 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -133,6 +133,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
             pCut->Delay = If_CutDelaySop( p, pCut );
         else
             pCut->Delay = If_CutDelay( p, pObj, pCut );
+        assert( pCut->Delay != -1 );
 //        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", 
@@ -213,25 +214,26 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                 int truthId = Abc_Lit2Var(pCut->iCutFunc);
                 if ( Vec_IntSize(p->vTtDsds[pCut->nLeaves]) <= truthId || Vec_IntEntry(p->vTtDsds[pCut->nLeaves], truthId) == -1 )
                 {
-                    pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct );
+                    pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthWR(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct );
                     while ( Vec_IntSize(p->vTtDsds[pCut->nLeaves]) <= truthId )
                     {
                         Vec_IntPush( p->vTtDsds[pCut->nLeaves], -1 );
                         for ( v = 0; v < Abc_MaxInt(6, pCut->nLeaves); v++ )
                             Vec_StrPush( p->vTtPerms[pCut->nLeaves], IF_BIG_CHAR );
                     }
-                    Vec_IntWriteEntry( p->vTtDsds[pCut->nLeaves], truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
+                    Vec_IntWriteEntry( p->vTtDsds[pCut->nLeaves], truthId, pCut->iCutDsd );
                     for ( v = 0; v < (int)pCut->nLeaves; v++ )
                         Vec_StrWriteEntry( p->vTtPerms[pCut->nLeaves], truthId * Abc_MaxInt(6, pCut->nLeaves) + v, (char)pCut->pPerm[v] );
                 }
                 else
                 {
-                    pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds[pCut->nLeaves], truthId), Abc_LitIsCompl(pCut->iCutFunc) );
+                    pCut->iCutDsd = Vec_IntEntry( p->vTtDsds[pCut->nLeaves], truthId );
                     for ( v = 0; v < (int)pCut->nLeaves; v++ )
                         pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms[pCut->nLeaves], truthId * Abc_MaxInt(6, pCut->nLeaves) + v );
 //                    assert( If_DsdManSuppSize(p->pIfDsdMan, pCut->iCutDsd) == (int)pCut->nLeaves );
                 }
 //                If_ManCacheRecord( p, pCut0->iCutDsd, pCut1->iCutDsd, nShared, pCut->iCutDsd );
+                pCut->iCutDsd = Abc_LitNotCond( pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc) );
             }
             // run user functions
             pCut->fUseless = 0;
@@ -289,6 +291,8 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
             pCut->Delay = If_CutDelaySop( p, pCut );
         else 
             pCut->Delay = If_CutDelay( p, pObj, pCut );
+        if ( pCut->Delay == -1 )
+            continue;
         if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
             continue;
         // compute area of the cut (this area may depend on the application specific cost)
diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c
index f2c9c833..23e6a69d 100644
--- a/src/map/if/ifTime.c
+++ b/src/map/if/ifTime.c
@@ -202,10 +202,19 @@ void If_CutPropagateRequired( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut, fl
     {
         if ( pCut->fUser )
         {
-            char Perm[IF_MAX_FUNC_LUTSIZE];
-            char * pPerm = p->pPars->fDelayOpt ? Perm : pCut->pPerm;
+            char Perm[IF_MAX_FUNC_LUTSIZE], * pPerm = Perm;
             if ( p->pPars->fDelayOpt )
-                If_CutSopBalancePinDelays( p, pCut, pPerm );
+            {
+                int Delay = If_CutSopBalancePinDelays( p, pCut, pPerm );
+                assert( Delay == pCut->Delay );
+            }
+            else if ( p->pPars->fDsdBalance )
+            {
+                int Delay = If_CutDsdBalancePinDelays( p, pCut, pPerm );
+                assert( Delay == pCut->Delay );
+            }
+            else 
+                pPerm = pCut->pPerm;
             If_CutForEachLeaf( p, pCut, pLeaf, i )
             {
                 Pin2PinDelay = pPerm ? (pPerm[i] == IF_BIG_CHAR ? -IF_BIG_CHAR : pPerm[i]) : 1;