source: vis_dev/vis-2.3/share/help/setCmd.txt @ 64

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

vis2.3

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