dsdInt.h File Reference

#include "misc/extra/extraBdd.h"
#include "dsd.h"

Go to the source code of this file.

Data Structures
struct	Dsd_Manager_t_
	STRUCTURE DEFINITIONS ///. More...
struct	Dsd_Node_t_

Macros
#define	MAXINPUTS   1000
	MACRO DEFINITIONS ///. More...

Functions
void	Dsd_CheckCacheAllocate (int nEntries)
	PARAMETERS ///. More...
void	Dsd_CheckCacheDeallocate ()
void	Dsd_CheckCacheClear ()
int	Dsd_CheckRootFunctionIdentity (DdManager *dd, DdNode *bF1, DdNode *bF2, DdNode *bC1, DdNode *bC2)
Dsd_Node_t *	Dsd_TreeNodeCreate (int Type, int nDecs, int BlockNum)
	FUNCTION DEFINITIONS ///. More...
void	Dsd_TreeNodeDelete (DdManager *dd, Dsd_Node_t *pNode)
void	Dsd_TreeUnmark (Dsd_Manager_t *dMan)
DdNode *	Dsd_TreeGetPrimeFunctionOld (DdManager *dd, Dsd_Node_t *pNode, int fRemap)

Variables
ABC_NAMESPACE_HEADER_START typedef unsigned char	byte
	TYPEDEF DEFINITIONS ///. More...

Macro Definition Documentation

#define MAXINPUTS   1000

MACRO DEFINITIONS ///.

Definition at line 69 of file dsdInt.h.

Function Documentation

void Dsd_CheckCacheAllocate

(

int

nEntries

)

PARAMETERS ///.

FUNCTION DECLARATIONS ///

PARAMETERS ///.

Function********************************************************************

Synopsis [(Re)allocates the local cache.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file dsdCheck.c.

{
    int nRequested;

    pCache = ABC_ALLOC( Dds_Cache_t, 1 );
    memset( pCache, 0, sizeof(Dds_Cache_t) );

    // check what is the size of the current cache
    nRequested = Abc_PrimeCudd( nEntries );
    if ( pCache->nTableSize != nRequested )
    { // the current size is different
        // deallocate the old, allocate the new
        if ( pCache->nTableSize )
            Dsd_CheckCacheDeallocate();
        // allocate memory for the hash table
        pCache->nTableSize = nRequested;
        pCache->pTable = ABC_ALLOC( Dsd_Entry_t, nRequested );
    }
    // otherwise, there is no need to allocate, just clean
    Dsd_CheckCacheClear();
//  printf( "\nThe number of allocated cache entries = %d.\n\n", pCache->nTableSize );
}

void Dsd_CheckCacheClear

(

)

Function********************************************************************

Synopsis [Clears the local cache.]

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file dsdCheck.c.

{
    int i;
    for ( i = 0; i < pCache->nTableSize; i++ )
        pCache->pTable[0].bX[0] = NULL;
}

void Dsd_CheckCacheDeallocate

(

)

Function********************************************************************

Synopsis [Deallocates the local cache.]

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file dsdCheck.c.

{
    ABC_FREE( pCache->pTable );
    ABC_FREE( pCache );
}

int Dsd_CheckRootFunctionIdentity	(	DdManager *	dd,
		DdNode *	bF1,
		DdNode *	bF2,
		DdNode *	bC1,
		DdNode *	bC2
	)

Function********************************************************************

Synopsis [Checks whether it is true that bF1(bC1=0) == bF2(bC2=0).]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file dsdCheck.c.

{
    int RetValue;
//  pCache->nSuccess = 0;
//  pCache->nFailure = 0;
    RetValue = Dsd_CheckRootFunctionIdentity_rec(dd, bF1, bF2, bC1, bC2);
//  printf( "Cache success = %d. Cache failure = %d.\n", pCache->nSuccess, pCache->nFailure );
    return RetValue;
}

DdNode* Dsd_TreeGetPrimeFunctionOld	(	DdManager *	dd,
		Dsd_Node_t *	pNode,
		int	fRemap
	)

Function*************************************************************

Synopsis [Retuns the function of one node of the decomposition tree.]

Description [This is the old procedure. It is now superceded by the procedure Dsd_TreeGetPrimeFunction() found in "dsdLocal.c".]

SideEffects []

SeeAlso []

Definition at line 1120 of file dsdTree.c.

{
    DdNode * bCof0,  * bCof1, * bCube0, * bCube1, * bNewFunc, * bTemp;
    int i;
    static int Permute[MAXINPUTS];

    assert( pNode );
    assert( !Dsd_IsComplement( pNode ) );
    assert( pNode->Type == DSD_NODE_PRIME );

    // transform the function of this block to depend on inputs
    // corresponding to the formal inputs

    // first, substitute those inputs that have some blocks associated with them
    // second, remap the inputs to the top of the manager (then, it is easy to output them)

    // start the function
    bNewFunc = pNode->G;  Cudd_Ref( bNewFunc );
    // go over all primary inputs
    for ( i = 0; i < pNode->nDecs; i++ )
    if ( pNode->pDecs[i]->Type != DSD_NODE_BUF ) // remap only if it is not the buffer
    {
        bCube0 = Extra_bddFindOneCube( dd, Cudd_Not(pNode->pDecs[i]->G) );  Cudd_Ref( bCube0 );
        bCof0 = Cudd_Cofactor( dd, bNewFunc, bCube0 );                     Cudd_Ref( bCof0 );
        Cudd_RecursiveDeref( dd, bCube0 );

        bCube1 = Extra_bddFindOneCube( dd,          pNode->pDecs[i]->G  );  Cudd_Ref( bCube1 );
        bCof1 = Cudd_Cofactor( dd, bNewFunc, bCube1 );                     Cudd_Ref( bCof1 );
        Cudd_RecursiveDeref( dd, bCube1 );

        Cudd_RecursiveDeref( dd, bNewFunc );

        // use the variable in the i-th level of the manager
//      bNewFunc = Cudd_bddIte( dd, dd->vars[dd->invperm[i]],bCof1,bCof0 );     Cudd_Ref( bNewFunc );
        // use the first variale in the support of the component
        bNewFunc = Cudd_bddIte( dd, dd->vars[pNode->pDecs[i]->S->index],bCof1,bCof0 );     Cudd_Ref( bNewFunc );
        Cudd_RecursiveDeref( dd, bCof0 );
        Cudd_RecursiveDeref( dd, bCof1 );
    }

    if ( fRemap )
    {
        // remap the function to the top of the manager
        // remap the function to the first variables of the manager
        for ( i = 0; i < pNode->nDecs; i++ )
    //      Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i];
            Permute[ pNode->pDecs[i]->S->index ] = i;

        bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, Permute );   Cudd_Ref( bNewFunc );
        Cudd_RecursiveDeref( dd, bTemp );
    }

    Cudd_Deref( bNewFunc );
    return bNewFunc;
}

