source: vis_dev/vis-2.1/share/help/setCmd.txt @ 15

Last change on this file since 15 was 11, checked in by cecile, 13 years ago

Add vis

File size: 10.3 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
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
Note: See TracBrowser for help on using the repository browser.