ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
dsdCheck.c File Reference
#include "dsdInt.h"
Include dependency graph for dsdCheck.c:

Go to the source code of this file.

Classes

struct  Dsd_Cache_t_
 
struct  Dsd_Entry_t_
 

Typedefs

typedef typedefABC_NAMESPACE_IMPL_START struct Dsd_Cache_t_ Dds_Cache_t
 DECLARATIONS ///.
 
typedef struct Dsd_Entry_t_ Dsd_Entry_t
 

Functions

void Dsd_CheckCacheAllocate (int nEntries)
 FUNCTION DEFINITIONS ///.
 
void Dsd_CheckCacheDeallocate ()
 
void Dsd_CheckCacheClear ()
 
int Dsd_CheckRootFunctionIdentity (DdManager *dd, DdNode *bF1, DdNode *bF2, DdNode *bC1, DdNode *bC2)
 

Typedef Documentation

◆ Dds_Cache_t

typedef typedefABC_NAMESPACE_IMPL_START struct Dsd_Cache_t_ Dds_Cache_t

DECLARATIONS ///.

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

FileName [dsdCheck.c]

PackageName [DSD: Disjoint-support decomposition package.]

Synopsis [Procedures to check the identity of root functions.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id
dsdCheck.c,v 1.0 2002/22/09 00:00:00 alanmi Exp

]

Definition at line 28 of file dsdCheck.c.

◆ Dsd_Entry_t

typedef struct Dsd_Entry_t_ Dsd_Entry_t

Definition at line 29 of file dsdCheck.c.

Function Documentation

◆ Dsd_CheckCacheAllocate()

void Dsd_CheckCacheAllocate ( int nEntries)

FUNCTION DEFINITIONS ///.

PARAMETERS ///.

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

Synopsis [(Re)allocates the local cache.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file dsdCheck.c.

64{
65 int nRequested;
66
67 pCache = ABC_ALLOC( Dds_Cache_t, 1 );
68 memset( pCache, 0, sizeof(Dds_Cache_t) );
69
70 // check what is the size of the current cache
71 nRequested = Abc_PrimeCudd( nEntries );
72 if ( pCache->nTableSize != nRequested )
73 { // the current size is different
74 // deallocate the old, allocate the new
75 if ( pCache->nTableSize )
77 // allocate memory for the hash table
78 pCache->nTableSize = nRequested;
79 pCache->pTable = ABC_ALLOC( Dsd_Entry_t, nRequested );
80 }
81 // otherwise, there is no need to allocate, just clean
83// printf( "\nThe number of allocated cache entries = %d.\n\n", pCache->nTableSize );
84}
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
void Dsd_CheckCacheDeallocate()
Definition dsdCheck.c:97
typedefABC_NAMESPACE_IMPL_START struct Dsd_Cache_t_ Dds_Cache_t
DECLARATIONS ///.
Definition dsdCheck.c:28
void Dsd_CheckCacheClear()
Definition dsdCheck.c:114
struct Dsd_Entry_t_ Dsd_Entry_t
Definition dsdCheck.c:29
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dsd_CheckCacheClear()

void Dsd_CheckCacheClear ( )

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

Synopsis [Clears the local cache.]

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file dsdCheck.c.

115{
116 int i;
117 for ( i = 0; i < pCache->nTableSize; i++ )
118 pCache->pTable[0].bX[0] = NULL;
119}
Here is the caller graph for this function:

◆ Dsd_CheckCacheDeallocate()

void Dsd_CheckCacheDeallocate ( )

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

Synopsis [Deallocates the local cache.]

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file dsdCheck.c.

98{
99 ABC_FREE( pCache->pTable );
100 ABC_FREE( pCache );
101}
#define ABC_FREE(obj)
Definition abc_global.h:267
Here is the caller graph for this function:

◆ Dsd_CheckRootFunctionIdentity()

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.

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