source: vis_dev/vis-2.3/src/ntk/ntkFlt.c @ 23

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

  FileName    [ntkFlt.c]

  PackageName [ntk]

  Synopsis    [Routines for creating a network from a hierarchy manager.]

  Author      [Adnan Aziz, Tom Shiple]

  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
  All rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.

  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

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

#include "ntkInt.h"

static char rcsid[] UNUSED = "$Id: ntkFlt.c,v 1.13 2009/04/11 22:17:58 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
#define MAX_NUMBER_BDD_VARS 500


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


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

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

static void NetworkBuildFormalToActualTableRecursively(Ntk_Network_t *network, Hrc_Node_t *hrcNode);
static void NetworkCreateNodesRecursively(Ntk_Network_t *network, Hrc_Node_t *hrcNode);
static void NodeCreateAsNecessary(Ntk_Network_t *network, char *nodeName, Var_Variable_t *var);
static boolean NetworkDeclareNodesRecursively(Ntk_Network_t *network, Hrc_Node_t *hrcNode, boolean buildMvfs, mdd_manager **mddMgr);
static array_t * LocalArrayJoin(array_t *array1, array_t *array2);
static array_t * TableCreateFormalInputNameArray(Tbl_Table_t *table, char *namePrefix);
static void NameArrayFree(array_t *nameArray);
static boolean NetworkAbstractNodes(Ntk_Network_t *network, lsList abstractedNames);
static boolean NodeDeclareWithTable(Ntk_Node_t *node, Tbl_Table_t *table, int outIndex, char *path, boolean buildMvfs, mdd_manager *mddMgr);
static void NetworkDeclareIONodes(Ntk_Network_t *network, Hrc_Node_t *hrcNode);
static void NetworkDeclareLatches(Ntk_Network_t *network, Hrc_Node_t *hrcNode);
static void MddManagerResetIfNecessary(mdd_manager **mddMgr);
static Mvf_Function_t * LocalMvfFunctionForTable(Tbl_Table_t *table, int outIndex, mdd_manager *mddMgr, array_t *varMap, int *offset);

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


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

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

  Synopsis [Builds a flat description of a subtree of hierarchy manager.]

  Description [Builds a flat description of a subtree of a hierarchy manager.
  The flattened names of variables are taken as those hierarchical names where
  the variables are defined.  The names are relative to the "current" node
  of the hierarchy manager, which can be set by calling
  Hrc_ManagerSetCurrentNode() first.  Nodes are created even for unused
  variables (i.e. variables that don't fanout to anything.)<p>

  AbstractedNames is a list of char*.  If the list is not NULL, then this list
  is interpreted as a list of variables to abstract.  If a given name in the
  list does not correspond to the hierarchical name of a node in the network,
  then NULL is returned, and an error message is written to error_string.
  Otherwise, a new primary input is created to drive the net identified by the
  variable name.  See the documentation for the command flatten_hierarchy for
  more information.<p>

  The verification routines assume deterministic and completely specified
  tables. If a table is found that is locally non-deterministic or incompletely
  specified, then a message is written to vis_stderr, and a NIL network is
  returned (the non-deterministic test is not performed on non-deterministic
  constant tables).  This test can be bypassed (in order to save time) by
  passing FALSE for buildMvfs. Note that this should be done with extreme
  caution, because bad tables could inadvertantly be allowed through and
  invalidate verification results obtained downstream.<p>

  Also, if a table has no inputs and more than 1 output, and its output space
  is not complete (i.e. the outputs are correlated), then the table is
  declared a "relation", and NIL is returned.]

  SideEffects []

  Comment [Proceeds in 3 phases: 1) builds a map from formals to actuals, 2)
  adds a node for each actual (i.e. for each node that will appear in the
  network) and 3) sets the types (and tables, where appropriate) for each
  node.]

  SeeAlso [Ntk_NetworkAlloc NetworkBuildFormalToActualTableRecursively
  NetworkCreateNodesRecursively NetworkDeclareNodesRecursively]

