Improvements to DSD balancing.

9 files changed, 174 insertions, 38 deletions

diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 5b4d1cfa..9958a63c 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -1588,6 +1588,8 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp, int fNormalized )
         assert( pPars->nLutSize <= If_DsdManVarNum(p) );
         assert( (pPars->pLutStruct == NULL && If_DsdManLutSize(p) == 0) || (pPars->pLutStruct && pPars->pLutStruct[0] - '0' == If_DsdManLutSize(p)) );
         pIfMan->pIfDsdMan = (If_DsdMan_t *)Abc_FrameReadManDsd();
+        if ( pPars->fDsdBalance )
+            If_DsdManAllocIsops( pIfMan->pIfDsdMan, pPars->nLutSize );
     }
     // compute switching for the IF objects
     if ( pPars->fPower )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9f424459..86500d7a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -15097,6 +15097,11 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pPars->pLutStruct )
     {
+        if ( pPars->fDsdBalance )
+        {
+            Abc_Print( -1, "Incompatible options (-S and -x).\n" );
+            return 1;
+        }
         if ( pPars->nLutSize < 6 || pPars->nLutSize > 16 )
         {
             Abc_Print( -1, "This feature only works for [6;16]-LUTs.\n" );
@@ -15122,12 +15127,12 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->pLutLib     =  NULL;
     }
     // modify for delay optimization
-    if ( pPars->fDelayOpt || pPars->fDsdBalance )
+    if ( pPars->fDelayOpt || pPars->fDsdBalance || pPars->fDelayOptLut )
     {
         pPars->fTruth      =  1;
         pPars->fCutMin     =  1;
         pPars->fExpRed     =  0;
-        pPars->fUseDsd     =  pPars->fDsdBalance;
+        pPars->fUseDsd     =  pPars->fDsdBalance || pPars->fDelayOptLut;
         pPars->pLutLib     =  NULL;
     }
     // modify for delay optimization
@@ -15162,7 +15167,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
             printf( "DSD manager has incompatible number of variables.\n" );
             return 0;
         }
-        if ( p && LutSize != If_DsdManLutSize(p) )
+        if ( p && LutSize != If_DsdManLutSize(p) && !pPars->fDsdBalance )
         {
             printf( "DSD manager has different LUT size.\n" );
             return 0;
@@ -29859,6 +29864,11 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pPars->pLutStruct )
     {
+        if ( pPars->fDsdBalance )
+        {
+            Abc_Print( -1, "Incompatible options (-S and -x).\n" );
+            return 1;
+        }
         if ( pPars->nLutSize < 6 || pPars->nLutSize > 16 )
         {
             Abc_Print( -1, "This feature only works for [6;16]-LUTs.\n" );
@@ -29886,12 +29896,12 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->pLutLib     =  NULL;
     }
     // modify for delay optimization
-    if ( pPars->fDelayOpt || pPars->fDsdBalance )
+    if ( pPars->fDelayOpt || pPars->fDsdBalance || pPars->fDelayOptLut )
     {
         pPars->fTruth      =  1;
         pPars->fCutMin     =  1;
         pPars->fExpRed     =  0;
-        pPars->fUseDsd     =  pPars->fDsdBalance;
+        pPars->fUseDsd     =  pPars->fDsdBalance || pPars->fDelayOptLut;
         pPars->pLutLib     =  NULL;
     }
     // modify for delay optimization
@@ -29926,7 +29936,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
             printf( "DSD manager has incompatible number of variables.\n" );
             return 0;
         }
-        if ( p && LutSize != If_DsdManLutSize(p) )
+        if ( p && LutSize != If_DsdManLutSize(p) && !pPars->fDsdBalance )
         {
             printf( "DSD manager has different LUT size.\n" );
             return 0;
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 5bab925e..8131a64a 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -144,6 +144,8 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
         assert( pPars->nLutSize <= If_DsdManVarNum(p) );
         assert( (pPars->pLutStruct == NULL && If_DsdManLutSize(p) == 0) || (pPars->pLutStruct && pPars->pLutStruct[0] - '0' == If_DsdManLutSize(p)) );
         pIfMan->pIfDsdMan = (If_DsdMan_t *)Abc_FrameReadManDsd();
+        if ( pPars->fDsdBalance )
+            If_DsdManAllocIsops( pIfMan->pIfDsdMan, pPars->nLutSize );
     }
 
     // perform FPGA mapping
