[13] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [calBddManager.c] |
---|
| 4 | |
---|
| 5 | PackageName [cal] |
---|
| 6 | |
---|
| 7 | Synopsis [Routines for maintaing the manager and creating |
---|
| 8 | variables etc.] |
---|
| 9 | |
---|
| 10 | Description [] |
---|
| 11 | |
---|
| 12 | SeeAlso [optional] |
---|
| 13 | |
---|
| 14 | Author [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 15 | Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 16 | ] |
---|
| 17 | |
---|
| 18 | Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. |
---|
| 19 | All rights reserved. |
---|
| 20 | |
---|
| 21 | Permission is hereby granted, without written agreement and without license |
---|
| 22 | or royalty fees, to use, copy, modify, and distribute this software and its |
---|
| 23 | documentation for any purpose, provided that the above copyright notice and |
---|
| 24 | the following two paragraphs appear in all copies of this software. |
---|
| 25 | |
---|
| 26 | IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR |
---|
| 27 | DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT |
---|
| 28 | OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF |
---|
| 29 | CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. |
---|
| 30 | |
---|
| 31 | THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, |
---|
| 32 | INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND |
---|
| 33 | FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN |
---|
| 34 | "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE |
---|
| 35 | MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] |
---|
| 36 | |
---|
| 37 | Revision [$Id: calBddManager.c,v 1.9 2002/09/21 20:39:24 fabio Exp $] |
---|
| 38 | |
---|
| 39 | ******************************************************************************/ |
---|
| 40 | |
---|
| 41 | #include "calInt.h" |
---|
| 42 | |
---|
| 43 | /*---------------------------------------------------------------------------*/ |
---|
| 44 | /* Constant declarations */ |
---|
| 45 | /*---------------------------------------------------------------------------*/ |
---|
| 46 | |
---|
| 47 | /*---------------------------------------------------------------------------*/ |
---|
| 48 | /* Type declarations */ |
---|
| 49 | /*---------------------------------------------------------------------------*/ |
---|
| 50 | |
---|
| 51 | /*---------------------------------------------------------------------------*/ |
---|
| 52 | /* Stucture declarations */ |
---|
| 53 | /*---------------------------------------------------------------------------*/ |
---|
| 54 | |
---|
| 55 | |
---|
| 56 | /*---------------------------------------------------------------------------*/ |
---|
| 57 | /* Variable declarations */ |
---|
| 58 | /*---------------------------------------------------------------------------*/ |
---|
| 59 | unsigned long calPrimes[] = |
---|
| 60 | { |
---|
| 61 | 1, |
---|
| 62 | 2, |
---|
| 63 | 3, |
---|
| 64 | 7, |
---|
| 65 | 13, |
---|
| 66 | 23, |
---|
| 67 | 59, |
---|
| 68 | 113, |
---|
| 69 | 241, |
---|
| 70 | 503, |
---|
| 71 | 1019, |
---|
| 72 | 2039, |
---|
| 73 | 4091, |
---|
| 74 | 8179, |
---|
| 75 | 11587, |
---|
| 76 | 16369, |
---|
| 77 | 23143, |
---|
| 78 | 32749, |
---|
| 79 | 46349, |
---|
| 80 | 65521, |
---|
| 81 | 92683, |
---|
| 82 | 131063, |
---|
| 83 | 185363, |
---|
| 84 | 262139, |
---|
| 85 | 330287, |
---|
| 86 | 416147, |
---|
| 87 | 524269, |
---|
| 88 | 660557, |
---|
| 89 | 832253, |
---|
| 90 | 1048571, |
---|
| 91 | 1321109, |
---|
| 92 | 1664501, |
---|
| 93 | 2097143, |
---|
| 94 | 2642201, |
---|
| 95 | 3328979, |
---|
| 96 | 4194287, |
---|
| 97 | 5284393, |
---|
| 98 | 6657919, |
---|
| 99 | 8388593, |
---|
| 100 | 10568797, |
---|
| 101 | 13315831, |
---|
| 102 | 16777199, |
---|
| 103 | 33554393, |
---|
| 104 | 67108859, |
---|
| 105 | 134217689, |
---|
| 106 | 268435399, |
---|
| 107 | 536870879, |
---|
| 108 | 1073741789, |
---|
| 109 | 2147483629 |
---|
| 110 | }; |
---|
| 111 | |
---|
| 112 | /*---------------------------------------------------------------------------*/ |
---|
| 113 | /* Macro declarations */ |
---|
| 114 | /*---------------------------------------------------------------------------*/ |
---|
| 115 | #define CalBddManagerGetNodeManager(bddManager, id) \ |
---|
| 116 | bddManager->nodeManagerArray[id] |
---|
| 117 | |
---|
| 118 | |
---|
| 119 | /**AutomaticStart*************************************************************/ |
---|
| 120 | |
---|
| 121 | /*---------------------------------------------------------------------------*/ |
---|
| 122 | /* Static function prototypes */ |
---|
| 123 | /*---------------------------------------------------------------------------*/ |
---|
| 124 | |
---|
| 125 | static void BddDefaultTransformFn(Cal_BddManager_t * bddManager, CalAddress_t value1, CalAddress_t value2, CalAddress_t * result1, CalAddress_t * result2, Cal_Pointer_t pointer); |
---|
| 126 | #ifdef CALBDDMANAGER |
---|
| 127 | static int CalBddManagerPrint(Cal_BddManager_t *bddManager); |
---|
| 128 | #endif /* CALBDDMANAGER */ |
---|
| 129 | |
---|
| 130 | /**AutomaticEnd***************************************************************/ |
---|
| 131 | |
---|
| 132 | |
---|
| 133 | /*---------------------------------------------------------------------------*/ |
---|
| 134 | /* Definition of exported functions */ |
---|
| 135 | /*---------------------------------------------------------------------------*/ |
---|
| 136 | /**Function******************************************************************** |
---|
| 137 | |
---|
| 138 | Synopsis [Creates and initializes a new BDD manager.] |
---|
| 139 | |
---|
| 140 | Description [Initializes and allocates fields of the BDD manager. Some of the |
---|
| 141 | fields are initialized for maxNumVars+1 or numVars+1, whereas some of them are |
---|
| 142 | initialized for maxNumVars or numVars. The first kind of fields are associated |
---|
| 143 | with the id of a variable and the second ones are with the index of the |
---|
| 144 | variable.] |
---|
| 145 | |
---|
| 146 | SideEffects [None] |
---|
| 147 | |
---|
| 148 | SeeAlso [Cal_BddManagerQuit] |
---|
| 149 | |
---|
| 150 | ******************************************************************************/ |
---|
| 151 | Cal_BddManager |
---|
| 152 | Cal_BddManagerInit(void) |
---|
| 153 | { |
---|
| 154 | Cal_BddManager_t *bddManager; |
---|
| 155 | int i; |
---|
| 156 | CalBddNode_t *bddNode; |
---|
| 157 | Cal_Bdd_t resultBdd; |
---|
| 158 | |
---|
| 159 | |
---|
| 160 | bddManager = Cal_MemAlloc(Cal_BddManager_t, 1); |
---|
| 161 | |
---|
| 162 | bddManager->numVars = 0; |
---|
| 163 | |
---|
| 164 | bddManager->maxNumVars = 30; |
---|
| 165 | |
---|
| 166 | bddManager->varBdds = Cal_MemAlloc(Cal_Bdd_t, bddManager->maxNumVars+1); |
---|
| 167 | |
---|
| 168 | bddManager->pageManager1 = CalPageManagerInit(4); |
---|
| 169 | bddManager->pageManager2 = CalPageManagerInit(NUM_PAGES_PER_SEGMENT); |
---|
| 170 | |
---|
| 171 | bddManager->nodeManagerArray = Cal_MemAlloc(CalNodeManager_t*, bddManager->maxNumVars+1); |
---|
| 172 | |
---|
| 173 | bddManager->nodeManagerArray[0] = CalNodeManagerInit(bddManager->pageManager1); |
---|
| 174 | bddManager->uniqueTable = Cal_MemAlloc(CalHashTable_t *, |
---|
| 175 | bddManager->maxNumVars+1); |
---|
| 176 | bddManager->uniqueTable[0] = CalHashTableInit(bddManager, 0); |
---|
| 177 | |
---|
| 178 | /* Constant One */ |
---|
| 179 | CalBddPutBddId(bddManager->bddOne, CAL_BDD_CONST_ID); |
---|
| 180 | CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], bddNode); |
---|
| 181 | CalBddPutBddNode(bddManager->bddOne, bddNode); |
---|
| 182 | /* ~0x0 put so that the node is not mistaken for forwarded node */ |
---|
| 183 | CalBddPutThenBddNode(bddManager->bddOne, (CalBddNode_t *)~0x0); |
---|
| 184 | CalBddPutElseBddNode(bddManager->bddOne, (CalBddNode_t *)~0x0); |
---|
| 185 | CalBddPutRefCount(bddManager->bddOne, CAL_MAX_REF_COUNT); |
---|
| 186 | CalBddNot(bddManager->bddOne, bddManager->bddZero); |
---|
| 187 | |
---|
| 188 | /* Create a user BDD */ |
---|
| 189 | CalHashTableAddDirectAux(bddManager->uniqueTable[0], bddManager->bddOne, |
---|
| 190 | bddManager->bddOne, &resultBdd); |
---|
| 191 | CalBddPutRefCount(resultBdd, CAL_MAX_REF_COUNT); |
---|
| 192 | bddManager->userOneBdd = CalBddGetBddNode(resultBdd); |
---|
| 193 | bddManager->userZeroBdd = CalBddNodeNot(bddManager->userOneBdd); |
---|
| 194 | |
---|
| 195 | /* Null BDD */ |
---|
| 196 | CalBddPutBddId(bddManager->bddNull, CAL_BDD_NULL_ID); |
---|
| 197 | CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], bddNode); |
---|
| 198 | CalBddPutBddNode(bddManager->bddNull, bddNode); |
---|
| 199 | /* ~0x10 put so that the node is not mistaken for forwarded node or |
---|
| 200 | the constant nodes. */ |
---|
| 201 | CalBddPutThenBddNode(bddManager->bddNull, (CalBddNode_t *)~0x10); |
---|
| 202 | CalBddPutElseBddNode(bddManager->bddNull, (CalBddNode_t *)~0x10); |
---|
| 203 | CalBddPutRefCount(bddManager->bddNull, CAL_MAX_REF_COUNT); |
---|
| 204 | /* Put in the unique table, so that it gets locked */ |
---|
| 205 | /*CalHashTableAddDirect(bddManager->uniqueTable[0], bddNode);*/ |
---|
| 206 | |
---|
| 207 | bddManager->indexToId = Cal_MemAlloc(Cal_BddId_t, bddManager->maxNumVars); |
---|
| 208 | bddManager->idToIndex = Cal_MemAlloc(Cal_BddIndex_t, bddManager->maxNumVars+1); |
---|
| 209 | bddManager->idToIndex[CAL_BDD_CONST_ID] = CAL_BDD_CONST_INDEX; |
---|
| 210 | |
---|
| 211 | bddManager->depth = DEFAULT_DEPTH; |
---|
| 212 | bddManager->maxDepth = DEFAULT_MAX_DEPTH; |
---|
| 213 | bddManager->pipelineState = READY; |
---|
| 214 | bddManager->pipelineDepth = PIPELINE_EXECUTION_DEPTH; |
---|
| 215 | bddManager->currentPipelineDepth = 0; |
---|
| 216 | bddManager->pipelineFn = CalOpAnd; |
---|
| 217 | |
---|
| 218 | |
---|
| 219 | bddManager->reqQue = Cal_MemAlloc(CalHashTable_t **, bddManager->maxDepth); |
---|
| 220 | bddManager->cacheTable = CalCacheTableTwoInit(bddManager); |
---|
| 221 | |
---|
| 222 | for (i=0; i < bddManager->maxDepth; i++){ |
---|
| 223 | bddManager->reqQue[i] = Cal_MemAlloc(CalHashTable_t *, |
---|
| 224 | bddManager->maxNumVars+1); |
---|
| 225 | bddManager->reqQue[i][0] = CalHashTableInit(bddManager, 0); |
---|
| 226 | } |
---|
| 227 | |
---|
| 228 | bddManager->requestNodeListArray = Cal_MemAlloc(CalRequestNode_t*, |
---|
| 229 | MAX_INSERT_DEPTH); |
---|
| 230 | for(i = 0; i < MAX_INSERT_DEPTH; i++){ |
---|
| 231 | bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t); |
---|
| 232 | } |
---|
| 233 | bddManager->userProvisionalNodeList = Cal_Nil(CalRequestNode_t); |
---|
| 234 | |
---|
| 235 | /* Garbage collection related information */ |
---|
| 236 | bddManager->numNodes = bddManager->numPeakNodes = 1; |
---|
| 237 | bddManager->numNodesFreed = 0; |
---|
| 238 | bddManager->gcCheck = CAL_GC_CHECK; |
---|
| 239 | bddManager->uniqueTableGCLimit = CAL_MIN_GC_LIMIT; |
---|
| 240 | bddManager->numGC = 0; |
---|
| 241 | bddManager->gcMode = 1; |
---|
| 242 | bddManager->nodeLimit = 0; |
---|
| 243 | bddManager->overflow = 0; |
---|
| 244 | bddManager->repackAfterGCThreshold = CAL_REPACK_AFTER_GC_THRESHOLD; |
---|
| 245 | |
---|
| 246 | |
---|
| 247 | /* Special functions */ |
---|
| 248 | bddManager->TransformFn = BddDefaultTransformFn; |
---|
| 249 | bddManager->transformEnv = 0; |
---|
| 250 | |
---|
| 251 | |
---|
| 252 | /* Association related information */ |
---|
| 253 | bddManager->associationList = Cal_Nil(CalAssociation_t); |
---|
| 254 | /*bddManager->tempAssociation = CAL_BDD_NEW_REC(bddManager, CalAssociation_t);*/ |
---|
| 255 | bddManager->tempAssociation = Cal_MemAlloc(CalAssociation_t, 1); |
---|
| 256 | bddManager->tempAssociation->id = -1; |
---|
| 257 | bddManager->tempAssociation->lastBddIndex = -1; |
---|
| 258 | bddManager->tempAssociation->varAssociation = |
---|
| 259 | Cal_MemAlloc(Cal_Bdd_t, bddManager->maxNumVars+1); |
---|
| 260 | for(i = 0; i < bddManager->maxNumVars+1; i++){ |
---|
| 261 | bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull; |
---|
| 262 | } |
---|
| 263 | bddManager->tempOpCode = -1; |
---|
| 264 | bddManager->currentAssociation = bddManager->tempAssociation; |
---|
| 265 | |
---|
| 266 | /* BDD reordering related information */ |
---|
| 267 | bddManager->dynamicReorderingEnableFlag = 1; |
---|
| 268 | bddManager->reorderMethod = CAL_REORDER_METHOD_DF; |
---|
| 269 | bddManager->reorderTechnique = CAL_REORDER_NONE; |
---|
| 270 | bddManager->numForwardedNodes = 0; |
---|
| 271 | bddManager->numReorderings = 0; |
---|
| 272 | bddManager->maxNumVarsSiftedPerReordering = 1000; |
---|
| 273 | bddManager->maxNumSwapsPerReordering = 2000000; |
---|
| 274 | bddManager->numSwaps = 0; |
---|
| 275 | bddManager->numTrivialSwaps = 0; |
---|
| 276 | bddManager->maxSiftingGrowth = 2.0; |
---|
| 277 | bddManager->reorderingThreshold = CAL_BDD_REORDER_THRESHOLD; |
---|
| 278 | bddManager->maxForwardedNodes = CAL_NUM_FORWARDED_NODES_LIMIT; |
---|
| 279 | bddManager->tableRepackThreshold = CAL_TABLE_REPACK_THRESHOLD; |
---|
| 280 | |
---|
| 281 | |
---|
| 282 | /*bddManager->superBlock = CAL_BDD_NEW_REC(bddManager, Cal_Block_t);*/ |
---|
| 283 | bddManager->superBlock = Cal_MemAlloc(Cal_Block_t, 1); |
---|
| 284 | bddManager->superBlock->numChildren=0; |
---|
| 285 | bddManager->superBlock->children=0; |
---|
| 286 | bddManager->superBlock->reorderable=1; |
---|
| 287 | bddManager->superBlock->firstIndex= -1; |
---|
| 288 | bddManager->superBlock->lastIndex=0; |
---|
| 289 | |
---|
| 290 | bddManager->hooks = Cal_Nil(void); |
---|
| 291 | |
---|
| 292 | return bddManager; |
---|
| 293 | } |
---|
| 294 | |
---|
| 295 | /**Function******************************************************************** |
---|
| 296 | |
---|
| 297 | Synopsis [Frees the BDD manager and all the associated allocations] |
---|
| 298 | |
---|
| 299 | Description [Frees the BDD manager and all the associated allocations] |
---|
| 300 | |
---|
| 301 | SideEffects [None] |
---|
| 302 | |
---|
| 303 | SeeAlso [Cal_BddManagerInit] |
---|
| 304 | |
---|
| 305 | ******************************************************************************/ |
---|
| 306 | int |
---|
| 307 | Cal_BddManagerQuit(Cal_BddManager bddManager) |
---|
| 308 | { |
---|
| 309 | int i, j; |
---|
| 310 | |
---|
| 311 | if(bddManager == Cal_Nil(Cal_BddManager_t)) return 1; |
---|
| 312 | |
---|
| 313 | for (i=0; i < bddManager->maxDepth; i++){ |
---|
| 314 | for (j=0; j <= bddManager->numVars; j++){ |
---|
| 315 | CalHashTableQuit(bddManager, bddManager->reqQue[i][j]); |
---|
| 316 | } |
---|
| 317 | Cal_MemFree(bddManager->reqQue[i]); |
---|
| 318 | } |
---|
| 319 | |
---|
| 320 | for (i=0; i <= bddManager->numVars; i++){ |
---|
| 321 | CalHashTableQuit(bddManager, bddManager->uniqueTable[i]); |
---|
| 322 | CalNodeManagerQuit(bddManager->nodeManagerArray[i]); |
---|
| 323 | } |
---|
| 324 | |
---|
| 325 | CalCacheTableTwoQuit(bddManager->cacheTable); |
---|
| 326 | Cal_MemFree(bddManager->tempAssociation->varAssociation); |
---|
| 327 | /*CAL_BDD_FREE_REC(bddManager, bddManager->tempAssociation, CalAssociation_t);*/ |
---|
| 328 | Cal_MemFree(bddManager->tempAssociation); |
---|
| 329 | /*CAL_BDD_FREE_REC(bddManager, bddManager->superBlock, Cal_Block_t);*/ |
---|
| 330 | CalFreeBlockRecursively(bddManager->superBlock); |
---|
| 331 | CalAssociationListFree(bddManager); |
---|
| 332 | Cal_MemFree(bddManager->varBdds); |
---|
| 333 | Cal_MemFree(bddManager->indexToId); |
---|
| 334 | Cal_MemFree(bddManager->idToIndex); |
---|
| 335 | Cal_MemFree(bddManager->uniqueTable); |
---|
| 336 | Cal_MemFree(bddManager->reqQue); |
---|
| 337 | Cal_MemFree(bddManager->requestNodeListArray); |
---|
| 338 | Cal_MemFree(bddManager->nodeManagerArray); |
---|
| 339 | CalPageManagerQuit(bddManager->pageManager1); |
---|
| 340 | CalPageManagerQuit(bddManager->pageManager2); |
---|
| 341 | Cal_MemFree(bddManager); |
---|
| 342 | |
---|
| 343 | return 0; |
---|
| 344 | } |
---|
| 345 | |
---|
| 346 | /**Function******************************************************************** |
---|
| 347 | |
---|
| 348 | Synopsis [Sets appropriate fields of BDD Manager.] |
---|
| 349 | |
---|
| 350 | Description [This function is used to set the parameters which are |
---|
| 351 | used to control the reordering process. "reorderingThreshold" |
---|
| 352 | determines the number of nodes below which reordering will NOT be |
---|
| 353 | invoked, "maxForwardedNodes" determines the maximum number of |
---|
| 354 | forwarded nodes which are allowed (at that point the cleanup must be |
---|
| 355 | done), and "repackingThreshold" determines the fraction of the page |
---|
| 356 | utilized below which repacking has to be invoked. These parameters |
---|
| 357 | have different effect on the computational and memory usage aspects |
---|
| 358 | of reordeing. For instance, higher value of "maxForwardedNodes" will |
---|
| 359 | result in process consuming more memory, and a lower value on the |
---|
| 360 | other hand would invoke the cleanup process repeatedly resulting in |
---|
| 361 | increased computation.] |
---|
| 362 | |
---|
| 363 | SideEffects [Sets appropriate fields of BDD Manager] |
---|
| 364 | |
---|
| 365 | SeeAlso [] |
---|
| 366 | |
---|
| 367 | ******************************************************************************/ |
---|
| 368 | void |
---|
| 369 | Cal_BddManagerSetParameters(Cal_BddManager bddManager, |
---|
| 370 | long reorderingThreshold, |
---|
| 371 | long maxForwardedNodes, |
---|
| 372 | double repackAfterGCThreshold, |
---|
| 373 | double tableRepackThreshold) |
---|
| 374 | { |
---|
| 375 | if (reorderingThreshold >= 0){ |
---|
| 376 | bddManager->reorderingThreshold = reorderingThreshold; |
---|
| 377 | } |
---|
| 378 | if (maxForwardedNodes >= 0){ |
---|
| 379 | bddManager->maxForwardedNodes = maxForwardedNodes; |
---|
| 380 | } |
---|
| 381 | if (repackAfterGCThreshold >= 0.0){ |
---|
| 382 | bddManager->repackAfterGCThreshold = (float) repackAfterGCThreshold; |
---|
| 383 | } |
---|
| 384 | if (tableRepackThreshold >= 0.0){ |
---|
| 385 | bddManager->tableRepackThreshold = (float) tableRepackThreshold; |
---|
| 386 | } |
---|
| 387 | } |
---|
| 388 | |
---|
| 389 | |
---|
| 390 | /**Function******************************************************************** |
---|
| 391 | |
---|
| 392 | Synopsis [Returns the number of BDD nodes] |
---|
| 393 | |
---|
| 394 | Description [Returns the number of BDD nodes] |
---|
| 395 | |
---|
| 396 | SideEffects [None] |
---|
| 397 | |
---|
| 398 | SeeAlso [Cal_BddTotalSize] |
---|
| 399 | |
---|
| 400 | ******************************************************************************/ |
---|
| 401 | unsigned long |
---|
| 402 | Cal_BddManagerGetNumNodes(Cal_BddManager bddManager) |
---|
| 403 | { |
---|
| 404 | return bddManager->numNodes; |
---|
| 405 | } |
---|
| 406 | |
---|
| 407 | |
---|
| 408 | |
---|
| 409 | /**Function******************************************************************** |
---|
| 410 | |
---|
| 411 | Synopsis [Creates and returns a new variable at the start of the variable |
---|
| 412 | order.] |
---|
| 413 | |
---|
| 414 | Description [Creates and returns a new variable at the start of the |
---|
| 415 | variable order.] |
---|
| 416 | |
---|
| 417 | SideEffects [None] |
---|
| 418 | |
---|
| 419 | ******************************************************************************/ |
---|
| 420 | Cal_Bdd |
---|
| 421 | Cal_BddManagerCreateNewVarFirst(Cal_BddManager bddManager) |
---|
| 422 | { |
---|
| 423 | return CalBddGetExternalBdd(bddManager, CalBddManagerCreateNewVar(bddManager, |
---|
| 424 | (Cal_BddIndex_t)0)); |
---|
| 425 | } |
---|
| 426 | |
---|
| 427 | /**Function******************************************************************** |
---|
| 428 | |
---|
| 429 | Synopsis [Creates and returns a new variable at the end of the variable |
---|
| 430 | order.] |
---|
| 431 | |
---|
| 432 | Description [Creates and returns a new variable at the end of the variable |
---|
| 433 | order.] |
---|
| 434 | |
---|
| 435 | SideEffects [None] |
---|
| 436 | |
---|
| 437 | ******************************************************************************/ |
---|
| 438 | Cal_Bdd |
---|
| 439 | Cal_BddManagerCreateNewVarLast(Cal_BddManager bddManager) |
---|
| 440 | { |
---|
| 441 | return CalBddGetExternalBdd(bddManager, |
---|
| 442 | CalBddManagerCreateNewVar(bddManager, |
---|
| 443 | (Cal_BddIndex_t) |
---|
| 444 | bddManager->numVars)); |
---|
| 445 | } |
---|
| 446 | |
---|
| 447 | |
---|
| 448 | |
---|
| 449 | /**Function******************************************************************** |
---|
| 450 | |
---|
| 451 | Synopsis [Creates and returns a new variable before the specified one in |
---|
| 452 | the variable order.] |
---|
| 453 | |
---|
| 454 | Description [Creates and returns a new variable before the specified one in |
---|
| 455 | the variable order.] |
---|
| 456 | |
---|
| 457 | SideEffects [None] |
---|
| 458 | |
---|
| 459 | ******************************************************************************/ |
---|
| 460 | Cal_Bdd |
---|
| 461 | Cal_BddManagerCreateNewVarBefore(Cal_BddManager bddManager, |
---|
| 462 | Cal_Bdd userBdd) |
---|
| 463 | { |
---|
| 464 | Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, userBdd); |
---|
| 465 | if (CalBddIsBddConst(calBdd)){ |
---|
| 466 | return Cal_BddManagerCreateNewVarLast(bddManager); |
---|
| 467 | } |
---|
| 468 | else{ |
---|
| 469 | return CalBddGetExternalBdd(bddManager, |
---|
| 470 | CalBddManagerCreateNewVar(bddManager, |
---|
| 471 | CalBddGetBddIndex(bddManager, |
---|
| 472 | calBdd))); |
---|
| 473 | } |
---|
| 474 | } |
---|
| 475 | |
---|
| 476 | /**Function******************************************************************** |
---|
| 477 | |
---|
| 478 | Synopsis [Creates and returns a new variable after the specified one in |
---|
| 479 | the variable order.] |
---|
| 480 | |
---|
| 481 | Description [Creates and returns a new variable after the specified one in |
---|
| 482 | the variable order.] |
---|
| 483 | |
---|
| 484 | SideEffects [None] |
---|
| 485 | |
---|
| 486 | ******************************************************************************/ |
---|
| 487 | Cal_Bdd |
---|
| 488 | Cal_BddManagerCreateNewVarAfter(Cal_BddManager bddManager, |
---|
| 489 | Cal_Bdd userBdd) |
---|
| 490 | { |
---|
| 491 | Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, userBdd); |
---|
| 492 | if (CalBddIsBddConst(calBdd)){ |
---|
| 493 | return Cal_BddManagerCreateNewVarLast(bddManager); |
---|
| 494 | } |
---|
| 495 | else{ |
---|
| 496 | return CalBddGetExternalBdd(bddManager, |
---|
| 497 | CalBddManagerCreateNewVar(bddManager, |
---|
| 498 | CalBddGetBddIndex(bddManager, calBdd)+1)); |
---|
| 499 | } |
---|
| 500 | } |
---|
| 501 | |
---|
| 502 | |
---|
| 503 | /**Function******************************************************************** |
---|
| 504 | |
---|
| 505 | Synopsis [Returns the variable with the specified index, null if no |
---|
| 506 | such variable exists] |
---|
| 507 | |
---|
| 508 | Description [Returns the variable with the specified index, null if no |
---|
| 509 | such variable exists] |
---|
| 510 | |
---|
| 511 | SideEffects [None] |
---|
| 512 | |
---|
| 513 | ******************************************************************************/ |
---|
| 514 | Cal_Bdd |
---|
| 515 | Cal_BddManagerGetVarWithIndex(Cal_BddManager bddManager, Cal_BddIndex_t index) |
---|
| 516 | { |
---|
| 517 | if (index >= bddManager->numVars){ |
---|
| 518 | CalBddWarningMessage("Index out of range"); |
---|
| 519 | return (Cal_Bdd) 0; |
---|
| 520 | } |
---|
| 521 | return CalBddGetExternalBdd(bddManager, |
---|
| 522 | bddManager->varBdds[bddManager->indexToId[index]]); |
---|
| 523 | } |
---|
| 524 | |
---|
| 525 | /**Function******************************************************************** |
---|
| 526 | |
---|
| 527 | Synopsis [Returns the variable with the specified id, null if no |
---|
| 528 | such variable exists] |
---|
| 529 | |
---|
| 530 | Description [Returns the variable with the specified id, null if no |
---|
| 531 | such variable exists] |
---|
| 532 | |
---|
| 533 | SideEffects [None] |
---|
| 534 | |
---|
| 535 | SeeAlso [optional] |
---|
| 536 | |
---|
| 537 | ******************************************************************************/ |
---|
| 538 | Cal_Bdd |
---|
| 539 | Cal_BddManagerGetVarWithId(Cal_BddManager bddManager, Cal_BddId_t id) |
---|
| 540 | { |
---|
| 541 | if (id <= 0 || id > bddManager->numVars){ |
---|
| 542 | CalBddWarningMessage("Id out of range"); |
---|
| 543 | return (Cal_Bdd) 0; |
---|
| 544 | } |
---|
| 545 | return CalBddGetExternalBdd(bddManager, bddManager->varBdds[id]); |
---|
| 546 | } |
---|
| 547 | |
---|
| 548 | /*---------------------------------------------------------------------------*/ |
---|
| 549 | /* Definition of internal functions */ |
---|
| 550 | /*---------------------------------------------------------------------------*/ |
---|
| 551 | /**Function******************************************************************** |
---|
| 552 | |
---|
| 553 | Synopsis [This function creates and returns a new variable with given |
---|
| 554 | index value.] |
---|
| 555 | |
---|
| 556 | Description [Right now this function does not handle the case when the |
---|
| 557 | package is working in multiprocessor mode. We need to put in the necessary |
---|
| 558 | code later.] |
---|
| 559 | |
---|
| 560 | SideEffects [If the number of variables in the manager exceeds that of value |
---|
| 561 | of numMaxVars, then we need to reallocate various fields of the manager. Also |
---|
| 562 | depending upon the value of "index", idToIndex and indexToId tables would |
---|
| 563 | change.] |
---|
| 564 | |
---|
| 565 | ******************************************************************************/ |
---|
| 566 | Cal_Bdd_t |
---|
| 567 | CalBddManagerCreateNewVar(Cal_BddManager_t * bddManager, Cal_BddIndex_t index) |
---|
| 568 | { |
---|
| 569 | Cal_Bdd_t calBdd; |
---|
| 570 | Cal_BddId_t varId; |
---|
| 571 | int totalNumVars, maxNumVars, i; |
---|
| 572 | CalAssociation_t *association; |
---|
| 573 | |
---|
| 574 | if (bddManager->numVars == CAL_MAX_VAR_ID){ |
---|
| 575 | CalBddFatalMessage("Cannot create any new variable, no more Id left."); |
---|
| 576 | } |
---|
| 577 | |
---|
| 578 | /* |
---|
| 579 | * Get the total number of variables. If the index is more than the total |
---|
| 580 | * number of variables, then report error. |
---|
| 581 | */ |
---|
| 582 | totalNumVars = bddManager->numVars; |
---|
| 583 | |
---|
| 584 | if (index > totalNumVars){ |
---|
| 585 | CalBddFatalMessage("The variable index out of range"); |
---|
| 586 | } |
---|
| 587 | |
---|
| 588 | |
---|
| 589 | /* |
---|
| 590 | * Create a new variable in the manager which contains this index. |
---|
| 591 | * This might lead to change in the id->index, and index->id |
---|
| 592 | * for other managers. |
---|
| 593 | */ |
---|
| 594 | |
---|
| 595 | /* |
---|
| 596 | * If the number of variables is equal to the maximum number of variables |
---|
| 597 | * then reallocate memory. |
---|
| 598 | */ |
---|
| 599 | if (bddManager->numVars == bddManager->maxNumVars){ |
---|
| 600 | int oldMaxNumVars; |
---|
| 601 | CalAssociation_t *p; |
---|
| 602 | |
---|
| 603 | oldMaxNumVars = bddManager->maxNumVars; |
---|
| 604 | if ((maxNumVars = 2*oldMaxNumVars) > CAL_MAX_VAR_ID){ |
---|
| 605 | maxNumVars = CAL_MAX_VAR_ID; |
---|
| 606 | } |
---|
| 607 | bddManager->maxNumVars = maxNumVars; |
---|
| 608 | bddManager->varBdds = Cal_MemRealloc(Cal_Bdd_t, |
---|
| 609 | bddManager->varBdds, maxNumVars+1); |
---|
| 610 | |
---|
| 611 | bddManager->nodeManagerArray = Cal_MemRealloc(CalNodeManager_t *, |
---|
| 612 | bddManager->nodeManagerArray, |
---|
| 613 | maxNumVars+1); |
---|
| 614 | |
---|
| 615 | bddManager->idToIndex = Cal_MemRealloc(Cal_BddIndex_t, bddManager->idToIndex, |
---|
| 616 | maxNumVars+1); |
---|
| 617 | |
---|
| 618 | bddManager->indexToId = Cal_MemRealloc(Cal_BddIndex_t, bddManager->indexToId, |
---|
| 619 | maxNumVars); |
---|
| 620 | |
---|
| 621 | bddManager->uniqueTable = Cal_MemRealloc(CalHashTable_t *, |
---|
| 622 | bddManager->uniqueTable, maxNumVars+1); |
---|
| 623 | |
---|
| 624 | for (i=0; i<bddManager->maxDepth; i++){ |
---|
| 625 | bddManager->reqQue[i] = Cal_MemRealloc(CalHashTable_t *, bddManager->reqQue[i], |
---|
| 626 | maxNumVars+1); |
---|
| 627 | } |
---|
| 628 | bddManager->tempAssociation->varAssociation = |
---|
| 629 | Cal_MemRealloc(Cal_Bdd_t, bddManager->tempAssociation->varAssociation, |
---|
| 630 | maxNumVars+1); |
---|
| 631 | /* CHECK LOOP INDICES */ |
---|
| 632 | for(i = oldMaxNumVars+1; i < maxNumVars+1; i++){ |
---|
| 633 | bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull; |
---|
| 634 | } |
---|
| 635 | for(p = bddManager->associationList; p; p = p->next){ |
---|
| 636 | p->varAssociation = |
---|
| 637 | Cal_MemRealloc(Cal_Bdd_t, p->varAssociation, maxNumVars+1); |
---|
| 638 | /* CHECK LOOP INDICES */ |
---|
| 639 | for(i = oldMaxNumVars+1; i < maxNumVars+1; i++){ |
---|
| 640 | p->varAssociation[i] = bddManager->bddNull; |
---|
| 641 | } |
---|
| 642 | } |
---|
| 643 | } |
---|
| 644 | |
---|
| 645 | /* If the variable has been created in the middle, shift the indices. */ |
---|
| 646 | if (index != bddManager->numVars){ |
---|
| 647 | for (i=0; i<bddManager->numVars; i++){ |
---|
| 648 | if (bddManager->idToIndex[i+1] >= index){ |
---|
| 649 | bddManager->idToIndex[i+1]++; |
---|
| 650 | } |
---|
| 651 | } |
---|
| 652 | } |
---|
| 653 | |
---|
| 654 | /* Fix indexToId table */ |
---|
| 655 | for (i=bddManager->numVars; i>index; i--){ |
---|
| 656 | bddManager->indexToId[i] = bddManager->indexToId[i-1]; |
---|
| 657 | } |
---|
| 658 | |
---|
| 659 | for(association = bddManager->associationList; association; |
---|
| 660 | association = |
---|
| 661 | association->next){ |
---|
| 662 | if (association->lastBddIndex >= index){ |
---|
| 663 | association->lastBddIndex++; |
---|
| 664 | } |
---|
| 665 | } |
---|
| 666 | if (bddManager->tempAssociation->lastBddIndex >= index){ |
---|
| 667 | bddManager->tempAssociation->lastBddIndex++; |
---|
| 668 | } |
---|
| 669 | |
---|
| 670 | bddManager->numVars++; |
---|
| 671 | varId = bddManager->numVars; |
---|
| 672 | |
---|
| 673 | bddManager->idToIndex[varId] = index; |
---|
| 674 | bddManager->indexToId[index] = varId; |
---|
| 675 | |
---|
| 676 | bddManager->nodeManagerArray[varId] = |
---|
| 677 | CalNodeManagerInit(bddManager->pageManager2); |
---|
| 678 | bddManager->uniqueTable[varId] = |
---|
| 679 | CalHashTableInit(bddManager, varId); |
---|
| 680 | |
---|
| 681 | /* insert node in the uniqueTableForId */ |
---|
| 682 | CalHashTableAddDirectAux(bddManager->uniqueTable[varId], |
---|
| 683 | bddManager->bddOne, bddManager->bddZero, &calBdd); |
---|
| 684 | CalBddPutRefCount(calBdd, CAL_MAX_REF_COUNT); |
---|
| 685 | bddManager->varBdds[varId] = calBdd; |
---|
| 686 | |
---|
| 687 | bddManager->numNodes++; |
---|
| 688 | |
---|
| 689 | #ifdef __OLD__ |
---|
| 690 | /* initialize req_que_for_id */ |
---|
| 691 | bddManager->reqQue[varId] = Cal_MemAlloc(CalHashTable_t*, bddManager->maxDepth); |
---|
| 692 | for (i=0; i<manager->maxDepth; i++){ |
---|
| 693 | bddManager->reqQue[varId][i] = CalHashTableInit(bddManager, varId); |
---|
| 694 | } |
---|
| 695 | #endif |
---|
| 696 | |
---|
| 697 | /* initialize req_que_for_id */ |
---|
| 698 | for (i=0; i<bddManager->maxDepth; i++){ |
---|
| 699 | bddManager->reqQue[i][varId] = |
---|
| 700 | CalHashTableInit(bddManager, varId); |
---|
| 701 | } |
---|
| 702 | CalBddShiftBlock(bddManager, bddManager->superBlock, (long)index); |
---|
| 703 | return calBdd; |
---|
| 704 | } |
---|
| 705 | |
---|
| 706 | |
---|
| 707 | /*---------------------------------------------------------------------------*/ |
---|
| 708 | /* Definition of static functions */ |
---|
| 709 | /*---------------------------------------------------------------------------*/ |
---|
| 710 | /**Function******************************************************************** |
---|
| 711 | |
---|
| 712 | Synopsis [required] |
---|
| 713 | |
---|
| 714 | Description [optional] |
---|
| 715 | |
---|
| 716 | SideEffects [required] |
---|
| 717 | |
---|
| 718 | SeeAlso [optional] |
---|
| 719 | |
---|
| 720 | ******************************************************************************/ |
---|
| 721 | static void |
---|
| 722 | BddDefaultTransformFn( |
---|
| 723 | Cal_BddManager_t * bddManager, |
---|
| 724 | CalAddress_t value1, |
---|
| 725 | CalAddress_t value2, |
---|
| 726 | CalAddress_t * result1, |
---|
| 727 | CalAddress_t * result2, |
---|
| 728 | Cal_Pointer_t pointer) |
---|
| 729 | { |
---|
| 730 | if (!value2) |
---|
| 731 | /* Will be a carry when taking 2's complement of value2. Thus, */ |
---|
| 732 | /* take 2's complement of high part. */ |
---|
| 733 | value1= -(long)value1; |
---|
| 734 | else |
---|
| 735 | { |
---|
| 736 | value2= -(long)value2; |
---|
| 737 | value1= ~value1; |
---|
| 738 | } |
---|
| 739 | *result1=value1; |
---|
| 740 | *result2=value2; |
---|
| 741 | } |
---|
| 742 | |
---|
| 743 | #ifdef CALBDDMANAGER |
---|
| 744 | |
---|
| 745 | /**Function******************************************************************** |
---|
| 746 | |
---|
| 747 | Synopsis [required] |
---|
| 748 | |
---|
| 749 | Description [optional] |
---|
| 750 | |
---|
| 751 | SideEffects [required] |
---|
| 752 | |
---|
| 753 | SeeAlso [optional] |
---|
| 754 | |
---|
| 755 | ******************************************************************************/ |
---|
| 756 | static int |
---|
| 757 | CalBddManagerPrint(Cal_BddManager_t *bddManager) |
---|
| 758 | { |
---|
| 759 | int i; |
---|
| 760 | CalHashTable_t *uniqueTableForId; |
---|
| 761 | printf("##################### BDD MANAGER #####################\n"); |
---|
| 762 | for(i = 1; i < bddManager->numVars; i++){ |
---|
| 763 | uniqueTableForId = bddManager->uniqueTable[i]; |
---|
| 764 | CalHashTablePrint(uniqueTableForId); |
---|
| 765 | } |
---|
| 766 | fflush(stdout); |
---|
| 767 | return 0; |
---|
| 768 | } |
---|
| 769 | |
---|
| 770 | |
---|
| 771 | main(argc, argv) |
---|
| 772 | int argc; |
---|
| 773 | char **argv; |
---|
| 774 | { |
---|
| 775 | Cal_Bdd_t n; |
---|
| 776 | Cal_BddManager_t *manager; |
---|
| 777 | |
---|
| 778 | manager = CalBddManagerInit(argc, argv); |
---|
| 779 | n = CalBddManagerCreateVariable(bddManager); |
---|
| 780 | CalBddFunctionPrint(n); |
---|
| 781 | n = CalBddManagerGetVariable(bddManager, 0); |
---|
| 782 | CalBddFunctionPrint(n); |
---|
| 783 | } |
---|
| 784 | #endif /* CALBDDMANAGER */ |
---|
| 785 | |
---|
| 786 | #ifdef __GC__ |
---|
| 787 | main(argc, argv) |
---|
| 788 | int argc; |
---|
| 789 | char **argv; |
---|
| 790 | { |
---|
| 791 | Cal_BddManager_t *manager; |
---|
| 792 | Cal_Bdd_t vars[256]; |
---|
| 793 | Cal_Bdd_t function, tempFunction; |
---|
| 794 | int i; |
---|
| 795 | int numVars; |
---|
| 796 | |
---|
| 797 | if (argc >= 2) |
---|
| 798 | numVars = atoi(argv[1]); |
---|
| 799 | else |
---|
| 800 | numVars = 3; |
---|
| 801 | |
---|
| 802 | manager = Cal_BddManagerInit(); |
---|
| 803 | |
---|
| 804 | for (i = 0; i < numVars; i++){ |
---|
| 805 | vars[i] = Cal_BddManagerCreateNewVarLast(bddManager); |
---|
| 806 | } |
---|
| 807 | |
---|
| 808 | function = vars[0]; |
---|
| 809 | for (i = 1; i < numVars - 1; i++){ |
---|
| 810 | tempFunction = Cal_BddITE(bddManager, vars[i], vars[i+1], function); |
---|
| 811 | Cal_BddFree(function); |
---|
| 812 | function = tempFunction; |
---|
| 813 | /*fprintf(stdout, "i = %d\n", i); |
---|
| 814 | unique_table_write(stdout, CalBddManager->unique_table); |
---|
| 815 | */ |
---|
| 816 | } |
---|
| 817 | fprintf(stdout, "\n******************Before Free****************\n"); |
---|
| 818 | for (i = 1; i <= numVars; i++){ |
---|
| 819 | CalHashTablePrint(bddManager->uniqueTable[i]); |
---|
| 820 | } |
---|
| 821 | Cal_BddFree(function); |
---|
| 822 | fprintf(stdout, "\n****************After Free****************\n"); |
---|
| 823 | for (i = 1; i <= numVars; i++){ |
---|
| 824 | CalHashTablePrint(bddManager->uniqueTable[i]); |
---|
| 825 | } |
---|
| 826 | Cal_BddManagerGC(bddManager); |
---|
| 827 | fprintf(stdout, "\n****************After GC****************\n"); |
---|
| 828 | for (i = 1; i <= numVars; i++){ |
---|
| 829 | CalHashTablePrint(bddManager->uniqueTable[i]); |
---|
| 830 | } |
---|
| 831 | } |
---|
| 832 | #endif |
---|