src/calBdd/calPipeline.c File Reference

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

Go to the source code of this file.

Functions

void Cal_PipelineSetDepth (Cal_BddManager bddManager, int depth)
int Cal_PipelineInit (Cal_BddManager bddManager, Cal_BddOp_t bddOp)
Cal_Bdd Cal_PipelineCreateProvisionalBdd (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
int Cal_PipelineExecute (Cal_BddManager bddManager)
Cal_Bdd Cal_PipelineUpdateProvisionalBdd (Cal_BddManager bddManager, Cal_Bdd provisionalBdd)
int Cal_BddIsProvisional (Cal_BddManager bddManager, Cal_Bdd userBdd)
void Cal_PipelineQuit (Cal_BddManager bddManager)
void CalBddReorderFixProvisionalNodes (Cal_BddManager_t *bddManager)
void CalCheckPipelineValidity (Cal_BddManager_t *bddManager)

Function Documentation

int Cal_BddIsProvisional ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

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

Synopsis [Returns 1, if the given user BDD contains provisional BDD node.]

Description [Returns 1, if the given user BDD contains provisional BDD node.]

SideEffects [None.]

SeeAlso []

Definition at line 344 of file calPipeline.c.

00345 {
00346   Cal_Bdd_t internalBdd = CalBddGetInternalBdd(bddManager, userBdd);
00347   return CalBddIsMarked(internalBdd);
00348 }

Cal_Bdd Cal_PipelineCreateProvisionalBdd ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd,
Cal_Bdd  gUserBdd 
)

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

Synopsis [Create a provisional BDD in the pipeline.]

Description [The provisional BDD is automatically freed once the pipeline is quitted.]

SideEffects []

SeeAlso []

Definition at line 170 of file calPipeline.c.

00172 {
00173   int insertDepth, operandDepth;
00174   CalRequestNode_t *requestNode;
00175   Cal_Bdd_t provisionalBdd, f, g;
00176   Cal_BddId_t bddId;
00177   Cal_Bdd userNode;
00178   
00179   insertDepth = 0;
00180   
00181   f = CalBddGetInternalBdd(bddManager, fUserBdd);
00182   g = CalBddGetInternalBdd(bddManager, gUserBdd);
00183   if(bddManager->pipelineState != CREATE){
00184     CalBddWarningMessage("Provisional Bdd not created: Pipeline is not initialized");
00185     return (Cal_Bdd) 0;
00186   }
00187   if(CalBddIsMarked(f)){
00188     CalBddGetDepth(f, operandDepth);
00189     if(insertDepth <= operandDepth){
00190       insertDepth = operandDepth + 1;
00191     }
00192   }
00193   if(CalBddIsMarked(g)){
00194     CalBddGetDepth(g, operandDepth);
00195     if(insertDepth <= operandDepth){
00196       insertDepth = operandDepth + 1;
00197     }
00198   }
00199   if (bddManager->pipelineDepth <= insertDepth){
00200     bddManager->pipelineDepth = insertDepth + 1;
00201   }
00202   if (insertDepth >= MAX_INSERT_DEPTH){
00203     CalBddWarningMessage("Provisional Bdd not created");
00204     CalBddWarningMessage("Maximum pipeline depth is reached");
00205     return (Cal_Bdd) 0;
00206   }
00207 
00208   CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
00209   CalRequestNodePutF(requestNode, f);
00210   CalRequestNodePutG(requestNode, g);
00211   CalRequestNodeMark(requestNode);
00212   CalRequestNodePutDepth(requestNode, insertDepth);
00213   CalRequestNodePutNextRequestNode(requestNode,
00214       bddManager->requestNodeListArray[insertDepth]);
00215   bddManager->requestNodeListArray[insertDepth] = requestNode;
00216 
00217   CalBddGetMinId2(bddManager, f, g, bddId);
00218   CalBddPutBddId(provisionalBdd, bddId);
00219   CalBddPutBddNode(provisionalBdd, (CalBddNode_t *)requestNode);
00220 
00221   CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], userNode);
00222   CalBddNodePutThenBdd(userNode, provisionalBdd);
00223   CalBddNodePutElseBdd(userNode, bddManager->bddOne);
00224   CalBddNodePutNextBddNode(userNode,
00225                            bddManager->userProvisionalNodeList);
00226   bddManager->userProvisionalNodeList = userNode;
00227   CalBddNodeIcrRefCount(userNode);
00228   return userNode;
00229 }

