src/part/partFrontier.c

Go to the documentation of this file.

#include "partInt.h"

static char rcsid[] UNUSED = "$Id: partFrontier.c,v 1.25 2005/05/11 20:50:32 jinh Exp $";

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


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

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


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

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


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

static void PartitionCreateEdges(graph_t *partition);
static Mvf_Function_t * NodeBuildMvf(Ntk_Node_t * node, st_table * nodeToMvfTable);
static Mvf_Function_t * NodeBuildMvf2(Ntk_Node_t * node, st_table * nodeToMvfTable, st_table *faninNumberTable);
static Mvf_Function_t * NodeBuildPseudoInputMvf(Ntk_Node_t * node);
static void PrintPartitionRecursively(vertex_t *vertex, st_table *vertexTable, int indent);

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

void 
Part_PartitionReadOrCreateBnvs(
  Ntk_Network_t *network,
  st_table *coiLatchTable,
  st_table *coiBnvTable)
{
  graph_t    *partition;
  lsGen      lsgen;
  vertex_t   *vertex;
  long       mddId;
  Ntk_Node_t *node;

  /* if the partition is not available, sweep the network  */
  partition = Part_NetworkReadPartition(network);
  if (partition == NIL(graph_t)) {
    PartInsertBnvs(network, coiLatchTable, coiBnvTable);
    return;
  }

  /* otherwise, go through the vertices */
  foreach_vertex(partition, lsgen, vertex) {
    mddId = PartVertexReadMddId(vertex);
    if (mddId == -1) continue;

    node = Ntk_NetworkFindNodeByMddId(network, mddId);
    assert(node != NIL(Ntk_Node_t));

    if ( !Ntk_NodeTestIsCombInput(node) &&
         Ntk_NodeReadNumFanouts(node)!=0 )
      st_insert(coiBnvTable, (char *)node, NIL(char));
  }
 
}

void
Part_PartitionWithExistingBnvs(
  Ntk_Network_t *network,
  graph_t *partition,
  st_table *coiBnvTable,
  st_table *absLatchTable,
  st_table *absBnvTable)
{

  PartPartitionWithExistingBnvs(network, partition, coiBnvTable, 
                                absLatchTable, absBnvTable);
}

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

