src/res/resCompose.c

Go to the documentation of this file.

#include "resInt.h"

static char rcsid[] UNUSED = "$Id: resCompose.c,v 1.30 2005/04/18 05:00:14 fabio Exp $";

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

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

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

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
long Res_composeTime;
long Res_shuffleTime;
long Res_smartVarTime;
long Res_orderTime;

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

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

static void UpdateUnassignedNodesWithNewIds(lsList orderList, array_t *newIdArray);
static lsList CreateNodeAndFaninOrderList(array_t *currentLayer);
static lsList ListAppend(Ntk_Node_t *nodePtr, lsList newList, lsList faninList);
static int IdCompare(const void *obj1, const void *obj2);
static int IdListCompare(lsGeneric item1, lsGeneric item2);
static lsList CreateFaninVarSetList(array_t *currentLayer, st_table *faninTable);
static bdd_node * ComposeLayer(bdd_manager *ddManager, bdd_node *residueDd, array_t *currentLayer, bdd_node **functionArray);
static Mvf_Function_t * NodeBuildConstantMvf(Ntk_Node_t * node, mdd_manager *mddMgr);

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


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

 
bdd_node *
BuildBDDforNode(Ntk_Network_t *network,
                Ntk_Node_t *nodePtr,
                int fanin)
{
  bdd_node *function;
  st_table *leaves;
  array_t *mvfArray;
  Mvf_Function_t *nodeFunction;
  Ntk_Node_t *faninNodePtr;
  lsGen netGen;
  array_t *root;
  int j;
  mdd_manager *mddMgr;

  /* if it is a constant, build the mvf for it */
  if( Ntk_NodeTestIsConstant(nodePtr) == 1) {
    mddMgr = (mdd_manager *)Ntk_NetworkReadMddManager(network);
    nodeFunction = NodeBuildConstantMvf(nodePtr, mddMgr);
  } else if (Ntk_NodeTestIsCombInput(nodePtr)) {
    /* the Bdd for a latch input is itself */
    mddMgr = (mdd_manager *)Ntk_NetworkReadMddManager(network);
    nodeFunction = Mvf_FunctionCreateFromVariable(mddMgr, Ntk_NodeReadMddId(nodePtr));
  } else {

    /* Set the root to build the Mvf */
    root = array_alloc(Ntk_Node_t *, 1);
    array_insert(Ntk_Node_t *, root, 0, nodePtr);
    
    /* Set the leaves depending on the fanin flag*/
    leaves = st_init_table(st_ptrcmp, st_ptrhash);
    if (fanin == IMMEDIATE_FANIN) {
      Ntk_NodeForEachFanin(nodePtr, j, faninNodePtr) {
        st_insert(leaves, (char *)faninNodePtr, (char *)NTM_UNUSED);
      }
    } else if (fanin == PRIMARY_INPUTS) {
      Ntk_NetworkForEachCombInput(network, netGen, nodePtr) {
        st_insert(leaves, (char *)nodePtr, (char *)NTM_UNUSED);
      }
    }
        
    /* Effectively compute the function (We are not using don't cares)*/
    mvfArray = Ntm_NetworkBuildMvfs(network, root, leaves, NIL(mdd_t));
    st_free_table(leaves);
    array_free(root);
    
    nodeFunction = array_fetch(Mvf_Function_t *, mvfArray, 0);
    /* since we built the MDD for only one root */
    array_free(mvfArray);
  } /* end of else if not a latch output */
  /* 
   * The function above returned a Mvf_Function_t, but since we are 
   * working with binary nodes (so far), we do not need the Mvf 
   * representation, therefore we only keep one single Bdd and deallocate
   * all the memory attached to the rest of the Mvf.
   */
  function = (bdd_node *)bdd_extract_node_as_is(Mvf_FunctionReadComponent(nodeFunction, 1));
  if (function != NULL) {
    bdd_ref(function);
  }
  
  /* Clean up */
  Mvf_FunctionFree(nodeFunction);
  return (function);
}