diff --git a/src/bool/kit/kitIsop.c b/src/bool/kit/kitIsop.c
index 2ff7d6f7..a0a0c197 100644
--- a/src/bool/kit/kitIsop.c
+++ b/src/bool/kit/kitIsop.c
@@ -101,10 +101,9 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB
     Vec_IntShrink( vMemory, pcRes->nCubes );
     return RetValue;
 }
-void Kit_TruthIsopPrint( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth )
+void Kit_TruthIsopPrintCover( Vec_Int_t * vCover, int nVars, int fCompl )
 {
     int i, k, Entry, Literal;
-    int RetValue = Kit_TruthIsop( puTruth, nVars, vCover, fTryBoth );
     if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0) )
     {
         printf( "Constant %d\n", Vec_IntSize(vCover) );
@@ -123,9 +122,14 @@ void Kit_TruthIsopPrint( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int
                 printf( "-" );
             else assert( 0 );
         }
-        printf( " %d\n", !RetValue );
+        printf( " %d\n", !fCompl );
     }
 }
+void Kit_TruthIsopPrint( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth )
+{
+    int fCompl = Kit_TruthIsop( puTruth, nVars, vCover, fTryBoth );
+    Kit_TruthIsopPrintCover( vCover, nVars, fCompl );
+}
 
 /**Function*************************************************************
 
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 3acc6844..eeb1abd7 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -526,12 +526,15 @@ extern int             If_CluCheckExt3( void * p, word * pTruth, int nVars, int
                            char * pLut0, char * pLut1, char * pLut2, word * pFunc0, word * pFunc1, word * pFunc2 );
 /*=== ifDelay.c =============================================================*/
 extern int             If_CutDelaySop( If_Man_t * p, If_Cut_t * pCut );
+extern int             If_CutSopBalanceEvalInt( Vec_Int_t * vCover, int * pTimes, int * pFaninLits, Vec_Int_t * vAig, int * piRes, int nSuppAll, int * pArea );
 extern int             If_CutSopBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig );
+extern int             If_CutSopBalancePinDelaysInt( Vec_Int_t * vCover, int * pTimes, word * pFaninRes, int nSuppAll, word * pRes );
 extern int             If_CutSopBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm );
 extern int             If_CutLutBalanceEval( If_Man_t * p, If_Cut_t * pCut );
 extern int             If_CutLutBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm );
 /*=== ifDsd.c =============================================================*/
 extern If_DsdMan_t *   If_DsdManAlloc( int nVars, int nLutSize );
+extern void            If_DsdManAllocIsops( If_DsdMan_t * p, int nLutSize );
 extern void            If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose );
 extern void            If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec, int fVerbose );
 extern void            If_DsdManFree( If_DsdMan_t * p, int fVerbose );
