VIS

src/res/resSmartVarUse.c File Reference

#include "resInt.h"
#include "var_set.h"
Include dependency graph for resSmartVarUse.c:

Go to the source code of this file.

Defines

#define DEFAULT_NUMBER_OF_VARIABLES   (sizeof(int)*16)
#define ELEMENTS_PER_WORD   (sizeof(int)<<3)
#define MaxSizeOfSet(set)   ((set)->n_words * ELEMENTS_PER_WORD)

Functions

static var_set_t * InitializeVariableManager (int numOfVars)
static void ResizeVariableManager (int newSize)
void MddCreateVariables (mdd_manager *mgr, int numVarsToBeAdded)
int * ResResidueVarAllocate (bdd_manager *ddManager, lsList orderList, array_t *newIdArray)
void ResResidueVarDeallocate (array_t *currentLayer)
void ResResidueFreeVariableManager (void)
void ResResidueInitializeVariableManager (int numOfVars)

Variables

static char rcsid[] UNUSED = "$Id: resSmartVarUse.c,v 1.15 2002/09/08 23:56:11 fabio Exp $"
static var_set_t * idSet = NIL(var_set_t)
static int numVarsInUse = 0

Define Documentation

#define DEFAULT_NUMBER_OF_VARIABLES   (sizeof(int)*16)

Definition at line 37 of file resSmartVarUse.c.

#define ELEMENTS_PER_WORD   (sizeof(int)<<3)

Definition at line 38 of file resSmartVarUse.c.

#define MaxSizeOfSet (   set)    ((set)->n_words * ELEMENTS_PER_WORD)

Definition at line 61 of file resSmartVarUse.c.


Function Documentation

static var_set_t * InitializeVariableManager ( int  numOfVars) [static]

AutomaticStart

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

Synopsis [Initializes the manager with an empty var_set.]

Description [Initializes the manager with an empty var_set. Default initialization if passed 0 parameter.]

SideEffects [Creates a var_set for variables]

SeeAlso [Res_ResidueSmartVarUseAllocate]

Definition at line 491 of file resSmartVarUse.c.

{
  if (numOfVars != 0) {
    if (numOfVars % ELEMENTS_PER_WORD != 0) {
      /* round up to the next word length */
      numOfVars = ((numOfVars/ELEMENTS_PER_WORD)+1)*ELEMENTS_PER_WORD;
    } 
  } else {
    numOfVars = DEFAULT_NUMBER_OF_VARIABLES;
  }

  /* default value of number of words = 2 */
  return var_set_new(numOfVars);

} /* End of InitializeVariableManager */

Here is the caller graph for this function:

void MddCreateVariables ( mdd_manager *  mgr,
int  numVarsToBeAdded 
)

AutomaticEnd Function********************************************************************

Synopsis [This procedure calls the mdd_create_variables in order to create mvar_list field of the hook.]

Description [ This procedure calls the mdd_create_variables in order to create mvar_list field of the hook. IMPORTANT: The mdd_create_variables procedure creates the variables in succession. So if new variables are required that are not in succession, those will not be created and hence cannot be used. This procedure takes as arguments the DD manager and the number of variables that need to be added to the manager.]

SideEffects [It modifies the manager->hook->mdd field.]

SeeAlso [Res_NetworkResidueVerify]

Definition at line 101 of file resSmartVarUse.c.

{
    array_t *mvar_values;
    array_t *mvar_names = NIL(array_t);
    array_t *mvar_strides = NIL(array_t);
    int i, two_values;

    if (numVarsToBeAdded <= 0) return;
    
    /* Create 2 mvar values 0,1 */
    mvar_values = array_alloc(int, numVarsToBeAdded);    

    /* Assume we create only Bdd variables here */
    two_values = 2;
    for(i = 0; i < numVarsToBeAdded; i++) {
      array_insert(int, mvar_values, i, two_values);
    }

    /* creates the mdd variables and updates the mvar_list field */
    mdd_create_variables(mgr, mvar_values, mvar_names, mvar_strides);
    
    array_free(mvar_values);

} /* End of MddCreateVariables */

Here is the caller graph for this function:

static void ResizeVariableManager ( int  newSize) [static]

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

Synopsis [Resizes the variable manager.]

Description [ Resizes the size of the variable manager by calling InitializeVariableManager with a larger size. Copies the old manager values in idSet]

SideEffects [Re-allocates memory for the manager]

SeeAlso [Res_ResidueSmartVarUseAllocate InitializeVariableManager]

Definition at line 521 of file resSmartVarUse.c.