bdd_node *
ComposeLayersIntoResidue(Ntk_Network_t *network, 
                         array_t *layerArray, 
                         bdd_node *residueDd,
                         array_t *outputArray)
{
  bdd_manager *ddManager;                 /* Dd Manager */
  bdd_node *newResidueDd = NIL(bdd_node); /* final composed Dd */
  bdd_node *currentDd;                   /* local copy of residue Dd to
                                          * perform composition
                                          */
  lsList outputList, orderList;          /* output and layer+fanin node
                                          * list fed to the ordering procedure
                                          */
  lsHandle nodeHandle;                   /* handle for node list */ 
  int *invPermArray;                     /* inverse permutation array
                                          * for the Dd manager
                                          */
  array_t *newIdArray;                   /* array with new Ids to be
                                          * assigned to each node
                                          */
  Ntk_Node_t *nodePtr;                   /* variable to store node pointer */
  array_t *currentLayer;                 /* current layer of nodes */
  int numNodes;                          /* number of nodes in current layer */
  bdd_node **functionArray;              /* array of Adds of the current nodes
                                          * in terms of their fanin
                                          */
                                          
  bdd_node *functionBdd;                 /* Bdds of current layer nodes */
  char *flagValue;                       /* string that stores flag values */
  int verbose;                           /* verbosity level */
  int j, k;                              /* iterators */
  int layerIndex, nodeIndex;             /* iterators */
  long tempTime, thisComposeTime;        /* local time measurement variables */
  long thisSmartVarTime, thisOrderTime;  /* local time measurement variables */
  long thisShuffleTime;                  /* local time measurement variables */
  int unassignedValue;                   /* NTK_UNASSIGNED_MDD_ID value holder */
  
  /* initialize local time measurement variables */
  tempTime = 0;
  thisSmartVarTime = 0;
  thisOrderTime = 0;
  thisShuffleTime = 0;
  thisComposeTime = 0;
  unassignedValue =  NTK_UNASSIGNED_MDD_ID;
  
  /* make a local copy of the residue Dd to compose the network into */
  bdd_ref(currentDd = residueDd);
  
  /* read verbosity flag */
  verbose = 0;
  flagValue = Cmd_FlagReadByName("residue_verbosity");
  if (flagValue != NIL(char)) {
    verbose = atoi(flagValue);
  }
  
  ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network);
  /* initialize the variable manager that keeps track of what variables
   * are in use in residue verification.
   */
  ResResidueInitializeVariableManager(bdd_num_vars(ddManager));
  
  /* assume the pos are labeled before they come here each time */
  outputList = lsCreate();

  /* outputs do not need to be ordered as the node ids are already
   * assigned. Here this list is created just so that the variable
   * manager can be updated
   */

  arrayForEachItem(Ntk_Node_t *, outputArray, j, nodePtr) {
    lsNewEnd(outputList, (lsGeneric)nodePtr, (lsHandle *)&nodeHandle);
  }
  
  newIdArray = array_alloc(int, 0);
  tempTime = util_cpu_time();
  /* update the variable manager with the output node ids */
  invPermArray = ResResidueVarAllocate(ddManager, outputList, newIdArray);
  if (invPermArray == NIL(int)) {
    error_append("Unable to update variable manager\n");
    array_free(newIdArray);
    ResResidueFreeVariableManager();
    return NULL;
  } /* end of error */
  thisSmartVarTime += util_cpu_time() - tempTime;
  FREE(invPermArray);
  array_free(newIdArray);
  lsDestroy(outputList, (void (*)(lsGeneric))0);

  /* start the main loop for composition of layers into the residue Add */
  for(layerIndex = 0; layerIndex < array_n(layerArray); layerIndex++) {
    /* fetch each layer */
    currentLayer = ResLayerFetchIthLayer(layerArray, layerIndex);
    numNodes = ResLayerNumNodes(currentLayer);
    if (verbose >= 3) {
      fprintf(vis_stdout, "Layer %d being composed", layerIndex);
      fprintf(vis_stdout, " with %d nodes\n", numNodes);
    }

    /* create the order of the nodes in the layer and their fanin
     * for composition
     */
    tempTime = util_cpu_time();
    orderList = CreateNodeAndFaninOrderList(currentLayer);
    thisOrderTime +=  util_cpu_time() - tempTime;

    /* assign new Ids if required and create the corresponding variables
     * in the manager
     */
    newIdArray = array_alloc(int, 0);
    tempTime = util_cpu_time();
    invPermArray = ResResidueVarAllocate(ddManager, orderList, newIdArray);
    if (invPermArray == NIL(int)) {
      error_append("Unable to update variable manager\n");
      bdd_recursive_deref(ddManager, currentDd);
      array_free(newIdArray);
      ResResidueFreeVariableManager();
      return NULL;
    } /* end of error */
    thisSmartVarTime += util_cpu_time() - tempTime;

    /* assign Ids to unassigned fanin nodes */
    if (array_n(newIdArray)) {
      UpdateUnassignedNodesWithNewIds(orderList, newIdArray);
    }
    array_free(newIdArray);
    lsDestroy(orderList, (void (*)(lsGeneric))0);
    
    /* shuffle the IDs */
    tempTime = util_cpu_time();
    (void) bdd_shuffle_heap(ddManager, invPermArray);
    thisShuffleTime += util_cpu_time() - tempTime;
    FREE(invPermArray);
    
    /* array initialized for dd nodes of the current layer */
    tempTime = util_cpu_time();
    functionArray = ALLOC(bdd_node *, numNodes);
    LayerForEachNode(currentLayer, nodeIndex, nodePtr) {

      /* build the BDD for the function of each node */
      functionBdd = BuildBDDforNode(network, nodePtr, IMMEDIATE_FANIN);
      if (functionBdd == NULL) { /* error */
        error_append("Unable to build function for node ");
        error_append(Ntk_NodeReadName(nodePtr));
        error_append("\n");
        for (k = 0; k < nodeIndex; k++) {
          bdd_recursive_deref(ddManager, functionArray[k]);
        }
        FREE(functionArray);
        bdd_recursive_deref(ddManager, currentDd);
        ResResidueFreeVariableManager();
        return NULL;
      } /* end of error */

      /* Convert to ADD */
      bdd_ref(functionArray[nodeIndex] = bdd_bdd_to_add(ddManager, functionBdd));
      bdd_recursive_deref(ddManager, functionBdd);
      if (functionArray[nodeIndex] == NULL) { /* error */
        error_append("Unable to build add from bdd for node ");
        error_append(Ntk_NodeReadName(nodePtr));
        error_append("\n");
        for (k = 0; k < nodeIndex; k++) {
          bdd_recursive_deref(ddManager, functionArray[k]);
        }
        FREE(functionArray);
        bdd_recursive_deref(ddManager, currentDd);
        ResResidueFreeVariableManager();
        return NULL;
      } /* end of error */
    } /* end of iterating over each node in a layer */
    /* compose the array into the residue ADD */

    /* Perform the actual composition of current layer */
    tempTime = util_cpu_time();
    newResidueDd = ComposeLayer(ddManager, currentDd,  currentLayer, functionArray);
    thisComposeTime += util_cpu_time() - tempTime;
    /* free old residue Dd */
    bdd_recursive_deref(ddManager, currentDd);
    if (newResidueDd == NULL) { /* error */
      error_append("Unable to do composition for layer\n");
      for (k = 0; k < numNodes; k++) {
        bdd_recursive_deref(ddManager, functionArray[k]);
      }
      FREE(functionArray);
      ResResidueFreeVariableManager();
      return NULL;
    } /* end of error */
    currentDd = newResidueDd;
    if (verbose >= 3) {
      mdd_t *fnMddT;
      int size;
      bdd_ref(currentDd);
      fnMddT = bdd_construct_bdd_t(ddManager, currentDd);
      size = bdd_size(fnMddT);
      bdd_free(fnMddT);
      fprintf(vis_stdout, "Layer %d has %d nodes\n", layerIndex,
              size);
    }
    
    /* free function array */
    for (j = 0; j < numNodes; j++) {
      bdd_recursive_deref(ddManager, functionArray[j]);
    }
    FREE(functionArray);
    
    /*  free ids of nodes just composed */
    ResResidueVarDeallocate(currentLayer);
    /* reset node Ids of the composed layer */
    LayerForEachNode(currentLayer, j, nodePtr) {
      if (!Ntk_NodeTestIsCombInput(nodePtr)) {
        Ntk_NodeSetMddId(nodePtr, unassignedValue);
      }
    }
  } /* end of iterating over the layers */

  /* free the variable manager */
  ResResidueFreeVariableManager();
  if (verbose >= 1) {
    (void) fprintf(vis_stdout, "ADD Compose Time = %.3f\n",(thisComposeTime)/1000.0);
    (void) fprintf(vis_stdout, "Smart variable allocation time = %.3f\n", (thisSmartVarTime)/1000.0);
    (void) fprintf(vis_stdout, "Shuffle time = %.3f\n", (thisShuffleTime)/1000.0);
    (void) fprintf(vis_stdout, "Order time = %.3f\n", (thisOrderTime)/1000.0);
  }
  /* update global time variables */
  Res_composeTime += thisComposeTime;
  Res_smartVarTime += thisSmartVarTime;
  Res_shuffleTime += thisShuffleTime;
  Res_orderTime += thisOrderTime;

  /* return the composed residue Dd in terms of the primary inputs */
  return(newResidueDd);
  
} /* End of ComposeLayersIntoResidue */

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