diff --git a/src/map/if/ifCount.h b/src/map/if/ifCount.h
index 478f1e9a..dcd3b63a 100644
--- a/src/map/if/ifCount.h
+++ b/src/map/if/ifCount.h
@@ -57,6 +57,7 @@ ABC_NAMESPACE_HEADER_START
 static inline int If_LogCreateAnd( Vec_Int_t * vAig, int iLit0, int iLit1, int nSuppAll )
 {
     int iObjId = Vec_IntSize(vAig)/2 + nSuppAll;
+    assert( Abc_Lit2Var(iLit0) != Abc_Lit2Var(iLit1) );
     Vec_IntPush( vAig, iLit0 );
     Vec_IntPush( vAig, iLit1 );
     return Abc_Var2Lit( iObjId, 0 );
@@ -285,6 +286,36 @@ static inline word If_AigVerifyArray( Vec_Int_t * vAig, int nLeaves )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void If_AigPrintArray( Vec_Int_t * vAig, int nLeaves )
+{
+    assert( Vec_IntSize(vAig) > 0 );
+    assert( Vec_IntEntryLast(vAig) < 2 );
+    if ( Vec_IntSize(vAig) == 1 ) // const
+        printf( "Const %d\n", Vec_IntEntry(vAig, 0) );
+    else if ( Vec_IntSize(vAig) == 2 ) // variable
+        printf( "Variable %s\n", Vec_IntEntry(vAig, 1) ? "Compl" : "" );
+    else
+    {
+        int i, iLit0, iLit1;
+        assert( Vec_IntSize(vAig) & 1 );
+        Vec_IntForEachEntryDouble( vAig, iLit0, iLit1, i )
+            printf( "%d %d\n", iLit0, iLit1 );
+        assert( i == Vec_IntSize(vAig) - 1 );
+        printf( "%s\n", Vec_IntEntry(vAig, i) ? "Compl" : "" );
+    }
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/map/if/ifDelay.c b/src/map/if/ifDelay.c
index 8eb2101d..21ae6585 100644
--- a/src/map/if/ifDelay.c
+++ b/src/map/if/ifDelay.c
@@ -116,13 +116,13 @@ int If_CutDelaySop( If_Man_t * p, If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-int If_CutSopBalancePinDelaysInt( Vec_Int_t * vCover, int * pTimes, int nSuppAll, char * pPerm )
+int If_CutSopBalancePinDelaysInt( Vec_Int_t * vCover, int * pTimes, word * pFaninRes, int nSuppAll, word * pRes )
 {
     word pPinDelsAnd[IF_MAX_FUNC_LUTSIZE], pPinDelsOr[IF_MAX_CUBES];
     int nCounterAnd, pCounterAnd[IF_MAX_FUNC_LUTSIZE];
     int nCounterOr,  pCounterOr[IF_MAX_CUBES];
     int i, k, Entry, Literal, Delay = 0;
-    word ResAnd, ResOr;
+    word ResAnd;
     if ( Vec_IntSize(vCover) > IF_MAX_CUBES )
         return -1;
     nCounterOr = 0;
@@ -133,7 +133,7 @@ int If_CutSopBalancePinDelaysInt( Vec_Int_t * vCover, int * pTimes, int nSuppAll
         {
             Literal = 3 & (Entry >> (k << 1));
             if ( Literal == 1 || Literal == 2 ) // neg or pos literal
-                Delay = If_LogCounterPinDelays( pCounterAnd, &nCounterAnd, pPinDelsAnd, pTimes[k], If_CutPinDelayInit(k), nSuppAll, 0 );
+                Delay = If_LogCounterPinDelays( pCounterAnd, &nCounterAnd, pPinDelsAnd, pTimes[k], pFaninRes[k], nSuppAll, 0 );
             else if ( Literal != 0 ) 
                 assert( 0 );
         }
@@ -142,8 +142,17 @@ int If_CutSopBalancePinDelaysInt( Vec_Int_t * vCover, int * pTimes, int nSuppAll
         Delay = If_LogCounterPinDelays( pCounterOr, &nCounterOr, pPinDelsOr, Delay, ResAnd, nSuppAll, 0 );
     }
     assert( nCounterOr > 0 );
-    ResOr = If_LogPinDelaysMulti( pPinDelsOr, nCounterOr, nSuppAll, 0 );
-    If_CutPinDelayTranslate( ResOr, nSuppAll, pPerm );
+    *pRes = If_LogPinDelaysMulti( pPinDelsOr, nCounterOr, nSuppAll, 0 );
+    return Delay;
+}
+int If_CutSopBalancePinDelaysIntInt( Vec_Int_t * vCover, int * pTimes, int nSuppAll, char * pPerm )
+{
+    int i, Delay;
+    word Res, FaninRes[IF_MAX_FUNC_LUTSIZE];
+    for ( i = 0; i < nSuppAll; i++ )
+        FaninRes[i] = If_CutPinDelayInit(i);
+    Delay = If_CutSopBalancePinDelaysInt( vCover, pTimes, FaninRes, nSuppAll, &Res );
+    If_CutPinDelayTranslate( Res, nSuppAll, pPerm );
     return Delay;
 }
 int If_CutSopBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm )
@@ -164,7 +173,7 @@ int If_CutSopBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm )
             return -1;
         for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
             pTimes[i] = (int)If_ObjCutBest(If_CutLeaf(p, pCut, i))->Delay; 
-        return If_CutSopBalancePinDelaysInt( vCover, pTimes, If_CutLeaveNum(pCut), pPerm );
+        return If_CutSopBalancePinDelaysIntInt( vCover, pTimes, If_CutLeaveNum(pCut), pPerm );
     }
 }
 
@@ -179,7 +188,7 @@ int If_CutSopBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm )
   SeeAlso     []
 
 ***********************************************************************/
