RELEASE NOTES FOR VIS 2.4


Release 2.4 of VIS improves VIS 2.3 in the following areas:
  1. Reads AIGER directly with command read_aiger. This command uses the "official" AIGER 1.9 library for parsing. Properties should still be specified in the usual way.
  2. New option -o to model_check allows one to select just one property from the property file.
  3. Command regression_test supports AIGER format.
  4. The commands model_check, ltl_model_check, lang_empty, and check_invariant use the new feature available in CUDD 2.5.0 to abandon variable reordering when a timeout is set and the deadline is approaching.
  5. Improved the mechanism for variable interpolation in the shell. It is now possible to write things like $basename.$ext.
  6. A new verbosity level (2) for dynamic_var_ordering allows the user to monitor the evolution of the variable order.
  7. Improved next-state variable matching for equivalence checking.
  8. A new option -d for init_verify combines the convenience of init_verify with the ability to enable reordering.
  9. Bug fixes.

RELEASE NOTES FOR VIS 2.3


Release 2.3 of VIS improves VIS 2.0 in the following areas:
  1. Builds with bison 2.4.1 and gcc 4.4.1
  2. Supports cusp-1.1 as external SAT solver for bounded model checking instead of zchaff
  3. Bug fixes
Release 2.2 of VIS improves VIS 2.0 in the following areas:
  1. Support for 32/64-bit compilation
  2. Ability to use 4 GB of RAM in 32-bit mode
  3. Builds with gcc 4.3 and bison 2.3
    Weak until support
  1. Improved efficiency (especially in flatten_hierarchy)
  2. Improved debugging support (new command write_network_blif_mv)
  3. Improved node matching for combinational equivalence (comb_verify)
  4. Bug fixes
    CUDD 2.4.2
    vis-verilog-models-1.2
Release 2.1 of VIS improves VIS 2.0 in the following areas:
  1. Revamped Bounded Model Checker with efficient termination criteria
  2. Grab and Puresat algorithms for invariant checking based on abstraction refinement
  3. DnC algorithm for language emptiness check based on abstraction refinement
  4. CirCUs SAT solver
  5. Fate and Free Will algorithm for the analysis of counterexamples
  6. Vacuity Detection for CTL
  7. Coverage Estimation for CTL
  8. Far Side Algorithm for Image Computation
  9. CUDD 2.4.1
  10. Miscellaneous
Bounded Model Checking

BMC in VIS 2.1 is much faster than it was in VIS 2.0. The construction of the circuit data structure, the encoding of the property, the use of a faster SAT solver all have contributed to this improvement.

BMC in VIS 2.1 can prove properties rather than just falsifying them. The following sequence of commands is used to perform bounded model checking with termination check:

   read_blif_mv model.mv
   flatten_hierarchy
   build_partition_maigs
   bounded_model_check -k 10 -r 2 model.ltl

The termination check will be performed every other step. For details on the stopping criteria, see

 M. Awedh and F. Somenzi, "Proving More Properties with Bounded Model
 Checking," CAV 2004, pp. 96-108, LNCS 3114.

Other new options to the bounded_model_check command allow one to control the formula encoding, the solver to be applied (CirCUs or zChaff) and, for the former, the incremental solving algorithm.

A new command ltl2snf allows one to translate an LTL formula to separation normal form.

top

Abstraction Refinement for Invariants

The check_invariant command allows the user the choice of one of two abstraction refinement algorithms for invariants. The Grab algorithm uses BDD-based model checking on the abstract model and SAT for counterexample concretization check. Its refinement strategy is game-theoretic. It is run as follows:

   read_blif_mv model.mv
   flatten_hierarchy
   build_partition_maigs
   check_invariant -A3 model.inv

For details of the algorithm, see

 C. Wang, B. Li, H. Jin, G. D. Hachtel, and F. Somenzi, "Improving
 Ariadne's Bundle by Following Multiple Threads in Abstraction
 Refinement," ICCAD 2003, pp. 408-415.

The puresat algorithm uses SAT as the only decision procedure for both abstract and concrete model. It analyzes the proofs of unsatisfiability to produce refinements. It is invoked as follows:

   read_blif_mv model.mv
   flatten_hierarchy
   build_partition_maigs
   check_invariant -A4 model.inv

The algorithm is described in

 B. Li, C. Wang, and F. Somenzi, "Abstraction Refinement in Symbolic
 Model Checking Using Satisfiability as the Only Decision Procedure,"
 STTT, vol.7, n. 2, pp. 143-155.

top

Abstraction Refinement for Language Emptiness

