source: vis_dev/glu-2.3/src/calBdd/calBddCompose.c @ 27

Last change on this file since 27 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 12.1 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calBddCompose.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routine for composing one BDD into another.]
8
9  Description []
10
11  SeeAlso     []
12
13  Author      [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)
14               Rajeev Ranjan   (rajeev@eecs.berkeley.edu)
15               ]
16  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
17  All rights reserved.
18
19  Permission is hereby granted, without written agreement and without license
20  or royalty fees, to use, copy, modify, and distribute this software and its
21  documentation for any purpose, provided that the above copyright notice and
22  the following two paragraphs appear in all copies of this software.
23
24  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
25  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
26  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
27  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28
29  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
30  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
31  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
32  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
33  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
34
35  Revision    [$Id: calBddCompose.c,v 1.1.1.3 1998/05/04 00:58:50 hsv Exp $]
36
37******************************************************************************/
38
39#include "calInt.h"
40
41/*---------------------------------------------------------------------------*/
42/* Constant declarations                                                     */
43/*---------------------------------------------------------------------------*/
44
45/*---------------------------------------------------------------------------*/
46/* Type declarations                                                         */
47/*---------------------------------------------------------------------------*/
48
49/*---------------------------------------------------------------------------*/
50/* Stucture declarations                                                     */
51/*---------------------------------------------------------------------------*/
52
53/*---------------------------------------------------------------------------*/
54/* Variable declarations                                                     */
55/*---------------------------------------------------------------------------*/
56
57/*---------------------------------------------------------------------------*/
58/* Macro declarations                                                        */
59/*---------------------------------------------------------------------------*/
60
61/**AutomaticStart*************************************************************/
62
63/*---------------------------------------------------------------------------*/
64/* Static function prototypes                                                */
65/*---------------------------------------------------------------------------*/
66
67
68/**AutomaticEnd***************************************************************/
69
70/*---------------------------------------------------------------------------*/
71/* Definition of exported functions                                          */
72/*---------------------------------------------------------------------------*/
73
74/**Function********************************************************************
75
76  Synopsis    [composition - substitute a BDD variable by a function]
77
78  Description [Returns the BDD obtained by substituting a variable by a function]
79
80  SideEffects [None]
81
82******************************************************************************/
83Cal_Bdd
84Cal_BddCompose(Cal_BddManager bddManager, Cal_Bdd  fUserBdd,
85               Cal_Bdd  gUserBdd, Cal_Bdd hUserBdd)
86{
87  Cal_Bdd_t result;
88  CalRequestNode_t *requestNode;
89  Cal_Bdd_t F, G, H;
90 
91  if (CalBddPreProcessing(bddManager, 3, fUserBdd, gUserBdd, hUserBdd) == 0){
92    result = bddManager->bddNull;
93  }
94  F = CalBddGetInternalBdd(bddManager, fUserBdd);
95  G = CalBddGetInternalBdd(bddManager, gUserBdd);
96  H = CalBddGetInternalBdd(bddManager, hUserBdd);
97
98  if(CalBddIsBddConst(G)){
99    CalBddNodeIcrRefCount(fUserBdd);
100    return fUserBdd;
101  }
102  CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
103  CalRequestNodePutF(requestNode, F);
104  CalRequestNodePutG(requestNode, H);
105  CalRequestNodePutNextRequestNode(requestNode, 0);
106  bddManager->requestNodeListArray[0] = requestNode;
107  /*
108  ** We can achieve a superscalar compose operation, provided G
109  ** is the same for all the compose operation
110  */
111
112  CalRequestNodeListCompose(bddManager, bddManager->requestNodeListArray[0],
113      CalBddGetBddIndex(bddManager, G));
114
115  CalRequestNodeGetThenRequest(requestNode, result);
116  CalNodeManagerFreeNode(bddManager->nodeManagerArray[0], requestNode);
117  bddManager->requestNodeListArray[0] = Cal_Nil(CalRequestNode_t);
118
119  return CalBddGetExternalBdd(bddManager, result);
120}
121
122/*---------------------------------------------------------------------------*/
123/* Definition of internal functions                                          */
124/*---------------------------------------------------------------------------*/
125/**Function********************************************************************
126
127  Synopsis    [required]
128
129  Description [optional]
130
131  SideEffects [required]
132
133  SeeAlso     [optional]
134
135  note        [THERE IS A POSSIBILITY OF HAVING A PIPELINED VERSION
136               NEED TO THINK IT THROUGH]
137
138******************************************************************************/
139void
140CalRequestNodeListCompose(Cal_BddManager_t * bddManager,
141                          CalRequestNode_t * requestNodeList,
142                          Cal_BddIndex_t  composeIndex)
143{
144  CalRequestNode_t *requestNode;
145  CalRequest_t F, H, result;
146  int bddId, bddIndex;
147  CalHashTable_t *hashTable, *uniqueTableForId;
148  CalHashTable_t **reqQueForCompose = bddManager->reqQue[0];
149  CalHashTable_t **reqQueForITE = bddManager->reqQue[1]; 
150 
151  /* ReqQueForComposeInsertUsingReqList */
152  for(requestNode = requestNodeList;
153      requestNode != Cal_Nil(CalRequestNode_t);
154      requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
155    CalRequestNodeGetF(requestNode, F);
156    CalRequestNodeGetG(requestNode, H);
157    CalComposeRequestCreate(bddManager, F, H, composeIndex, 
158        reqQueForCompose, reqQueForITE, &result);
159    CalRequestNodePutThenRequest(requestNode, result);
160    CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
161  }
162
163  /* ReqQueApply */
164  for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
165    bddId = bddManager->indexToId[bddIndex];
166    hashTable = reqQueForCompose[bddId];
167    if(hashTable->numEntries){
168      CalHashTableComposeApply(bddManager, hashTable, composeIndex, 
169          reqQueForCompose, reqQueForITE);
170    }
171    hashTable = reqQueForITE[bddId];
172    if(hashTable->numEntries){
173      CalHashTableITEApply(bddManager, hashTable, reqQueForITE);
174    }
175  }
176
177  /* ReqQueReduce */
178  for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
179    bddId = bddManager->indexToId[bddIndex];
180    uniqueTableForId = bddManager->uniqueTable[bddId];
181    hashTable = reqQueForCompose[bddId];
182    if(hashTable->numEntries){
183      CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
184    }
185    hashTable = reqQueForITE[bddId];
186    if(hashTable->numEntries){
187      CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
188    }
189  }
190
191  /* ReqListArrayReqForward */
192  for(requestNode = requestNodeList; requestNode != Cal_Nil(CalRequestNode_t);
193      requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
194    CalRequestNodeGetThenRequest(requestNode, result);
195    CalRequestIsForwardedTo(result);
196    CalRequestNodePutThenRequest(requestNode, result);
197  }
198
199  /* ReqQueCleanUp */
200  for(bddId = 1; bddId <= bddManager->numVars; bddId++){
201    CalHashTableCleanUp(reqQueForCompose[bddId]);
202    CalHashTableCleanUp(reqQueForITE[bddId]);
203  }
204}
205
206
207/**Function********************************************************************
208
209  Synopsis    [required]
210
211  Description [optional]
212
213  SideEffects [required]
214
215  SeeAlso     [optional]
216
217******************************************************************************/
218void
219CalHashTableComposeApply(Cal_BddManager_t *bddManager,
220                         CalHashTable_t *hashTable,
221                         Cal_BddIndex_t  gIndex,
222                         CalHashTable_t **reqQueForCompose,
223                         CalHashTable_t **reqQueForITE)
224{
225  int i, numBins = hashTable->numBins;
226  CalBddNode_t **bins = hashTable->bins;
227  CalRequestNode_t *requestNode;
228  Cal_Bdd_t fx, fxbar;
229  Cal_Bdd_t hx, hxbar;
230  Cal_Bdd_t calBdd1, calBdd2, calBdd3;
231  Cal_Bdd_t result;
232  Cal_BddId_t bddId;
233  Cal_BddIndex_t index;
234 
235  for(i = 0; i < numBins; i++){
236    for(requestNode = bins[i];
237        requestNode != Cal_Nil(CalRequestNode_t);
238        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
239
240      /* Process the requestNode */
241      CalRequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, hx, hxbar);
242
243      /* Process left cofactor */
244      index = CalBddGetBddIndex(bddManager, fx);
245      if(index > gIndex){
246        CalBddIcrRefCount(fx);
247        CalRequestNodePutThenRequest(requestNode, fx);
248      }
249      else if(index < gIndex){
250        CalBddGetMinId2(bddManager, fx, hx, bddId);
251        CalHashTableFindOrAdd(reqQueForCompose[bddId], fx, hx, &result);
252        CalBddIcrRefCount(result);
253        CalRequestNodePutThenRequest(requestNode, result);
254      }
255      else{
256        /* fxIndex == gIndex */
257        /* RequestNodeThen = ITE(hx, fxThen, fxElse) */
258        calBdd1 = hx;
259        CalBddGetThenBdd(fx, calBdd2);
260        CalBddGetElseBdd(fx, calBdd3);
261        result = CalOpITE(bddManager, calBdd1, calBdd2, calBdd3, reqQueForITE);
262        CalBddIcrRefCount(result);
263        CalRequestNodePutThenRequest(requestNode, result);
264      }
265
266      /* Process right cofactor */
267      index = CalBddGetBddIndex(bddManager, fxbar);
268      if(index > gIndex){
269        CalBddIcrRefCount(fxbar);
270        CalRequestNodePutElseRequest(requestNode, fxbar);
271      }
272      else if(index < gIndex){
273        CalBddGetMinId2(bddManager, fxbar, hxbar, bddId);
274        CalHashTableFindOrAdd(reqQueForCompose[bddId], fxbar, hxbar, &result);
275        CalBddIcrRefCount(result);
276        CalRequestNodePutElseRequest(requestNode, result);
277      }
278      else{
279        /* fxbarIndex == gIndex */
280        /* RequestNodeElse = ITE(hxbar, fxbarThen, fxbarElse) */
281        calBdd1 = hxbar;
282        CalBddGetThenBdd(fxbar, calBdd2);
283        CalBddGetElseBdd(fxbar, calBdd3);
284        result = CalOpITE(bddManager, calBdd1, calBdd2, calBdd3, reqQueForITE);
285        CalBddIcrRefCount(result);
286        CalRequestNodePutElseRequest(requestNode, result);
287      }
288    }
289  }
290}
291
292/**Function********************************************************************
293
294  Synopsis    [required]
295
296  Description [optional]
297
298  SideEffects [required]
299
300  SeeAlso     [optional]
301
302******************************************************************************/
303void
304CalComposeRequestCreate(Cal_BddManager_t * bddManager,
305                        Cal_Bdd_t  f,
306                        Cal_Bdd_t  h,
307                        Cal_BddIndex_t  composeIndex,
308                        CalHashTable_t **reqQueForCompose,
309                        CalHashTable_t **reqQueForITE,
310                        Cal_Bdd_t *resultPtr)
311{
312  Cal_BddIndex_t index;
313  Cal_BddId_t bddId;
314
315  index = CalBddGetBddIndex(bddManager, f);
316  if(index > composeIndex){
317    *resultPtr = f;
318  }
319  else if(index < composeIndex){
320    CalBddGetMinId2(bddManager, f, h, bddId);
321    CalHashTableFindOrAdd(reqQueForCompose[bddId], f, h, resultPtr);
322  }
323  else{
324    Cal_Bdd_t calBdd1, calBdd2, calBdd3;
325    calBdd1 = h;
326    CalBddGetThenBdd(f, calBdd2);
327    CalBddGetElseBdd(f, calBdd3);
328    *resultPtr = CalOpITE(bddManager, calBdd1, calBdd2, calBdd3, reqQueForITE);
329  }
330}
331
332/*---------------------------------------------------------------------------*/
333/* Definition of static functions                                            */
334/*---------------------------------------------------------------------------*/
Note: See TracBrowser for help on using the repository browser.