source: vis_dev/vis-2.3/src/res/resCompose.c @ 104

/**CFile***********************************************************************

  FileName    [resCompose.c]

  PackageName [res]

  Synopsis [This file contains all relevant procedures for the composition of
  the nodes of the circuit into the residue Add.]

  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"

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

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

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

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


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


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

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

  Synopsis [Return a referenced BDD for the function of a node.]

  Description [Return a referenced BDD for the function of a node. This
  procedure uses the Ntm call but frees the rest of the MDD structure and
  returns the bdd only. The arguments to this function are the network to which
  this node belongs, the node whose bdd is required and the type of fanin
  support its BDDs need to be in terms of.]

  SideEffects   []

  SeeAlso            [Res_NetworkResidueVerify]

******************************************************************************/
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);
}


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

  Synopsis [Procedure to compose the network into the residue ADD.]

  Description [Procedure to compose the network into the residue ADD.  Assume
  here that the output nodes are labeled with the same ids as the vars in the
  initial residue dd. The variable manager has to be initialized for smart
  variable allocation. First the variable manager is updated with the output
  node Ids. Starting from the last layer, the nodes in each layer are ordered
  with their fanins such that the nodes being composed in are always above
  their fanin. This list is given to the variable manager to update the Ids in
  use, provide available Ids for the unassigned nodes and allocate new
  variables in both the variable and Dd manager. The variable manager then
  marks all the node and fanin ids in use and returns an id array for the
  unassigned nodes, reusing the ids whenever possible. It is also responsible
  for creating an inverse permutation array with the current layer nodes and
  their fanins in the order of the list and nodes unrelated at the bottom. The
  unassigned nodes are updated with the ID array. The inverse permutation array
  is fed to a CUDD procedure that moves the Ids to the required levels. Once
  this order is achieved, composition is performed depending on the method
  specified. Since the variable allocation procedure assumes that nodes with
  unassigned IDs need to be filled with the holes closest to them, the ID on
  each node is cleared after composition. This also makes it cleaner. The
  variable manager is freed at the end of the procedure. The result of the
  composition is the new residue Dd and is used for composition of the next
  layer. The procedure returns the residue Dd in terms of the primary
  inputs. The arguments to this function are the network to which the layers
  belong, the layer array structure and the residue DD into which the circuit
  needs to be composed into.This assumes that the residue DD has as many
  variables as the number of outputs and the Ids of the variables starts with
  0.]

  SideEffects []

  SeeAlso     [ResidueVerification]

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

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

  Synopsis  [Updates unassigned nodes in list with mdd ids in the array.]

  Description [Updates unassigned nodes in list with mdd ids in the array. The
  procedure steps through all nodes in a list and assigns them an id from the
  array. The parameters to this procedure are the list of nodes, some of which
  may not have assigned IDs and the array containing new Ids ready to be
  assigned to the nodes.]
  
  SideEffects   []

  SeeAlso            [ComposeLayersIntoResidue]

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


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

  Synopsis  [Creates a list of the nodes of layer and the fanin nodes
  of the layer.]

  Description [Creates a list of the nodes of a layer and the order in which
  they should appear in the dd manager for the composition process.  The main
  idea is to be as efficient in composition as possible. This requires nodes
  with overlapping support to be together, nodes being above their fanins in
  the dd order (to perform fewer ITE calls) and nodes being composed in at the
  top of the DD. This requires shuffling of the nodes in the layer to the top
  and their fanins below them.  Shuffling is done by sifting and is an
  expensive operation. Hence the motivation to keep the shuffles to as few as
  possible. So we start with layer where the nodes are sorted according to
  their level in the dd manager. It is a greedy heuristic that tries to
  minimize the sifting.  Next the nodes with overlapping support are brought
  together. Finally the fanin Nodes are sorted according to their levels too
  and inserted below the last (in the order) node of their fanout. The
  procedure returns the final sorted list of the nodes in the layer and their
  fanin. Note: It is assumed that the current layer has Ids assigned to
  it. This implies that the Primary outputs need special assignment of Ids and
  every other node automatically gets assigned Ids since they appear in the
  transitive fanin of some output. The function takes as an argument the layer
  to be ordered.]
  
  SideEffects   []

  SeeAlso            [ComposeLayersIntoResidue]

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


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

  Synopsis  [Procedure to add fanin nodes below a particular node.]

  Description [ Procedure to add fanin nodes below a particular node.  Finds
  the node in the list after which fanin list is to be added.  Adds nodes in
  the fanin list to the new list. This procedure takes as arguments the nodePtr
  after which the fanins are to be inserted, the collated list where the fanins
  should be inserted and a list of fanins. The updated list is returned.]

  SideEffects   [New list is added to.]

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

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

  Synopsis  [ Compares the Ids of 2 nodes.]

  Description [Compares the Ids of 2 nodes. It is a procedure fed to array
  sort.]
  
  SideEffects   []

  SeeAlso            [CreateNodeAndFaninOrderList]

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

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

  Synopsis  [Compares the Ids of 2 nodes.]

  Description [Compares the Ids of 2 nodes. it is fed to s list sort routine. ]
  
  SideEffects   []

  SeeAlso            [CreateNodeAndFaninOrderList]

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


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

  Synopsis  [Creates a list of var set of support for each node in layer.]

  Description [ Creates a list of var set of support for each node in layer.
  For each node in the layer, create a var set of support based on the fanin
  index stored in the fanin table. Returns a list of var sets. Takes as
  arguments the current layer whose support sets need to be formed and a table
  with the fanin and their unique IDs.]
  
  SideEffects   []

  SeeAlso            [CreateNodeAndFaninOrderList]

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

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

  Synopsis [Procedure that does the actual composition of a layer into the
  residue add.]

  Description [ Procedure that does the actual composition of a layer into the
  residue add depending on the method specified. Note for vector composition,
  this procedure assumes that currentLayer is sorted according to the levels
  and according to common support. This is done in
  CreateNodeAndFaninOrderList. The procedure takes as arguments the DD manager,
  the residue DD, the current layer that needs to be composed in and the array
  of the function BDDs of the nodes to be composed in (in 1-to-1 correspondence
  with the current layer. The procedure returns the composed Dd.]
  
  SideEffects   []

  SeeAlso            [ComposeLayersIntoResidue]

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

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

  Synopsis [Builds MVF for a node with no inputs, and only one row in its
  table.]

  Description [Builds MVF for a constant, then node should be a constant,
  combinational node.  In this case, an MVF is built with a single component
  (indexed by the value of node) is one, and all other components are zero.]

  SideEffects []

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