static void
UpdateUnassignedNodesWithNewIds(lsList orderList,   
                                array_t *newIdArray) 
{
  int i, id;
  lsGen listGen;
  Ntk_Node_t *nodePtr;
  char *flagValue;
  int verbose;
  
  verbose = 0;
  flagValue = Cmd_FlagReadByName("residue_verbosity");
  if (flagValue != NIL(char)) {
    verbose = atoi(flagValue);
  }

  /* step through each item in the list to find nodes with unassigned Ids */
  i = 0;
  lsForEachItem(orderList, listGen, nodePtr) {
    if (Ntk_NodeReadMddId(nodePtr) == NTK_UNASSIGNED_MDD_ID) {
      id = array_fetch(int, newIdArray, i);
      Ntk_NodeSetMddId(nodePtr, id);
      i++;
      if (verbose >= 4) {
        fprintf(vis_stdout, "Id %d being assigned to node %s\n", id,
                Ntk_NodeReadName(nodePtr));
      }
    }
  }
  assert(i == array_n(newIdArray));
  return;
} /* End of UpdateUnassignedNodesWithNewIds */


static lsList
CreateNodeAndFaninOrderList(array_t *currentLayer) 
{
  st_table *faninTable;       /* table to store fanin */
  lsList layerList;           /* list of nodes in layer */
  lsList faninVarSetList;     /* list of support corresponding to layer
                               * nodes.
                               */
  lsList newList;             /* ordered list of nodes and fanins */
  lsGen listGen;              /* generator to step through list */
  lsGen layerGen, faninGen;   /* generators to step through lists */
  int totalFanins;/* variable to store total number of fanins
                               * of this layer
                               */
  int intersect;              /* number of elements in the intersection
                               * of support.
                               */
  int i, j, faninIndex;       /* iterators */
  Ntk_Node_t *nodePtr;        /* node pointer variables */
  Ntk_Node_t *faninNodePtr;   /* node pointer variables */
  Ntk_Node_t *nextNodePtr;    /* node pointer variables */
  lsHandle nodeHandle;        /* handle for ls procedure */
  lsHandle varSetHandle;      /* handle for ls procedure */
  lsHandle newNodeHandle;     /* handle for ls procedure */
  lsHandle maxIntersectNodeHandle;   /* handle for ls procedure */
  lsHandle maxIntersectVarSetHandle; /* handle for ls procedure */
  var_set_t *currVarSet;      /* support of current node */
  var_set_t *varSetIntersect; /* intersection of support between 2 nodes */
  var_set_t *nextVarSet;      /* support of next node */
  array_t *faninArray;        /* array of fanin of a node read from network */
  lsList faninList;           /* list of fanins of current layer */
  int nodeIndex;              /* iterator */
  int verbose;                /* verbosity level */
  char *flagValue;            /* string to read flag value */
  
  verbose = 0;
  flagValue = Cmd_FlagReadByName("residue_verbosity");
  if (flagValue != NIL(char)) {
    verbose = atoi(flagValue);
  }

  /* sort current layer by position in the dd manager for least number
   * of shuffles
   */
  LayerSort(currentLayer, IdCompare);
  /* create a list to be able to order the list and later manipulation */
  layerList = lsCreate();
  if (verbose >= 4) {
    fprintf(vis_stdout, "Nodes in this layer are: ");
  }
  LayerForEachNode(currentLayer, i, nodePtr) {
    lsNewEnd(layerList, (lsGeneric)nodePtr, (lsHandle *)&nodeHandle);
    if (verbose >= 4) {
      fprintf(vis_stdout, "%s ",Ntk_NodeReadName(nodePtr));
    }
  }
  if (verbose >= 4) {
    fprintf(vis_stdout, "\n");
  }

  /* insert all fanins in a table with a unique index. This is to identify
   * each fanin as a support variable
   */
  faninIndex = 0;
  faninTable = st_init_table(st_ptrcmp, st_ptrhash);

  LayerForEachNode(currentLayer, nodeIndex, nodePtr) {
    Ntk_NodeForEachFanin(nodePtr, j, faninNodePtr) {
      /* here constants are omitted, so that they are not assigned an
       * Id. The other case to be avoided is when the node in consideration
       * is a latch output i.e. a combinational input. Hence it is not
       * desirable that the latch data input and latch initial input
       * be considered as its fanin.
       */
      if ((!st_is_member(faninTable, (char *)faninNodePtr)) &&
        (!(Ntk_NodeTestIsConstant(faninNodePtr) ||
        (Ntk_NodeTestIsLatch(nodePtr) &&
         (Ntk_NodeTestIsLatchDataInput(faninNodePtr) ||
          Ntk_NodeTestIsLatchInitialInput(faninNodePtr)))))) {
        st_insert(faninTable, (char *)faninNodePtr,
                  (char *)(long)faninIndex);
        faninIndex++;
      }
    }
  }
  /* keep a count of the total number of fanins to this layer */
  totalFanins = faninIndex;
  
  /* Create fanin var set for each node */
  faninVarSetList = CreateFaninVarSetList(currentLayer, faninTable);
  st_free_table(faninTable);

  /* Main sorting part: Like Insertion Sort*/
  /* initialize to first item from both layer and fanin lists */
  /* starting here, find the list element in the list with max overlap
   * with this element. Here each node in the layer is brought up
   * neighbor
   */
  (void) lsFirstItem(faninVarSetList, &currVarSet, &varSetHandle);
  (void) lsFirstItem(layerList, &nodePtr, &nodeHandle);
  (void) lsRemoveItem(nodeHandle, &nodePtr);
  (void) lsRemoveItem(varSetHandle, &currVarSet);
  
  /* insert first item in new list */
  newList = lsCreate();
  lsNewEnd(newList, (lsGeneric)nodePtr, (lsHandle *)&newNodeHandle);
  
  /* create var set for checking overlap of support */
  varSetIntersect = var_set_new(totalFanins);
  /* done when all the nodes in the layerList have been transferred
   * to new list. In each iteration of this list, the node with max
   * support overlap with the current node is taken out of the list
   * and added to the new list. Its corresponding var set is also
   * removed, the current var set is freed and the new var set is
   * set to the current var set. The var set list has to be manipulated
   * simultaneously to keep the correspondence between the node list
   * and its support list.
   */
  while(lsLength(newList) != ResLayerNumNodes(currentLayer)) { /* while not done */
    /* create generators to step through list */
    faninGen = lsStart(faninVarSetList);
    layerGen = lsStart(layerList);
    /* initialize */
    intersect = 0;
    maxIntersectNodeHandle = NULL;
    maxIntersectVarSetHandle = NULL;
    while (lsNext(layerGen, &nextNodePtr, &nodeHandle) != LS_NOMORE) {
      /* clear result var set */
      var_set_clear(varSetIntersect);
      /* position var set corresponding to node in layer list */
      lsNext(faninGen, &nextVarSet, &varSetHandle);
      /* get support overlap */
      varSetIntersect = var_set_and(varSetIntersect, currVarSet, nextVarSet);
      /* check if current overlap is larger than current max */
      if (var_set_n_elts(varSetIntersect) > intersect) {
        /* record current position */
        intersect = var_set_n_elts(varSetIntersect);
        maxIntersectNodeHandle = nodeHandle;
        maxIntersectVarSetHandle = varSetHandle;
      }
    } /* end of iterating over layer list */

    /* destroy Generator */
    (void) lsFinish(layerGen);
    (void) lsFinish(faninGen);
    /* free current var set */
    var_set_free(currVarSet);
    /* process differently if there was overlap and if there wasn't */
    if (maxIntersectNodeHandle == NULL) {
      /* support overlap was zero with the rest of the nodes */
      /* set current item to first in the lists */
      (void) lsFirstItem(faninVarSetList, &nextVarSet, &maxIntersectVarSetHandle);
      (void) lsFirstItem(layerList, &nextNodePtr, &maxIntersectNodeHandle);
    }
    
    /* remove max support overlap item from the lists */
    (void) lsRemoveItem(maxIntersectNodeHandle, &nextNodePtr);
    (void) lsRemoveItem(maxIntersectVarSetHandle, &nextVarSet);
    
    /* add node to the new list */
    lsNewEnd(newList, (lsGeneric)nextNodePtr, (lsHandle *)&newNodeHandle);
    /* move current item to the new item */
    currVarSet = nextVarSet;

  }
  /* Clean up */
  var_set_free(varSetIntersect);
  var_set_free(currVarSet);
  lsDestroy(faninVarSetList, (void (*)(lsGeneric))0);
  lsDestroy(layerList, (void (*)(lsGeneric))0);
  /* end of sorting part */
  
  /* insert nodes in new order in the current layer */
  i = 0;
  lsForEachItem(newList, listGen, nodePtr) {
    LayerAddNodeAtIthPosition(currentLayer, i, nodePtr);
    i++;
  }
  assert(lsLength(newList) == array_n(currentLayer));

  /* keep track of running update of the fanins included */
  faninTable = st_init_table(st_ptrcmp, st_ptrhash);
  /* insert fanin nodes after the last node in the order */
  nodeIndex = ResLayerNumNodes(currentLayer)-1;
  /* while nodes exist that have to be processed and all fanins haven't
   * been processed, repeat
   */
  while ((nodeIndex >= 0) || (st_count(faninTable) != totalFanins)) {
    nodePtr = LayerFetchIthNode(currentLayer, nodeIndex);
    faninArray = Ntk_NodeReadFanins(nodePtr);
    /* create a fanin list to append to the nodeList */
    faninList = lsCreate();
    arrayForEachItem(Ntk_Node_t *, faninArray, i, faninNodePtr) {
      /* only include those fanins that haven't appeared yet. Also
       * exclude the cases where the node is a constant and it is
       * a latch data/initial input. You don't want to compose a
       * latch output i.e. a combinational input with the latch input.
       */
      if ((!st_is_member(faninTable, (char *)faninNodePtr)) &&
          (!(Ntk_NodeTestIsConstant(faninNodePtr) ||
             (Ntk_NodeTestIsLatch(nodePtr) &&
              (Ntk_NodeTestIsLatchDataInput(faninNodePtr) ||
               Ntk_NodeTestIsLatchInitialInput(faninNodePtr)))))) {
        lsNewEnd(faninList, (lsGeneric)faninNodePtr, (lsHandle *)&nodeHandle);
        st_insert(faninTable, (char *)faninNodePtr, NIL(char));
        /* done when all fanins have been processed */
        if (st_count(faninTable) == totalFanins) break;
      }
    }
    /* if list is not empty add fanin behind the node */
    if (lsLength(faninList)) { 
      /* sort fanins by their level in the ddmanager */
      lsSort(faninList, IdListCompare);
      /* append the fanin list to the node list */
      newList = ListAppend(nodePtr, newList, faninList);
    }
    lsDestroy(faninList, (void (*)(lsGeneric))0);
    nodeIndex--;

  } /* end of while fanin nodes need to be processed and nodes
     * are present in layer */
  st_free_table(faninTable);
  assert(lsLength(newList) == (array_n(currentLayer) + totalFanins));

  return(newList);
} /* End of CreateNodeAndFaninOrderList */