void
PartPartitionFrontier(Ntk_Network_t *network,
                      graph_t *partition,
                      lsList  rootList,
                      lsList  leaveList,
                      mdd_t   *careSet)
{
  Ntk_Node_t    *node;           /* Pointer to iterate over nodes */
  lsGen         gen;                /* To iterate over lists */
  vertex_t      *vertex;          /* Destination of the edge being added */
  char          *name;              /* Name of the node being processed */
  int           mddId;              /* Id of the node being processed */
  int           i;
  mdd_manager   *mddManager = PartPartitionReadMddManager(partition);
  /* nodeToMvfTable maps a node to the mvf in the form that is needed to build
     mvfs for the fanouts of the node.  I.e., a cutpoint node is mapped to an
     mdd for a new variable. */
  st_table *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
  st_table *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
  st_table *topoNodeTable;
  Ntk_Node_t *fanoutNode;
  array_t *rootNodesArray;
  long fanoutNumber = 0;
  Mvf_Function_t *nodeMvf; 
  long bddSize;
  int sizeThreshold;
  lsList topologicalNodeList;
  lsGen lsgen;
  st_generator *stgen;
  char *flagValue =  Cmd_FlagReadByName("partition_threshold");

  if (flagValue == NIL(char)){
    sizeThreshold = 1000; /* the default value */
  }
  else {
    sizeThreshold = atoi(flagValue);
  }

  /* Put combinational inputs in the leafNodesTable. */
  if (leaveList == (lsList)0) {
    Ntk_NetworkForEachCombInput(network, gen, node) {
      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
    }
  } /* End of then */ 
  else {
    lsForEachItem(leaveList, gen, node) {
      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
    }
  } /* End of if-then-else */

  
  /* Take the nodes in rootList as the roots */
  if (rootList == (lsList)0) {
    rootNodesArray = array_alloc(Ntk_Node_t *, 
                               Ntk_NetworkReadNumCombOutputs(network));
    i = 0;
    Ntk_NetworkForEachCombOutput(network, gen, node) {
      array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
    }

  } /* End of then */ 
  else {
    rootNodesArray = array_alloc(Ntk_Node_t *, lsLength(rootList));
    i = 0;
    lsForEachItem(rootList, gen, node) {
      array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
    }
  } /* End of if-then-else */

  /* Get an array of nodes sorted in topological order */
  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
                                                           rootNodesArray,
                                                           leafNodesTable);   

  /* For each node, compute the number of its fanouts */
  topoNodeTable = st_init_table(st_ptrcmp, st_ptrhash);
  lsForEachItem(topologicalNodeList, lsgen, node){
    st_insert(topoNodeTable, (char *)node, NIL(char));
  }
  lsForEachItem(topologicalNodeList, lsgen, node){
    fanoutNumber = 0;
    Ntk_NodeForEachFanout(node, i, fanoutNode) {
      if (st_is_member(topoNodeTable, fanoutNode) &&
          !st_is_member(leafNodesTable, fanoutNode))
        fanoutNumber++;
    }
    st_insert(topoNodeTable, node, (char *) fanoutNumber);
  }

  /* For each leaf nodes, create a vertex in the partition, create the mvf, and
   * a mapping of name to vertex, and mddId to vertex.
   */
  st_foreach_item(leafNodesTable, stgen, &node, NULL) {
    if (!st_lookup(topoNodeTable, node, &fanoutNumber)) {
      continue;
    }
    mddId = Ntk_NodeReadMddId(node);
    assert(mddId != NTK_UNASSIGNED_MDD_ID);
    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    st_insert(PartPartitionReadNameToVertex(partition), name, vertex);
    st_insert(PartPartitionReadMddIdToVertex(partition), (char *)(long)mddId,
              vertex); 

    if (Ntk_NodeTestIsPseudoInput(node)){
      nodeMvf = NodeBuildPseudoInputMvf(node);
    }
    else {
      nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
    }

    if (fanoutNumber <= 0) {
      st_insert(nodeToMvfTable, (char *)node, NIL(char));
    }else
      st_insert(nodeToMvfTable, (char *)node, 
                (char *)Mvf_FunctionDuplicate(nodeMvf));

    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf,
                                                             mddId);
  }

  st_free_table(leafNodesTable);
  

  fflush(vis_stdout);

  /* Go through the topologicalNodeList
   * a. If the node is of combinational input type, continue.
   *
   * b. Otherwise, Build the Mdd for this node, in terms of the function of the
   *    fanin nodes in. If the Mdd size exceeds the threshold, create an Mdd ID
   *    for this node.
   */

  lsForEachItem(topologicalNodeList, lsgen, node){
    if (st_is_member(nodeToMvfTable, (char *)node)) continue;

    nodeMvf = NodeBuildMvf2(node, nodeToMvfTable, topoNodeTable);
    bddSize = bdd_size_multiple(nodeMvf);

    if ((bddSize <= sizeThreshold) && !Ntk_NodeTestIsCombOutput(node)) {
      st_insert(nodeToMvfTable, node, nodeMvf);
      continue;
    }

    /* node either is a primary output, or has an mvf exceeding the
     * threshold. 
     */
    st_lookup(topoNodeTable, node, &fanoutNumber);
    if ( (bddSize > sizeThreshold) &&  fanoutNumber > 0 ) {
      if ((mddId = Ntk_NodeReadMddId(node)) == -1){
        Ord_NetworkAssignMddIdForNode(network, node);
        mddId = Ntk_NodeReadMddId(node);
      }
      st_insert(nodeToMvfTable, node,
                Mvf_FunctionCreateFromVariable(mddManager,mddId));
    }else {
      if (fanoutNumber <= 0) {
        st_insert(nodeToMvfTable, node, NIL(char));
      }else
        st_insert(nodeToMvfTable, (char *)node, 
                  (char *)Mvf_FunctionDuplicate(nodeMvf));
    }

    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    mddId = Ntk_NodeReadMddId(node);
    st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);
    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf, 
                                                             mddId);
    if (mddId != -1){
      st_insert(PartPartitionReadMddIdToVertex(partition),
                (char *)(long)mddId, (char *)vertex);
    }
  }/* for each member of topologicalNodeList */
  

  /* sanity check */
  st_foreach_item(nodeToMvfTable, stgen, &node, &nodeMvf) {
#if 0
    if (nodeMvf != NIL(Mvf_Function_t)) {
      int chk = st_lookup(topoNodeTable, node, &fanoutNumber);
      Ntk_NodeForEachFanout(node, i, fanoutNode) {
        fprintf(vis_stdout, "\nunclean node %s   =>   %s", 
                Ntk_NodeReadName(node),
                Ntk_NodeReadName(fanoutNode));
        if (Ntk_NodeTestIsLatch(fanoutNode))
          fprintf(vis_stdout, "\t(latch)");
      }
    }
#else
    assert (nodeMvf == NIL(Mvf_Function_t)) ;
#endif
  }

  PartitionCreateEdges(partition);
  array_free(rootNodesArray);
  st_free_table(nodeToMvfTable);
  st_free_table(topoNodeTable);
  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
}

