/**CFile*********************************************************************** FileName [ordCmd.c] PackageName [ord] Synopsis [Command interface to the ordering package.] Author [Adnan Aziz, Tom Shiple, Serdar Tasiran] Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved. Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software. IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] ******************************************************************************/ #include "ordInt.h" static char rcsid[] UNUSED = "$Id: ordCmd.c,v 1.37 2005/05/19 03:22:55 awedh Exp $"; /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ static jmp_buf timeOutEnv; /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static int CommandStaticOrder(Hrc_Manager_t ** hmgr, int argc, char ** argv); static int CommandReadOrder(Hrc_Manager_t ** hmgr, int argc, char ** argv); static int CommandWriteOrder(Hrc_Manager_t ** hmgr, int argc, char ** argv); static int CommandDynamicVarOrdering(Hrc_Manager_t ** hmgr, int argc, char ** argv); static int CommandPrintBddStats(Hrc_Manager_t ** hmgr, int argc, char ** argv); static Ord_OrderType StringConvertToOrderType(char *string); static bdd_reorder_type_t StringConvertToDynOrderType(char *string); static char * DynOrderTypeConvertToString(bdd_reorder_type_t method); static boolean NetworkCheckSuppliedNodeList(Ntk_Network_t * network, lsList suppliedNodeList, Ord_OrderType orderType); static void TimeOutHandle(void); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Initializes the order package.] SideEffects [] SeeAlso [Ord_End] ******************************************************************************/ void Ord_Init(void) { Cmd_CommandAdd("static_order", CommandStaticOrder, 0); Cmd_CommandAdd("read_order", CommandReadOrder, 0); Cmd_CommandAdd("write_order", CommandWriteOrder, 0); Cmd_CommandAdd("dynamic_var_ordering", CommandDynamicVarOrdering, 0); Cmd_CommandAdd("print_bdd_stats", CommandPrintBddStats, 0); } /**Function******************************************************************** Synopsis [Ends the order package.] SideEffects [] SeeAlso [Ord_Init] ******************************************************************************/ void Ord_End(void) { } /**Function******************************************************************** Synopsis [Checks that all nodes corresponding to orderType have MDD ids.] Description [For each node of network that falls in the class given by orderType, checks that the node has an MDD id. If all such nodes have MDD ids, return 1, else returns 0. orderType can have one of 3 values: Ord_All_c, checks all nodes of network; Ord_InputAndLatch_c, checks all combinational inputs and latch next states; Ord_NextStateNode_c, checks all next state nodes. Returns 0 on the first such node not having an MDD id, and writes an error message in error_string. Also returns 0 if the network doesn't have an MDD manager.] SideEffects [] ******************************************************************************/ boolean Ord_NetworkTestAreVariablesOrdered( Ntk_Network_t * network, Ord_OrderType orderType) { lsGen gen; Ntk_Node_t *node; mdd_manager *mddManager = Ntk_NetworkReadMddManager(network); assert((orderType == Ord_All_c) || (orderType == Ord_InputAndLatch_c) || (orderType == Ord_NextStateNode_c)); if (mddManager == NIL(mdd_manager)) { error_append("network doesn't have an MDD manager\n"); return 0; } /* * Next state nodes are included by all 3 order types. */ Ntk_NetworkForEachNode(network, gen, node) { if ((orderType == Ord_All_c) || Ntk_NodeTestIsNextStateNode(node)) { if (Ntk_NodeReadMddId(node) == NTK_UNASSIGNED_MDD_ID) { error_append("node "); error_append(Ntk_NodeReadName(node)); error_append(" not ordered\n"); (void) lsFinish(gen); return 0; } } else if ((orderType == Ord_InputAndLatch_c) && Ntk_NodeTestIsCombInput(node)) { if (Ntk_NodeReadMddId(node) == NTK_UNASSIGNED_MDD_ID) { error_append("node "); error_append(Ntk_NodeReadName(node)); error_append(" not ordered\n"); (void) lsFinish(gen); return 0; } } /* else, this node is not included by orderType */ } return 1; } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Implements the static_order command.] SideEffects [] CommandName [static_order] CommandSynopsis [order the MDD variables of the flattened network] CommandArguments [\[-a\] \[-h\] \[-n <method>\] \[-o <type>\] \[-r <method>\] -s <type> \[-t <timeOut>\] \[-v #\] <file>] CommandDescription [Order the MDD variables of the flattened network. MDD variables must be created before MDDs can be built. Networks with combinational cycles cannot be ordered. If the MDD variables have already been ordered, then this command does nothing. To undo the current ordering, reinvoke the command flatten_hierarchy.

Command options:

-a
Order each next state variable immediately following the variables in the support of the corresponding next state function. By default, each next state variable is placed immeadiately following the corresponding present state variable. It has been observed experimentally that ordering the NS variable after the PS variable is almost always better; however, as a last b resort, you might want to try this option.

Unless the -a flag is set, the PS and NS variables corresponding to latches are grouped together and cannot be separated by dynamic reordering. (This is done even when the ordering is read from a file - adjacent PS/NS vars in the file are grouped).

-h
Print the command usage.

-n <method>
Specify which node ordering method to use. Node ordering is the process of computing a total ordering on all the network nodes. This ordering is then projected onto the set of nodes specified by -o type. In the complexity measures below, n is the number of network nodes, E is the number of network edges, and k is the number of latches. "Method" must be one of the following:

interleave: (default) Uses Algorithm 2 of Fujii et al., "Interleaving Based Variable Ordering Methods for OBDDs", ICCAD 1993. The complexity is O(E+nlog(n)).

append: Uses the algorithm of Malik, et al. "Logic Verification using Binary Decision Diagrams in a Logic Synthesis Environment," ICCAD, 1988. Nodes are visited in DFS order, and appended to a global order list in the order they are visited. The fanins of a node are visited in order of decreasing depth. The roots of the DFS are visited in the order determined by the -r method. The complexity is O(E+nlog(n)).

