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