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

/**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.]

******************************************************************************/

#include "resInt.h" 
#include "var_set.h"

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

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define DEFAULT_NUMBER_OF_VARIABLES (sizeof(int)*16)
#define ELEMENTS_PER_WORD (sizeof(int)<<3)

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

static var_set_t *idSet = NIL(var_set_t);
static int numVarsInUse = 0;

/*--------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/
/* based on the fact that var set word size = ELEMENTS_PER_WORD */
#define MaxSizeOfSet(set) ((set)->n_words * ELEMENTS_PER_WORD)

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static var_set_t * InitializeVariableManager(int numOfVars);
static void ResizeVariableManager(int newSize);

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

/**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]

******************************************************************************/
void
MddCreateVariables(mdd_manager *mgr,     
                   int numVarsToBeAdded) 
{
    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 */

/**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]

******************************************************************************/
int *
ResResidueVarAllocate(bdd_manager *ddManager,  
                         lsList orderList,   
                         array_t *newIdArray)
{
  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 */

/**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]

******************************************************************************/
void
ResResidueVarDeallocate(array_t *currentLayer)
{
  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 */

/**Function********************************************************************

  Synopsis           [Deallocates the variable manager.]

  Description [ Deallocates the variable manager. Resets the static variable
  - numVarsInUse.]

  SideEffects        [Modifies the idSet accordingly.]

  SeeAlso            [ResResidueInitializeVariableManager]


******************************************************************************/
void
ResResidueFreeVariableManager(void)
{

  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 */

/**Function********************************************************************

  Synopsis [Initialize the variable manager with some variables.]

  SideEffects        []

  SeeAlso            [ResResidueFreeVariableManager]

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


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

/**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]

******************************************************************************/
static var_set_t *
InitializeVariableManager(int numOfVars)
{
  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 */

/**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]

******************************************************************************/
static void
ResizeVariableManager(int newSize)
{
  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 */