******************************************************************************/
Ntk_Network_t *
Ntk_HrcNodeConvertToNetwork(
  Hrc_Node_t *hrcNode,
  boolean     buildMvfs,
  lsList abstractedNames)
{
  mdd_manager   *mddMgr;
  boolean        status1     = TRUE;
  boolean        status2     = TRUE;
  char          *hrcNodeName = Hrc_NodeReadInstanceName(hrcNode);
  Ntk_Network_t *network     = Ntk_NetworkAlloc(hrcNodeName);

  NetworkBuildFormalToActualTableRecursively(network, hrcNode);
  NetworkCreateNodesRecursively(network, hrcNode);

  /*
   * The MDD manager is for building temporary MDDs.  For robustness, enable
   * reordering.
   */
  mddMgr = mdd_init_empty();
  bdd_dynamic_reordering(mddMgr, BDD_REORDER_SIFT, BDD_REORDER_VERBOSITY_DEFAULT);
  status1 = NetworkDeclareNodesRecursively(network, hrcNode, buildMvfs, &mddMgr);
  mdd_quit(mddMgr);

  if (abstractedNames != (lsList) NULL) {
    status2 = NetworkAbstractNodes(network, abstractedNames);
  }

  if (!(status1 && status2)) {
    Ntk_NetworkFree(network);
    return NIL(Ntk_Network_t);
  }
  else {
    return network;
  }
}


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


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


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

  Synopsis    [Creates mapping from formal names to actual names.]

  Description [Loads the formal-to-actual table of network.  For each formal
  variable name in hrcNode, maps it to a unique actual variable name.  The map
  is many-to-one.  The rule is that a formal is resolved to the actual as high
  in the hierarchy as possible.  Proceeds recursively by examining
  subcircuits. Note that only formals are in the domain of the map. Also, care
  has to be taken when looking at net in parent since they may also be
  formals.]

  SideEffects []

******************************************************************************/
static void
NetworkBuildFormalToActualTableRecursively(
  Ntk_Network_t *network,
  Hrc_Node_t *hrcNode)
{
  st_generator *stGen;
  char         *childName;
  Hrc_Node_t   *childHrcNode;

  /*
   * For each child of the current hnode, process its I/O variables, and
   * then recurse on its children.
   */
  Hrc_NodeForEachChild(hrcNode, stGen, childName, childHrcNode) {

    int i;
    array_t *childFormalInputs  = Hrc_NodeReadFormalInputs(childHrcNode);
    array_t *childFormalOutputs = Hrc_NodeReadFormalOutputs(childHrcNode);
    array_t *childFormalIoArray = LocalArrayJoin(childFormalInputs, childFormalOutputs);

    array_t *childActualInputs  = Hrc_NodeReadActualInputs(childHrcNode);
    array_t *childActualOutputs = Hrc_NodeReadActualOutputs(childHrcNode);
    array_t *childActualIoArray = LocalArrayJoin(childActualInputs, childActualOutputs);


    /*
     * For each I/O variable, construct the appropriate hierarchical name for
     * the variable in childHrcNode (formalName) and the variable in the
     * hrcNode (actualName).  If actualName already has a corresponding
     * actual, then use that, otherwise use actualName as is.  Add
     * correspondence from formal (formalName) to actual (actualName).
     */
    for(i = 0 ; i < array_n(childActualIoArray) ; i++) {
      Var_Variable_t *actualVar = array_fetch(Var_Variable_t *, childActualIoArray, i);
      Var_Variable_t *formalVar = array_fetch(Var_Variable_t *, childFormalIoArray, i);

      char *nodeName   = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
      /* Special case the situation where hrcNode is current node. */
      char *actualName = (strcmp(nodeName, ""))
          ? util_strcat3(nodeName, ".",
                         Var_VariableReadName(actualVar))
          : util_strsav(Var_VariableReadName(actualVar));

      char *childNodeName = Hrc_NodeFindHierarchicalName(childHrcNode, TRUE);
      char *formalName = util_strcat3(childNodeName, ".",
                                      Var_VariableReadName(formalVar));

      /*
       * It is correct to call this function with actualName.  We want to
       * check if actualVar is itself a formalVar one level up.
       */
      char *tempName   = Ntk_NetworkReadActualNameFromFormalName(network, actualName);

      FREE(nodeName);
      FREE(childNodeName);

      /*
       * (tempName != NIL) => this net is a formal in hrcNode
       */
      if (tempName != NIL(char)) {
        FREE(actualName);
        actualName = tempName;
      }

      /*
       * Ntk_NetworkInsertFormalNameToActualName makes copies of the strings
       */
      Ntk_NetworkInsertFormalNameToActualName(network, formalName, actualName);

      if (tempName == NIL(char)) {
        FREE(actualName);
      }
      FREE(formalName);
    }
    array_free(childFormalIoArray);
    array_free(childActualIoArray);

    /*
     * Recurse.
     */
    NetworkBuildFormalToActualTableRecursively(network, childHrcNode);
  }
}


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

  Synopsis    [Creates placeholders for all the nodes in the network.]

  Description [Working top-down, creates placeholders for all the nodes in the
  network.  After this function is executed, each node will have a name and
  Var_Variable_t, but nothing else.  Note that nodes are created for reset
  logic; they are given the name of their corresponding latch, suffixed by
  $INIT.]

  SideEffects []

  SeeAlso     [NodeCreateAsNecessary]

