RELEASE NOTES FOR VIS 2.3

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

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

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

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.

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.

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

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

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.

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

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

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.

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.

• Glu and vis can be built using g++ as compiler by configuring as follows:

     ./configure --enable-gcc=g++
     

• The code in glu has gone through another round of rejuvenation. This process allows vis to be built with recent versions of gcc (3.3 and later) without producing any type-punning warning.
• Two bugs have been fixed in early termination detection in CTL model checking.
• A bug has been fixed in the treatment of multi-valued inputs.
• Vis no longer crashes when compute_reach is invoked with the -i option.
• Timeout values for model_check, check_invariant, and lang_empty are now in CPU time instead of elapsed time. This is beneficial when running regression tests in the presence of other processes.
• The ctime command is no longer supported.