source: vis_dev/glu-2.3/src/calBdd/calBddOp.c @ 50

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

library glu 2.3
File size: 33.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calBddOp.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routines for performing simple boolean operations on a
8  pair of BDDs or on an array of pair of BDDs or on an array of BDDs.]
9
10  Description [The "cal" specific routines are "Cal_BddPairwiseAnd/Or",
11  "Cal_BddMultiwayAnd/Or".]
12
13  SeeAlso     [optional]
14
15  Author      [Rajeev Ranjan   (rajeev@eecs.berkeley.edu)
16               Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)
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: calBddOp.c,v 1.1.1.3 1998/05/04 00:58:52 hsv 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
60/*---------------------------------------------------------------------------*/
61/* Macro declarations                                                        */
62/*---------------------------------------------------------------------------*/
63
64/**AutomaticStart*************************************************************/
65
66/*---------------------------------------------------------------------------*/
67/* Static function prototypes                                                */
68/*---------------------------------------------------------------------------*/
69
70static Cal_Bdd_t * BddArrayOpBF(Cal_BddManager_t * bddManager, Cal_Bdd_t* bddArray, int numFunction, CalOpProc_t calOpProc);
71static Cal_Bdd_t BddMultiwayOp(Cal_BddManager_t * bddManager, Cal_Bdd_t * calBddArray, int numBdds, CalOpProc_t op);
72static void BddArrayToRequestNodeListArray(Cal_BddManager_t * bddManager, Cal_Bdd_t * calBddArray, int numBdds);
73static int CeilLog2(int number);
74
75/**AutomaticEnd***************************************************************/
76
77/*---------------------------------------------------------------------------*/
78/* Definition of exported functions                                          */
79/*---------------------------------------------------------------------------*/
80/**Function********************************************************************
81
82  Synopsis    [Returns the BDD for logical AND of argument BDDs]
83
84  Description [Returns the BDD for logical AND of f and g]
85
86  SideEffects [None]
87
88******************************************************************************/
89Cal_Bdd
90Cal_BddAnd(
91  Cal_BddManager bddManager,
92  Cal_Bdd  fUserBdd,
93  Cal_Bdd  gUserBdd)
94{
95  Cal_Bdd_t result;
96  Cal_Bdd userResult;
97  Cal_Bdd_t F, G;
98
99  if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
100    F = CalBddGetInternalBdd(bddManager, fUserBdd);
101    G = CalBddGetInternalBdd(bddManager, gUserBdd);
102    result = CalBddOpBF(bddManager, CalOpAnd, F, G);
103  }
104  else {
105    return (Cal_Bdd)0;
106  }
107  userResult =  CalBddGetExternalBdd(bddManager, result);
108  if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
109    Cal_BddFree(bddManager, userResult);
110    Cal_BddManagerGC(bddManager);
111    return (Cal_Bdd) 0;
112  }
113  return userResult;
114}
115
116/**Function********************************************************************
117
118  Synopsis    [Returns the BDD for logical NAND of argument BDDs]
119
120  Description [Returns the BDD for logical NAND of f and g]
121
122  SideEffects [None]
123
124******************************************************************************/
125Cal_Bdd
126Cal_BddNand(
127  Cal_BddManager bddManager,
128  Cal_Bdd fUserBdd,
129  Cal_Bdd gUserBdd)
130{
131  Cal_Bdd_t result;
132  Cal_Bdd_t F, G;
133  Cal_Bdd userResult;
134  if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
135    F = CalBddGetInternalBdd(bddManager, fUserBdd); 
136    G = CalBddGetInternalBdd(bddManager, gUserBdd); 
137    result = CalBddOpBF(bddManager, CalOpNand, F, G);
138  }
139  else{
140    return (Cal_Bdd) 0;
141  }
142  userResult =  CalBddGetExternalBdd(bddManager, result);
143  if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
144    Cal_BddFree(bddManager, userResult);
145    Cal_BddManagerGC(bddManager);
146    return (Cal_Bdd) 0;
147  }
148  return userResult;
149}
150
151/**Function********************************************************************
152
153  Synopsis    [Returns the BDD for logical OR of argument BDDs]
154
155  Description [Returns the BDD for logical OR of f and g]
156
157  SideEffects [None]
158
159******************************************************************************/
160Cal_Bdd
161Cal_BddOr(Cal_BddManager bddManager,
162          Cal_Bdd fUserBdd,
163          Cal_Bdd gUserBdd)
164{
165  Cal_Bdd_t result;
166  Cal_Bdd_t F, G;
167  Cal_Bdd userResult;
168  if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
169    F = CalBddGetInternalBdd(bddManager, fUserBdd); 
170    G = CalBddGetInternalBdd(bddManager, gUserBdd); 
171    result = CalBddOpBF(bddManager, CalOpOr, F, G);
172  }
173  else{
174    return (Cal_Bdd) 0;
175  }
176  userResult =  CalBddGetExternalBdd(bddManager, result);
177  if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
178    Cal_BddFree(bddManager, userResult);
179    Cal_BddManagerGC(bddManager);
180    return (Cal_Bdd) 0;
181  }
182  return userResult;
183}
184
185/**Function********************************************************************
186
187  Synopsis    [Returns the BDD for logical NOR of argument BDDs]
188
189  Description [Returns the BDD for logical NOR of f and g]
190
191  SideEffects [None]
192
193******************************************************************************/
194Cal_Bdd
195Cal_BddNor(Cal_BddManager bddManager,
196           Cal_Bdd fUserBdd,
197           Cal_Bdd gUserBdd)
198{
199  Cal_Bdd_t result;
200  Cal_Bdd userResult;
201  Cal_Bdd_t F, G;
202  if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
203    F = CalBddGetInternalBdd(bddManager, fUserBdd); 
204    G = CalBddGetInternalBdd(bddManager, gUserBdd); 
205    result = CalBddOpBF(bddManager, CalOpOr, F, G);
206    CalBddNot(result, result);
207  }
208  else{
209    return (Cal_Bdd) 0;
210  }
211  userResult =  CalBddGetExternalBdd(bddManager, result);
212  if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
213    Cal_BddFree(bddManager, userResult);
214    Cal_BddManagerGC(bddManager);
215    return (Cal_Bdd) 0;
216  }
217  return userResult;
218}
219
220/**Function********************************************************************
221
222  Synopsis    [Returns the BDD for logical exclusive OR of argument BDDs]
223
224  Description [Returns the BDD for logical exclusive OR of f and g]
225
226  SideEffects [None]
227
228******************************************************************************/
229Cal_Bdd
230Cal_BddXor(Cal_BddManager bddManager,
231           Cal_Bdd fUserBdd,
232           Cal_Bdd gUserBdd)
233{
234  Cal_Bdd_t result;
235  Cal_Bdd userResult;
236  Cal_Bdd_t F, G;
237  if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
238    F = CalBddGetInternalBdd(bddManager, fUserBdd); 
239    G = CalBddGetInternalBdd(bddManager, gUserBdd); 
240    result = CalBddOpBF(bddManager, CalOpXor, F, G);
241  }
242  else{
243    return (Cal_Bdd) 0;
244  }
245  userResult =  CalBddGetExternalBdd(bddManager, result);
246  if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
247    Cal_BddFree(bddManager, userResult);
248    Cal_BddManagerGC(bddManager);
249    return (Cal_Bdd) 0;
250  }
251  return userResult;
252}
253
254/**Function********************************************************************
255
256  Synopsis    [Returns the BDD for logical exclusive NOR of argument BDDs]
257
258  Description [Returns the BDD for logical exclusive NOR of f and g]
259
260  SideEffects [None]
261
262******************************************************************************/
263Cal_Bdd
264Cal_BddXnor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
265{
266  Cal_Bdd_t result;
267  Cal_Bdd userResult;
268  Cal_Bdd_t F, G;
269  if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
270    F = CalBddGetInternalBdd(bddManager, fUserBdd); 
271    G = CalBddGetInternalBdd(bddManager, gUserBdd); 
272    result = CalBddOpBF(bddManager, CalOpXor, F, G);
273    CalBddNot(result, result);
274  }
275  else{
276    return (Cal_Bdd) 0;
277  }
278  userResult =  CalBddGetExternalBdd(bddManager, result);
279  if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
280    Cal_BddFree(bddManager, userResult);
281    Cal_BddManagerGC(bddManager);
282    return (Cal_Bdd) 0;
283  }
284  return userResult;
285}
286
287/**Function********************************************************************
288
289  Synopsis    [Returns an array of BDDs obtained by logical AND of BDD pairs
290  specified by an BDD array in which a BDD at an even location is paired with
291  a BDD at an odd location of the array]
292
293  Description [Returns an array of BDDs obtained by logical AND of BDD pairs
294  specified by an BDD array in which a BDD at an even location is paired with
295  a BDD at an odd location of the array]
296
297  SideEffects [None]
298
299  SeeAlso     [Cal_BddPairwiseOr]
300
301******************************************************************************/
302Cal_Bdd *
303Cal_BddPairwiseAnd(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
304{
305  int i, num;
306  Cal_Bdd_t *bddArray;
307  Cal_Bdd_t *resultArray;
308  Cal_Bdd userBdd;
309  Cal_Bdd *userResultArray;
310 
311  for (num = 0; (userBdd = userBddArray[num]); num++){
312    if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
313      return Cal_Nil(Cal_Bdd);
314    }
315  }
316  if ((num == 0) || (num%2 != 0)){
317    fprintf(stdout,"Odd number of arguments passed to array AND\n");
318    return Cal_Nil(Cal_Bdd);
319  }
320  bddArray = Cal_MemAlloc(Cal_Bdd_t, num);
321  for (i = 0; i < num; i++){
322    bddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
323  }
324  resultArray =  BddArrayOpBF(bddManager, bddArray, num, CalOpAnd);
325  userResultArray = Cal_MemAlloc(Cal_Bdd, num/2);
326  for (i=0; i<num/2; i++){
327    userResultArray[i] = CalBddGetExternalBdd(bddManager, resultArray[i]);
328  }
329  Cal_MemFree(bddArray);
330  Cal_MemFree(resultArray);
331  if (CalBddPostProcessing(bddManager)  == CAL_BDD_OVERFLOWED){
332    for (i=0; i<num/2; i++){
333      Cal_BddFree(bddManager, userResultArray[i]);
334      userResultArray[i] = (Cal_Bdd) 0;
335    }
336    Cal_BddManagerGC(bddManager);
337    return userResultArray;
338  }
339  return userResultArray;
340}
341
342/**Function********************************************************************
343
344  Synopsis    [Returns an array of BDDs obtained by logical OR of BDD pairs
345  specified by an BDD array in which a BDD at an even location is paired with
346  a BDD at an odd location of the array]
347
348  Description [Returns an array of BDDs obtained by logical OR of BDD pairs
349  specified by an BDD array in which a BDD at an even location is paired with
350  a BDD at an odd location of the array]
351
352  SideEffects [None]
353
354  SeeAlso     [Cal_BddPairwiseAnd]
355
356******************************************************************************/
357Cal_Bdd *
358Cal_BddPairwiseOr(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
359{
360  int i, num=0;
361  Cal_Bdd_t *bddArray;
362  Cal_Bdd_t *resultArray;
363  Cal_Bdd userBdd;
364  Cal_Bdd *userResultArray;
365 
366  for (num = 0; (userBdd = userBddArray[num]); num++){
367    if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
368      return Cal_Nil(Cal_Bdd);
369    }
370  }
371  if ((num == 0) || (num%2 != 0)){
372    fprintf(stdout,"Odd number of arguments passed to array OR\n");
373    return Cal_Nil(Cal_Bdd);
374  }
375  bddArray = Cal_MemAlloc(Cal_Bdd_t, num);
376  for (i = 0; i < num; i++){
377    bddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
378  }
379  resultArray =  BddArrayOpBF(bddManager, bddArray, num, CalOpOr);
380  userResultArray = Cal_MemAlloc(Cal_Bdd, num/2);
381  for (i=0; i<num/2; i++){
382    userResultArray[i] = CalBddGetExternalBdd(bddManager, resultArray[i]);
383  }
384  Cal_MemFree(bddArray);
385  Cal_MemFree(resultArray);
386  return userResultArray;
387}
388
389/**Function********************************************************************
390
391  Synopsis    [Returns an array of BDDs obtained by logical XOR of BDD pairs
392  specified by an BDD array in which a BDD at an even location is paired with
393  a BDD at an odd location of the array]
394
395  Description [Returns an array of BDDs obtained by logical XOR of BDD pairs
396  specified by an BDD array in which a BDD at an even location is paired with
397  a BDD at an odd location of the array]
398
399  SideEffects [None]
400
401  SeeAlso     [Cal_BddPairwiseAnd]
402
403******************************************************************************/
404Cal_Bdd *
405Cal_BddPairwiseXor(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
406{
407  int i, num=0;
408  Cal_Bdd_t *bddArray;
409  Cal_Bdd_t *resultArray;
410  Cal_Bdd userBdd;
411  Cal_Bdd *userResultArray;
412 
413  for (num = 0; (userBdd = userBddArray[num]); num++){
414    if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
415      return Cal_Nil(Cal_Bdd);
416    }
417  }
418  if ((num == 0) || (num%2 != 0)){
419    fprintf(stdout,"Odd number of arguments passed to array OR\n");
420    return Cal_Nil(Cal_Bdd);
421  }
422  bddArray = Cal_MemAlloc(Cal_Bdd_t, num);
423  for (i = 0; i < num; i++){
424    bddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
425  }
426  resultArray =  BddArrayOpBF(bddManager, bddArray, num, CalOpXor);
427  userResultArray = Cal_MemAlloc(Cal_Bdd, num/2);
428  for (i=0; i<num/2; i++){
429    userResultArray[i] = CalBddGetExternalBdd(bddManager, resultArray[i]);
430  }
431  Cal_MemFree(bddArray);
432  Cal_MemFree(resultArray);
433  return userResultArray;
434}
435
436
437
438/**Function********************************************************************
439
440  Synopsis    [Returns the BDD for logical AND of argument BDDs]
441
442  Description [Returns the BDD for logical AND of set of BDDs in the bddArray]
443
444  SideEffects [None]
445
446******************************************************************************/
447Cal_Bdd
448Cal_BddMultiwayAnd(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
449{
450  int i, numBdds = 0;
451  Cal_Bdd_t result;
452  Cal_Bdd_t *calBddArray;
453  Cal_Bdd userBdd;
454
455  for (numBdds  = 0; (userBdd = userBddArray[numBdds]); numBdds++){
456    if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
457      return (Cal_Bdd) 0;
458    }
459  }
460 
461  if (numBdds == 0){
462    CalBddWarningMessage("Multiway AND called with 0 length array");
463    return (Cal_Bdd) 0;
464  }
465  else if (numBdds == 1){
466    return Cal_BddIdentity(bddManager, userBddArray[0]);
467  }
468  else{
469    calBddArray = Cal_MemAlloc(Cal_Bdd_t, numBdds+1);
470    for (i = 0; i < numBdds; i++){
471      calBddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
472    }
473    result = BddMultiwayOp(bddManager, calBddArray, numBdds, CalOpAnd);
474    Cal_MemFree(calBddArray);
475  }
476  return CalBddGetExternalBdd(bddManager, result);
477}
478 
479/**Function********************************************************************
480
481  Synopsis    [Returns the BDD for logical OR of argument BDDs]
482
483  Description [Returns the BDD for logical OR of set of BDDs in the bddArray]
484
485  SideEffects [None]
486
487******************************************************************************/
488Cal_Bdd
489Cal_BddMultiwayOr(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
490{
491  int i, numBdds = 0;
492  Cal_Bdd_t result;
493  Cal_Bdd_t *calBddArray;
494  Cal_Bdd userBdd;
495
496  for (numBdds = 0; (userBdd = userBddArray[numBdds]); numBdds++){
497    if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
498      return (Cal_Bdd) 0;
499    }
500  }
501 
502  if (numBdds == 0){
503    CalBddWarningMessage("Multiway OR called with 0 length array");
504    return (Cal_Bdd) 0;
505  }
506  else if (numBdds == 1){
507    return Cal_BddIdentity(bddManager, userBddArray[0]);
508  }
509  else{
510    calBddArray = Cal_MemAlloc(Cal_Bdd_t, numBdds+1);
511    for (i = 0; i < numBdds; i++){
512      calBddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
513    }
514    result = BddMultiwayOp(bddManager, calBddArray, numBdds, CalOpOr);
515    Cal_MemFree(calBddArray);
516  }
517  return CalBddGetExternalBdd(bddManager, result);
518}
519 
520/**Function********************************************************************
521
522  Synopsis    [Returns the BDD for logical XOR of argument BDDs]
523
524  Description [Returns the BDD for logical XOR of set of BDDs in the bddArray]
525
526  SideEffects [None]
527
528******************************************************************************/
529Cal_Bdd
530Cal_BddMultiwayXor(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
531{
532  int i, numBdds = 0;
533  Cal_Bdd_t result;
534  Cal_Bdd_t *calBddArray;
535  Cal_Bdd userBdd;
536
537  for (numBdds = 0; (userBdd = userBddArray[numBdds]); numBdds++){
538    if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
539      return (Cal_Bdd) 0;
540    }
541  }
542 
543  if (numBdds == 0){
544    CalBddWarningMessage("Multiway OR called with 0 length array");
545    return (Cal_Bdd) 0;
546  }
547  else if (numBdds == 1){
548    return Cal_BddIdentity(bddManager, userBddArray[0]);
549  }
550  else{
551    calBddArray = Cal_MemAlloc(Cal_Bdd_t, numBdds+1);
552    for (i = 0; i < numBdds; i++){
553      calBddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
554    }
555    result = BddMultiwayOp(bddManager, calBddArray, numBdds, CalOpXor);
556    Cal_MemFree(calBddArray);
557  }
558  return CalBddGetExternalBdd(bddManager, result);
559}
560
561
562/*---------------------------------------------------------------------------*/
563/* Definition of internal functions                                          */
564/*---------------------------------------------------------------------------*/
565
566
567/**Function********************************************************************
568
569  Synopsis    [Computes result BDDs for an array of lists, each entry of which
570  is pair of pointers, each of which points to a operand BDD or an entry in
571  another list with a smaller array index]
572
573  Description [Computes result BDDs for an array of lists, each entry of which
574  is pair of pointers, each of which points to a operand BDD or an entry in
575  another list with a smaller array index]
576
577  SideEffects [ThenBDD pointer of an entry is over written by the result BDD
578  and ElseBDD pointer is marked using FORWARD_FLAG]
579
580******************************************************************************/
581void
582CalRequestNodeListArrayOp(Cal_BddManager_t * bddManager,
583                          CalRequestNode_t ** requestNodeListArray,
584                          CalOpProc_t calOpProc)
585{
586  CalRequestNode_t *requestNode;
587  CalRequest_t F, G, result;
588  int pipeDepth, bddId, bddIndex;
589  CalHashTable_t **reqQueAtPipeDepth, *hashTable, *uniqueTableForId;
590  CalHashTable_t ***reqQue = bddManager->reqQue;
591 
592  /* ReqQueInsertUsingReqListArray */
593  for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
594    reqQueAtPipeDepth = reqQue[pipeDepth];
595    for(requestNode = requestNodeListArray[pipeDepth];
596        requestNode != Cal_Nil(CalRequestNode_t);
597        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
598      CalRequestNodeGetF(requestNode, F);
599      CalRequestIsForwardedTo(F);
600      CalRequestNodeGetG(requestNode, G);
601      CalRequestIsForwardedTo(G);
602      if((*calOpProc)(bddManager, F, G, &result) == 0){
603        CalBddNormalize(F, G);
604        CalBddGetMinId2(bddManager, F, G, bddId);
605        CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], F, G, &result);
606      }
607      CalRequestNodePutThenRequest(requestNode, result);
608      CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
609    }
610  }
611
612  /* ReqQueApply */
613  for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
614    bddId = bddManager->indexToId[bddIndex];
615    for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
616      reqQueAtPipeDepth = reqQue[pipeDepth];
617      hashTable = reqQueAtPipeDepth[bddId];
618      if(hashTable->numEntries){
619        CalHashTableApply(bddManager, hashTable, reqQueAtPipeDepth, calOpProc);
620      }
621    }
622  }
623
624#ifdef COMPUTE_MEMORY_OVERHEAD
625  {
626    calNumEntriesAfterApply = 0;
627    for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
628      bddId = bddManager->indexToId[bddIndex];
629      for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
630        reqQueAtPipeDepth = reqQue[pipeDepth];
631        hashTable = reqQueAtPipeDepth[bddId];
632        calNumEntriesAfterApply += hashTable->numEntries;
633      }
634    }
635  }
636#endif
637
638  /* ReqQueReduce */
639  for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
640    bddId = bddManager->indexToId[bddIndex];
641    uniqueTableForId = bddManager->uniqueTable[bddId];
642    for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
643      hashTable = reqQue[pipeDepth][bddId];
644      if(hashTable->numEntries){
645        CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
646      }
647    }
648  }
649
650#ifdef COMPUTE_MEMORY_OVERHEAD
651  {
652    CalRequestNode_t *requestNode;
653    calNumEntriesAfterReduce = 0;
654    for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
655      CalRequestNode_t *next;
656      Cal_BddId_t bddId;
657      bddId = bddManager->indexToId[bddIndex];
658      for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
659        hashTable = reqQue[pipeDepth][bddId];
660        for (requestNode = hashTable->requestNodeList;
661             requestNode != Cal_Nil(CalRequestNode_t); requestNode = next){
662          next = CalRequestNodeGetNextRequestNode(requestNode);
663          calNumEntriesAfterReduce++;
664        }
665      }
666    }
667    calAfterReduceToAfterApplyNodesRatio =
668        ((double)calNumEntriesAfterReduce)/((double)calNumEntriesAfterApply); 
669    calAfterReduceToUniqueTableNodesRatio = 
670        ((double)calNumEntriesAfterReduce)/((double)bddManager->numNodes);
671  }
672#endif
673
674  /* ReqListArrayReqForward */
675  for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
676    for(requestNode = requestNodeListArray[pipeDepth];
677        requestNode != Cal_Nil(CalRequestNode_t);
678        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
679      CalRequestNodeGetThenRequest(requestNode, result);
680      CalRequestIsForwardedTo(result);
681      Cal_Assert(CalBddIsForwarded(result) == 0);
682      CalRequestNodePutThenRequest(requestNode, result);
683    }
684  }
685
686  /* ReqQueCleanUp */
687  for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
688    reqQueAtPipeDepth = reqQue[pipeDepth];
689    for(bddId = 1; bddId <= bddManager->numVars; bddId++){
690      CalHashTableCleanUp(reqQueAtPipeDepth[bddId]);
691    }
692  }
693}
694
695/**Function********************************************************************
696
697  Synopsis    [Internal routine to compute a logical operation on a pair of BDDs]
698
699  Description [Internal routine to compute a logical operation on a pair of BDDs]
700
701  SideEffects [None]
702
703******************************************************************************/
704Cal_Bdd_t
705CalBddOpBF(
706  Cal_BddManager_t * bddManager,
707  CalOpProc_t calOpProc,
708  Cal_Bdd_t  F,
709  Cal_Bdd_t  G)
710{
711  Cal_Bdd_t result;
712  Cal_BddId_t minId, bddId;
713  /*Cal_BddIndex_t minIndex; Commented out because of the problem on alpha*/ 
714  int minIndex;
715  int bddIndex;
716  CalHashTable_t *hashTable, **hashTableArray, *uniqueTableForId;
717 
718  if (calOpProc(bddManager, F, G, &result)){
719    return result;
720  }
721  CalBddGetMinIdAndMinIndex(bddManager, F, G, minId, minIndex);
722  hashTableArray = bddManager->reqQue[0];
723  CalHashTableFindOrAdd(hashTableArray[minId], F, G, &result);
724 
725  /* ReqQueApply */
726  for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
727    bddId = bddManager->indexToId[bddIndex];
728    hashTable = hashTableArray[bddId];
729    if(hashTable->numEntries){
730      CalHashTableApply(bddManager, hashTable, hashTableArray, calOpProc);
731    }
732  }
733#ifdef COMPUTE_MEMORY_OVERHEAD
734  {
735    calNumEntriesAfterApply = 0;
736    for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
737      bddId = bddManager->indexToId[bddIndex];
738      hashTable = hashTableArray[bddId];
739      calNumEntriesAfterApply += hashTable->numEntries;
740    }
741  }
742#endif
743  /* ReqQueReduce */
744  for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
745    bddId = bddManager->indexToId[bddIndex];
746    uniqueTableForId = bddManager->uniqueTable[bddId];
747    hashTable = hashTableArray[bddId];
748    if(hashTable->numEntries){
749      CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
750    }
751  }
752  CalRequestIsForwardedTo(result);
753
754#ifdef COMPUTE_MEMORY_OVERHEAD
755  {
756    CalRequestNode_t *requestNode;
757    calNumEntriesAfterReduce = 0;
758    for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
759      CalRequestNode_t *next;
760      Cal_BddId_t bddId;
761     
762      bddId = bddManager->indexToId[bddIndex];
763      hashTable = hashTableArray[bddId];
764      for (requestNode = hashTable->requestNodeList; requestNode !=
765                                                         Cal_Nil(CalRequestNode_t);
766                                                     requestNode = next){
767        next = CalRequestNodeGetNextRequestNode(requestNode);
768        calNumEntriesAfterReduce++;
769      }
770    }
771    calAfterReduceToAfterApplyNodesRatio =
772        ((double)calNumEntriesAfterReduce)/((double)calNumEntriesAfterApply); 
773    calAfterReduceToUniqueTableNodesRatio = 
774        ((double)calNumEntriesAfterReduce)/((double)bddManager->numNodes);
775  }
776#endif
777
778  /* Clean up */
779  for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
780    bddId = bddManager->indexToId[bddIndex];
781    CalHashTableCleanUp(hashTableArray[bddId]);
782  }
783  return result;
784}
785
786
787
788/*---------------------------------------------------------------------------*/
789/* Definition of static functions                                            */
790/*---------------------------------------------------------------------------*/
791/**Function********************************************************************
792
793  Synopsis    [Internal common routine for Cal_BddPairwiseAnd and Cal_BddPairwiseOr]
794
795  SideEffects [None]
796
797******************************************************************************/
798static Cal_Bdd_t *
799BddArrayOpBF(Cal_BddManager_t * bddManager, Cal_Bdd_t*  bddArray,
800                int numFunction, CalOpProc_t calOpProc)
801{
802  Cal_BddId_t minId, bddId;
803  /*Cal_BddIndex_t minIndex = 0;*/
804  int minIndex = 0;
805  int bddIndex;
806  CalHashTable_t *hashTable, **hashTableArray, *uniqueTableForId;
807  Cal_Bdd_t F, G, result;
808  int numPairs = numFunction/2;
809  Cal_Bdd_t *resultArray = Cal_MemAlloc(Cal_Bdd_t, numPairs);
810  int i;
811 
812  hashTableArray = bddManager->reqQue[0];
813  for (i=0; i<numPairs; i++){
814    F = bddArray[i<<1];
815    G = bddArray[(i<<1)+1];
816    if ((*calOpProc)(bddManager, F, G, &result) == 0){
817      CalBddGetMinIdAndMinIndex(bddManager, F, G, minId, minIndex);
818      CalHashTableFindOrAdd(hashTableArray[minId], F, G, &result);
819    }
820    resultArray[i] = result;
821  }
822 
823 
824  /* ReqQueApply */
825  for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
826    bddId = bddManager->indexToId[bddIndex];
827    hashTable = hashTableArray[bddId];
828    if(hashTable->numEntries){
829      CalHashTableApply(bddManager, hashTable, hashTableArray, calOpProc);
830    }
831  }
832
833  /* ReqQueReduce */
834  for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
835    bddId = bddManager->indexToId[bddIndex];
836    uniqueTableForId = bddManager->uniqueTable[bddId];
837    hashTable = hashTableArray[bddId];
838    if(hashTable->numEntries){
839      CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
840    }
841  }
842  for (i=0; i<numPairs; i++){
843    CalRequestIsForwardedTo(resultArray[i]);
844  }
845  /* Clean up */
846  for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
847    bddId = bddManager->indexToId[bddIndex];
848    CalHashTableCleanUp(hashTableArray[bddId]);
849  }
850  return resultArray;
851}
852
853/**Function********************************************************************
854
855  Synopsis    [Internal routine for multiway operations]
856
857  Description [Internal routine for multiway operations]
858
859  SideEffects [None]
860
861******************************************************************************/
862static Cal_Bdd_t
863BddMultiwayOp(Cal_BddManager_t * bddManager, Cal_Bdd_t * calBddArray,
864              int  numBdds, CalOpProc_t op)
865{
866  int pipeDepth;
867  CalRequestNode_t *requestNode;
868  Cal_Bdd_t result;
869 
870  BddArrayToRequestNodeListArray(bddManager, calBddArray, numBdds);
871  CalRequestNodeListArrayOp(bddManager, bddManager->requestNodeListArray, op);
872  for(pipeDepth = 0; pipeDepth < bddManager->depth-1; pipeDepth++){
873    CalRequestNode_t *next;
874    for(requestNode = bddManager->requestNodeListArray[pipeDepth];
875        requestNode != Cal_Nil(CalRequestNode_t); requestNode = next){
876      next = CalRequestNodeGetNextRequestNode(requestNode);
877      CalNodeManagerFreeNode(bddManager->nodeManagerArray[0],
878                             requestNode);
879    }
880    bddManager->requestNodeListArray[pipeDepth] =
881        Cal_Nil(CalRequestNode_t);
882  }
883  requestNode = bddManager->requestNodeListArray[bddManager->depth-1];
884  bddManager->requestNodeListArray[bddManager->depth-1] =
885      Cal_Nil(CalRequestNode_t); 
886  CalRequestNodeGetThenRequest(requestNode, result); 
887  CalNodeManagerFreeNode(bddManager->nodeManagerArray[0],
888                         requestNode);
889  return result;
890}
891
892
893/**Function********************************************************************
894
895  Synopsis    [Converts an array of BDDs to a list of requests representing BDD
896  pairs]
897
898  Description [Converts an array of BDDs to a list of requests representing BDD]
899
900  SideEffects [None]
901
902******************************************************************************/
903static void
904BddArrayToRequestNodeListArray(
905  Cal_BddManager_t * bddManager,
906  Cal_Bdd_t * calBddArray,
907  int  numBdds)
908{
909  int i;
910  Cal_Bdd_t lastBdd;
911  CalRequestNode_t *even, *odd, *requestNode, *requestNodeList, *head;
912 
913  bddManager->depth = CeilLog2(numBdds);
914  if (bddManager->depth > 10){
915    CalBddFatalMessage("Don't be stooopid\n, Use lesser depth\n");
916  }
917   
918  if (bddManager->depth > bddManager->maxDepth){
919    /* Need to reallocate the memory for reqQue and
920       requestNodeListArray */
921    int oldMaxDepth = bddManager->maxDepth;
922    bddManager->maxDepth = bddManager->depth;
923   
924    for (i=0; i<bddManager->maxDepth; i++){
925      bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t);
926    }
927
928    bddManager->reqQue = Cal_MemRealloc(CalHashTable_t **, bddManager->reqQue,
929                                 bddManager->maxDepth);
930    for (i=oldMaxDepth; i<bddManager->maxDepth; i++){
931      int j;
932      bddManager->reqQue[i] = Cal_MemAlloc(CalHashTable_t *, bddManager->maxNumVars+1);
933      for (j=0; j<bddManager->numVars+1; j++){
934        bddManager->reqQue[i][j] = CalHashTableInit(bddManager, j);
935      }
936    }
937  }
938  lastBdd = bddManager->bddNull;
939  if (numBdds%2 != 0){/* Odd number of Bdd's */
940    lastBdd = calBddArray[numBdds-1];
941  }
942  requestNodeList = bddManager->requestNodeListArray[0];
943  for (i=0; i<numBdds/2; i++){
944    CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
945    CalRequestNodePutF(requestNode, calBddArray[2*i]);
946    CalRequestNodePutG(requestNode, calBddArray[2*i+1]);
947    CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
948    requestNodeList = requestNode;
949  }
950  bddManager->requestNodeListArray[0] = requestNodeList;
951
952  for (i=1; i<bddManager->depth; i++){
953    requestNodeList = bddManager->requestNodeListArray[i];
954    head = bddManager->requestNodeListArray[i-1];
955    while ((odd = head) && (even = head->nextBddNode)){
956      CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
957      /*
958       * We don't have to worry about the Id's attached with
959       * the requestNode or with the then and else part of it.
960       */
961      CalRequestNodePutThenRequestNode(requestNode, odd);
962      CalRequestNodePutElseRequestNode(requestNode, even);
963      CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
964      requestNodeList = requestNode;
965      head = CalRequestNodeGetNextRequestNode(even);
966    }
967    if (odd != Cal_Nil(CalRequestNode_t)){/* There is an  odd node at this
968                                      level */
969      if (CalBddIsBddNull(bddManager,lastBdd)){ /* There are no odd nodes
970                                                 * from previous levels, so
971                                                 * make this an odd node.
972                                                 */
973        CalBddPutBddNode(lastBdd, odd);
974      }
975      else{ /* There exists an odd node, so make a pair now. */
976        CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
977        CalRequestNodePutThenRequestNode(requestNode, odd);
978        CalRequestNodePutElseRequest(requestNode, lastBdd);
979        CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
980        lastBdd = bddManager->bddNull;
981        requestNodeList = requestNode;
982      }
983    }
984    bddManager->requestNodeListArray[i] = requestNodeList;
985  }
986}
987
988
989
990/**Function********************************************************************
991
992  Synopsis    [Returns the smallest integer greater than or equal to log2 of a
993  number]
994
995  Description [Returns the smallest integer greater than or equal to log2 of a
996  number (The assumption is that the number is >= 1)]
997
998  SideEffects [None]
999
1000******************************************************************************/
1001static int
1002CeilLog2(
1003  int  number)
1004{
1005  int num, count;
1006  for (num=number, count=0; num > 1; num >>= 1, count++);
1007  if ((1 << count) != number) count++;
1008  return count;
1009}
1010
1011
1012 
1013
1014
1015
Note: See TracBrowser for help on using the repository browser.