The lang_empty command has a new option that runs the "Divide and Compose" (DnC) algorithm described in

 C. Wang, R. Bloem, G. D. Hachtel, K. Ravi, and F. Somenzi, "Divide and
 Compose: SCC Refinement for Language Emptiness", CONCUR 2001,
 pp. 456-471, LNCS 2154.

The algorithm, which is based on refinement of the strongly connected components of the model, is invoked as follows:

   read_blif_mv model.mv
   init_verify
   lang_empty -A 1

top

CirCUs SAT solver

VIS 2.1 includes the SAT solver CirCUs, a short description of which can be found in

 H. Jin, M. Awedh, and F. Somenzi, "CirCUs: A Satisfiability Solver
 Geared Towards Bounded Model Checking," CAV 2004, pp. 519-522, LNCS
 3114.

CirCUs is an incremental SAT solver that accepts input in circuit, CNF, and BDD form. It is the default solver for bounded model checking and abstraction refinement algorithms. It can also be invoked from the VIS prompt as a stand-alone CNF SAT solver on a set of clauses described in DIMACS format:

  cnf_sat input.cnf

top

Fate and Free Will Algorithm

The counterexamples produced by model_check and check_invariant can be optionally generated with the Fate and Free Will algorithm of

 H. Jin, K. Ravi, and F. Somenzi, "Fate and Free Will in Error Traces,"
 STTT, vol. 6, n. 2, pp. 102-116.

The algorithm assumes a partition of the inputs into variables controlled by the environment and variables controlled by the system, and divides a counterexample into fated and free segments. In a fated segment, the values of the variables controlled by the environment suffice to impose progress toward violation of the property. In a free segment, the other variables are also required.

To run the Fate and Free Will algorithm, one prepares a file with the inputs that the system controls. For a failing invariant, the invocation is like this:

   read_blif_mv model.mv
   init_verify
   check_invariant -d1 -i -w system_inputs

The last command is replaced by

   model_check -d2 -i -w system_inputs

for a CTL property. The -W option can be used to assign all inputs to the system, while the -G option invokes a variant of the algorithm.

top

Vacuity Detection for CTL

VIS 2.1 implements two algorithms for the detection of vacuity in CTL model checking. A formula passes vacuously if it can be strengthened by replacement of one of its subformulae with "bottom" and still pass. Likewise, a formula fails vacuously if it can be weakened by replacement of one of its subformulae with "top" and still fail.

The algorithm of Beer et al. (CAV 97) is invoked with the -B option as follows:

   read_blif_mv model.mv
   init_verify
   model_check -B model.ctl

his algorithm applies to a subset of ACTL and considers only passing properties. If an error trace is requested with -d, in case of vacuous pass, an interesting witness is produced.

The second algorithm for vacuity detection is an extension of the one describe in

 M. Purandare and F. Somenzi, "Vacuum Cleaning CTL Formulae," CAV 2002,
 pp. 485-499, LNCS 2404.

This algorithm applies a thorough vacuity detection to all of CTL and to both passing and failing properties. With -d, it produces interesting witnesses for passing properties and interesting counterexamples for failing ones.

The current implementation is limited in its treatment of the operators <-> (equivalence) and ^ (exclusive or).

top

Coverage Estimation for CTL

VIS 2.1 provides two algorithms for coverage estimation in CTL model checking. Both are invoked with options passed to the model_check command.

The first algorithm is the one of Hoskote et al. (DAC 1999). It applies to a subset of ACTL. The option is -C. The second algorithm is an improved version of the same described in

 N. Jayakumar, M. Purandare, and F. Somenzi, "Dos and Don'ts of CTL
 State Coverage Estimation," DAC 2003, pp. 292-295.

To invoke the improved coverage estimation algorithm one writes:

   read_blif_mv model.mv
   init_verify
   model_check -I model.ctl

top

Far Side Algorithm for Image Computation

By setting image_farside_method to 1, a user of VIS 2.1 can invoke the Far Side approach to image computation which applies a compositional method based on don't cares to speed up reachability analysis. The algorithm is described in

 C. Wang, G. D. Hachtel, and F. Somenzi, "The Compositional Far Side of
 Image Computation," ICCAD 2003, pp. 334-340.

See the documentation of the "set" command for the details.

top

CUDD 2.4.1

VIS-2.0 includes CUDD 2.4.1. Compared to the version that was included in VIS-2.0, the new version has faster grabage collection, provides improved support for C++ compilation, contains a number of bug fixes and several new functions, including functions for the manipulation of prime implicants of a function.

top

Miscellaneous

top