src/calBdd/calBddCompose.c File Reference

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

Go to the source code of this file.

Functions

Cal_Bdd Cal_BddCompose (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd, Cal_Bdd hUserBdd)
void CalRequestNodeListCompose (Cal_BddManager_t *bddManager, CalRequestNode_t *requestNodeList, Cal_BddIndex_t composeIndex)
void CalHashTableComposeApply (Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, Cal_BddIndex_t gIndex, CalHashTable_t **reqQueForCompose, CalHashTable_t **reqQueForITE)
void CalComposeRequestCreate (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t h, Cal_BddIndex_t composeIndex, CalHashTable_t **reqQueForCompose, CalHashTable_t **reqQueForITE, Cal_Bdd_t *resultPtr)

Function Documentation

Cal_Bdd Cal_BddCompose ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd,
Cal_Bdd  gUserBdd,
Cal_Bdd  hUserBdd 
)

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

FileName [calBddCompose.c]

PackageName [cal]

Synopsis [Routine for composing one BDD into another.]

Description []

SeeAlso []

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

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

Synopsis [composition - substitute a BDD variable by a function]

Description [Returns the BDD obtained by substituting a variable by a function]

SideEffects [None]

Definition at line 84 of file calBddCompose.c.

00086 {
00087   Cal_Bdd_t result;
00088   CalRequestNode_t *requestNode;
00089   Cal_Bdd_t F, G, H;
00090   
00091   if (CalBddPreProcessing(bddManager, 3, fUserBdd, gUserBdd, hUserBdd) == 0){
00092     result = bddManager->bddNull;
00093   }
00094   F = CalBddGetInternalBdd(bddManager, fUserBdd);
00095   G = CalBddGetInternalBdd(bddManager, gUserBdd);
00096   H = CalBddGetInternalBdd(bddManager, hUserBdd);
00097 
00098   if(CalBddIsBddConst(G)){
00099     CalBddNodeIcrRefCount(fUserBdd);
00100     return fUserBdd;
00101   }
00102   CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
00103   CalRequestNodePutF(requestNode, F);
00104   CalRequestNodePutG(requestNode, H);
00105   CalRequestNodePutNextRequestNode(requestNode, 0);
00106   bddManager->requestNodeListArray[0] = requestNode;
00107   /*
00108   ** We can achieve a superscalar compose operation, provided G
00109   ** is the same for all the compose operation 
00110   */
00111 
00112   CalRequestNodeListCompose(bddManager, bddManager->requestNodeListArray[0],
00113       CalBddGetBddIndex(bddManager, G));
00114 
00115   CalRequestNodeGetThenRequest(requestNode, result);
00116   CalNodeManagerFreeNode(bddManager->nodeManagerArray[0], requestNode);
00117   bddManager->requestNodeListArray[0] = Cal_Nil(CalRequestNode_t);
00118 
00119   return CalBddGetExternalBdd(bddManager, result);
00120 }

void CalComposeRequestCreate ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
Cal_Bdd_t  h,
Cal_BddIndex_t  composeIndex,
CalHashTable_t **  reqQueForCompose,
CalHashTable_t **  reqQueForITE,
Cal_Bdd_t *  resultPtr 
)

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 304 of file calBddCompose.c.

00311 {
00312   Cal_BddIndex_t index;
00313   Cal_BddId_t bddId;
00314 
00315   index = CalBddGetBddIndex(bddManager, f);
00316   if(index > composeIndex){
00317     *resultPtr = f;
00318   }
00319   else if(index < composeIndex){
00320     CalBddGetMinId2(bddManager, f, h, bddId);
00321     CalHashTableFindOrAdd(reqQueForCompose[bddId], f, h, resultPtr);
00322   }
00323   else{
00324     Cal_Bdd_t calBdd1, calBdd2, calBdd3;
00325     calBdd1 = h;
00326     CalBddGetThenBdd(f, calBdd2);
00327     CalBddGetElseBdd(f, calBdd3);
00328     *resultPtr = CalOpITE(bddManager, calBdd1, calBdd2, calBdd3, reqQueForITE);
00329   }
00330 }

void CalHashTableComposeApply ( Cal_BddManager_t *  bddManager,
CalHashTable_t *  hashTable,
Cal_BddIndex_t  gIndex,
CalHashTable_t **  reqQueForCompose,
CalHashTable_t **  reqQueForITE 
)

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 219 of file calBddCompose.c.