******************************************************************************/
static void
NetworkCreateNodesRecursively(
  Ntk_Network_t *network,
  Hrc_Node_t    *hrcNode)
{
  st_generator   *stGen;
  Var_Variable_t *var;
  Hrc_Latch_t    *latch;
  char           *varName;
  char           *latchName;
  char           *childName;
  Hrc_Node_t     *childHrcNode;
  char           *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
  char           *separator = (char *) ((strcmp(path, "")) ? "." : "");

  /*
   * The separator is used to handle the special case when hrcNode is the
   * current node in the hierarchy.  If it is, we don't want a "." before the
   * variable names.
   */

  Hrc_NodeForEachVariable(hrcNode, stGen, varName, var) {
    char *nodeName = util_strcat3(path, separator, varName);
    NodeCreateAsNecessary(network, nodeName, var);
    FREE(nodeName);
  }

  /*
   * Variable for reset is the same as for present state.  Hence, iterating
   * through the list of variables gets us just the present state.  Therefore,
   * we need to special case the reset (or init) nodes.
   */
  Hrc_NodeForEachLatch(hrcNode, stGen, latchName, latch) {
    char *partialNodeName = util_strcat3(path, separator, latchName);
    char *nodeName        = util_strcat3(partialNodeName, "$INIT", "");

    FREE(partialNodeName);
    NodeCreateAsNecessary(network, nodeName, Hrc_LatchReadOutput(latch));
    FREE(nodeName);
  }
  FREE(path);

  /* Recurse. */
  Hrc_NodeForEachChild(hrcNode, stGen, childName, childHrcNode) {
    NetworkCreateNodesRecursively(network, childHrcNode);
  }
}


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

  Synopsis [Creates a node with a given name, if one doesn't already exist.]

  Description [If a node with nodeName already exists in the network, then
  does nothing.  Otherwise, creates a new node in the network with nodeName
  and variable.]

  SideEffects []

******************************************************************************/
static void
NodeCreateAsNecessary(
  Ntk_Network_t  *network,
  char           *nodeName,
  Var_Variable_t *var)
{
  if (Ntk_NetworkFindNodeByName(network, nodeName)) {
    return;
  }

  (void) Ntk_NodeCreateInNetwork(network, nodeName, var);
}


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

  Synopsis    [Add functionality to the Ntk_Node_t's for this Hrc_Node_t.]

  Description [Add functionality to the Ntk_Node_t's for this Hrc_Node_t.
  Proceeds in 3 stages: 1) sets PI's and PO's; this is achieved by looking at
  PI/POs which are not formals, 2) adds tables to combinational logic, taking
  care to get the non-deterministic/deterministic constants right, 3) iterates
  over latches, adding type latch to nodes which have a name correspoding to
  this latch's ps name, and declaring the initialization logic for the
  latch.<p>

  If a table is found that is non-deterministic or incompletely specified,
  then a message is written to vis_stderr, and FALSE is returned (the
  non-deterministic test is not performed on non-deterministic constant
  tables).  Also, if a table has no inputs and more than 1 output and its
  output space is not complete, then it's declared a "relation", and FALSE is
  returned.  However, even if FALSE is returned, the nodes are still
  declared.<p>

  The non-deterministic or incompletely specified tests can be bypassed by
  passing FALSE for buildMvfs. See Ntk_HrcNodeConvertToNetwork for more info.]

  SideEffects []

