[11] | 1 | |
---|
| 2 | set - set an environment variable |
---|
| 3 | _________________________________________________________________ |
---|
| 4 | |
---|
| 5 | set [-h] [<name>] [<value>] |
---|
| 6 | |
---|
| 7 | A variable environment is maintained by the command interpreter. The |
---|
| 8 | "set" command sets a variable to a particular value, and the "unset" |
---|
| 9 | command removes the definition of a variable. If "set" is given no |
---|
| 10 | arguments, it prints the current value of all variables. |
---|
| 11 | |
---|
| 12 | Command options: |
---|
| 13 | |
---|
| 14 | -h |
---|
| 15 | Print the command usage. |
---|
| 16 | |
---|
| 17 | <name> |
---|
| 18 | Variable name |
---|
| 19 | |
---|
| 20 | <value> |
---|
| 21 | Value to be assigned to the variable. |
---|
| 22 | |
---|
| 23 | Interpolation of variables is allowed when using the set command. The |
---|
| 24 | variables are referred to with the prefix of '$'. So for example, the |
---|
| 25 | following can be done to check the value of a set variable: |
---|
| 26 | vis> set foo bar |
---|
| 27 | vis> echo $foo |
---|
| 28 | bar |
---|
| 29 | The last line "bar" will the output produced by vis. |
---|
| 30 | |
---|
| 31 | Variables can be extended by using the character ':' to concatenate |
---|
| 32 | values. For example : |
---|
| 33 | vis> set foo bar |
---|
| 34 | vis> set foo $foo:foobar |
---|
| 35 | vis> echo $foo |
---|
| 36 | bar:foobar |
---|
| 37 | The variable foo is extended with the value foobar . |
---|
| 38 | |
---|
| 39 | Whitespace characters may be present within quotes. However, variable |
---|
| 40 | interpolation lays the restriction that the characters ':' and '/' may |
---|
| 41 | not be used within quotes. This is to allow for recursive |
---|
| 42 | interpolation. So for example, the following is allowed |
---|
| 43 | vis> set "foo bar" this |
---|
| 44 | vis> echo $"foo bar" |
---|
| 45 | this |
---|
| 46 | The last line will be the output produced by vis. |
---|
| 47 | But in the following, the value of the variable foo/bar will not be |
---|
| 48 | interpreted correctly: |
---|
| 49 | |
---|
| 50 | vis> set "foo/bar" this |
---|
| 51 | vis> echo $"foo/bar" |
---|
| 52 | foo/bar |
---|
| 53 | If a variable is not set by the "set" command, then the variable is |
---|
| 54 | returned unchanged. |
---|
| 55 | |
---|
| 56 | Different commands use environment information for different purposes. |
---|
| 57 | The command interpreter makes use of the following parameters: |
---|
| 58 | |
---|
| 59 | autoexec |
---|
| 60 | Defines a command string to be automatically executed after |
---|
| 61 | every command processed by the command interpreter. This is |
---|
| 62 | useful for things like timing commands, or tracing the progress |
---|
| 63 | of optimization. |
---|
| 64 | |
---|
| 65 | open_path |
---|
| 66 | "open_path" (in analogy to the shell-variable PATH) is a list |
---|
| 67 | of colon-separated strings giving directories to be searched |
---|
| 68 | whenever a file is opened for read. Typically the current |
---|
| 69 | directory (.) is first in this list. The standard system |
---|
| 70 | library (typically $VIS_LIBRARY_PATH) is always implicitly |
---|
| 71 | appended to the current path. This provides a convenient |
---|
| 72 | short-hand mechanism for reaching standard library files. |
---|
| 73 | |
---|
| 74 | vis_stderr |
---|
| 75 | Standard error (normally stderr) can be re-directed to a file |
---|
| 76 | by setting the variable vis_stderr. |
---|
| 77 | |
---|
| 78 | vis_stdout |
---|
| 79 | Standard output (normally stdout) can be re-directed to a file |
---|
| 80 | by setting the variable vis_stdout. |
---|
| 81 | |
---|
| 82 | Building MDDs for the network makes use of following setting: |
---|
| 83 | |
---|
| 84 | partition_method |
---|
| 85 | This parameter is used to select the method for creating the |
---|
| 86 | partition. The vertices of a partition correspond to the |
---|
| 87 | combinational inputs, combinational outputs, and any |
---|
| 88 | intermediate nodes used. Each vertex has a multi-valued |
---|
| 89 | function (represented by MDDs) expressing the function of the |
---|
| 90 | corresponding network node in terms of the partition vertices |
---|
| 91 | in its transitive fanin. Hence, the MDDs of the partition |
---|
| 92 | represent a partial collapsing of the network. The possible |
---|
| 93 | values of partition_method are: |
---|
| 94 | |
---|
| 95 | inout |
---|
| 96 | Expresses the combinational outputs in terms of the |
---|
| 97 | combinational inputs. This is the default partitioning |
---|
| 98 | method. |
---|
| 99 | |
---|
| 100 | total |
---|
| 101 | The partition built is isomorphic to the combinational |
---|
| 102 | part of the network. The function of each node is |
---|
| 103 | expressed in terms of its immediate fanins. |
---|
| 104 | |
---|
| 105 | frontier |
---|
| 106 | The partition built contains the combinational part of |
---|
| 107 | the network as well as vertices corresponding to some |
---|
| 108 | intermediate nodes. These vertices are generated to |
---|
| 109 | control the MDD sizes of the combinational outputs. The |
---|
| 110 | number of intermediate variables can be controlled by the |
---|
| 111 | parameter "partition_threshold". The method "inout" and |
---|
| 112 | "total" are special cases of this method (corresponding |
---|
| 113 | to a partition_threshold of infinity and 0 respectively). |
---|
| 114 | |
---|
| 115 | partition_threshold |
---|
| 116 | This parameter is used in conjuction with the selection of |
---|
| 117 | "frontier" as partition method. This determines the threshold |
---|
| 118 | at which a new MDD variable is created in the partition. |
---|
| 119 | |
---|
| 120 | Image computation makes use of following settings: |
---|
| 121 | |
---|
| 122 | image_method |
---|
| 123 | The "image_method" parameter is used to control the image |
---|
| 124 | method used in various symbolic analysis techniques. Currently, |
---|
| 125 | two image methods are implemented. Use "set image_method |
---|
| 126 | <method>" to choose the appropriate method. |
---|
| 127 | |
---|
| 128 | monolithic |
---|
| 129 | This is the most naive approach possible. However, this |
---|
| 130 | method is not suitable for circuits with more than 20 |
---|
| 131 | latches. |
---|
| 132 | |
---|
| 133 | tfm |
---|
| 134 | This is the pure transition function method. This method |
---|
| 135 | is supposed not to be used in general fixpoint |
---|
| 136 | computations. Approximate traversal is an application of |
---|
| 137 | this method. Basically this method is made as a part of |
---|
| 138 | hybrid method. For more detailed options, see the help of |
---|
| 139 | print_tfm_options command. |
---|
| 140 | |
---|
| 141 | hybrid |
---|
| 142 | This is a hybrid method combining transition relation and |
---|
| 143 | function methods. Transition relation method is based on |
---|
| 144 | conjunction of partitioned transition relation, whereas |
---|
| 145 | transition function method is based on splitting on an |
---|
| 146 | input or output variable recursively. The hybrid method |
---|
| 147 | choose either splitting or conjunction at each recursion |
---|
| 148 | dynamically using the dependence matrix. For details, |
---|
| 149 | refer to the paper "To split or to Conjoin: The Question |
---|
| 150 | in Image Computation" by In-Ho Moon, James Kukula, Kavita |
---|
| 151 | Ravi, and Fabio Somenzi, DAC'00. Also for more detailed |
---|
| 152 | options, see the help of print_hybrid_options command. |
---|
| 153 | |
---|
| 154 | iwls95 |
---|
| 155 | This technique is based on the early variable |
---|
| 156 | quantification and related heuristics of Ranjan, et al. |
---|
| 157 | "Efficient BDD Algorithms for FSM Synthesis and |
---|
| 158 | Verification", IWLS 1995. First, from the given |
---|
| 159 | multivalued functions, bit level relations are created. |
---|
| 160 | These relations are then clustered based on the value of |
---|
| 161 | threshold value controlled by image_cluster_size |
---|
| 162 | parameter. Next the relations are ordered for early |
---|
| 163 | variable quantification. This ordering is controlled by |
---|
| 164 | the parameters image_W1, image_W2, image_W3, and |
---|
| 165 | image_W4. |
---|
| 166 | |
---|
| 167 | mlp |
---|
| 168 | This technique is based on minimizing the variable |
---|
| 169 | lifetime in the conjunctions of the partitioned |
---|
| 170 | transition relation. The method is called MLP (Minimal |
---|
| 171 | Lifetime Permutation). For details, refer to the paper |
---|
| 172 | "Border-Block Triangular Form and Conjunction Schedule in |
---|
| 173 | Image Computation" by In-Ho Moon, Gary Hachtel, and Fabio |
---|
| 174 | Somenzi, FMCAD'00. Also for more detailed options, see |
---|
| 175 | the help of print_mlp_options command. |
---|
| 176 | |
---|
| 177 | image_farside_method |
---|
| 178 | This parameter is used in conjunction with the selection of |
---|
| 179 | iwls95, mlp, orlinear as the image_method. When the value is 1, |
---|
| 180 | the compositional far side image computation approach is |
---|
| 181 | enabled; when the value is 0, this feature is disabled |
---|
| 182 | (default). |
---|
| 183 | |
---|
| 184 | image_cluster_size |
---|
| 185 | This parameter is used in conjunction with the selection of |
---|
| 186 | iwls95 as the image_method. The value of this parameter is used |
---|
| 187 | as threshold value for creating clusters. The default value of |
---|
| 188 | this parameter is 5000 which has been empirically proved to be |
---|
| 189 | an optimal value. |
---|
| 190 | |
---|
| 191 | image_W1, image_W2, image_W3, image_W4 |
---|
| 192 | These parameters are used in conjunction with the selection of |
---|
| 193 | iwls95 as the image_method. They control the weights associated |
---|
| 194 | with various factors in ordering the clusters. The default |
---|
| 195 | values are 6, 1, 1, and 2 respectively. For a detailed |
---|
| 196 | description of these parameters, please refer to the paper in |
---|
| 197 | IWLS'95 proceedings. |
---|
| 198 | |
---|
| 199 | image_verbosity |
---|
| 200 | Sets the verbosity mode (0 minimum to 4 maximum), for the image |
---|
| 201 | method iwls95. |
---|
| 202 | |
---|
| 203 | image_minimize_method <method> |
---|
| 204 | Sets a minimization method to minimize the transition relation |
---|
| 205 | or an image/preimage computaion with a set of dont-care states. |
---|
| 206 | |
---|
| 207 | Methods: 0 : restrict (default). |
---|
| 208 | |
---|
| 209 | 1 : constrain |
---|
| 210 | |
---|
| 211 | 2 : compact (currently supported by only CUDD) |
---|
| 212 | |
---|
| 213 | 3 : squeeze (currently supported by only CUDD) |
---|
| 214 | |
---|
| 215 | scc_method <method> |
---|
| 216 | Sets the symbolic method to enumerate strongly connected |
---|
| 217 | components (SCCs). Symbolic SCC enumeration is the core |
---|
| 218 | computation in LTL and fair-CTL model checking. |
---|
| 219 | |
---|
| 220 | Methods: lockstep : the O(nlogn) time LockStep algorithm |
---|
| 221 | (default). |
---|
| 222 | |
---|
| 223 | Methods: linearstep : the linear time symbolic algorithm |
---|
| 224 | (default). |
---|
| 225 | _________________________________________________________________ |
---|
| 226 | |
---|
| 227 | Last updated on 20050519 10h16 |
---|