1 files changed, 97 insertions, 32 deletions

diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c
index 8de8391f..f2e19945 100644
--- a/src/opt/lpk/lpkAbcDsd.c
+++ b/src/opt/lpk/lpkAbcDsd.c
@@ -30,9 +30,11 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the variable whose cofs have min sum of supp sizes.]
+  Synopsis    [Cofactors TTs w.r.t. all vars and finds the best var.]
 
-  Description []
+  Description [The best variable is the variable with the minimum 
+  sum total of the support sizes of all truth tables. This procedure 
+  computes and returns cofactors w.r.t. the best variable.]
                
   SideEffects []
 
@@ -42,6 +44,7 @@
 int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs )
 {
     int i, Var, VarBest, nSuppSize0, nSuppSize1, nSuppTotalMin, nSuppTotalCur, nSuppMaxMin, nSuppMaxCur;
+    assert( nTruths > 0 );
     VarBest = -1;
     Lpk_SuppForEachVar( p->uSupp, Var )
     {
@@ -85,7 +88,7 @@ int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTrut
   SeeAlso     []
 
 ***********************************************************************/
-unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets )
+unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets, int nSizeMax )
 {
     unsigned i, iLitFanin, uSupport, uSuppCur;
     Kit_DsdObj_t * pObj;
@@ -99,7 +102,7 @@ unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets
         uSupport = 0;
         Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
         {
-            uSupps[i] = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets );
+            uSupps[i] = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets, nSizeMax );
             uSupport |= uSupps[i];
         }
         // create all subsets, except empty and full
@@ -110,7 +113,8 @@ unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets
             for ( i = 0; i < pObj->nFans; i++ )
                 if ( s & (1 << i) )
                     uSuppCur |= uSupps[i];
-            Vec_IntPush( vSets, uSuppCur );
+            if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax )
+                Vec_IntPush( vSets, uSuppCur );
         }
         return uSupport;
     }
@@ -119,9 +123,10 @@ unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets
     uSupport = 0;
     Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
     {
-        uSuppCur  = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets );
+        uSuppCur  = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets, nSizeMax );
         uSupport |= uSuppCur;
-        Vec_IntPush( vSets, uSuppCur );
+        if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax )
+            Vec_IntPush( vSets, uSuppCur );
     }
     return uSupport;
 }
@@ -150,12 +155,15 @@ Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax )
     if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
     {
         uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
-        Vec_IntPush( vSets, uSupport );
+        if ( Kit_WordCountOnes(uSupport) <= nSizeMax )
+            Vec_IntPush( vSets, uSupport );
         return vSets;
     }
-    uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets );
+    uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets, nSizeMax );
     assert( (uSupport & 0xFFFF0000) == 0 );
-    Vec_IntPush( vSets, uSupport );
+    // add the total support of the network
+    if ( Kit_WordCountOnes(uSupport) <= nSizeMax )
+        Vec_IntPush( vSets, uSupport );
     // set the remaining variables
     Vec_IntForEachEntry( vSets, Number, i )
     {
@@ -176,7 +184,7 @@ Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1 )
+Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSizeMax )
 {
     Vec_Int_t * vSets;
     int Entry0, Entry1, Entry;
@@ -188,7 +196,8 @@ Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1 )
         Entry = Entry0 | Entry1;
         if ( (Entry & (Entry >> 16)) )
             continue;
-        Vec_IntPush( vSets, Entry );
+        if ( Kit_WordCountOnes(Entry) <= nSizeMax )
+            Vec_IntPush( vSets, Entry );
     }
     return vSets;
 }
@@ -266,14 +275,15 @@ void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5
   SeeAlso     []
 
 ***********************************************************************/
-Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth )
+void Lpk_DsdAnalizeOne( Lpk_Fun_t * p, int nCofDepth, Lpk_Res_t * pRes )
 {
-    static Lpk_Res_t Res, * pRes = &Res;
     unsigned * ppTruths[5][16];
     Vec_Int_t * pvBSets[4][8];
     Kit_DsdNtk_t * pNtkDec, * pTemp;
     unsigned uBoundSet;
     int i, k, nVarsBS, nVarsRem, Delay, Area;
+    assert( nCofDepth >= 0 && nCofDepth < 4 );
+    assert( nCofDepth < (int)p->nLutK - 1 );
     Lpk_FunAllocTruthTables( p, nCofDepth, ppTruths );
     // find the best cofactors
     memset( pRes, 0, sizeof(Lpk_Res_t) );
@@ -291,7 +301,7 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth )
     // derive the set of feasible boundsets
     for ( i = nCofDepth - 1; i >= 0; i-- )
         for ( k = 0; k < (1<<i); k++ )
-            pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1] );
+            pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1], p->nLutK - nCofDepth );
     // compare the resulting boundsets
     Vec_IntForEachEntry( pvBSets[0][0], uBoundSet, i )
     {
@@ -299,12 +309,13 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth )
             continue;
         assert( (uBoundSet & (uBoundSet >> 16)) == 0 );
         nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF );
+        assert( nVarsBS <= (int)p->nLutK - nCofDepth );
         nVarsRem = p->nVars - nVarsBS + nCofDepth + 1;
-        Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
         Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK );
-        if ( Delay > (int)p->nDelayLim || Area > (int)p->nAreaLim )
+        Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
+        if ( Area > (int)p->nAreaLim || Delay > (int)p->nDelayLim )
             continue;
-        if ( uBoundSet == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem )
+        if ( pRes->BSVars == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem )
         {
             pRes->nBSVars = nVarsBS;
             pRes->BSVars = uBoundSet;
@@ -316,7 +327,60 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth )
     }
     // free cofactor storage
     Lpk_FunFreeTruthTables( p, nCofDepth, ppTruths );