******************************************************************************/
static boolean
NetworkDeclareNodesRecursively(
  Ntk_Network_t *network,
  Hrc_Node_t    *hrcNode,
  boolean        buildMvfs,
  mdd_manager  **mddMgr)
{
  int i;
  st_generator   *stGen;
  char           *latchName;
  Var_Variable_t *var;
  Hrc_Latch_t    *latch;
  Tbl_Table_t    *table;
  char           *childName;
  Hrc_Node_t     *childHrcNode;
  boolean         result = TRUE;
  char           *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
  char           *separator = (char *) ((strcmp(path, "")) ? "." : "");

  /*
   * First declare the network's PI/PO nodes.
   */
  NetworkDeclareIONodes(network, hrcNode);

  /*
   * Next, declare those nodes whose function is represented by a table.  Note
   * that his iterator does not pick up those tables that define the
   * initialization logic of latches.
   */
  Hrc_NodeForEachNameTable(hrcNode, i, table) {
    int index;
    Tbl_TableForEachOutputVar(table, index, var) {
      boolean     status;
      char       *fullVarName = util_strcat3(path, separator,
                                               Var_VariableReadName(var));
      Ntk_Node_t *node        = Ntk_NetworkFindNodeByName(network, fullVarName);

      FREE(fullVarName);
      status = NodeDeclareWithTable(node, table, index, path, buildMvfs, *mddMgr);
      if (!status) {
        result = FALSE;
      }
      MddManagerResetIfNecessary(mddMgr);
    }
  }

  /*
   * Declare each latch and its corresponding next state shadow node.
   */
  NetworkDeclareLatches(network, hrcNode);

  /*
   * Declare the "initial" node corresponding to each latch.
   */
  Hrc_NodeForEachLatch(hrcNode, stGen, latchName, latch) {
    int index;

    table = Hrc_LatchReadResetTable(latch);

    /*
     * There is only one output variable (the 0th output) for any table
     * defining the initial function of a latch, but we use an iterator to get
     * the variable for convenience.
     */
    Tbl_TableForEachOutputVar(table, index, var) {
      boolean      status;
      char        *fullVarName = util_strcat3(path, separator, Var_VariableReadName(var));
      char        *initName    = util_strcat3(fullVarName, "$INIT", "");
      Ntk_Node_t  *node        = Ntk_NetworkFindNodeByName(network, initName);

      /*
       * Since the output of this table corresponds to a latch PS, can get name
       * of the initial node by attaching $INIT.
       */
      FREE(fullVarName);
      FREE(initName);

      status = NodeDeclareWithTable(node, table, index, path, buildMvfs, *mddMgr);
      if (!status) {
        result = FALSE;
      }
      MddManagerResetIfNecessary(mddMgr);
    }
  }
  FREE(path);

  /* Recurse. */
  Hrc_NodeForEachChild(hrcNode, stGen, childName, childHrcNode) {
    boolean status = NetworkDeclareNodesRecursively(network, childHrcNode,
                                                    buildMvfs, mddMgr);
    if (!status) {
      result = FALSE;
    }
  }

  return result;
}


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

  Synopsis    [Creates a new array consisting of array1 and array2.]

  Description [Returns a new array which consists of the elements of array 1
  followed by the elements of array2.]

  Comment     [It is suspected that the array_join from the array package is
  buggy when one of the arrays has 0 length.  Hence, we defined our own.]

  SideEffects []

