src/ntk/ntkNtk.c

Go to the documentation of this file.

#include "ntkInt.h"
#include "mdd.h"

static char rcsid[] UNUSED = "$Id: ntkNtk.c,v 1.23 2010/04/09 23:44:05 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/
typedef struct ApplInfoStruct {
  Ntk_ApplInfoFreeFn  freeFn;  /* application function to free data */
  void               *data;    /* application data */
} ApplInfo_t;


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

static char * NodeReadNameFromTable(Ntk_Node_t *node, st_table *name2ToName1);
static Tbl_Table_t * DuplicateTableAndVars(Ntk_Node_t *node, char *name);

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

char *
Ntk_NetworkReadName(
  Ntk_Network_t * network)
{
  return (network->name);
}


mdd_manager *
Ntk_NetworkReadMddManager(
  Ntk_Network_t * network)
{
  return (network->mddManager);
}


void
Ntk_NetworkSetMddManager(
  Ntk_Network_t  * network,
  mdd_manager * mddManager)
{
  network->mddManager = mddManager;
}

mAig_Manager_t *
Ntk_NetworkReadMAigManager(
  Ntk_Network_t * network)
{
  return (network->mAigManager);
}


void
Ntk_NetworkSetMAigManager(
  Ntk_Network_t * network,
  mAig_Manager_t * mAigManager)
{
  network->mAigManager = mAigManager;
}

mdd_manager *
Ntk_NetworkInitializeMddManager(
  Ntk_Network_t * network)
{
  network->mddManager = mdd_init_empty();

  return (network->mddManager);
}


bdd_reorder_type_t
Ntk_NetworkReadDynamicVarOrderingMethod(
  Ntk_Network_t * network)
{
  return (network->dynVarOrdMethod);
}


void
Ntk_NetworkSetDynamicVarOrderingMethod(
  Ntk_Network_t * network,
  bdd_reorder_type_t dynVarOrdMethod,
  bdd_reorder_verbosity_t verbosity)
{
  bdd_dynamic_reordering(network->mddManager, dynVarOrdMethod, verbosity);
  if (bdd_get_package_name() != CUDD) {
    if (dynVarOrdMethod == BDD_REORDER_SIFT ||
        dynVarOrdMethod == BDD_REORDER_WINDOW ||
        dynVarOrdMethod == BDD_REORDER_NONE) {
      network->dynVarOrdMethod = dynVarOrdMethod;
    } else
      network->dynVarOrdMethod = BDD_REORDER_SIFT;
  } else
    network->dynVarOrdMethod = dynVarOrdMethod;
}


void *
Ntk_NetworkReadUndef(
  Ntk_Network_t * network)
{
  return (network->undef);
}


void
Ntk_NetworkSetUndef(
  Ntk_Network_t * network,
  void * value)
{
  network->undef = value;
}


Ntk_Node_t *
Ntk_NetworkFindNodeByMddId(
  Ntk_Network_t * network,
  int             mddId)
{
  Ntk_Node_t *node = NIL(Ntk_Node_t);

  if (mddId != NTK_UNASSIGNED_MDD_ID) {
    st_lookup(network->mddIdToNode, (char *) (long) mddId, &node);
  }

  return (node);
}


Ntk_Node_t *
Ntk_NetworkFindNodeByActualName(
  Ntk_Network_t * network,
  char * name)
{
  Ntk_Node_t *node = NIL(Ntk_Node_t);

  st_lookup(network->actualNameToNode, name, &node);

  return (node);
}


Ntk_Node_t *
Ntk_NetworkFindNodeByName(
  Ntk_Network_t * network,
  char * name)
{
  Ntk_Node_t *node = NIL(Ntk_Node_t);
  char *actualName = Ntk_NetworkReadActualNameFromFormalName(network, name);

  /*
   * If there was no actual name corresponding to name in the formal to actual
   * table, then treat name as an actualName.
   */
  if (actualName == NIL(char)) {
    actualName = name;
  }

  st_lookup(network->actualNameToNode, actualName, &node);

  return (node);
}


char *
Ntk_NetworkReadActualNameFromFormalName(
  Ntk_Network_t * network,
  char * formalName)
{
  char *actualName = NIL(char);

  st_lookup(network->formalNameToActualName, formalName, &actualName);

  return (actualName);
}