{
  var_set_t *newSet;
  int i;

  /* resize only if the new size is larger than the previous size */
  assert(newSize > MaxSizeOfSet(idSet));

  /* create a new set with the new size */
  newSet = InitializeVariableManager(newSize);
  
  for (i=0; i < idSet->n_words; i++) {
    newSet->data[i] |= idSet->data[i];
  }
  /* free the old id set, not using ResResidueFreeVariableManager()
   * because it resets the numVarsInUse
   */
  var_set_free(idSet);

  idSet = newSet;
  return;
} /* End of ResizeVariableManager */

Here is the call graph for this function:

Here is the caller graph for this function:

void ResResidueFreeVariableManager ( void  )

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

Synopsis [Deallocates the variable manager.]

Description [ Deallocates the variable manager. Resets the static variable

  • numVarsInUse.]

SideEffects [Modifies the idSet accordingly.]

SeeAlso [ResResidueInitializeVariableManager]

Definition at line 442 of file resSmartVarUse.c.

{

  if (idSet == NIL(var_set_t)) {
    return;
  } /* End of if */

  numVarsInUse = 0;
  var_set_free(idSet);

  idSet = NIL(var_set_t);

  return;
} /* End of ResResidueFreeVariableManager */

Here is the caller graph for this function:

void ResResidueInitializeVariableManager ( int  numOfVars)

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

Synopsis [Initialize the variable manager with some variables.]

SideEffects []

SeeAlso [ResResidueFreeVariableManager]

Definition at line 467 of file resSmartVarUse.c.

{
  idSet = InitializeVariableManager(numOfVars);
  return;
} /* End of ResResidueInitializeVariableManager */

Here is the call graph for this function:

Here is the caller graph for this function:

int* ResResidueVarAllocate ( bdd_manager *  ddManager,
lsList  orderList,
array_t *  newIdArray 
)

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

Synopsis [Manages the id assignment to the nodes in a smart way.]

Description [Manages the id assignment to the nodes in a smart way. This procedure is responsible for keeping track of which ids are in use during the composition process. It is also responsible for allocating new Ids to nodes with unassigned ids. The procedure reuses ids not in use to fill the new requirements. it is also responsible for creating new variables in the bdd_manager if required. The procedure returns a list of new Ids that can be used to assign to the nodes. It also returns the inverse permutation array that is used by the manager to shuffle the ids. Assume that for each composition idSet starts with empty set. The procedure accepts the following parameters: the DD manager, an ordered list of nodes and their fanins and an array to fill in the new Ids to be assigned to the unassigned nodes.]

SideEffects []

SeeAlso [ResResidueVarDeallocate]

Definition at line 149 of file resSmartVarUse.c.

