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

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

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