1 | |
---|
2 | bdd_sat_bounded_model_check - performs an LTL bounded model checking on a |
---|
3 | flattened network |
---|
4 | _________________________________________________________________ |
---|
5 | |
---|
6 | bdd_sat_bounded_model_check [-h] [-v <verbosity_level>] [-d <dbg_level>] |
---|
7 | [-i] -m <minimum_length> -k <maximum_length> -s <step_value> -o <cnf_file> |
---|
8 | <ltl_file> |
---|
9 | |
---|
10 | Performs an LTL bounded model checking on a flattened network. This command |
---|
11 | looks for a counterexample of length ⥠minimum_length and †maximum_length. |
---|
12 | It increments the length by step_value. Before calling this command, the |
---|
13 | user should have initialized the design by calling the command |
---|
14 | [1]flatten_hierarchy, and then calling the command [2]build_partition_maigs. |
---|
15 | |
---|
16 | The value of maximum length must be >= minimum length. |
---|
17 | |
---|
18 | Command options: |
---|
19 | |
---|
20 | -h |
---|
21 | Print the command usage. |
---|
22 | |
---|
23 | -m <minimum_length> |
---|
24 | Minimum length of counterexample to be checked (default is 0). |
---|
25 | |
---|
26 | -k <maximum_length> |
---|
27 | Maximum length of counterexample to be checked (default is 1). |
---|
28 | |
---|
29 | -s <step_value> |
---|
30 | Incrementing value of counterexample length (default is 1). |
---|
31 | |
---|
32 | -r <inductive_Step> |
---|
33 | Use inductive proof at each step_value to check if the property |
---|
34 | passes (default is 0). 0 means don't use the inductive proof. BMC |
---|
35 | will check using the indcution if the property passes if the current |
---|
36 | length of the counterexample is a multiple of inductive_Step. |
---|
37 | |
---|
38 | -F <fairness_file> |
---|
39 | Read fairness constraints from <fairness_file>. Each formula in the |
---|
40 | file is a condition that must hold infinitely often on a fair path. |
---|
41 | |
---|
42 | -o <cnf_file> Save the CNF formula in <cnf_file> |
---|
43 | -t <timeOutPeriod> |
---|
44 | Specify the time out period (in seconds) after which the command |
---|
45 | aborts. By default this option is set to infinity. |
---|
46 | |
---|
47 | -v <verbosity_level> |
---|
48 | Specify verbosity level. This sets the amount of feedback on CPU |
---|
49 | usage and code status. |
---|
50 | verbosity_level must be one of the following: |
---|
51 | |
---|
52 | 0: No feedback provided. This is the default. |
---|
53 | |
---|
54 | 1: Feedback on code location. |
---|
55 | |
---|
56 | 2: Feedback on code location and CPU usage. |
---|
57 | |
---|
58 | -d <dbg_level> |
---|
59 | Specify the amount of debugging performed when the BMC models check |
---|
60 | the LTL formula. |
---|
61 | |
---|
62 | dbg_level must be one of the following: |
---|
63 | |
---|
64 | 0: No debugging performed. dbg_level=0 is the default. |
---|
65 | |
---|
66 | 1: Debugging with minimal output: generate counter-example if the LTL |
---|
67 | formula fails and the counterexample length. |
---|
68 | |
---|
69 | -h |
---|
70 | Print the command usage. |
---|
71 | |
---|
72 | -i |
---|
73 | Print input values causing transitions between states during |
---|
74 | debugging. |
---|
75 | |
---|
76 | -o <cnf_file>; |
---|
77 | File containing CNF of the counterexample if exist. If specifies, the |
---|
78 | user can exam this file looking for information about the generated |
---|
79 | path. This file will be the input to the SAT solver. The contents of |
---|
80 | this file is in dimacs format. |
---|
81 | |
---|
82 | <ltl_file> |
---|
83 | File containing LTL formulas to be model checked. |
---|
84 | _________________________________________________________________ |
---|
85 | |
---|
86 | Last updated on 20100410 00h02 |
---|
87 | |
---|
88 | References |
---|
89 | |
---|
90 | 1. file://localhost/projects/development/hsv/vis/common/doc/html/flatten_hierarchyCmd.html |
---|
91 | 2. file://localhost/projects/development/hsv/vis/common/doc/html/build_partition_maigsCmd.html |
---|