source: vis_dev/vis-2.3/src/ord/ordCmd.c @ 45

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

vis2.3

File size: 55.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ordCmd.c]
4
5  PackageName [ord]
6
7  Synopsis    [Command interface to the ordering package.]
8
9  Author      [Adnan Aziz, Tom Shiple, Serdar Tasiran]
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 "ordInt.h"
33
34static char rcsid[] UNUSED = "$Id: ordCmd.c,v 1.37 2005/05/19 03:22:55 awedh Exp $";
35
36/*---------------------------------------------------------------------------*/
37/* Variable declarations                                                     */
38/*---------------------------------------------------------------------------*/
39static jmp_buf timeOutEnv;
40
41
42/**AutomaticStart*************************************************************/
43
44/*---------------------------------------------------------------------------*/
45/* Static function prototypes                                                */
46/*---------------------------------------------------------------------------*/
47
48static int CommandStaticOrder(Hrc_Manager_t ** hmgr, int argc, char ** argv);
49static int CommandReadOrder(Hrc_Manager_t ** hmgr, int argc, char ** argv);
50static int CommandWriteOrder(Hrc_Manager_t ** hmgr, int argc, char ** argv);
51static int CommandDynamicVarOrdering(Hrc_Manager_t ** hmgr, int argc, char ** argv);
52static int CommandPrintBddStats(Hrc_Manager_t ** hmgr, int argc, char ** argv);
53static Ord_OrderType StringConvertToOrderType(char *string);
54static bdd_reorder_type_t StringConvertToDynOrderType(char *string);
55static char * DynOrderTypeConvertToString(bdd_reorder_type_t method);
56static boolean NetworkCheckSuppliedNodeList(Ntk_Network_t * network, lsList suppliedNodeList, Ord_OrderType orderType);
57static void TimeOutHandle(void);
58
59/**AutomaticEnd***************************************************************/
60
61
62/*---------------------------------------------------------------------------*/
63/* Definition of exported functions                                          */
64/*---------------------------------------------------------------------------*/
65
66/**Function********************************************************************
67
68  Synopsis    [Initializes the order package.]
69
70  SideEffects []
71
72  SeeAlso     [Ord_End]
73
74******************************************************************************/
75void
76Ord_Init(void)
77{
78  Cmd_CommandAdd("static_order", CommandStaticOrder, 0);
79  Cmd_CommandAdd("read_order", CommandReadOrder, 0);
80  Cmd_CommandAdd("write_order", CommandWriteOrder, 0);
81  Cmd_CommandAdd("dynamic_var_ordering", CommandDynamicVarOrdering, 0);
82  Cmd_CommandAdd("print_bdd_stats", CommandPrintBddStats, 0);
83}
84
85
86/**Function********************************************************************
87
88  Synopsis    [Ends the order package.]
89
90  SideEffects []
91
92  SeeAlso     [Ord_Init]
93
94******************************************************************************/
95void
96Ord_End(void)
97{
98}
99
100
101/**Function********************************************************************
102
103  Synopsis    [Checks that all nodes corresponding to orderType have MDD ids.]
104
105  Description [For each node of network that falls in the class given by
106  orderType, checks that the node has an MDD id.  If all such nodes have MDD
107  ids, return 1, else returns 0.  orderType can have one of 3 values:
108  Ord_All_c, checks all nodes of network; Ord_InputAndLatch_c, checks all
109  combinational inputs and latch next states; Ord_NextStateNode_c, checks all
110  next state nodes.  Returns 0 on the first such node not having an MDD id,
111  and writes an error message in error_string.  Also returns 0 if the network
112  doesn't have an MDD manager.]
113
114  SideEffects []
115
116******************************************************************************/
117boolean
118Ord_NetworkTestAreVariablesOrdered(
119  Ntk_Network_t * network,
120  Ord_OrderType  orderType)
121{
122  lsGen          gen;
123  Ntk_Node_t    *node;
124  mdd_manager   *mddManager = Ntk_NetworkReadMddManager(network);
125 
126  assert((orderType == Ord_All_c) || (orderType == Ord_InputAndLatch_c)
127         || (orderType == Ord_NextStateNode_c));
128
129  if (mddManager == NIL(mdd_manager)) {
130    error_append("network doesn't have an MDD manager\n");
131  return 0;
132  }
133
134  /*
135   * Next state nodes are included by all 3 order types.
136   */
137  Ntk_NetworkForEachNode(network, gen, node) {
138    if ((orderType == Ord_All_c) || Ntk_NodeTestIsNextStateNode(node)) {
139      if (Ntk_NodeReadMddId(node) == NTK_UNASSIGNED_MDD_ID) {
140        error_append("node ");
141        error_append(Ntk_NodeReadName(node));
142        error_append(" not ordered\n");
143        (void) lsFinish(gen);
144        return 0;
145      }
146    }
147    else if ((orderType == Ord_InputAndLatch_c)
148             && Ntk_NodeTestIsCombInput(node)) {
149      if (Ntk_NodeReadMddId(node) == NTK_UNASSIGNED_MDD_ID) {
150        error_append("node ");
151        error_append(Ntk_NodeReadName(node));
152        error_append(" not ordered\n");
153        (void) lsFinish(gen);
154        return 0;
155      }
156    }
157    /* else, this node is not included by orderType */
158  }
159
160  return 1;
161}
162
163
164/*---------------------------------------------------------------------------*/
165/* Definition of internal functions                                          */
166/*---------------------------------------------------------------------------*/
167
168
169/*---------------------------------------------------------------------------*/
170/* Definition of static functions                                            */
171/*---------------------------------------------------------------------------*/
172
173/**Function********************************************************************
174
175  Synopsis    [Implements the static_order command.]
176
177  SideEffects []
178
179  CommandName [static_order]
180
181  CommandSynopsis [order the MDD variables of the flattened network]
182
183  CommandArguments [\[-a\] \[-h\] \[-n <method>\] \[-o <type>\]
184  \[-r <method>\] -s <type> \[-t <timeOut>\] \[-v #\]
185  <file>]
186
187  CommandDescription [Order the MDD variables of the flattened network.  MDD
188  variables must be created before MDDs can be built.  Networks with
189  combinational cycles cannot be ordered.  If the MDD variables have already
190  been ordered, then this command does nothing.  To undo the current ordering,
191  reinvoke the command <tt>flatten_hierarchy</tt>.
192  <p>
193 
194
195  Command options:<p>
196
197  <dl>
198
199  <dt> -a
200  <dd> Order each next state variable immediately following the variables in
201  the support of the corresponding next state function.  By default, each next
202  state variable is placed immeadiately following the corresponding present
203  state variable.  It has been observed experimentally that ordering the NS
204  variable after the PS variable is almost always better; however, as a last
205b  resort, you might want to try this option.<p>
206
207  Unless the -a flag is set, the PS and NS variables corresponding to latches
208  are grouped together and cannot be separated by dynamic reordering. (This is
209  done even when the ordering is read from a file - adjacent PS/NS vars in the
210  file are grouped).<p>
211 
212  <dt> -h
213  <dd> Print the command usage.<p>
214 
215  <dt> -n &lt;method&gt;
216
217  <dd> Specify which node ordering method to use.  Node ordering is the
218  process of computing a total ordering on all the network nodes.  This
219  ordering is then projected onto the set of nodes specified by <tt>-o
220  type</tt>. In the complexity measures below, n is the number of network
221  nodes, E is the number of network edges, and k is the number of
222  latches. "Method" must be one of the following:<p>
223
224  <b>interleave:</b> (default) Uses Algorithm 2 of Fujii et al.,
225  "Interleaving Based Variable Ordering Methods for OBDDs", ICCAD 1993.
226  The complexity is O(E+nlog(n)).<p>
227
228  <b>append:</b> Uses the algorithm of Malik, et al. "Logic Verification using
229  Binary Decision Diagrams in a Logic Synthesis Environment," ICCAD,
230  1988. Nodes are visited in DFS order, and appended to a global order list in
231  the order they are visited.  The fanins of a node are visited in order of
232  decreasing depth. The roots of the DFS are visited in the order determined
233  by the <tt>-r method</tt>.  The complexity is O(E+nlog(n)).<p>
234 
235  <b>merge_left:</b> Uses an algorithm alluded to in Fujii et al.,
236  "Interleaving Based Variable Ordering Methods for OBDDs", ICCAD 1993. Nodes
237  are visited in DFS order.  At a given node g, its fanins are visited in
238  order of decreasing depth.  For each fanin fi, a total order is computed for
239  all the nodes in the transitive fanin (TFI) of fi, including fi itself.
240  This ordering is merged into the combined ordering from fanins of higher
241  priority.  After processing all of the fanins, the result is a total
242  ordering on all TFI nodes of g.  Finally, g is appended to the end of this
243  ordering, yielding a topological ordering. For example if the ordering for
244  f1 is list1 = (a,b,d,f1) and for f2 is list2=(c,d,e,f2), and f1 has greater
245  depth than f2, then the ordering for g is (c,a,b,d,e,f2,f1,g). The merge is
246  done by inserting into list1 those nodes in list2 not already in list1, in
247  such a way that the inserted nodes remain as close as possible to their left
248  neighbors in list2 ("insert as far left as possible"). The roots of the DFS
249  are merged in the order determined by <tt>-r method</tt>.  The complexity is
250  O(n^2) (currently, there is a bug which causes more memory to be consumed
251  than necessary).<p>
252
253  <b>merge_right:</b> Same as <tt>merge_left</tt>, except that the merge is
254  done in such a way that the inserted nodes remain as close as possible to
255  their right neighbors in list2 ("insert as far right as possible"). For the
256  example above, the ordering for g is (a,b,c,d,f1,e,f2,g).  It has been
257  observed experimentally that neither <tt>merge_left</tt> nor
258  <tt>merge_right</tt> is superior to the other; there are cases where
259  verification times out with <tt>merge_left</tt> but not
260  <tt>merge_right</tt>, and vice versa.<p>
261
262
263  <dt> -o &lt;type&gt; <dd> Specify the network nodes for which MDD variables
264  should be created.  Type can be one of the following:<p>
265
266  <b>all:</b> Order all the nodes of the network.  This is normally not used.<p>
267
268  <b>input_and_latch:</b> (default) Order the primary inputs, pseudo
269  inputs, latches, and next state variables.  This is the minimum set of nodes
270  that need to be ordered to perform operations on FSMs (e.g. model checking,
271  reachability).  For purely combinational circuits, just the primary and
272  pseudo inputs are ordered.<p>
273
274 
275  <dt> -r &lt;method&gt;
276
277  <dd> Specify which root ordering method to use.  The "roots" of a network
278  refer to the roots of the cones of logic driving the combinational outputs
279  (data latch inputs, initial state latch inputs, and primary outputs) of a
280  network. Root ordering is used to determine in which order to visit the
281  roots of the network for the DFS carried out in node ordering (see
282  <tt>-n</tt>). "Method" must be one of the following:<p>
283
284  <b>depth:</b> (default for 30 or more latches) Roots are ordered based on
285  logic depth (i.e. longest path to a combinational input).  Greater depth
286  roots appear earlier in the ordering. All data latch inputs appear before
287  all other combinational outputs. The complexity is O(E+nlog(n)). It has been
288  observed experimentally that <tt>mincomm</tt> produces superior orderings to
289  <tt>depth</tt>.  However, the complexity of the <tt>mincomm</tt> algorithm
290  is such that it cannot produce orderings for designs with more than a
291  hundred or so latches.  Hence, for big designs, use <tt>depth</tt>, followed
292  optionally by <tt>dynamic_var_ordering</tt>.<p>
293
294  <b>mincomm:</b> (default for less than 30 latches) Uses the algorithm of
295  Aziz, et al. "BDD Variable Ordering for Interacting Finite State Machines,"
296  DAC, 1994. First, the latches are ordered to decrease a communication
297  complexity bound (where backward edges are more expensive than forward
298  edges) on the latch communication graph. This directly gives an ordering for
299  the data latch inputs.  The remaining combinational outputs are ordered
300  after the data latch inputs, in decreasing order of their depth. The total
301  complexity is O(nlog(n)+E+k^3).<p>
302
303
304  <dt> -s &lt;type&gt;
305
306  <dd> Used in conjunction with <tt>&lt;file&gt;</tt> to specify which
307  nodes are supplied in the ordering file. Type can be one of the following
308  (there is no default):<p>
309
310  <b>all:</b> The ordering file supplies all the nodes of the network.
311  The ordering generated is the supplied order, projected onto the set of nodes
312  specified by <tt>-o</tt>.<p>
313
314  <b>input_and_latch:</b> The ordering file supplies the primary inputs,
315  pseudo inputs, latches, and next state variables. The ordering generated is
316  exactly what is supplied (in the case of <tt>-o input_and_latch</tt>). <tt>-o
317  all</tt> is incompatible with <tt>-s input_and_latch</tt>.<p>
318
319  <b>next_state_node:</b> The ordering file supplies next state
320  variables. During the ordering algorithm, the next state functions are
321  visited in the order in which their corresponding next state variables
322  appear in the file. The order of the next state variables in the ordering
323  generated is not necessarily maintained.<p>
324
325  <b>partial:</b> The ordering file supplies an arbitrary subset of nodes
326  of the network. The ordering algorithm works by finding a total ordering on
327  all the nodes (independent of the ordering supplied), then merging the
328  computed order into the supplied order (maintaining the relative order of
329  the supplied order), and then projecting the resulting ordering onto the set
330  of nodes specified by <tt>-o</tt>.<p>
331 
332
333  <dt> -t &lt;timeOut&gt;
334  <dd> Time in seconds allowed to perform static ordering.  If the flattened
335  network has more than a couple hundred latches and you are using option
336  <tt>-r mincomm</tt>, then you might want to set a timeOut to limit the
337  allowed time.  The default is no limit.<p>
338
339  <dt> -v #
340  <dd> Print debug information.
341  <dd>
342
343  0 Nothing is printed out.  This is the default.<p>
344 
345  >= 1 Prints the nodes read from the input file (satisfying the supplied
346  order type); prints the root order used for exploring the network.<p>
347 
348  >= 2 Prints the depth of nodes.<p>
349 
350  >= 3 Prints the ordering computed at each node.<p>
351
352 
353  <dt> &lt;file&gt;
354
355  <dd> A file containing names of network nodes, used to specify a variable
356  ordering. The name of a node is the full hierarchical path name, starting
357  from the current hierarchical node.  A node should appear at most once in
358  the file.  Each node name should appear at the beginning of a new line, with
359  no white space preceeding it.  The end of a node name is marked by white
360  space, and any other text on the rest of the line is ignored.  Any line
361  starting with "#" or white space is ignored. See <tt>write_order</tt>
362  for a sample file. Note that the variable ordering cannot be specified at
363  the bit-level; it can only be specified at the multi-valued variable level.
364
365  </dl>
366  ]
367
368 
369  SeeAlso     [CommandWriteOrder]
370
371******************************************************************************/
372static int
373CommandStaticOrder(
374  Hrc_Manager_t ** hmgr,
375  int  argc,
376  char ** argv)
377{
378  int                   c;
379  FILE                 *fp;
380  static int            timeOutPeriod;
381  static int            verbose;
382  static Ord_NodeMethod nodeMethod;
383  static Ord_RootMethod rootMethod;
384  static Ord_OrderType  suppliedOrderType;
385  static Ord_OrderType  generatedOrderType;
386  static boolean        nsAfterSupport;
387  lsList                suppliedNodeList = (lsList) NULL;
388                                /* list of Ntk_Node_t * */
389  Ntk_Network_t        *network;
390
391  /*
392   * These are the default values.  These variables must be declared static
393   * to avoid lint warnings.  Since they are static, we must reinitialize
394   * them outside of the variable declarations.
395   */
396  timeOutPeriod      = 0; 
397  verbose            = 0;
398  nodeMethod         = Ord_NodesByDefault_c;
399  rootMethod         = Ord_RootsByDefault_c;
400  suppliedOrderType  = Ord_Unassigned_c;   /* default */
401  generatedOrderType = Ord_InputAndLatch_c;/* default */
402  nsAfterSupport     = FALSE;              /* default */
403 
404  /*
405   * Parse the command line.
406   */
407  util_getopt_reset();
408  while ((c = util_getopt(argc, argv, "av:o:s:t:n:r:h")) != EOF) {
409    switch (c) {
410      case 'a':
411        nsAfterSupport = TRUE;
412        break;
413      case 'h':
414        goto usage;
415      case 'v':
416        verbose = atoi(util_optarg);
417        break;
418      case 't':
419        timeOutPeriod = atoi(util_optarg);
420        break;
421      case 'o':
422        generatedOrderType = StringConvertToOrderType(util_optarg);
423        if ((generatedOrderType == Ord_NextStateNode_c)
424            || (generatedOrderType == Ord_Partial_c)) { 
425          (void) fprintf(vis_stderr, "disallowed output order type: %s\n", util_optarg);
426          goto usage;
427        }
428        else if (generatedOrderType == Ord_Unassigned_c) {
429          (void) fprintf(vis_stderr, "unknown output order type: %s\n", util_optarg);
430          goto usage;
431        }
432        break;
433      case 's':
434        suppliedOrderType = StringConvertToOrderType(util_optarg);
435        if (suppliedOrderType == Ord_Unassigned_c) {
436          (void) fprintf(vis_stderr, "unknown input order type: %s\n", util_optarg);
437          goto usage;
438        }
439        break;
440      case 'n':
441        if (strcmp("interleave", util_optarg) == 0) { 
442          nodeMethod = Ord_NodesByInterleaving_c;
443        }
444        else if (strcmp("merge_left", util_optarg) == 0) { 
445          nodeMethod = Ord_NodesByMergingLeft_c;
446        }
447        else if (strcmp("merge_right", util_optarg) == 0) { 
448          nodeMethod = Ord_NodesByMergingRight_c;
449        }
450        else if (strcmp("append", util_optarg) == 0) { 
451          nodeMethod = Ord_NodesByAppending_c;
452        }
453        else {
454          (void) fprintf(vis_stderr, "unknown node order method: %s\n", util_optarg);
455          goto usage;
456        }
457        break;
458      case 'r':
459        if (strcmp("depth", util_optarg) == 0) { 
460          rootMethod = Ord_RootsByDepth_c;
461        }
462        else if (strcmp("mincomm", util_optarg) == 0) { 
463          rootMethod = Ord_RootsByPerm_c;
464        }
465        else {
466          (void) fprintf(vis_stderr, "unknown root order method: %s\n", util_optarg);
467          goto usage;
468        }
469        break;
470      default:
471        goto usage;
472    }
473  }
474
475  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
476  if (network == NIL(Ntk_Network_t)) {
477    return 1;
478  }
479
480  if ((suppliedOrderType == Ord_InputAndLatch_c) && (generatedOrderType == Ord_All_c)) {
481    (void) fprintf(vis_stderr, "-o all -s input_and_latch not currently supported\n");
482    return 1;
483  }
484
485  /*
486   * The minimum set of variables that can be ordered are those specified by
487   * Ord_InputAndLatch_c.  If these have already been ordered, then just return.
488   */
489  if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c)) {
490    (void) fprintf(vis_stderr, "Variables already ordered. ");
491    (void) fprintf(vis_stderr, "Reinvoke flatten_hierarchy to undo variable ordering.\n");
492    return 1;
493  }
494 
495   
496  /*
497   * Process the input ordering file.
498   */
499  if (suppliedOrderType == Ord_Unassigned_c) {
500    if (argc - util_optind > 0) {
501      (void) fprintf(vis_stderr, "must specify -s if supplying order file\n");
502      goto usage;
503    }
504  }
505  else {
506    if (argc - util_optind == 0) {
507      (void) fprintf(vis_stderr, "order file not provided\n");
508      goto usage;
509    }
510    else if (argc - util_optind > 1) {
511      (void) fprintf(vis_stderr, "too many arguments\n");
512      goto usage;
513    }
514
515    fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
516    if (fp == NIL(FILE)) {
517      (void) fprintf(vis_stderr, "File %s is not readable, please check if it exists\n", argv[util_optind]);
518      return 1;
519    }
520    else {
521      boolean status;
522     
523      error_init();
524      status = Ord_FileReadNodeList(fp, network, &suppliedNodeList, verbose);
525      if (status == FALSE) {
526        (void) fprintf(vis_stderr, "Error reading ordering file:\n");
527        (void) fprintf(vis_stderr, "%s", error_string());
528        (void) fprintf(vis_stderr, "Cannot perform static ordering.\n");
529        (void) fclose(fp);
530        return 1;
531      }
532      else if (NetworkCheckSuppliedNodeList(network, suppliedNodeList,
533                                            suppliedOrderType) == FALSE) { 
534        (void) fprintf(vis_stderr, "Incorrect nodes supplied:\n");
535        (void) fprintf(vis_stderr, "%s", error_string());
536        (void) fprintf(vis_stderr, "Cannot perform static ordering.\n");
537        (void) fclose(fp);
538        (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL);
539        return 1;
540      }
541      else {
542        (void) fclose(fp);
543        if (verbose > 0) {
544          (void) fprintf(vis_stdout, "\nNodes supplied in ordering file, ");
545          (void) fprintf(vis_stdout, "according to -s option: \n");
546          OrdNodeListWrite(vis_stdout, suppliedNodeList);
547        }
548      }
549    }
550  }
551 
552 
553  /*
554   * In order for static ordering to proceed, network must not have any
555   * combinational cycles.
556   */
557  error_init();
558  if(Ntk_NetworkTestIsAcyclic(network) == 0) {
559    (void) fprintf(vis_stderr, "Combinational cycle found: ");
560    (void) fprintf(vis_stderr, "%s\n", error_string());
561    (void) fprintf(vis_stderr, "cannot perform static ordering\n");
562    if (suppliedOrderType != Ord_Unassigned_c) {
563      (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL);
564    }
565    return 1;
566  }
567
568  /* Start the timer before calling the variable ordering routine. */
569  if (timeOutPeriod > 0){
570    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
571    (void) alarm(timeOutPeriod);
572    if (setjmp(timeOutEnv) > 0) {
573      (void) fprintf(vis_stderr, "Timeout occurred after %d seconds.\n", timeOutPeriod);
574      alarm(0);
575      return 1;
576    }
577  }
578
579  /*
580   * Order the variables.
581   */
582  Ord_NetworkOrderVariables(network, rootMethod, nodeMethod, nsAfterSupport, 
583                            generatedOrderType, suppliedOrderType,
584                            suppliedNodeList, verbose);
585
586  if (suppliedOrderType != Ord_Unassigned_c) {
587    (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL);
588  }
589
590  /*
591   * As a sanity check, make sure that all the variables in generatedOrderType
592   * have an MDD id.
593   */
594  assert(Ord_NetworkTestAreVariablesOrdered(network, generatedOrderType));
595 
596  alarm(0);
597  return 0;  /* Everything okay */
598
599  usage:
600  (void) fprintf(vis_stderr, "usage: static_order [-a] [-h] [-n method] [-o type] [-r method] -s type [-t time] [-v #] file\n");
601  (void) fprintf(vis_stderr, "   -a        order NS variables after support\n");
602  (void) fprintf(vis_stderr, "   -h        print the command usage\n");
603  (void) fprintf(vis_stderr, "   -n method node ordering method\n");
604  (void) fprintf(vis_stderr, "             (interleave (default), append, merge_left, merge_right)\n");
605  (void) fprintf(vis_stderr, "   -o type   nodes to order (all, input_and_latch (default))\n");
606  (void) fprintf(vis_stderr, "   -r method root ordering method (depth, mincomm (default for < 30 latches))\n");
607  (void) fprintf(vis_stderr, "   -s type   nodes in file (all, input_and_latch, next_state_node, partial)\n");
608  (void) fprintf(vis_stderr, "   -t time   time out period (in seconds)\n");
609  (void) fprintf(vis_stderr, "   -v #      verbosity level\n");
610  (void) fprintf(vis_stderr, "   file      supplied ordering of nodes\n");
611
612  return 1;
613}
614
615
616/**Function********************************************************************
617
618  Synopsis    [Implements the read_order command.]
619
620  SideEffects []
621
622  CommandName [read_order]
623
624  CommandSynopsis [Read and reorder variable order from a file.]
625
626  CommandArguments [\[-h\] \[-v\] \[&lt;file&gt;\]]
627
628  CommandDescription [This command reads variable order from a file and
629  reorder variable order according to the order. This command can be used
630  any time after static_order command. However, the users should notice that
631  there is a possibility to get BDD blowups during this command.
632  <p>
633 
634
635  Command options:<p>
636
637  <dl>
638
639  <dt> -h
640  <dd> Print the command usage.<p>
641
642  <dt> -g &lt;group&gt;
643
644  <dd> Specify whether to group present and next state variables or not.<p>
645
646  <b>0:</b> Do not group.<p>
647
648  <b>1:</b> Do group (default).<p>
649
650  <dt> -v
651  <dd> Print debug information.
652  <dd>
653 
654  <dt> &lt;file&gt;
655
656  <dd> A file containing names of network nodes, used to specify a variable
657  ordering. The name of a node is the full hierarchical path name, starting
658  from the current hierarchical node.  A node should appear at most once in
659  the file.  Each node name should appear at the beginning of a new line, with
660  no white space preceeding it.  The end of a node name is marked by white
661  space, and any other text on the rest of the line is ignored.  Any line
662  starting with "#" or white space is ignored. See <tt>write_order</tt>
663  for a sample file. Note that the variable ordering cannot be specified at
664  the bit-level; it can only be specified at the multi-valued variable level.
665
666  </dl>
667  ]
668
669 
670  SeeAlso     [CommandStaticOrder CommandWriteOrder]
671
672******************************************************************************/
673static int
674CommandReadOrder(
675  Hrc_Manager_t ** hmgr,
676  int  argc,
677  char ** argv)
678{
679  int           c, status;
680  FILE          *fp;
681  int           verbose = 0;
682  int           group = 0;
683  lsList        suppliedNodeList = (lsList)NULL; /* list of Ntk_Node_t * */
684  Ntk_Network_t *network;
685  mdd_manager   *mddMgr;
686
687  if (bdd_get_package_name() != CUDD) {
688    fprintf(vis_stderr,
689           "** ord error: read_order can be used only with the CUDD package\n");
690  }
691
692  /*
693   * Parse the command line.
694   */
695  util_getopt_reset();
696  while ((c = util_getopt(argc, argv, "hg:v")) != EOF) {
697    switch (c) {
698      case 'h':
699        goto usage;
700      case 'g':
701        group = atoi(util_optarg);
702        break;
703      case 'v':
704        verbose = 1;
705        break;
706      default:
707        goto usage;
708    }
709  }
710
711  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
712  if (network == NIL(Ntk_Network_t)) {
713    return 1;
714  }
715
716  if (!Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c)) {
717    (void) fprintf(vis_stderr,
718                   "** ord error: static_order was not called yet.\n");
719    return 1;
720  }
721
722  /*
723   * Process the input ordering file.
724   */
725  if (argc - util_optind == 0) {
726    (void) fprintf(vis_stderr, "order file not provided\n");
727    goto usage;
728  }
729  else if (argc - util_optind > 1) {
730    (void) fprintf(vis_stderr, "too many arguments\n");
731    goto usage;
732  }
733
734  fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
735  if (fp == NIL(FILE)) {
736    return 1;
737  } else {
738    boolean status;
739   
740    error_init();
741    status = Ord_FileReadNodeList(fp, network, &suppliedNodeList, verbose);
742    if (status == FALSE) {
743      (void) fprintf(vis_stderr, "Error reading ordering file:\n");
744      (void) fprintf(vis_stderr, "%s", error_string());
745      (void) fprintf(vis_stderr, "Cannot perform static ordering.\n");
746      (void) fclose(fp);
747      return 1;
748    } else if (NetworkCheckSuppliedNodeList(network, suppliedNodeList,
749                                            Ord_InputAndLatch_c) == FALSE) { 
750      (void) fprintf(vis_stderr, "Incorrect nodes supplied:\n");
751      (void) fprintf(vis_stderr, "%s", error_string());
752      (void) fprintf(vis_stderr, "Cannot perform read_order.\n");
753      (void) fclose(fp);
754      (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL);
755      return 1;
756    } else {
757      (void) fclose(fp);
758      if (verbose > 0) {
759        (void) fprintf(vis_stdout, "\nNew variable order from file %s:\n",
760                        argv[util_optind]);
761        OrdNodeListWrite(vis_stdout, suppliedNodeList);
762      }
763    }
764  }
765 
766  /*
767   * Reorder the variables.
768   */
769  mddMgr = Ntk_NetworkReadMddManager(network);
770  status = OrdMakeNewVariableOrder(mddMgr, suppliedNodeList, group, verbose);
771
772  (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL);
773  if (status)
774    return 1;
775
776  alarm(0);
777  return 0;  /* Everything okay */
778
779  usage:
780  (void) fprintf(vis_stderr, "usage: read_order [-g #] [-h] [-v] file\n");
781  (void) fprintf(vis_stderr, "   -h        print the command usage\n");
782  (void) fprintf(vis_stderr, "   -g #      ps/ns variables grouping\n");
783  (void) fprintf(vis_stderr, "             0 : do not group ps/ns\n");
784  (void) fprintf(vis_stderr, "             1 : group ps/ns (default)\n");
785  (void) fprintf(vis_stderr, "   -v        verbosity on\n");
786  (void) fprintf(vis_stderr, "   file      variable order file\n");
787
788  return 1;
789}
790
791
792/**Function********************************************************************
793
794  Synopsis    [Implements the write_order command.]
795
796  SideEffects [none]
797
798  CommandName [write_order]
799
800  CommandSynopsis [write the current order of the MDD variables of the
801  flattened network]
802
803  CommandArguments [\[-h\] \[-o &lt;type&gt;\] \[&lt;file&gt;\]]
804
805  CommandDescription [Write the current order of the MDD variables of the
806  flattened network.  If no file name is specified, the output is written to
807  stdout. A sample output is shown here.
808
809  <pre>
810  # name                 type            mddId vals levs
811  system.choosing0      primary-input       31    2 (61)
812  system.p0.pc          latch               32   11 (62, 63, 64, 65)
813  </pre>
814
815  The first column gives the full hierarchical path name of the node, starting
816  from the current hierarchical node. The second column gives the type of the
817  node in the flattened network (see the command <tt>print_network</tt>).  The third
818  column gives the MDD id of the node; this can be thought of as just another
819  name for the node.  The fourth column gives the number of values that the
820  multi-valued variable at the output of the node can assume.  The last column
821  gives the levels of the BDD variables that encode the multi-valued variable
822  (0 is the topmost level of the BDD). <p>
823
824  The bits of a multi-valued variable need not appear consecutively (due to
825  dynamic variable ordering).  Each node appears at most once in the output
826  file. The nodes in the file appear in ascending order of the lowest level
827  bit in the encoding of the node's multi-valued variable (e.g. a node with
828  levels (12, 73) will appear before a node with levels (17, 21, 25)).<p>
829 
830  To specify a variable ordering for static_order, a convenient tactic is to
831  write out the current ordering, edit the file to rearrange the ordering (or
832  comment out some nodes, using "#"), and then read the file back in using
833  <tt>static_order</tt>. Note that everything after the first column is
834  ignored when the file is read in.<p>
835
836  Command options:<p> 
837 
838  <dl>
839
840  <dt> -h
841  <dd> Print the command usage.<p>
842
843  <dt> -o &lt;type&gt;
844  <dd> Specify the network nodes to write out.  Type can be one of the following:<p>
845
846  <b>all:</b> Write out all the nodes of the network.  This option is
847  allowed only if all variables have been ordered.<p>
848
849  <b>input_and_latch:</b> (default) Write out the primary inputs, pseudo
850  inputs, latches, and next state variables.  <p>
851
852  <b>next_state_node:</b> Write out the next state variables (node type is
853  "shadow").  This file can be modified and read back in using the
854  <tt>static_order -s next_state_node</tt> command.<p>
855 
856  <dt> &lt;file&gt;
857
858  <dd> File to which to write the ordering.  By default, the ordering is
859  written to stdout.<p>
860 
861  </dl>]
862
863******************************************************************************/
864static int
865CommandWriteOrder(
866  Hrc_Manager_t ** hmgr,
867  int  argc,
868  char ** argv)
869{
870  int            c;
871  FILE          *fp;
872  int            status;
873  Ord_OrderType  orderType = Ord_InputAndLatch_c; /* default */
874  Ntk_Network_t *network;
875 
876  /*
877   * Parse the command line.
878   */
879  util_getopt_reset();
880  while ((c = util_getopt(argc, argv, "ho:")) != EOF) {
881    switch (c) {
882      case 'h':
883        goto usage;
884      case 'o':
885        orderType = StringConvertToOrderType(util_optarg);
886        if (orderType == Ord_Partial_c) { 
887          (void) fprintf(vis_stderr, "disallowed output order type: %s\n", util_optarg);
888          goto usage;
889        }
890        else if (orderType == Ord_Unassigned_c) {
891          (void) fprintf(vis_stderr, "unknown output order type: %s\n", util_optarg);
892          goto usage;
893        }
894        break;
895      default:
896        goto usage;
897    }
898  }
899
900  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
901  if (network == NIL(Ntk_Network_t)) {
902    return 1;
903  }
904
905  /*
906   * Open the destination file.
907   */
908  if (argc - util_optind == 0) {
909    fp = Cmd_FileOpen("-", "w", NIL(char *), /* silent */0);
910  }
911  else if (argc - util_optind == 1) {
912    fp = Cmd_FileOpen(argv[util_optind], "w", NIL(char *), /* silent */0);
913  }
914  else {
915    goto usage;
916  }
917  if (fp == NIL(FILE)) {
918    return 1;
919  }
920
921  error_init();
922  if (Ord_NetworkPrintVariableOrder(fp, network, orderType) == 0) {
923    (void) fprintf(vis_stderr, "Not all nodes are ordered: ");
924    (void) fprintf(vis_stderr, "%s", error_string());
925    status = 1;
926  }
927  else {
928    status = 0;  /* success */
929  }
930
931  if (fp != stdout) {
932    (void) fclose(fp);
933  }
934  return (status);
935 
936usage:
937  (void) fprintf(vis_stderr, "usage: write_order [-h] [-o type] [file]\n");
938  (void) fprintf(vis_stderr, "   -h        print the command usage\n");
939  (void) fprintf(vis_stderr, "   -o type   nodes to write (all, input_and_latch (default), next_state_node)\n");
940  (void) fprintf(vis_stderr, "   file      output file name\n");
941
942  return 1;
943}
944
945
946/**Function********************************************************************
947
948  Synopsis    [Implements the dynamic_var_ordering command.]
949
950  SideEffects []
951
952  CommandName [dynamic_var_ordering]
953
954  CommandSynopsis [control the application of dynamic variable ordering]
955
956  CommandArguments [ \[-d\] \[-e &lt;method&gt;\] \[-f &lt;method&gt;\]
957  \[-h\]]
958
959  CommandDescription [Control the application of dynamic variable ordering to the
960  flattened network. Dynamic ordering is a technique to reorder the MDD
961  variables to reduce the size of the existing MDDs.  When no options are
962  specified, the current status of dynamic ordering is displayed.  At most one
963  of the options -e, -f, and -d should be specified.  The commands
964  <tt>flatten_hierarchy</tt> and <tt>static_order</tt> must be invoked before
965  this command.<p>
966
967  Dynamic ordering may be time consuming, but can often reduce the size of the
968  MDDs dramatically.  The good points to invoke dynamic ordering explicitly
969  (using the -f option) are after the commands <tt>build_partition_mdds</tt>
970  and <tt>print_img_info</tt>.  If dynamic ordering finds a good ordering,
971  then you may wish to save this ordering (using <tt>write_order</tt>) and
972  reuse it (using <tt>static_order -s</tt>) in the future. A common sequence
973  used to get a good ordering is the following:<p>
974
975  <pre>
976  init_verify
977  print_img_info
978  dynamic_var_ordering -f sift
979  write_order <file>
980  flatten_hierarchy
981  static_order -s input_and_latch -f <file>
982  build_partition_mdds
983  print_img_info
984  dynamic_var_ordering -f sift
985  </pre> 
986 
987  <p>For many large examples, there is no single best variable order,
988  or that order is hard to find.  For example, the best ordering
989  during partitioning of the network may be different from the best
990  ordering during a model check. In that case you can use automatic
991  reordering, using the <tt>-e</tt> option. This will trigger
992  reordering whenever the total size of the MDD increases by a certain
993  factor. Often, the <tt>init</tt> command is replaced by the
994  following sequence:
995 
996  <pre>
997  flatten_hierarchy
998  static_order
999  dynamic_var_ordering -e sift
1000  build_partition_mdds
1001  </pre>
1002 
1003  Command options:<p> 
1004
1005  <dl>
1006
1007  <dt> -d
1008  <dd> Disable dynamic ordering from triggering automatically.<p>
1009 
1010  <dt> -e &lt;method&gt;
1011  <dd> Enable dynamic ordering to trigger automatically whenever a certain
1012  threshold on the overall MDD size is reached. "Method" must be one of the following:<p>
1013
1014  <b>window:</b> Permutes the variables within windows of three adjacent
1015  variables so as to minimize the overall MDD size.  This process is repeated
1016  until no more reduction in size occurs.<p>
1017
1018  <b>sift:</b> Moves each variable throughout the order to find an optimal
1019  position for that variable (assuming all other variables are fixed).  This
1020  generally achieves greater size reductions than the window method, but is
1021  slower.<p>
1022 
1023  The following methods are only available if VIS has been linked with the Bdd
1024  package from the University of Colorado (cuBdd).</b><p>
1025
1026  <b>random:</b> Pairs of variables are randomly chosen, and swapped in the
1027  order. The swap is performed by a series of swaps of adjacent variables. The
1028  best order among those obtained by the series of swaps is retained. The
1029  number of pairs chosen for swapping equals the number of variables in the
1030  diagram.<p>
1031
1032  <b>random_pivot:</b> Same as <b>random</b>, but the two variables are chosen
1033  so that the first is above the variable with the largest number of nodes, and
1034  the second is below that variable.  In case there are several variables tied
1035  for the maximum number of nodes, the one closest to the root is used.<p>
1036
1037  <b>sift_converge:</b> The <b>sift</b> method is iterated until no further
1038  improvement is obtained.<p>
1039
1040  <b>symmetry_sift:</b> This method is an implementation of symmetric
1041  sifting. It is similar to sifting, with one addition: Variables that become
1042  adjacent during sifting are tested for symmetry. If they are symmetric, they
1043  are linked in a group. Sifting then continues with a group being moved,
1044  instead of a single variable.<p>
1045
1046  <b>symmetry_sift_converge:</b> The <b>symmetry_sift</b> method is iterated
1047  until no further improvement is obtained.<p>
1048
1049  <b>window{2,3,4}:</b> Permutes the variables within windows of n adjacent
1050  variables, where "n" can be either 2, 3 or 4, so as to minimize the overall
1051  MDD size.<p>
1052
1053  <b>window{2,3,4}_converge:</b> The <b>window{2,3,4}</b> method is iterated
1054  until no further improvement is obtained.<p>
1055
1056  <b>group_sift:</b> This method is similar to <b>symmetry_sift</b>,
1057  but uses more general criteria to create groups.<p>
1058
1059  <b>group_sift_converge:</b> The <b>group_sift</b> method is iterated until no
1060  further improvement is obtained.<p>
1061
1062  <b>lazy_sift:</b> This method is similar to <b>group_sift</b>, but the
1063  creation of groups takes into account the pairing of present and next state
1064  variables.<p>
1065
1066  <b>annealing:</b> This method is an implementation of simulated annealing for
1067  variable ordering. This method is potentially very slow.<p>
1068
1069  <b>genetic:</b> This method is an implementation of a genetic algorithm for
1070  variable ordering. This method is potentially very slow.<p>
1071
1072  <dt> -f &lt;method&gt;
1073  <dd> Force dynamic ordering to be invoked immediately.  The values for
1074  method are the same as in option -e.<p>
1075
1076  <dt> -h
1077  <dd> Print the command usage.
1078
1079  <dt> -v &lt;#&gt;
1080  <dd> Verbosity level. Default is 0. For values greater than 0,
1081  statistics pertaining to reordering will be printed whenever
1082  reordering occurs.
1083 
1084  </dl>
1085  ]
1086 
1087******************************************************************************/
1088static int
1089CommandDynamicVarOrdering(
1090  Hrc_Manager_t ** hmgr,
1091  int  argc,
1092  char ** argv)
1093{
1094  int                 c;
1095  bdd_reorder_type_t  currentMethod;
1096  bdd_reorder_type_t  dynOrderingMethod = BDD_REORDER_NONE; /* for lint */
1097  boolean             disableFlag       = FALSE;
1098  boolean             enableFlag        = FALSE;
1099  boolean             forceFlag         = FALSE;
1100  Ntk_Network_t      *network;
1101  int verbosityFlag = -1;
1102  bdd_reorder_verbosity_t reorderVerbosity = BDD_REORDER_VERBOSITY_DEFAULT;
1103
1104  /*
1105   * Parse the command line.
1106   */
1107  util_getopt_reset();
1108  while ((c = util_getopt(argc, argv, "df:e:hv:")) != EOF) {
1109    switch (c) {
1110      case 'h':
1111        goto usage;
1112      case 'f':
1113        forceFlag = TRUE;
1114        dynOrderingMethod = StringConvertToDynOrderType(util_optarg);
1115        if (dynOrderingMethod == BDD_REORDER_NONE) {
1116          (void) fprintf(vis_stderr, "unknown method: %s\n", util_optarg);
1117          goto usage;
1118        }
1119        break;
1120      case 'e':
1121        enableFlag = TRUE;
1122        dynOrderingMethod = StringConvertToDynOrderType(util_optarg);
1123        if (dynOrderingMethod == BDD_REORDER_NONE) {
1124          (void) fprintf(vis_stderr, "unknown method: %s\n", util_optarg);
1125          goto usage;
1126        }
1127        break;
1128      case 'd':
1129        disableFlag = TRUE;
1130        break;
1131      case 'v':
1132        verbosityFlag = atoi(util_optarg);
1133        break;
1134    default:
1135        goto usage;
1136    }
1137  }
1138  if (c == EOF && argc != util_optind)
1139    goto usage;
1140
1141  switch (verbosityFlag) {
1142  case 0: reorderVerbosity = BDD_REORDER_NO_VERBOSITY; break;
1143  case 1: reorderVerbosity = BDD_REORDER_VERBOSITY; break;
1144  default: reorderVerbosity = BDD_REORDER_VERBOSITY_DEFAULT; break;
1145  }
1146 
1147  /* flatten_hierarchy and static_order must have been invoked already. */
1148  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
1149  if (network == NIL(Ntk_Network_t)) {
1150    return 1;
1151  }
1152  if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c) == FALSE) {
1153    (void) fprintf(vis_stderr, "The MDD variables have not been ordered. ");
1154    (void) fprintf(vis_stderr, "Use static_order.\n");
1155    return 1;
1156  }
1157
1158  /* At most one option is allowed. */
1159  if ((disableFlag && enableFlag) || (disableFlag && forceFlag)
1160      || (enableFlag && forceFlag)) {
1161    (void) fprintf(vis_stderr, "Only one of -d, -f, -e is allowed.\n");
1162    return 1;
1163  }
1164
1165  /*
1166   * Get the current method for reading and to save in case temporarily
1167   * overwritten.
1168   */
1169  currentMethod = Ntk_NetworkReadDynamicVarOrderingMethod(network);
1170 
1171  /* If no options are given, then just display current status. */
1172  if (!(disableFlag || enableFlag || forceFlag)) {
1173    if (currentMethod == BDD_REORDER_NONE) {
1174      (void) fprintf(vis_stdout, "Dynamic variable ordering is disabled.\n");
1175    }
1176    else {
1177      (void) fprintf(vis_stdout, "Dynamic variable ordering is enabled ");
1178      (void) fprintf(vis_stdout, "with method %s.\n",
1179                     DynOrderTypeConvertToString(currentMethod));
1180    }
1181  }
1182
1183  if (disableFlag) {
1184    if (currentMethod == BDD_REORDER_NONE) {
1185      (void) fprintf(vis_stdout, "Dynamic variable ordering is already disabled.\n");
1186    }
1187    else {
1188      (void) fprintf(vis_stdout, "Dynamic variable ordering is disabled.\n");
1189      Ntk_NetworkSetDynamicVarOrderingMethod(network, BDD_REORDER_NONE, reorderVerbosity);
1190    }
1191  }
1192
1193  /*
1194   * Set the dynamic ordering method of the network.  Note that
1195   * Ntk_NetworkSetDynamicVarOrderingMethod makes the necessary call to
1196   * bdd_dynamic_reordering.
1197   */
1198  if (enableFlag) {
1199    Ntk_NetworkSetDynamicVarOrderingMethod(network, dynOrderingMethod,
1200                                           reorderVerbosity);
1201    if (bdd_get_package_name() != CUDD)
1202      dynOrderingMethod = Ntk_NetworkReadDynamicVarOrderingMethod(network);
1203    (void) fprintf(vis_stdout,
1204                   "Dynamic variable ordering is enabled with method %s.\n",
1205                   DynOrderTypeConvertToString(dynOrderingMethod));
1206  }
1207
1208  /*
1209   * Force a reordering.  Note that the mddManager has to have the method set
1210   * before calling bdd_reorder.  This is done via a call to
1211   * Ntk_NetworkSetDynamicVarOrderingMethod with dynOrderingMethod.  The value
1212   * of the ordering method is restored afterwards.
1213   */
1214  if (forceFlag) {
1215    mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
1216    bdd_reorder_verbosity_t prevReorderVerbosity;
1217    prevReorderVerbosity = bdd_reordering_reporting(mddManager);
1218
1219    (void) fprintf(vis_stdout, "Dynamic variable ordering forced ");
1220    (void) fprintf(vis_stdout, "with method %s....\n",
1221                   DynOrderTypeConvertToString(dynOrderingMethod));
1222    Ntk_NetworkSetDynamicVarOrderingMethod(network, dynOrderingMethod, reorderVerbosity);
1223    bdd_reorder(Ntk_NetworkReadMddManager(network));
1224    Ntk_NetworkSetDynamicVarOrderingMethod(network, currentMethod, prevReorderVerbosity);
1225  }
1226
1227  return 0;  /* Everything okay */
1228
1229usage:
1230  (void) fprintf(vis_stderr, "usage: dynamic_var_ordering [-d] [-e method] [-f method] [-h]\n");
1231  (void) fprintf(vis_stderr, "   -d        disable dynamic ordering\n");
1232  (void) fprintf(vis_stderr, "   -e method enable dynamic ordering with method (window, sift)\n");
1233  (void) fprintf(vis_stderr, "   -f method force dynamic ordering with method (window, sift)\n");
1234  (void) fprintf(vis_stderr, "   -h        print the command usage\n");
1235  (void) fprintf(vis_stderr, "   -v #      verbosity level \n");
1236 
1237  return 1;
1238}
1239
1240
1241/**Function********************************************************************
1242
1243  Synopsis    [Implements the print_bdd_stats command.]
1244
1245  SideEffects []
1246
1247  CommandName [print_bdd_stats]
1248
1249  CommandSynopsis [print the BDD statistics for the flattened network]
1250
1251  CommandArguments [\[-h\]]
1252
1253  CommandDescription [Print the BDD statistics for the flattened network.  The
1254  MDDs representing the functions of the network are themselves represented by
1255  BDDs via an encoding of the multi-valued variables into binary valued
1256  variables.  The statistics given by this command depend on the underlying
1257  BDD package with which VIS was linked.  To get more information about the
1258  statistics, consult the documentation for the given BDD package.  The
1259  commands <tt>flatten_hierarchy</tt> and <tt>static_order</tt> must be
1260  invoked before this command.<p>
1261
1262  Command options:<p> 
1263
1264  <dl>
1265
1266  <dt> -h
1267  <dd> Print the command usage.
1268
1269  </dl>
1270  ]
1271 
1272******************************************************************************/
1273static int
1274CommandPrintBddStats(
1275  Hrc_Manager_t ** hmgr,
1276  int  argc,
1277  char ** argv)
1278{
1279  int            c;
1280  Ntk_Network_t *network;
1281
1282  /*
1283   * Parse the command line.
1284   */
1285  util_getopt_reset();
1286  while ((c = util_getopt(argc, argv, "h")) != EOF) {
1287    switch (c) {
1288      case 'h':
1289        goto usage;
1290      default:
1291        goto usage;
1292    }
1293  }
1294
1295  /* flatten_hierarchy and static_order must have been invoked already. */
1296  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
1297  if (network == NIL(Ntk_Network_t)) {
1298    return 1;
1299  }
1300  if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c) == FALSE) {
1301    (void) fprintf(vis_stderr, "The MDD variables have not been ordered. ");
1302    (void) fprintf(vis_stderr, "Use static_order.\n");
1303    return 1;
1304  }
1305
1306  bdd_print_stats(Ntk_NetworkReadMddManager(network), vis_stdout);
1307
1308  return 0;  /* Everything okay */
1309
1310usage:
1311  (void) fprintf(vis_stderr, "usage: print_bdd_stats [-h]\n");
1312  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
1313
1314  return 1;
1315}
1316
1317
1318/**Function********************************************************************
1319
1320  Synopsis    [Converts a string to an order type.]
1321
1322  Description [Converts a string to an order type. If string does not refer to
1323  one of the allowed order types, then returns Ord_Unassigned_c.]
1324
1325  SideEffects []
1326
1327******************************************************************************/
1328static Ord_OrderType
1329StringConvertToOrderType(
1330  char *string)
1331{
1332  if (strcmp("all", string) == 0) { 
1333    return Ord_All_c; 
1334  }
1335  else if (strcmp("input_and_latch", string) == 0) { 
1336    return Ord_InputAndLatch_c;
1337  }
1338  else if (strcmp("next_state_node", string) == 0) {
1339    return Ord_NextStateNode_c;
1340  }
1341  else if (strcmp("partial", string) == 0) {
1342    return Ord_Partial_c;
1343  }
1344  else {
1345    return Ord_Unassigned_c;
1346  }
1347}
1348
1349
1350/**Function********************************************************************
1351
1352  Synopsis    [Converts a string to a dynamic ordering method type.]
1353
1354  Description [Converts a string to a dynamic ordering method type. If string
1355  is not "sift" or "window", then returns BDD_REORDER_NONE.]
1356
1357  SideEffects []
1358
1359******************************************************************************/
1360static bdd_reorder_type_t
1361StringConvertToDynOrderType(
1362  char *string)
1363{
1364  if (strcmp("sift", string) == 0) { 
1365    return BDD_REORDER_SIFT;
1366  }
1367  else if (strcmp("window", string) == 0) { 
1368    return BDD_REORDER_WINDOW;
1369  }
1370  else if (strcmp("random", string) == 0) { 
1371    return BDD_REORDER_RANDOM;
1372  }
1373  else if (strcmp("random_pivot", string) == 0) { 
1374    return  BDD_REORDER_RANDOM_PIVOT;
1375  }
1376  else if (strcmp("sift_converge", string) == 0) { 
1377    return  BDD_REORDER_SIFT_CONVERGE;
1378  }
1379  else if (strcmp("symmetry_sift", string) == 0) { 
1380    return  BDD_REORDER_SYMM_SIFT;
1381  }
1382  else if (strcmp("symmetry_sift_converge", string) == 0) { 
1383    return  BDD_REORDER_SYMM_SIFT_CONV;
1384  }
1385  else if (strcmp("window2", string) == 0) { 
1386    return  BDD_REORDER_WINDOW2;
1387  }
1388  else if (strcmp("window3", string) == 0) { 
1389    return  BDD_REORDER_WINDOW3;
1390  }
1391  else if (strcmp("window4", string) == 0) { 
1392    return  BDD_REORDER_WINDOW4;
1393  }
1394  else if (strcmp("window2_converge", string) == 0) { 
1395    return  BDD_REORDER_WINDOW2_CONV;
1396  }
1397  else if (strcmp("window3_converge", string) == 0) { 
1398    return  BDD_REORDER_WINDOW3_CONV;
1399  }
1400  else if (strcmp("window4_converge", string) == 0) { 
1401    return  BDD_REORDER_WINDOW4_CONV;
1402  }
1403  else if (strcmp("group_sift", string) == 0) { 
1404    return  BDD_REORDER_GROUP_SIFT;
1405  }
1406  else if (strcmp("group_sift_converge", string) == 0) { 
1407    return  BDD_REORDER_GROUP_SIFT_CONV;
1408  }
1409  else if (strcmp("annealing", string) == 0) { 
1410    return  BDD_REORDER_ANNEALING;
1411  }
1412  else if (strcmp("genetic", string) == 0) { 
1413    return  BDD_REORDER_GENETIC;
1414  }
1415  else if (strcmp("exact", string) == 0) { 
1416    return  BDD_REORDER_EXACT;
1417  }
1418  else if (strcmp("lazy_sift", string) == 0) {
1419    return BDD_REORDER_LAZY_SIFT;
1420  }
1421  else {
1422    return BDD_REORDER_NONE;
1423  }
1424}
1425
1426
1427/**Function********************************************************************
1428
1429  Synopsis    [Converts a dynamic ordering method type to a string.]
1430
1431  Description [Converts a dynamic ordering method type to a string.  This
1432  string must NOT be freed by the caller.]
1433
1434  SideEffects []
1435
1436******************************************************************************/
1437static char *
1438DynOrderTypeConvertToString(
1439  bdd_reorder_type_t method)
1440{
1441  if (method == BDD_REORDER_SIFT) {
1442    return "sift"; 
1443  }
1444  else if (method == BDD_REORDER_WINDOW) {
1445    return "window"; 
1446  }
1447  else if (method == BDD_REORDER_NONE) {
1448    return "none"; 
1449  }
1450  else if (method == BDD_REORDER_RANDOM) { 
1451    return "random";
1452  }
1453  else if (method == BDD_REORDER_RANDOM_PIVOT) { 
1454    return "random_pivot";
1455  }
1456  else if (method == BDD_REORDER_SIFT_CONVERGE) { 
1457    return "sift_converge";
1458  }
1459  else if (method == BDD_REORDER_SYMM_SIFT) { 
1460    return "symmetry_sift";
1461  }
1462  else if (method == BDD_REORDER_SYMM_SIFT_CONV) { 
1463    return "symmetry_sift_converge";
1464  }
1465  else if (method == BDD_REORDER_WINDOW2) { 
1466    return "window2";
1467  }
1468  else if (method == BDD_REORDER_WINDOW3) { 
1469    return "window3";
1470  }
1471  else if (method == BDD_REORDER_WINDOW4) { 
1472    return "window4";
1473  }
1474  else if (method == BDD_REORDER_WINDOW2_CONV) { 
1475    return "window2_converge";
1476  }
1477  else if (method == BDD_REORDER_WINDOW3_CONV) { 
1478    return "window3_converge";
1479  }
1480  else if (method == BDD_REORDER_WINDOW4_CONV) { 
1481    return "window4_converge";
1482  }
1483  else if (method == BDD_REORDER_GROUP_SIFT) { 
1484    return "group_sift";
1485  }
1486  else if (method == BDD_REORDER_GROUP_SIFT_CONV) { 
1487    return "group_sift_converge";
1488  }
1489  else if (method == BDD_REORDER_ANNEALING) { 
1490    return "annealing";
1491  }
1492  else if (method == BDD_REORDER_GENETIC) { 
1493    return "genetic";
1494  }
1495  else if (method ==  BDD_REORDER_EXACT) { 
1496    return "exact";
1497  }
1498  else if (method == BDD_REORDER_LAZY_SIFT) {
1499    return "lazy_sift";
1500  }
1501  else {
1502    fail("unrecognized method");
1503    return NIL(char); /* not reached */
1504  }
1505}
1506
1507
1508/**Function********************************************************************
1509
1510  Synopsis    [Verifies that suppliedNodeList has the correct nodes.]
1511
1512  Description [Returns TRUE if the set of nodes in suppliedNodeList matches
1513  the set of nodes in network specified by orderType; else returns FALSE and
1514  writes a message to error_string. OrderType should be one of the following:
1515  1) Ord_All_c: should match the set of all nodes in network; 2)
1516  Ord_InputAndLatch_c: should match the set of inputs (primary + pseudo),
1517  latches, and next state nodes; 3) Ord_NextStateNode_c: should match the set
1518  of next state nodes; number should be the number of latches; 4)
1519  Ord_Partial_c: returns TRUE automatically.]
1520
1521  SideEffects []
1522
1523******************************************************************************/
1524static boolean
1525NetworkCheckSuppliedNodeList(
1526  Ntk_Network_t * network,
1527  lsList  suppliedNodeList,
1528  Ord_OrderType  orderType)
1529{
1530  lsGen         gen;
1531  st_generator *stGen;
1532  Ntk_Node_t   *node;
1533  st_table     *requiredNodes;
1534  st_table     *suppliedNodes;
1535  char         *dummy;
1536  boolean       returnFlag = TRUE;
1537 
1538  assert(orderType != Ord_Unassigned_c);
1539
1540  if (orderType == Ord_Partial_c) {
1541    return TRUE;
1542  }
1543 
1544  /* At this point, orderType must be one of the these. */
1545  assert((orderType == Ord_All_c) || (orderType == Ord_InputAndLatch_c)
1546         || (orderType == Ord_NextStateNode_c));
1547 
1548
1549  /*
1550   * Build up the table of required nodes. Next state nodes are included by
1551   * all 3 order types.
1552   */
1553  requiredNodes = st_init_table(st_ptrcmp, st_ptrhash);
1554  Ntk_NetworkForEachNode(network, gen, node) {
1555    if ((orderType == Ord_All_c) || Ntk_NodeTestIsNextStateNode(node)) {
1556      st_insert(requiredNodes, (char *) node, NIL(char));
1557    }
1558    else if ((orderType == Ord_InputAndLatch_c)
1559             && Ntk_NodeTestIsCombInput(node)) {
1560      st_insert(requiredNodes, (char *) node, NIL(char));
1561    }
1562    /* else, this node is not included by orderType */
1563  }
1564
1565  /*
1566   * Convert suppliedNodeList to the table of supplied nodes.
1567   */
1568  suppliedNodes = st_init_table(st_ptrcmp, st_ptrhash);
1569  lsForEachItem(suppliedNodeList, gen, node) {
1570    int status = st_insert(suppliedNodes, (char *) node, NIL(char));
1571    if (status) {
1572      error_append("node ");
1573      error_append(Ntk_NodeReadName(node));
1574      error_append(" appears more than once in ordering file\n");
1575      returnFlag = FALSE;
1576    }
1577  }
1578
1579  /*
1580   * Check that suppliedNodes is contained in requiredNodes.
1581   */
1582  st_foreach_item(suppliedNodes, stGen, &node, &dummy) {
1583    if (!st_is_member(requiredNodes, node)) {
1584      error_append("node ");
1585      error_append(Ntk_NodeReadName(node));
1586      error_append(" supplied but not required\n");
1587      returnFlag = FALSE;
1588    }
1589  }
1590 
1591  /*
1592   * Check that suppliedNodes is contained in requiredNodes.
1593   */
1594  st_foreach_item(requiredNodes, stGen, &node, &dummy) {
1595    if (!st_is_member(suppliedNodes, node)) {
1596      error_append("node ");
1597      error_append(Ntk_NodeReadName(node));
1598      error_append(" required but not supplied\n");
1599      returnFlag = FALSE;
1600    }
1601  }
1602 
1603  st_free_table(requiredNodes);
1604  st_free_table(suppliedNodes);
1605  return returnFlag;
1606}
1607
1608
1609/**Function********************************************************************
1610
1611  Synopsis    [Handle function for timeout.]
1612
1613  Description [This function is called when the time out occurs.]
1614
1615  SideEffects []
1616
1617******************************************************************************/
1618static void
1619TimeOutHandle(void)
1620{
1621  longjmp(timeOutEnv, 1);
1622}
Note: See TracBrowser for help on using the repository browser.