******************************************************************************/
static array_t *
LocalArrayJoin(
  array_t *array1,
  array_t *array2)
{
  if (array_n(array1) == 0) {
    return (array_dup(array2));
  }
  else if (array_n(array2) == 0) {
    return (array_dup(array1));
  }
  else {
    return (array_join(array1, array2));
  }
}


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

  Synopsis    [Creates an array of table input names.]

  Description [Creates an array of table input names.  For the ith input of
  table, the string "namePrefix.variableName_i" is placed in the ith position
  of the returned array, where variableName_i is the name of the variable
  corresponding to the ith input.  (If namePrefix is "", then just
  "variableName_i" is used.)  It is the responsiblity of the caller to free
  the strings in the returned array.]

  SideEffects []

  SeeAlso     [NameArrayFree]

******************************************************************************/
static array_t *
TableCreateFormalInputNameArray(
  Tbl_Table_t *table,
  char        *namePrefix)
{
  int             index;
  array_t        *nameArray;
  Var_Variable_t *var;
  char           *separator = (char *) ((strcmp(namePrefix, "")) ? "." : "");

  /*
   * Allocate an array of length equal to the number of inputs of the table.
   * Then, for each input, add the full path name of the input to the array.
   */
  nameArray = array_alloc(char *, Tbl_TableReadNumInputs(table));
  Tbl_TableForEachInputVar(table, index, var) {
    char *inputFullName = util_strcat3(namePrefix, separator, Var_VariableReadName(var));
    array_insert(char *, nameArray, index, inputFullName);
  }

  return (nameArray);
}


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

  Synopsis    [Frees the strings in an array, and frees the array itself.]

  SideEffects []

  SeeAlso     [TableCreateFormalInputNameArray]

******************************************************************************/
static void
NameArrayFree(
  array_t *nameArray)
{
  int i;

  for (i = 0; i < array_n(nameArray); i++) {
    char *name = array_fetch(char *, nameArray, i);
    FREE(name);
  }
  array_free(nameArray);
}

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

  Synopsis    [Abstract each node named in abstractedNames.]

  Description [Abstract each node named in abstractedNames. A node x is
  abstracted by creating a single new primary input node, with the name x$ABS
  and with the same variable as x, which will fanout to every node the
  original node fanned out to. The old node will continue to exists as before
  but will have no fanouts after abstraction; it can still be referred to in
  CTL formulas, etc.]

  SideEffects []

