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 |
---|