#if 0
void
PartPartitionFrontierOld(Ntk_Network_t *network,
                      graph_t *partition,
                      lsList  rootList,
                      lsList  leaveList,
                      mdd_t   *careSet)
{
  Ntk_Node_t    *node;           /* Pointer to iterate over nodes */
  lsGen         gen;                /* To iterate over lists */
  vertex_t      *vertex;          /* Destination of the edge being added */
  char          *name;              /* Name of the node being processed */
  int           mddId;              /* Id of the node being processed */
  int           i;
  mdd_manager   *mddManager = PartPartitionReadMddManager(partition);
  /* nodeToMvfTable maps a node to the mvf in the form that is needed to build
     mvfs for the fanouts of the node.  I.e., a cutpoint node is mapped to an
     mdd for a new variable. */
  st_table *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
  st_table *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
  array_t *rootNodesArray;
  Mvf_Function_t *nodeMvf; 
  long bddSize;
  int sizeThreshold;
  lsList topologicalNodeList;
  lsGen lsgen;
  st_generator *stgen;
  char *flagValue =  Cmd_FlagReadByName("partition_threshold");
  if (flagValue == NIL(char)){
    sizeThreshold = 1000; /* the default value */
  }
  else {
    sizeThreshold = atoi(flagValue);
  }

  /* Put combinational inputs in the leafNodesTable. */
  if (leaveList == (lsList)0) {
    Ntk_NetworkForEachCombInput(network, gen, node) {
      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
    }
  } /* End of then */ 
  else {
    lsForEachItem(leaveList, gen, node) {
      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
    }
  } /* End of if-then-else */

  /*
   * For each leaf nodes, create a vertex in the partition, create the mvf, and
   * a mapping of name to vertex, and mddId to vertex.
   */
  st_foreach_item(leafNodesTable, stgen, &node, NULL){
    mddId = Ntk_NodeReadMddId(node);
    assert(mddId != NTK_UNASSIGNED_MDD_ID);
    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);
    st_insert(PartPartitionReadMddIdToVertex(partition), (char *)(long)mddId,
              (char *)vertex); 
    if (Ntk_NodeTestIsPseudoInput(node)){
      nodeMvf = NodeBuildPseudoInputMvf(node);
    }
    else {
      nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
    }
    st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf,
                                                             mddId);
  }

  
  /* Take the nodes in rootList as the roots */
  if (rootList == (lsList)0) {
    rootNodesArray = array_alloc(Ntk_Node_t *, 
                               Ntk_NetworkReadNumCombOutputs(network));
    i = 0;
    Ntk_NetworkForEachCombOutput(network, gen, node) {
      array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
    }
  } /* End of then */ 
  else {
    rootNodesArray = array_alloc(Ntk_Node_t *, lsLength(rootList));
    i = 0;
    lsForEachItem(rootList, gen, node) {
      array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
    }
  } /* End of if-then-else */

  

  /* Get an array of nodes sorted in topological order */
  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
                                                           rootNodesArray,
                                                           leafNodesTable);   
  
  st_free_table(leafNodesTable);
  

  /* Go through the topologicalNodeList
   * a. If the node is of combinational input type, continue.
   *
   * b. Otherwise, Build the Mdd for this node, in terms of the function of the
   *    fanin nodes in. If the Mdd size exceeds the threshold, create an Mdd ID
   *    for this node.
   */

  lsForEachItem(topologicalNodeList, lsgen, node){
    if (st_is_member(nodeToMvfTable, (char *)node)) continue;
    nodeMvf = NodeBuildMvf(node, nodeToMvfTable);
    bddSize = bdd_size_multiple(nodeMvf);
    if ((bddSize <= sizeThreshold) &&
        (Ntk_NodeTestIsCombOutput(node) == 0)){
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
      continue;
    }
    /* node either is a primary output, or has an mvf exceeding the
       threshold. */
    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    st_insert(PartPartitionReadNameToVertex(partition), name,
              (char *)vertex);
    if ((bddSize > sizeThreshold) &&
        (Ntk_NodeReadNumFanouts(node) != 0)){
      if ((mddId = Ntk_NodeReadMddId(node)) == -1){
        Ord_NetworkAssignMddIdForNode(network, node);
        mddId = Ntk_NodeReadMddId(node);
      }
      st_insert(nodeToMvfTable, (char *)node,
                (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
    }
    else {
      /* Small mvf, or no fanout */
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
    }
    mddId = Ntk_NodeReadMddId(node);
    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name,
                                                             nodeMvf, 
                                                             mddId);
    if (mddId != -1){
      st_insert(PartPartitionReadMddIdToVertex(partition),
                (char *)(long)mddId, (char *)vertex);
    }
  }/* for each member of topologicalNodeList */
  
  /*
   * Free the Mvfs in nodeToMvfTable not associated with vertices in the
   * partition.  The mvfs of inputs are always in the partition; hence,
   * their mvfs should always be preserved.  For outputs, we have to free
   * the mvf in nodeToMvfTable if the output is also a cutpoint, because in
   * this case the mvf in the partition vertex and the one in the
   * nodeToMvfTable are different.
   */

  lsForEachItem(topologicalNodeList, gen, node){ 
    if (!Ntk_NodeTestIsCombInput(node)){
      if(!Ntk_NodeTestIsCombOutput(node)){ 
        st_lookup(nodeToMvfTable, node, &nodeMvf); 
        assert(nodeMvf != NIL(Mvf_Function_t)); 
        Mvf_FunctionFree(nodeMvf);
      } else {
        Mvf_Function_t *vertexMvf;
        
        name =  Ntk_NodeReadName(node);
        vertex = Part_PartitionFindVertexByName(partition, name);
        st_lookup(nodeToMvfTable, node, &nodeMvf);
        vertexMvf = PartVertexReadFunction(vertex);
        assert(nodeMvf != NIL(Mvf_Function_t) &&
               vertexMvf != NIL(Mvf_Function_t));
        if(vertexMvf != nodeMvf){
          Mvf_FunctionFree(nodeMvf);
        }
      }
    }/* not input */
  }/* for each node */

  PartitionCreateEdges(partition);
  array_free(rootNodesArray);
  st_free_table(nodeToMvfTable);
  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
}
#endif