******************************************************************************/
static boolean
NetworkAbstractNodes(
  Ntk_Network_t *network,
  lsList abstractedNames)
{
  char  *name;
  lsGen gen;

  /*
   * For each abstracted name, cut the corresponding net, and introduce a new
   * node.
   */
  lsForEachItem(abstractedNames, gen, name) {
    Var_Variable_t *var;
    Ntk_Node_t     *abstractNode;
    array_t        *abstractNodeFanouts;
    int             i;
    Ntk_Node_t     *fanout;
    char           *abstractNodeName;
    Ntk_Node_t     *node = Ntk_NetworkFindNodeByName(network, name);

    /* Make sure the name corresponds to a node in the network. */
    if (node == NIL(Ntk_Node_t)) {
      error_append("Could not find node corresponding to name: ");
      error_append(name);
      error_append("\n");
      return FALSE;
    }

    /* Create the new node in the network as a primary input. */
    abstractNodeName = util_strcat3(name, "$ABS", "");
    var = Ntk_NodeReadVariable(node);
    abstractNode = Ntk_NodeCreateInNetwork(network, abstractNodeName, var);
    FREE(abstractNodeName);
    Ntk_NodeDeclareAsPrimaryInput(abstractNode);

    /*
     * For each fanout y of the node x being abstracted, replace x in y's
     * fanin list by the new node, and add y to the fanout list of the new
     * node.
     */
    abstractNodeFanouts = Ntk_NodeReadFanouts(abstractNode);
    Ntk_NodeForEachFanout(node, i, fanout) {
      int      index        = Ntk_NodeReadFaninIndex(fanout, node);
      array_t *fanoutFanins = Ntk_NodeReadFanins(fanout);

      array_insert(Ntk_Node_t *, fanoutFanins, index, abstractNode);
      array_insert_last(Ntk_Node_t *, abstractNodeFanouts, fanout);
    }

    /*
     * Replace the fanout array of the node being abstracted with an empty
     * array.
     */
    array_free(node->fanouts);
    node->fanouts = array_alloc(Ntk_Node_t *, 0);
  }

  return TRUE;
}


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

  Synopsis    [Declare a node with a table, and run some tests.]

  Description [Declare a node with a table, and run some tests.  Creates the
  MVF for the output of table denoted by outIndex, in terms of the table
  inputs (new MDD variables are created).  This MVF is created within mddMgr,
  and freed at the end of the function.  The MVF is checked to see if it
  represents nondeterministic or incompletely specified behavior.  If it does,
  a message is written to vis_stderr, and FALSE is returned.  Also, if a table
  has no inputs and more than 1 output and its output space is not complete,
  then it's declared a "relation", and FALSE is returned.<p>

  If the table passes these tests, then a reduced table is built for this
  table output, consisting of just that output and the input columns in the
  support of that output.  The node is then declared as a "pseudo-input" if
  the table represents a nondeterministic constant, or a "combinational" node
  otherwise.<p>

  Building the MVF, performing the tests, and building the reduced table, is
  bypassed if the input buildMvfs is FALSE.  Note that this should be done with
  extreme caution, because bad tables could inadvertantly be allowed through
  and invalidate verification results obtained downstream.]

  SideEffects []

******************************************************************************/
static boolean
NodeDeclareWithTable(
  Ntk_Node_t  *node,
  Tbl_Table_t *table,
  int          outIndex,
  char        *path,
  boolean      buildMvfs,
  mdd_manager *mddMgr)
{
  Tbl_Table_t *newTable;
  int          newOutIndex;
  boolean      result   = TRUE;
  char        *nodeName = Ntk_NodeReadName(node);

  /*
   * If table has no inputs and more than one output, and its output space is
   * not complete (i.e. not all output minterms are present, so the outputs
   * are correlated), then declare the table a relation.
   */
  if ((Tbl_TableReadNumInputs(table) == 0)
      && (Tbl_TableReadNumOutputs(table) > 1)) {
    if (!Tbl_TableTestIsOutputSpaceComplete(table, mddMgr)) {
      (void) fprintf(vis_stderr, "Table %s is a relation\n", nodeName);
      result = FALSE;
    }
  }

  if (!buildMvfs) {
    newTable = Tbl_TableSoftDup(table);
    newOutIndex = outIndex;
  }
  else {
    Mvf_Function_t *outMvf;
    int             offset;
    int             numInputs     = Tbl_TableReadNumInputs(table);
    array_t        *varMap        = array_alloc(int, numInputs);

    outMvf = LocalMvfFunctionForTable(table, outIndex, mddMgr,
                                      varMap, &offset);
    /*
     * If the function is not a non-deterministic constant, or it has some
     * inputs, then check that it is deterministic. Always check that it is
     * completely specified.
     */
    if ((numInputs > 0)
        || !Mvf_FunctionTestIsNonDeterministicConstant(outMvf)) {
      if (!Mvf_FunctionTestIsDeterministic(outMvf)) {
        (void) fprintf(vis_stderr, "Table %s is not deterministic\n", nodeName);
        result = FALSE;
      }
    }
    if (!Mvf_FunctionTestIsCompletelySpecified(outMvf)) {
      (void) fprintf(vis_stderr, "Table %s is not completely specified\n", nodeName);
      result = FALSE;
    }

    /*
     * Build the reduced table for the output corresponding to outIndex.  The
     * reduced table will have only one output column (column 0), and will have
     * only those input columns corresponding to the variables appearing in the
     * support of outMvf.
     */
    newTable = Tbl_TableCreateTrueSupportTableForOutput(table, outMvf, mddMgr,
                                                        offset, outIndex,
                                                        varMap);
    newOutIndex = 0;
    array_free(varMap);
    Mvf_FunctionFree(outMvf);
  }


  /*
   * Declare the node with the reduced table.
   */
  if (Tbl_TableTestIsNonDeterministicConstant(newTable, newOutIndex)) {
    Ntk_NodeDeclareAsPseudoInput(node, newTable, newOutIndex);
  }
  else {
    array_t *formalInputNameArray = TableCreateFormalInputNameArray(newTable, path);

    /* Ntk_NodeDeclareAsCombinational will test for constants. */
    Ntk_NodeDeclareAsCombinational(node, newTable, formalInputNameArray, newOutIndex);
    NameArrayFree(formalInputNameArray);
  }

  return result;
}


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

  Synopsis    [Declares the primary inputs and outputs of the network.]

  Description [Declares the primary inputs and outputs of the network. Does
  this by iterating over the variables of the hrcNode.  Any variable it finds
  that doesn't have a corresponding actual name in the network's corresponding
  formal-to-actual table is considered a primary IO.]

  SideEffects []

