Disjoint-support decomposition with cofactoring and boolean difference analysis

from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
entitled "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis" presented in ICCD'15.

3 files changed, 618 insertions, 0 deletions

diff --git a/src/opt/dsc/dsc.c b/src/opt/dsc/dsc.c
new file mode 100644
index 00000000..409b040f
--- /dev/null
+++ b/src/opt/dsc/dsc.c
@@ -0,0 +1,526 @@
+/**CFile****************************************************************
+
+  FileName    [dsc.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Disjoint support decomposition - ICCD'15]
+
+  Synopsis    [Disjoint-support decomposition with cofactoring and boolean difference analysis
+               from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
+               "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis," ICCD'15]
+
+  Author      [Vinicius Callegaro, Mayler G. A. Martins, Felipe S. Marranghello, Renato P. Ribas and Andre I. Reis]
+
+  Affiliation [UFRGS - Federal University of Rio Grande do Sul - Brazil]
+
+  Date        [Ver. 1.0. Started - October 24, 2014.]
+
+  Revision    [$Id: dsc.h,v 1.00 2014/10/24 00:00:00 vcallegaro Exp $]
+
+***********************************************************************/
+
+#include "dsc.h"
+#include <assert.h>
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+/*
+    This code performs truth-table-based decomposition for 6-variable functions.
+    Representation of operations:
+    ! = not;
+    (ab) = a and b;
+    [ab] = a xor b;
+*/
+typedef struct Dsc_node_t_ Dsc_node_t;
+struct Dsc_node_t_
+{
+    word *pNegCof;
+    word *pPosCof;
+    word *pBoolDiff;
+    unsigned int on[DSC_MAX_VAR+1]; // pos cofactor spec - first element denotes the size of the array
+    unsigned int off[DSC_MAX_VAR+1]; // neg cofactor spec - first element denotes the size of the array
+    char exp[DSC_MAX_STR];
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+inline void xorInPlace( word * pOut, word * pIn2, int nWords)
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] ^= pIn2[w];
+}
+
+void dsc_debug_node(Dsc_node_t * pNode, int nVars, const int TRUTH_WORDS) {
+    printf("Node:\t%s\n",pNode->exp);
+    printf("\tneg cof:\t");Abc_TtPrintHexRev(stdout, pNode->pNegCof, nVars);
+    printf("\tpos cof:\t");Abc_TtPrintHexRev(stdout, pNode->pPosCof, nVars);
+    printf("\tbool diff:\t");Abc_TtPrintHexRev(stdout, pNode->pBoolDiff, nVars);
+    printf("\toff:\t");
+    int i;
+    for (i=1;i<=pNode->off[0];i++) {
+        printf("%c%c", (pNode->off[i] & 1U) ? ' ' : '!', 'a'+(pNode->off[i] >> 1));
+    }
+    printf("\ton:\t");
+    for (i=1;i<=pNode->on[0];i++) {
+        printf("%c%c", (pNode->on[i] & 1U) ? ' ' : '!', 'a'+(pNode->on[i] >> 1));
+    }
+    printf("\n");
+}
+
+inline int dsc_and_test(Dsc_node_t *ni, Dsc_node_t *nj, const int TRUTH_WORDS, int* ci, int* cj) {
+            if (Abc_TtEqual(ni->pNegCof, nj->pNegCof, TRUTH_WORDS)) {*ci=1; *cj=1; return 1;}
+    else     if (Abc_TtEqual(ni->pNegCof, nj->pPosCof, TRUTH_WORDS)) {*ci=1; *cj=0; return 1;}
+    else     if (Abc_TtEqual(ni->pPosCof, nj->pNegCof, TRUTH_WORDS)) {*ci=0; *cj=1; return 1;}
+    else     if (Abc_TtEqual(ni->pPosCof, nj->pPosCof, TRUTH_WORDS)) {*ci=0; *cj=0; return 1;}
+    return 0;
+}
+
+inline int dsc_xor_test(Dsc_node_t *ni, Dsc_node_t *nj, const int TRUTH_WORDS) {
+    return Abc_TtEqual(ni->pBoolDiff, nj->pBoolDiff, TRUTH_WORDS);
+}
+
+void concat(char* target, char begin, char end, char* s1, int s1Polarity, char* s2, int s2Polarity) {
+    *target++ = begin;
+    //s1
+    if (!s1Polarity)
+        *target++ = '!';
+    while (*s1 != '\0')
+        *target++ = *s1++;
+    // s2
+    if (!s2Polarity)
+        *target++ = '!';
+    while (*s2 != '\0')
+        *target++ = *s2++;
+    // end
+    *target++ = end;
+    *target = '\0';
+}
+
+void cubeCofactor(word * const pTruth, const unsigned int * const cubeCof, const int TRUTH_WORDS) {
+    int size = cubeCof[0];
+    int i;
+    for (i = 1; i <= size; i++) {
+        unsigned int c = cubeCof[i];
+        if (c & 1U) {
+            Abc_TtCofactor1(pTruth, TRUTH_WORDS, c >> 1);
+        } else {
+            Abc_TtCofactor0(pTruth, TRUTH_WORDS, c >> 1);
+        }
+    }
+}
+
+void merge(unsigned int * const pOut, const unsigned int * const pIn) {
+    const int elementsToCopy = pIn[0];
+    int i, j;
+    for (i = pOut[0]+1, j = 1; j <= elementsToCopy; i++, j++) {
+        pOut[i] = pIn[j];
+    }
+    pOut[0] += elementsToCopy;
+}
+
+void dsc_and_group(Dsc_node_t * pOut, Dsc_node_t * ni, int niPolarity, Dsc_node_t * nj, int njPolarity, int nVars, const int TRUTH_WORDS) {
+    // expression
+    concat(pOut->exp, '(', ')', ni->exp, niPolarity, nj->exp, njPolarity);
+    // ON-OFF
+    unsigned int* xiOFF, * xiON, * xjOFF, * xjON;
+    if (niPolarity) {
+        xiOFF = ni->off;
+        xiON = ni->on;
+    } else {
+        xiOFF = ni->on;
+        xiON = ni->off;
+    }
+    if (njPolarity) {
+        xjOFF = nj->off;
+        xjON = nj->on;
+    } else {
+        xjOFF = nj->on;
+        xjON = nj->off;
+    }
+    // creating both the new OFF specification and negative cofactor of the new group
+    {
+        // first element of the array represents the size of the cube-cofactor
+        int xiOFFSize = xiOFF[0];
+        int xjOFFSize = xjOFF[0];
+        if (xiOFFSize <= xjOFFSize) {
+            pOut->off[0] = xiOFFSize; // set the number of elements
+            int i;
+            for (i = 1; i <= xiOFFSize; i++) {
+                pOut->off[i] = xiOFF[i];
+            }
+        } else {
+            pOut->off[0] = xjOFFSize; // set the number of elements
+            int i;
+            for (i = 1; i <= xjOFFSize; i++) {
+                pOut->off[i] = xjOFF[i];
+            }
+        }
+        // set the negative cofactor of the new group
+        pOut->pNegCof = niPolarity ? ni->pNegCof : ni->pPosCof;
+    }
+    // creating both new ON specification and positive cofactor of the new group
+    {
+        unsigned int xiONSize = xiON[0];
+        unsigned int xjONSize = xjON[0];
+        pOut->on[0] = xiONSize + xjONSize;
+        int i;
+        for (i = 1; i <= xiONSize; i++) {
+            pOut->on[i] = xiON[i];
+        }
+        int j;
+        for (j = 1; j <= xjONSize; j++) {
+            pOut->on[i++] = xjON[j];
+        }
+        // set the positive cofactor of the new group
+        if (xiONSize >= xjONSize) {
+            pOut->pPosCof = niPolarity ? ni->pPosCof : ni->pNegCof;
+            cubeCofactor(pOut->pPosCof, xjON, TRUTH_WORDS);
+        } else {
+            pOut->pPosCof = njPolarity ? nj->pPosCof : nj->pNegCof;
+            cubeCofactor(pOut->pPosCof, xiON, TRUTH_WORDS);
+        }
+    }
+    // set the boolean difference of the new group
+    pOut->pBoolDiff = njPolarity ? nj->pNegCof : nj->pPosCof;
+    xorInPlace(pOut->pBoolDiff, pOut->pPosCof, TRUTH_WORDS);
+}
+
+void dsc_xor_group(Dsc_node_t * pOut, Dsc_node_t * ni, Dsc_node_t * nj, int nVars, const int TRUTH_WORDS) {
+    // expression
+    concat(pOut->exp, '[', ']', ni->exp, 1, nj->exp, 1);
+    //
+    const unsigned int const * xiOFF = ni->off;
+    const unsigned int const * xiON = ni->on;
+    const unsigned int const * xjOFF = nj->off;
+    const unsigned int const * xjON = nj->on;
+    //
+    const int xiOFFSize = xiOFF[0];
+    const int xiONSize = xiON[0];
+    const int xjOFFSize = xjOFF[0];
+    const int xjONSize = xjON[0];
+    // minCubeCofs
+    int minCCSize = xiOFFSize;
+    int minCCPolarity = 0;
+    Dsc_node_t * minCCNode = ni;
+    if (minCCSize > xiONSize) {
+        minCCSize = xiONSize;
+        minCCPolarity = 1;
+        //minCCNode = ni;
+    }
+    if (minCCSize > xjOFFSize) {
+        minCCSize = xjOFFSize;
+        minCCPolarity = 0;
+        minCCNode = nj;
+    }
+    if (minCCSize > xjONSize) {
+        minCCSize = xjONSize;
+        minCCPolarity = 1;
+        minCCNode = nj;
+    }
+    //
+    if (minCCNode == ni) {
+        if (minCCPolarity) {
+            // gOFF = xiON, xjON
+            pOut->pNegCof = nj->pPosCof;
+            cubeCofactor(pOut->pNegCof, xiON, TRUTH_WORDS);
+            // gON = xiON, xjOFF
+            pOut->pPosCof = nj->pNegCof;
+            cubeCofactor(pOut->pPosCof, xiON, TRUTH_WORDS);
+        } else {
+            // gOFF = xiOFF, xjOFF
+            pOut->pNegCof = nj->pNegCof;
+            cubeCofactor(pOut->pNegCof, xiOFF, TRUTH_WORDS);
+            // gON = xiOFF, xjON
+            pOut->pPosCof = nj->pPosCof;
+            cubeCofactor(pOut->pPosCof, xiOFF, TRUTH_WORDS);
+        }
+    }else  {
+        if (minCCPolarity) {
+            // gOFF = xjON, xiON
+            pOut->pNegCof = ni->pPosCof;
+            cubeCofactor(pOut->pNegCof, xjON, TRUTH_WORDS);
+            // gON = xjON, xiOFF
+            pOut->pPosCof = ni->pNegCof;
+            cubeCofactor(pOut->pPosCof, xjON, TRUTH_WORDS);
+        } else {
+            // gOFF = xjOFF, xiOFF
+            pOut->pNegCof = ni->pNegCof;
+            cubeCofactor(pOut->pNegCof, xjOFF, TRUTH_WORDS);
+            // gON = xjOFF, xiON
+            pOut->pPosCof = ni->pPosCof;
+            cubeCofactor(pOut->pPosCof, xjOFF, TRUTH_WORDS);
+        }
+    }
+    // bool diff
+    pOut->pBoolDiff = ni->pBoolDiff;
+    // evaluating specs
+    // off spec
+    pOut->off[0] = 0;
+    if ((xiOFFSize+xjOFFSize) <= (xiONSize+xjONSize)) {
+        merge(pOut->off, xiOFF);
+        merge(pOut->off, xjOFF);
+    } else {
+        merge(pOut->off, xiON);
+        merge(pOut->off, xjON);
+    }
+    // on spec
+    pOut->on[0] = 0;
+    if ((xiOFFSize+xjONSize) <= (xiONSize+xjOFFSize)) {
+        merge(pOut->on, xiOFF);
+        merge(pOut->on, xjON);
+    } else {
+        merge(pOut->on, xiON);
+        merge(pOut->on, xjOFF);
+    }
+}
+
+/**
+ * memory allocator with a capacity of storing 3*nVars
+ * truth-tables for negative and positive cofactors and
+ * the boolean difference for each input variable
+ */
+extern word * Dsc_alloc_pool(int nVars) {
+    return ABC_ALLOC(word, 3 * Abc_TtWordNum(nVars) * nVars);
+}
+
+/**
+ * just free the memory pool
+ */
+extern void Dsc_free_pool(word * pool) {
+    ABC_FREE(pool);
+}
+
+/**
+ * This method implements the paper proposed by V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
+ * entitled "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis", presented at ICCD 2015.
+ * pTruth: pointer for the truth table representing the target function.
+ * nVarsInit: the number of variables of the truth table of the target function.
+ * pRes: pointer for storing the resulting decomposition, whenever a decomposition can be found.
+ * pool: NULL or a pointer for with a capacity of storing 3*nVars truth-tables. IF NULL, the function will allocate and free the memory of each call.
+ * (the results presented on ICCD paper are running this method with NULL for the memory pool).
+ * The method returns 0 if a full decomposition was found and a negative value otherwise.
+ */
+extern int Dsc_Decompose(word * pTruth, const int nVarsInit, char * const pRes, word *pool) {
+    const int TRUTH_WORDS = Abc_TtWordNum(nVarsInit);
+    const int NEED_POOL_ALLOC = (pool == NULL);
+
+    pRes[0] = '\0';
+    pRes[1] = '\0';
+
+    Dsc_node_t nodes[DSC_MAX_VAR];
+    Dsc_node_t *newNodes[DSC_MAX_VAR];
+    Dsc_node_t *oldNodes[DSC_MAX_VAR];
+
+    int n = 0; // n will represent the number of current nodes (i.e. support)
+
+    if (NEED_POOL_ALLOC)
+        pool = ABC_ALLOC(word, 3 * TRUTH_WORDS * nVarsInit);
+
+    // block for the node data allocation
+    {
+        // pointer for the next free truth word
+        word *pNextTruth = pool;
+        int iVar;
+        for (iVar = 0; iVar < nVarsInit; iVar++) {
+            // negative cofactor
+            Abc_TtCofactor0p(pNextTruth, pTruth, TRUTH_WORDS, iVar);
+            // dont care test
+            if (!Abc_TtEqual(pNextTruth, pTruth, TRUTH_WORDS)) {
+                Dsc_node_t *node = &nodes[iVar];
+                node->pNegCof = pNextTruth;
+                // increment next truth pointer
+                pNextTruth += TRUTH_WORDS;
+                // positive cofactor
+                node->pPosCof = pNextTruth;
+                Abc_TtCofactor1p(node->pPosCof, pTruth, TRUTH_WORDS, iVar);
+                // increment next truth pointer
+                pNextTruth += TRUTH_WORDS;
+                // boolean difference
+                node->pBoolDiff = pNextTruth;
+                Abc_TtXor(node->pBoolDiff, node->pNegCof, node->pPosCof, TRUTH_WORDS, 0);
+                // increment next truth pointer
+                pNextTruth += TRUTH_WORDS;
+                // define on spec -
+                node->on[0] = 1; node->on[1] = (iVar << 1) | 1u; // lit = i*2+1, when polarity=true
+                // define off spec
+                node->off[0] = 1; node->off[1] = iVar << 1;// lit=i*2 otherwise
+                // store the node expression
+                node->exp[0] = 'a'+iVar; // TODO fix the variable names
+                node->exp[1] = '\0';
+                // add the node to the newNodes array
+                newNodes[n++] = node;
+            }
+        }
+    }
+    //const int initialSupport = n;
+    if (n == 0) {
+        if (NEED_POOL_ALLOC)
+            ABC_FREE(pool);
+        if (Abc_TtIsConst0(pTruth, TRUTH_WORDS)) {
+            { if ( pRes ) pRes[0] = '0', pRes[1] = '\0'; }
+            return 0;
+        } else if (Abc_TtIsConst1(pTruth, TRUTH_WORDS)) {
+            { if ( pRes ) pRes[0] = '1', pRes[1] = '\0'; }
+            return 0;
+        } else {
+            Abc_Print(-1, "ERROR. No variable in the support of f, but f isn't constant!\n");
+            return -1;
+        }
+    }
+    Dsc_node_t freeNodes[DSC_MAX_VAR]; // N is the maximum number of possible groups.
+    int f = 0; // f represent the next free position in the freeNodes array
+
+    int o = 0; // o stands for the number of already tested nodes
+    while (n > 0) {
+        int tempN = 0;
+        int i, j, iPolarity, jPolarity;
+        Dsc_node_t *ni, *nj, *newNode = NULL;
+        for (i = 0; i < n; i++) {
+            ni = newNodes[i];
+            newNode = NULL;
+            j = 0;
+            while (j < o) {
+                nj = oldNodes[j];
+                if (dsc_and_test(ni, nj, TRUTH_WORDS, &iPolarity, &jPolarity)) {
+                    newNode = &freeNodes[f++];
+                    dsc_and_group(newNode, ni, iPolarity, nj, jPolarity, nVarsInit, TRUTH_WORDS);
+                }
+                // XOR test
+                if ((newNode == NULL)  && (dsc_xor_test(ni, nj, TRUTH_WORDS))) {
+                    newNode = &freeNodes[f++];
+                    dsc_xor_group(newNode, ni, nj, nVarsInit, TRUTH_WORDS);
+                }
+                if (newNode != NULL) {
+                    oldNodes[j] = oldNodes[--o];
+                    break;
+                } else {
+                    j++;
+                }
+            }
+            if (newNode != NULL) {
+                newNodes[tempN++] = newNode;
+            } else {
+                oldNodes[o++] = ni;
+            }
+        }
+        n = tempN;
+    }
+    if (o == 1) {
+        Dsc_node_t * solution = oldNodes[0];
+        if (Abc_TtIsConst0(solution->pNegCof, TRUTH_WORDS) && Abc_TtIsConst1(solution->pPosCof, TRUTH_WORDS)) {
+            // Direct solution found
+            if ( pRes )
+                strcpy( pRes, solution->exp);
+            if (NEED_POOL_ALLOC)
+                ABC_FREE(pool);
+            return 0;
+        } else if (Abc_TtIsConst1(solution->pNegCof, TRUTH_WORDS) && Abc_TtIsConst0(solution->pPosCof, TRUTH_WORDS)) {
+            // Complementary solution found
+            if ( pRes ) {
+                pRes[0] = '!';
+                strcpy( &pRes[1], solution->exp);
+            }
+            if (NEED_POOL_ALLOC)
+                ABC_FREE(pool);
+            return 0;
+        } else {
+            printf("DSC ERROR: Final DSC node found, but differs from target function.\n");
+            if (NEED_POOL_ALLOC)
+                ABC_FREE(pool);
+            return -1;
+        }
+    }
+    if (NEED_POOL_ALLOC)
+        ABC_FREE(pool);
+    return -1;
+}
+
+
+/**Function*************************************************************
+  Synopsis    [DSD formula manipulation.]
+  Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]
+***********************************************************************/
+int * Dsc_ComputeMatches( char * p )
+{
+    static int pMatches[DSC_MAX_VAR];
+    int pNested[DSC_MAX_VAR];
+    int v, nNested = 0;
+    for ( v = 0; p[v]; v++ )
+    {
+        pMatches[v] = 0;
+        if ( p[v] == '(' || p[v] == '[' || p[v] == '<' || p[v] == '{' )
+            pNested[nNested++] = v;
+        else if ( p[v] == ')' || p[v] == ']' || p[v] == '>' || p[v] == '}' )
+            pMatches[pNested[--nNested]] = v;
+        assert( nNested < DSC_MAX_VAR );
+    }
+    assert( nNested == 0 );
+    return pMatches;
+}
+
+/**Function*************************************************************
+  Synopsis    [DSD formula manipulation.]
+  Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]
+***********************************************************************/
+int Dsc_CountAnds_rec( char * pStr, char ** p, int * pMatches )
+{
+    if ( **p == '!' )
+        (*p)++;
+    while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
+        (*p)++;
+    if ( **p == '<' )
+    {
+        char * q = pStr + pMatches[*p - pStr];
+        if ( *(q+1) == '{' )
+            *p = q+1;
+    }
+    if ( **p >= 'a' && **p <= 'z' ) // var
+        return 0;
+    if ( **p == '(' || **p == '[' ) // and/or/xor
+    {
+        int Counter = 0, AddOn = (**p == '(')? 1 : 3;
+        char * q = pStr + pMatches[ *p - pStr ];
+        assert( *q == **p + 1 + (**p != '(') );
+        for ( (*p)++; *p < q; (*p)++ )
+            Counter += AddOn + Dsc_CountAnds_rec( pStr, p, pMatches );
+        assert( *p == q );
+        return Counter - AddOn;
+    }
+    if ( **p == '<' || **p == '{' ) // mux
+    {
+        int Counter = 3;
+        char * q = pStr + pMatches[ *p - pStr ];
+        assert( *q == **p + 1 + (**p != '(') );
+        for ( (*p)++; *p < q; (*p)++ )
+            Counter += Dsc_CountAnds_rec( pStr, p, pMatches );
+        assert( *p == q );
+        return Counter;
+    }
+    assert( 0 );
+    return 0;
+}
+/**Function*************************************************************
+  Synopsis    [DSD formula manipulation.]
+  Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]
+***********************************************************************/
+extern int Dsc_CountAnds( char * pDsd )
+{
+    if ( pDsd[1] == 0 )
+        return 0;
+    return Dsc_CountAnds_rec( pDsd, &pDsd, Dsc_ComputeMatches(pDsd) );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/opt/dsc/dsc.h b/src/opt/dsc/dsc.h
new file mode 100644
index 00000000..bf8958ea
--- /dev/null
+++ b/src/opt/dsc/dsc.h
@@ -0,0 +1,91 @@
+/**CFile****************************************************************
+
+  FileName    [dsc.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Disjoint support decomposition - ICCD'15]
+
+  Synopsis    [Disjoint-support decomposition with cofactoring and boolean difference analysis
+               from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
+               "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis," ICCD'15]
+
+  Author      [Vinicius Callegaro, Mayler G. A. Martins, Felipe S. Marranghello, Renato P. Ribas and Andre I. Reis]
+
+  Affiliation [UFRGS - Federal University of Rio Grande do Sul - Brazil]
+
+  Date        [Ver. 1.0. Started - October 24, 2014.]
+
+  Revision    [$Id: dsc.h,v 1.00 2014/10/24 00:00:00 vcallegaro Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__DSC___h
+#define ABC__DSC___h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+#include <stdio.h>
+#include <string.h>
+#include "misc/util/abc_global.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+#define DSC_MAX_VAR        16 // should be 6 or more, i.e. DSC_MAX_VAR >= 6
+#define DSC_MAX_STR        DSC_MAX_VAR << 2 // DSC_MAX_VAR * 4
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== dsc.c ==========================================================*/
+
+/**
+ * memory allocator with a capacity of storing 3*nVars
+ * truth-tables for negative and positive cofactors and
+ * the boolean difference for each input variable
+ */
+extern word * Dsc_alloc_pool(int nVars);
+
+/**
+ * This method implements the paper proposed by V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
+ * entitled "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis", presented at ICCD 2015.
+ * pTruth: pointer for the truth table representing the target function.
+ * nVarsInit: the number of variables of the truth table of the target function.
+ * pRes: pointer for storing the resulting decomposition, whenever a decomposition can be found.
+ * pool: NULL or a pointer for with a capacity of storing 3*nVars truth-tables. IF NULL, the function will allocate and free the memory of each call.
+ * (the results presented on ICCD paper are running this method with NULL for the memory pool).
+ * The method returns 0 if a full decomposition was found and a negative value otherwise.
+ */
+extern int Dsc_Decompose(word * pTruth, const int nVarsInit, char * const pRes, word *pool);
+
+/**
+ * just free the memory pool
+ */
+extern void Dsc_free_pool(word * pool);
+
+int * Dsc_ComputeMatches( char * p );
+int Dsc_CountAnds_rec( char * pStr, char ** p, int * pMatches );
+extern int Dsc_CountAnds( char * pDsd );
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dsc/module.make b/src/opt/dsc/module.make
new file mode 100644
index 00000000..b2fd70c4
--- /dev/null
+++ b/src/opt/dsc/module.make
@@ -0,0 +1 @@
+SRC +=    src/opt/dsc/dsc.c