static lsList
ListAppend(Ntk_Node_t *nodePtr, 
           lsList newList,      
           lsList faninList)    
{
  lsGen layerGen, newGen, faninGen;
  Ntk_Node_t *currNodePtr, *faninNodePtr;
  lsHandle nodeHandle, faninNodeHandle;
  lsStatus status;
  
  layerGen = lsEnd(newList);
  /* find the spot to insert fanin List */
  while(lsPrev(layerGen, &currNodePtr, &nodeHandle) != LS_NOMORE) {
    if (nodePtr == currNodePtr) {
      /* when spot found, insert fanin list */
      newGen = lsGenHandle(nodeHandle, &currNodePtr, LS_AFTER);
      lsForEachItem(faninList, faninGen, faninNodePtr) {
        status = lsInAfter(newGen, (lsGeneric)faninNodePtr, (lsHandle *)&faninNodeHandle);
        if (status != LS_OK) {
          error_append("Something wrong with fanin list to be appended\n");
          status = lsFinish(layerGen);
          status = lsFinish(newGen);
          status = lsFinish(faninGen);
          return NULL;
        }
      } /* end of iterating through the fanin list */
      /* done as fanin list has been inserted */
      lsFinish(newGen);
      break;
    } /* end of if node found  in the list */
  } /* end of stepping through the new list */
  
  /* Clean up generators */
  lsFinish(layerGen);
  
  /* return modified list */
  return (newList);
}/* End of ListAppend */
    