void
PartUpdateFrontier(Ntk_Network_t *network,
                   graph_t *partition,
                   lsList  rootList,
                   lsList  leaveList,
                   mdd_t   *careSet)
{
  Ntk_Node_t    *node;           /* Pointer to iterate over nodes */
  lsGen         gen;                /* To iterate over lists */
  vertex_t      *vertex;          /* Destination of the edge being added */
  char          *name;              /* Name of the node being processed */
  int           mddId;              /* Id of the node being processed */
  int           i, flag;
  mdd_manager   *mddManager = PartPartitionReadMddManager(partition);
  /* nodeToMvfTable maps a node to the mvf in the form that is needed to build
     mvfs for the fanouts of the node.  I.e., a cutpoint node is mapped to an
     mdd for a new variable. */
  st_table *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
  st_table *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
  array_t *rootNodesArray;
  Mvf_Function_t *nodeMvf; 
  long bddSize;
  int sizeThreshold;
  lsList topologicalNodeList;
  lsGen lsgen;
  st_generator *stgen;
  char *flagValue =  Cmd_FlagReadByName("partition_threshold");
  
  if (flagValue == NIL(char)){
    sizeThreshold = 1000; /* the default value */
  }
  else {
    sizeThreshold = atoi(flagValue);
  }

  /* Put combinational inputs in the leafNodesTable. */
  if (leaveList == (lsList)0) {
    Ntk_NetworkForEachCombInput(network, gen, node) {
      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
    }
  } /* End of then */ 
  else {
    lsForEachItem(leaveList, gen, node) {
      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
    }
  } /* End of if-then-else */

  /*
   * For each leaf nodes, create a vertex in the partition, create the mvf, and
   * a mapping of name to vertex, and mddId to vertex.
   * Notices that: if a vertex exists in the partition, use it instead of 
   * creating a new one.
   */
  st_foreach_item(leafNodesTable, stgen, &node, NULL){
    mddId = Ntk_NodeReadMddId(node);
    name  = Ntk_NodeReadName(node);
    assert(mddId != NTK_UNASSIGNED_MDD_ID);
    flag = st_lookup(PartPartitionReadNameToVertex(partition), 
                     name, &vertex);
    if (flag) {
      nodeMvf = ((PartVertexInfo_t *)(vertex->user_data))->functionality.mvf;
      st_insert(nodeToMvfTable, node, nodeMvf);
      /*
      name = Ntk_NodeReadName(node);
      fprintf(vis_stdout, "warning: node %s already in the partition\n",
              name);
      */
    }else {
      vertex = g_add_vertex(partition);
      st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);
      st_insert(PartPartitionReadMddIdToVertex(partition), (char *)(long)mddId,
                (char *)vertex); 
      if (Ntk_NodeTestIsPseudoInput(node)){
        nodeMvf = NodeBuildPseudoInputMvf(node);
      }else {
        nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
      }
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
      vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf,
                                                               mddId);
    }
  }
  
  /* Take the nodes in rootList as the roots */
  if (rootList == (lsList)0) {
    rootNodesArray = array_alloc(Ntk_Node_t *, 
                               Ntk_NetworkReadNumCombOutputs(network));
    i = 0;
    Ntk_NetworkForEachCombOutput(network, gen, node) {
      name = Ntk_NodeReadName(node);
      if ( !st_is_member(PartPartitionReadNameToVertex(partition), name) )
        array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
    }
  } /* End of then */ 
  else {
    rootNodesArray = array_alloc(Ntk_Node_t *, lsLength(rootList));
    i = 0;
    lsForEachItem(rootList, gen, node) {
      name = Ntk_NodeReadName(node);
      if ( !st_is_member(PartPartitionReadNameToVertex(partition), name) )
        array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
    }
  } /* End of if-then-else */

  

  /* Get an array of nodes sorted in topological order */
  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
                                                           rootNodesArray,
                                                           leafNodesTable);   
  
  st_free_table(leafNodesTable);
  

  /* Go through the topologicalNodeList
   * a. If the node is of combinational input type, continue.
   *
   * b. Otherwise, Build the Mdd for this node, in terms of the function of the
   *    fanin nodes in. If the Mdd size exceeds the threshold, create an Mdd ID
   *    for this node.
   */

  lsForEachItem(topologicalNodeList, lsgen, node){
    if (st_is_member(nodeToMvfTable, node)) continue;
    name = Ntk_NodeReadName(node);
    flag = st_lookup(PartPartitionReadNameToVertex(partition), 
                     name, &vertex);
    if (flag) {
      mddId = Ntk_NodeReadMddId(node);
      if (mddId != -1)
        st_insert(nodeToMvfTable, node,
                  (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
      else {
        nodeMvf = PartVertexReadFunction(vertex);
        st_insert(nodeToMvfTable, node, nodeMvf);
      }
      continue;
    }
    nodeMvf = NodeBuildMvf(node, nodeToMvfTable);
    bddSize = bdd_size_multiple(nodeMvf);
    if ((bddSize <= sizeThreshold) &&
        (Ntk_NodeTestIsCombOutput(node) == 0)){
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
      continue;
    }
    /* node either is a primary output, or has an mvf exceeding the
       threshold. */
    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    st_insert(PartPartitionReadNameToVertex(partition), name,
              (char *)vertex);
    if ((bddSize > sizeThreshold) &&
        (Ntk_NodeReadNumFanouts(node) != 0)){
      if ((mddId = Ntk_NodeReadMddId(node)) == -1){
        Ord_NetworkAssignMddIdForNode(network, node);
        mddId = Ntk_NodeReadMddId(node);
      }
      st_insert(nodeToMvfTable, (char *)node,
                (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
    }
    else {
      /* Small mvf, or no fanout */
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
    }
    mddId = Ntk_NodeReadMddId(node);
    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name,
                                                             nodeMvf, 
                                                             mddId);
    if (mddId != -1){
      st_insert(PartPartitionReadMddIdToVertex(partition),
                (char *)(long)mddId, (char *)vertex);
    }
  }/* for each member of topologicalNodeList */
  
  /*
   * Free the Mvfs in nodeToMvfTable not associated with vertices in the
   * partition.  The mvfs of inputs are always in the partition; hence,
   * their mvfs should always be preserved.  For outputs, we have to free
   * the mvf in nodeToMvfTable if the output is also a cutpoint, because in
   * this case the mvf in the partition vertex and the one in the
   * nodeToMvfTable are different.
   */

  lsForEachItem(topologicalNodeList, gen, node){ 
    if (!Ntk_NodeTestIsCombInput(node)){
      if(!Ntk_NodeTestIsCombOutput(node)){ 
        st_lookup(nodeToMvfTable, node, &nodeMvf); 
        assert(nodeMvf != NIL(Mvf_Function_t)); 
        Mvf_FunctionFree(nodeMvf);
      } else {
        Mvf_Function_t *vertexMvf;
        
        name =  Ntk_NodeReadName(node);
        vertex = Part_PartitionFindVertexByName(partition, name);
        st_lookup(nodeToMvfTable, node, &nodeMvf);
        vertexMvf = PartVertexReadFunction(vertex);
        assert(nodeMvf != NIL(Mvf_Function_t) &&
               vertexMvf != NIL(Mvf_Function_t));
        if(vertexMvf != nodeMvf){
          Mvf_FunctionFree(nodeMvf);
        }
      }
    }/* not input */
  }/* for each node */

  PartitionCreateEdges(partition);
  array_free(rootNodesArray);
  st_free_table(nodeToMvfTable);
  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
}

void
PartInsertBnvs(
  Ntk_Network_t *network,
  st_table *coiLatchTable,
  st_table *coiBnvTable)
{
  mdd_manager    *mddManager = Ntk_NetworkReadMddManager(network);
  st_table       *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
  st_table       *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
  lsList         topologicalNodeList;
  st_table       *topoNodeTable;
  array_t        *rootNodesArray;
  Ntk_Node_t     *fanoutNode, *node;
  Mvf_Function_t *nodeMvf; 
  long           bddSize, sizeThreshold, fanoutNumber, mddId;
  int            i;
  lsGen          lsgen;
  st_generator   *stgen;
  char           *flagValue;

  flagValue =  Cmd_FlagReadByName("partition_threshold");
  if (flagValue == NIL(char)){
    sizeThreshold = 1000; /* the default value */
  }
  else {
    sizeThreshold = atoi(flagValue);
  }

  /* Put latch data inputs in the rootNodesArray */
  rootNodesArray = array_alloc(Ntk_Node_t *, 0);
  st_foreach_item(coiLatchTable, stgen, &node, NULL) {
    array_insert_last(Ntk_Node_t *, rootNodesArray, 
                      Ntk_LatchReadDataInput(node));
    array_insert_last(Ntk_Node_t *, rootNodesArray, 
                      Ntk_LatchReadInitialInput(node));
  }

  /* Put combinational inputs, as well as the existing coiBnvs, in the
   * leafNodesTable. */
  Ntk_NetworkForEachCombInput(network, lsgen, node) {
    st_insert(leafNodesTable, node, (char *) (long) (-1) );
  }
  st_foreach_item(coiBnvTable, stgen, &node, NULL) {
    st_insert(leafNodesTable, node, (char *) (long) (-1) );
  }
  
  /* Get an array of nodes sorted in topological order */
  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
                                                           rootNodesArray,
                                                           leafNodesTable);   

  /* For each node, compute the number of fanouts */
  topoNodeTable = st_init_table(st_ptrcmp, st_ptrhash);
  lsForEachItem(topologicalNodeList, lsgen, node){
    st_insert(topoNodeTable, (char *)node, NIL(char));
  }
  lsForEachItem(topologicalNodeList, lsgen, node){
    fanoutNumber = 0;
    Ntk_NodeForEachFanout(node, i, fanoutNode) {
      if (st_is_member(topoNodeTable, (char *)fanoutNode) &&
          !st_is_member(leafNodesTable, (char *)fanoutNode) )
        fanoutNumber++;
    }
    st_insert(topoNodeTable, (char *)node, (char *)fanoutNumber);
  }

  /* assign mddIds to latches if necessary */
  /* chao: this may be too slow! */
  /* chao: this order may not be as good as static_order */
  lsForEachItem(topologicalNodeList, lsgen, node){
    if (Ntk_NodeTestIsInput(node)) {
      Ord_NetworkAssignMddIdForNode(network, node);
    }else if (Ntk_NodeTestIsLatch(node)) {
      Ord_NetworkAssignMddIdForNode(network, node);
      Ord_NetworkAssignMddIdForNode(network, Ntk_NodeReadShadow(node));
    }
  }
  st_foreach_item(coiLatchTable, stgen, &node, NULL) {
    Ord_NetworkAssignMddIdForNode(network, node);
    Ord_NetworkAssignMddIdForNode(network, Ntk_NodeReadShadow(node));
  }

  /* create nodeMvf for leaf nodes */
  st_foreach_item(leafNodesTable, stgen, &node, NULL) {
    if (!st_lookup(topoNodeTable, node, &fanoutNumber)) {
      continue;
    }
    mddId = Ntk_NodeReadMddId(node);
    assert(mddId != NTK_UNASSIGNED_MDD_ID);

    if (Ntk_NodeTestIsPseudoInput(node)){
      nodeMvf = NodeBuildPseudoInputMvf(node);
    }
    else {
      nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
    }

    if (fanoutNumber <= 0) {
      Mvf_FunctionFree(nodeMvf);
      st_insert(nodeToMvfTable, (char *)node, NIL(char));
    }
    else
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
  }

  st_free_table(leafNodesTable);


  /* Go through the topologicalNodeList
   * a. If the node is of combinational input type, continue.
   *
   * b. Otherwise, Build the Mdd for this node, in terms of the function of the
   *    fanin nodes in. If the Mdd size exceeds the threshold, create an Mdd ID
   *    for this node.
   */
  lsForEachItem(topologicalNodeList, lsgen, node){
    if (st_is_member(nodeToMvfTable, node)) 
      continue;

    nodeMvf = NodeBuildMvf2(node, nodeToMvfTable, topoNodeTable);
    bddSize = bdd_size_multiple(nodeMvf);
    st_lookup(topoNodeTable, node, &fanoutNumber);

    if ((bddSize <= sizeThreshold) && !Ntk_NodeTestIsCombOutput(node)) {
      assert(fanoutNumber > 0);
      st_insert(nodeToMvfTable, node, nodeMvf);
      continue;
    }
    /* node either is a primary output, or has an mvf exceeding the
       threshold. */
    if ((bddSize > sizeThreshold) && fanoutNumber > 0) {
                                   /*(Ntk_NodeReadNumFanouts(node) != 0)) { */
      /* ADD A bnv !!! */
      st_insert(coiBnvTable, (char *)node, NIL(char));

      if ((mddId = Ntk_NodeReadMddId(node)) == -1){
        Ord_NetworkAssignMddIdForNode(network, node);
        mddId = Ntk_NodeReadMddId(node);
      }

      st_insert(nodeToMvfTable, (char *)node,
                (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
      Mvf_FunctionFree(nodeMvf);
    }else {
      if (fanoutNumber <= 0) {
        Mvf_FunctionFree(nodeMvf);
        st_insert(nodeToMvfTable, node, NIL(char));
      }
      else
        st_insert(nodeToMvfTable, node, (char *)nodeMvf);
    }

  }/* for each member of topologicalNodeList */
  
  /* sanity check */
  st_foreach_item(nodeToMvfTable, stgen, &node, &nodeMvf) {
#if 0
    if (nodeMvf != NIL(Mvf_Function_t)) {
      st_lookup(topoNodeTable, node, &fanoutNumber);
      fprintf(vis_stdout, "\nunclean node = %s, fanout# = %d",
              Ntk_NodeReadName(node), fanoutNumber);
    }
#else
    assert (nodeMvf == NIL(Mvf_Function_t));
#endif
  }

  array_free(rootNodesArray);
  st_free_table(nodeToMvfTable);
  st_free_table(topoNodeTable);
  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
}

void
PartPartitionWithExistingBnvs(
  Ntk_Network_t *network,
  graph_t *partition,
  st_table *coiBnvTable,
  st_table *absLatchTable,
  st_table *absBnvTable)
{
  mdd_manager    *mddManager = PartPartitionReadMddManager(partition);
  st_table       *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
  st_table       *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
  array_t        *rootNodesArray, *combNodesArray;
  lsList         topologicalNodeList;
  st_table       *topoNodeTable;
  Ntk_Node_t     *fanoutNode, *node;
  Mvf_Function_t *nodeMvf; 
  vertex_t       *vertex;         
  long           mddId, fanoutNumber;
  char           *name;           
  lsGen          lsgen;
  st_generator   *stgen;
  int            i;

  /* Put latch data inputs in the rootNodesArray */
  rootNodesArray = array_alloc(Ntk_Node_t *, 0);
  st_foreach_item(absLatchTable, stgen, &node, NULL) {
    array_insert_last(Ntk_Node_t *, rootNodesArray, 
                      Ntk_LatchReadDataInput(node));
    array_insert_last(Ntk_Node_t *, rootNodesArray, 
                      Ntk_LatchReadInitialInput(node));
  }

  /* Put also latch initial inputs in the rootNodesArray */
  combNodesArray = Ntk_NodeComputeTransitiveFaninNodes(network,
                                                       rootNodesArray,
                                                       TRUE, TRUE);
  arrayForEachItem(Ntk_Node_t *, combNodesArray, i, node) {
    if ( Ntk_NodeTestIsLatch(node) && 
         !st_is_member(absLatchTable, (char *)node) )
      array_insert_last(Ntk_Node_t *, rootNodesArray, 
                        Ntk_LatchReadInitialInput(node));
  }
  array_free(combNodesArray);


  /* Put combinational inputs in the leafNodesTable. */
  Ntk_NetworkForEachCombInput(network, lsgen, node) {
    st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
  }
  /* Put BNVs that are not in absBnvTable in the leafNodesTable */
  st_foreach_item(coiBnvTable, stgen, &node, NULL) {
    if (!st_is_member(absBnvTable, (char *)node))
      st_insert(leafNodesTable, node, (char *) (long) (-1) );
  }

  /* Get an array of nodes sorted in topological order  */
  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
                                                           rootNodesArray,
                                                           leafNodesTable);

  /* For each node, compute the number of fanouts */
  topoNodeTable = st_init_table(st_ptrcmp, st_ptrhash);
  lsForEachItem(topologicalNodeList, lsgen, node){
    st_insert(topoNodeTable, (char *)node, NIL(char));
  }
  lsForEachItem(topologicalNodeList, lsgen, node){
    fanoutNumber = 0;
    Ntk_NodeForEachFanout(node, i, fanoutNode) {
      if (st_is_member(topoNodeTable, (char *)fanoutNode) &&
          !st_is_member(leafNodesTable, (char *)fanoutNode))
        fanoutNumber++;
    }
    st_insert(topoNodeTable, (char *)node, (char *)fanoutNumber);
   }

  /* Create partition vertices for the leaves 
   */
  st_foreach_item(leafNodesTable, stgen, &node, NULL){
    if (!st_lookup(topoNodeTable, node, &fanoutNumber))
      continue;
    mddId = Ntk_NodeReadMddId(node);
    if (mddId == NTK_UNASSIGNED_MDD_ID) {
        /* it is a input sign under the fanin cone of the initialInput
         * of some invisible latches */
        assert(Ntk_NodeTestIsInput(node));
        Ord_NetworkAssignMddIdForNode(network, node);
        mddId = Ntk_NodeReadMddId(node);
    }
    /*assert(mddId != NTK_UNASSIGNED_MDD_ID);*/
    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);
    st_insert(PartPartitionReadMddIdToVertex(partition), (char *)(long)mddId,
              (char *)vertex); 
    if (Ntk_NodeTestIsPseudoInput(node)){
      nodeMvf = NodeBuildPseudoInputMvf(node);
    }
    else {
      nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
    }

    if (fanoutNumber <= 0) 
      st_insert(nodeToMvfTable, (char *)node, NIL(char));
    else
      st_insert(nodeToMvfTable, (char *)node, 
                (char *)Mvf_FunctionDuplicate(nodeMvf));

    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf,
                                                             mddId);
  }

  /* Go through the topologicalNodeList, and build Mdds for nodes in
   * the absBnvTable
   */
  lsForEachItem(topologicalNodeList, lsgen, node){
    if (st_is_member(nodeToMvfTable, (char *)node)) continue;

    nodeMvf = NodeBuildMvf2(node, nodeToMvfTable, topoNodeTable);

    if ( !st_is_member(absBnvTable,(char *)node) && 
         !Ntk_NodeTestIsCombOutput(node)) {
      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
      continue;  
    }
    
    /* node is either a primary output, or a boolean network var */
    vertex = g_add_vertex(partition);
    name  = Ntk_NodeReadName(node);
    st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);

    if (st_is_member(absBnvTable,node)) {
      /* ADD a bnv !!! */
      mddId = Ntk_NodeReadMddId(node);
      assert(mddId != -1);
      st_insert(nodeToMvfTable, node,
                (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
    }else {
      st_lookup(topoNodeTable, node, &fanoutNumber);
      if (fanoutNumber <= 0) 
        st_insert(nodeToMvfTable, node, NIL(char));
      else
        st_insert(nodeToMvfTable, node, 
                  (char *)Mvf_FunctionDuplicate(nodeMvf));
    }

    mddId = Ntk_NodeReadMddId(node);
    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf, 
                                                             mddId);
    if (mddId != -1){
      st_insert(PartPartitionReadMddIdToVertex(partition),
                (char *)(long)mddId, (char *)vertex);
    }
  }/* for each member of topologicalNodeList */

  /* sanity check */
  st_foreach_item(nodeToMvfTable, stgen, &node, &nodeMvf) {
#if 1
    if (nodeMvf != NIL(Mvf_Function_t)) {
      st_lookup(topoNodeTable, node, &fanoutNumber);
      fprintf(vis_stdout, "\nunclean node = %s, fanout# = %ld",
              Ntk_NodeReadName(node), fanoutNumber);
    }
#else
    assert(nodeMvf == NIL(Mvf_Function_t));
#endif
  }

  PartitionCreateEdges(partition);
  array_free(rootNodesArray);
  st_free_table(nodeToMvfTable);
  st_free_table(topoNodeTable);
  st_free_table(leafNodesTable);
  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
}


