diff options
Diffstat (limited to 'src/aig/kit/cloud.h')
| -rw-r--r-- | src/aig/kit/cloud.h | 269 |
1 files changed, 269 insertions, 0 deletions
diff --git a/src/aig/kit/cloud.h b/src/aig/kit/cloud.h new file mode 100644 index 00000000..ac9d45f4 --- /dev/null +++ b/src/aig/kit/cloud.h @@ -0,0 +1,269 @@ +/**CFile**************************************************************** + + FileName [cloud.h] + + PackageName [Fast application-specific BDD package.] + + Synopsis [Interface of the package.] + + Author [Alan Mishchenko <alanmi@ece.pdx.edu>] + + Affiliation [ECE Department. Portland State University, Portland, Oregon.] + + Date [Ver. 1.0. Started - June 10, 2002.] + + Revision [$Id: cloud.h,v 1.0 2002/06/10 03:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CLOUD_H__ +#define __CLOUD_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +#include <stdio.h> +#include <stdlib.h> +#include <assert.h> +#include <time.h> + +#ifdef _WIN32 +#define inline __inline // compatible with MS VS 6.0 +#endif + +//////////////////////////////////////////////////////////////////////// +// n | 2^n || n | 2^n || n | 2^n || n | 2^n // +//====================================================================// +// 1 | 2 || 9 | 512 || 17 | 131,072 || 25 | 33,554,432 // +// 2 | 4 || 10 | 1,024 || 18 | 262,144 || 26 | 67,108,864 // +// 3 | 8 || 11 | 2,048 || 19 | 524,288 || 27 | 134,217,728 // +// 4 | 16 || 12 | 4,096 || 20 | 1,048,576 || 28 | 268,435,456 // +// 5 | 32 || 13 | 8,192 || 21 | 2,097,152 || 29 | 536,870,912 // +// 6 | 64 || 14 | 16,384 || 22 | 4,194,304 || 30 | 1,073,741,824 // +// 7 | 128 || 15 | 32,768 || 23 | 8,388,608 || 31 | 2,147,483,648 // +// 8 | 256 || 16 | 65,536 || 24 | 16,777,216 || 32 | 4,294,967,296 // +//////////////////////////////////////////////////////////////////////// + +// data structure typedefs +typedef struct cloudManager CloudManager; +typedef unsigned CloudVar; +typedef unsigned CloudSign; +typedef struct cloudNode CloudNode; +typedef struct cloudCacheEntry1 CloudCacheEntry1; +typedef struct cloudCacheEntry2 CloudCacheEntry2; +typedef struct cloudCacheEntry3 CloudCacheEntry3; + +// operation codes used to set up the cache +typedef enum { + CLOUD_OPER_AND, + CLOUD_OPER_XOR, + CLOUD_OPER_BDIFF, + CLOUD_OPER_LEQ +} CloudOper; + +/* +// the number of operators using cache +static int CacheOperNum = 4; + +// the ratio of cache size to the unique table size for each operator +static int CacheLogRatioDefault[4] = { + 4, // CLOUD_OPER_AND, + 8, // CLOUD_OPER_XOR, + 8, // CLOUD_OPER_BDIFF, + 8 // CLOUD_OPER_LEQ +}; + +// the ratio of cache size to the unique table size for each operator +static int CacheSize[4] = { + 2, // CLOUD_OPER_AND, + 2, // CLOUD_OPER_XOR, + 2, // CLOUD_OPER_BDIFF, + 2 // CLOUD_OPER_LEQ +}; +*/ + +// data structure definitions +struct cloudManager // the fast bdd manager +{ + // variables + int nVars; // the number of variables allocated + // bits + int bitsNode; // the number of bits used for the node + int bitsCache[4]; // default: bitsNode - CacheSizeRatio[i] + // shifts + int shiftUnique; // 8*sizeof(unsigned) - (bitsNode + 1) + int shiftCache[4]; // 8*sizeof(unsigned) - bitsCache[i] + // nodes + int nNodesAlloc; // 2 ^ (bitsNode + 1) + int nNodesLimit; // 2 ^ bitsNode + int nNodesCur; // the current number of nodes (including const1 and vars) + // signature + CloudSign nSignCur; + + // statistics + int nMemUsed; // memory usage in bytes + // cache stats + int nUniqueHits; // hits in the unique table + int nUniqueMisses; // misses in the unique table + int nCacheHits; // hits in the caches + int nCacheMisses; // misses in the caches + // the number of steps through the hash table + int nUniqueSteps; + + // tables + CloudNode * tUnique; // the unique table to store BDD nodes + + // special nodes + CloudNode * pNodeStart; // the pointer to the first node + CloudNode * pNodeEnd; // the pointer to the first node out of the table + + // constants and variables + CloudNode * one; // the one function + CloudNode * zero; // the zero function + CloudNode ** vars; // the elementary variables + + // temporary storage for nodes + CloudNode ** ppNodes; + + // caches + CloudCacheEntry2 * tCaches[20]; // caches +}; + +struct cloudNode // representation of the node in the unique table +{ + CloudSign s; // signature + CloudVar v; // variable + CloudNode * e; // negative cofactor + CloudNode * t; // positive cofactor +}; +struct cloudCacheEntry1 // one-argument cache +{ + CloudSign s; // signature + CloudNode * a; // argument 1 + CloudNode * r; // result +}; +struct cloudCacheEntry2 // the two-argument cache +{ + CloudSign s; // signature + CloudNode * a; + CloudNode * b; + CloudNode * r; +}; +struct cloudCacheEntry3 // the three-argument cache +{ + CloudSign s; // signature + CloudNode * a; + CloudNode * b; + CloudNode * c; + CloudNode * r; +}; + + +// parameters +#define CLOUD_NODE_BITS 23 +#define CLOUD_ONE ((unsigned)0x00000001) +#define CLOUD_NOT_ONE ((unsigned)0xfffffffe) +#define CLOUD_VOID ((unsigned)0x00000000) + +#define CLOUD_CONST_INDEX ((unsigned)0x0fffffff) +#define CLOUD_MARK_ON ((unsigned)0x10000000) +#define CLOUD_MARK_OFF ((unsigned)0xefffffff) + +// hash functions a la Buddy +#define cloudHashBuddy2(x,y,s) ((((x)+(y))*((x)+(y)+1)/2) & ((1<<(32-(s)))-1)) +#define cloudHashBuddy3(x,y,z,s) (cloudHashBuddy2((cloudHashBuddy2((x),(y),(s))),(z),(s)) & ((1<<(32-(s)))-1)) +// hash functions a la Cudd +#define DD_P1 12582917 +#define DD_P2 4256249 +#define DD_P3 741457 +#define DD_P4 1618033999 +#define cloudHashCudd2(f,g,s) ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s)) +#define cloudHashCudd3(f,g,h,s) (((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2 + (unsigned)(h)) * DD_P3) >> (s)) + +// node complementation (using node) +#define Cloud_Regular(p) ((CloudNode*)(((unsigned)(p)) & CLOUD_NOT_ONE)) // get the regular node (w/o bubble) +#define Cloud_Not(p) ((CloudNode*)(((unsigned)(p)) ^ CLOUD_ONE)) // complement the node +#define Cloud_NotCond(p,c) (((int)(c))? Cloud_Not(p):(p)) // complement the node conditionally +#define Cloud_IsComplement(p) ((int)(((unsigned)(p)) & CLOUD_ONE)) // check if complemented +// checking constants (using node) +#define Cloud_IsConstant(p) (((Cloud_Regular(p))->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX) +#define cloudIsConstant(p) (((p)->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX) + +// retrieving values from the node (using node structure) +#define Cloud_V(p) ((Cloud_Regular(p))->v) +#define Cloud_E(p) ((Cloud_Regular(p))->e) +#define Cloud_T(p) ((Cloud_Regular(p))->t) +// retrieving values from the regular node (using node structure) +#define cloudV(p) ((p)->v) +#define cloudE(p) ((p)->e) +#define cloudT(p) ((p)->t) +// marking/unmarking (using node structure) +#define cloudNodeMark(p) ((p)->v |= CLOUD_MARK_ON) +#define cloudNodeUnmark(p) ((p)->v &= CLOUD_MARK_OFF) +#define cloudNodeIsMarked(p) ((int)((p)->v & CLOUD_MARK_ON)) + +// cache lookups and inserts (using node) +#define cloudCacheLookup1(p,sign,f) (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (CLOUD_VOID)) +#define cloudCacheLookup2(p,sign,f,g) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (CLOUD_VOID)) +#define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (CLOUD_VOID)) +// cache inserts +#define cloudCacheInsert1(p,sign,f,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->r = (r))) +#define cloudCacheInsert2(p,sign,f,g,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->r = (r))) +#define cloudCacheInsert3(p,sign,f,g,h,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->c = (h)), ((p)->r = (r))) + +//#define CLOUD_ASSERT(p) (assert((p) >= (dd->pNodeStart-1) && (p) < dd->pNodeEnd)) +#define CLOUD_ASSERT(p) assert((p) >= dd->tUnique && (p) < dd->tUnique+dd->nNodesAlloc) + +// utility macros +#ifndef ALLOC +#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num))) +#endif + +#ifndef CALLOC +#define CALLOC(type, num) ((type *) calloc((num), sizeof(type))) +#endif + +#ifndef FREE +#define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0) +#endif + +#ifndef PRT +#define PRT(a,t) fprintf( stdout, "%s = ", (a)); printf( "%.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) ) +#endif + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// +// starting/stopping +extern CloudManager * Cloud_Init( int nVars, int nBits ); +extern void Cloud_Quit( CloudManager * dd ); +extern void Cloud_Restart( CloudManager * dd ); +extern void Cloud_CacheAllocate( CloudManager * dd, CloudOper oper, int size ); +extern CloudNode * Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e ); +// support and node count +extern CloudNode * Cloud_Support( CloudManager * dd, CloudNode * n ); +extern int Cloud_SupportSize( CloudManager * dd, CloudNode * n ); +extern int Cloud_DagSize( CloudManager * dd, CloudNode * n ); +extern int Cloud_DagCollect( CloudManager * dd, CloudNode * n ); +extern int Cloud_SharingSize( CloudManager * dd, CloudNode * * pn, int nn ); +// cubes +extern CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * n ); +extern void Cloud_bddPrint( CloudManager * dd, CloudNode * Func ); +extern void Cloud_bddPrintCube( CloudManager * dd, CloudNode * Cube ); +// operations +extern CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g ); +extern CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g ); +// stats +extern void Cloud_PrintInfo( CloudManager * dd ); +extern void Cloud_PrintHashTable( CloudManager * dd ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// |