static int
IdCompare(const void *obj1,
          const void *obj2)
{
  Ntk_Node_t *nodePtr1, *nodePtr2;
  int id1 , id2;
  int level1, level2;
  Ntk_Network_t *network;
  bdd_manager *ddManager;
  
  nodePtr1 = *(Ntk_Node_t **)obj1;
  nodePtr2 = *(Ntk_Node_t **)obj2;
  id1 = Ntk_NodeReadMddId((Ntk_Node_t *)nodePtr1);
  id2 = Ntk_NodeReadMddId((Ntk_Node_t *)nodePtr2);
  /* if unassigned Ids return the value before reading the
   * position . If equal return -1.
   */
  if ((id1 == NTK_UNASSIGNED_MDD_ID) || (id2 == NTK_UNASSIGNED_MDD_ID)) {
    if (id1 == NTK_UNASSIGNED_MDD_ID) {
      return -1;
    } else {
      return 1;
    }
  }

  network = Ntk_NodeReadNetwork(nodePtr1);
  ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network);
  level1 = bdd_get_level_from_id(ddManager, id1);
  level2 = bdd_get_level_from_id(ddManager, id2);
  if (level1 > level2) {
    return 1;
  } else if (level1 == level2) {
    return 0;
  } else {
    return -1;
  }
} /* End of IdCompare */