******************************************************************************/
static void
NetworkDeclareIONodes(
  Ntk_Network_t *network,
  Hrc_Node_t    *hrcNode)
{
  st_generator   *stGen;
  char           *varName;
  Var_Variable_t *var;
  char           *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
  char           *separator = (char *) ((strcmp(path, "")) ? "." : "");

  Hrc_NodeForEachVariable(hrcNode, stGen, varName, var) {
    if (Var_VariableTestIsPO(var) || Var_VariableTestIsPI(var)) {
      char *fullVarName = util_strcat3(path, separator, Var_VariableReadName(var));
      char *tmpName     = Ntk_NetworkReadActualNameFromFormalName(network, fullVarName);

      /*
       * If tmpName == NIL, this must be a PI/PO of the top most node in the hierarchy of
       * nodes. Hence, this is a true input/output of the hierarchy.
       */
      if (tmpName == NIL(char)) {
        Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, fullVarName);
        if (Var_VariableTestIsPO(var)) {
          Ntk_NodeDeclareAsPrimaryOutput(node);
        }
        else {
          Ntk_NodeDeclareAsPrimaryInput(node);
        }
      }
      FREE(fullVarName);
    }
  }
  FREE(path);
}


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

  Synopsis    [Declares the latches of the network.]

  Description [Declares the latches of the network. Does this by iterating
  over the latches of the hrcNode.  For each latch, also creates and declares
  a corresponding next state shadow node.]

  SideEffects []

******************************************************************************/
static void
NetworkDeclareLatches(
  Ntk_Network_t *network,
  Hrc_Node_t    *hrcNode)
{
  st_generator   *stGen;
  char           *name;
  Hrc_Latch_t    *latch;
  char           *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE);
  char           *separator = (char *) ((strcmp(path, "")) ? "." : "");

  Hrc_NodeForEachLatch(hrcNode, stGen, name, latch) {
    char       *nextStateName;
    Ntk_Node_t *nextStateNode;
    char       *latchName = util_strcat3(path, separator,
                             Var_VariableReadName(Hrc_LatchReadOutput(latch)));
    char       *initName  = util_strcat3(latchName, "$INIT", "");
    char       *dataName  = util_strcat3(path, separator,
                             Var_VariableReadName(Hrc_LatchReadInput(latch)));
    Ntk_Node_t *latchNode = Ntk_NetworkFindNodeByName(network, latchName);

    FREE(latchName);
    Ntk_NodeDeclareAsLatch(latchNode, dataName, initName);
    FREE(initName);
    FREE(dataName);

    /*
     * Create the corresponding shadow next state node for the latch.  This holds
     * the next state variable.
     */
    nextStateName = util_strcat3(Ntk_NodeReadName(latchNode), "$NS", "");
    nextStateNode = Ntk_NodeCreateInNetwork(network, nextStateName,
                                            Hrc_LatchReadOutput(latch));
    FREE(nextStateName);
    Ntk_NodeDeclareAsShadow(nextStateNode, latchNode);
  }
  FREE(path);
}


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

  Synopsis    [Potentially quits mddMgr and starts a new one.]

  Description [Quits mddMgr if the number of binary variables exceeds
  MAX_NUMBER_BDD_VARS, and starts a new manager with no variables.
  Initializing an empty MDD manager is costly in some BDD packages, so we want
  to avoid doing it often (say, once per table).  On the other hand, we don't
  want the manager to have too many variables, because then reordering becomes
  expensive.]

  SideEffects []

