iterative_model_check - Perform CTL model checking on an abstracted system with automatic refinement algorithm.

Command options:

-h

Print the command usage.

-x

Perform the verification exactly. No approximation is done.

-t <secs>

Time in seconds allowed for verification. The default is no limit.

-v <number>

Specify verbosity level. Use 0 for no feedback (default), 1 for more, and 2 for maximum feedback.

-D <number>

Specify extent to which don't cares are used to simplify the MDDs.

• 0: No don't cares used. This is the default.
• 1: Use reachability information to compute the don't-care set.
• 2: Use reachability information, and minimize the transition relation with respect to the `frontier set' (aggresive minimization).
• 3: Use approximate reachability information.

-r <number>

Specify refinement method.

• 0: Static scheduling by name sorting. Fast, easy, but less accurate.
• 1: Static scheduling by latch affinity. Slow, but more accurate. This is the default.

-i <number>

The number of state variables to be added for exact computation at each iteration. The default is 4.

-l <number>

Type of lower-bound approximation method.

• 0: Take a subset of each transition sub-relation by BDD subsetting.
• 1: Take a subset by universal quantification. This is the default.

-p <number>

Type of partition method. If 'build_partition_mdds' is already invoked, this option is ignored. Notice that some next state functions might not be available after iterative_model_checking command is performed because of this option.

• 0: Build all next state functions. Same as 'build_partition_mdds'. This is the default.
• 1: Build the next state functions related to the formulas. Build all next state functions that are necessary to prove all formulas.
• 2: Build the next state functions incrementally. None of next state functions are removed.

-g <number>

Type of operational graph.

• 0: Negative Operational Graph. Good to prove a formula true.
• 1: Positive Operational Graph. Good to prove a formula false.
• 2: Mixed Operational Graph. Good to prove any formula, but it may be slower. This is the default.

<ctlfile>

File containing the CTL formulas to be verified.

Related "set" options:

ctl_change_bracket <yes/no>

Vl2mv automatically converts "[]" to "<>" in node names, therefore CTL parser does the same thing. However, in some cases a user does not want to change node names in CTL parsing. Then, use this set option by giving "no". Default is "yes".

See also commands : model_check, incremental_ctl_verification

1. Jae-Young Jang, In-Ho Moon, and Gary D. Hachtel. Iterative Abstraction-based CTL Model Checking. Design, Automation and Test in Europe (DATE), 2000

2. Jae-Young Jang. Iterative Abstraction-based CTL Model Checking. Ph. D. Thesis. University of Colorado, 1999.