Improved DSD.

5 files changed, 297 insertions, 17 deletions

diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index cb3c6832..a8876889 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -27,7 +27,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1 );
+extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -281,7 +281,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                 If_CutPerm0(pCut, pCut0), 
                 Abc_NamStr(p->pNamDsd, pCut1->iDsd), 
                 If_CutPerm1(pCut, pCut1), 
-                pObj->fCompl0, pObj->fCompl1 );
+                pObj->fCompl0, pObj->fCompl1, pCut->nLimit );
             pCut->iDsd = Abc_NamStrFindOrAdd( p->pNamDsd, pName, NULL );
         }
         
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index 755af85c..a6db62a5 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -40,7 +40,7 @@
 ABC_NAMESPACE_HEADER_START
 
 #define DAU_MAX_VAR    12 // should be 6 or more
-#define DAU_MAX_STR   256
+#define DAU_MAX_STR  2048
 #define DAU_MAX_WORD  (1<<(DAU_MAX_VAR-6))
 
 ////////////////////////////////////////////////////////////////////////
@@ -70,7 +70,7 @@ extern int           Dau_DsdCountAnds( char * pDsd );
 
 /*=== dauMerge.c  ==========================================================*/
 extern void          Dau_DsdRemoveBraces( char * pDsd, int * pMatches );