******************************************************************************/
static void
MddManagerResetIfNecessary(
  mdd_manager **mddMgr)
{
  if (bdd_num_vars(*mddMgr) > MAX_NUMBER_BDD_VARS) {
    mdd_quit(*mddMgr);
    *mddMgr = mdd_init_empty();
    bdd_dynamic_reordering(*mddMgr, BDD_REORDER_SIFT, BDD_REORDER_VERBOSITY_DEFAULT);
  }
}


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

  Synopsis    [Builds the MVF of a table in terms of local variables.]

  Description [Builds the MVF of a table in terms of local variables.  Also
  computes the offset of the local variables in the MDD manager and builds
  a map from the input columns of the table to the MDD id's.  The offset is
  always 0 if the MDD manager is restarted.]

  SideEffects [varMap and offsetPtr are returned as side effects]

******************************************************************************/
static Mvf_Function_t *
LocalMvfFunctionForTable(
  Tbl_Table_t *table,
  int outIndex,
  mdd_manager *mddMgr,
  array_t *varMap,
  int *offsetPtr
  )
{
  Mvf_Function_t *outMvf;
  Var_Variable_t *var;
  int             colNum;
  int             offset;
  int             i;
  int             numInputs     = Tbl_TableReadNumInputs(table);
  array_t        *faninMvfArray = array_alloc(Mvf_Function_t *, numInputs);
  array_t        *mvarValues    = array_alloc(int, numInputs);
  st_table       *varTable      = st_init_table(st_ptrcmp,st_ptrhash);

  /* Create MDD variables for the table inputs.  If there are more inputs
   * tied to the sameVar_Variable_t, create just one MDD variable.  Record
   * the mapping from inputs to variable indices in varMap.
   */
  Tbl_TableForEachInputVar(table, colNum, var) {
    int index;
    if (st_lookup_int(varTable,var,&index)) {
      array_insert_last(int, varMap, index);
    } else {
      index = array_n(mvarValues);
      array_insert_last(int, varMap, index);
      st_insert(varTable, var, (char *) (long) index);
      array_insert_last(int, mvarValues, Var_VariableReadNumValues(var));
    }
  }
  st_free_table(varTable);

  /* Restarting the manager is optional.  The effect is to get rid of the
   * MDD variable information in the manager, without incurring the cost
   * of quitting and re-initializing the manager. */
  mdd_restart(mddMgr);
  offset = array_n(mdd_ret_mvar_list(mddMgr));  /* number of existing mvars */
  assert(offset == 0);
  mdd_create_variables(mddMgr, mvarValues, NIL(array_t), NIL(array_t));
  array_free(mvarValues);

  /*
   * Construct an MVF for each table input. The MVF for column i is the MVF
   * for MDD variable i.
   */
  for (i = 0; i < numInputs; i++) {
    int index = array_fetch(int, varMap, i);
    Mvf_Function_t *faninMvf = Mvf_FunctionCreateFromVariable(mddMgr, (index + offset));
    array_insert_last(Mvf_Function_t *, faninMvfArray, faninMvf);
  }

  /* Compute the MVF of the output indexed by outIndex. */
  outMvf = Tbl_TableBuildMvfFromFanins(table, outIndex, faninMvfArray, mddMgr);
  Mvf_FunctionArrayFree(faninMvfArray);

  *offsetPtr = offset;
  return outMvf;

} /* LocalMvfFunctionForTable */