
  ltl_model_check - perform LTL model checking on a flattened network
     _________________________________________________________________

   ltl_model_check  [-a  <ltl2aut_algorithm>]  [-b]  [-d <dbg_level>] [-f
   <dbg_file>] [-h] [-i] [-m] [-s] [-t <time_out_period>][-v <verbosity_level>]
   [-A <le_method>] [-D <dc_level>] [-L <lockstep_mode>] [-S <schedule>] [-F]
   [-X] [-Y] [-M] <ltl_file>

   Performs LTL model checking on a flattened network. Before calling this
   command, the user should have initialized the design by calling the command
   [1]init_verify. Regardless of the options, no 'false positives' or 'false
   negatives' will occur: the result is correct for the given circuit.

   Properties to be verified should be provided as LTL formulae in the file
   ltl_file. Note that the support of any wire referred to in a formula should
   consist only of latches. For the precise syntax of LTL formulas, see the
   [2]VIS CTL and LTL syntax manual.

   A  formula passes iff it is true for all initial states of the system.
   Therefore, in the presence of multiple initial states, if a formula fails,
   the negation of the formula may also fail.

   If  a  formula does not pass, a (potentially partial) proof of failure
   (referred to as a debug trace) is demonstrated. Fair paths are represented
   by a finite sequence of states (the stem) leading to a fair cycle, i.e. a
   cycle  on which there is a state from each fairness condition. Whether
   demostrate the proof or not can be specified (see option -d).

   Command options:

   -a <ltl2aut_algorithm>
          Specify  the  algorithm used in LTL formula -> Buechi automaton
          translation.

          ltl2aut_algorithm must be one of the following:

          0: GPVW.

          1: GPVW+.

          2: LTL2AUT.

          3: WRING (default).

   -b
          Use boolean minimization during the LTL to Automaton translation.

   -d <dbg_level>
          Specify whether to demonstrate a counter-example when the system
          fails a formula being checked.

          dbg_level must be one of the following:

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

          1: Generate a counter-example (a path to a fair cycle).

   -f <dbg_file>
          Write the debugger output to dbg_file.

   -h
          Print the command usage.

   -i
          Print  input  values  causing transitions between states during
          debugging. Both primary and pseudo inputs are printed.

   -m
          Pipe debugger output through the UNIX utility more.

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

   -s
          Print debug output in the format accepted by the [3]simulate command.

   -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.

   -A <le_method>
          Specify whether the compositional SCC analysis algorithm, Divide and
          Compose (DnC), is enabled for language emptiness checking. The DnC
          algorithm first enumerates fair SCCs in an over-approximated abstract
          model,  and then successively refines them in the more concrete
          models. Since non-fair SCCs can be ignored in the more concrete
          models, a potentially large part of the state space are pruned away
          early on when the computations are cheap.

          le_method must be one of the following:

          0 : no use of Divide and Compose (Default).

          1 : use Divide and Compose.

   -D <dc_level>
          Specify extent to which don't cares are used to simplify MDDs in
          model checking. Don't cares are minterms on which the value taken by
          functions  does  not affect the computation; potentially, these
          minterms can be used to simplify MDDs and reduce the time taken to
          perform model checking.
          dc_level must be one of the following:

          0 : No don't cares are used.

          1 : Use unreachable states as don't cares. This is the default.

          2 : Use unreachable states as don't cares and in the EU computation,
          use 'frontiers' for image computation.

          3  : First compute an overapproximation of the reachable states
          (ARDC), and use that as the cares set. Use `frontiers' for image
          computation. For help on controlling options for ARDC, look up help
          on the command: [4]print_ardc_options. Refer to Moon, Jang, Somenzi,
          Pixley, Yuan, "Approximate Reachability Don't Cares for {CTL} Model
          Checking",  ICCAD98,  and to two papers by Cho et al, IEEE TCAD
          December 1996: one is for State Space Decomposition and the other is
          for Approximate FSM Traversal.

   -S <schedule>
          Specify schedule for GSH algorithm, which generalizes the Emerson-Lei
          algorithm and is used to compute greatest fixpoints. The choice of
          schedule  affects the sequence in which EX and EU operators are
          applied. It makes a difference only when fairness constraints are
          specified.
          <schedule> must be one of the following:

          EL : EU and EX operators strictly alternate. This is the default.

          EL1 : EX is applied once for every application of all EUs.

          EL2 : EX is applied repeatedly after each application of all EUs.

          budget : a hybrid of EL and EL2

          random : enabled operators are applied in (pseudo-)random order.

          off : GSH is disabled, and the old algorithm is used instead. The old
          algorithm  uses  the  EL  , but the termination checks are less
          sophisticated than in GSH.

   -F
          Use forward analysis in the computation of the greatest fixpoint.
          This option is incompatible with -d 1 or higher and can only be used
          with -D 1.

   -L <lockstep_mode>
          Use the lockstep algorithm, which is based on fair SCC enumeration.
          <lockstep_mode> must be one of the following:

          off : Lockstep is disabled. This is the default. Language emptiness
          is checked by computing a hull of the fair SCCs.

          on : Lockstep is enabled.

          all : Lockstep is enabled; all fair SCCs are enumerated instead of
          terminating as soon as one is found. This can be used to study the
          SCCs of a graph, but it is slower than the default option.

          n : (n is a positive integer). Lockstep is enabled and up to n fair
          SCCs are enumerated. This is less expensive than all , but still less
          efficient than on , even when n = 1 .

   -X
          Disable strength reduction (use different decision procedures for
          strong, weak, and terminal automaton). Strength reduction is the
          default.  Refer  to  Bloem,  Ravi, Somenzi, "Efficient Decision
          Procedures for LTL Model Checking," CAV99.

   -Y
          Disable incremental construction of the partition for (MxA). Instead,
          build a new partition from the scratch. Incremental construction of
          the partition is the default.

   -Z
          Add arcs into the Buechi automaton by direct simulation relation, to
          heuristically reduce the length of shortest counter-example in model
          checking. Refer to Awedh and Somenze, "Proving More Properties with
          Bounded Model Checking," CAV04.

   -M
          Maximize (adding arcs to) Buechi automaton using Direct Simulation.

   <ltl_file>
          File containing LTL formulas to be model checked.

   Related "set" options:

   ltl_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,  approximate_model_check,
          incremental_ctl_verification
            __________________________________________________________

          Last updated on 20100410 00h02

References

   1. file://localhost/projects/development/hsv/vis/common/doc/html/init_verifyCmd.html
   2. file://localhost/projects/development/hsv/vis/common/doc/ctl/ctl/ctl.html
   3. file://localhost/projects/development/hsv/vis/common/doc/html/simulateCmd.html
   4. file://localhost/projects/development/hsv/vis/common/doc/html/print_ardc_optionsCmd.html