int Cal_PipelineExecute ( Cal_BddManager  bddManager  ) 

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

Synopsis [Executes a pipeline.]

Description [All the results are computed. User should update the BDDs of interest. Eventually this feature would become transparent.]

SideEffects [required]

SeeAlso [optional]

Definition at line 244 of file calPipeline.c.

00245 {
00246   CalRequestNode_t **requestNodeListArray, *node, *nextNode;
00247   int  i;
00248   Cal_Bdd_t thenBdd;
00249   int automaticDepthControlFlag = 0;
00250   int pipelineDepth;
00251   
00252   if(bddManager->pipelineState != CREATE){
00253     CalBddWarningMessage("Pipeline cannot be executed");
00254     return 0;
00255   }
00256 
00257   /* Check if we need to control the depth value using some heuristic */
00258   if (bddManager->depth == 0) automaticDepthControlFlag = 1;
00259   
00260   requestNodeListArray = bddManager->requestNodeListArray;
00261   pipelineDepth = bddManager->pipelineDepth;
00262   while(pipelineDepth){
00263     if (automaticDepthControlFlag){
00264       if (bddManager->numNodes < 10000) bddManager->depth = 4;
00265       else if (bddManager->numNodes < 100000) bddManager->depth = 2;
00266       else bddManager->depth = 1;
00267     }
00268     if(bddManager->depth > pipelineDepth){
00269       bddManager->depth = pipelineDepth;
00270     }
00271     CalRequestNodeListArrayOp(bddManager, requestNodeListArray,
00272                               bddManager->pipelineFn);
00273     pipelineDepth -= bddManager->depth;
00274 
00275     /* Lock the results, in case garbage collection needs to be
00276        invoked */
00277     for (i=0; i<bddManager->depth; i++){
00278       for (node = requestNodeListArray[i]; node; node = nextNode){
00279         nextNode = CalBddNodeGetNextBddNode(node);
00280         CalBddNodeGetThenBdd(node, thenBdd);
00281         CalBddIcrRefCount(thenBdd);
00282       }
00283     }
00284     /* Save the current pipelineDepth */
00285     bddManager->currentPipelineDepth = pipelineDepth;
00286     if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00287       /* Abort, may be we should clean up a little bit */
00288       fprintf(stderr,"Bdd Overflow: Aborting\n");
00289       return 0;
00290     }
00291     requestNodeListArray += bddManager->depth;
00292   }
00293   /* Need to decrement the reference counts */
00294   for (i=0; i<bddManager->pipelineDepth; i++){
00295     for (node=bddManager->requestNodeListArray[i]; node; node = nextNode){
00296       nextNode = CalBddNodeGetNextBddNode(node);
00297       CalBddNodeGetThenBdd(node, thenBdd);
00298       CalBddDcrRefCount(thenBdd);
00299     }
00300   }
00301   bddManager->pipelineState = UPDATE;
00302   return 1;
00303 }

int Cal_PipelineInit ( Cal_BddManager  bddManager,
Cal_BddOp_t  bddOp 
)

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

Synopsis [Initialize a BDD pipeline.]

Description [All the operations for this pipeline must be of the same kind.]

SideEffects [None.]

SeeAlso []

Definition at line 130 of file calPipeline.c.

