diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 3 | ||||
| -rw-r--r-- | src/base/abci/abcDec.c | 22 | ||||
| -rw-r--r-- | src/opt/dsc/dsc.c | 526 | ||||
| -rw-r--r-- | src/opt/dsc/dsc.h | 91 | ||||
| -rw-r--r-- | src/opt/dsc/module.make | 1 |
6 files changed, 643 insertions, 2 deletions
@@ -22,7 +22,7 @@ MODULES := \ src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \ src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \ src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \ - src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/sfm \ + src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm \ src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \ src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \ src/bool/rsb src/bool/rpo \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 953a6c6a..ffcd5054 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -6212,6 +6212,9 @@ usage: Abc_Print( -2, "\t 3: disjoint-support decomposition with cofactoring\n" ); Abc_Print( -2, "\t 4: updated disjoint-support decomposition with cofactoring\n" ); Abc_Print( -2, "\t 5: enumerating decomposable variable sets\n" ); + Abc_Print( -2, "\t 6: disjoint-support decomposition with cofactoring and boolean difference analysis\n" ); + Abc_Print( -2, "\t from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,\n"); + Abc_Print( -2, "\t \"Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis,\" ICCD'15.\n" ); Abc_Print( -2, "\t-N <num> : the number of support variables (binary files only) [default = unused]\n" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c index 919a46de..8bb04f16 100644 --- a/src/base/abci/abcDec.c +++ b/src/base/abci/abcDec.c @@ -26,6 +26,7 @@ #include "bool/kit/kit.h" #include "opt/dau/dau.h" #include "misc/util/utilTruth.h" +#include "opt/dsc/dsc.h" ABC_NAMESPACE_IMPL_START @@ -484,6 +485,8 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose ) pAlgoName = "fast DSD"; else if ( DecType == 5 ) pAlgoName = "analysis"; + else if ( DecType == 6 ) + pAlgoName = "DSD ICCD'15"; if ( pAlgoName ) printf( "Applying %-10s to %8d func%s of %2d vars... ", @@ -577,6 +580,23 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose ) if ( fVerbose ) printf( "\n" ); } + } else if ( DecType == 6 ) + { + char pDsd[DSC_MAX_STR]; + /* memory pool with a capacity of storing 3*nVars + truth-tables for negative and positive cofactors and + the boolean difference for each input variable */ + word *mem_pool = Dsc_alloc_pool(p->nVars); + for ( i = 0; i < p->nFuncs; i++ ) + { + if ( fVerbose ) + printf( "%7d : ", i ); + Dsc_Decompose(p->pFuncs[i], p->nVars, pDsd, mem_pool); + if ( fVerbose ) + printf( "%s\n", pDsd[0] ? pDsd : "NULL"); + nNodes += Dsc_CountAnds( pDsd ); + } + Dsc_free_pool(mem_pool); } else assert( 0 ); @@ -629,7 +649,7 @@ int Abc_DecTest( char * pFileName, int DecType, int nVarNum, int fVerbose ) printf( "Using truth tables from file \"%s\"...\n", pFileName ); if ( DecType == 0 ) { if ( nVarNum < 0 ) Abc_TtStoreTest( pFileName ); } - else if ( DecType >= 1 && DecType <= 5 ) + else if ( DecType >= 1 && DecType <= 6 ) Abc_TruthDecTest( pFileName, DecType, nVarNum, fVerbose ); else printf( "Unknown decomposition type value (%d).\n", DecType ); 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 |