1 /**CFile**************************************************************** 2 3 FileName [cloud.h] 4 5 PackageName [Fast application-specific BDD package.] 6 7 Synopsis [Interface of the package.] 8 9 Author [Alan Mishchenko <alanmi@ece.pdx.edu>] 10 11 Affiliation [ECE Department. Portland State University, Portland, Oregon.] 12 13 Date [Ver. 1.0. Started - June 10, 2002.] 14 15 Revision [$Id: cloud.h,v 1.0 2002/06/10 03:00:00 alanmi Exp $] 16 17 ***********************************************************************/ 18 19 #ifndef ABC__aig__kit__cloud_h 20 #define ABC__aig__kit__cloud_h 21 22 23 #include <stdio.h> 24 #include <stdlib.h> 25 #include <assert.h> 26 27 #include "misc/util/abc_global.h" 28 29 30 31 ABC_NAMESPACE_HEADER_START 32 33 34 #ifdef _WIN32 35 #define inline __inline // compatible with MS VS 6.0 36 #endif 37 38 //////////////////////////////////////////////////////////////////////// 39 // n | 2^n || n | 2^n || n | 2^n || n | 2^n // 40 //====================================================================// 41 // 1 | 2 || 9 | 512 || 17 | 131,072 || 25 | 33,554,432 // 42 // 2 | 4 || 10 | 1,024 || 18 | 262,144 || 26 | 67,108,864 // 43 // 3 | 8 || 11 | 2,048 || 19 | 524,288 || 27 | 134,217,728 // 44 // 4 | 16 || 12 | 4,096 || 20 | 1,048,576 || 28 | 268,435,456 // 45 // 5 | 32 || 13 | 8,192 || 21 | 2,097,152 || 29 | 536,870,912 // 46 // 6 | 64 || 14 | 16,384 || 22 | 4,194,304 || 30 | 1,073,741,824 // 47 // 7 | 128 || 15 | 32,768 || 23 | 8,388,608 || 31 | 2,147,483,648 // 48 // 8 | 256 || 16 | 65,536 || 24 | 16,777,216 || 32 | 4,294,967,296 // 49 //////////////////////////////////////////////////////////////////////// 50 51 // data structure typedefs 52 typedef struct cloudManager CloudManager; 53 typedef unsigned CloudVar; 54 typedef unsigned CloudSign; 55 typedef struct cloudNode CloudNode; 56 typedef struct cloudCacheEntry1 CloudCacheEntry1; 57 typedef struct cloudCacheEntry2 CloudCacheEntry2; 58 typedef struct cloudCacheEntry3 CloudCacheEntry3; 59 60 // operation codes used to set up the cache 61 typedef enum { 62 CLOUD_OPER_AND, 63 CLOUD_OPER_XOR, 64 CLOUD_OPER_BDIFF, 65 CLOUD_OPER_LEQ 66 } CloudOper; 67 68 /* 69 // the number of operators using cache 70 static int CacheOperNum = 4; 71 72 // the ratio of cache size to the unique table size for each operator 73 static int CacheLogRatioDefault[4] = { 74 4, // CLOUD_OPER_AND, 75 8, // CLOUD_OPER_XOR, 76 8, // CLOUD_OPER_BDIFF, 77 8 // CLOUD_OPER_LEQ 78 }; 79 80 // the ratio of cache size to the unique table size for each operator 81 static int CacheSize[4] = { 82 2, // CLOUD_OPER_AND, 83 2, // CLOUD_OPER_XOR, 84 2, // CLOUD_OPER_BDIFF, 85 2 // CLOUD_OPER_LEQ 86 }; 87 */ 88 89 // data structure definitions 90 struct cloudManager // the fast bdd manager 91 { 92 // variables 93 int nVars; // the number of variables allocated 94 // bits 95 int bitsNode; // the number of bits used for the node 96 int bitsCache[4]; // default: bitsNode - CacheSizeRatio[i] 97 // shifts 98 int shiftUnique; // 8*sizeof(unsigned) - (bitsNode + 1) 99 int shiftCache[4]; // 8*sizeof(unsigned) - bitsCache[i] 100 // nodes 101 int nNodesAlloc; // 2 ^ (bitsNode + 1) 102 int nNodesLimit; // 2 ^ bitsNode 103 int nNodesCur; // the current number of nodes (including const1 and vars) 104 // signature 105 CloudSign nSignCur; 106 107 // statistics 108 int nMemUsed; // memory usage in bytes 109 // cache stats 110 int nUniqueHits; // hits in the unique table 111 int nUniqueMisses; // misses in the unique table 112 int nCacheHits; // hits in the caches 113 int nCacheMisses; // misses in the caches 114 // the number of steps through the hash table 115 int nUniqueSteps; 116 117 // tables 118 CloudNode * tUnique; // the unique table to store BDD nodes 119 120 // special nodes 121 CloudNode * pNodeStart; // the pointer to the first node 122 CloudNode * pNodeEnd; // the pointer to the first node out of the table 123 124 // constants and variables 125 CloudNode * one; // the one function 126 CloudNode * zero; // the zero function 127 CloudNode ** vars; // the elementary variables 128 129 // temporary storage for nodes 130 CloudNode ** ppNodes; 131 132 // caches 133 CloudCacheEntry2 * tCaches[20]; // caches 134 }; 135 136 struct cloudNode // representation of the node in the unique table 137 { 138 CloudSign s; // signature 139 CloudVar v; // variable 140 CloudNode * e; // negative cofactor 141 CloudNode * t; // positive cofactor 142 }; 143 struct cloudCacheEntry1 // one-argument cache 144 { 145 CloudSign s; // signature 146 CloudNode * a; // argument 1 147 CloudNode * r; // result 148 }; 149 struct cloudCacheEntry2 // the two-argument cache 150 { 151 CloudSign s; // signature 152 CloudNode * a; 153 CloudNode * b; 154 CloudNode * r; 155 }; 156 struct cloudCacheEntry3 // the three-argument cache 157 { 158 CloudSign s; // signature 159 CloudNode * a; 160 CloudNode * b; 161 CloudNode * c; 162 CloudNode * r; 163 }; 164 165 166 // parameters 167 #define CLOUD_NODE_BITS 23 168 169 #define CLOUD_CONST_INDEX ((unsigned)0x0fffffff) 170 #define CLOUD_MARK_ON ((unsigned)0x10000000) 171 #define CLOUD_MARK_OFF ((unsigned)0xefffffff) 172 173 // hash functions a la Buddy 174 #define cloudHashBuddy2(x,y,s) ((((x)+(y))*((x)+(y)+1)/2) & ((1<<(32-(s)))-1)) 175 #define cloudHashBuddy3(x,y,z,s) (cloudHashBuddy2((cloudHashBuddy2((x),(y),(s))),(z),(s)) & ((1<<(32-(s)))-1)) 176 // hash functions a la Cudd 177 #define DD_P1 12582917 178 #define DD_P2 4256249 179 #define DD_P3 741457 180 #define DD_P4 1618033999 181 #define cloudHashCudd2(f,g,s) ((((unsigned)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2) >> (s)) 182 #define cloudHashCudd3(f,g,h,s) (((((unsigned)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2 + (unsigned)(ABC_PTRUINT_T)(h)) * DD_P3) >> (s)) 183 184 // node complementation (using node) 185 #define Cloud_Regular(p) ((CloudNode*)(((ABC_PTRUINT_T)(p)) & ~01)) // get the regular node (w/o bubble) 186 #define Cloud_Not(p) ((CloudNode*)(((ABC_PTRUINT_T)(p)) ^ 01)) // complement the node 187 #define Cloud_NotCond(p,c) ((CloudNode*)(((ABC_PTRUINT_T)(p)) ^ (c))) // complement the node conditionally 188 #define Cloud_IsComplement(p) ((int)(((ABC_PTRUINT_T)(p)) & 01)) // check if complemented 189 // checking constants (using node) 190 #define Cloud_IsConstant(p) (((Cloud_Regular(p))->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX) 191 #define cloudIsConstant(p) (((p)->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX) 192 193 // retrieving values from the node (using node structure) 194 #define Cloud_V(p) ((Cloud_Regular(p))->v) 195 #define Cloud_E(p) ((Cloud_Regular(p))->e) 196 #define Cloud_T(p) ((Cloud_Regular(p))->t) 197 // retrieving values from the regular node (using node structure) 198 #define cloudV(p) ((p)->v) 199 #define cloudE(p) ((p)->e) 200 #define cloudT(p) ((p)->t) 201 // marking/unmarking (using node structure) 202 #define cloudNodeMark(p) ((p)->v |= CLOUD_MARK_ON) 203 #define cloudNodeUnmark(p) ((p)->v &= CLOUD_MARK_OFF) 204 #define cloudNodeIsMarked(p) ((int)((p)->v & CLOUD_MARK_ON)) 205 206 // cache lookups and inserts (using node) 207 #define cloudCacheLookup1(p,sign,f) (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (0)) 208 #define cloudCacheLookup2(p,sign,f,g) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (0)) 209 #define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (0)) 210 // cache inserts 211 #define cloudCacheInsert1(p,sign,f,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->r = (r))) 212 #define cloudCacheInsert2(p,sign,f,g,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->r = (r))) 213 #define cloudCacheInsert3(p,sign,f,g,h,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->c = (h)), ((p)->r = (r))) 214 215 //#define CLOUD_ASSERT(p) (assert((p) >= (dd->pNodeStart-1) && (p) < dd->pNodeEnd)) 216 #define CLOUD_ASSERT(p) assert((p) >= dd->tUnique && (p) < dd->tUnique+dd->nNodesAlloc) 217 218 //////////////////////////////////////////////////////////////////////// 219 /// FUNCTION DECLARATIONS /// 220 //////////////////////////////////////////////////////////////////////// 221 // starting/stopping 222 extern CloudManager * Cloud_Init( int nVars, int nBits ); 223 extern void Cloud_Quit( CloudManager * dd ); 224 extern void Cloud_Restart( CloudManager * dd ); 225 extern void Cloud_CacheAllocate( CloudManager * dd, CloudOper oper, int size ); 226 extern CloudNode * Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e ); 227 // support and node count 228 extern CloudNode * Cloud_Support( CloudManager * dd, CloudNode * n ); 229 extern int Cloud_SupportSize( CloudManager * dd, CloudNode * n ); 230 extern int Cloud_DagSize( CloudManager * dd, CloudNode * n ); 231 extern int Cloud_DagCollect( CloudManager * dd, CloudNode * n ); 232 extern int Cloud_SharingSize( CloudManager * dd, CloudNode * * pn, int nn ); 233 // cubes 234 extern CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * n ); 235 extern void Cloud_bddPrint( CloudManager * dd, CloudNode * Func ); 236 extern void Cloud_bddPrintCube( CloudManager * dd, CloudNode * Cube ); 237 // operations 238 extern CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g ); 239 extern CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g ); 240 // stats 241 extern void Cloud_PrintInfo( CloudManager * dd ); 242 extern void Cloud_PrintHashTable( CloudManager * dd ); 243 244 245 246 ABC_NAMESPACE_HEADER_END 247 248 249 250 #endif 251 252 //////////////////////////////////////////////////////////////////////// 253 /// END OF FILE /// 254 //////////////////////////////////////////////////////////////////////// 255