00131 {
00132   CalBddPostProcessing(bddManager);
00133   if(bddManager->pipelineState != READY){
00134     CalBddWarningMessage("Pipeline cannot be initialized");
00135     return 0;
00136   }
00137   else{
00138     bddManager->pipelineState = CREATE;
00139     switch(bddOp){
00140     case CAL_AND :
00141       bddManager->pipelineFn = CalOpAnd;
00142       break;
00143     case CAL_OR  :
00144       bddManager->pipelineFn = CalOpOr;
00145       break;
00146     case CAL_XOR :
00147       bddManager->pipelineFn = CalOpXor;
00148       break;
00149     default  :
00150       CalBddWarningMessage("Unknown Bdd Operation type");
00151       return 0;
00152     }
00153     return 1;
00154   }  
00155 }

void Cal_PipelineQuit ( Cal_BddManager  bddManager  ) 

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

Synopsis [Resets the pipeline freeing all resources.]

Description [The user must make sure to update all provisional BDDs of interest before calling this routine.]

SideEffects []

SeeAlso []

Definition at line 363 of file calPipeline.c.

00364 {
00365   CalRequestNode_t *requestNode, *next;
00366   int i;
00367 
00368   bddManager->pipelineState = READY;
00369   for(i = 0; i < bddManager->pipelineDepth; i++){
00370     for(requestNode = bddManager->requestNodeListArray[i], 
00371         bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t);
00372         requestNode != Cal_Nil(CalRequestNode_t);
00373         requestNode = next){
00374       next = CalRequestNodeGetNextRequestNode(requestNode);
00375       CalNodeManagerFreeNode(bddManager->nodeManagerArray[0], requestNode);
00376     }
00377     bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t);
00378   }
00379   bddManager->pipelineDepth = 0;
00380   for (requestNode = bddManager->userProvisionalNodeList; requestNode;
00381        requestNode = next){
00382     next = CalRequestNodeGetNextRequestNode(requestNode);
00383     CalNodeManagerFreeNode(bddManager->nodeManagerArray[0],
00384                            requestNode);
00385   }
00386   bddManager->userProvisionalNodeList = Cal_Nil(CalRequestNode_t);
00387 }

void Cal_PipelineSetDepth ( Cal_BddManager  bddManager,
int  depth 
)

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

FileName [calPipeline.c]

PackageName [cal]

Synopsis [Routines for creating and managing the pipelined BDD operations.]

Description [Eventually we would like to have this feature transparent to the user.]

SeeAlso [optional]

Author [ Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@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
calPipeline.c,v 1.1.1.3 1998/05/04 00:59:01 hsv Exp

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

Synopsis [Set depth of a BDD pipeline.]

Description [The "depth" determines the amount of dependency we would allow in pipelined computation.]

SideEffects [None.]

SeeAlso []

Definition at line 91 of file calPipeline.c.

00092 {
00093   int i, j;
00094   if(depth > 6){
00095     CalBddWarningMessage("PipelineDepth can not exceed 6\n");
00096     CalBddWarningMessage("setting PipelineDepth to 6\n");
00097     depth = 6;
00098   }
00099   if(bddManager->maxDepth < depth){
00100     int oldMaxDepth = bddManager->maxDepth;
00101     bddManager->depth = bddManager->maxDepth = depth;
00102     bddManager->reqQue = Cal_MemRealloc(CalHashTable_t **, bddManager->reqQue,
00103                                  bddManager->maxDepth);
00104     for(i = oldMaxDepth; i < bddManager->maxDepth; i++){
00105       bddManager->reqQue[i] = Cal_MemAlloc(CalHashTable_t *, bddManager->maxNumVars+1);
00106       for(j = 0; j < bddManager->numVars+1; j++){
00107         bddManager->reqQue[i][j] =
00108             CalHashTableInit(bddManager, j);
00109       }
00110     }
00111   }
00112   else{
00113     bddManager->depth = depth;
00114   }  
00115 }

Cal_Bdd Cal_PipelineUpdateProvisionalBdd ( Cal_BddManager  bddManager,
Cal_Bdd  provisionalBdd 
)

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

Synopsis [Update a provisional Bdd obtained during pipelining.]

Description [The provisional BDD is automatically freed after quitting pipeline.]

SideEffects []

SeeAlso []

Definition at line 318 of file calPipeline.c.

00320 {
00321   Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, provisionalBdd);
00322   if(bddManager->pipelineState != UPDATE){
00323     CalBddWarningMessage("Provisional Bdd cannot be updated");
00324     return (Cal_Bdd) 0;
00325   }
00326   CalBddGetThenBdd(calBdd, calBdd);
00327   return CalBddGetExternalBdd(bddManager, calBdd);
00328 }