{
  lsGen listGen;             /* generator to step through a list of nodes */
  Ntk_Node_t *nodePtr;       /* variable to store node pointer */
  int nodeId;                /* mdd id of a node */
  char *flagValue;           /* string to store flag value */
  int newVarsRequired;       /* number of new variables required by layer */
  int verbose;               /* verbosity value */
  var_set_t *assignedSet;    /* var_set of assigned  Ids in this layer */
  var_set_t *idsNotInList;   /* set of assigned Ids not in layer or fanin */
  var_set_t *notAssignedSet; /* var_set of Ids not in this layer */
  int *invPermArray;         /* inverse permutation array for shuffle */
  int invPermIndex, newIdIndex;  /* iterators */
  int i, j, id;              /* iterators */
  int holes;                  /* number of holes filled so far */
  int lastDdId;              /* last variable in dd manager before expansion */
  int numberOfFreeVars;      /* number of free variables */

  /* read verbosity flag */
  verbose = 0;
  flagValue = Cmd_FlagReadByName("residue_verbosity");
  if (flagValue != NIL(char)) {
    verbose = atoi(flagValue);
  }
  /* no work required */
  if (!lsLength(orderList)) {
    error_append("Something wrong order list is empty \n");
    return NIL(int);
  }

  /* if manager not yet initialized, initialize here */
  if (idSet == NIL(var_set_t)) {
    ResResidueInitializeVariableManager(lsLength(orderList));
  }

  /* number of nodes with unassigned Ids */
  newVarsRequired = 0;

  /* for output nodes list, ids are assigned, just set them in the
   * var set
   */
  if (var_set_is_empty(idSet)) {
    invPermArray = ALLOC(int, bdd_num_vars(ddManager));
    for (i = 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
      invPermArray[i] = bdd_get_id_from_level(ddManager, i);
    }  
    invPermIndex = 0;
    lsForEachItem(orderList, listGen, nodePtr) {
      nodeId = Ntk_NodeReadMddId(nodePtr);
      assert(nodeId != NTK_UNASSIGNED_MDD_ID);
      /* mark output node mdd id as in use */
      var_set_set_elt(idSet, nodeId);
      /* increase number of variables in use */
      numVarsInUse++;
      invPermArray[invPermIndex] = nodeId;
      invPermArray[nodeId] = invPermIndex;
      invPermIndex++;
    }
    return(invPermArray);
  }

  /* create a set for already assigned Ids */
  assignedSet = var_set_new(MaxSizeOfSet(idSet));

  /* for each item in the list, check against the set if Id
   * is assigned. Also create a set to isolate assigned Ids
   * that are not in the list. If unassigned Id, increment
   * new variables
   */
  lsForEachItem(orderList, listGen, nodePtr) {
    nodeId = Ntk_NodeReadMddId(nodePtr);
    if (nodeId != NTK_UNASSIGNED_MDD_ID) {
      assert(var_set_get_elt(idSet, nodeId) == 1);
      /* create a var set with assigned ids in list */
      var_set_set_elt(assignedSet, nodeId);
    } else {
      newVarsRequired++;
    }
  }
  
  /* find out from the set, the assigned Ids which are not in
   * this list
   */
  idsNotInList = var_set_new(MaxSizeOfSet(idSet));
  
  /* do the operation idSet - assignedSet */
  notAssignedSet = var_set_new(MaxSizeOfSet(idSet));
  notAssignedSet = var_set_not(notAssignedSet, assignedSet);
  idsNotInList = var_set_and(idsNotInList, notAssignedSet, idSet);
  var_set_free(assignedSet);
  var_set_free(notAssignedSet);
  
  
  /* initialize return value */
  if (newVarsRequired) {
    
    if (verbose >= 3) {
      fprintf(vis_stdout, "Number of new variables to be assigned = %d\n",
              newVarsRequired);
    }
    /* compute number of free variables available in the manager */
    numberOfFreeVars = MaxSizeOfSet(idSet) - numVarsInUse;

    /* if too few free variables available, resize manager */
    if (numberOfFreeVars < newVarsRequired) {
      ResizeVariableManager(numVarsInUse + newVarsRequired);
    }

    invPermArray = ALLOC(int, bdd_num_vars(ddManager));
    /* fill the inverse permutation array */
    for (i = 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
      invPermArray[i] = bdd_get_id_from_level(ddManager, i);
    }
    /* create the array of new ids ; assign them starting from the
     * top(in position) available ID
     */
    /* number of available ids in the variable manager */
    holes = 0;
    /* There could be two cases here: the number of new vars required
     * are filled by holes or new variables are required in the DD
     * manager to fill the requirement
     */
    
    /* assign as many new Ids as required by the list */
    for (i = 0; ((unsigned) i < bdd_num_vars(ddManager)) && (holes < newVarsRequired); i++) {
      /* done when holes fill the new variable requirements or when
       * new variables are needed in the ddManager
       */
      if (!var_set_get_elt(idSet, invPermArray[i])) {
        /* the number of holes filled above are the variables that exist in
         * the ddManager and are not in use
         */
        array_insert_last(int , newIdArray, invPermArray[i]);
        holes++;
      }
    }
    FREE(invPermArray);
    if (verbose >= 4) {
      if (holes) {
        fprintf(vis_stdout, "Holes filled are ids:");
        arrayForEachItem(int, newIdArray, i, nodeId) {
          fprintf(vis_stdout, "%d ", nodeId);
        }
        fprintf(vis_stdout, "\n");
      }
    }

    
    /* newVarsRequired-holes is the number of variables to be added to the
     * mdd manager
     */
    if (holes < newVarsRequired) {
      lastDdId = bdd_num_vars(ddManager);
      /* create mdd variables, dirty stuff needed to add to the mvar_list */
      MddCreateVariables((mdd_manager *)ddManager, newVarsRequired - holes);
      
      /* since all the variables were created in the end, use the ids
       * starting at the size of the manager
       */
      for(i = 0; i < (newVarsRequired-holes); i++) {
        array_insert_last(int, newIdArray, lastDdId+i);
      }
      if (verbose >= 4) {
        fprintf(vis_stdout, "New dd ids assigned are: ");
        for(i = 0; i < (newVarsRequired-holes); i++) {
          fprintf(vis_stdout, "%d ", array_fetch(int, newIdArray, holes+i));
        } 
        fprintf(vis_stdout, "\n");
      }
    } /* end of new vars needed to be assigned in the manager */
  } /* end of new vars need to be assigned to nodes */

  /* Create Inverse Permutation Array for the DD Manager */
  
  /* create inverse permutation array with nodes in list */ 
  invPermArray = ALLOC(int, bdd_num_vars(ddManager));
  invPermIndex = 0;
  newIdIndex = 0;
  if (verbose >= 4) {
    fprintf(vis_stdout, "Final order to shuffle heap is:\n");
  }
  lsForEachItem(orderList, listGen, nodePtr) {
    /* for nodes with assigned ids, get id from node */
    nodeId = Ntk_NodeReadMddId(nodePtr);
    if (nodeId == NTK_UNASSIGNED_MDD_ID) {
      /* for nodes with unassigned ids, get id from array */
      nodeId = array_fetch(int, newIdArray, newIdIndex);
      /* update var set with teh new ids added */
      var_set_set_elt(idSet, nodeId);
      numVarsInUse++;
      newIdIndex++;
    }
    invPermArray[invPermIndex] = nodeId;
    if (verbose >= 4) {
      fprintf(vis_stdout, "%d ", nodeId);
    }
    invPermIndex++;
  }
  /* all new ids been accounted for */
  assert(newIdIndex == array_n(newIdArray));

  /* push nodes  not in list with assigned Ids below those in list */
  /* fill inv Perm array with Ids that are not in the list
   * and not in the idsNotInList. These are ids in the
   * ddManager that are not in idSet. 
   */
  /* if the number of ids in use in residue verification is less
   * than that in the manager
   */
  if (((unsigned) invPermIndex < bdd_num_vars(ddManager)) ||
      (!var_set_is_empty(idsNotInList))) {

    /* collect the ids that are not in use in residue verification */
    for (j = 0; (unsigned) j < bdd_num_vars(ddManager); j++) {
      /* if not idSet, it means that it is not in use by
       * residue verification, hence add to the end of invpermArray.
       * Get id from the invPermArray that was filled in the
       * above lines(where invPermArray was copied in the manager).
       * Nodes already in the list will not get added since idSet
       * was updated as the list was read. The id is read from the
       * invPermArray so as to not disturb the relative order of
       * the ids not in use and those in the manager. The check
       * has the additional clause on the id <
       * MaxSizeOfSet(idsNotInList)since idsNotInList was created
       * before the additional variables were added to the manager.
       */
      id = bdd_get_id_from_level(ddManager, j);
      if ((!var_set_get_elt(idSet, id)) ||
           (((unsigned) id < MaxSizeOfSet(idsNotInList)) &&
            (var_set_get_elt(idsNotInList, id)))) {
        /* add to the inverse permutation array */
        invPermArray[invPermIndex] = id;
        if (verbose >= 4) {
          fprintf(vis_stdout, "%d ", id);
        }
        invPermIndex++;
      } /* end of if not in idSet */
    } /* end of iterating through the ids in the dd manager */
  } /* end of if */ 
  if (verbose >= 4) {
    fprintf(vis_stdout, "\n");
  }

  var_set_free(idsNotInList);
  assert(invPermIndex == bdd_num_vars(ddManager));
  
  return(invPermArray);
}/* End of ResResidueVarAllocate */