-int If_CutSopBalanceEvalIntInt( Vec_Int_t * vCover, int * pTimes, Vec_Int_t * vAig, int * piRes, int nSuppAll, int * pArea )
+int If_CutSopBalanceEvalInt( Vec_Int_t * vCover, int * pTimes, int * pFaninLits, Vec_Int_t * vAig, int * piRes, int nSuppAll, int * pArea )
 {
     int nCounterAnd, pCounterAnd[IF_MAX_FUNC_LUTSIZE], pFaninLitsAnd[IF_MAX_FUNC_LUTSIZE];
     int nCounterOr,  pCounterOr[IF_MAX_CUBES],  pFaninLitsOr[IF_MAX_CUBES];
@@ -194,9 +203,9 @@ int If_CutSopBalanceEvalIntInt( Vec_Int_t * vCover, int * pTimes, Vec_Int_t * vA
         {
             Literal = 3 & (Entry >> (k << 1));
             if ( Literal == 1 ) // neg literal
-                nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], Abc_Var2Lit(k, 1), vAig, nSuppAll, 0 );
+                nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], Abc_LitNot(pFaninLits[k]), vAig, nSuppAll, 0 );
             else if ( Literal == 2 ) // pos literal
-                nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], Abc_Var2Lit(k, 0), vAig, nSuppAll, 0 );
+                nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], pFaninLits[k], vAig, nSuppAll, 0 );
             else if ( Literal != 0 ) 
                 assert( 0 );
         }
@@ -210,17 +219,23 @@ int If_CutSopBalanceEvalIntInt( Vec_Int_t * vCover, int * pTimes, Vec_Int_t * vA
     }
     assert( nCounterOr > 0 );
     if ( vAig )
+    {
         *piRes = Abc_LitNot( If_LogCreateAndXorMulti( vAig, pFaninLitsOr, nCounterOr, nSuppAll, 0 ) );
+        if ( ((vCover->nCap >> 16) & 1) )  // hack to remember complemented attribute
+            *piRes = Abc_LitNot( *piRes );
+    }
     else       
         *pArea += Vec_IntSize(vCover) == 1 ? 0 : Vec_IntSize(vCover) - 1;
     return Delay;
 }
-int If_CutSopBalanceEvalInt( Vec_Int_t * vCover, int nLeaves, int * pTimes, Vec_Int_t * vAig, int fCompl, int * pArea ) 
+int If_CutSopBalanceEvalIntInt( Vec_Int_t * vCover, int nLeaves, int * pTimes, Vec_Int_t * vAig, int fCompl, int * pArea ) 
 {
-    int iRes = 0, Res;
-    if ( Vec_IntSize(vCover) == 0 )
-        return -1;
-    Res = If_CutSopBalanceEvalIntInt( vCover, pTimes, vAig, &iRes, nLeaves, pArea );
+    int pFaninLits[IF_MAX_FUNC_LUTSIZE];
+    int iRes = 0, Res, k;
+    if ( vAig )
+        for ( k = 0; k < nLeaves; k++ )
+            pFaninLits[k] = Abc_Var2Lit(k, 0);
+    Res = If_CutSopBalanceEvalInt( vCover, pTimes, pFaninLits, vAig, &iRes, nLeaves, pArea );
     if ( Res == -1 )
         return -1;
     assert( vAig == NULL || Abc_Lit2Var(iRes) == nLeaves + Abc_Lit2Var(Vec_IntSize(vAig)) - 1 );
@@ -255,12 +270,14 @@ int If_CutSopBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig )
     else
     {
         Vec_Int_t * vCover = Vec_WecEntry( p->vTtIsops[pCut->nLeaves], Abc_Lit2Var(If_CutTruthLit(pCut)) );
-        int fCompl = Abc_LitIsCompl(If_CutTruthLit(pCut)) ^ ((vCover->nCap >> 16) & 1); // hack to remember complemented attribute
         int Delay, Area = 0;
         int i, pTimes[IF_MAX_FUNC_LUTSIZE];
+        if ( vCover == NULL )
+            return -1;
+        assert( Vec_IntSize(vCover) > 0 );
         for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
             pTimes[i] = (int)If_ObjCutBest(If_CutLeaf(p, pCut, i))->Delay; 
-        Delay = If_CutSopBalanceEvalInt( vCover, If_CutLeaveNum(pCut), pTimes, vAig, fCompl, &Area );
+        Delay = If_CutSopBalanceEvalIntInt( vCover, If_CutLeaveNum(pCut), pTimes, vAig, Abc_LitIsCompl(If_CutTruthLit(pCut)), &Area );
         pCut->Cost = Area;
         return Delay;
     }
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index cc90b6cd..5ccfb19b 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -24,6 +24,7 @@
 #include "misc/extra/extra.h"
 #include "sat/bsat/satSolver.h"
 #include "aig/gia/gia.h"