void
Ntk_NetworkInsertFormalNameToActualName(
  Ntk_Network_t * network,
  char * formalName,
  char * actualName)
{
  char *formalNameCopy = util_strsav(formalName);
  char *actualNameCopy = util_strsav(actualName);

  st_insert(network->formalNameToActualName, formalNameCopy, actualNameCopy);
}


int
Ntk_NetworkReadNumNodes(
  Ntk_Network_t * network)
{
  return (lsLength(network->nodes));
}


int
Ntk_NetworkReadNumLatches(
  Ntk_Network_t * network)
{
  return (lsLength(network->latches));
}


int
Ntk_NetworkReadNumCombInputs(
  Ntk_Network_t * network)
{
  return (lsLength(network->combInputs));
}


int
Ntk_NetworkReadNumCombOutputs(
  Ntk_Network_t * network)
{
  return (lsLength(network->combOutputs));
}


int
Ntk_NetworkReadNumPrimaryInputs(
  Ntk_Network_t * network)
{
  return (lsLength(network->primaryInputs));
}


int
Ntk_NetworkReadNumPseudoInputs(
  Ntk_Network_t * network)
{
  return (lsLength(network->pseudoInputs));
}


int
Ntk_NetworkReadNumInputs(
  Ntk_Network_t * network)
{
  return (lsLength(network->inputs));
}


int
Ntk_NetworkReadNumPrimaryOutputs(
  Ntk_Network_t * network)
{
  return (lsLength(network->primaryOutputs));
}


lsList
Ntk_NetworkReadNodes(
  Ntk_Network_t * network)
{
  return (network->nodes);
}


lsList
Ntk_NetworkReadCombInputs(
  Ntk_Network_t * network)
{
  return (network->combInputs);
}


lsList
Ntk_NetworkReadCombOutputs(
  Ntk_Network_t * network)
{
  return (network->combOutputs);
}


lsList
Ntk_NetworkReadLatches(
  Ntk_Network_t * network)
{
  return (network->latches);
}


lsList
Ntk_NetworkReadPrimaryInputs(
  Ntk_Network_t * network)
{
  return (network->primaryInputs);
}


lsList
Ntk_NetworkReadPseudoInputs(
  Ntk_Network_t * network)
{
  return (network->pseudoInputs);
}


lsList
Ntk_NetworkReadInputs(
  Ntk_Network_t * network)
{
  return (network->inputs);
}


lsList
Ntk_NetworkReadPrimaryOutputs(
  Ntk_Network_t * network)
{
  return (network->primaryOutputs);
}


boolean
Ntk_NetworkAddApplInfo(
  Ntk_Network_t * network,
  char * key,
  Ntk_ApplInfoFreeFn  freeFn,
  void * data)
{
  ApplInfo_t *applInfo;
  boolean     status;

  if (st_lookup(network->applInfoTable, key, &applInfo)) {
    (*applInfo->freeFn)(applInfo->data);
    status = TRUE;
  }
  else {
    char *keyCopy = util_strsav(key);

    applInfo = ALLOC(ApplInfo_t, 1);
    st_insert(network->applInfoTable, keyCopy, (char *) applInfo);
    status = FALSE;
  }

  applInfo->freeFn = freeFn;
  applInfo->data   = data;
  return status;
}

boolean
Ntk_NetworkSetApplInfo(
  Ntk_Network_t * network,
  char * key,
  Ntk_ApplInfoFreeFn  freeFn,
  void * data)
{
  ApplInfo_t *applInfo;
  boolean     status;

  if (st_lookup(network->applInfoTable, key, &applInfo)) {
    status = TRUE;
  }
  else {
    char *keyCopy = util_strsav(key);

    applInfo = ALLOC(ApplInfo_t, 1);
    st_insert(network->applInfoTable, keyCopy, (char *) applInfo);
    status = FALSE;
  }

  applInfo->freeFn = freeFn;
  applInfo->data   = data;
  return status;
}


void *
Ntk_NetworkReadApplInfo(
  Ntk_Network_t * network,
  char * key)
{
  int         status;
  ApplInfo_t *applInfo;

  status = st_lookup(network->applInfoTable, key, &applInfo);
  if (status == 1) {
    return (applInfo->data);
  }
  else {
    return (NIL(void));
  }
}


