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.
topAbstraction 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.
topAbstraction 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
topCirCUs 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:
topFate 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.
topVacuity 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).
topCoverage 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
topFar 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.
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.