Dsd_Node_t* Dsd_TreeNodeCreate	(	int	Type,
		int	nDecs,
		int	BlockNum
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Create the DSD node.]

Description []

SideEffects []

SeeAlso []

Definition at line 61 of file dsdTree.c.

{
    // allocate memory for this node 
    Dsd_Node_t * p = (Dsd_Node_t *) ABC_ALLOC( char, sizeof(Dsd_Node_t) );
    memset( p, 0, sizeof(Dsd_Node_t) );
    p->Type       = (Dsd_Type_t)Type;       // the type of this block
    p->nDecs      = nDecs;                  // the number of decompositions
    if ( p->nDecs )
    {
        p->pDecs      = (Dsd_Node_t **) ABC_ALLOC( char, p->nDecs * sizeof(Dsd_Node_t *) );
        p->pDecs[0]   = NULL;
    }
    return p;
}

void Dsd_TreeNodeDelete	(	DdManager *	dd,
		Dsd_Node_t *	pNode
	)

Function*************************************************************

Synopsis [Frees the DSD node.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file dsdTree.c.

{
    if ( pNode->G )  Cudd_RecursiveDeref( dd, pNode->G );
    if ( pNode->S )  Cudd_RecursiveDeref( dd, pNode->S );
    ABC_FREE( pNode->pDecs );
    ABC_FREE( pNode );
}

void Dsd_TreeUnmark

(

Dsd_Manager_t *

pDsdMan

)

Function*************************************************************

Synopsis [Unmarks the decomposition tree.]

Description [This function assumes that originally pNode->nVisits are set to zero!]

SideEffects []

SeeAlso []

Definition at line 107 of file dsdTree.c.

{
    int i;
    for ( i = 0; i < pDsdMan->nRoots; i++ )
        Dsd_TreeUnmark_rec( Dsd_Regular( pDsdMan->pRoots[i] ) );
}

Variable Documentation

ABC_NAMESPACE_HEADER_START typedef unsigned char byte

TYPEDEF DEFINITIONS ///.

CFile****************************************************************

FileName [dsdInt.h]

PackageName [DSD: Disjoint-support decomposition package.]

Synopsis [Internal declarations of the package.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 8.0. Started - September 22, 2003.]

Revision [

Id:

dsdInt.h,v 1.0 2002/22/09 00:00:00 alanmi Exp

]

Definition at line 33 of file dsdInt.h.