source: vis_dev/vis-2.1/share/help/approximate_model_checkCmd.txt @ 11

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

Add vis
File size: 8.2 KB
Line 
1
2  approximate_model_check - perform ACTL model checking on an abstracted and
3  flattened network
4     _________________________________________________________________
5
6   approximate_model_check [-h] [-v <verbosity_level>] <ctl_file>
7
8   Performs  ACTL  model checking on an abstracted and flattened network.
9   Predefined  abstractions are performed prior to model checking. Before
10   calling  this  command, the user should have initialized the design by
11   calling the command [1]init_verify.
12
13   The  command  includes  two  dual  algorithms.  The  user  should  set
14   appropriate  environment  parameters  associated  with  the command to
15   execute  proper algorithm. By default, the command makes its effort to
16   prove  whether  given  ACTL  formula is positive. To check whether the
17   ACTL  formula  is  negative, user should set the environment parameter
18   amc_prove_false  prior  to executing the command. See [2]below for the
19   environment parameters associated with this command.
20
21   Properties  to  be verified should be provided as ACTL formulas in the
22   file  <ctl_file>.  The command only accepts ACTL formulas. Mixed, ECTL
23   expressions  are  not  supported. ACTL formulas are those in which all
24   quantifiers are universal and negation is only allowed at the level of
25   atomic  propositions.  For the precise syntax of CTL formulas, see the
26   [3]VIS CTL and LTL syntax manual.
27
28   The  command  is  designed  to  tackle  the state explosion problem we
29   encounter  when  dealing with large and complex circuits. Based on the
30   initial   size   of   the  group,  the  command  constructs  over-  or
31   under-approximation  of the transition relation of the system. A group
32   (subsystem)  is  a portion of the original circuit containing a subset
33   of  the  latches and their next state functions. The initial size of a
34   group  can  be  set with the [4]amc_sizeof_group environment variable.
35   These initial approximations may not contain every detail of the exact
36   system.  However  they  may  contain  enough  information to determine
37   whether  the formula is positive or negative. Starting from an initial
38   coarse  approximation,  the  command makes its effort to prove whether
39   given  ACTL  formula is positive or negative. When the procedure fails
40   to  prove  correctness  of the formula with initial approximations, it
41   automatically refines the approximations. It repeats the process until
42   the  algorithm  produces  a reliable result or the available resources
43   are exhausted.
44
45   Due   to  the  overhead  procedures,  for  some  circuits,  the  exact
46   [5]model_check   method   may   evaluate  formulas  faster  with  less
47   resources.  If  any  formula  evaluates  to  false,  a  debug trace is
48   reported.
49
50   The  command  does not use fairness constraints even if they have been
51   read with the [6]read_fairness command.
52
53   Command options:
54
55   -h
56          Print the command usage.
57
58   -v <verbosity_level>
59          Specify  verbosity  level.  verbosity_level  must be one of the
60          following:
61
62          0 : No feedback provided. This is the default.
63          1 : Some feedback.
64          2 : Lots of feedback.
65
66   -t <timeOutPeriod>
67          Specify  the  time  out  period  (in  seconds)  after which the
68          command aborts. By default this option is set to infinity.
69
70   <ctl_file>
71          File containing ACTL formulas to be model checked.
72
73   Environment Parameters:
74
75   Environment  parameters  should  be set using the set command from the
76   VIS shell
77   (e.g. vis> set amc_prove_false).
78
79   amc_prove_false
80          When the parameter is set, the command makes its effort to
81          prove whether given ACTL formula is negative. The command
82          constructs a set of under-approximations of the transition
83          relations of the system. When the formula evaluates to false, a
84          debug trace is reported by default.
85
86   amc_grouping_method <grouping method>
87          Specifies grouping method. Grouping method is a method for
88          grouping number of latches into single subsystem. Two methods
89          are supported.
90
91          Grouping  based  on  hierarchy(default)  :  The  method  groups
92          latches based on the hierarchy of the system. Normally, complex
93          circuits  are  designed  in  multiple  processes.  Furthermore,
94          processes  form  a  hierarchy. The method uses this information
95          provided  by  the  original  design. When a design described in
96          high  level  description language is transformed into low level
97          BLIF  format,  the  processes are transformed into subcircuits.
98          The   method   groups   those  latches  that  are  within  same
99          subcircuit.
100
101          Grouping  based  on  latch  dependencies(latch_dependency): The
102          method  groups  those latches that are closely related. Closely
103          related latches are those who has many (transitive) connections
104          between them.
105
106          When  the  parameter  is  not specified, the command by default
107          uses hierarchical grouping method.
108
109   amc_sizeof_group <integer value>
110          Determines the number of latches in each group(subsystem). The
111          default value is 8. The initial size of the subsystem
112          determines the initial degree of approximations of the
113          transition relations. There's no proven rule of setting the
114          value. Some experimental results show that setting the value to
115          about 5-20% of overall number of latches is reasonable(e.g. if
116          the system contains 100 latches set the value to 5-20).
117          However, the suggested range may not work well with some
118          examples.
119
120   amc_DC_level <integer value>
121          Specifies don't care levels. Default level is 0. Absence of the
122          parameter sets the amc_DC_level to 0.
123          amc_DC_level must be one of the following:
124
125        0: No don't cares are used. This is the default.
126
127        1: Use unreachable states as don't cares.
128
129        2: Aggressively use DC's to simplify MDD's in model checking.
130
131          Using  don't  cares  may take more time for some examples since
132          the approximate model checker computes the reachable states for
133          each  subsystem.  For  some large circuits it is undesirable to
134          set don't care level.
135
136   Related "set" options:
137
138   ctl_change_bracket <yes/no>
139          Vl2mv  automatically  converts  "[]"  to  "<>"  in  node names,
140          therefore  CTL  parser  does  the  same thing. However, in some
141          cases a user does not want to change node names in CTL parsing.
142          Then, use this set option by giving "no". Default is "yes".
143
144   See also commands : model_check, incremental_ctl_verification
145
146   Examples:
147   Here  are  some  example  sequences  of  the  VIS executions using the
148   approximate model checker.
149
150   read_blif_mv abp/abp.mv
151   flatten_hierarchy
152   static_order
153   build_partition_mdds
154   set amc_sizeof_group 4
155   approximate_model_check abp/abpt.ctl
156   time
157   quit
158
159   read_blif_mv coherence/coherence.mv
160   flatten_hierarchy
161   static_order
162   build_partition_mdds
163   set amc_sizeof_group 8
164   set amc_prove_false
165   set amc_DC_level 0
166   approximate_model_check coherence/coherence2.ctl
167   time
168   quit
169
170   The  algorithm  used by approximate_model_check is described in detail
171   in [7]ftp://vlsi.colorado.edu/pub/iccad96.ps
172     _________________________________________________________________
173
174   Last updated on 20050519 10h16
175
176References
177
178   1. file://localhost/projects/development/hsv/vis/common/doc/html/init_verifyCmd.html
179   2. file://localhost/projects/development/hsv/vis/common/doc/html/approximate_model_checkCmd.html#environment
180   3. file://localhost/projects/development/hsv/vis/common/doc/ctl/ctl/ctl.html
181   4. file://localhost/projects/development/hsv/vis/common/doc/html/approximate_model_checkCmd.html#sizeofgroup
182   5. file://localhost/projects/development/hsv/vis/common/doc/html/model_checkCmd.html
183   6. file://localhost/projects/development/hsv/vis/common/doc/html/read_fairnessCmd.html
184   7. ftp://vlsi.colorado.edu/pub/iccad96.ps
Note: See TracBrowser for help on using the repository browser.