merge_left: Uses an algorithm alluded to in Fujii et al., "Interleaving Based Variable Ordering Methods for OBDDs", ICCAD 1993. Nodes are visited in DFS order. At a given node g, its fanins are visited in order of decreasing depth. For each fanin fi, a total order is computed for all the nodes in the transitive fanin (TFI) of fi, including fi itself. This ordering is merged into the combined ordering from fanins of higher priority. After processing all of the fanins, the result is a total ordering on all TFI nodes of g. Finally, g is appended to the end of this ordering, yielding a topological ordering. For example if the ordering for f1 is list1 = (a,b,d,f1) and for f2 is list2=(c,d,e,f2), and f1 has greater depth than f2, then the ordering for g is (c,a,b,d,e,f2,f1,g). The merge is done by inserting into list1 those nodes in list2 not already in list1, in such a way that the inserted nodes remain as close as possible to their left neighbors in list2 ("insert as far left as possible"). The roots of the DFS are merged in the order determined by -r method. The complexity is O(n^2) (currently, there is a bug which causes more memory to be consumed than necessary).

merge_right: Same as merge_left, except that the merge is done in such a way that the inserted nodes remain as close as possible to their right neighbors in list2 ("insert as far right as possible"). For the example above, the ordering for g is (a,b,c,d,f1,e,f2,g). It has been observed experimentally that neither merge_left nor merge_right is superior to the other; there are cases where verification times out with merge_left but not merge_right, and vice versa.

-o <type>
Specify the network nodes for which MDD variables should be created. Type can be one of the following:

all: Order all the nodes of the network. This is normally not used.

input_and_latch: (default) Order the primary inputs, pseudo inputs, latches, and next state variables. This is the minimum set of nodes that need to be ordered to perform operations on FSMs (e.g. model checking, reachability). For purely combinational circuits, just the primary and pseudo inputs are ordered.

-r <method>
Specify which root ordering method to use. The "roots" of a network refer to the roots of the cones of logic driving the combinational outputs (data latch inputs, initial state latch inputs, and primary outputs) of a network. Root ordering is used to determine in which order to visit the roots of the network for the DFS carried out in node ordering (see -n). "Method" must be one of the following:

depth: (default for 30 or more latches) Roots are ordered based on logic depth (i.e. longest path to a combinational input). Greater depth roots appear earlier in the ordering. All data latch inputs appear before all other combinational outputs. The complexity is O(E+nlog(n)). It has been observed experimentally that mincomm produces superior orderings to depth. However, the complexity of the mincomm algorithm is such that it cannot produce orderings for designs with more than a hundred or so latches. Hence, for big designs, use depth, followed optionally by dynamic_var_ordering.

mincomm: (default for less than 30 latches) Uses the algorithm of Aziz, et al. "BDD Variable Ordering for Interacting Finite State Machines," DAC, 1994. First, the latches are ordered to decrease a communication complexity bound (where backward edges are more expensive than forward edges) on the latch communication graph. This directly gives an ordering for the data latch inputs. The remaining combinational outputs are ordered after the data latch inputs, in decreasing order of their depth. The total complexity is O(nlog(n)+E+k^3).

-s <type>
Used in conjunction with <file> to specify which nodes are supplied in the ordering file. Type can be one of the following (there is no default):

all: The ordering file supplies all the nodes of the network. The ordering generated is the supplied order, projected onto the set of nodes specified by -o.

input_and_latch: The ordering file supplies the primary inputs, pseudo inputs, latches, and next state variables. The ordering generated is exactly what is supplied (in the case of -o input_and_latch). -o all is incompatible with -s input_and_latch.

next_state_node: The ordering file supplies next state variables. During the ordering algorithm, the next state functions are visited in the order in which their corresponding next state variables appear in the file. The order of the next state variables in the ordering generated is not necessarily maintained.

partial: The ordering file supplies an arbitrary subset of nodes of the network. The ordering algorithm works by finding a total ordering on all the nodes (independent of the ordering supplied), then merging the computed order into the supplied order (maintaining the relative order of the supplied order), and then projecting the resulting ordering onto the set of nodes specified by -o.

-t <timeOut>
Time in seconds allowed to perform static ordering. If the flattened network has more than a couple hundred latches and you are using option -r mincomm, then you might want to set a timeOut to limit the allowed time. The default is no limit.

-v #
Print debug information.
0 Nothing is printed out. This is the default.

>= 1 Prints the nodes read from the input file (satisfying the supplied order type); prints the root order used for exploring the network.

>= 2 Prints the depth of nodes.

>= 3 Prints the ordering computed at each node.