Here is the call graph for this function:

Here is the caller graph for this function:

void ResResidueVarDeallocate ( array_t *  currentLayer)

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

Synopsis [Frees the indices of the nodes in the array.]

Description [Frees the indices of the nodes in the array. Decrements the static variable numVarsInUse.]

SideEffects [Modifies the manager accordingly.]

SeeAlso [ResResidueVarAllocate]

Definition at line 413 of file resSmartVarUse.c.

{
  int i=0;
  int nodeId;
  Ntk_Node_t *nodePtr;
  
  LayerForEachNode(currentLayer, i, nodePtr) {
    nodeId = Ntk_NodeReadMddId(nodePtr);
    var_set_clear_elt(idSet, nodeId);
    numVarsInUse--;
  }

  return;
} /* End of Res_ResidueVarUseDeallocate */

Here is the call graph for this function:

Here is the caller graph for this function:


Variable Documentation

var_set_t* idSet = NIL(var_set_t) [static]

Definition at line 54 of file resSmartVarUse.c.

int numVarsInUse = 0 [static]

Definition at line 55 of file resSmartVarUse.c.

char rcsid [] UNUSED = "$Id: resSmartVarUse.c,v 1.15 2002/09/08 23:56:11 fabio Exp $" [static]

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

FileName [resSmartVarUse.c]

PackageName [res]

Synopsis [This file provides functions to handle Dd variables in the composition phase of the residue verification.]

Description [When composing a residue bdd from outputs to inputs, in principle, every node used on that composition should have a unique variable Id. However, the number of nodes may be too big for the manager to handle. The functions in this file keep track of the variables in use during residue verification. In certain sense, these functions are the interface of some kind of manager, handling the requirements of variables. That is why there are some static variables defined in this file.]

Author [Kavita Ravi <ravi@boulder.colorado.edu> and Abelardo Pardo <abel@boulder.colorado.edu>]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 31 of file resSmartVarUse.c.