void
PartPrintPartition(graph_t *partition)
{
  vertex_t *vertex;
  lsList vertexList = g_get_vertices(partition);
  lsGen gen;
  st_table *vertexTable = st_init_table(st_ptrcmp, st_ptrhash);
  fprintf(vis_stdout,"******* Printing Partition *********\n");
  lsForEachItem(vertexList, gen, vertex){
    PrintPartitionRecursively(vertex,vertexTable,0);
  }
  fprintf(vis_stdout,"******* End Printing Partition *********\n");
  st_free_table(vertexTable);
}

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

static void
PartitionCreateEdges(graph_t *partition)
{
  lsList vertexList;
  lsGen gen;
  vertex_t *toVertex;
  edge_t *edge;

  /* this will be executed only when used inside PartitionUpdateFrontier */
  foreach_edge(partition, gen, edge) {
    g_delete_edge(edge, (void(*)(gGeneric))0);
  }

  vertexList = g_get_vertices(partition);

  lsForEachItem(vertexList, gen, toVertex) {
    st_table     *mddSupport; /* To store the support of the Mvf_Function */
    st_generator *stGen;      /* To iterate over the MddIds of the support */
    vertex_t     *fromVertex; /* Will hold the current vertex in the support */
    Mvf_Function_t *mddFunction;
    long          mddId;
    
    mddFunction = PartVertexReadFunction(toVertex);
    mddSupport = PartCreateFunctionSupportTable(mddFunction);
    st_foreach_item(mddSupport, stGen, &mddId, NULL) {
      st_lookup(PartPartitionReadMddIdToVertex(partition), (char *) mddId,
                &fromVertex);  
      /* 
       * Add the edge to the graph. Make sure a self loop is not added. The
       * self loop may be produced by a mdd that has in its support the same
       * variables that represent the mddId of the node.
       */
      if (fromVertex != toVertex) {
        g_add_edge(fromVertex, toVertex);
      }
    }
    st_free_table(mddSupport);
  } 
}