<file>
A file containing names of network nodes, used to specify a variable ordering. The name of a node is the full hierarchical path name, starting from the current hierarchical node. A node should appear at most once in the file. Each node name should appear at the beginning of a new line, with no white space preceeding it. The end of a node name is marked by white space, and any other text on the rest of the line is ignored. Any line starting with "#" or white space is ignored. See write_order for a sample file. Note that the variable ordering cannot be specified at the bit-level; it can only be specified at the multi-valued variable level.
] SeeAlso [CommandWriteOrder] ******************************************************************************/ static int CommandStaticOrder( Hrc_Manager_t ** hmgr, int argc, char ** argv) { int c; FILE *fp; static int timeOutPeriod; static int verbose; static Ord_NodeMethod nodeMethod; static Ord_RootMethod rootMethod; static Ord_OrderType suppliedOrderType; static Ord_OrderType generatedOrderType; static boolean nsAfterSupport; lsList suppliedNodeList = (lsList) NULL; /* list of Ntk_Node_t * */ Ntk_Network_t *network; /* * These are the default values. These variables must be declared static * to avoid lint warnings. Since they are static, we must reinitialize * them outside of the variable declarations. */ timeOutPeriod = 0; verbose = 0; nodeMethod = Ord_NodesByDefault_c; rootMethod = Ord_RootsByDefault_c; suppliedOrderType = Ord_Unassigned_c; /* default */ generatedOrderType = Ord_InputAndLatch_c;/* default */ nsAfterSupport = FALSE; /* default */ /* * Parse the command line. */ util_getopt_reset(); while ((c = util_getopt(argc, argv, "av:o:s:t:n:r:h")) != EOF) { switch (c) { case 'a': nsAfterSupport = TRUE; break; case 'h': goto usage; case 'v': verbose = atoi(util_optarg); break; case 't': timeOutPeriod = atoi(util_optarg); break; case 'o': generatedOrderType = StringConvertToOrderType(util_optarg); if ((generatedOrderType == Ord_NextStateNode_c) || (generatedOrderType == Ord_Partial_c)) { (void) fprintf(vis_stderr, "disallowed output order type: %s\n", util_optarg); goto usage; } else if (generatedOrderType == Ord_Unassigned_c) { (void) fprintf(vis_stderr, "unknown output order type: %s\n", util_optarg); goto usage; } break; case 's': suppliedOrderType = StringConvertToOrderType(util_optarg); if (suppliedOrderType == Ord_Unassigned_c) { (void) fprintf(vis_stderr, "unknown input order type: %s\n", util_optarg); goto usage; } break; case 'n': if (strcmp("interleave", util_optarg) == 0) { nodeMethod = Ord_NodesByInterleaving_c; } else if (strcmp("merge_left", util_optarg) == 0) { nodeMethod = Ord_NodesByMergingLeft_c; } else if (strcmp("merge_right", util_optarg) == 0) { nodeMethod = Ord_NodesByMergingRight_c; } else if (strcmp("append", util_optarg) == 0) { nodeMethod = Ord_NodesByAppending_c; } else { (void) fprintf(vis_stderr, "unknown node order method: %s\n", util_optarg); goto usage; } break; case 'r': if (strcmp("depth", util_optarg) == 0) { rootMethod = Ord_RootsByDepth_c; } else if (strcmp("mincomm", util_optarg) == 0) { rootMethod = Ord_RootsByPerm_c; } else { (void) fprintf(vis_stderr, "unknown root order method: %s\n", util_optarg); goto usage; } break; default: goto usage; } } network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); if (network == NIL(Ntk_Network_t)) { return 1; } if ((suppliedOrderType == Ord_InputAndLatch_c) && (generatedOrderType == Ord_All_c)) { (void) fprintf(vis_stderr, "-o all -s input_and_latch not currently supported\n"); return 1; } /* * The minimum set of variables that can be ordered are those specified by * Ord_InputAndLatch_c. If these have already been ordered, then just return. */ if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c)) { (void) fprintf(vis_stderr, "Variables already ordered. "); (void) fprintf(vis_stderr, "Reinvoke flatten_hierarchy to undo variable ordering.\n"); return 1; } /* * Process the input ordering file. */ if (suppliedOrderType == Ord_Unassigned_c) { if (argc - util_optind > 0) { (void) fprintf(vis_stderr, "must specify -s if supplying order file\n"); goto usage; } } else { if (argc - util_optind == 0) { (void) fprintf(vis_stderr, "order file not provided\n"); goto usage; } else if (argc - util_optind > 1) { (void) fprintf(vis_stderr, "too many arguments\n"); goto usage; } fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0); if (fp == NIL(FILE)) { (void) fprintf(vis_stderr, "File %s is not readable, please check if it exists\n", argv[util_optind]); return 1; } else { boolean status; error_init(); status = Ord_FileReadNodeList(fp, network, &suppliedNodeList, verbose); if (status == FALSE) { (void) fprintf(vis_stderr, "Error reading ordering file:\n"); (void) fprintf(vis_stderr, "%s", error_string()); (void) fprintf(vis_stderr, "Cannot perform static ordering.\n"); (void) fclose(fp); return 1; } else if (NetworkCheckSuppliedNodeList(network, suppliedNodeList, suppliedOrderType) == FALSE) { (void) fprintf(vis_stderr, "Incorrect nodes supplied:\n"); (void) fprintf(vis_stderr, "%s", error_string()); (void) fprintf(vis_stderr, "Cannot perform static ordering.\n"); (void) fclose(fp); (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL); return 1; } else { (void) fclose(fp); if (verbose > 0) { (void) fprintf(vis_stdout, "\nNodes supplied in ordering file, "); (void) fprintf(vis_stdout, "according to -s option: \n"); OrdNodeListWrite(vis_stdout, suppliedNodeList); } } } } /* * In order for static ordering to proceed, network must not have any * combinational cycles. */ error_init(); if(Ntk_NetworkTestIsAcyclic(network) == 0) { (void) fprintf(vis_stderr, "Combinational cycle found: "); (void) fprintf(vis_stderr, "%s\n", error_string()); (void) fprintf(vis_stderr, "cannot perform static ordering\n"); if (suppliedOrderType != Ord_Unassigned_c) { (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL); } return 1; } /* Start the timer before calling the variable ordering routine. */ if (timeOutPeriod > 0){ (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); (void) alarm(timeOutPeriod); if (setjmp(timeOutEnv) > 0) { (void) fprintf(vis_stderr, "Timeout occurred after %d seconds.\n", timeOutPeriod); alarm(0); return 1; } } /* * Order the variables. */ Ord_NetworkOrderVariables(network, rootMethod, nodeMethod, nsAfterSupport, generatedOrderType, suppliedOrderType, suppliedNodeList, verbose); if (suppliedOrderType != Ord_Unassigned_c) { (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL); } /* * As a sanity check, make sure that all the variables in generatedOrderType * have an MDD id. */ assert(Ord_NetworkTestAreVariablesOrdered(network, generatedOrderType)); alarm(0); return 0; /* Everything okay */ usage: (void) fprintf(vis_stderr, "usage: static_order [-a] [-h] [-n method] [-o type] [-r method] -s type [-t time] [-v #] file\n"); (void) fprintf(vis_stderr, " -a order NS variables after support\n"); (void) fprintf(vis_stderr, " -h print the command usage\n"); (void) fprintf(vis_stderr, " -n method node ordering method\n"); (void) fprintf(vis_stderr, " (interleave (default), append, merge_left, merge_right)\n"); (void) fprintf(vis_stderr, " -o type nodes to order (all, input_and_latch (default))\n"); (void) fprintf(vis_stderr, " -r method root ordering method (depth, mincomm (default for < 30 latches))\n"); (void) fprintf(vis_stderr, " -s type nodes in file (all, input_and_latch, next_state_node, partial)\n"); (void) fprintf(vis_stderr, " -t time time out period (in seconds)\n"); (void) fprintf(vis_stderr, " -v # verbosity level\n"); (void) fprintf(vis_stderr, " file supplied ordering of nodes\n"); return 1; } /**Function******************************************************************** Synopsis [Implements the read_order command.] SideEffects [] CommandName [read_order] CommandSynopsis [Read and reorder variable order from a file.] CommandArguments [\[-h\] \[-v\] \[<file>\]] CommandDescription [This command reads variable order from a file and reorder variable order according to the order. This command can be used any time after static_order command. However, the users should notice that there is a possibility to get BDD blowups during this command.

Command options:

-h
Print the command usage.

-g <group>
Specify whether to group present and next state variables or not.

0: Do not group.

1: Do group (default).

-v
Print debug information.
<file>
A file containing names of network nodes, used to specify a variable ordering. The name of a node is the full hierarchical path name, starting from the current hierarchical node. A node should appear at most once in the file. Each node name should appear at the beginning of a new line, with no white space preceeding it. The end of a node name is marked by white space, and any other text on the rest of the line is ignored. Any line starting with "#" or white space is ignored. See write_order for a sample file. Note that the variable ordering cannot be specified at the bit-level; it can only be specified at the multi-valued variable level.
] SeeAlso [CommandStaticOrder CommandWriteOrder] ******************************************************************************/ static int CommandReadOrder( Hrc_Manager_t ** hmgr, int argc, char ** argv) { int c, status; FILE *fp; int verbose = 0; int group = 0; lsList suppliedNodeList = (lsList)NULL; /* list of Ntk_Node_t * */ Ntk_Network_t *network; mdd_manager *mddMgr; if (bdd_get_package_name() != CUDD) { fprintf(vis_stderr, "** ord error: read_order can be used only with the CUDD package\n"); } /* * Parse the command line. */ util_getopt_reset(); while ((c = util_getopt(argc, argv, "hg:v")) != EOF) { switch (c) { case 'h': goto usage; case 'g': group = atoi(util_optarg); break; case 'v': verbose = 1; break; default: goto usage; } } network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); if (network == NIL(Ntk_Network_t)) { return 1; } if (!Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c)) { (void) fprintf(vis_stderr, "** ord error: static_order was not called yet.\n"); return 1; } /* * Process the input ordering file. */ if (argc - util_optind == 0) { (void) fprintf(vis_stderr, "order file not provided\n"); goto usage; } else if (argc - util_optind > 1) { (void) fprintf(vis_stderr, "too many arguments\n"); goto usage; } fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0); if (fp == NIL(FILE)) { return 1; } else { boolean status; error_init(); status = Ord_FileReadNodeList(fp, network, &suppliedNodeList, verbose); if (status == FALSE) { (void) fprintf(vis_stderr, "Error reading ordering file:\n"); (void) fprintf(vis_stderr, "%s", error_string()); (void) fprintf(vis_stderr, "Cannot perform static ordering.\n"); (void) fclose(fp); return 1; } else if (NetworkCheckSuppliedNodeList(network, suppliedNodeList, Ord_InputAndLatch_c) == FALSE) { (void) fprintf(vis_stderr, "Incorrect nodes supplied:\n"); (void) fprintf(vis_stderr, "%s", error_string()); (void) fprintf(vis_stderr, "Cannot perform read_order.\n"); (void) fclose(fp); (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL); return 1; } else { (void) fclose(fp); if (verbose > 0) { (void) fprintf(vis_stdout, "\nNew variable order from file %s:\n", argv[util_optind]); OrdNodeListWrite(vis_stdout, suppliedNodeList); } } } /* * Reorder the variables. */ mddMgr = Ntk_NetworkReadMddManager(network); status = OrdMakeNewVariableOrder(mddMgr, suppliedNodeList, group, verbose); (void) lsDestroy(suppliedNodeList, (void (*) (lsGeneric)) NULL); if (status) return 1; alarm(0); return 0; /* Everything okay */ usage: (void) fprintf(vis_stderr, "usage: read_order [-g #] [-h] [-v] file\n"); (void) fprintf(vis_stderr, " -h print the command usage\n"); (void) fprintf(vis_stderr, " -g # ps/ns variables grouping\n"); (void) fprintf(vis_stderr, " 0 : do not group ps/ns\n"); (void) fprintf(vis_stderr, " 1 : group ps/ns (default)\n"); (void) fprintf(vis_stderr, " -v verbosity on\n"); (void) fprintf(vis_stderr, " file variable order file\n"); return 1; } /**Function******************************************************************** Synopsis [Implements the write_order command.] SideEffects [none] CommandName [write_order] CommandSynopsis [write the current order of the MDD variables of the flattened network] CommandArguments [\[-h\] \[-o <type>\] \[<file>\]] CommandDescription [Write the current order of the MDD variables of the flattened network. If no file name is specified, the output is written to stdout. A sample output is shown here.
  # name                 type            mddId vals levs
  system.choosing0      primary-input       31    2 (61)
  system.p0.pc          latch               32   11 (62, 63, 64, 65)
  
The first column gives the full hierarchical path name of the node, starting from the current hierarchical node. The second column gives the type of the node in the flattened network (see the command print_network). The third column gives the MDD id of the node; this can be thought of as just another name for the node. The fourth column gives the number of values that the multi-valued variable at the output of the node can assume. The last column gives the levels of the BDD variables that encode the multi-valued variable (0 is the topmost level of the BDD).

The bits of a multi-valued variable need not appear consecutively (due to dynamic variable ordering). Each node appears at most once in the output file. The nodes in the file appear in ascending order of the lowest level bit in the encoding of the node's multi-valued variable (e.g. a node with levels (12, 73) will appear before a node with levels (17, 21, 25)).

To specify a variable ordering for static_order, a convenient tactic is to write out the current ordering, edit the file to rearrange the ordering (or comment out some nodes, using "#"), and then read the file back in using static_order. Note that everything after the first column is ignored when the file is read in.

Command options:

-h
Print the command usage.

-o <type>
Specify the network nodes to write out. Type can be one of the following:

all: Write out all the nodes of the network. This option is allowed only if all variables have been ordered.

input_and_latch: (default) Write out the primary inputs, pseudo inputs, latches, and next state variables.

next_state_node: Write out the next state variables (node type is "shadow"). This file can be modified and read back in using the static_order -s next_state_node command.

<file>
File to which to write the ordering. By default, the ordering is written to stdout.

] ******************************************************************************/ static int CommandWriteOrder( Hrc_Manager_t ** hmgr, int argc, char ** argv) { int c; FILE *fp; int status; Ord_OrderType orderType = Ord_InputAndLatch_c; /* default */ Ntk_Network_t *network; /* * Parse the command line. */ util_getopt_reset(); while ((c = util_getopt(argc, argv, "ho:")) != EOF) { switch (c) { case 'h': goto usage; case 'o': orderType = StringConvertToOrderType(util_optarg); if (orderType == Ord_Partial_c) { (void) fprintf(vis_stderr, "disallowed output order type: %s\n", util_optarg); goto usage; } else if (orderType == Ord_Unassigned_c) { (void) fprintf(vis_stderr, "unknown output order type: %s\n", util_optarg); goto usage; } break; default: goto usage; } } network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); if (network == NIL(Ntk_Network_t)) { return 1; } /* * Open the destination file. */ if (argc - util_optind == 0) { fp = Cmd_FileOpen("-", "w", NIL(char *), /* silent */0); } else if (argc - util_optind == 1) { fp = Cmd_FileOpen(argv[util_optind], "w", NIL(char *), /* silent */0); } else { goto usage; } if (fp == NIL(FILE)) { return 1; } error_init(); if (Ord_NetworkPrintVariableOrder(fp, network, orderType) == 0) { (void) fprintf(vis_stderr, "Not all nodes are ordered: "); (void) fprintf(vis_stderr, "%s", error_string()); status = 1; } else { status = 0; /* success */ } if (fp != stdout) { (void) fclose(fp); } return (status); usage: (void) fprintf(vis_stderr, "usage: write_order [-h] [-o type] [file]\n"); (void) fprintf(vis_stderr, " -h print the command usage\n"); (void) fprintf(vis_stderr, " -o type nodes to write (all, input_and_latch (default), next_state_node)\n"); (void) fprintf(vis_stderr, " file output file name\n"); return 1; } /**Function******************************************************************** Synopsis [Implements the dynamic_var_ordering command.] SideEffects [] CommandName [dynamic_var_ordering] CommandSynopsis [control the application of dynamic variable ordering] CommandArguments [ \[-d\] \[-e <method>\] \[-f <method>\] \[-h\]] CommandDescription [Control the application of dynamic variable ordering to the flattened network. Dynamic ordering is a technique to reorder the MDD variables to reduce the size of the existing MDDs. When no options are specified, the current status of dynamic ordering is displayed. At most one of the options -e, -f, and -d should be specified. The commands flatten_hierarchy and static_order must be invoked before this command.

Dynamic ordering may be time consuming, but can often reduce the size of the MDDs dramatically. The good points to invoke dynamic ordering explicitly (using the -f option) are after the commands build_partition_mdds and print_img_info. If dynamic ordering finds a good ordering, then you may wish to save this ordering (using write_order) and reuse it (using static_order -s) in the future. A common sequence used to get a good ordering is the following:

  init_verify
  print_img_info
  dynamic_var_ordering -f sift
  write_order 
  flatten_hierarchy
  static_order -s input_and_latch -f 
  build_partition_mdds
  print_img_info
  dynamic_var_ordering -f sift
  

For many large examples, there is no single best variable order, or that order is hard to find. For example, the best ordering during partitioning of the network may be different from the best ordering during a model check. In that case you can use automatic reordering, using the -e option. This will trigger reordering whenever the total size of the MDD increases by a certain factor. Often, the init command is replaced by the following sequence:

  flatten_hierarchy 
  static_order
  dynamic_var_ordering -e sift
  build_partition_mdds
  
Command options:

-d
Disable dynamic ordering from triggering automatically.

-e <method>
Enable dynamic ordering to trigger automatically whenever a certain threshold on the overall MDD size is reached. "Method" must be one of the following:

window: Permutes the variables within windows of three adjacent variables so as to minimize the overall MDD size. This process is repeated until no more reduction in size occurs.

sift: Moves each variable throughout the order to find an optimal position for that variable (assuming all other variables are fixed). This generally achieves greater size reductions than the window method, but is slower.

The following methods are only available if VIS has been linked with the Bdd package from the University of Colorado (cuBdd).

random: Pairs of variables are randomly chosen, and swapped in the order. The swap is performed by a series of swaps of adjacent variables. The best order among those obtained by the series of swaps is retained. The number of pairs chosen for swapping equals the number of variables in the diagram.

random_pivot: Same as random, but the two variables are chosen so that the first is above the variable with the largest number of nodes, and the second is below that variable. In case there are several variables tied for the maximum number of nodes, the one closest to the root is used.

sift_converge: The sift method is iterated until no further improvement is obtained.

symmetry_sift: This method is an implementation of symmetric sifting. It is similar to sifting, with one addition: Variables that become adjacent during sifting are tested for symmetry. If they are symmetric, they are linked in a group. Sifting then continues with a group being moved, instead of a single variable.

symmetry_sift_converge: The symmetry_sift method is iterated until no further improvement is obtained.

window{2,3,4}: Permutes the variables within windows of n adjacent variables, where "n" can be either 2, 3 or 4, so as to minimize the overall MDD size.

window{2,3,4}_converge: The window{2,3,4} method is iterated until no further improvement is obtained.

group_sift: This method is similar to symmetry_sift, but uses more general criteria to create groups.

group_sift_converge: The group_sift method is iterated until no further improvement is obtained.

lazy_sift: This method is similar to group_sift, but the creation of groups takes into account the pairing of present and next state variables.

annealing: This method is an implementation of simulated annealing for variable ordering. This method is potentially very slow.

genetic: This method is an implementation of a genetic algorithm for variable ordering. This method is potentially very slow.

-f <method>
Force dynamic ordering to be invoked immediately. The values for method are the same as in option -e.

-h
Print the command usage.
-v <#>
Verbosity level. Default is 0. For values greater than 0, statistics pertaining to reordering will be printed whenever reordering occurs.
] ******************************************************************************/ static int CommandDynamicVarOrdering( Hrc_Manager_t ** hmgr, int argc, char ** argv) { int c; bdd_reorder_type_t currentMethod; bdd_reorder_type_t dynOrderingMethod = BDD_REORDER_NONE; /* for lint */ boolean disableFlag = FALSE; boolean enableFlag = FALSE; boolean forceFlag = FALSE; Ntk_Network_t *network; int verbosityFlag = -1; bdd_reorder_verbosity_t reorderVerbosity = BDD_REORDER_VERBOSITY_DEFAULT; /* * Parse the command line. */ util_getopt_reset(); while ((c = util_getopt(argc, argv, "df:e:hv:")) != EOF) { switch (c) { case 'h': goto usage; case 'f': forceFlag = TRUE; dynOrderingMethod = StringConvertToDynOrderType(util_optarg); if (dynOrderingMethod == BDD_REORDER_NONE) { (void) fprintf(vis_stderr, "unknown method: %s\n", util_optarg); goto usage; } break; case 'e': enableFlag = TRUE; dynOrderingMethod = StringConvertToDynOrderType(util_optarg); if (dynOrderingMethod == BDD_REORDER_NONE) { (void) fprintf(vis_stderr, "unknown method: %s\n", util_optarg); goto usage; } break; case 'd': disableFlag = TRUE; break; case 'v': verbosityFlag = atoi(util_optarg); break; default: goto usage; } } if (c == EOF && argc != util_optind) goto usage; switch (verbosityFlag) { case 0: reorderVerbosity = BDD_REORDER_NO_VERBOSITY; break; case 1: reorderVerbosity = BDD_REORDER_VERBOSITY; break; default: reorderVerbosity = BDD_REORDER_VERBOSITY_DEFAULT; break; } /* flatten_hierarchy and static_order must have been invoked already. */ network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); if (network == NIL(Ntk_Network_t)) { return 1; } if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c) == FALSE) { (void) fprintf(vis_stderr, "The MDD variables have not been ordered. "); (void) fprintf(vis_stderr, "Use static_order.\n"); return 1; } /* At most one option is allowed. */ if ((disableFlag && enableFlag) || (disableFlag && forceFlag) || (enableFlag && forceFlag)) { (void) fprintf(vis_stderr, "Only one of -d, -f, -e is allowed.\n"); return 1; } /* * Get the current method for reading and to save in case temporarily * overwritten. */ currentMethod = Ntk_NetworkReadDynamicVarOrderingMethod(network); /* If no options are given, then just display current status. */ if (!(disableFlag || enableFlag || forceFlag)) { if (currentMethod == BDD_REORDER_NONE) { (void) fprintf(vis_stdout, "Dynamic variable ordering is disabled.\n"); } else { (void) fprintf(vis_stdout, "Dynamic variable ordering is enabled "); (void) fprintf(vis_stdout, "with method %s.\n", DynOrderTypeConvertToString(currentMethod)); } } if (disableFlag) { if (currentMethod == BDD_REORDER_NONE) { (void) fprintf(vis_stdout, "Dynamic variable ordering is already disabled.\n"); } else { (void) fprintf(vis_stdout, "Dynamic variable ordering is disabled.\n"); Ntk_NetworkSetDynamicVarOrderingMethod(network, BDD_REORDER_NONE, reorderVerbosity); } } /* * Set the dynamic ordering method of the network. Note that * Ntk_NetworkSetDynamicVarOrderingMethod makes the necessary call to * bdd_dynamic_reordering. */ if (enableFlag) { Ntk_NetworkSetDynamicVarOrderingMethod(network, dynOrderingMethod, reorderVerbosity); if (bdd_get_package_name() != CUDD) dynOrderingMethod = Ntk_NetworkReadDynamicVarOrderingMethod(network); (void) fprintf(vis_stdout, "Dynamic variable ordering is enabled with method %s.\n", DynOrderTypeConvertToString(dynOrderingMethod)); } /* * Force a reordering. Note that the mddManager has to have the method set * before calling bdd_reorder. This is done via a call to * Ntk_NetworkSetDynamicVarOrderingMethod with dynOrderingMethod. The value * of the ordering method is restored afterwards. */ if (forceFlag) { mdd_manager *mddManager = Ntk_NetworkReadMddManager(network); bdd_reorder_verbosity_t prevReorderVerbosity; prevReorderVerbosity = bdd_reordering_reporting(mddManager); (void) fprintf(vis_stdout, "Dynamic variable ordering forced "); (void) fprintf(vis_stdout, "with method %s....\n", DynOrderTypeConvertToString(dynOrderingMethod)); Ntk_NetworkSetDynamicVarOrderingMethod(network, dynOrderingMethod, reorderVerbosity); bdd_reorder(Ntk_NetworkReadMddManager(network)); Ntk_NetworkSetDynamicVarOrderingMethod(network, currentMethod, prevReorderVerbosity); } return 0; /* Everything okay */ usage: (void) fprintf(vis_stderr, "usage: dynamic_var_ordering [-d] [-e method] [-f method] [-h]\n"); (void) fprintf(vis_stderr, " -d disable dynamic ordering\n"); (void) fprintf(vis_stderr, " -e method enable dynamic ordering with method (window, sift)\n"); (void) fprintf(vis_stderr, " -f method force dynamic ordering with method (window, sift)\n"); (void) fprintf(vis_stderr, " -h print the command usage\n"); (void) fprintf(vis_stderr, " -v # verbosity level \n"); return 1; } /**Function******************************************************************** Synopsis [Implements the print_bdd_stats command.] SideEffects [] CommandName [print_bdd_stats] CommandSynopsis [print the BDD statistics for the flattened network] CommandArguments [\[-h\]] CommandDescription [Print the BDD statistics for the flattened network. The MDDs representing the functions of the network are themselves represented by BDDs via an encoding of the multi-valued variables into binary valued variables. The statistics given by this command depend on the underlying BDD package with which VIS was linked. To get more information about the statistics, consult the documentation for the given BDD package. The commands flatten_hierarchy and static_order must be invoked before this command.

Command options:

-h
Print the command usage.
] ******************************************************************************/ static int CommandPrintBddStats( Hrc_Manager_t ** hmgr, int argc, char ** argv) { int c; Ntk_Network_t *network; /* * Parse the command line. */ util_getopt_reset(); while ((c = util_getopt(argc, argv, "h")) != EOF) { switch (c) { case 'h': goto usage; default: goto usage; } } /* flatten_hierarchy and static_order must have been invoked already. */ network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); if (network == NIL(Ntk_Network_t)) { return 1; } if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c) == FALSE) { (void) fprintf(vis_stderr, "The MDD variables have not been ordered. "); (void) fprintf(vis_stderr, "Use static_order.\n"); return 1; } bdd_print_stats(Ntk_NetworkReadMddManager(network), vis_stdout); return 0; /* Everything okay */ usage: (void) fprintf(vis_stderr, "usage: print_bdd_stats [-h]\n"); (void) fprintf(vis_stderr, " -h print the command usage\n"); return 1; } /**Function******************************************************************** Synopsis [Converts a string to an order type.] Description [Converts a string to an order type. If string does not refer to one of the allowed order types, then returns Ord_Unassigned_c.] SideEffects [] ******************************************************************************/ static Ord_OrderType StringConvertToOrderType( char *string) { if (strcmp("all", string) == 0) { return Ord_All_c; } else if (strcmp("input_and_latch", string) == 0) { return Ord_InputAndLatch_c; } else if (strcmp("next_state_node", string) == 0) { return Ord_NextStateNode_c; } else if (strcmp("partial", string) == 0) { return Ord_Partial_c; } else { return Ord_Unassigned_c; } } /**Function******************************************************************** Synopsis [Converts a string to a dynamic ordering method type.] Description [Converts a string to a dynamic ordering method type. If string is not "sift" or "window", then returns BDD_REORDER_NONE.] SideEffects [] ******************************************************************************/ static bdd_reorder_type_t StringConvertToDynOrderType( char *string) { if (strcmp("sift", string) == 0) { return BDD_REORDER_SIFT; } else if (strcmp("window", string) == 0) { return BDD_REORDER_WINDOW; } else if (strcmp("random", string) == 0) { return BDD_REORDER_RANDOM; } else if (strcmp("random_pivot", string) == 0) { return BDD_REORDER_RANDOM_PIVOT; } else if (strcmp("sift_converge", string) == 0) { return BDD_REORDER_SIFT_CONVERGE; } else if (strcmp("symmetry_sift", string) == 0) { return BDD_REORDER_SYMM_SIFT; } else if (strcmp("symmetry_sift_converge", string) == 0) { return BDD_REORDER_SYMM_SIFT_CONV; } else if (strcmp("window2", string) == 0) { return BDD_REORDER_WINDOW2; } else if (strcmp("window3", string) == 0) { return BDD_REORDER_WINDOW3; } else if (strcmp("window4", string) == 0) { return BDD_REORDER_WINDOW4; } else if (strcmp("window2_converge", string) == 0) { return BDD_REORDER_WINDOW2_CONV; } else if (strcmp("window3_converge", string) == 0) { return BDD_REORDER_WINDOW3_CONV; } else if (strcmp("window4_converge", string) == 0) { return BDD_REORDER_WINDOW4_CONV; } else if (strcmp("group_sift", string) == 0) { return BDD_REORDER_GROUP_SIFT; } else if (strcmp("group_sift_converge", string) == 0) { return BDD_REORDER_GROUP_SIFT_CONV; } else if (strcmp("annealing", string) == 0) { return BDD_REORDER_ANNEALING; } else if (strcmp("genetic", string) == 0) { return BDD_REORDER_GENETIC; } else if (strcmp("exact", string) == 0) { return BDD_REORDER_EXACT; } else if (strcmp("lazy_sift", string) == 0) { return BDD_REORDER_LAZY_SIFT; } else { return BDD_REORDER_NONE; } } /**Function******************************************************************** Synopsis [Converts a dynamic ordering method type to a string.] Description [Converts a dynamic ordering method type to a string. This string must NOT be freed by the caller.] SideEffects [] ******************************************************************************/ static char * DynOrderTypeConvertToString( bdd_reorder_type_t method) { if (method == BDD_REORDER_SIFT) { return "sift"; } else if (method == BDD_REORDER_WINDOW) { return "window"; } else if (method == BDD_REORDER_NONE) { return "none"; } else if (method == BDD_REORDER_RANDOM) { return "random"; } else if (method == BDD_REORDER_RANDOM_PIVOT) { return "random_pivot"; } else if (method == BDD_REORDER_SIFT_CONVERGE) { return "sift_converge"; } else if (method == BDD_REORDER_SYMM_SIFT) { return "symmetry_sift"; } else if (method == BDD_REORDER_SYMM_SIFT_CONV) { return "symmetry_sift_converge"; } else if (method == BDD_REORDER_WINDOW2) { return "window2"; } else if (method == BDD_REORDER_WINDOW3) { return "window3"; } else if (method == BDD_REORDER_WINDOW4) { return "window4"; } else if (method == BDD_REORDER_WINDOW2_CONV) { return "window2_converge"; } else if (method == BDD_REORDER_WINDOW3_CONV) { return "window3_converge"; } else if (method == BDD_REORDER_WINDOW4_CONV) { return "window4_converge"; } else if (method == BDD_REORDER_GROUP_SIFT) { return "group_sift"; } else if (method == BDD_REORDER_GROUP_SIFT_CONV) { return "group_sift_converge"; } else if (method == BDD_REORDER_ANNEALING) { return "annealing"; } else if (method == BDD_REORDER_GENETIC) { return "genetic"; } else if (method == BDD_REORDER_EXACT) { return "exact"; } else if (method == BDD_REORDER_LAZY_SIFT) { return "lazy_sift"; } else { fail("unrecognized method"); return NIL(char); /* not reached */ } } /**Function******************************************************************** Synopsis [Verifies that suppliedNodeList has the correct nodes.] Description [Returns TRUE if the set of nodes in suppliedNodeList matches the set of nodes in network specified by orderType; else returns FALSE and writes a message to error_string. OrderType should be one of the following: 1) Ord_All_c: should match the set of all nodes in network; 2) Ord_InputAndLatch_c: should match the set of inputs (primary + pseudo), latches, and next state nodes; 3) Ord_NextStateNode_c: should match the set of next state nodes; number should be the number of latches; 4) Ord_Partial_c: returns TRUE automatically.] SideEffects [] ******************************************************************************/ static boolean NetworkCheckSuppliedNodeList( Ntk_Network_t * network, lsList suppliedNodeList, Ord_OrderType orderType) { lsGen gen; st_generator *stGen; Ntk_Node_t *node; st_table *requiredNodes; st_table *suppliedNodes; char *dummy; boolean returnFlag = TRUE; assert(orderType != Ord_Unassigned_c); if (orderType == Ord_Partial_c) { return TRUE; } /* At this point, orderType must be one of the these. */ assert((orderType == Ord_All_c) || (orderType == Ord_InputAndLatch_c) || (orderType == Ord_NextStateNode_c)); /* * Build up the table of required nodes. Next state nodes are included by * all 3 order types. */ requiredNodes = st_init_table(st_ptrcmp, st_ptrhash); Ntk_NetworkForEachNode(network, gen, node) { if ((orderType == Ord_All_c) || Ntk_NodeTestIsNextStateNode(node)) { st_insert(requiredNodes, (char *) node, NIL(char)); } else if ((orderType == Ord_InputAndLatch_c) && Ntk_NodeTestIsCombInput(node)) { st_insert(requiredNodes, (char *) node, NIL(char)); } /* else, this node is not included by orderType */ } /* * Convert suppliedNodeList to the table of supplied nodes. */ suppliedNodes = st_init_table(st_ptrcmp, st_ptrhash); lsForEachItem(suppliedNodeList, gen, node) { int status = st_insert(suppliedNodes, (char *) node, NIL(char)); if (status) { error_append("node "); error_append(Ntk_NodeReadName(node)); error_append(" appears more than once in ordering file\n"); returnFlag = FALSE; } } /* * Check that suppliedNodes is contained in requiredNodes. */ st_foreach_item(suppliedNodes, stGen, &node, &dummy) { if (!st_is_member(requiredNodes, node)) { error_append("node "); error_append(Ntk_NodeReadName(node)); error_append(" supplied but not required\n"); returnFlag = FALSE; } } /* * Check that suppliedNodes is contained in requiredNodes. */ st_foreach_item(requiredNodes, stGen, &node, &dummy) { if (!st_is_member(suppliedNodes, node)) { error_append("node "); error_append(Ntk_NodeReadName(node)); error_append(" required but not supplied\n"); returnFlag = FALSE; } } st_free_table(requiredNodes); st_free_table(suppliedNodes); return returnFlag; } /**Function******************************************************************** Synopsis [Handle function for timeout.] Description [This function is called when the time out occurs.] SideEffects [] ******************************************************************************/ static void TimeOutHandle(void) { longjmp(timeOutEnv, 1); }