void CalBddReorderFixProvisionalNodes ( Cal_BddManager_t *  bddManager  ) 

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 404 of file calPipeline.c.

00405 {
00406   CalRequestNode_t **requestNodeListArray =
00407       bddManager->requestNodeListArray;
00408   CalRequestNode_t *node, *nextNode;
00409   int i;
00410   Cal_Bdd_t thenBdd, elseBdd;
00411   
00412   for (i=0;
00413        i<bddManager->pipelineDepth-bddManager->currentPipelineDepth;
00414        i++){ 
00415     for (node = *requestNodeListArray; node; node = nextNode){
00416       nextNode = CalBddNodeGetNextBddNode(node);
00417       Cal_Assert(CalBddNodeIsForwarded(node));
00418       CalBddNodeGetThenBdd(node, thenBdd);
00419       if (CalBddIsForwarded(thenBdd)) {
00420         CalBddForward(thenBdd);
00421       }
00422       CalBddNodePutThenBdd(node, thenBdd);
00423       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00424     }
00425     requestNodeListArray++;
00426   }
00427   for (; i<bddManager->pipelineDepth; i++){
00428     for (node = *requestNodeListArray; node; node = nextNode){
00429       nextNode = CalBddNodeGetNextBddNode(node);
00430       Cal_Assert(CalBddNodeIsForwarded(node) == 0);
00431       CalBddNodeGetThenBdd(node, thenBdd);
00432       if (CalBddIsForwarded(thenBdd)) {
00433         CalBddForward(thenBdd);
00434       }
00435       CalBddNodePutThenBdd(node, thenBdd);
00436       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00437       CalBddNodeGetElseBdd(node, elseBdd);
00438       if (CalBddIsForwarded(elseBdd)) {
00439         CalBddForward(elseBdd);
00440       }
00441       CalBddNodePutElseBdd(node, elseBdd);
00442       Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
00443     }
00444     requestNodeListArray++;
00445   }
00446 }

void CalCheckPipelineValidity ( Cal_BddManager_t *  bddManager  ) 

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 460 of file calPipeline.c.

00461 {
00462   CalRequestNode_t **requestNodeListArray =
00463       bddManager->requestNodeListArray;
00464   CalRequestNode_t *node, *nextNode;
00465   int i;
00466   Cal_Bdd_t thenBdd, elseBdd;
00467   
00468   for (i=0;
00469        i<bddManager->pipelineDepth-bddManager->currentPipelineDepth;
00470        i++){ 
00471     for (node = *requestNodeListArray; node; node = nextNode){
00472       nextNode = CalBddNodeGetNextBddNode(node);
00473       Cal_Assert(CalBddNodeIsForwarded(node));
00474       CalBddNodeGetThenBdd(node, thenBdd);
00475       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00476     }
00477     requestNodeListArray++;
00478   }
00479   for (; i<bddManager->pipelineDepth; i++){
00480     for (node = *requestNodeListArray; node; node = nextNode){
00481       nextNode = CalBddNodeGetNextBddNode(node);
00482       Cal_Assert(CalBddNodeIsForwarded(node) == 0); 
00483       CalBddNodeGetThenBdd(node, thenBdd);
00484       /*Cal_Assert(CalBddIsForwarded(thenBdd) == 0);*/
00485       /* This is possible since the actual BDD of thenBdd could have been
00486          computed and it is forwarded, however this node is not yet
00487          updated with the result */
00488       CalBddNodeGetElseBdd(node, elseBdd);
00489       /*Cal_Assert(CalBddIsForwarded(elseBdd) == 0);*/
00490     }
00491     requestNodeListArray++;
00492   }
00493 }

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