boolean
Ntk_NetworkFreeApplInfo(
  Ntk_Network_t * network,
  char * key)
{
  int         status;
  ApplInfo_t *applInfo;

  status = st_lookup(network->applInfoTable, key, &applInfo);

  if (status == 1) {
    st_delete(network->applInfoTable, &key, &applInfo);
    (*applInfo->freeFn)(applInfo->data);
    FREE(key);  /* frees the string contained in the table */
    FREE(applInfo);
  }

  return ((status) ? TRUE : FALSE);
}


Ntk_Network_t *
Ntk_NetworkAlloc(
  char * name)
{
  Ntk_Network_t *network = ALLOC(Ntk_Network_t, 1);

  network->name                   = util_strsav(name);
  network->nodes                  = lsCreate();
  network->combInputs             = lsCreate();
  network->combOutputs            = lsCreate();
  network->latches                = lsCreate();
  network->primaryInputs          = lsCreate();
  network->pseudoInputs           = lsCreate();
  network->inputs                 = lsCreate();
  network->primaryOutputs         = lsCreate();
  network->combOutputsTable       = st_init_table(st_ptrcmp, st_ptrhash);
  network->mddIdToNode            = st_init_table(st_numcmp, st_numhash);
  network->actualNameToNode       = st_init_table(strcmp, st_strhash);
  network->formalNameToActualName = st_init_table(strcmp, st_strhash);
  network->applInfoTable          = st_init_table(strcmp, st_strhash);
  network->mddManager             = NIL(mdd_manager);
  network->mAigManager            = NIL(mAig_Manager_t);
  network->dynVarOrdMethod        = BDD_REORDER_NONE;
  network->undef                  = NIL(void);

  return network;
}