static int
IdListCompare(lsGeneric item1,
              lsGeneric item2)
{
  Ntk_Node_t *nodePtr1, *nodePtr2;
  int id1 , id2;
  int level1, level2;
  Ntk_Network_t *network;
  bdd_manager *ddManager;

  
  nodePtr1 = (Ntk_Node_t *)item1;
  nodePtr2 = (Ntk_Node_t *)item2;
  id1 = Ntk_NodeReadMddId((Ntk_Node_t *)nodePtr1);
  id2 = Ntk_NodeReadMddId((Ntk_Node_t *)nodePtr2);
  /* if unassigned Ids return the value before reading the
   * position . If equal return -1.
   */
  if ((id1 == NTK_UNASSIGNED_MDD_ID) || (id2 == NTK_UNASSIGNED_MDD_ID)) {
    if (id1 == NTK_UNASSIGNED_MDD_ID) {
      return -1;
    } else {
      return 1;
    }
  }
  network = Ntk_NodeReadNetwork(nodePtr1);
  ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network);
  level1 = bdd_get_level_from_id(ddManager, id1);
  level2 = bdd_get_level_from_id(ddManager, id2);
  if (level1 > level2) {
    return 1;
  } else if (level1 == level2) {
    return 0;
  } else {
    return -1;
  }
} /* End of IdListCompare */


static lsList
CreateFaninVarSetList(array_t *currentLayer, 
                      st_table *faninTable)  
{
  Ntk_Node_t *nodePtr, *faninNodePtr;  /* variables to store nodes */
  array_t *faninArray;                 /* array of fanin of nodes */
  lsList faninVarSetList;              /* list of var set representing
                                        * support of nodes in layer
                                        */
  var_set_t *currVarSet;               /* var set indicating current
                                        * node support
                                        */
  lsHandle varSetHandle;               /* handle for ls procedure */
  int totalFanins;                     /* total number of fanins of this
                                        * layer.
                                        */
  int i, j, faninIndex;                /* iterators */


  
  totalFanins = (int)st_count(faninTable);
  faninVarSetList = lsCreate();
  /* create var-set of support for each node in this layer */
  arrayForEachItem(Ntk_Node_t *, currentLayer, i, nodePtr) {
    faninArray = Ntk_NodeReadFanins(nodePtr);
    currVarSet = var_set_new(totalFanins);
    /* if the above node is a constant, the var set will be empty
     * also if it a latch output(comb. input), then the var set will
     * be empty.
     */
    arrayForEachItem(Ntk_Node_t *, faninArray, j, faninNodePtr) {
      /* process only those fanins in the table, i.e. no constants
       * no latch inputs (combinational outputs) are fanins to this array
       */
      if (st_lookup_int(faninTable, (char *)faninNodePtr, &faninIndex)) {
        /* these aren't supposed to be here */
        assert(!((Ntk_NodeTestIsConstant(faninNodePtr) ||
                  (Ntk_NodeTestIsLatch(nodePtr) &&
                   (Ntk_NodeTestIsLatchDataInput(faninNodePtr) ||
                    Ntk_NodeTestIsLatchInitialInput(faninNodePtr))))));
        /* set the bit in the support according to the index the fanin
         * was assigned
         */
        var_set_set_elt(currVarSet, faninIndex);
      } /* end of if is in the fanin table (has no constants and no
         * latch data or initial input.
         */
    } /* end of if present in fanin table */
    /* insert var set in fanin var set list */
    lsNewEnd(faninVarSetList, (lsGeneric)currVarSet, (lsHandle *)&varSetHandle);
  }
  return (faninVarSetList);
} /* End of CreateFaninVarSetList */