-extern char *        Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1 );
+extern char *        Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars );
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/opt/dau/dauArray.c b/src/opt/dau/dauArray.c
new file mode 100644
index 00000000..75fc99d4
--- /dev/null
+++ b/src/opt/dau/dauArray.c
@@ -0,0 +1,268 @@
+/**CFile****************************************************************
+
+  FileName    [dauArray.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware unmapping.]
+
+  Synopsis    [Array representation of DSD.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: dauArray.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dauInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// network types
+typedef enum { 
+    DAU_DSD_NONE = 0,      // 0:  unknown
+    DAU_DSD_CONST0,        // 1:  constant
+    DAU_DSD_VAR,           // 2:  variable
+    DAU_DSD_AND,           // 3:  AND
+    DAU_DSD_XOR,           // 4:  XOR
+    DAU_DSD_MUX,           // 5:  MUX
+    DAU_DSD_PRIME          // 6:  PRIME
+} Dau_DsdType_t;
+
+typedef struct Dau_Dsd_t_ Dau_Dsd_t;
+struct Dau_Dsd_t_
+{
+    unsigned       iVar    :   5;  // variable
+    unsigned       nFans   :   5;  // fanin count
+    unsigned       Depth   :   5;  // tree depth
+    unsigned       Offset  :   5;  // the diff between this and other node
+    unsigned       Data    :   5;  // user data
+    unsigned       Type    :   3;  // node type
+    unsigned       fCompl  :   1;  // the complemented attribute
+    unsigned       fUnused :   1;  // this vertice is unused
+};
+
+static inline void Dau_DsdClean( Dau_Dsd_t * p ) { *((int *)p) = 0; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+int Dau_DsdCountAnd( Dau_Dsd_t * p )
+{
+    int Count, Costs[7] = {0, 0, 0, 1, 3, 3, 3};
+    for ( Count = 0; p->Type; p++ )
+        Count += Costs[p->Type];
+    return Count;
+}
+
+/*
+void Dau_DsdMark( Dau_Dsd_t * p, int nSize, int * pMarks )
+{
+    int pStore[DAU_MAX_VAR] = {0};
+    Dau_Dsd_t * q;
+    if ( p->Type == DAU_DSD_CONST || p->Type == DAU_DSD_VAR )
+        return;
+    for ( q = p + nSize - 1; q >= p; q-- )
+    {
+        if ( q->Type == DAU_DSD_VAR )
+            pStore[q->Depth] += pMarks[q->iVar];
+        else 
+        {
+            q->Data = pStore[q->Depth+1]; pStore[q->Depth+1] = 0;
+            pStore[q->Depth] += (q->Data == q->nFans);            
+        }
+    }
+}
+*/
+
+int Dau_DsdConstruct( char * pDsd, Dau_Dsd_t * pStore )
+{
+    Dau_Dsd_t * pLevel[DAU_MAX_VAR];
+    Dau_Dsd_t * q = pStore;
+    int d = -1, fCompl = 0;
+    if ( Dau_DsdIsConst(pDsd) )
+    {
+        Dau_DsdClean( q );
+        q->Type   = DAU_DSD_CONST0;
+        q->fCompl = Dau_DsdIsConst1(pDsd);
+        return 1;
+    }
+    for ( --q; *pDsd; pDsd++ )
+    {
+        if ( *pDsd == '!' )
+        {
+            fCompl ^= 1;
+            continue;
+        }
+        if ( *pDsd == ')' || *pDsd == ']' || *pDsd == '>' || *pDsd == '}' )
+        {
+            assert( fCompl == 0 );
+            if ( --d >= 0 )
+            {
+                pLevel[d]->nFans++;
+                if ( pLevel[d]->Data > pLevel[d+1]->Data )
+                    pLevel[d]->Data = pLevel[d+1]->Data;
+            }
+            continue;
+        }
+        Dau_DsdClean( ++q );
+        q->Data = 31;
+        q->fCompl = fCompl;
+        fCompl = 0;
+        if ( *pDsd >= 'a' && *pDsd <= 'z' )
+        {
+            q->Type   = DAU_DSD_VAR;
+            q->iVar   = *pDsd - 'a';
+            q->Depth  = d + 1;
+            if ( d >= 0 )
+            {
+                pLevel[d]->nFans++;
+                if ( pLevel[d]->Data > q->iVar )
+                    pLevel[d]->Data = q->iVar;
+            }
+            continue;
+        }
+        if ( *pDsd == '(' )
+            q->Type = DAU_DSD_AND;
+        else if ( *pDsd == '[' )
+            q->Type = DAU_DSD_XOR;
+        else if ( *pDsd == '<' )
+            q->Type = DAU_DSD_MUX;
+        else if ( *pDsd == '{' )
+            q->Type = DAU_DSD_PRIME;
+        else assert( 0 );
+        pLevel[++d] = q;
+        q->Depth = d;
+    }
+    assert( d == -1 );
+    Dau_DsdClean( ++q );
+    return q - pStore;
+}
+
+void Dau_DsdPrint( Dau_Dsd_t * p )
+{
+    char OpenType[7]  = {0, 0, 0, '(', '[', '<', '{'};
+    char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'};
+    char pTypes[DAU_MAX_VAR];
+    int d, pVisits[DAU_MAX_VAR];
+    if ( p->Type == DAU_DSD_CONST0 )
+    {
+        printf( "%d\n", p->fCompl );
+        return;
+    }
+    pVisits[0] = 1;
+    for ( d = 0; p->Type; p++ )
+    {
+        if ( p->fCompl )
+            printf( "!" );
+        if ( p->Type == DAU_DSD_VAR )
+        {
+            printf( "%c", 'a' + p->iVar );
+            while ( d > 0 && --pVisits[d] == 0 )
+                printf( "%c", pTypes[d--] );
+        }
+        else
+        {
+            pVisits[++d] = p->nFans;
+            printf( "%c", OpenType[p->Type] );
+            printf( "%c", 'a' + p->Data );
+            printf( "%d", p->Depth );
+            pTypes[d]  = CloseType[p->Type];
+        }
+    }
+    assert( d == 0 );
+    printf( "\n" );
+}
+
+void Dau_DsdDepth( Dau_Dsd_t * p )
+{
+    int d, pVisits[DAU_MAX_VAR];
+    if ( p->Type == DAU_DSD_CONST0 )
+        return;
+    pVisits[0] = 1;
+    for ( d = 0; p->Type; p++ )
+    {
+        p->Depth = d;
+        if ( p->Type == DAU_DSD_VAR )
+            while ( d > 0 && --pVisits[d] == 0 )
+                d--;
+        else
+            pVisits[++d] = p->nFans;
+    }
+    assert( d == 0 );
+}
+
+void Dau_DsdRemoveUseless( Dau_Dsd_t * p )
+{
+    Dau_Dsd_t * q = p, * pLevel[DAU_MAX_VAR];
+    int d, fChange = 0, pVisits[DAU_MAX_VAR];
+    if ( p->Type == DAU_DSD_CONST0 )
+        return;
+    pVisits[0] = 1;
+    for ( d = 0; p->Type; p++ )
+    {
+        p->Depth = d;
+        if ( p->Type == DAU_DSD_VAR )
+            while ( d > 0 && --pVisits[d] == 0 )
+                d--;
+        else
+        {
+            if ( d > 0 && (pLevel[d-1]->Type == DAU_DSD_XOR && p->Type == DAU_DSD_XOR ||
+                           pLevel[d-1]->Type == DAU_DSD_AND && p->Type == DAU_DSD_AND && !p->fCompl) )
+            {
+                pLevel[d-1]->nFans += p->nFans - 1;
+                pVisits[d] += p->nFans - 1;
+                p->fUnused = 1;
+                fChange = 1;
+            }
+            else
+            {
+                pLevel[d++] = p;
+                pVisits[d] = p->nFans;
+            }
+        }
+    }
+    assert( d == 0 );
+    // compact
+    if ( fChange )
+    {
+        for ( p = q; p->Type; p++ )
+            if ( !p->fUnused )
+                *q++ = *p;
+        Dau_DsdClean( q );
+    }
+}
+
+void Dau_DsdTest22()
+{
+    Dau_Dsd_t pStore[2 * DAU_MAX_VAR];
+//    char * pDsd = "[(ab)c(f!(he))]";
+//    char * pDsd = "[(abd)cf(f!{she})]";
+    char * pDsd = "[(abd)[cf](f(sg(he)))]";
+//    char * pDsd = "[(ab)[cf]]";
+    int i, nSize = Dau_DsdConstruct( pDsd, pStore );
+//    Dau_DsdDepth( pStore );
+    Dau_DsdPrint( pStore );
+
+    Dau_DsdRemoveUseless( pStore );
+
+    Dau_DsdPrint( pStore );
+    i = 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/dau/dauDivs.c b/src/opt/dau/dauDivs.c
index 424a11df..a75b13a9 100644
--- a/src/opt/dau/dauDivs.c
+++ b/src/opt/dau/dauDivs.c
@@ -102,6 +102,7 @@ void Dau_DsdTest()
     Dau_DsdDivisors( &t, nVars );
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dau/dauMerge.c b/src/opt/dau/dauMerge.c
index af4eff9c..b286c2cf 100644
--- a/src/opt/dau/dauMerge.c
+++ b/src/opt/dau/dauMerge.c
@@ -20,6 +20,7 @@
 
 #include "dau.h"
 #include "dauInt.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -584,7 +585,7 @@ clock_t s_TimeComp[4] = {0};
   SeeAlso     []
 
 ***********************************************************************/
-char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1 )
+char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars )
 {
     int fVerbose = 0;
     int fCheck = 0;
@@ -602,7 +603,8 @@ char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, i
     int pMatches[DAU_MAX_STR];
     int nVarsShared, nVarsTotal;
     Dau_Sto_t S, * pS = &S;
-    word Truth, t = 0, t0 = 0, t1 = 0;
+    word * pTruth, * pt = NULL, * pt0 = NULL, * pt1 = NULL;
+    word pParts[3][DAU_MAX_WORD];
     int Status;
     clock_t clk = clock();
     Counter++;
@@ -645,9 +647,16 @@ printf( "%s\n", pDsd1 );
 
 
     if ( fCheck )
-        t0 = Dau_Dsd6ToTruth( pDsd0 );
+    {
+        pt0 = Dau_DsdToTruth( pDsd0, nVars );
+        Abc_TtCopy( pParts[0], pt0, Abc_TtWordNum(nVars), 0 );
+    }
     if ( fCheck )
-        t1 = Dau_Dsd6ToTruth( pDsd1 );
+    {
+        pt1 = Dau_DsdToTruth( pDsd1, nVars );
+        Abc_TtCopy( pParts[1], pt1, Abc_TtWordNum(nVars), 0 );
+        Abc_TtAnd( pParts[2], pParts[0], pParts[1], Abc_TtWordNum(nVars), 0 );
+    }
 
     // find shared varaiables
     nVarsShared = Dau_DsdMergeFindShared(pDsd0, pDsd1, pMatches0, pMatches1, pVarPres);
@@ -706,15 +715,15 @@ if ( fVerbose )
 Dau_DsdMergeStorePrintDefs( pS );
 
     // create new function
-    assert( nVarsTotal <= 6 );
+//    assert( nVarsTotal <= 6 );
     sprintf( pS->pOutput, "(%s%s)", pDsd0, pDsd1 );
-    Truth = Dau_Dsd6ToTruth( pS->pOutput );
-    Status = Dau_DsdDecompose( &Truth, nVarsTotal, 0, pS->pOutput );
+    pTruth = Dau_DsdToTruth( pS->pOutput, nVarsTotal );
+    Status = Dau_DsdDecompose( pTruth, nVarsTotal, 0, pS->pOutput );
 //printf( "%d ", Status );
     if ( Status == -1 ) // did not find 1-step DSD
         return NULL;
-    if ( Status > 6 ) // non-DSD part is too large
-        return NULL;
+//    if ( Status > 6 ) // non-DSD part is too large
+//        return NULL;
     if ( Dau_DsdIsConst(pS->pOutput) )
     {
         strcpy( pRes, pS->pOutput );
@@ -746,9 +755,11 @@ if ( fVerbose )
 printf( "%s\n", pRes );
 
     if ( fCheck )
-        t = Dau_Dsd6ToTruth( pRes );
-    if ( t != (t0 & t1) )
-        printf( "Dau_DsdMerge(): Verification failed!\n" );
+    {
+        pt = Dau_DsdToTruth( pRes, nVars );
+        if ( !Abc_TtEqual( pParts[2], pt, Abc_TtWordNum(nVars) ) )
+            printf( "Dau_DsdMerge(): Verification failed!\n" );
+    }
 
     if ( Status == 0 )
         s_TimeComp[1] += clock() - clk;
@@ -800,7 +811,7 @@ void Dau_DsdTest66()
 //    Dau_DsdMergeStatus( pStr, pMatches, 2, pStatus );
 //    Dau_DsdMergePrintWithStatus( pStr, pStatus );
 
-    pRes = Dau_DsdMerge( pStr1, Perm0, pStr2, Perm0, 0, 0 );
+    pRes = Dau_DsdMerge( pStr1, Perm0, pStr2, Perm0, 0, 0, 6 );
 
     t = 0; 
 }