void
Ntk_NetworkFree(
  Ntk_Network_t * network)
{
  char *formal;
  char *actual;
  char *key;
  ApplInfo_t *applInfo;
  Ntk_Node_t *node;
  lsGen gen;
  st_generator *stGen;


  if (network == NIL(Ntk_Network_t)) {
    return;
  }

  FREE(network->name);

  Ntk_NetworkForEachNode(network, gen, node) {
    Ntk_NodeFree(node);
  }

  (void) lsDestroy(network->nodes,           (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->combInputs,      (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->combOutputs,     (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->latches,         (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->primaryInputs,   (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->pseudoInputs,    (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->inputs,          (void (*) (lsGeneric)) NULL);
  (void) lsDestroy(network->primaryOutputs,  (void (*) (lsGeneric)) NULL);
  st_free_table(network->combOutputsTable);
  st_free_table(network->mddIdToNode);

  /*
   * The keys in this table are strings representing node names.  The strings
   * are owned by the nodes, so we don't free them here.
   */
  st_free_table(network->actualNameToNode);

  /*
   * Free all the strings in the formalNameToActualName table before freeing
   * the table itself.
   */
  st_foreach_item(network->formalNameToActualName, stGen, &formal, &actual) {
    FREE(formal);
    FREE(actual);
  }

  st_free_table(network->formalNameToActualName);

  /*
   * Free all the key/applInfo pairs in the applInfoTable, and then free the
   * table itself.
   */
  st_foreach_item(network->applInfoTable, stGen, &key, &applInfo) {
    FREE(key);
    (*applInfo->freeFn)(applInfo->data);
    FREE(applInfo);
  }
  st_free_table(network->applInfoTable);

  if (network->mddManager != NIL(mdd_manager)) {
    mdd_quit(network->mddManager);
  }

  if (network->mAigManager != NIL(mAig_Manager_t)) {
    mAig_quit(network->mAigManager);
  }

  FREE(network);
}


void
Ntk_NetworkFreeCallback(
  void * data /* an object of type Ntk_Network_t*  type casted to void* */)
{
  Ntk_NetworkFree((Ntk_Network_t *) data);
}


void
Ntk_NetworkWriteBlifMv(
  FILE *fp,
  Ntk_Network_t *network,
  boolean promotePseudo
  )
{
  lsGen gen;
  Ntk_Node_t *node;
  int i;

  (void) fprintf(fp, ".model %s\n", Ntk_NetworkReadName(network));

  /* .inputs */
  if (Ntk_NetworkReadNumPrimaryInputs(network) != 0) {
    (void) fprintf(fp, ".inputs");
    Ntk_NetworkForEachPrimaryInput(network, gen, node) {
      (void) fprintf(fp, " %s", Ntk_NodeReadName(node));
    }
    (void) fprintf(fp, "\n");
  }

  if (promotePseudo && Ntk_NetworkReadNumPseudoInputs(network) != 0) {
    (void) fprintf(fp, "# pseudo inputs\n");
    (void) fprintf(fp, ".inputs");
    Ntk_NetworkForEachPseudoInput(network, gen, node) {
      (void) fprintf(fp, " %s", Ntk_NodeReadName(node));
    }
    (void) fprintf(fp, "\n");
  }

  /* .outputs */
  if (Ntk_NetworkReadNumPrimaryOutputs(network) != 0) {
    (void) fprintf(fp, ".outputs");
    Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
      (void) fprintf(fp, " %s", Ntk_NodeReadName(node));
    }
    (void) fprintf(fp, "\n");
  }

  /* .mv .names .latch .reset */
  Ntk_NetworkForEachNode(network, gen, node) {
    Var_Variable_t *var = Ntk_NodeReadVariable(node);
    char *nodeName = Ntk_NodeReadName(node);
    boolean is_enum = Var_VariableTestIsEnumerative(var);
    int range = Var_VariableReadNumValues(var);

    if (Ntk_NodeTestIsShadow(node)) continue;
    if (Ntk_NodeTestIsCombinational(node) &&
        Ntk_NodeTestIsLatchInitialInput(node)) continue;

    if (is_enum) {
      if (range != 2) {
        /* Boolean enumerative variables need no .mv declaration. */
        (void) fprintf(fp, ".mv %s %d\n", nodeName, range);
      }
    } else {
      /* Variable is symbolic. */
      (void) fprintf(fp, ".mv %s %d", nodeName, range);
      for (i = 0; i < range; i++) {
        (void) fprintf(fp, " %s",
                       Var_VariableReadSymbolicValueFromIndex(var, i));
      }
      (void) fprintf(fp, "\n");
    }
  }

  if (!promotePseudo && Ntk_NetworkReadNumPseudoInputs(network) != 0) {
    (void) fprintf(fp, "# pseudo inputs start\n");
    Ntk_NetworkForEachPseudoInput(network, gen, node) {
      Tbl_Table_t *dupTable = DuplicateTableAndVars(node,
                                                    Ntk_NodeReadName(node));
      Tbl_TableWriteBlifMvToFile(dupTable, 0, fp);
      Tbl_TableFree(dupTable);
    }
    (void) fprintf(fp, "# pseudo inputs end\n");
  }

  Ntk_NetworkForEachNode(network, gen, node) {

    if (Ntk_NodeTestIsShadow(node)) continue;
    if (Ntk_NodeTestIsCombinational(node) &&
        Ntk_NodeTestIsLatchInitialInput(node)) continue;

    if (Ntk_NodeTestIsCombinational(node)) {
      Tbl_Table_t *dupTable = DuplicateTableAndVars(node,
                                                    Ntk_NodeReadName(node));
      Tbl_TableWriteBlifMvToFile(dupTable, 0, fp);
      Tbl_TableFree(dupTable);
    } else if (Ntk_NodeTestIsLatch(node)) {
      Ntk_Node_t *data = Ntk_LatchReadDataInput(node);
      Ntk_Node_t *reset = Ntk_LatchReadInitialInput(node);
      Tbl_Table_t *dupTable = DuplicateTableAndVars(reset,
                                                    Ntk_NodeReadName(node));
      (void) fprintf(fp, ".latch %s %s\n", Ntk_NodeReadName(data),
                     Ntk_NodeReadName(node));
      Tbl_TableWriteBlifMvToFile(dupTable, 1, fp);
      Tbl_TableFree(dupTable);
    }
  }

  (void) fprintf(fp, ".end\n");

} /* Ntk_NetworkWriteBlifMv */


void
Ntk_NetworkPrint(
  FILE * fp,
  Ntk_Network_t * network,
  boolean printIo,
  boolean printTableStats)
{
  Ntk_Node_t *node;
  lsGen       gen;

  (void) fprintf(fp, "Nodes of network %s:\n", Ntk_NetworkReadName(network));

  Ntk_NetworkForEachNode(network, gen, node) {
    Ntk_NodePrint(fp, node, printIo, printTableStats);
    /*
     * It's nice to have a line separating nodes when we print the fanins and
     * fanouts or table stats.
     */
    if (printIo || printTableStats) {
      (void) fprintf(fp, "\n");
    }
  }
}


void
Ntk_NetworkPrintStats(
  FILE * fp,
  Ntk_Network_t * network)
{
  lsGen          gen;
  Ntk_Node_t     *node;
  int            numConstants     = 0;
  int            numCombinational = 0;
  int            numEdges         = 0;
  mdd_manager  *mddMgr;

  /*
   * Count the number of constants and the number of combinational nodes.
   */
  Ntk_NetworkForEachNode(network, gen, node) {
    numEdges += Ntk_NodeReadNumFanouts(node);
    if (Ntk_NodeTestIsConstant(node)) {
      numConstants++;
    }
    if (Ntk_NodeTestIsCombinational(node)) {
      numCombinational++;
    }
  }

  mddMgr = Ntk_NetworkReadMddManager(network);

  if (mddMgr == NIL(mdd_manager)){
     (void) fprintf(fp, "%s  combinational=%d  pi=%d  po=%d  latches=%d  pseudo=%d  const=%d  edges=%d\n",
                 Ntk_NetworkReadName(network),
                 numCombinational,
                 Ntk_NetworkReadNumPrimaryInputs(network),
                 Ntk_NetworkReadNumPrimaryOutputs(network),
                 Ntk_NetworkReadNumLatches(network),
                 Ntk_NetworkReadNumPseudoInputs(network),
                 numConstants,
                 numEdges
                 );
  }else{
     array_t *bddIdArray;
     lsGen gen;
     Ntk_Node_t *latch;
     int n_boolean_latches;
     array_t *mddIdArray = array_alloc(int, 0);

     Ntk_NetworkForEachLatch(network, gen, latch){
       array_insert_last(int, mddIdArray, Ntk_NodeReadMddId(latch));
     }

     bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr, mddIdArray);
     n_boolean_latches = array_n(bddIdArray);
     array_free(mddIdArray);
     array_free(bddIdArray);

     (void) fprintf(fp, "%s  combinational=%d  pi=%d  po=%d  latches=%d (boolean_latches=%d)  pseudo=%d  const=%d  edges=%d\n",
                 Ntk_NetworkReadName(network),
                 numCombinational,
                 Ntk_NetworkReadNumPrimaryInputs(network),
                 Ntk_NetworkReadNumPrimaryOutputs(network),
                 Ntk_NetworkReadNumLatches(network),
                 n_boolean_latches,
                 Ntk_NetworkReadNumPseudoInputs(network),
                 numConstants,
                 numEdges
                 );
  }
}


Ntk_Network_t *
Ntk_NetworkDuplicate(
  Ntk_Network_t * oldNetwork)
{
  int            i;
  lsGen          gen;
  Ntk_Node_t    *oldNode;
  Ntk_Node_t    *oldFaninNode;
  Ntk_Node_t    *oldOriginNode;
  Ntk_Node_t    *newOriginNode;
  array_t       *faninNameArray;
  Ntk_Network_t *newNetwork = Ntk_NetworkAlloc(Ntk_NetworkReadName(oldNetwork));


  /*
   * For each node in oldNetwork, create a node in newNetwork.
   */
  Ntk_NetworkForEachNode(oldNetwork, gen, oldNode) {
    (void) Ntk_NodeCreateInNetwork(newNetwork, Ntk_NodeReadName(oldNode),
                                   Ntk_NodeReadVariable(oldNode));
  }

  /*
   * For each node in oldNetwork, declare the corresponding node in newNetwork
   * using the type of the oldNode.
   */
  Ntk_NetworkForEachNode(oldNetwork, gen, oldNode) {
    char       *nodeName = Ntk_NodeReadName(oldNode);
    Ntk_Node_t *newNode  = Ntk_NetworkFindNodeByActualName(newNetwork, nodeName);
    assert(newNode != NIL(Ntk_Node_t));

    /*
     * Handle items that are independent of node type.
     */
    if (Ntk_NodeTestIsPrimaryOutput(oldNode)) {
      Ntk_NodeDeclareAsPrimaryOutput(newNode);
    }

    switch (oldNode->type) {
      case NtkPrimaryInput_c:
        Ntk_NodeDeclareAsPrimaryInput(newNode);
        break;
      case NtkPseudoInput_c:
        Ntk_NodeDeclareAsPseudoInput(newNode,
                                     Tbl_TableSoftDup(Ntk_NodeReadTable(oldNode)),
                                     Ntk_NodeReadOutputIndex(oldNode));
        break;
      case NtkLatch_c:
        Ntk_NodeDeclareAsLatch(newNode,
                               Ntk_NodeReadName(Ntk_LatchReadDataInput(oldNode)),
                               Ntk_NodeReadName(Ntk_LatchReadInitialInput(oldNode)));
        break;
      case NtkCombinational_c:
        /*
         * Create the array of names of the fanins of oldNode.
         */
        faninNameArray = array_alloc(char *, Ntk_NodeReadNumFanins(oldNode));
        Ntk_NodeForEachFanin(oldNode, i, oldFaninNode) {
          char *faninName = Ntk_NodeReadName(oldFaninNode);
          array_insert(char *, faninNameArray, i, faninName);
        }

        Ntk_NodeDeclareAsCombinational(newNode,
                                       Tbl_TableSoftDup(Ntk_NodeReadTable(oldNode)),
                                       faninNameArray,
                                       Ntk_NodeReadOutputIndex(oldNode));
        array_free(faninNameArray);
        break;
      case NtkShadow_c:
        oldOriginNode = Ntk_ShadowReadOrigin(oldNode);
        newOriginNode = Ntk_NetworkFindNodeByActualName(newNetwork,
                                                        Ntk_NodeReadName(oldOriginNode));
        Ntk_NodeDeclareAsShadow(newNode, newOriginNode);
        break;
      case NtkUnassigned_c:
        fail("Unexpected unassigned node type");
        break;
      default:
        fail("Unexpected type");
        break;
    }
  }

  return (newNetwork);
}


void
Ntk_NetworkAppendNetwork(
  Ntk_Network_t * network1,
  Ntk_Network_t * network2,
  st_table *name2ToName1)
{
  st_generator *stGen;
  lsGen         gen;
  Ntk_Node_t   *node1;
  Ntk_Node_t   *node2;
  char         *name1;
  char         *name2;
  st_table     *localName2ToName1 = st_init_table(strcmp, st_strhash);


  /*
   * For each node in network2, create a node in network1 as necessary. The
   * undef field of node2 is set to TRUE if a new node is created in network1
   * for it; else, it is set to FALSE. localName2ToName1 is a superset of
   * name2ToName1; in addition to the contents of name2ToName1, it contains
   * the new names (those appended with $NTK2) for those nodes being appended
   * to network2, and type II inputs.
   */
  Ntk_NetworkForEachNode(network2, gen, node2) {
    name1 = NIL(char);
    name2 = Ntk_NodeReadName(node2);
    st_lookup(name2ToName1, name2, &name1);
    if (name1 != NIL(char)) {
      /*
       * Name2 is in name2ToName1 table (type I input).  Hence, we will be
       * using the node in network1 corresponding to name1.  Assert that node2
       * is in fact an input, that name1 refers to an input node in network1, and
       * that node1 and node2 have the same variable domains.
       */
      Ntk_NodeSetUndef(node2, (void *) FALSE);
      st_insert(localName2ToName1, name2, util_strsav(name1));

      assert(Ntk_NodeTestIsInput(node2));
      node1 = Ntk_NetworkFindNodeByName(network1, name1);
      assert(node1 != NIL(Ntk_Node_t));
      assert(Var_VariablesTestHaveSameDomain(Ntk_NodeReadVariable(node1),
                                             Ntk_NodeReadVariable(node2)));
    }
    else {
      /*
       * Name2 is *not* in name2ToName1 table.  There are 2 possibilities: 1)
       * a node with name2 already exists in network1, and node2 is an input
       * (type II input); in this case, a) add map of name2 to name2 in the
       * localName2ToName1, b) assert that node1 is in fact an input, and c)
       * don't create a new node in network1; 2) a node with name2 doesn't
       * exist in network1, or node2 is not an input (type III inputs and
       * non-inputs); in this case, we unconditionally create a new node in
       * network1 using name2$NTK2.
       */
      node1 = Ntk_NetworkFindNodeByName(network1, name2);

      if ((node1 != NIL(Ntk_Node_t)) && Ntk_NodeTestIsInput(node2)) {
        Ntk_NodeSetUndef(node2, (void *) FALSE);
        st_insert(localName2ToName1, name2, util_strsav(name2));
      }
      else {
        char *newName = util_strcat3(name2, "$NTK2", "");
        Ntk_NodeSetUndef(node2, (void *) TRUE);
        st_insert(localName2ToName1, name2, newName);
        (void) Ntk_NodeCreateInNetwork(network1, newName,
                                       Ntk_NodeReadVariable(node2));
      }
    }
  }

  /*
   * For each node in network2 for which a new node was created in network1,
   * declare the corresponding node in network1 using the type of the node2.
   * (NOTE: this section shares a lot with Ntk_NetworkDuplicate, but is
   * sufficiently different that we don't share any code.)
   */
  Ntk_NetworkForEachNode(network2, gen, node2) {
    if (Ntk_NodeReadUndef(node2) == NIL(void)) {
      /*
       * node2 is superseded by a node in network1.
       */
      continue;
    }

    name2 = NodeReadNameFromTable(node2, localName2ToName1);
    node1 = Ntk_NetworkFindNodeByName(network1, name2);
    assert(node1 != NIL(Ntk_Node_t));

    /*
     * Handle items that are independent of node type.
     */
    if (Ntk_NodeTestIsPrimaryOutput(node2)) {
      Ntk_NodeDeclareAsPrimaryOutput(node1);
    }

    switch (node2->type) {
      case NtkPrimaryInput_c:
        Ntk_NodeDeclareAsPrimaryInput(node1);
        break;

      case NtkPseudoInput_c:
        Ntk_NodeDeclareAsPseudoInput(node1,
                                     Tbl_TableSoftDup(Ntk_NodeReadTable(node2)),
                                     Ntk_NodeReadOutputIndex(node2));
        break;

      case NtkLatch_c:
      {
        char *dataName = NodeReadNameFromTable(Ntk_LatchReadDataInput(node2),
                                               localName2ToName1);
        char *initName = NodeReadNameFromTable(Ntk_LatchReadInitialInput(node2),
                                               localName2ToName1);

        Ntk_NodeDeclareAsLatch(node1, dataName, initName);
        break;
      }

      case NtkCombinational_c:
      {
        int         i;
        Ntk_Node_t *faninNode2;
        array_t    *faninNameArray;

        /*
         * Create the array of names of the fanins of node2.
         */
        faninNameArray = array_alloc(char *, Ntk_NodeReadNumFanins(node2));
        Ntk_NodeForEachFanin(node2, i, faninNode2) {
          char *faninName = NodeReadNameFromTable(faninNode2, localName2ToName1);
          array_insert(char *, faninNameArray, i, faninName);
        }

        Ntk_NodeDeclareAsCombinational(node1,
                                       Tbl_TableSoftDup(Ntk_NodeReadTable(node2)),
                                       faninNameArray,
                                       Ntk_NodeReadOutputIndex(node2));
        array_free(faninNameArray);
        break;
      }

      case NtkShadow_c:
      {
        char       *originName;
        Ntk_Node_t *originNode2;
        Ntk_Node_t *originNode1;

        originNode2 = Ntk_ShadowReadOrigin(node2);
        /*
         * Currently, we don't allow a shadow node whose origin in a type I or
         * II input.  This is because, what if the corresponding node in
         * network1 (of the type I or II input), also has a shadow node?  Then
         * we would try to add a shadow node to a node already having a shadow;
         * this is illegal.
         */
        assert((boolean) (long) Ntk_NodeReadUndef(node2));
        originName = NodeReadNameFromTable(originNode2, localName2ToName1);
        originNode1 = Ntk_NetworkFindNodeByName(network1, originName);

        Ntk_NodeDeclareAsShadow(node1, originNode1);
        break;
      }

      case NtkUnassigned_c:
        fail("Unexpected unassigned node type");
        break;
      default:
        fail("Unexpected type");
        break;
    }
  }

  /*
   * Free all the values strings in the localName2ToName1, before freeing
   * the table itself.  The keys are not freed.
   */
  st_foreach_item(localName2ToName1, stGen, &name2, &name1) {
    FREE(name1);
  }
  st_free_table(localName2ToName1);
}


int
Ntk_NetworkPrintDot(
  FILE *fp,
  Ntk_Network_t *network)
{
  lsGen       gen;
  int i;
  Ntk_Node_t *nodePtr;
  Ntk_Node_t *fanoutPtr;
  time_t      now           = time(0);
  struct tm  *nowStructPtr  = localtime(& now);
  char       *nowTxt        = asctime(nowStructPtr);
  char       *networkName   = Ntk_NetworkReadName(network);

  /*
   * Write out the header for the output file.
   */

  (void) fprintf(fp, "# %s\n", Vm_VisReadVersion());
  (void) fprintf(fp, "# network name: %s\n", networkName);
  (void) fprintf(fp, "# generated: %s", nowTxt);
  (void) fprintf(fp, "#\n");

  (void) fprintf(fp, "# Network with %d nodes\n",
                 Ntk_NetworkReadNumNodes(network));

  (void) fprintf(fp, "digraph \"%s\" {\n  rotate=90;\n", networkName);
  (void) fprintf(fp, "  margin=0.5;\n  label=\"%s\";\n", networkName);
  (void) fprintf(fp, "  size=\"10,7.5\";\n  ratio=\"fill\";\n");

  /* Force the inputs and outputs to be printed at the same level in the graph */
  (void) fprintf(fp, "  { rank=same; ");
  Ntk_NetworkForEachCombInput(network,gen, nodePtr) {
    (void) fprintf(fp, "\"%s\"; ", Ntk_NodeReadName(nodePtr));
  }
  (void) fprintf(fp, "}\n");
  (void) fprintf(fp, "  { rank=same; ");
  Ntk_NetworkForEachCombOutput(network,gen, nodePtr) {
    (void) fprintf(fp, "\"%s\"; ", Ntk_NodeReadName(nodePtr));
  }
  (void) fprintf(fp, "}\n");

  /* Print all the edges */
  Ntk_NetworkForEachNode(network, gen, nodePtr) {

    if (Ntk_NodeReadNumFanouts(nodePtr) == 0 &&
        Ntk_NodeReadNumFanins(nodePtr) == 0) {
      /* Print the dot description for a node */
      (void) fprintf(fp, "  \"%s\";\n", Ntk_NodeReadName(nodePtr));
    } /* End of if */

    /* Print the edges comming out of that node */
    Ntk_NodeForEachFanout(nodePtr, i, fanoutPtr) {
      (void) fprintf(fp, "  \"%s\" -> \"%s\";\n", Ntk_NodeReadName(nodePtr),
                     Ntk_NodeReadName(fanoutPtr));
    }
  }

  (void) fprintf(fp, "}\n");

  return 1;
}

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

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

static char *
NodeReadNameFromTable(
  Ntk_Node_t *node,
  st_table *name2ToName1)
{
  char    *name1  = NIL(char);
  char    *name2  = Ntk_NodeReadName(node);
  boolean  status UNUSED = st_lookup(name2ToName1, name2, &name1);

  assert(status);
  return name1;
}


static Tbl_Table_t *
DuplicateTableAndVars(
  Ntk_Node_t *node,
  char *name
  )
{
  Var_Variable_t *var, *newVar;
  Tbl_Table_t *dupTable, *tbl;
  int col;
  Tbl_Table_t *table = Ntk_NodeReadTable(node);
  array_t *split = Tbl_TableSplit(table);
  int outIndex = Ntk_NodeReadOutputIndex(node);

  arrayForEachItem(Tbl_Table_t *, split, col, tbl) {
    if (col == outIndex) {
      dupTable = tbl;
    } else {
      Tbl_TableFree(tbl);
    }
  }
  array_free(split);

  Tbl_TableForEachInputVar(dupTable, col, var) {
    Ntk_Node_t *fanin = Ntk_NodeReadFaninNode(node, col);
    char *newName = Ntk_NodeReadName(fanin);
    newVar = Var_VariableDup(var, NIL(Hrc_Node_t));
    Var_VariableChangeName(newVar, newName);
    Tbl_TableSetVar(dupTable, col, newVar, 0);
  }

  var = array_fetch(Var_Variable_t *,Tbl_TableReadOutputVars(dupTable), 0);
  newVar = Var_VariableDup(var, NIL(Hrc_Node_t));
  Var_VariableChangeName(newVar, name);
  Tbl_TableSetVar(dupTable, 0, newVar, 1);

  return dupTable;

} /* DuplicateTableAndVars */