[14] | 1 | |
---|
| 2 | lang_empty - perform language emptiness check on a flattened network |
---|
| 3 | _________________________________________________________________ |
---|
| 4 | |
---|
| 5 | lang_empty [-b] [-d <dbg_level>] [-f <dbg_file>] [-h] [-i] [-s] [-t |
---|
| 6 | <time_out_period>] [-v <verbosity_level>] [-A <le_method>] [-D <dc_level>] |
---|
| 7 | [-S <schedule>] [-L <lockstep_mode>] |
---|
| 8 | |
---|
| 9 | Performs language emptiness check on a flattened network. The language is |
---|
| 10 | not empty when there is a fair path starting at an initial state. Before |
---|
| 11 | calling this command, the user should have initialized the design by calling |
---|
| 12 | the command [1]init_verify. |
---|
| 13 | |
---|
| 14 | A fairness constraint can be read in by calling the [2]read_fairness |
---|
| 15 | command; if none is specified, all paths are taken to be fair. |
---|
| 16 | |
---|
| 17 | The system is reduced automatically with respect to the set of fairness |
---|
| 18 | constraints. If the language is not empty, a proof of this fact is |
---|
| 19 | generated. A proof is a fair path starting at an initial state. This is |
---|
| 20 | represented by a finite sequence of states starting at an initial state (the |
---|
| 21 | stem) leading to a fair cycle, i.e., a cycle on which there lies a state |
---|
| 22 | from each fairness condition. |
---|
| 23 | |
---|
| 24 | Command options: |
---|
| 25 | |
---|
| 26 | -b |
---|
| 27 | Use backward analysis when performing debugging; the default is to |
---|
| 28 | use forward analysis. This should be tried when the debugger spends a |
---|
| 29 | large amount of time when creating a path to a fair cycle. |
---|
| 30 | |
---|
| 31 | -d <dbg_level> |
---|
| 32 | Specify whether to demonstrate a proof of the language non-emptiness |
---|
| 33 | |
---|
| 34 | dbg_level must be one of the following: |
---|
| 35 | |
---|
| 36 | 0 : No debugging performed. This is the default. |
---|
| 37 | |
---|
| 38 | 1 : Generate a path to a fair cycle. |
---|
| 39 | |
---|
| 40 | -f <dbg_file> |
---|
| 41 | Write the debugger output to dbg_file. |
---|
| 42 | |
---|
| 43 | -h |
---|
| 44 | Print the command usage. |
---|
| 45 | |
---|
| 46 | -m |
---|
| 47 | Pipe debugger output through the UNIX utility more. |
---|
| 48 | |
---|
| 49 | -i |
---|
| 50 | Print input values causing transitions between states during |
---|
| 51 | debugging. Both primary and pseudo inputs are printed. |
---|
| 52 | |
---|
| 53 | -s |
---|
| 54 | Print debug output in the format accepted by the [3]simulate command. |
---|
| 55 | |
---|
| 56 | -t <timeOutPeriod> |
---|
| 57 | Specify the time out period (in seconds) after which the command |
---|
| 58 | aborts. By default this option is set to infinity. |
---|
| 59 | |
---|
| 60 | -v <verbosity_level> |
---|
| 61 | Specify verbosity level. This sets the amount of feedback on CPU |
---|
| 62 | usage and code status. |
---|
| 63 | |
---|
| 64 | verbosity_level must be one of the following: |
---|
| 65 | |
---|
| 66 | 0 : No feedback provided. This is the default. |
---|
| 67 | |
---|
| 68 | 1 : Feedback on code location. |
---|
| 69 | |
---|
| 70 | 2 : Feedback on code location and CPU usage. |
---|
| 71 | |
---|
| 72 | -A <le_method> |
---|
| 73 | Specify whether the compositional SCC analysis algorithm, Divide and |
---|
| 74 | Compose (DnC), is enabled for language emptiness checking. The DnC |
---|
| 75 | algorithm first enumerates fair SCCs in an over-approximated abstract |
---|
| 76 | model, and then successively refines them in the more concrete |
---|
| 77 | models. Since non-fair SCCs can be ignored in the more concrete |
---|
| 78 | models, a potentially large part of the state space are pruned away |
---|
| 79 | early on when the computations are cheap. |
---|
| 80 | |
---|
| 81 | le_method must be one of the following: |
---|
| 82 | |
---|
| 83 | 0 : no use of Divide and Compose (Default). |
---|
| 84 | |
---|
| 85 | 1 : use Divide and Compose. |
---|
| 86 | |
---|
| 87 | -D <dc_level> |
---|
| 88 | Specify extent to which don't cares are used to simplify MDDs. Don't |
---|
| 89 | cares are minterms on which the value taken by functions does not |
---|
| 90 | affect the computation; potentially, these minterms can be used to |
---|
| 91 | simplify MDDs and reduce time taken to perform MDD computations. |
---|
| 92 | |
---|
| 93 | dc_level must be one of the following: |
---|
| 94 | |
---|
| 95 | 0 : No don't cares are used. |
---|
| 96 | |
---|
| 97 | 1 : Use unreachable states as don't cares. This is the default. |
---|
| 98 | |
---|
| 99 | -S <schedule> |
---|
| 100 | Specify schedule for GSH algorithm, which generalizes the Emerson-Lei |
---|
| 101 | algorithm and is used to compute greatest fixpoints. The choice of |
---|
| 102 | schedule affects the sequence in which EX and EU operators are |
---|
| 103 | applied. It makes a difference only when fairness constraints are |
---|
| 104 | specified. |
---|
| 105 | <schedule> must be one of the following: |
---|
| 106 | |
---|
| 107 | EL : EU and EX operators strictly alternate. This is the default. |
---|
| 108 | |
---|
| 109 | EL1 : EX is applied once for every application of all EUs. |
---|
| 110 | |
---|
| 111 | EL2 : EX is applied repeatedly after each application of all EUs. |
---|
| 112 | |
---|
| 113 | budget : a hybrid of EL and EL2. |
---|
| 114 | |
---|
| 115 | random : enabled operators are applied in (pseudo-)random order. |
---|
| 116 | |
---|
| 117 | off : GSH is disabled, and the old algorithm is used instead. The old |
---|
| 118 | algorithm uses the EL , but the termination checks are less |
---|
| 119 | sophisticated than in GSH. |
---|
| 120 | |
---|
| 121 | -F |
---|
| 122 | Use forward analysis in the computation of the greatest fixpoint. |
---|
| 123 | This option is incompatible with -d 1 or higher and can only be used |
---|
| 124 | with -D 1. |
---|
| 125 | |
---|
| 126 | -L <lockstep_mode> |
---|
| 127 | Use the lockstep algorithm, which is based on fair SCC enumeration. |
---|
| 128 | <lockstep_mode> must be one of the following: |
---|
| 129 | |
---|
| 130 | off : Lockstep is disabled. This is the default. Language emptiness |
---|
| 131 | is checked by computing a hull of the fair SCCs. |
---|
| 132 | |
---|
| 133 | on : Lockstep is enabled. |
---|
| 134 | |
---|
| 135 | all : Lockstep is enabled; all fair SCCs are enumerated instead of |
---|
| 136 | terminating as soon as one is found. This can be used to study the |
---|
| 137 | SCCs of a graph, but it is slower than the default option. |
---|
| 138 | |
---|
| 139 | n : (n is a positive integer). Lockstep is enabled and up to n fair |
---|
| 140 | SCCs are enumerated. This is less expensive than all , but still less |
---|
| 141 | efficient than on , even when n = 1 . |
---|
| 142 | _________________________________________________________________ |
---|
| 143 | |
---|
| 144 | Last updated on 20100410 00h02 |
---|
| 145 | |
---|
| 146 | References |
---|
| 147 | |
---|
| 148 | 1. file://localhost/projects/development/hsv/vis/common/doc/html/init_verifyCmd.html |
---|
| 149 | 2. file://localhost/projects/development/hsv/vis/common/doc/html/read_fairnessCmd.html |
---|
| 150 | 3. file://localhost/projects/development/hsv/vis/common/doc/html/simulateCmd.html |
---|