static Mvf_Function_t *
NodeBuildMvf(Ntk_Node_t * node, st_table * nodeToMvfTable)
{
  int i;
  Mvf_Function_t *resultMvf;
  Ntk_Node_t *faninNode;
  array_t *faninMvfs = array_alloc(Mvf_Function_t *,
                                            Ntk_NodeReadNumFanins(node));
  mdd_manager *mddMgr = Ntk_NetworkReadMddManager(Ntk_NodeReadNetwork(node)); 
  int columnIndex = Ntk_NodeReadOutputIndex(node);
  Tbl_Table_t *table = Ntk_NodeReadTable(node);
  
  Ntk_NodeForEachFanin(node, i, faninNode) {
    Mvf_Function_t *tmpMvf;
    st_lookup(nodeToMvfTable, faninNode, &tmpMvf); 
    assert(tmpMvf);
    array_insert(Mvf_Function_t *, faninMvfs, i, tmpMvf);
  }
  
  resultMvf = Tbl_TableBuildMvfFromFanins(table, columnIndex,
                                          faninMvfs, mddMgr);    
  
  /* Don't free the MVFs themselves, but just free the array. */
  array_free(faninMvfs);
  return resultMvf;
}
    
static Mvf_Function_t *
NodeBuildMvf2(
  Ntk_Node_t * node, 
  st_table * nodeToMvfTable,
  st_table * faninNumberTable)
{
  long faninNumber;
  int i;
  Mvf_Function_t *resultMvf;
  Ntk_Node_t *faninNode;
  array_t *faninMvfs = array_alloc(Mvf_Function_t *,
                                   Ntk_NodeReadNumFanins(node));
  mdd_manager *mddMgr = Ntk_NetworkReadMddManager(Ntk_NodeReadNetwork(node)); 
  int columnIndex = Ntk_NodeReadOutputIndex(node);
  Tbl_Table_t *table = Ntk_NodeReadTable(node);
  
  Ntk_NodeForEachFanin(node, i, faninNode) {
    Mvf_Function_t *tmpMvf;
    st_lookup(nodeToMvfTable, faninNode, &tmpMvf); 
    assert(tmpMvf);
    array_insert(Mvf_Function_t *, faninMvfs, i, tmpMvf);
  }
  
  resultMvf = Tbl_TableBuildMvfFromFanins(table, columnIndex,
                                          faninMvfs, mddMgr);    
  
  /* Don't free the MVFs themselves, but just free the array. */
  array_free(faninMvfs);

  /* if the fanin node is no longer useful, remove its Mvfs */
  Ntk_NodeForEachFanin(node, i, faninNode) {
    st_lookup(faninNumberTable, faninNode, &faninNumber);
    assert(faninNumber > 0);
    faninNumber--;
    st_insert(faninNumberTable, faninNode, (char *)faninNumber);

    if (faninNumber <= 0) {
      Mvf_Function_t *tmpMvf;
      st_lookup(nodeToMvfTable, faninNode, &tmpMvf); 
      Mvf_FunctionFree(tmpMvf);
      st_insert(nodeToMvfTable, faninNode, NIL(char));
    }
  }

  return resultMvf;
}
    
      

