source: vis_dev/vis-2.3/src/res/resSmartVarUse.c @ 23

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

vis2.3
File size: 19.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [resSmartVarUse.c]
4
5  PackageName [res]
6
7  Synopsis [This file provides functions to handle Dd variables in the
8  composition phase of the residue verification.]
9
10  Description [When composing a residue bdd from outputs to inputs, in
11  principle, every node used on that composition should have a unique
12  variable Id. However, the number of nodes may be too big for the
13  manager to handle. The functions in this file keep track of the
14  variables in use during residue verification. In certain sense,
15  these functions are the interface of some kind of manager, handling
16  the requirements of variables. That is why there are some static
17  variables defined in this file.]
18
19  Author      [Kavita Ravi    <ravi@boulder.colorado.edu> and
20               Abelardo Pardo <abel@boulder.colorado.edu>]
21
22  Copyright [This file was created at the University of Colorado at Boulder.
23  The University of Colorado at Boulder makes no warranty about the suitability
24  of this software for any purpose.  It is presented on an AS IS basis.]
25
26******************************************************************************/
27
28#include "resInt.h"
29#include "var_set.h"
30
31static char rcsid[] UNUSED = "$Id: resSmartVarUse.c,v 1.15 2002/09/08 23:56:11 fabio Exp $";
32
33/*---------------------------------------------------------------------------*/
34/* Constant declarations                                                     */
35/*---------------------------------------------------------------------------*/
36
37#define DEFAULT_NUMBER_OF_VARIABLES (sizeof(int)*16)
38#define ELEMENTS_PER_WORD (sizeof(int)<<3)
39
40/*---------------------------------------------------------------------------*/
41/* Type declarations                                                         */
42/*---------------------------------------------------------------------------*/
43
44
45/*---------------------------------------------------------------------------*/
46/* Structure declarations                                                    */
47/*---------------------------------------------------------------------------*/
48
49
50/*---------------------------------------------------------------------------*/
51/* Variable declarations                                                     */
52/*---------------------------------------------------------------------------*/
53
54static var_set_t *idSet = NIL(var_set_t);
55static int numVarsInUse = 0;
56
57/*--------------------------------------------------------------------*/
58/* Macro declarations                                                        */
59/*---------------------------------------------------------------------------*/
60/* based on the fact that var set word size = ELEMENTS_PER_WORD */
61#define MaxSizeOfSet(set) ((set)->n_words * ELEMENTS_PER_WORD)
62
63/**AutomaticStart*************************************************************/
64
65/*---------------------------------------------------------------------------*/
66/* Static function prototypes                                                */
67/*---------------------------------------------------------------------------*/
68
69static var_set_t * InitializeVariableManager(int numOfVars);
70static void ResizeVariableManager(int newSize);
71
72/**AutomaticEnd***************************************************************/
73
74
75/*---------------------------------------------------------------------------*/
76/* Definition of exported functions                                          */
77/*---------------------------------------------------------------------------*/
78
79/*---------------------------------------------------------------------------*/
80/* Definition of internal functions                                          */
81/*---------------------------------------------------------------------------*/
82
83/**Function********************************************************************
84
85  Synopsis [This procedure calls the mdd_create_variables in order to create
86  mvar_list field of the hook.]
87 
88  Description [ This procedure calls the mdd_create_variables in order to
89  create mvar_list field of the hook. IMPORTANT: The mdd_create_variables
90  procedure creates the variables in succession. So if new variables are
91  required that are not in succession, those will not be created and hence
92  cannot be used. This procedure takes as arguments the DD manager and the
93  number of variables that need to be added to the manager.]
94
95  SideEffects   [It modifies the manager->hook->mdd field.]
96
97  SeeAlso            [Res_NetworkResidueVerify]
98
99******************************************************************************/
100void
101MddCreateVariables(mdd_manager *mgr,     
102                   int numVarsToBeAdded) 
103{
104    array_t *mvar_values;
105    array_t *mvar_names = NIL(array_t);
106    array_t *mvar_strides = NIL(array_t);
107    int i, two_values;
108
109    if (numVarsToBeAdded <= 0) return;
110   
111    /* Create 2 mvar values 0,1 */
112    mvar_values = array_alloc(int, numVarsToBeAdded);   
113
114    /* Assume we create only Bdd variables here */
115    two_values = 2;
116    for(i = 0; i < numVarsToBeAdded; i++) {
117      array_insert(int, mvar_values, i, two_values);
118    }
119
120    /* creates the mdd variables and updates the mvar_list field */
121    mdd_create_variables(mgr, mvar_values, mvar_names, mvar_strides);
122   
123    array_free(mvar_values);
124
125} /* End of MddCreateVariables */
126
127/**Function********************************************************************
128
129  Synopsis [Manages the id assignment to the nodes in a smart way.]
130 
131  Description [Manages the id assignment to the nodes in a smart way.  This
132  procedure is responsible for keeping track of which ids are in use during the
133  composition process. It is also responsible for allocating new Ids to nodes
134  with unassigned ids. The procedure reuses ids not in use to fill the new
135  requirements. it is also responsible for creating new variables in the
136  bdd_manager if required. The procedure returns a list of new Ids that can be
137  used to assign to the nodes. It also returns the inverse permutation array
138  that is used by the manager to shuffle the ids.  Assume that for each
139  composition idSet starts with empty set. The procedure accepts the following
140  parameters: the DD manager, an ordered list of nodes and their fanins and an
141  array to fill in the new Ids to be assigned to the unassigned nodes.]
142
143  SideEffects        []
144
145  SeeAlso            [ResResidueVarDeallocate]
146
147******************************************************************************/
148int *
149ResResidueVarAllocate(bdd_manager *ddManager, 
150                         lsList orderList,   
151                         array_t *newIdArray)
152{
153  lsGen listGen;             /* generator to step through a list of nodes */
154  Ntk_Node_t *nodePtr;       /* variable to store node pointer */
155  int nodeId;                /* mdd id of a node */
156  char *flagValue;           /* string to store flag value */
157  int newVarsRequired;       /* number of new variables required by layer */
158  int verbose;               /* verbosity value */
159  var_set_t *assignedSet;    /* var_set of assigned  Ids in this layer */
160  var_set_t *idsNotInList;   /* set of assigned Ids not in layer or fanin */
161  var_set_t *notAssignedSet; /* var_set of Ids not in this layer */
162  int *invPermArray;         /* inverse permutation array for shuffle */
163  int invPermIndex, newIdIndex;  /* iterators */
164  int i, j, id;              /* iterators */
165  int holes;                  /* number of holes filled so far */
166  int lastDdId;              /* last variable in dd manager before expansion */
167  int numberOfFreeVars;      /* number of free variables */
168
169  /* read verbosity flag */
170  verbose = 0;
171  flagValue = Cmd_FlagReadByName("residue_verbosity");
172  if (flagValue != NIL(char)) {
173    verbose = atoi(flagValue);
174  }
175  /* no work required */
176  if (!lsLength(orderList)) {
177    error_append("Something wrong order list is empty \n");
178    return NIL(int);
179  }
180
181  /* if manager not yet initialized, initialize here */
182  if (idSet == NIL(var_set_t)) {
183    ResResidueInitializeVariableManager(lsLength(orderList));
184  }
185
186  /* number of nodes with unassigned Ids */
187  newVarsRequired = 0;
188
189  /* for output nodes list, ids are assigned, just set them in the
190   * var set
191   */
192  if (var_set_is_empty(idSet)) {
193    invPermArray = ALLOC(int, bdd_num_vars(ddManager));
194    for (i = 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
195      invPermArray[i] = bdd_get_id_from_level(ddManager, i);
196    } 
197    invPermIndex = 0;
198    lsForEachItem(orderList, listGen, nodePtr) {
199      nodeId = Ntk_NodeReadMddId(nodePtr);
200      assert(nodeId != NTK_UNASSIGNED_MDD_ID);
201      /* mark output node mdd id as in use */
202      var_set_set_elt(idSet, nodeId);
203      /* increase number of variables in use */
204      numVarsInUse++;
205      invPermArray[invPermIndex] = nodeId;
206      invPermArray[nodeId] = invPermIndex;
207      invPermIndex++;
208    }
209    return(invPermArray);
210  }
211
212  /* create a set for already assigned Ids */
213  assignedSet = var_set_new(MaxSizeOfSet(idSet));
214
215  /* for each item in the list, check against the set if Id
216   * is assigned. Also create a set to isolate assigned Ids
217   * that are not in the list. If unassigned Id, increment
218   * new variables
219   */
220  lsForEachItem(orderList, listGen, nodePtr) {
221    nodeId = Ntk_NodeReadMddId(nodePtr);
222    if (nodeId != NTK_UNASSIGNED_MDD_ID) {
223      assert(var_set_get_elt(idSet, nodeId) == 1);
224      /* create a var set with assigned ids in list */
225      var_set_set_elt(assignedSet, nodeId);
226    } else {
227      newVarsRequired++;
228    }
229  }
230 
231  /* find out from the set, the assigned Ids which are not in
232   * this list
233   */
234  idsNotInList = var_set_new(MaxSizeOfSet(idSet));
235 
236  /* do the operation idSet - assignedSet */
237  notAssignedSet = var_set_new(MaxSizeOfSet(idSet));
238  notAssignedSet = var_set_not(notAssignedSet, assignedSet);
239  idsNotInList = var_set_and(idsNotInList, notAssignedSet, idSet);
240  var_set_free(assignedSet);
241  var_set_free(notAssignedSet);
242 
243 
244  /* initialize return value */
245  if (newVarsRequired) {
246   
247    if (verbose >= 3) {
248      fprintf(vis_stdout, "Number of new variables to be assigned = %d\n",
249              newVarsRequired);
250    }
251    /* compute number of free variables available in the manager */
252    numberOfFreeVars = MaxSizeOfSet(idSet) - numVarsInUse;
253
254    /* if too few free variables available, resize manager */
255    if (numberOfFreeVars < newVarsRequired) {
256      ResizeVariableManager(numVarsInUse + newVarsRequired);
257    }
258
259    invPermArray = ALLOC(int, bdd_num_vars(ddManager));
260    /* fill the inverse permutation array */
261    for (i = 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
262      invPermArray[i] = bdd_get_id_from_level(ddManager, i);
263    }
264    /* create the array of new ids ; assign them starting from the
265     * top(in position) available ID
266     */
267    /* number of available ids in the variable manager */
268    holes = 0;
269    /* There could be two cases here: the number of new vars required
270     * are filled by holes or new variables are required in the DD
271     * manager to fill the requirement
272     */
273   
274    /* assign as many new Ids as required by the list */
275    for (i = 0; ((unsigned) i < bdd_num_vars(ddManager)) && (holes < newVarsRequired); i++) {
276      /* done when holes fill the new variable requirements or when
277       * new variables are needed in the ddManager
278       */
279      if (!var_set_get_elt(idSet, invPermArray[i])) {
280        /* the number of holes filled above are the variables that exist in
281         * the ddManager and are not in use
282         */
283        array_insert_last(int , newIdArray, invPermArray[i]);
284        holes++;
285      }
286    }
287    FREE(invPermArray);
288    if (verbose >= 4) {
289      if (holes) {
290        fprintf(vis_stdout, "Holes filled are ids:");
291        arrayForEachItem(int, newIdArray, i, nodeId) {
292          fprintf(vis_stdout, "%d ", nodeId);
293        }
294        fprintf(vis_stdout, "\n");
295      }
296    }
297
298   
299    /* newVarsRequired-holes is the number of variables to be added to the
300     * mdd manager
301     */
302    if (holes < newVarsRequired) {
303      lastDdId = bdd_num_vars(ddManager);
304      /* create mdd variables, dirty stuff needed to add to the mvar_list */
305      MddCreateVariables((mdd_manager *)ddManager, newVarsRequired - holes);
306     
307      /* since all the variables were created in the end, use the ids
308       * starting at the size of the manager
309       */
310      for(i = 0; i < (newVarsRequired-holes); i++) {
311        array_insert_last(int, newIdArray, lastDdId+i);
312      }
313      if (verbose >= 4) {
314        fprintf(vis_stdout, "New dd ids assigned are: ");
315        for(i = 0; i < (newVarsRequired-holes); i++) {
316          fprintf(vis_stdout, "%d ", array_fetch(int, newIdArray, holes+i));
317        } 
318        fprintf(vis_stdout, "\n");
319      }
320    } /* end of new vars needed to be assigned in the manager */
321  } /* end of new vars need to be assigned to nodes */
322
323  /* Create Inverse Permutation Array for the DD Manager */
324 
325  /* create inverse permutation array with nodes in list */ 
326  invPermArray = ALLOC(int, bdd_num_vars(ddManager));
327  invPermIndex = 0;
328  newIdIndex = 0;
329  if (verbose >= 4) {
330    fprintf(vis_stdout, "Final order to shuffle heap is:\n");
331  }
332  lsForEachItem(orderList, listGen, nodePtr) {
333    /* for nodes with assigned ids, get id from node */
334    nodeId = Ntk_NodeReadMddId(nodePtr);
335    if (nodeId == NTK_UNASSIGNED_MDD_ID) {
336      /* for nodes with unassigned ids, get id from array */
337      nodeId = array_fetch(int, newIdArray, newIdIndex);
338      /* update var set with teh new ids added */
339      var_set_set_elt(idSet, nodeId);
340      numVarsInUse++;
341      newIdIndex++;
342    }
343    invPermArray[invPermIndex] = nodeId;
344    if (verbose >= 4) {
345      fprintf(vis_stdout, "%d ", nodeId);
346    }
347    invPermIndex++;
348  }
349  /* all new ids been accounted for */
350  assert(newIdIndex == array_n(newIdArray));
351
352  /* push nodes  not in list with assigned Ids below those in list */
353  /* fill inv Perm array with Ids that are not in the list
354   * and not in the idsNotInList. These are ids in the
355   * ddManager that are not in idSet.
356   */
357  /* if the number of ids in use in residue verification is less
358   * than that in the manager
359   */
360  if (((unsigned) invPermIndex < bdd_num_vars(ddManager)) ||
361      (!var_set_is_empty(idsNotInList))) {
362
363    /* collect the ids that are not in use in residue verification */
364    for (j = 0; (unsigned) j < bdd_num_vars(ddManager); j++) {
365      /* if not idSet, it means that it is not in use by
366       * residue verification, hence add to the end of invpermArray.
367       * Get id from the invPermArray that was filled in the
368       * above lines(where invPermArray was copied in the manager).
369       * Nodes already in the list will not get added since idSet
370       * was updated as the list was read. The id is read from the
371       * invPermArray so as to not disturb the relative order of
372       * the ids not in use and those in the manager. The check
373       * has the additional clause on the id <
374       * MaxSizeOfSet(idsNotInList)since idsNotInList was created
375       * before the additional variables were added to the manager.
376       */
377      id = bdd_get_id_from_level(ddManager, j);
378      if ((!var_set_get_elt(idSet, id)) ||
379           (((unsigned) id < MaxSizeOfSet(idsNotInList)) &&
380            (var_set_get_elt(idsNotInList, id)))) {
381        /* add to the inverse permutation array */
382        invPermArray[invPermIndex] = id;
383        if (verbose >= 4) {
384          fprintf(vis_stdout, "%d ", id);
385        }
386        invPermIndex++;
387      } /* end of if not in idSet */
388    } /* end of iterating through the ids in the dd manager */
389  } /* end of if */ 
390  if (verbose >= 4) {
391    fprintf(vis_stdout, "\n");
392  }
393
394  var_set_free(idsNotInList);
395  assert(invPermIndex == bdd_num_vars(ddManager));
396 
397  return(invPermArray);
398}/* End of ResResidueVarAllocate */
399
400/**Function********************************************************************
401
402  Synopsis           [Frees the indices of the nodes in the array.]
403
404  Description        [Frees the indices of the nodes in the array. Decrements
405  the static variable numVarsInUse.]
406 
407  SideEffects        [Modifies the manager accordingly.]
408
409  SeeAlso            [ResResidueVarAllocate]
410
411******************************************************************************/
412void
413ResResidueVarDeallocate(array_t *currentLayer)
414{
415  int i=0;
416  int nodeId;
417  Ntk_Node_t *nodePtr;
418 
419  LayerForEachNode(currentLayer, i, nodePtr) {
420    nodeId = Ntk_NodeReadMddId(nodePtr);
421    var_set_clear_elt(idSet, nodeId);
422    numVarsInUse--;
423  }
424
425  return;
426} /* End of Res_ResidueVarUseDeallocate */
427
428/**Function********************************************************************
429
430  Synopsis           [Deallocates the variable manager.]
431
432  Description [ Deallocates the variable manager. Resets the static variable
433  - numVarsInUse.]
434
435  SideEffects        [Modifies the idSet accordingly.]
436
437  SeeAlso            [ResResidueInitializeVariableManager]
438
439
440******************************************************************************/
441void
442ResResidueFreeVariableManager(void)
443{
444
445  if (idSet == NIL(var_set_t)) {
446    return;
447  } /* End of if */
448
449  numVarsInUse = 0;
450  var_set_free(idSet);
451
452  idSet = NIL(var_set_t);
453
454  return;
455} /* End of ResResidueFreeVariableManager */
456
457/**Function********************************************************************
458
459  Synopsis [Initialize the variable manager with some variables.]
460
461  SideEffects        []
462
463  SeeAlso            [ResResidueFreeVariableManager]
464
465******************************************************************************/
466void
467ResResidueInitializeVariableManager(int numOfVars)
468{
469  idSet = InitializeVariableManager(numOfVars);
470  return;
471} /* End of ResResidueInitializeVariableManager */
472
473
474/*---------------------------------------------------------------------------*/
475/* Definition of static functions                                            */
476/*---------------------------------------------------------------------------*/
477
478/**Function********************************************************************
479
480  Synopsis [Initializes the manager with an empty var_set.]
481
482  Description [Initializes the manager with an empty var_set. Default
483  initialization if passed 0 parameter.]
484 
485  SideEffects [Creates a var_set for variables]
486
487  SeeAlso            [Res_ResidueSmartVarUseAllocate]
488
489******************************************************************************/
490static var_set_t *
491InitializeVariableManager(int numOfVars)
492{
493  if (numOfVars != 0) {
494    if (numOfVars % ELEMENTS_PER_WORD != 0) {
495      /* round up to the next word length */
496      numOfVars = ((numOfVars/ELEMENTS_PER_WORD)+1)*ELEMENTS_PER_WORD;
497    } 
498  } else {
499    numOfVars = DEFAULT_NUMBER_OF_VARIABLES;
500  }
501
502  /* default value of number of words = 2 */
503  return var_set_new(numOfVars);
504
505} /* End of InitializeVariableManager */
506
507/**Function********************************************************************
508
509  Synopsis    [Resizes the variable manager.]
510
511  Description [ Resizes the size of the variable manager by calling
512  InitializeVariableManager with a larger size. Copies the old manager values
513  in idSet]
514 
515  SideEffects [Re-allocates memory for the manager]
516
517  SeeAlso [Res_ResidueSmartVarUseAllocate InitializeVariableManager]
518
519******************************************************************************/
520static void
521ResizeVariableManager(int newSize)
522{
523  var_set_t *newSet;
524  int i;
525
526  /* resize only if the new size is larger than the previous size */
527  assert(newSize > MaxSizeOfSet(idSet));
528
529  /* create a new set with the new size */
530  newSet = InitializeVariableManager(newSize);
531 
532  for (i=0; i < idSet->n_words; i++) {
533    newSet->data[i] |= idSet->data[i];
534  }
535  /* free the old id set, not using ResResidueFreeVariableManager()
536   * because it resets the numVarsInUse
537   */
538  var_set_free(idSet);
539
540  idSet = newSet;
541  return;
542} /* End of ResizeVariableManager */
543
544
545
546
547
548
549
550
551
552
553
554
555
Note: See TracBrowser for help on using the repository browser.