[11] | 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 | |
---|
| 176 | References |
---|
| 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 |
---|