source: vis_dev/vis-2.3/src/ntk/ntkCmd.c @ 46

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

  FileName    [ntkCmd.c]

  PackageName [ntk]

  Synopsis    [Command interface to the ntk package.]

  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: ntkCmd.c,v 1.19 2010/04/09 23:44:05 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
/*
 * States of the state machine used to parse the input variable name list file.
 */
#define STATE_TEST 0 /* next char is in first column */
#define STATE_WAIT 1 /* wait until end of line '\n' is reached */
#define STATE_IN   2 /* parsing a variable name */

/*
 * Maximum permissible length of a variable name in the input variable name list file.
 */
#define MAX_NAME_LENGTH 200

int NtkDebug;

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

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

static int CommandPrintNetworkStats(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandPrintNetwork(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandPrintNetworkDot(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandWriteNetworkBlifMv(Hrc_Manager_t ** hmgr, int  argc, char ** argv);
static int CommandFlattenHierarchy(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandTestNetworkAcyclic(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandInitVerify(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandNetworkSweep(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static boolean FileReadNameList(FILE * fp, lsList * nameList, int verbose);

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


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

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

  Synopsis    [Initializes the network package.]

  SideEffects []

  SeeAlso     [Ntk_End]

******************************************************************************/
void
Ntk_Init(void)
{
  Cmd_CommandAdd("print_network_stats",   CommandPrintNetworkStats,   0);
  Cmd_CommandAdd("print_network",         CommandPrintNetwork,        0);
  Cmd_CommandAdd("print_network_dot",     CommandPrintNetworkDot,     0);
  Cmd_CommandAdd("flatten_hierarchy",     CommandFlattenHierarchy,    1);
  Cmd_CommandAdd("test_network_acyclic",  CommandTestNetworkAcyclic,  0);
  Cmd_CommandAdd("init_verify",           CommandInitVerify,          0);
  Cmd_CommandAdd("network_sweep",         CommandNetworkSweep,        1);
  Cmd_CommandAdd("write_network_blif_mv", CommandWriteNetworkBlifMv,  0);
}


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

  Synopsis    [Ends the network package.]

  SideEffects []

  SeeAlso     [Ntk_Init]

******************************************************************************/
void
Ntk_End(void)
{
}


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

  Synopsis    [Returns the current network of a hierarchy manager.]

  Description [Returns the network of the current node of a hierarchy
  manager. Assumes hmgr is non-NULL. If the current node or network is NULL,
  then a message is printed to vis_stderr, and NULL is returned.]

  SideEffects []

  SeeAlso     [Hrc_ManagerReadCurrentNode]

******************************************************************************/
Ntk_Network_t *
Ntk_HrcManagerReadCurrentNetwork(Hrc_Manager_t *hmgr)
{
  Hrc_Node_t *currentNode;
  Ntk_Network_t *network;

  assert(hmgr != NIL(Hrc_Manager_t));
  currentNode = Hrc_ManagerReadCurrentNode(hmgr);
  if (currentNode == NIL(Hrc_Node_t)) {
    (void) fprintf(vis_stderr, "The hierarchy manager is empty.  Read in design.\n");
    return NIL(Ntk_Network_t);
  }

  network = (Ntk_Network_t *) Hrc_NodeReadApplInfo(currentNode,
                                                   NTK_HRC_NODE_APPL_KEY);
  if (network == NIL(Ntk_Network_t)) {
    (void) fprintf(vis_stdout, "There is no network. Use flatten_hierarchy.\n");
    return NIL(Ntk_Network_t);
  }

  return network;
}

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


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

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

  Synopsis    [Implements the print_network_stats command.]

  CommandName [print_network_stats]

  CommandSynopsis [print statistics about the flattened network]

  CommandArguments [\[-h\]]

  CommandDescription [Prints the following statistics about the flattened
  network:

  <dl>
  
  <li> <b>name:</b> the name of the flattened network

  <li> <b>combinational:</b> the number of nodes which have a table defining
  the function of the node (excludes pseudo inputs)

  <li> <b>primary inputs:</b> the number of primary input nodes of the
  flattened network

  <li> <b>primary outputs:</b> the number of primary output nodes of the
  flattened network

  <li> <b>latches:</b> the number of (multi-valued) latches

  <li> <b>pseudo inputs:</b> the number of pseudo input nodes of the
  flattened network

  <li> <b>constants:</b> the number of combinational nodes that implement a
  multi-valued constant

  <li> <b>edges:</b> the number of fanouts in the network (e.g. if the output
  of a node is used in two places, this contributes two to the sum)

  </dl>

  Note that <tt>flatten_hierarchy</tt> must be called before this command.<p>

  Example output:
  <pre>
  small  combinational=2  pi=2  po=0  latches=1  pseudo=0  const=1  edges=4
  </pre>

  Command options:<p>  

  <dl><dt> -h
  <dd> Print the command usage.<p> 
  </dl>

  ]
  
  SideEffects []

******************************************************************************/
static int
CommandPrintNetworkStats(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int            c;
  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);

  /*
   * Parse the command line.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "h")) != EOF) {
    switch (c) {
      case 'h':
        goto usage;
      default:
        goto usage;
    }
  }
  
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }

  Ntk_NetworkPrintStats(vis_stdout, network);
  return 0;             /* normal exit */

usage:
  (void) fprintf(vis_stderr, "usage: print_network_stats [-h]\n");
  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
  return 1;             /* error exit */
}


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

  Synopsis    [Implements the print_network command.]

  CommandName [print_network]

  CommandSynopsis [print information about the flattened network]

  CommandArguments [\[-f\] \[-h\] \[-t\]]

  CommandDescription [Prints the name of the flattened network, and
  information about each node.  For each node, prints the following:

  <dl>

  <li> <b>name:</b> the name of the node

  <li> <b>mdd:</b> MDD id (-1 is uninitialized)

  <li> <b>type:</b> one of combinational, primary-input, pseudo-input, latch,
  or shadow

  <li> <b>derived attributes:</b> list of derived attributes of the node

  </dl>

  See the ntk documentation for more information on types and attributes. The
  following is an example describing information associated with a node.

  <pre>
  small.latch_in: mdd=2, combinational; data-input comb-output
  </pre>

  The flattened name of the node is "small.latch_in", its MDD id is 2, it is
  of type combinational, and it is both a data input to a latch, and a
  combinational output.<p>
  
  Command options:<p>  

  <dl>

  <dt> -f
  <dd> Print the fanins and fanouts of each node.<p> 

  <dt> -h
  <dd> Print the command usage.<p> 

  <dt> -t
  <dd> Print table statistics for those nodes having tables.<p> 

  </dl>]

  SideEffects []

******************************************************************************/
static int
CommandPrintNetwork(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int            c;
  boolean        printIo         = FALSE;  /* default */
  boolean        printTableStats = FALSE;  /* default */
  Ntk_Network_t *network         = Ntk_HrcManagerReadCurrentNetwork(*hmgr);

  /*
   * Parse the command line.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "fth")) != EOF) {
    switch (c) {
      case 'f':
        printIo = TRUE;
        break;
      case 't':
        printTableStats = TRUE;
        break;
      case 'h':
        goto usage;
      default:
        goto usage;
    }
  }
  
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }

  Ntk_NetworkPrint(vis_stdout, network, printIo, printTableStats);
  return 0;             /* normal exit */

usage:
  (void) fprintf(vis_stderr, "usage: print_network [-f] [-h] [-t]\n");
  (void) fprintf(vis_stderr, "   -f  print fanins and fanouts of nodes\n");
  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
  (void) fprintf(vis_stderr, "   -t  print table stats of nodes having tables\n");
  return 1;             /* error exit */
}


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

  Synopsis    [Implements the print_network_dot command.]

  CommandName [print_network_dot]

  CommandSynopsis [print a dot description of the flattened network]

  CommandArguments [\[-h\] &lt;file_name&gt;]

  CommandDescription [Write a file in the format taken by the tool <tt>dot</tt>
  depicting the topology of the network. Dot is a tool that given a description
  of a graph in a certain format it produces a postscript print of the
  graph. For more information about <tt>dot</tt> look in <a
  href="http://www.research.att.com/orgs/ssr/book/reuse">
  http://www.research.att.com/orgs/ssr/book/reuse</a>. Once a dot file is
  produced with this command, the shell command <tt>dot -Tps <filename>
  &gt;<file>.ps</tt> will produce the postscript file depicting the network.<p>

  If no argument is specified on the command line, the description is written
  to the standard output.<p>

  Command options:<p>
  <dl><dt> -h
  <dd> Print the command usage.
  </dl>]

  SideEffects []

******************************************************************************/
static int
CommandPrintNetworkDot(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  FILE *fp;
  int c, status;
  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);

  util_getopt_reset();
  while ((c = util_getopt(argc,argv,"h")) != EOF){
    switch(c){
      case 'h':
        goto usage;
      default:
        goto usage;
    }
  }

  /* Check if the network has been read in */
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }

  if (argc == 1) {
    fp = stdout;
  }
  else if (argc == 2) {
    fp = Cmd_FileOpen(*(++argv), "w", NIL(char *), /* silent */ 1);
    if (fp == NIL(FILE)) {
      (void) fprintf(vis_stderr, "Cannot write to %s\n", *argv);
      return 1;
    }
  }
  else {
    goto usage;
  }

  error_init();
  status = Ntk_NetworkPrintDot(fp, network);
  (void) fprintf(vis_stderr, "%s", error_string());
  fflush(fp);
  if (fp != stdout) {
    (void) fclose(fp);
  }
  return (status ? 0 : 1);

 usage:
  (void) fprintf(vis_stderr, "usage: print_network_dot [-h] [file]\n");
  (void) fprintf(vis_stderr, "    -h\t\tprint the command usage\n");
  return 1;
}


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

  Synopsis    [Write a (flattened) network in blif-MV format.]

  CommandName [write_network_blif_mv]

  CommandSynopsis [write a blif-MV description of the flattened network]

  CommandArguments [\[-h\] \[-p\] &lt;file_name&gt;]

  CommandDescription [Write a file in Blif-MV format describing the
  network. <p>

  If no argument is specified on the command line, the description is written
  to the vis standard output.<p>

  Command options:<p>
  <dl><dt> -h
  <dd> Print the command usage.
  <dt> -p
  <dd> Promote pseudo inputs to primary inputs.
  </dl>]

  SideEffects []

******************************************************************************/
static int
CommandWriteNetworkBlifMv(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  FILE *fp;
  int c;
  boolean promotePseudo = FALSE;
  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);

  /* Check whether the network has been created. */
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }

  util_getopt_reset();
  while ((c = util_getopt(argc,argv,"hp")) != EOF){
    switch(c){
    case 'h':
      goto usage;
    case 'p':
      promotePseudo = TRUE;
      argv++;
      argc--;
      break;
    default:
      goto usage;
    }
  }

  if (argc == 1) {
    fp = vis_stdout;
  } else if (argc == 2) {
    fp = Cmd_FileOpen(*(++argv), "w", NIL(char *), /* silent */ 1);
    if (fp == NIL(FILE)) {
      (void) fprintf(vis_stderr, "Cannot write to %s\n", *argv);
      return 1;
    }
  } else {
    goto usage;
  }

  error_init();
  Ntk_NetworkWriteBlifMv(fp, network, promotePseudo);
  (void) fprintf(vis_stderr, "%s", error_string());
  fflush(fp);
  if (fp != vis_stdout) {
    (void) fclose(fp);
  }
  return 1;

 usage:
  (void) fprintf(vis_stderr, "usage: write_network_blif_mv [-h] [file]\n");
  (void) fprintf(vis_stderr, "    -h\t\tprint the command usage\n");
  (void) fprintf(vis_stderr, "    -p\t\tpromote pseudo inputs to primary inputs\n");
  return 1;

} /* CommandWriteNetworkBlifMv */


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

  Synopsis    [Implements the flatten_hierarchy command.]

  CommandName [flatten_hierarchy]

  CommandSynopsis [create a flattened network]

  CommandArguments [\[-a &lt;file&gt;\] \[-b\] \[-h\] \[-s\] \[-v #\]]

  CommandDescription [Creates a flattened network from a hierarchical
  description.  The flattened network encompasses everything from the
  current node of the hierarchy (reached by the command <tt>cd</tt>),
  down to and including the leaves.  It creates a view with the
  hierarchy removed, but retains the multi-level logic structure.  The
  resulting flattened network is stored with the current node. Every
  table in the flattened network is checked whether it is completely
  specified and deterministic. This is the starting point for
  verification related commands. <p>

  A limited form of abstraction can be done by providing a list of variables
  to treat as primary inputs.  See the information under &lt;file&gt;
  below.<p>
  
  The verification part of VIS requires the functions specified by the BLIF-MV
  tables to be completely specified and deterministic.  These conditions are
  checked during the flattening process; if a table is found that is
  incompletely specified or is nondeterministic, then an error message is
  written and a flattened network is not created.  The exception to this
  rule is tables specifying "pseudo inputs"; these are tables with no inputs,
  and a single output that can take more than one value.  Such tables are
  generated by vl2mv to model the "$ND" construct in Verilog.<p>
  
  If this command is invoked a second time from the same point in the
  hierarchy, the previous network is deleted and a new one is created.  This
  is the tactic to follow if you want to change some aspect of the current
  network, such as MDD variable ordering or <tt>image_method</tt>.<p>

  Command options:<p>  

  <dl>

  <dt> -a &lt;file&gt;

  <dd> A file containing names of variables, used to specify which variables
  to abstract. The name of a variable is the full hierarchical path name,
  starting from just after the current hierarchy node (i.e., if the current
  node is foo, and you want to refer to variable x in foo, then just use x).
  A variable should appear at most once in the file.  Each variable name
  should appear at the beginning of a new line, with no white space preceding
  it.  The end of a variable name is marked by white space, and any other text
  on the rest of the line is ignored.  Any line starting with "#" or white
  space is ignored.  A sample file is shown here.<p>

  <pre>
  # variables to abstract to model check liveness property
  choosing0 
  p0.pc     
  </pre>

  For each variable x appearing in the file, a new primary input node named
  x$ABS is created to drive all the nodes that were previously driven by x.
  Hence, the node x will not have any fanouts; however, x and its transitive
  fanins will remain in the network. <p>

  Abstracting a net effectively allows it to take any value in its range, at
  every clock cycle. This mechanism can be used to perform manual
  abstractions.  The variables to abstract should not affect the correctness
  of the property being checked.  This usually simplifies the network, and
  permits some verification tasks to complete that would not otherwise.  Note,
  however, that by increasing the behavior of the system, false negatives are
  possible when checking universal properties, and false positives are
  possible when checking existential properties. <p>

  A convenient way of generating the hierarchical variable names is by using
  the write_order command. Note that abstracting next state variables has no
  effect.<p>


  <dt> -b
  <dd> This option has no effect any longer.<p>

  <dt> -h
  <dd> Print the command usage. <p>

  <dt> -s
  <dd> Do not perform a sweep. <p>

  <dt> -v #
  <dd> Print debug information.
  <dd>

  0: (default) Nothing is printed out.<p>
  
  >= 2: Prints the variables read from the input file.<p>
  
  
  </dl>

  ]
  
  SideEffects []

******************************************************************************/
static int
CommandFlattenHierarchy(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int            c;
  Ntk_Network_t *network;
  char          *fileName    = NIL(char);
  int            verbose     = 0;       /* default */
  int            sweep       = 1;  
  lsList         varNameList = (lsList) NULL;
  Hrc_Node_t    *currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
  
  /*
   * Parse the command line.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "a:bhsv:")) != EOF) {
    switch (c) {
      case 'a':
        fileName = util_optarg;
        break;
      case 'b':
        break;
      case 'h':
        goto usage;
      case 's':
        sweep = 0;
        break;        
      case 'v':
        verbose = atoi(util_optarg);
        break;
      default:
        goto usage;
    }
  }

  if (currentNode == NIL(Hrc_Node_t)) { 
    (void) fprintf(vis_stdout, "The hierarchy manager is empty.  Read in design.\n");
    return 1;
  }
    
  /*
   * Process the file containing the variable names.
   */
  if (fileName != NIL(char)) {
    FILE *fp = Cmd_FileOpen(fileName, "r", NIL(char *), 0);
    if (fp == NIL(FILE)) {
      return 1;
    }
    else {
      boolean status;
      
      error_init();
      status = FileReadNameList(fp, &varNameList, verbose);
      (void) fclose(fp);
      if (status == FALSE) {
        (void) fprintf(vis_stderr, "Error reading variable name file:\n");
        (void) fprintf(vis_stderr, "%s", error_string());
        (void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
        return 1;
      }
    }
  }

  
  /*
   * If a network already exists, delete it.  Then create the new one, and
   * register it with the hrcNode.
   */
  network = (Ntk_Network_t *) Hrc_NodeReadApplInfo(currentNode,
                                                   NTK_HRC_NODE_APPL_KEY);
  if (network != NIL(Ntk_Network_t)) {
    (void) fprintf(vis_stdout, "Deleting current network and creating new one.\n");
    Hrc_NodeFreeApplInfo(currentNode, NTK_HRC_NODE_APPL_KEY);
  }

  error_init();

  network = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, varNameList);

  /* Clean up the varNameList. */
  if (varNameList != (lsList) NULL) {
    lsGen  gen;
    char  *varName;
    
    lsForEachItem(varNameList, gen, varName) {
      FREE(varName);
    }
    (void) lsDestroy(varNameList, (void (*) (lsGeneric)) NULL);
  }
  /* sweep network */
  if (network != NIL(Ntk_Network_t) && sweep ==1) {
    Ntk_NetworkSweep(network, verbose); 
  }
  
  if (network == NIL(Ntk_Network_t)) {
    (void) fprintf(vis_stderr, "%s", error_string());
    (void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
    return 1;
  }
  
  Hrc_NodeAddApplInfo(currentNode, NTK_HRC_NODE_APPL_KEY,
                      (Hrc_ApplInfoFreeFn) Ntk_NetworkFreeCallback,
                      (Hrc_ApplInfoChangeFn) NULL,  /* not currently used by hrc */
                      (void *) network);

  return 0;             /* normal exit */

usage:
  (void) fprintf(vis_stderr, "usage: flatten_hierarchy [-a file] [-b] [-h] [-s] [-v #]\n");
  (void) fprintf(vis_stderr, "   -a file  variables to abstract\n");
  (void) fprintf(vis_stderr, "   -b       not used any longer\n");
  (void) fprintf(vis_stderr, "   -h       print the command usage\n");
  (void) fprintf(vis_stderr, "   -s       do not perform a sweep\n");  
  (void) fprintf(vis_stderr, "   -v #     verbosity level\n");
  return 1;             /* error exit */
}


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

  Synopsis    [Implements the test_network_acyclic command.]

  CommandName [test_network_acyclic]

  CommandSynopsis [determine whether the network is acyclic]

  CommandArguments [\[-h\]]

  CommandDescription [If the flattened network has a combinational
  cycle, then prints information about one of the cycles.  If no cycles are
  present, then it prints a message to this effect.<p>  

  Command options:<p>  

  <dl><dt> -h
  <dd> Print the command usage.<p> 
  </dl>
  ]
  
  SideEffects []

******************************************************************************/
static int
CommandTestNetworkAcyclic(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int            c;
  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);

  /*
   * Parse the command line.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "h")) != EOF) {
    switch (c) {
      case 'h':
        goto usage;
      default:
        goto usage;
    }
  }
  
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }

  error_init();
  if (Ntk_NetworkTestIsAcyclic(network) == 0) {
    (void) fprintf(vis_stdout, "Combinational cycle found: ");
    (void) fprintf(vis_stdout, "%s", error_string());
    (void) fprintf(vis_stdout, "\n");
  }
  else {
    (void) fprintf(vis_stdout, "Network has no combinational cycles\n");
  }
  return 0;             /* normal exit */


usage:
  (void) fprintf(vis_stderr, "usage: test_network_acyclic [-h]\n");
  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
  return 1;             /* error exit */
}


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

  Synopsis    [Implements the init_verify command.]

  CommandName [init_verify]

  CommandSynopsis [create and initialize a flattened network for verification]

  CommandArguments [\[-b\] \[-h\]]

  CommandDescription [This command initializes the system for verification,
  and is equivalent to the command sequence <tt>flatten_hierarchy;
  static_order; build_partition_mdds</tt>.  If a command returns an error
  condition, then the sequence is aborted.  After <tt>init_verify</tt> has
  successfully executed, various commands can be invoked, like
  <tt>model_check</tt>, <tt>compute_reach</tt>, <tt>simulate</tt>,
  <tt>print_network_stats</tt>, and <tt>seq_verify</tt>.<p>

  Please note that init_verify does not enable dynamic variable
  reordering. Sometimes, though, this is needed to complete building
  the partitions, and one has to initialize the verification by hand.
  Similarly, it may be wise to turn on dynamic variable reordering after
  init, so that further commands complete more easily. See the help page
  for <tt>dynamic_var_ordering</tt>.


  <p>Command options:<p>  

  <dl><dt> -b
  <dd> This option has no effect any longer. <p>
  </dl>
  <dl><dt> -h
  <dd> Print the command usage.<p> 
  </dl>

  ]
  
  SideEffects []

******************************************************************************/
static int
CommandInitVerify(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int         c;
  Hrc_Node_t *currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
  
  /*
   * Parse the command line.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "bh")) != EOF) {
    switch (c) {
      case 'b':
        break;
      case 'h':
        goto usage;
      default:
        goto usage;
    }
  }

  if (currentNode == NIL(Hrc_Node_t)) { 
    (void) fprintf(vis_stdout, "The hierarchy manager is empty.  Read in design.\n");
    return 1;
  }
    
  /*
   * Call the commands one-by-one, returning upon the first error.
   */
  if (Cmd_CommandExecute(hmgr, "flatten_hierarchy")) {
    return 1;
  }
  
  if (Cmd_CommandExecute(hmgr, "static_order")) {
    return 1;
  }
  
  if (Cmd_CommandExecute(hmgr, "build_partition_mdds")) {
    return 1;
  }
  
  return 0;             /* normal exit */


usage:
  (void) fprintf(vis_stderr, "usage: init_verify [-b] [-h]\n");
  (void) fprintf(vis_stderr, "   -b  not used any longer.\n");
  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
  return 1;             /* error exit */
}


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

  Synopsis    [Implements the network_sweep command.]

  CommandName [network_sweep]

  CommandSynopsis [sweeps the network to ensure that deterministic constants
  are removed]

  CommandArguments [\[-h\]\[-v\]]

  CommandDescription [This function performs a sweep on the given
  Ntk_Network_t. It propagates all the deterministic constant nodes, and
  removes all buffer nodes. It modifies the network.

  Command options:<p>  

  <dl><dt> -h
  <dd> Print the command usage.<p> 
  </dl>

  <dl><dt> -v
  <dd> Print debug information.<p> 
  </dl>
  ]
  
  SideEffects []

******************************************************************************/
static int
CommandNetworkSweep(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int           c;
  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  int           verbosity = 0;

  /*
   * Parse the command line.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "hv")) != EOF) {
    switch (c) {
      case 'h':
        goto usage;
      case 'v':
        verbosity = 1;
        break;
      default:
        goto usage;
    }
  }
  
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }
  
  Ntk_NetworkSweep(network, verbosity);
  return 0;

usage:
  (void) fprintf(vis_stderr, "usage: network_sweep [-h][-v]\n");
  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
  (void) fprintf(vis_stderr, "   -v  print debug information\n");  
  return 1;             /* error exit */
}

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

  Synopsis    [Returns a list of names corresponding to the names in a file.]

  Description [Parses a file and builds a name list corresponding to the names
  found in the first "column" of each line of the file.  Any line starting
  with the comment character '#' or white space is ignored.  No checks are
  made to see if the names are well-formed in any respect. If a problem is
  found while parsing the file (e.g. name length exceeded), then a message is
  written to error_string, the partial name list is freed, and the function
  returns FALSE; otherwise, it returns TRUE, and a pointer to a list is
  returned.]

  Comment [The parser consists of 3 states.  See the documentation
  accompanying the #defines defining the state names.  This code was adapted
  from Ord_FileReadNodeList.]
  
  SideEffects []

******************************************************************************/
static boolean
FileReadNameList(
  FILE * fp,
  lsList * nameList /* of char *, for return */,
  int verbose)
{
  int     c;
  int     state;
  int     curPosition = 0;
  char   *name;
  char    string[MAX_NAME_LENGTH];
  boolean returnFlag = TRUE;
  
  *nameList = lsCreate();

  state = STATE_TEST;
  while ((c = fgetc(fp)) != EOF) {

    switch (state) {
      case STATE_TEST:
        /* At start of a new line. */
        if (c == '#') {
          /* Line starting with comment character; wait for newline */
          state = STATE_WAIT;
        }
        else if ((c == ' ') || (c == '\t')) {
          /* Line starting with white space; wait for newline */
          state = STATE_WAIT;
        }
        else if (c == '\n') {
          /* Line starting with newline; go to next line */
          state = STATE_TEST;
        }
        else {
          /* Assume starting a name. */
          curPosition = 0;
          string[curPosition++] = c;
          state = STATE_IN;
        }
        break;
      case STATE_WAIT:
        /*
         * Waiting for the newline character.
         */
        state = (c == '\n') ? STATE_TEST : STATE_WAIT;
        break;
      case STATE_IN:
        /*
         * Parsing a name.  If white space reached, then terminate the
         * name and process it.  Else, continue parsing.
         */
        if ((c == ' ') || (c == '\n') || (c == '\t')) {
          string[curPosition] = '\0';
          name = util_strsav(string);
          if (verbose > 1) {
            (void) fprintf(vis_stdout, "Reading name: %s\n", name);
          }
          (void) lsNewEnd(*nameList, (lsGeneric) name, LS_NH);  
          
          state = (c == '\n') ? STATE_TEST : STATE_WAIT;
        }
        else {
          string[curPosition++] = c;
          if (curPosition >= MAX_NAME_LENGTH) {
            error_append("maximum name length exceeded");
            returnFlag = FALSE;
          }
          state = STATE_IN; /* redundant, but be explicit */
        }
        break;
      default:
        fail("unrecognized state");
    }
  }

  /*
   * Handle case where EOF terminates a name.
   */
  if (state == STATE_IN) {
    string[curPosition] = '\0';
    name = util_strsav(string);
    if (verbose > 1) {
      (void) fprintf(vis_stdout, "Reading name: %s\n", name);
    }
    (void) lsNewEnd(*nameList, (lsGeneric) name, LS_NH);  
          
  }

  if (returnFlag) {
    return TRUE;
  }
  else {
    (void) lsDestroy(*nameList, (void (*) (lsGeneric)) NULL);
    return FALSE;
  }
}