+#include "bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -72,6 +73,7 @@ struct If_DsdMan_t_
     word **        pTtElems;       // elementary TTs
     Vec_Mem_t *    vTtMem[IF_MAX_FUNC_LUTSIZE+1];  // truth table memory and hash table
     Vec_Ptr_t *    vTtDecs[IF_MAX_FUNC_LUTSIZE+1]; // truth table decompositions
+    Vec_Wec_t *    vIsops[IF_MAX_FUNC_LUTSIZE+1];  // ISOP for each function
     int *          pSched[IF_MAX_FUNC_LUTSIZE];    // grey code schedules
     Gia_Man_t *    pTtGia;         // GIA to represent truth tables
     Vec_Int_t *    vCover;         // temporary memory
@@ -232,14 +234,41 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
     Gia_ManHashAlloc( p->pTtGia );
     for ( v = 0; v < nVars; v++ )
         Gia_ManAppendCi( p->pTtGia );
-    p->vCover   = Vec_IntAlloc( 0 );
 */
     for ( v = 2; v < nVars; v++ )
         p->pSched[v] = Extra_GreyCodeSchedule( v );
     if ( LutSize )
     p->pSat     = If_ManSatBuildXY( LutSize );
+    p->vCover   = Vec_IntAlloc( 0 );
     return p;
 }
+void If_DsdManAllocIsops( If_DsdMan_t * p, int nLutSize )
+{
+    Vec_Int_t * vLevel;
+    int v, i, fCompl;
+    word * pTruth;
+    if ( p->vIsops[3] != NULL )
+        return;
+    if ( Vec_PtrSize(&p->vObjs) > 2 )
+        printf( "Warning: DSD manager is already started without ISOPs.\n" );
+    for ( v = 3; v <= nLutSize; v++ )
+    {
+        p->vIsops[v] = Vec_WecAlloc( 100 );
+        Vec_MemForEachEntry( p->vTtMem[v], pTruth, i )
+        {
+            vLevel = Vec_WecPushLevel( p->vIsops[v] );
+            fCompl = Kit_TruthIsop( (unsigned *)pTruth, v, p->vCover, 1 );
+            if ( fCompl >= 0 && Vec_IntSize(p->vCover) <= 8 )
+            {
+                Vec_IntGrow( vLevel, Vec_IntSize(p->vCover) );
+                Vec_IntAppend( vLevel, p->vCover );
+                if ( fCompl )
+                    vLevel->nCap ^= (1<<16); // hack to remember complemented attribute
+            }
+        }
+        assert( Vec_WecSize(p->vIsops[v]) == Vec_MemEntryNum(p->vTtMem[v]) );
+    }
+}
 void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
 {
     int v;
@@ -262,6 +291,8 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
         Vec_MemHashFree( p->vTtMem[v] );
         Vec_MemFree( p->vTtMem[v] );
         Vec_VecFree( (Vec_Vec_t *)(p->vTtDecs[v]) );
+        if ( p->vIsops[v] )
+            Vec_WecFree( p->vIsops[v] );
     }
     Vec_IntFreeP( &p->vTemp1 );
     Vec_IntFreeP( &p->vTemp2 );
@@ -842,6 +873,7 @@ int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int trut
 }
 int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word * pTruth )
 {
+    int PrevSize       = (Type == IF_DSD_PRIME) ? Vec_MemEntryNum( p->vTtMem[nLits] ) : -1;   
     int objId, truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem[nLits], pTruth) : -1;
     unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId );
 //abctime clk;
@@ -855,6 +887,19 @@ int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word
         Vec_PtrPush( p->vTtDecs[nLits], vSets );
 //        Dau_DecPrintSets( vSets, nLits );
     }
+    if ( p->vIsops[nLits] && truthId >= 0 && PrevSize != Vec_MemEntryNum(p->vTtMem[nLits]) )
+    {
+        Vec_Int_t * vLevel = Vec_WecPushLevel( p->vIsops[nLits] );
+        int fCompl = Kit_TruthIsop( (unsigned *)pTruth, nLits, p->vCover, 1 );
+        if ( fCompl >= 0 && Vec_IntSize(p->vCover) <= 8 )
+        {
+            Vec_IntGrow( vLevel, Vec_IntSize(p->vCover) );
+            Vec_IntAppend( vLevel, p->vCover );
+            if ( fCompl )
+                vLevel->nCap ^= (1<<16); // hack to remember complemented attribute
+        }
+        assert( Vec_WecSize(p->vIsops[nLits]) == Vec_MemEntryNum(p->vTtMem[nLits]) );
+    }
     if ( p->pTtGia && truthId >= 0 && truthId == Vec_MemEntryNum(p->vTtMem[nLits])-1 )
     {
 //        int nObjOld = Gia_ManAndNum(p->pTtGia);
@@ -1868,7 +1913,6 @@ void If_DsdManTest()
 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 );
