bdd_sat_bounded_model_check - performs an LTL bounded model checking on a flattened network

Performs an LTL bounded model checking on a flattened network. This command looks for a counterexample of length ≥ minimum_length and ≤ maximum_length. It increments the length by step_value. Before calling this command, the user should have initialized the design by calling the command flatten_hierarchy, and then calling the command build_partition_maigs.

The value of maximum length must be >= minimum length.

Command options:

-h

Print the command usage.

-m <minimum_length>

Minimum length of counterexample to be checked (default is 0).

-k <maximum_length>

Maximum length of counterexample to be checked (default is 1).

-s <step_value>

Incrementing value of counterexample length (default is 1).

-r <inductive_Step>

Use inductive proof at each step_value to check if the property passes (default is 0). 0 means don't use the inductive proof. BMC will check using the indcution if the property passes if the current length of the counterexample is a multiple of inductive_Step.

-F <fairness_file>

Read fairness constraints from <fairness_file>. Each formula in the file is a condition that must hold infinitely often on a fair path.

-o <cnf_file> Save the CNF formula in <cnf_file>

-t <timeOutPeriod>

Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.

-v <verbosity_level>

Specify verbosity level. This sets the amount of feedback on CPU usage and code status.
verbosity_level must be one of the following:

0: No feedback provided. This is the default.

1: Feedback on code location.

2: Feedback on code location and CPU usage.

-d <dbg_level>

Specify the amount of debugging performed when the BMC models check the LTL formula.

dbg_level must be one of the following:

0: No debugging performed. dbg_level=0 is the default.

1: Debugging with minimal output: generate counter-example if the LTL formula fails and the counterexample length.

-h

Print the command usage.

-i

Print input values causing transitions between states during debugging.

-o <cnf_file>;

File containing CNF of the counterexample if exist. If specifies, the user can exam this file looking for information about the generated path. This file will be the input to the SAT solver. The contents of this file is in dimacs format.

<ltl_file>

File containing LTL formulas to be model checked.