-    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DSD-based decomposition of the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p )
+{
+    static Lpk_Res_t Res0, * pRes0 = &Res0;
+    static Lpk_Res_t Res1, * pRes1 = &Res1;
+    static Lpk_Res_t Res2, * pRes2 = &Res2;
+    static Lpk_Res_t Res3, * pRes3 = &Res3;
+    memset( pRes0, 0, sizeof(Lpk_Res_t) );
+    memset( pRes1, 0, sizeof(Lpk_Res_t) );
+    memset( pRes2, 0, sizeof(Lpk_Res_t) );
+    memset( pRes3, 0, sizeof(Lpk_Res_t) );
+    assert( p->uSupp == Kit_BitMask(p->nVars) );
+
+    // try decomposition without cofactoring
+    Lpk_DsdAnalizeOne( p, 0, pRes0 );
+    if ( pRes0->nBSVars == (int)p->nLutK && pRes0->AreaEst <= (int)p->nAreaLim && pRes0->DelayEst <= (int)p->nDelayLim )
+        return pRes0;
+
+    // cofactor 1 time
+    if ( p->nLutK >= 3 ) 
+        Lpk_DsdAnalizeOne( p, 1, pRes1 );
+    assert( pRes1->nBSVars <= (int)p->nLutK - 1 );
+    if ( pRes1->nBSVars == (int)p->nLutK - 1 && pRes1->AreaEst <= (int)p->nAreaLim && pRes1->DelayEst <= (int)p->nDelayLim )
+        return pRes1;
+
+    // cofactor 2 times
+    if ( p->nLutK >= 4 ) 
+        Lpk_DsdAnalizeOne( p, 2, pRes2 );
+    assert( pRes2->nBSVars <= (int)p->nLutK - 2 );
+    if ( pRes2->nBSVars == (int)p->nLutK - 2 && pRes2->AreaEst <= (int)p->nAreaLim && pRes2->DelayEst <= (int)p->nDelayLim )
+        return pRes2;
+
+    // cofactor 3 times
+    if ( p->nLutK >= 5 ) 
+        Lpk_DsdAnalizeOne( p, 3, pRes3 );
+    assert( pRes3->nBSVars <= (int)p->nLutK - 3 );
+    if ( pRes3->nBSVars == (int)p->nLutK - 3 && pRes3->AreaEst <= (int)p->nAreaLim && pRes3->DelayEst <= (int)p->nDelayLim )
+        return pRes3;
+
+    // choose the best under these conditions
+
+    return NULL;
 }
 
 /**Function*************************************************************
@@ -332,19 +396,21 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth )
 ***********************************************************************/
 Lpk_Fun_t * Lpk_DsdSplit( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet )
 {
+    Lpk_Fun_t * pNew;
     Kit_DsdMan_t * pDsdMan;
     Kit_DsdNtk_t * pNtkDec, * pTemp;
     unsigned * pTruth  = Lpk_FunTruth( p, 0 );
     unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
     unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
-    Lpk_Fun_t * pNew;
     unsigned * ppTruths[5][16];
     char pBSVars[5];
-    int i, k, nVars, nCofs;
+    int i, k, nVars, iVacVar, nCofs;
     // get the bound set variables
     nVars = Lpk_SuppToVars( uBoundSet, pBSVars );
+    // get the vacuous variable
+    iVacVar = pBSVars[0];
     // compute the cofactors
-    Lpk_FunAllocTruthTables( p, nCofVars, ppTruths );
+    Lpk_FunAllocTruthTables( p, nCofVars + 1, ppTruths );
     for ( i = 0; i < nCofVars; i++ )
         for ( k = 0; k < (1<<i); k++ )
         {
@@ -353,38 +419,37 @@ Lpk_Fun_t * Lpk_DsdSplit( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned
         }
     // decompose each cofactor w.r.t. the bound set
     nCofs = (1<<nCofVars);
-    pDsdMan = Kit_DsdManAlloc( p->nVars, p->nVars * 4 );
+    pDsdMan = Kit_DsdManAlloc( p->nVars, p->nVars * 2 );
     for ( k = 0; k < nCofs; k++ )
     {
         pNtkDec = Kit_DsdDecompose( ppTruths[nCofVars][k], p->nVars );
         pNtkDec = Kit_DsdExpand( pTemp = pNtkDec );      Kit_DsdNtkFree( pTemp );
-        Kit_DsdTruthPartialTwo( pDsdMan, pNtkDec, uBoundSet, pBSVars[0], ppTruths[nCofVars+1][k], ppTruths[nCofVars+1][nCofs+k] );
+        Kit_DsdTruthPartialTwo( pDsdMan, pNtkDec, uBoundSet, iVacVar, ppTruths[nCofVars+1][k], ppTruths[nCofVars+1][nCofs+k] );
         Kit_DsdNtkFree( pNtkDec );
     }
     Kit_DsdManFree( pDsdMan );
-    // compute the composition function
-    for ( i = nCofVars - 1; i >= 1; i-- )
+    // compute the composition/decomposition functions (they will be in pTruth0/pTruth1)
+    for ( i = nCofVars; i >= 1; i-- )
         for ( k = 0; k < (1<<i); k++ )
-            Kit_TruthMuxVar( ppTruths[i][k], ppTruths[i+1][2*k+0], ppTruths[i+1][2*k+1], nVars, pCofVars[i] );
-    // now the composition/decomposition functions are in pTruth0/pTruth1
+            Kit_TruthMuxVar( ppTruths[i][k], ppTruths[i+1][2*k+0], ppTruths[i+1][2*k+1], nVars, pCofVars[i-1] );
 
     // derive the new component
     pNew = Lpk_FunDup( p, pTruth1 );
     // update the old component
     Kit_TruthCopy( pTruth, pTruth0, p->nVars );
     p->uSupp = Kit_TruthSupport( pTruth0, p->nVars );
-    p->pFanins[pBSVars[0]] = pNew->Id;
-    p->pDelays[pBSVars[0]] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
+    p->pFanins[iVacVar] = pNew->Id;
+    p->pDelays[iVacVar] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
     // support minimize both
     Lpk_FunSuppMinimize( p );
     Lpk_FunSuppMinimize( pNew );
     // update delay and area requirements
-    pNew->nDelayLim = p->nDelayLim - 1;
+    pNew->nDelayLim = p->pDelays[iVacVar];
     pNew->nAreaLim = 1;
     p->nAreaLim = p->nAreaLim - 1;
 
     // free cofactor storage
-    Lpk_FunFreeTruthTables( p, nCofVars, ppTruths );
+    Lpk_FunFreeTruthTables( p, nCofVars + 1, ppTruths );
     return pNew;
 }