00224 {
00225   int i, numBins = hashTable->numBins;
00226   CalBddNode_t **bins = hashTable->bins;
00227   CalRequestNode_t *requestNode;
00228   Cal_Bdd_t fx, fxbar;
00229   Cal_Bdd_t hx, hxbar;
00230   Cal_Bdd_t calBdd1, calBdd2, calBdd3;
00231   Cal_Bdd_t result;
00232   Cal_BddId_t bddId;
00233   Cal_BddIndex_t index;
00234   
00235   for(i = 0; i < numBins; i++){
00236     for(requestNode = bins[i];
00237         requestNode != Cal_Nil(CalRequestNode_t);
00238         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00239 
00240       /* Process the requestNode */
00241       CalRequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, hx, hxbar);
00242 
00243       /* Process left cofactor */
00244       index = CalBddGetBddIndex(bddManager, fx);
00245       if(index > gIndex){
00246         CalBddIcrRefCount(fx);
00247         CalRequestNodePutThenRequest(requestNode, fx);
00248       }
00249       else if(index < gIndex){
00250         CalBddGetMinId2(bddManager, fx, hx, bddId);
00251         CalHashTableFindOrAdd(reqQueForCompose[bddId], fx, hx, &result);
00252         CalBddIcrRefCount(result);
00253         CalRequestNodePutThenRequest(requestNode, result);
00254       }
00255       else{
00256         /* fxIndex == gIndex */
00257         /* RequestNodeThen = ITE(hx, fxThen, fxElse) */
00258         calBdd1 = hx;
00259         CalBddGetThenBdd(fx, calBdd2);
00260         CalBddGetElseBdd(fx, calBdd3);
00261         result = CalOpITE(bddManager, calBdd1, calBdd2, calBdd3, reqQueForITE);
00262         CalBddIcrRefCount(result);
00263         CalRequestNodePutThenRequest(requestNode, result);
00264       }
00265 
00266       /* Process right cofactor */
00267       index = CalBddGetBddIndex(bddManager, fxbar);
00268       if(index > gIndex){
00269         CalBddIcrRefCount(fxbar);
00270         CalRequestNodePutElseRequest(requestNode, fxbar);
00271       }
00272       else if(index < gIndex){
00273         CalBddGetMinId2(bddManager, fxbar, hxbar, bddId);
00274         CalHashTableFindOrAdd(reqQueForCompose[bddId], fxbar, hxbar, &result);
00275         CalBddIcrRefCount(result);
00276         CalRequestNodePutElseRequest(requestNode, result);
00277       }
00278       else{
00279         /* fxbarIndex == gIndex */
00280         /* RequestNodeElse = ITE(hxbar, fxbarThen, fxbarElse) */
00281         calBdd1 = hxbar;
00282         CalBddGetThenBdd(fxbar, calBdd2);
00283         CalBddGetElseBdd(fxbar, calBdd3);
00284         result = CalOpITE(bddManager, calBdd1, calBdd2, calBdd3, reqQueForITE);
00285         CalBddIcrRefCount(result);
00286         CalRequestNodePutElseRequest(requestNode, result);
00287       }
00288     }
00289   }
00290 }

void CalRequestNodeListCompose ( Cal_BddManager_t *  bddManager,
CalRequestNode_t *  requestNodeList,
Cal_BddIndex_t  composeIndex 
)

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

note [THERE IS A POSSIBILITY OF HAVING A PIPELINED VERSION NEED TO THINK IT THROUGH]

Definition at line 140 of file calBddCompose.c.

00143 {
00144   CalRequestNode_t *requestNode;
00145   CalRequest_t F, H, result;
00146   int bddId, bddIndex;
00147   CalHashTable_t *hashTable, *uniqueTableForId;
00148   CalHashTable_t **reqQueForCompose = bddManager->reqQue[0];
00149   CalHashTable_t **reqQueForITE = bddManager->reqQue[1]; 
00150   
00151   /* ReqQueForComposeInsertUsingReqList */
00152   for(requestNode = requestNodeList;
00153       requestNode != Cal_Nil(CalRequestNode_t);
00154       requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00155     CalRequestNodeGetF(requestNode, F);
00156     CalRequestNodeGetG(requestNode, H);
00157     CalComposeRequestCreate(bddManager, F, H, composeIndex, 
00158         reqQueForCompose, reqQueForITE, &result);
00159     CalRequestNodePutThenRequest(requestNode, result);
00160     CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00161   }
00162 
00163   /* ReqQueApply */
00164   for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00165     bddId = bddManager->indexToId[bddIndex];
00166     hashTable = reqQueForCompose[bddId];
00167     if(hashTable->numEntries){
00168       CalHashTableComposeApply(bddManager, hashTable, composeIndex, 
00169           reqQueForCompose, reqQueForITE);
00170     }
00171     hashTable = reqQueForITE[bddId];
00172     if(hashTable->numEntries){
00173       CalHashTableITEApply(bddManager, hashTable, reqQueForITE);
00174     }
00175   }
00176 
00177   /* ReqQueReduce */
00178   for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
00179     bddId = bddManager->indexToId[bddIndex];
00180     uniqueTableForId = bddManager->uniqueTable[bddId];
00181     hashTable = reqQueForCompose[bddId];
00182     if(hashTable->numEntries){
00183       CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00184     }
00185     hashTable = reqQueForITE[bddId];
00186     if(hashTable->numEntries){
00187       CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00188     }
00189   }
00190 
00191   /* ReqListArrayReqForward */
00192   for(requestNode = requestNodeList; requestNode != Cal_Nil(CalRequestNode_t);
00193       requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00194     CalRequestNodeGetThenRequest(requestNode, result);
00195     CalRequestIsForwardedTo(result);
00196     CalRequestNodePutThenRequest(requestNode, result);
00197   }
00198 
00199   /* ReqQueCleanUp */
00200   for(bddId = 1; bddId <= bddManager->numVars; bddId++){
00201     CalHashTableCleanUp(reqQueForCompose[bddId]);
00202     CalHashTableCleanUp(reqQueForITE[bddId]);
00203   }
00204 }

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