static bdd_node *
ComposeLayer(bdd_manager *ddManager,    
             bdd_node *residueDd,       
             array_t *currentLayer,   
             bdd_node **functionArray)  
{
  Ntk_Node_t *nodePtr;          /* variable to store nodes */
  char *flagValue;              /* string to read flag value */
  ResCompositionMethod method;  /* type of composition to be performed */
  int i, j, layerIndex;                     /* iterators */
  int nodeId;                   /* current node id */
  bdd_node **composeVector;       /* vector required for composition */
  bdd_node *new_ = NIL(bdd_node), *andDd,*yDd, *nodeReln, *currentDd; /* temporary Dds */
  int maxLayerSize;             /* max size of layers */
  int first, last;              /* first and last positions of the array */
  
  /* read the type of composition to be performed, default is vector
   * composition.
   */
  flagValue = Cmd_FlagReadByName("residue_composition_method");
  if (flagValue == NIL(char)) {
    method = ResDefaultComposeMethod_c;
  } else if (strcmp(flagValue, "vector") == 0) {
      method = ResVector_c;
  } else if (strcmp(flagValue, "onegate") == 0) {
    method =  ResOneGateAtATime_c;
  } else if (strcmp(flagValue, "preimage") == 0) {
    method = ResPreimageComputation_c;
  } else if (strcmp(flagValue, "superG") == 0) {
    method = ResSuperG_c;
  } else {
    fprintf(vis_stderr, 
            "** res warning: Unknown composition method, %s, resorting to default.\n", 
            flagValue);
    method = ResDefaultComposeMethod_c;
  } 

  switch(method) {

  case ResVector_c:
  case ResSuperG_c:
    {
      /* read the flag for maximum value of layer size */
      flagValue = Cmd_FlagReadByName("residue_layer_size");
      if (flagValue == NIL(char)) {
        maxLayerSize = ResLayerNumNodes(currentLayer);  
      } else {
        maxLayerSize = atoi(flagValue);
      }
      /* if max layer size is within 5 nodes of the length of the
       * size of the array, resize it to the size of the array
       */
      if (maxLayerSize + 5 >= ResLayerNumNodes(currentLayer)) {
        maxLayerSize = ResLayerNumNodes(currentLayer);
      }

      /* initialize a vector with projection functions */
      composeVector = ALLOC(bdd_node *, bdd_num_vars(ddManager));
      for(i = 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
        bdd_ref(composeVector[i] = bdd_add_ith_var(ddManager, i));
        if (composeVector[i] == NIL(bdd_node)) { /* error */
          error_append("Something wrong in obtaining projection functions");
          for(j = 0; j < i; j++) {
            bdd_recursive_deref(ddManager, composeVector[j]);
          }
          return NIL(bdd_node);
        } /* end of if error */
      }
      /* break this layer up into sub-layers to ease composition
       * process. Hence the composition will be performed for several
       * subarrays.
       */
      /* start at the end of the layer */
      layerIndex = ResLayerNumNodes(currentLayer);
      /* make a local copy */
      bdd_ref(currentDd = residueDd);
      do {
        /* extract sublayers in the size of maxLayerSize starting from the
         * end of the layer or a smaller sub-layer (leftover) in the end
         */

        /* record last+1 position of the sub-layer in the current layer */
        last = layerIndex;

        /* record the position of the beginning of this sub-layer */ 
        first = (last < maxLayerSize) ? 0 : (last - maxLayerSize);

        /* iterate through the layer to find the sublayer */
        while(layerIndex  > first) { /* extract sub-layer */
          layerIndex--;
          nodePtr = LayerFetchIthNode(currentLayer, layerIndex);
          nodeId = Ntk_NodeReadMddId(nodePtr);
          bdd_recursive_deref(ddManager, composeVector[nodeId]);
          /* plug in the functions of the nodes in the layer instead of
           * the projection functions
           */
          bdd_ref(composeVector[nodeId] = functionArray[layerIndex]);
        }

        /* perform composition */
        if (method == ResVector_c) {
          bdd_ref(new_ = bdd_add_vector_compose(ddManager, currentDd, composeVector));
        } else {
          bdd_ref(new_ = bdd_add_nonsim_compose(ddManager, currentDd, composeVector));
        }

        /* free old copy and use new to compose in the next sub-layer, if any */
        bdd_recursive_deref(ddManager, currentDd);
        currentDd = new_;
        
        if (new_ == NULL) { /* error */
          error_append("NULL Dd returned on vector or superG compose\n");
          break;
        } /* end of error */

        /* undo the compose vector changes for this sub-array to
         * prepare it for the next subarray. Replace the function of
         * nodes with the projection functions
         */
        for (i = first; i < last; i++) {
          nodePtr = LayerFetchIthNode(currentLayer, i);
          nodeId = Ntk_NodeReadMddId(nodePtr);
          bdd_recursive_deref(ddManager, composeVector[nodeId]);
          bdd_ref(composeVector[nodeId] = bdd_add_ith_var(ddManager, nodeId));
        }
      } while(layerIndex  > 0);

      /* clean up */
      for(i = 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
        bdd_recursive_deref(ddManager, composeVector[i]);
      }
      FREE(composeVector);
      break;
    } /* end of cases: ResVector_c, ResSuperG_c */
  case ResOneGateAtATime_c:
    {
      /* duplicate  as current Dd gets freed later */
      bdd_ref(currentDd = residueDd);
      /* compose the nodes in one at a time */
      LayerForEachNode(currentLayer, i, nodePtr) {
        nodeId = Ntk_NodeReadMddId(nodePtr);
        bdd_ref(new_ = bdd_add_compose(ddManager, currentDd, functionArray[i],
                                       nodeId));
        bdd_recursive_deref(ddManager, currentDd);
        if (new_ == NULL) { /* error */
          error_append("NULL Dd returned on single gate compose, node: ");
          error_append(Ntk_NodeReadName(nodePtr));
          error_append("\n");
          return NULL;
        } /* end of error */
        currentDd = new_;
      }
      break;
    } /* end of case Res_OneGateAtATime_c */
  case ResPreimageComputation_c:
    {
      /* duplicate  as current Dd gets freed later */
      bdd_ref(currentDd = residueDd);
      /* form the y_i \equiv f_i(x) relation, this would be wrong
       * if the node appeared again in the circuit. But here it is
       * correct due to the one time rule
       */
      LayerForEachNode(currentLayer, i, nodePtr) {
        nodeId = Ntk_NodeReadMddId(nodePtr);
        /* find the var for this node */
        bdd_ref(yDd = bdd_add_ith_var(ddManager, nodeId));
        if (yDd == NULL) { /* error */
          error_append("Null Dd returned on preimage compose- y_i stage. ");
          error_append("Node: ");
          error_append(Ntk_NodeReadName(nodePtr));
          bdd_recursive_deref(ddManager, currentDd);
          error_append("\n");
          return NULL;
        } /* end of error */
        /* construct the relation */
        bdd_ref(nodeReln = bdd_add_apply(ddManager, bdd_add_xnor, yDd, functionArray[i]));

        if (nodeReln == NULL) { /* error */
          error_append("Null Dd returned on preimage compose - node reln stage");
          error_append("Node: ");
          error_append(Ntk_NodeReadName(nodePtr));
          bdd_recursive_deref(ddManager, yDd);
          bdd_recursive_deref(ddManager, currentDd);
          error_append("\n");
          return NULL;
        } /* end of error */
        /* perform the and of the and-abstract */
        bdd_ref(andDd = bdd_add_apply(ddManager, bdd_add_times, currentDd, nodeReln));
        bdd_recursive_deref(ddManager, currentDd);
        bdd_recursive_deref(ddManager, nodeReln);
        if (andDd == NULL) { /* error */
          error_append("Null Dd returned on preimage compose - and dd stage");
          error_append("Node: ");
          error_append(Ntk_NodeReadName(nodePtr));
          error_append("\n");
          bdd_recursive_deref(ddManager, yDd);
          return NULL;
        } /* end of error */
        /* perform the abstract of the and-abstract */
        bdd_ref(new_ = bdd_add_exist_abstract(ddManager, andDd, yDd));
        bdd_recursive_deref(ddManager, andDd);
        bdd_recursive_deref(ddManager, yDd);
        if (new_ == NULL) { /* error */
          error_append("Null Dd returned on preimage compose - and dd stage");
          error_append("Node: ");
          error_append((char *)Ntk_NodeReadName(nodePtr));
          error_append("\n");
          return NULL;
        } /* end of error */
        currentDd = new_;
      }
      break;
    } /* end of case Res_PreimageComputation_c */
  } /* end of switch(method) */
  
  /* return the new composed Dd */
  return new_;
} /* End of ComposeLayersIntoResidue */
 

static Mvf_Function_t *
NodeBuildConstantMvf(
  Ntk_Node_t * node,
  mdd_manager *mddMgr)
{
  int             value        = 0; /* initialized to stop lint complaining */
  mdd_t          *oneMdd       = mdd_one(mddMgr);
  Var_Variable_t *variable     = Ntk_NodeReadVariable(node);
  int             numVarValues = Var_VariableReadNumValues(variable);
  Mvf_Function_t *mvf          = Mvf_FunctionAlloc(mddMgr, numVarValues);
  int          outputIndex = Ntk_NodeReadOutputIndex(node);
  Tbl_Table_t *table       = Ntk_NodeReadTable(node);

  assert(Ntk_NodeTestIsConstant(node));
  value = Tbl_TableReadConstValue(table, outputIndex);
  assert(value != -1);
  
  Mvf_FunctionAddMintermsToComponent(mvf, value, oneMdd);
  mdd_free(oneMdd);
  return mvf;
}