static Mvf_Function_t *
NodeBuildPseudoInputMvf(
  Ntk_Node_t * node)
{
  mdd_manager  *mddMgr = Ntk_NetworkReadMddManager(Ntk_NodeReadNetwork(node));
  int          mddId = Ntk_NodeReadMddId( node );
  int          columnIndex = Ntk_NodeReadOutputIndex( node );
  Tbl_Table_t  *table = Ntk_NodeReadTable( node );
  Mvf_Function_t *mvf = Tbl_TableBuildNonDetConstantMvf(table, columnIndex,
                                                        mddId, mddMgr);

  mdd_t *vMdd, *tMdd, *rMdd;
  int lIndex, needProcess, i;

  rMdd = mdd_zero(mddMgr);
  needProcess = 0;
  lIndex = 0;
  for(i=0; i<mvf->num; i++) {
    vMdd = array_fetch(mdd_t *, mvf, i);
    if(mdd_equal(vMdd, rMdd)) {
      needProcess = 1;
    }
    else {
      lIndex = i;
    }
  }
  if(needProcess) {
    for(i=0; i<lIndex; i++) {
      vMdd = array_fetch(mdd_t *, mvf, i);
      tMdd = mdd_or(vMdd, rMdd, 1, 1);
      mdd_free(rMdd);
      rMdd = tMdd;
    }
    vMdd = array_fetch(mdd_t *, mvf, lIndex);
    mdd_free(vMdd);
    tMdd = mdd_not(rMdd);
    mdd_free(rMdd);
    array_insert(mdd_t *, mvf, lIndex, tMdd);
  }
  else {
    mdd_free(rMdd);
  }

  return mvf;
}


static void
PrintPartitionRecursively(vertex_t *vertex, st_table *vertexTable, int
                          indent)
{
  int i;
  lsList faninEdges;
  lsGen gen;
  vertex_t *faninVertex;
  edge_t *faninEdge;
  
  if (st_is_member(vertexTable, (char *)vertex)) return;
  st_insert(vertexTable, (char *)vertex, NIL(char));
  for(i=0; i<= indent; i++) fprintf(vis_stdout," ");
  fprintf(vis_stdout,"%s %d\n", Part_VertexReadName(vertex),
          Part_VertexReadMddId(vertex)); 
  faninEdges = g_get_in_edges(vertex);
  if (lsLength(faninEdges) == 0) return;
  lsForEachItem(faninEdges, gen, faninEdge){
    faninVertex = g_e_source(faninEdge);
    PrintPartitionRecursively(faninVertex, vertexTable,indent+2);
  }
}