src/ntk/ntkFlt.c

Go to the documentation of this file.

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


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

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

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


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


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


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


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


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


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


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

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


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


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


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


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


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