dsc.h File Reference

#include <stdio.h>
#include <string.h>
#include "misc/util/abc_global.h"

Include dependency graph for dsc.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros
#define	DSC_MAX_VAR   16
	INCLUDES ///.
#define	DSC_MAX_STR   DSC_MAX_VAR << 2

Functions
word *	Dsc_alloc_pool (int nVars)
	BASIC TYPES ///.
int	Dsc_Decompose (word *pTruth, const int nVarsInit, char *const pRes, word *pool)
void	Dsc_free_pool (word *pool)
int *	Dsc_ComputeMatches (char *p)
int	Dsc_CountAnds_rec (char *pStr, char **p, int *pMatches)
int	Dsc_CountAnds (char *pDsd)

Macro Definition Documentation

DSC_MAX_STR

#define DSC_MAX_STR   DSC_MAX_VAR << 2

Definition at line 41 of file dsc.h.

DSC_MAX_VAR

#define DSC_MAX_VAR   16

INCLUDES ///.

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

] PARAMETERS ///

Definition at line 40 of file dsc.h.

Function Documentation

Dsc_alloc_pool()

word * Dsc_alloc_pool ( int nVars )

extern

BASIC TYPES ///.

MACRO DEFINITIONS /// FUNCTION DECLARATIONS /// memory allocator with a capacity of storing 3*nVars truth-tables for negative and positive cofactors and the boolean difference for each input variable

memory allocator with a capacity of storing 3*nVars truth-tables for negative and positive cofactors and the boolean difference for each input variable

Definition at line 290 of file dsc.c.

                                        {
    return ABC_ALLOC(word, 3 * Abc_TtWordNum(nVars) * nVars);
}

Here is the caller graph for this function:

Dsc_ComputeMatches()

int * Dsc_ComputeMatches

(

char *

p

)

Function************************************************************* Synopsis [DSD formula manipulation.] Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]

Definition at line 450 of file dsc.c.

{
    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;
}

Here is the caller graph for this function:

Dsc_CountAnds()

int Dsc_CountAnds ( char * pDsd )

extern

Function************************************************************* Synopsis [DSD formula manipulation.] Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]

Definition at line 513 of file dsc.c.

{
    if ( pDsd[1] == 0 )
        return 0;
    return Dsc_CountAnds_rec( pDsd, &pDsd, Dsc_ComputeMatches(pDsd) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dsc_CountAnds_rec()

int Dsc_CountAnds_rec	(	char *	pStr,
		char **	p,
		int *	pMatches )

Function************************************************************* Synopsis [DSD formula manipulation.] Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]

Definition at line 472 of file dsc.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dsc_Decompose()

int Dsc_Decompose ( word * pTruth, const int nVarsInit, char *const pRes, word * pool )

extern

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.

Definition at line 311 of file dsc.c.

                                                                                            {
    const int TRUTH_WORDS = Abc_TtWordNum(nVarsInit);
    const int NEED_POOL_ALLOC = (pool == NULL);
 
    Dsc_node_t nodes[DSC_MAX_VAR];
    Dsc_node_t *newNodes[DSC_MAX_VAR];
    Dsc_node_t *oldNodes[DSC_MAX_VAR];
 
    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
    int n = 0; // n will represent the number of current nodes (i.e. support)
 
    pRes[0] = '\0';
    pRes[1] = '\0';
 
    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;
        }
    }
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Dsc_free_pool()

void Dsc_free_pool ( word * pool )

extern

just free the memory pool

Definition at line 297 of file dsc.c.

                                       {
    ABC_FREE(pool);
}

Here is the caller graph for this function: