src/calBdd/calReorderUtil.c File Reference

#include "calInt.h"
Include dependency graph for calReorderUtil.c:

Go to the source code of this file.

Functions

void CalBddReorderFixUserBddPtrs (Cal_BddManager bddManager)
int CalCheckAllValidity (Cal_BddManager bddManager)
int CalCheckValidityOfNodesForId (Cal_BddManager bddManager, int id)
int CalCheckValidityOfNodesForWindow (Cal_BddManager bddManager, Cal_BddIndex_t index, int numLevels)
int CalCheckValidityOfANode (Cal_BddManager_t *bddManager, CalBddNode_t *bddNode, int id)
void CalCheckRefCountValidity (Cal_BddManager_t *bddManager)
int CalCheckAssoc (Cal_BddManager_t *bddManager)
void CalFixupAssoc (Cal_BddManager_t *bddManager, long id1, long id2, CalAssociation_t *assoc)
void CalBddReorderFixCofactors (Cal_BddManager bddManager, Cal_BddId_t id)
void CalBddReorderReclaimForwardedNodes (Cal_BddManager bddManager, int startIndex, int endIndex)

Function Documentation

void CalBddReorderFixCofactors ( Cal_BddManager  bddManager,
Cal_BddId_t  id 
)

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

Synopsis [Fixes the cofactors of the nodes belonging to the given index.]

Description [This routine traverses the unique table and for each node, looks at the then and else cofactors. If needed fixes the cofactors.]

SideEffects [required]

SeeAlso [optional]

Definition at line 528 of file calReorderUtil.c.

00529 {
00530   CalHashTable_t *uniqueTableForId =
00531       bddManager->uniqueTable[id];
00532   CalBddNode_t *bddNode, *nextBddNode, **bins, *thenBddNode, *elseBddNode;
00533   Cal_Bdd_t f0, f1;
00534   long numBins;
00535   int i, rehashFlag;
00536   
00537   numBins = uniqueTableForId->numBins;
00538   bins = uniqueTableForId->bins;
00539 
00540   for(i = 0; i < numBins; i++) {
00541     for(bddNode = bins[i];
00542         bddNode != Cal_Nil(CalBddNode_t);
00543         bddNode = nextBddNode) {
00544       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00545       /*
00546        * Process one bddNode at a time
00547        */
00548       /*
00549       ** Because we have kept all the forwarding nodes in the list,
00550       ** this should not be a forwarding node.
00551       */
00552       Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
00553       Cal_Assert(CalBddNodeIsRefCountZero(bddNode) == 0);
00554       thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00555       elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00556       rehashFlag = 0;
00557       CalBddNodeGetThenBdd(bddNode, f1);
00558       CalBddNodeGetElseBdd(bddNode, f0);
00559       if (CalBddIsForwarded(f1)) {
00560         CalBddForward(f1);
00561         CalBddNodePutThenBdd(bddNode, f1);
00562         rehashFlag = 1;
00563       }
00564       Cal_Assert(CalBddIsForwarded(f1) == 0);
00565       if (CalBddIsForwarded(f0)) {
00566         CalBddForward(f0);
00567         CalBddNodePutElseBdd(bddNode, f0); 
00568         rehashFlag = 1;
00569       }
00570       Cal_Assert(CalBddIsForwarded(f0) == 0);
00571       /* Rehash if necessary */
00572       if (rehashFlag) {
00573         CalUniqueTableForIdRehashNode(uniqueTableForId, bddNode, thenBddNode,
00574                                       elseBddNode);
00575       }
00576     }
00577   }
00578 }

void CalBddReorderFixUserBddPtrs ( Cal_BddManager  bddManager  ) 

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

FileName [calReorderUtil.c]

PackageName [cal]

Synopsis [Some utility routines used by both breadth-first and depth-first reordering techniques.]

Description []

SeeAlso [optional]

Author [Rajeev K. Ranjan (rajeev@ic.eecs.berkeley.edu) Wilsin Gosti (wilsin@ic.eecs.berkeley.edu)] Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id
calReorderUtil.c,v 1.3 2002/09/22 00:37:04 fabio Exp

]AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 88 of file calReorderUtil.c.

00089 {
00090   CalHashTable_t *userBddUniqueTable = bddManager->uniqueTable[0];
00091   int i;
00092   int numBins;
00093   int rehashFlag;
00094   CalBddNode_t **bins;
00095   CalBddNode_t *bddNode;
00096   CalBddNode_t *nextBddNode;
00097   CalBddNode_t *thenBddNode;
00098   CalBddNode_t *elseBddNode;
00099   Cal_Bdd_t internalBdd;
00100 
00101   numBins = userBddUniqueTable->numBins;
00102   bins = userBddUniqueTable->bins;
00103 
00104   for(i = 0; i < numBins; i++) {
00105     for(bddNode = bins[i];
00106         bddNode != Cal_Nil(CalBddNode_t);
00107         bddNode = nextBddNode) {
00108       /*
00109        * Process one bddNode at a time
00110        */
00111       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00112       rehashFlag = 0;
00113 
00114       thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00115       elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00116       CalBddNodeGetThenBdd(bddNode, internalBdd);
00117       if (CalBddIsForwarded(internalBdd)) {
00118         CalBddForward(internalBdd);
00119         CalBddNodePutThenBdd(bddNode, internalBdd);
00120         rehashFlag = 1;
00121       }
00122       Cal_Assert(CalBddIsForwarded(internalBdd) == 0);
00123       /*Cal_Assert(!CalBddIsRefCountZero(internalBdd));*/
00124       /*
00125        * Rehash if necessary
00126        */
00127       if (rehashFlag) {
00128         CalUniqueTableForIdRehashNode(userBddUniqueTable, bddNode,
00129                                       thenBddNode, elseBddNode);
00130       }
00131     }
00132   }
00133 }

void CalBddReorderReclaimForwardedNodes ( Cal_BddManager  bddManager,
int  startIndex,
int  endIndex 
)

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 592 of file calReorderUtil.c.

00594 {
00595   Cal_BddIndex_t index;
00596   Cal_BddId_t id;
00597   CalHashTable_t *uniqueTableForId;
00598   CalNodeManager_t *nodeManager;
00599   
00600   for(index = startIndex; index <= endIndex; index++){
00601     id = bddManager->indexToId[index];
00602     uniqueTableForId = bddManager->uniqueTable[id];
00603     nodeManager = uniqueTableForId->nodeManager;
00604     uniqueTableForId->endNode->nextBddNode = nodeManager->freeNodeList;
00605     nodeManager->freeNodeList = uniqueTableForId->startNode.nextBddNode;
00606     uniqueTableForId->endNode = &(uniqueTableForId->startNode);
00607     uniqueTableForId->startNode.nextBddNode = NULL;
00608   }
00609   bddManager->numForwardedNodes = 0;
00610 }

int CalCheckAllValidity ( Cal_BddManager  bddManager  ) 

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 147 of file calReorderUtil.c.

00148 {
00149   int id;
00150   for(id = 0; id <= bddManager->numVars; id++){
00151     CalCheckValidityOfNodesForId(bddManager, id);
00152   }
00153   CalCheckAssociationValidity(bddManager);
00154   if (bddManager->pipelineState == CREATE){
00155     CalCheckPipelineValidity(bddManager);
00156   }
00157   CalCheckRefCountValidity(bddManager);
00158   CalCheckCacheTableValidity(bddManager);
00159   return 1;
00160 }

int CalCheckAssoc ( Cal_BddManager_t *  bddManager  ) 

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 447 of file calReorderUtil.c.

00448 {
00449   CalAssociation_t *assoc, *nextAssoc;
00450   int i;
00451   int expectedLastBddIndex, bddIndex;
00452 
00453   for(assoc = bddManager->associationList;
00454       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00455     nextAssoc = assoc->next;
00456     expectedLastBddIndex = -1;
00457     for (i=1; i <= bddManager->numVars; i++){
00458       if (CalBddIsBddNull(bddManager, assoc->varAssociation[i]) == 0){
00459         bddIndex = bddManager->idToIndex[i];
00460         if (expectedLastBddIndex < bddIndex){
00461           expectedLastBddIndex = bddIndex;
00462         }
00463       }
00464     }
00465     Cal_Assert(expectedLastBddIndex == assoc->lastBddIndex);
00466   }
00467   /* fix temporary association */
00468   assoc = bddManager->tempAssociation;
00469   expectedLastBddIndex = -1;
00470   for (i=1; i <= bddManager->numVars; i++){
00471     if (CalBddIsBddNull(bddManager, assoc->varAssociation[i]) == 0){
00472       bddIndex = bddManager->idToIndex[i];
00473       if (expectedLastBddIndex < bddIndex){
00474         expectedLastBddIndex = bddIndex;
00475       }
00476     }
00477   }
00478   Cal_Assert(expectedLastBddIndex == assoc->lastBddIndex);
00479   return 1;
00480 }

void CalCheckRefCountValidity ( Cal_BddManager_t *  bddManager  ) 

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 315 of file calReorderUtil.c.

00316 {
00317   int i, numBins, index;
00318   CalHashTable_t *uniqueTableForId;
00319   CalBddNode_t *bddNode, *nextBddNode;
00320   Cal_Bdd_t thenBdd, elseBdd, internalBdd;
00321   CalAssociation_t *assoc, *nextAssoc;
00322   
00323   /* First traverse the user BDDs */
00324   uniqueTableForId = bddManager->uniqueTable[0];
00325   numBins = uniqueTableForId->numBins;
00326   for (i = 0; i < numBins; i++){
00327     for (bddNode = uniqueTableForId->bins[i]; bddNode;
00328          bddNode = nextBddNode){
00329       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00330       CalBddNodeGetThenBdd(bddNode, internalBdd);
00331       CalBddDcrRefCount(internalBdd);
00332     }
00333   }
00334       /* Traverse the associations */
00335   
00336   for(assoc = bddManager->associationList;
00337       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00338     nextAssoc = assoc->next;
00339     for (i=1; i <= bddManager->numVars; i++){
00340         if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00341             CalBddDcrRefCount(assoc->varAssociation[i]);
00342         }
00343     }
00344   }
00345   /* temporary association */
00346   assoc = bddManager->tempAssociation;
00347   for (i=1; i <= bddManager->numVars; i++){
00348       if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00349           CalBddDcrRefCount(assoc->varAssociation[i]);
00350       }
00351   }
00352 
00353   
00354   /* Now traverse all the nodes in order */
00355   for (index = 0; index < bddManager->numVars; index++){
00356     uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
00357     numBins = uniqueTableForId->numBins;
00358     for (i = 0; i < numBins; i++){
00359       for (bddNode = uniqueTableForId->bins[i]; bddNode;
00360            bddNode = nextBddNode){
00361         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00362         CalBddNodeGetThenBdd(bddNode, thenBdd);
00363         CalBddNodeGetElseBdd(bddNode, elseBdd);
00364         CalBddDcrRefCount(thenBdd);
00365         CalBddDcrRefCount(elseBdd);
00366       }
00367     }
00368   }
00369 
00370   /* All the reference count must be zero  or max */
00371   for (index = 0; index < bddManager->numVars; index++){
00372     uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
00373     numBins = uniqueTableForId->numBins;
00374     for (i = 0; i < numBins; i++){
00375       for (bddNode = uniqueTableForId->bins[i]; bddNode;
00376            bddNode = nextBddNode){
00377         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00378         /* If the pipeline execution is going on, the following
00379            assertion will not hold */
00380         if (bddManager->pipelineState != CREATE){
00381           Cal_Assert(CalBddNodeIsRefCountZero(bddNode) ||
00382                      CalBddNodeIsRefCountMax(bddNode));
00383         }
00384       }
00385     }
00386   }
00387 
00388   /* Put back the ref count */
00389   /* traverse all the nodes in order */
00390   for (index = 0; index < bddManager->numVars; index++){
00391     uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
00392     numBins = uniqueTableForId->numBins;
00393     for (i = 0; i < numBins; i++){
00394       for (bddNode = uniqueTableForId->bins[i]; bddNode;
00395            bddNode = nextBddNode){
00396         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00397         CalBddNodeGetThenBdd(bddNode, thenBdd);
00398         CalBddNodeGetElseBdd(bddNode, elseBdd);
00399         CalBddIcrRefCount(thenBdd);
00400         CalBddIcrRefCount(elseBdd);
00401       }
00402     }
00403   }
00404       /* Traverse the associations */
00405   for(assoc = bddManager->associationList;
00406       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00407     nextAssoc = assoc->next;
00408     for (i=1; i <= bddManager->numVars; i++){
00409         if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00410             CalBddIcrRefCount(assoc->varAssociation[i]);
00411         }
00412     }
00413   }
00414   /* temporary association */
00415   assoc = bddManager->tempAssociation;
00416   for (i=1; i <= bddManager->numVars; i++){
00417       if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00418           CalBddIcrRefCount(assoc->varAssociation[i]);
00419       }
00420   }
00421 
00422   /* Traverse the user BDDs */
00423   uniqueTableForId = bddManager->uniqueTable[0];
00424   numBins = uniqueTableForId->numBins;
00425   for (i = 0; i < numBins; i++){
00426     for (bddNode = uniqueTableForId->bins[i]; bddNode;
00427          bddNode = nextBddNode){
00428       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00429       CalBddNodeGetThenBdd(bddNode, internalBdd);
00430       CalBddIcrRefCount(internalBdd);
00431     }
00432   }
00433 }

int CalCheckValidityOfANode ( Cal_BddManager_t *  bddManager,
CalBddNode_t *  bddNode,
int  id 
)

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 263 of file calReorderUtil.c.

00265 {
00266   Cal_Bdd_t thenBdd, elseBdd, thenBdd_, elseBdd_, bdd;
00267   if (id != 0){
00268     /* id = 0 corresponds to the constants and the user BDDs */
00269     Cal_Assert(bddManager->idToIndex[id] <
00270                bddManager->idToIndex[bddNode->thenBddId]);   
00271     Cal_Assert(bddManager->idToIndex[id] < 
00272                bddManager->idToIndex[bddNode->elseBddId]);
00273   }
00274   Cal_Assert(!CalBddNodeIsForwarded(bddNode));
00275   Cal_Assert(!CalBddNodeIsRefCountZero(bddNode));
00276   CalBddNodeGetThenBdd(bddNode, thenBdd);
00277   CalBddNodeGetElseBdd(bddNode, elseBdd);
00278   Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00279   Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
00280   Cal_Assert(!CalBddIsRefCountZero(thenBdd));
00281   Cal_Assert(!CalBddIsRefCountZero(elseBdd));
00282   /* Make sure that the then and else bdd nodes are part of the
00283      respective unique tables */
00284   if (bddNode->thenBddId != 0){
00285     CalBddGetThenBdd(thenBdd, thenBdd_);
00286     CalBddGetElseBdd(thenBdd, elseBdd_);
00287     Cal_Assert(
00288       CalUniqueTableForIdLookup(bddManager,
00289                                 bddManager->uniqueTable[bddNode->thenBddId],  
00290                                 thenBdd_, elseBdd_, &bdd));
00291   }
00292   if (bddNode->elseBddId != 0){
00293     CalBddGetThenBdd(elseBdd, thenBdd_);
00294     CalBddGetElseBdd(elseBdd, elseBdd_);
00295     Cal_Assert(
00296       CalUniqueTableForIdLookup(bddManager,
00297                                 bddManager->uniqueTable[bddNode->elseBddId],
00298                                 thenBdd_, elseBdd_, &bdd));
00299   }
00300   return 1;
00301 }

int CalCheckValidityOfNodesForId ( Cal_BddManager  bddManager,
int  id 
)

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 175 of file calReorderUtil.c.

00176 {
00177   int i, numBins;
00178   CalHashTable_t *uniqueTableForId;
00179   CalBddNode_t *bddNode, *nextBddNode;
00180   Cal_Bdd_t thenBdd, elseBdd;
00181   
00182   uniqueTableForId = bddManager->uniqueTable[id];
00183   Cal_Assert(uniqueTableForId->startNode.nextBddNode == NULL);
00184   numBins = uniqueTableForId->numBins;
00185   for (i = 0; i < numBins; i++){
00186     for (bddNode = uniqueTableForId->bins[i]; bddNode;
00187          bddNode = nextBddNode){
00188       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00189       CalCheckValidityOfANode(bddManager, bddNode, id);
00190       CalBddNodeGetThenBdd(bddNode, thenBdd);
00191       CalBddNodeGetElseBdd(bddNode, elseBdd);
00192       Cal_Assert(CalDoHash2(CalBddGetBddNode(thenBdd),
00193                             CalBddGetBddNode(elseBdd), 
00194                             uniqueTableForId) == i);
00195     }
00196   }
00197   return 1;
00198 }

int CalCheckValidityOfNodesForWindow ( Cal_BddManager  bddManager,
Cal_BddIndex_t  index,
int  numLevels 
)

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 213 of file calReorderUtil.c.

00215 {
00216   int i, numBins, j;
00217   CalHashTable_t *uniqueTableForId;
00218   CalBddNode_t *bddNode, *nextBddNode;
00219   Cal_Bdd_t thenBdd, elseBdd;
00220 
00221   for (i = 0; i < numLevels; i++){
00222     uniqueTableForId =
00223         bddManager->uniqueTable[bddManager->indexToId[index+i]]; 
00224     numBins = uniqueTableForId->numBins;
00225     for (j = 0; j < numBins; j++){
00226       for (bddNode = uniqueTableForId->bins[j]; bddNode;
00227            bddNode = nextBddNode){
00228         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00229         Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
00230         CalBddNodeGetThenBdd(bddNode, thenBdd);
00231         CalBddNodeGetElseBdd(bddNode, elseBdd);
00232         Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00233         Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
00234         Cal_Assert(CalDoHash2(CalBddGetBddNode(thenBdd),
00235                               CalBddGetBddNode(elseBdd), 
00236                              uniqueTableForId) == j);
00237       }
00238     }
00239     for (bddNode = uniqueTableForId->startNode.nextBddNode; bddNode;
00240          bddNode = nextBddNode){ 
00241       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00242       CalBddNodeGetThenBdd(bddNode, thenBdd);
00243       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00244     }
00245   }
00246   return 1;
00247 }

void CalFixupAssoc ( Cal_BddManager_t *  bddManager,
long  id1,
long  id2,
CalAssociation_t *  assoc 
)

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 494 of file calReorderUtil.c.

00496 {
00497   if (assoc->lastBddIndex == -1) return;
00498   /* Variable with id1 is moving down a spot. */
00499   if ((CalBddIsBddNull(bddManager, assoc->varAssociation[id1]) == 0)
00500       && (assoc->lastBddIndex == bddManager->idToIndex[id1])){
00501     assoc->lastBddIndex++;
00502   }
00503   else if ((CalBddIsBddNull(bddManager, assoc->varAssociation[id1])) &&
00504            (CalBddIsBddNull(bddManager, assoc->varAssociation[id2]) ==
00505             0) && 
00506   (assoc->lastBddIndex == bddManager->idToIndex[id2])){
00507     assoc->lastBddIndex--;
00508   }
00509   Cal_Assert((assoc->lastBddIndex >= 0) && (assoc->lastBddIndex <=
00510                                            CAL_BDD_CONST_INDEX));
00511    
00512 }

Generated on Tue Jan 12 13:57:13 2010 for glu-2.2 by  doxygen 1.6.1