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

Last change on this file since 23 was 14, checked in by cecile, 13 years ago

vis2.3

File size: 31.6 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ntkCmd.c]
4
5  PackageName [ntk]
6
7  Synopsis    [Command interface to the ntk package.]
8
9  Author      [Adnan Aziz, Tom Shiple]
10
11  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
12  All rights reserved.
13
14  Permission is hereby granted, without written agreement and without license
15  or royalty fees, to use, copy, modify, and distribute this software and its
16  documentation for any purpose, provided that the above copyright notice and
17  the following two paragraphs appear in all copies of this software.
18
19  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
20  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
21  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
22  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
23
24  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
25  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
26  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
27  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
28  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
29
30******************************************************************************/
31
32#include "ntkInt.h"
33
34static char rcsid[] UNUSED = "$Id: ntkCmd.c,v 1.19 2010/04/09 23:44:05 fabio Exp $";
35
36/*---------------------------------------------------------------------------*/
37/* Constant declarations                                                     */
38/*---------------------------------------------------------------------------*/
39/*
40 * States of the state machine used to parse the input variable name list file.
41 */
42#define STATE_TEST 0 /* next char is in first column */
43#define STATE_WAIT 1 /* wait until end of line '\n' is reached */
44#define STATE_IN   2 /* parsing a variable name */
45
46/*
47 * Maximum permissible length of a variable name in the input variable name list file.
48 */
49#define MAX_NAME_LENGTH 200
50
51int NtkDebug;
52
53/**AutomaticStart*************************************************************/
54
55/*---------------------------------------------------------------------------*/
56/* Static function prototypes                                                */
57/*---------------------------------------------------------------------------*/
58
59static int CommandPrintNetworkStats(Hrc_Manager_t ** hmgr, int argc, char ** argv);
60static int CommandPrintNetwork(Hrc_Manager_t ** hmgr, int argc, char ** argv);
61static int CommandPrintNetworkDot(Hrc_Manager_t ** hmgr, int argc, char ** argv);
62static int CommandWriteNetworkBlifMv(Hrc_Manager_t ** hmgr, int  argc, char ** argv);
63static int CommandFlattenHierarchy(Hrc_Manager_t ** hmgr, int argc, char ** argv);
64static int CommandTestNetworkAcyclic(Hrc_Manager_t ** hmgr, int argc, char ** argv);
65static int CommandInitVerify(Hrc_Manager_t ** hmgr, int argc, char ** argv);
66static int CommandNetworkSweep(Hrc_Manager_t ** hmgr, int argc, char ** argv);
67static boolean FileReadNameList(FILE * fp, lsList * nameList, int verbose);
68
69/**AutomaticEnd***************************************************************/
70
71
72/*---------------------------------------------------------------------------*/
73/* Definition of exported functions                                          */
74/*---------------------------------------------------------------------------*/
75
76/**Function********************************************************************
77
78  Synopsis    [Initializes the network package.]
79
80  SideEffects []
81
82  SeeAlso     [Ntk_End]
83
84******************************************************************************/
85void
86Ntk_Init(void)
87{
88  Cmd_CommandAdd("print_network_stats",   CommandPrintNetworkStats,   0);
89  Cmd_CommandAdd("print_network",         CommandPrintNetwork,        0);
90  Cmd_CommandAdd("print_network_dot",     CommandPrintNetworkDot,     0);
91  Cmd_CommandAdd("flatten_hierarchy",     CommandFlattenHierarchy,    1);
92  Cmd_CommandAdd("test_network_acyclic",  CommandTestNetworkAcyclic,  0);
93  Cmd_CommandAdd("init_verify",           CommandInitVerify,          0);
94  Cmd_CommandAdd("network_sweep",         CommandNetworkSweep,        1);
95  Cmd_CommandAdd("write_network_blif_mv", CommandWriteNetworkBlifMv,  0);
96}
97
98
99/**Function********************************************************************
100
101  Synopsis    [Ends the network package.]
102
103  SideEffects []
104
105  SeeAlso     [Ntk_Init]
106
107******************************************************************************/
108void
109Ntk_End(void)
110{
111}
112
113
114/**Function********************************************************************
115
116  Synopsis    [Returns the current network of a hierarchy manager.]
117
118  Description [Returns the network of the current node of a hierarchy
119  manager. Assumes hmgr is non-NULL. If the current node or network is NULL,
120  then a message is printed to vis_stderr, and NULL is returned.]
121
122  SideEffects []
123
124  SeeAlso     [Hrc_ManagerReadCurrentNode]
125
126******************************************************************************/
127Ntk_Network_t *
128Ntk_HrcManagerReadCurrentNetwork(Hrc_Manager_t *hmgr)
129{
130  Hrc_Node_t *currentNode;
131  Ntk_Network_t *network;
132
133  assert(hmgr != NIL(Hrc_Manager_t));
134  currentNode = Hrc_ManagerReadCurrentNode(hmgr);
135  if (currentNode == NIL(Hrc_Node_t)) {
136    (void) fprintf(vis_stderr, "The hierarchy manager is empty.  Read in design.\n");
137    return NIL(Ntk_Network_t);
138  }
139
140  network = (Ntk_Network_t *) Hrc_NodeReadApplInfo(currentNode,
141                                                   NTK_HRC_NODE_APPL_KEY);
142  if (network == NIL(Ntk_Network_t)) {
143    (void) fprintf(vis_stdout, "There is no network. Use flatten_hierarchy.\n");
144    return NIL(Ntk_Network_t);
145  }
146
147  return network;
148}
149
150 
151/*---------------------------------------------------------------------------*/
152/* Definition of internal functions                                          */
153/*---------------------------------------------------------------------------*/
154
155
156/*---------------------------------------------------------------------------*/
157/* Definition of static functions                                            */
158/*---------------------------------------------------------------------------*/
159
160/**Function********************************************************************
161
162  Synopsis    [Implements the print_network_stats command.]
163
164  CommandName [print_network_stats]
165
166  CommandSynopsis [print statistics about the flattened network]
167
168  CommandArguments [\[-h\]]
169
170  CommandDescription [Prints the following statistics about the flattened
171  network:
172
173  <dl>
174 
175  <li> <b>name:</b> the name of the flattened network
176
177  <li> <b>combinational:</b> the number of nodes which have a table defining
178  the function of the node (excludes pseudo inputs)
179
180  <li> <b>primary inputs:</b> the number of primary input nodes of the
181  flattened network
182
183  <li> <b>primary outputs:</b> the number of primary output nodes of the
184  flattened network
185
186  <li> <b>latches:</b> the number of (multi-valued) latches
187
188  <li> <b>pseudo inputs:</b> the number of pseudo input nodes of the
189  flattened network
190
191  <li> <b>constants:</b> the number of combinational nodes that implement a
192  multi-valued constant
193
194  <li> <b>edges:</b> the number of fanouts in the network (e.g. if the output
195  of a node is used in two places, this contributes two to the sum)
196
197  </dl>
198
199  Note that <tt>flatten_hierarchy</tt> must be called before this command.<p>
200
201  Example output:
202  <pre>
203  small  combinational=2  pi=2  po=0  latches=1  pseudo=0  const=1  edges=4
204  </pre>
205
206  Command options:<p> 
207
208  <dl><dt> -h
209  <dd> Print the command usage.<p>
210  </dl>
211
212  ]
213 
214  SideEffects []
215
216******************************************************************************/
217static int
218CommandPrintNetworkStats(
219  Hrc_Manager_t ** hmgr,
220  int  argc,
221  char ** argv)
222{
223  int            c;
224  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
225
226  /*
227   * Parse the command line.
228   */
229  util_getopt_reset();
230  while ((c = util_getopt(argc, argv, "h")) != EOF) {
231    switch (c) {
232      case 'h':
233        goto usage;
234      default:
235        goto usage;
236    }
237  }
238 
239  if (network == NIL(Ntk_Network_t)) {
240    return 1;
241  }
242
243  Ntk_NetworkPrintStats(vis_stdout, network);
244  return 0;             /* normal exit */
245
246usage:
247  (void) fprintf(vis_stderr, "usage: print_network_stats [-h]\n");
248  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
249  return 1;             /* error exit */
250}
251
252
253/**Function********************************************************************
254
255  Synopsis    [Implements the print_network command.]
256
257  CommandName [print_network]
258
259  CommandSynopsis [print information about the flattened network]
260
261  CommandArguments [\[-f\] \[-h\] \[-t\]]
262
263  CommandDescription [Prints the name of the flattened network, and
264  information about each node.  For each node, prints the following:
265
266  <dl>
267
268  <li> <b>name:</b> the name of the node
269
270  <li> <b>mdd:</b> MDD id (-1 is uninitialized)
271
272  <li> <b>type:</b> one of combinational, primary-input, pseudo-input, latch,
273  or shadow
274
275  <li> <b>derived attributes:</b> list of derived attributes of the node
276
277  </dl>
278
279  See the ntk documentation for more information on types and attributes. The
280  following is an example describing information associated with a node.
281
282  <pre>
283  small.latch_in: mdd=2, combinational; data-input comb-output
284  </pre>
285
286  The flattened name of the node is "small.latch_in", its MDD id is 2, it is
287  of type combinational, and it is both a data input to a latch, and a
288  combinational output.<p>
289 
290  Command options:<p> 
291
292  <dl>
293
294  <dt> -f
295  <dd> Print the fanins and fanouts of each node.<p>
296
297  <dt> -h
298  <dd> Print the command usage.<p>
299
300  <dt> -t
301  <dd> Print table statistics for those nodes having tables.<p>
302
303  </dl>]
304
305  SideEffects []
306
307******************************************************************************/
308static int
309CommandPrintNetwork(
310  Hrc_Manager_t ** hmgr,
311  int  argc,
312  char ** argv)
313{
314  int            c;
315  boolean        printIo         = FALSE;  /* default */
316  boolean        printTableStats = FALSE;  /* default */
317  Ntk_Network_t *network         = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
318
319  /*
320   * Parse the command line.
321   */
322  util_getopt_reset();
323  while ((c = util_getopt(argc, argv, "fth")) != EOF) {
324    switch (c) {
325      case 'f':
326        printIo = TRUE;
327        break;
328      case 't':
329        printTableStats = TRUE;
330        break;
331      case 'h':
332        goto usage;
333      default:
334        goto usage;
335    }
336  }
337 
338  if (network == NIL(Ntk_Network_t)) {
339    return 1;
340  }
341
342  Ntk_NetworkPrint(vis_stdout, network, printIo, printTableStats);
343  return 0;             /* normal exit */
344
345usage:
346  (void) fprintf(vis_stderr, "usage: print_network [-f] [-h] [-t]\n");
347  (void) fprintf(vis_stderr, "   -f  print fanins and fanouts of nodes\n");
348  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
349  (void) fprintf(vis_stderr, "   -t  print table stats of nodes having tables\n");
350  return 1;             /* error exit */
351}
352
353
354/**Function********************************************************************
355
356  Synopsis    [Implements the print_network_dot command.]
357
358  CommandName [print_network_dot]
359
360  CommandSynopsis [print a dot description of the flattened network]
361
362  CommandArguments [\[-h\] &lt;file_name&gt;]
363
364  CommandDescription [Write a file in the format taken by the tool <tt>dot</tt>
365  depicting the topology of the network. Dot is a tool that given a description
366  of a graph in a certain format it produces a postscript print of the
367  graph. For more information about <tt>dot</tt> look in <a
368  href="http://www.research.att.com/orgs/ssr/book/reuse">
369  http://www.research.att.com/orgs/ssr/book/reuse</a>. Once a dot file is
370  produced with this command, the shell command <tt>dot -Tps <filename>
371  &gt;<file>.ps</tt> will produce the postscript file depicting the network.<p>
372
373  If no argument is specified on the command line, the description is written
374  to the standard output.<p>
375
376  Command options:<p>
377  <dl><dt> -h
378  <dd> Print the command usage.
379  </dl>]
380
381  SideEffects []
382
383******************************************************************************/
384static int
385CommandPrintNetworkDot(
386  Hrc_Manager_t ** hmgr,
387  int  argc,
388  char ** argv)
389{
390  FILE *fp;
391  int c, status;
392  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
393
394  util_getopt_reset();
395  while ((c = util_getopt(argc,argv,"h")) != EOF){
396    switch(c){
397      case 'h':
398        goto usage;
399      default:
400        goto usage;
401    }
402  }
403
404  /* Check if the network has been read in */
405  if (network == NIL(Ntk_Network_t)) {
406    return 1;
407  }
408
409  if (argc == 1) {
410    fp = stdout;
411  }
412  else if (argc == 2) {
413    fp = Cmd_FileOpen(*(++argv), "w", NIL(char *), /* silent */ 1);
414    if (fp == NIL(FILE)) {
415      (void) fprintf(vis_stderr, "Cannot write to %s\n", *argv);
416      return 1;
417    }
418  }
419  else {
420    goto usage;
421  }
422
423  error_init();
424  status = Ntk_NetworkPrintDot(fp, network);
425  (void) fprintf(vis_stderr, "%s", error_string());
426  fflush(fp);
427  if (fp != stdout) {
428    (void) fclose(fp);
429  }
430  return (status ? 0 : 1);
431
432 usage:
433  (void) fprintf(vis_stderr, "usage: print_network_dot [-h] [file]\n");
434  (void) fprintf(vis_stderr, "    -h\t\tprint the command usage\n");
435  return 1;
436}
437
438
439/**Function********************************************************************
440
441  Synopsis    [Write a (flattened) network in blif-MV format.]
442
443  CommandName [write_network_blif_mv]
444
445  CommandSynopsis [write a blif-MV description of the flattened network]
446
447  CommandArguments [\[-h\] \[-p\] &lt;file_name&gt;]
448
449  CommandDescription [Write a file in Blif-MV format describing the
450  network. <p>
451
452  If no argument is specified on the command line, the description is written
453  to the vis standard output.<p>
454
455  Command options:<p>
456  <dl><dt> -h
457  <dd> Print the command usage.
458  <dt> -p
459  <dd> Promote pseudo inputs to primary inputs.
460  </dl>]
461
462  SideEffects []
463
464******************************************************************************/
465static int
466CommandWriteNetworkBlifMv(
467  Hrc_Manager_t ** hmgr,
468  int  argc,
469  char ** argv)
470{
471  FILE *fp;
472  int c;
473  boolean promotePseudo = FALSE;
474  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
475
476  /* Check whether the network has been created. */
477  if (network == NIL(Ntk_Network_t)) {
478    return 1;
479  }
480
481  util_getopt_reset();
482  while ((c = util_getopt(argc,argv,"hp")) != EOF){
483    switch(c){
484    case 'h':
485      goto usage;
486    case 'p':
487      promotePseudo = TRUE;
488      argv++;
489      argc--;
490      break;
491    default:
492      goto usage;
493    }
494  }
495
496  if (argc == 1) {
497    fp = vis_stdout;
498  } else if (argc == 2) {
499    fp = Cmd_FileOpen(*(++argv), "w", NIL(char *), /* silent */ 1);
500    if (fp == NIL(FILE)) {
501      (void) fprintf(vis_stderr, "Cannot write to %s\n", *argv);
502      return 1;
503    }
504  } else {
505    goto usage;
506  }
507
508  error_init();
509  Ntk_NetworkWriteBlifMv(fp, network, promotePseudo);
510  (void) fprintf(vis_stderr, "%s", error_string());
511  fflush(fp);
512  if (fp != vis_stdout) {
513    (void) fclose(fp);
514  }
515  return 1;
516
517 usage:
518  (void) fprintf(vis_stderr, "usage: write_network_blif_mv [-h] [file]\n");
519  (void) fprintf(vis_stderr, "    -h\t\tprint the command usage\n");
520  (void) fprintf(vis_stderr, "    -p\t\tpromote pseudo inputs to primary inputs\n");
521  return 1;
522
523} /* CommandWriteNetworkBlifMv */
524
525
526/**Function********************************************************************
527
528  Synopsis    [Implements the flatten_hierarchy command.]
529
530  CommandName [flatten_hierarchy]
531
532  CommandSynopsis [create a flattened network]
533
534  CommandArguments [\[-a &lt;file&gt;\] \[-b\] \[-h\] \[-s\] \[-v #\]]
535
536  CommandDescription [Creates a flattened network from a hierarchical
537  description.  The flattened network encompasses everything from the
538  current node of the hierarchy (reached by the command <tt>cd</tt>),
539  down to and including the leaves.  It creates a view with the
540  hierarchy removed, but retains the multi-level logic structure.  The
541  resulting flattened network is stored with the current node. Every
542  table in the flattened network is checked whether it is completely
543  specified and deterministic. This is the starting point for
544  verification related commands. <p>
545
546  A limited form of abstraction can be done by providing a list of variables
547  to treat as primary inputs.  See the information under &lt;file&gt;
548  below.<p>
549 
550  The verification part of VIS requires the functions specified by the BLIF-MV
551  tables to be completely specified and deterministic.  These conditions are
552  checked during the flattening process; if a table is found that is
553  incompletely specified or is nondeterministic, then an error message is
554  written and a flattened network is not created.  The exception to this
555  rule is tables specifying "pseudo inputs"; these are tables with no inputs,
556  and a single output that can take more than one value.  Such tables are
557  generated by vl2mv to model the "$ND" construct in Verilog.<p>
558 
559  If this command is invoked a second time from the same point in the
560  hierarchy, the previous network is deleted and a new one is created.  This
561  is the tactic to follow if you want to change some aspect of the current
562  network, such as MDD variable ordering or <tt>image_method</tt>.<p>
563
564  Command options:<p> 
565
566  <dl>
567
568  <dt> -a &lt;file&gt;
569
570  <dd> A file containing names of variables, used to specify which variables
571  to abstract. The name of a variable is the full hierarchical path name,
572  starting from just after the current hierarchy node (i.e., if the current
573  node is foo, and you want to refer to variable x in foo, then just use x).
574  A variable should appear at most once in the file.  Each variable name
575  should appear at the beginning of a new line, with no white space preceding
576  it.  The end of a variable name is marked by white space, and any other text
577  on the rest of the line is ignored.  Any line starting with "#" or white
578  space is ignored.  A sample file is shown here.<p>
579
580  <pre>
581  # variables to abstract to model check liveness property
582  choosing0
583  p0.pc     
584  </pre>
585
586  For each variable x appearing in the file, a new primary input node named
587  x$ABS is created to drive all the nodes that were previously driven by x.
588  Hence, the node x will not have any fanouts; however, x and its transitive
589  fanins will remain in the network. <p>
590
591  Abstracting a net effectively allows it to take any value in its range, at
592  every clock cycle. This mechanism can be used to perform manual
593  abstractions.  The variables to abstract should not affect the correctness
594  of the property being checked.  This usually simplifies the network, and
595  permits some verification tasks to complete that would not otherwise.  Note,
596  however, that by increasing the behavior of the system, false negatives are
597  possible when checking universal properties, and false positives are
598  possible when checking existential properties. <p>
599
600  A convenient way of generating the hierarchical variable names is by using
601  the write_order command. Note that abstracting next state variables has no
602  effect.<p>
603
604
605  <dt> -b
606  <dd> This option has no effect any longer.<p>
607
608  <dt> -h
609  <dd> Print the command usage. <p>
610
611  <dt> -s
612  <dd> Do not perform a sweep. <p>
613
614  <dt> -v #
615  <dd> Print debug information.
616  <dd>
617
618  0: (default) Nothing is printed out.<p>
619 
620  >= 2: Prints the variables read from the input file.<p>
621 
622 
623  </dl>
624
625  ]
626 
627  SideEffects []
628
629******************************************************************************/
630static int
631CommandFlattenHierarchy(
632  Hrc_Manager_t ** hmgr,
633  int  argc,
634  char ** argv)
635{
636  int            c;
637  Ntk_Network_t *network;
638  char          *fileName    = NIL(char);
639  int            verbose     = 0;       /* default */
640  int            sweep       = 1; 
641  lsList         varNameList = (lsList) NULL;
642  Hrc_Node_t    *currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
643 
644  /*
645   * Parse the command line.
646   */
647  util_getopt_reset();
648  while ((c = util_getopt(argc, argv, "a:bhsv:")) != EOF) {
649    switch (c) {
650      case 'a':
651        fileName = util_optarg;
652        break;
653      case 'b':
654        break;
655      case 'h':
656        goto usage;
657      case 's':
658        sweep = 0;
659        break;       
660      case 'v':
661        verbose = atoi(util_optarg);
662        break;
663      default:
664        goto usage;
665    }
666  }
667
668  if (currentNode == NIL(Hrc_Node_t)) { 
669    (void) fprintf(vis_stdout, "The hierarchy manager is empty.  Read in design.\n");
670    return 1;
671  }
672   
673  /*
674   * Process the file containing the variable names.
675   */
676  if (fileName != NIL(char)) {
677    FILE *fp = Cmd_FileOpen(fileName, "r", NIL(char *), 0);
678    if (fp == NIL(FILE)) {
679      return 1;
680    }
681    else {
682      boolean status;
683     
684      error_init();
685      status = FileReadNameList(fp, &varNameList, verbose);
686      (void) fclose(fp);
687      if (status == FALSE) {
688        (void) fprintf(vis_stderr, "Error reading variable name file:\n");
689        (void) fprintf(vis_stderr, "%s", error_string());
690        (void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
691        return 1;
692      }
693    }
694  }
695
696 
697  /*
698   * If a network already exists, delete it.  Then create the new one, and
699   * register it with the hrcNode.
700   */
701  network = (Ntk_Network_t *) Hrc_NodeReadApplInfo(currentNode,
702                                                   NTK_HRC_NODE_APPL_KEY);
703  if (network != NIL(Ntk_Network_t)) {
704    (void) fprintf(vis_stdout, "Deleting current network and creating new one.\n");
705    Hrc_NodeFreeApplInfo(currentNode, NTK_HRC_NODE_APPL_KEY);
706  }
707
708  error_init();
709
710  network = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, varNameList);
711
712  /* Clean up the varNameList. */
713  if (varNameList != (lsList) NULL) {
714    lsGen  gen;
715    char  *varName;
716   
717    lsForEachItem(varNameList, gen, varName) {
718      FREE(varName);
719    }
720    (void) lsDestroy(varNameList, (void (*) (lsGeneric)) NULL);
721  }
722  /* sweep network */
723  if (network != NIL(Ntk_Network_t) && sweep ==1) {
724    Ntk_NetworkSweep(network, verbose); 
725  }
726 
727  if (network == NIL(Ntk_Network_t)) {
728    (void) fprintf(vis_stderr, "%s", error_string());
729    (void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
730    return 1;
731  }
732 
733  Hrc_NodeAddApplInfo(currentNode, NTK_HRC_NODE_APPL_KEY,
734                      (Hrc_ApplInfoFreeFn) Ntk_NetworkFreeCallback,
735                      (Hrc_ApplInfoChangeFn) NULL,  /* not currently used by hrc */
736                      (void *) network);
737
738  return 0;             /* normal exit */
739
740usage:
741  (void) fprintf(vis_stderr, "usage: flatten_hierarchy [-a file] [-b] [-h] [-s] [-v #]\n");
742  (void) fprintf(vis_stderr, "   -a file  variables to abstract\n");
743  (void) fprintf(vis_stderr, "   -b       not used any longer\n");
744  (void) fprintf(vis_stderr, "   -h       print the command usage\n");
745  (void) fprintf(vis_stderr, "   -s       do not perform a sweep\n"); 
746  (void) fprintf(vis_stderr, "   -v #     verbosity level\n");
747  return 1;             /* error exit */
748}
749
750
751/**Function********************************************************************
752
753  Synopsis    [Implements the test_network_acyclic command.]
754
755  CommandName [test_network_acyclic]
756
757  CommandSynopsis [determine whether the network is acyclic]
758
759  CommandArguments [\[-h\]]
760
761  CommandDescription [If the flattened network has a combinational
762  cycle, then prints information about one of the cycles.  If no cycles are
763  present, then it prints a message to this effect.<p> 
764
765  Command options:<p> 
766
767  <dl><dt> -h
768  <dd> Print the command usage.<p>
769  </dl>
770  ]
771 
772  SideEffects []
773
774******************************************************************************/
775static int
776CommandTestNetworkAcyclic(
777  Hrc_Manager_t ** hmgr,
778  int  argc,
779  char ** argv)
780{
781  int            c;
782  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
783
784  /*
785   * Parse the command line.
786   */
787  util_getopt_reset();
788  while ((c = util_getopt(argc, argv, "h")) != EOF) {
789    switch (c) {
790      case 'h':
791        goto usage;
792      default:
793        goto usage;
794    }
795  }
796 
797  if (network == NIL(Ntk_Network_t)) {
798    return 1;
799  }
800
801  error_init();
802  if (Ntk_NetworkTestIsAcyclic(network) == 0) {
803    (void) fprintf(vis_stdout, "Combinational cycle found: ");
804    (void) fprintf(vis_stdout, "%s", error_string());
805    (void) fprintf(vis_stdout, "\n");
806  }
807  else {
808    (void) fprintf(vis_stdout, "Network has no combinational cycles\n");
809  }
810  return 0;             /* normal exit */
811
812
813usage:
814  (void) fprintf(vis_stderr, "usage: test_network_acyclic [-h]\n");
815  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
816  return 1;             /* error exit */
817}
818
819
820/**Function********************************************************************
821
822  Synopsis    [Implements the init_verify command.]
823
824  CommandName [init_verify]
825
826  CommandSynopsis [create and initialize a flattened network for verification]
827
828  CommandArguments [\[-b\] \[-h\]]
829
830  CommandDescription [This command initializes the system for verification,
831  and is equivalent to the command sequence <tt>flatten_hierarchy;
832  static_order; build_partition_mdds</tt>.  If a command returns an error
833  condition, then the sequence is aborted.  After <tt>init_verify</tt> has
834  successfully executed, various commands can be invoked, like
835  <tt>model_check</tt>, <tt>compute_reach</tt>, <tt>simulate</tt>,
836  <tt>print_network_stats</tt>, and <tt>seq_verify</tt>.<p>
837
838  Please note that init_verify does not enable dynamic variable
839  reordering. Sometimes, though, this is needed to complete building
840  the partitions, and one has to initialize the verification by hand.
841  Similarly, it may be wise to turn on dynamic variable reordering after
842  init, so that further commands complete more easily. See the help page
843  for <tt>dynamic_var_ordering</tt>.
844
845
846  <p>Command options:<p> 
847
848  <dl><dt> -b
849  <dd> This option has no effect any longer. <p>
850  </dl>
851  <dl><dt> -h
852  <dd> Print the command usage.<p>
853  </dl>
854
855  ]
856 
857  SideEffects []
858
859******************************************************************************/
860static int
861CommandInitVerify(
862  Hrc_Manager_t ** hmgr,
863  int  argc,
864  char ** argv)
865{
866  int         c;
867  Hrc_Node_t *currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
868 
869  /*
870   * Parse the command line.
871   */
872  util_getopt_reset();
873  while ((c = util_getopt(argc, argv, "bh")) != EOF) {
874    switch (c) {
875      case 'b':
876        break;
877      case 'h':
878        goto usage;
879      default:
880        goto usage;
881    }
882  }
883
884  if (currentNode == NIL(Hrc_Node_t)) { 
885    (void) fprintf(vis_stdout, "The hierarchy manager is empty.  Read in design.\n");
886    return 1;
887  }
888   
889  /*
890   * Call the commands one-by-one, returning upon the first error.
891   */
892  if (Cmd_CommandExecute(hmgr, "flatten_hierarchy")) {
893    return 1;
894  }
895 
896  if (Cmd_CommandExecute(hmgr, "static_order")) {
897    return 1;
898  }
899 
900  if (Cmd_CommandExecute(hmgr, "build_partition_mdds")) {
901    return 1;
902  }
903 
904  return 0;             /* normal exit */
905
906
907usage:
908  (void) fprintf(vis_stderr, "usage: init_verify [-b] [-h]\n");
909  (void) fprintf(vis_stderr, "   -b  not used any longer.\n");
910  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
911  return 1;             /* error exit */
912}
913
914
915/**Function********************************************************************
916
917  Synopsis    [Implements the network_sweep command.]
918
919  CommandName [network_sweep]
920
921  CommandSynopsis [sweeps the network to ensure that deterministic constants
922  are removed]
923
924  CommandArguments [\[-h\]\[-v\]]
925
926  CommandDescription [This function performs a sweep on the given
927  Ntk_Network_t. It propagates all the deterministic constant nodes, and
928  removes all buffer nodes. It modifies the network.
929
930  Command options:<p> 
931
932  <dl><dt> -h
933  <dd> Print the command usage.<p>
934  </dl>
935
936  <dl><dt> -v
937  <dd> Print debug information.<p>
938  </dl>
939  ]
940 
941  SideEffects []
942
943******************************************************************************/
944static int
945CommandNetworkSweep(
946  Hrc_Manager_t ** hmgr,
947  int  argc,
948  char ** argv)
949{
950  int           c;
951  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
952  int           verbosity = 0;
953
954  /*
955   * Parse the command line.
956   */
957  util_getopt_reset();
958  while ((c = util_getopt(argc, argv, "hv")) != EOF) {
959    switch (c) {
960      case 'h':
961        goto usage;
962      case 'v':
963        verbosity = 1;
964        break;
965      default:
966        goto usage;
967    }
968  }
969 
970  if (network == NIL(Ntk_Network_t)) {
971    return 1;
972  }
973 
974  Ntk_NetworkSweep(network, verbosity);
975  return 0;
976
977usage:
978  (void) fprintf(vis_stderr, "usage: network_sweep [-h][-v]\n");
979  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
980  (void) fprintf(vis_stderr, "   -v  print debug information\n"); 
981  return 1;             /* error exit */
982}
983
984/**Function********************************************************************
985
986  Synopsis    [Returns a list of names corresponding to the names in a file.]
987
988  Description [Parses a file and builds a name list corresponding to the names
989  found in the first "column" of each line of the file.  Any line starting
990  with the comment character '#' or white space is ignored.  No checks are
991  made to see if the names are well-formed in any respect. If a problem is
992  found while parsing the file (e.g. name length exceeded), then a message is
993  written to error_string, the partial name list is freed, and the function
994  returns FALSE; otherwise, it returns TRUE, and a pointer to a list is
995  returned.]
996
997  Comment [The parser consists of 3 states.  See the documentation
998  accompanying the #defines defining the state names.  This code was adapted
999  from Ord_FileReadNodeList.]
1000 
1001  SideEffects []
1002
1003******************************************************************************/
1004static boolean
1005FileReadNameList(
1006  FILE * fp,
1007  lsList * nameList /* of char *, for return */,
1008  int verbose)
1009{
1010  int     c;
1011  int     state;
1012  int     curPosition = 0;
1013  char   *name;
1014  char    string[MAX_NAME_LENGTH];
1015  boolean returnFlag = TRUE;
1016 
1017  *nameList = lsCreate();
1018
1019  state = STATE_TEST;
1020  while ((c = fgetc(fp)) != EOF) {
1021
1022    switch (state) {
1023      case STATE_TEST:
1024        /* At start of a new line. */
1025        if (c == '#') {
1026          /* Line starting with comment character; wait for newline */
1027          state = STATE_WAIT;
1028        }
1029        else if ((c == ' ') || (c == '\t')) {
1030          /* Line starting with white space; wait for newline */
1031          state = STATE_WAIT;
1032        }
1033        else if (c == '\n') {
1034          /* Line starting with newline; go to next line */
1035          state = STATE_TEST;
1036        }
1037        else {
1038          /* Assume starting a name. */
1039          curPosition = 0;
1040          string[curPosition++] = c;
1041          state = STATE_IN;
1042        }
1043        break;
1044      case STATE_WAIT:
1045        /*
1046         * Waiting for the newline character.
1047         */
1048        state = (c == '\n') ? STATE_TEST : STATE_WAIT;
1049        break;
1050      case STATE_IN:
1051        /*
1052         * Parsing a name.  If white space reached, then terminate the
1053         * name and process it.  Else, continue parsing.
1054         */
1055        if ((c == ' ') || (c == '\n') || (c == '\t')) {
1056          string[curPosition] = '\0';
1057          name = util_strsav(string);
1058          if (verbose > 1) {
1059            (void) fprintf(vis_stdout, "Reading name: %s\n", name);
1060          }
1061          (void) lsNewEnd(*nameList, (lsGeneric) name, LS_NH); 
1062         
1063          state = (c == '\n') ? STATE_TEST : STATE_WAIT;
1064        }
1065        else {
1066          string[curPosition++] = c;
1067          if (curPosition >= MAX_NAME_LENGTH) {
1068            error_append("maximum name length exceeded");
1069            returnFlag = FALSE;
1070          }
1071          state = STATE_IN; /* redundant, but be explicit */
1072        }
1073        break;
1074      default:
1075        fail("unrecognized state");
1076    }
1077  }
1078
1079  /*
1080   * Handle case where EOF terminates a name.
1081   */
1082  if (state == STATE_IN) {
1083    string[curPosition] = '\0';
1084    name = util_strsav(string);
1085    if (verbose > 1) {
1086      (void) fprintf(vis_stdout, "Reading name: %s\n", name);
1087    }
1088    (void) lsNewEnd(*nameList, (lsGeneric) name, LS_NH); 
1089         
1090  }
1091
1092  if (returnFlag) {
1093    return TRUE;
1094  }
1095  else {
1096    (void) lsDestroy(*nameList, (void (*) (lsGeneric)) NULL);
1097    return FALSE;
1098  }
1099}
1100
1101 
Note: See TracBrowser for help on using the repository browser.