source: vis_dev/glu-2.3/src/calBdd/calPipeline.c @ 102

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

library glu 2.3
File size: 16.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calPipeline.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routines for creating and managing the pipelined BDD
8  operations.]
9
10  Description [Eventually we would like to have this feature
11  transparent to the user.]
12
13  SeeAlso     [optional]
14
15  Author      [ Rajeev K. Ranjan   (rajeev@eecs.berkeley.edu)
16                Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)
17              ]
18
19  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
20  All rights reserved.
21
22  Permission is hereby granted, without written agreement and without license
23  or royalty fees, to use, copy, modify, and distribute this software and its
24  documentation for any purpose, provided that the above copyright notice and
25  the following two paragraphs appear in all copies of this software.
26
27  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
28  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
29  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
30  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
31
32  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
33  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
34  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
35  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
36  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
37
38  Revision    [$Id: calPipeline.c,v 1.1.1.3 1998/05/04 00:59:01 hsv Exp $]
39
40******************************************************************************/
41
42#include "calInt.h"
43
44/*---------------------------------------------------------------------------*/
45/* Constant declarations                                                     */
46/*---------------------------------------------------------------------------*/
47
48/*---------------------------------------------------------------------------*/
49/* Type declarations                                                         */
50/*---------------------------------------------------------------------------*/
51
52
53/*---------------------------------------------------------------------------*/
54/* Stucture declarations                                                     */
55/*---------------------------------------------------------------------------*/
56
57/*---------------------------------------------------------------------------*/
58/* Variable declarations                                                     */
59/*---------------------------------------------------------------------------*/
60
61/*---------------------------------------------------------------------------*/
62/* Macro declarations                                                        */
63/*---------------------------------------------------------------------------*/
64
65/**AutomaticStart*************************************************************/
66
67/*---------------------------------------------------------------------------*/
68/* Static function prototypes                                                */
69/*---------------------------------------------------------------------------*/
70
71
72/**AutomaticEnd***************************************************************/
73
74
75/*---------------------------------------------------------------------------*/
76/* Definition of exported functions                                          */
77/*---------------------------------------------------------------------------*/
78/**Function********************************************************************
79
80  Synopsis    [Set depth of a BDD pipeline.]
81
82  Description [The "depth" determines the amount of dependency we
83  would allow in pipelined computation.]
84
85  SideEffects [None.]
86
87  SeeAlso     []
88
89******************************************************************************/
90void
91Cal_PipelineSetDepth(Cal_BddManager bddManager, int depth)
92{
93  int i, j;
94  if(depth > 6){
95    CalBddWarningMessage("PipelineDepth can not exceed 6\n");
96    CalBddWarningMessage("setting PipelineDepth to 6\n");
97    depth = 6;
98  }
99  if(bddManager->maxDepth < depth){
100    int oldMaxDepth = bddManager->maxDepth;
101    bddManager->depth = bddManager->maxDepth = depth;
102    bddManager->reqQue = Cal_MemRealloc(CalHashTable_t **, bddManager->reqQue,
103                                 bddManager->maxDepth);
104    for(i = oldMaxDepth; i < bddManager->maxDepth; i++){
105      bddManager->reqQue[i] = Cal_MemAlloc(CalHashTable_t *, bddManager->maxNumVars+1);
106      for(j = 0; j < bddManager->numVars+1; j++){
107        bddManager->reqQue[i][j] =
108            CalHashTableInit(bddManager, j);
109      }
110    }
111  }
112  else{
113    bddManager->depth = depth;
114  } 
115}
116
117/**Function********************************************************************
118
119  Synopsis    [Initialize a BDD pipeline.]
120
121  Description [All the operations for this pipeline must be of the
122  same kind.]
123
124  SideEffects [None.]
125
126  SeeAlso     []
127
128******************************************************************************/
129int
130Cal_PipelineInit(Cal_BddManager bddManager, Cal_BddOp_t bddOp)
131{
132  CalBddPostProcessing(bddManager);
133  if(bddManager->pipelineState != READY){
134    CalBddWarningMessage("Pipeline cannot be initialized");
135    return 0;
136  }
137  else{
138    bddManager->pipelineState = CREATE;
139    switch(bddOp){
140    case CAL_AND :
141      bddManager->pipelineFn = CalOpAnd;
142      break;
143    case CAL_OR  :
144      bddManager->pipelineFn = CalOpOr;
145      break;
146    case CAL_XOR :
147      bddManager->pipelineFn = CalOpXor;
148      break;
149    default  :
150      CalBddWarningMessage("Unknown Bdd Operation type");
151      return 0;
152    }
153    return 1;
154  } 
155}
156
157/**Function********************************************************************
158
159  Synopsis    [Create a provisional BDD in the pipeline.]
160
161  Description [The provisional BDD is automatically freed once the
162  pipeline is quitted.]
163
164  SideEffects []
165
166  SeeAlso     []
167
168******************************************************************************/
169Cal_Bdd
170Cal_PipelineCreateProvisionalBdd(Cal_BddManager bddManager, Cal_Bdd fUserBdd,
171                                 Cal_Bdd gUserBdd)
172{
173  int insertDepth, operandDepth;
174  CalRequestNode_t *requestNode;
175  Cal_Bdd_t provisionalBdd, f, g;
176  Cal_BddId_t bddId;
177  Cal_Bdd userNode;
178 
179  insertDepth = 0;
180 
181  f = CalBddGetInternalBdd(bddManager, fUserBdd);
182  g = CalBddGetInternalBdd(bddManager, gUserBdd);
183  if(bddManager->pipelineState != CREATE){
184    CalBddWarningMessage("Provisional Bdd not created: Pipeline is not initialized");
185    return (Cal_Bdd) 0;
186  }
187  if(CalBddIsMarked(f)){
188    CalBddGetDepth(f, operandDepth);
189    if(insertDepth <= operandDepth){
190      insertDepth = operandDepth + 1;
191    }
192  }
193  if(CalBddIsMarked(g)){
194    CalBddGetDepth(g, operandDepth);
195    if(insertDepth <= operandDepth){
196      insertDepth = operandDepth + 1;
197    }
198  }
199  if (bddManager->pipelineDepth <= insertDepth){
200    bddManager->pipelineDepth = insertDepth + 1;
201  }
202  if (insertDepth >= MAX_INSERT_DEPTH){
203    CalBddWarningMessage("Provisional Bdd not created");
204    CalBddWarningMessage("Maximum pipeline depth is reached");
205    return (Cal_Bdd) 0;
206  }
207
208  CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
209  CalRequestNodePutF(requestNode, f);
210  CalRequestNodePutG(requestNode, g);
211  CalRequestNodeMark(requestNode);
212  CalRequestNodePutDepth(requestNode, insertDepth);
213  CalRequestNodePutNextRequestNode(requestNode,
214      bddManager->requestNodeListArray[insertDepth]);
215  bddManager->requestNodeListArray[insertDepth] = requestNode;
216
217  CalBddGetMinId2(bddManager, f, g, bddId);
218  CalBddPutBddId(provisionalBdd, bddId);
219  CalBddPutBddNode(provisionalBdd, (CalBddNode_t *)requestNode);
220
221  CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], userNode);
222  CalBddNodePutThenBdd(userNode, provisionalBdd);
223  CalBddNodePutElseBdd(userNode, bddManager->bddOne);
224  CalBddNodePutNextBddNode(userNode,
225                           bddManager->userProvisionalNodeList);
226  bddManager->userProvisionalNodeList = userNode;
227  CalBddNodeIcrRefCount(userNode);
228  return userNode;
229}
230
231/**Function********************************************************************
232
233  Synopsis    [Executes a pipeline.]
234
235  Description [All the results are computed. User should update the
236  BDDs of interest. Eventually this feature would become transparent.]
237
238  SideEffects [required]
239
240  SeeAlso     [optional]
241
242******************************************************************************/
243int
244Cal_PipelineExecute(Cal_BddManager bddManager)
245{
246  CalRequestNode_t **requestNodeListArray, *node, *nextNode;
247  int  i;
248  Cal_Bdd_t thenBdd;
249  int automaticDepthControlFlag = 0;
250  int pipelineDepth;
251 
252  if(bddManager->pipelineState != CREATE){
253    CalBddWarningMessage("Pipeline cannot be executed");
254    return 0;
255  }
256
257  /* Check if we need to control the depth value using some heuristic */
258  if (bddManager->depth == 0) automaticDepthControlFlag = 1;
259 
260  requestNodeListArray = bddManager->requestNodeListArray;
261  pipelineDepth = bddManager->pipelineDepth;
262  while(pipelineDepth){
263    if (automaticDepthControlFlag){
264      if (bddManager->numNodes < 10000) bddManager->depth = 4;
265      else if (bddManager->numNodes < 100000) bddManager->depth = 2;
266      else bddManager->depth = 1;
267    }
268    if(bddManager->depth > pipelineDepth){
269      bddManager->depth = pipelineDepth;
270    }
271    CalRequestNodeListArrayOp(bddManager, requestNodeListArray,
272                              bddManager->pipelineFn);
273    pipelineDepth -= bddManager->depth;
274
275    /* Lock the results, in case garbage collection needs to be
276       invoked */
277    for (i=0; i<bddManager->depth; i++){
278      for (node = requestNodeListArray[i]; node; node = nextNode){
279        nextNode = CalBddNodeGetNextBddNode(node);
280        CalBddNodeGetThenBdd(node, thenBdd);
281        CalBddIcrRefCount(thenBdd);
282      }
283    }
284    /* Save the current pipelineDepth */
285    bddManager->currentPipelineDepth = pipelineDepth;
286    if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
287      /* Abort, may be we should clean up a little bit */
288      fprintf(stderr,"Bdd Overflow: Aborting\n");
289      return 0;
290    }
291    requestNodeListArray += bddManager->depth;
292  }
293  /* Need to decrement the reference counts */
294  for (i=0; i<bddManager->pipelineDepth; i++){
295    for (node=bddManager->requestNodeListArray[i]; node; node = nextNode){
296      nextNode = CalBddNodeGetNextBddNode(node);
297      CalBddNodeGetThenBdd(node, thenBdd);
298      CalBddDcrRefCount(thenBdd);
299    }
300  }
301  bddManager->pipelineState = UPDATE;
302  return 1;
303}
304 
305/**Function********************************************************************
306
307  Synopsis    [Update a provisional Bdd obtained during pipelining.]
308
309  Description [The provisional BDD is automatically freed after
310  quitting pipeline.]
311
312  SideEffects []
313
314  SeeAlso     []
315
316******************************************************************************/
317Cal_Bdd
318Cal_PipelineUpdateProvisionalBdd(Cal_BddManager bddManager,
319                                 Cal_Bdd provisionalBdd) 
320{
321  Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, provisionalBdd);
322  if(bddManager->pipelineState != UPDATE){
323    CalBddWarningMessage("Provisional Bdd cannot be updated");
324    return (Cal_Bdd) 0;
325  }
326  CalBddGetThenBdd(calBdd, calBdd);
327  return CalBddGetExternalBdd(bddManager, calBdd);
328}
329
330/**Function********************************************************************
331
332  Synopsis           [Returns 1, if the given user BDD contains
333  provisional BDD node.]
334
335  Description        [Returns 1, if the given user BDD contains
336  provisional BDD node.]
337
338  SideEffects        [None.]
339
340  SeeAlso            []
341
342******************************************************************************/
343int
344Cal_BddIsProvisional(Cal_BddManager bddManager, Cal_Bdd userBdd)
345{
346  Cal_Bdd_t internalBdd = CalBddGetInternalBdd(bddManager, userBdd);
347  return CalBddIsMarked(internalBdd);
348}
349
350/**Function********************************************************************
351
352  Synopsis    [Resets the pipeline freeing all resources.]
353
354  Description [The user must make sure to update all provisional BDDs
355  of interest before calling this routine.]
356
357  SideEffects []
358
359  SeeAlso     []
360
361******************************************************************************/
362void
363Cal_PipelineQuit(Cal_BddManager bddManager)
364{
365  CalRequestNode_t *requestNode, *next;
366  int i;
367
368  bddManager->pipelineState = READY;
369  for(i = 0; i < bddManager->pipelineDepth; i++){
370    for(requestNode = bddManager->requestNodeListArray[i], 
371        bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t);
372        requestNode != Cal_Nil(CalRequestNode_t);
373        requestNode = next){
374      next = CalRequestNodeGetNextRequestNode(requestNode);
375      CalNodeManagerFreeNode(bddManager->nodeManagerArray[0], requestNode);
376    }
377    bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t);
378  }
379  bddManager->pipelineDepth = 0;
380  for (requestNode = bddManager->userProvisionalNodeList; requestNode;
381       requestNode = next){
382    next = CalRequestNodeGetNextRequestNode(requestNode);
383    CalNodeManagerFreeNode(bddManager->nodeManagerArray[0],
384                           requestNode);
385  }
386  bddManager->userProvisionalNodeList = Cal_Nil(CalRequestNode_t);
387}
388
389/*---------------------------------------------------------------------------*/
390/* Definition of internal functions                                          */
391/*---------------------------------------------------------------------------*/
392/**Function********************************************************************
393
394  Synopsis           [required]
395
396  Description        [optional]
397
398  SideEffects        [required]
399
400  SeeAlso            [optional]
401
402******************************************************************************/
403void
404CalBddReorderFixProvisionalNodes(Cal_BddManager_t *bddManager)
405{
406  CalRequestNode_t **requestNodeListArray =
407      bddManager->requestNodeListArray;
408  CalRequestNode_t *node, *nextNode;
409  int i;
410  Cal_Bdd_t thenBdd, elseBdd;
411 
412  for (i=0;
413       i<bddManager->pipelineDepth-bddManager->currentPipelineDepth;
414       i++){ 
415    for (node = *requestNodeListArray; node; node = nextNode){
416      nextNode = CalBddNodeGetNextBddNode(node);
417      Cal_Assert(CalBddNodeIsForwarded(node));
418      CalBddNodeGetThenBdd(node, thenBdd);
419      if (CalBddIsForwarded(thenBdd)) {
420        CalBddForward(thenBdd);
421      }
422      CalBddNodePutThenBdd(node, thenBdd);
423      Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
424    }
425    requestNodeListArray++;
426  }
427  for (; i<bddManager->pipelineDepth; i++){
428    for (node = *requestNodeListArray; node; node = nextNode){
429      nextNode = CalBddNodeGetNextBddNode(node);
430      Cal_Assert(CalBddNodeIsForwarded(node) == 0);
431      CalBddNodeGetThenBdd(node, thenBdd);
432      if (CalBddIsForwarded(thenBdd)) {
433        CalBddForward(thenBdd);
434      }
435      CalBddNodePutThenBdd(node, thenBdd);
436      Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
437      CalBddNodeGetElseBdd(node, elseBdd);
438      if (CalBddIsForwarded(elseBdd)) {
439        CalBddForward(elseBdd);
440      }
441      CalBddNodePutElseBdd(node, elseBdd);
442      Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
443    }
444    requestNodeListArray++;
445  }
446}
447
448/**Function********************************************************************
449
450  Synopsis           [required]
451
452  Description        [optional]
453
454  SideEffects        [required]
455
456  SeeAlso            [optional]
457
458******************************************************************************/
459void
460CalCheckPipelineValidity(Cal_BddManager_t *bddManager)
461{
462  CalRequestNode_t **requestNodeListArray =
463      bddManager->requestNodeListArray;
464  CalRequestNode_t *node, *nextNode;
465  int i;
466  Cal_Bdd_t thenBdd, elseBdd;
467 
468  for (i=0;
469       i<bddManager->pipelineDepth-bddManager->currentPipelineDepth;
470       i++){ 
471    for (node = *requestNodeListArray; node; node = nextNode){
472      nextNode = CalBddNodeGetNextBddNode(node);
473      Cal_Assert(CalBddNodeIsForwarded(node));
474      CalBddNodeGetThenBdd(node, thenBdd);
475      Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
476    }
477    requestNodeListArray++;
478  }
479  for (; i<bddManager->pipelineDepth; i++){
480    for (node = *requestNodeListArray; node; node = nextNode){
481      nextNode = CalBddNodeGetNextBddNode(node);
482      Cal_Assert(CalBddNodeIsForwarded(node) == 0); 
483      CalBddNodeGetThenBdd(node, thenBdd);
484      /*Cal_Assert(CalBddIsForwarded(thenBdd) == 0);*/
485      /* This is possible since the actual BDD of thenBdd could have been
486         computed and it is forwarded, however this node is not yet
487         updated with the result */
488      CalBddNodeGetElseBdd(node, elseBdd);
489      /*Cal_Assert(CalBddIsForwarded(elseBdd) == 0);*/
490    }
491    requestNodeListArray++;
492  }
493}
494/*---------------------------------------------------------------------------*/
495/* Definition of static functions                                            */
496/*---------------------------------------------------------------------------*/
497
Note: See TracBrowser for help on using the repository browser.