-    assert( If_DsdObjType(pObj) != IF_DSD_PRIME );
     if ( If_DsdObjType(pObj) == IF_DSD_VAR )
     {
         int iCutVar = Abc_Lit2Var(pPermLits[(*pnSupp)++]);
@@ -1878,13 +1922,23 @@ int If_CutDsdBalancePinDelays_rec( If_DsdMan_t * p, int Id, int * pTimes, word *
     if ( If_DsdObjType(pObj) == IF_DSD_MUX )
     {
         word pFaninRes[3], Res0, Res1;
-        int i, iFanin, Delay[3];
+        int i, iFanin, Delays[3];
         If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
-            Delay[i] = If_CutDsdBalancePinDelays_rec( p, Abc_Lit2Var(iFanin), pTimes, pFaninRes+i, pnSupp, nSuppAll, pPermLits );
+            Delays[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]));
+        return 2 + Abc_MaxInt(Delays[0], Abc_MaxInt(Delays[1], Delays[2]));
+    }
+    if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
+    {
+        word pFaninRes[IF_MAX_FUNC_LUTSIZE];
+        int i, iFanin, Delays[IF_MAX_FUNC_LUTSIZE];
+        Vec_Int_t * vCover = Vec_WecEntry( p->vIsops[pObj->nFans], If_DsdObjTruthId(p, pObj) );
+        assert( Vec_IntSize(vCover) > 0 );
+        If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
+            Delays[i] = If_CutDsdBalancePinDelays_rec( p, Abc_Lit2Var(iFanin), pTimes, pFaninRes+i, pnSupp, nSuppAll, pPermLits );
+        return If_CutSopBalancePinDelaysInt( vCover, Delays, pFaninRes, nSuppAll, pRes );
     }
     assert( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_XOR );
     {
@@ -1941,8 +1995,6 @@ int If_CutDsdBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm )
 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] );
@@ -1953,11 +2005,11 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup
     }
     if ( If_DsdObjType(pObj) == IF_DSD_MUX )
     {
-        int i, iFanin, Delay[3], pFaninLits[3];
+        int i, iFanin, Delays[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, pPermLits );
-            if ( Delay[i] == -1 )
+            Delays[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits );
+            if ( Delays[i] == -1 )
                 return -1;
             pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
         }
@@ -1965,7 +2017,22 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup
             *piLit = If_LogCreateMux( vAig, pFaninLits[0], pFaninLits[1], pFaninLits[2], nSuppAll );
         else
             *pArea += 3;
-        return 2 + Abc_MaxInt(Delay[0], Abc_MaxInt(Delay[1], Delay[2]));
+        return 2 + Abc_MaxInt(Delays[0], Abc_MaxInt(Delays[1], Delays[2]));
+    }
+    if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
+    {
+        int i, iFanin, Delays[IF_MAX_FUNC_LUTSIZE], pFaninLits[IF_MAX_FUNC_LUTSIZE];
+        Vec_Int_t * vCover = Vec_WecEntry( p->vIsops[pObj->nFans], If_DsdObjTruthId(p, pObj) );
+        if ( Vec_IntSize(vCover) == 0 )
+            return -1;
+        If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, i )
+        {
+            Delays[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits );
+            if ( Delays[i] == -1 )
+                return -1;
+            pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
+        }
+        return If_CutSopBalanceEvalInt( vCover, Delays, pFaninLits, vAig, piLit, nSuppAll, pArea );
     }
     assert( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_XOR );
     {
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 633f7695..443822ac 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -222,9 +222,9 @@ void If_ManStop( If_Man_t * p )
     Vec_PtrFreeP( &p->vObjsRev );
     Vec_PtrFreeP( &p->vLatchOrder );
     Vec_IntFreeP( &p->vLags );
-    for ( i = 6; i <= p->pPars->nLutSize; i++ )
+    for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
         Vec_IntFreeP( &p->vTtDsds[i] );
-    for ( i = 6; i <= p->pPars->nLutSize; i++ )
+    for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
         Vec_StrFreeP( &p->vTtPerms[i] );
     Vec_IntFreeP( &p->vCutData );
     Vec_IntFreeP( &p->vPairRes );