VIS NEWS -*-indented-text-*- History of user-visible changes. Please sent bug reports to vis-users@colorado.edu. Please let us know what version of VIS you are running and what architecture you are running it on. ====================================================================== Version 2.1 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. The construction of the MDDs is not needed if termination check is needed for invariant properties only. 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. 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 By default, grab enables dynamic variable reordering for the abstract model. One can override this behavior by explicitly building partition MDDs. 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. 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 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 either circuit or CNF 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 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. This algorithm is only available when vis is linked with the cu BDD package. It 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. 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 This 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). 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 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. 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. Miscellaneous ------------- * 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. ====================================================================== Version 2.0 Release 2.0 of VIS improves VIS 1.4 in the following areas: 1. LTL model checking 2. SAT-based Bounded Model Checking (BMC) 3. Minimum Lifetime Permutation (MLP) algorithm for conjuction scheduling 4. Generalized SCC Hull (GSH) algorithm for greatest fixpoint computation 5. Lockstep algorithm for language emptiness 6. Built-in regression test facility 7. CUDD 2.3.2 8. Miscellaneous LTL model checking ------------------ VIS-2.0 has a new command ltl_model_check that model checks LTL formulae. The syntax for LTL is quite similar to that used for CTL. Another new command, ltl_to_aut, translates LTL formulae into Buechi automata. SAT-Based Bounded Model Checking -------------------------------- VIS-2.0 has a new command bounded_model_check for bounded LTL model checking. The SAT solver zchaff (http://www.ee.princeton.edu/~chaff/) must be in the executable path for this command to work. The following sequence of commands is used to perform bounded model checking: read_blif_mv model.mv flatten_hierarchy build_partition_maigs bounded_model_check -k 10 model.ltl where "-k 10" specifies the bound on the length of the counterexample. Minimum Lifetime Permutation (MLP) Algorithm for Conjuction Scheduling ---------------------------------------------------------------------- The MLP algorithm can considerably speed up image computations. It is selected by typing set image_method mlp For details on the algorithm, see I-H. Moon, G. D. Hachtel, and F. Somenzi, "Border-Block Triangular Form and Conjunction Schedule in Image Computation," FMCAD 2000, pp. 73-90, LNCS 1954. Generalized SCC Hull (GSH) Algorithm for Greatest Fixpoint Computation ---------------------------------------------------------------------- The commands model_check, ltl_model_check, and lang_empty use a new algorithm for greatest fixpoint computations. This algorithm has different "schedules" that can be controlled with the -S option. For details on the algorithm, see K. Ravi, R. Bloem, and F. Somenzi, "A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles," FMCAD 2000, pp. 143-160, LNCS 1954. F. Somenzi, K. Ravi, and R. Bloem, "Analysis of Symbolic {SCC} Hull Algorithms," FMCAD 2002, To appear. Lockstep Algorithm for Language Emptiness ----------------------------------------- In VIS-2.0, the commands ltl_model_check and lang_empty can use the lockstep algorithm to perform the language emptiness check. The use of the lockstep algorithm as an alternative to the GSH algorithm is controlled by the -L option. For details of Lockstep, see R. Bloem, H. N. Gabow, and F. Somenzi, "An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps," FMCAD 2000, pp. 37-54, LNCS 1954. Built-in Regression Test Facility --------------------------------- VIS-2.0 has a new command regression_test which allows users to compare runs of two different versions of vis, or runs with different options. CUDD 2.3.2 ---------- VIS-2.0 includes CUDD 2.3.2. Compared to the version that was included in VIS-1.4, the new version contains a number of bug fixes and several new functions. In particular, there is a new function that will compute the AND of two BDDs only if the result does not require the creation of too many nodes. This function is used by VIS-2.0 to make clustering of the transition relation more robust. Miscellaneous ------------- * Improved counterexample generation in model_check with -d3 and -d4. * Changes in verbosity level (-v option) of model_check. The new verbosity levels are: -v0: unchanged (minimum verbosity) -v1: essential statistics (new) -v2: equivalent to the old -v1 -v3: equivalent to the old -v2 * Fixed bug and extended early termination detection in CTL model checking. * Fixed bug in guided search for CTL model checking which affected counterexample generation with global hints. * Vis no longer crashes when a directory name is specified in a command line instead of a regular file name. * Fixed several bugs in approximate_model_check, incremental_ctl_verification, and iterative_model_check. * The code in glu has been substantially rejuvenated. ====================================================================== Version 1.4 Release 1.4 of VIS improves VIS 1.3 in the following areas: 1. Hybrid Image Computation 2. Guided Search for Reachability Analysis and Invariant Checking 3. Guided Search for CTL Model Checking 4. Least Fix-point Machine-By-Machine Approximate FSM Traversal (LMBM) 5. Iterative Abstraction-based Model Checking (IMC) 6. Lazy Sifting 7. SPFD-based Placement and Logic Optimization 8. Truesim 9. Arithmetic Functions with Extended Double Precision (EPD) 10. CUDD 2.3.1 11. Miscellaneous 1. Hybrid Image Computation --------------------------- Image computation is the key step in fix-point computation. Traditionally two techniques have been used: The transition relation method is based on conjunction of a partitioned transition relation, whereas the transition function method is based on splitting on an input or output variable recursively. The hybrid method chooses either splitting or conjunction at each recursion dynamically using the dependence matrix. This hybrid approach combines, in a unified framework, conjunction, input and output splitting, and a host of auxiliary techniques that can significantly speed up the computation. See: I.-H. Moon, J.H. Kukula, K. Ravi, F. Somenzi, "To Split or to Conjoin: The Question in Image Computation", Proceedings of the Design Automation Conference (DAC), pages 73-90, 2000. Also, the transition function method is implemented as a part of the hybrid computation. The transition function method itself can be used as an independent image method. However, we do not recommend to use this method in general cases, even though it may work well for approximate reachability analysis. The implementation of the transition function method is basically for experimental purposes. ** Usage: set image_method hybrid set image_method tfm Also refer to: print_hybrid_options and print_tfm_options 2. Guided Search for Reachability Analysis ------------------------------------------ VIS-1.4 introduces the use of hints to guide the exploration of the state space. This may result in orders-of-magnitude reductions in time and space requirements. Good hints can often be found with the help of simple heuristics by someone who understands the circuit well enough to devise simulation stimuli or verification properties for it. Hints are applied by constraining the transition relation of the system to be verified. They specify possible values for (subsets of) the primary inputs and state variables. The constrained traversal of the state space may proceed much faster than the standard breadth-first search, because the traversal with hints is designed to produce smaller BDDs. Once all states reachable following the hints have been visited, the system is unconstrained and reachability analysis proceeds on the original system. Given enough resources, the algorithm will therefore search all reachable states, unless a state that violates the invariant is found. See: K. Ravi, F. Somenzi, "Hints to accelerate Symbolic Traversal", Correct Hardware Design and Verification Methods (CHARME), pages 250-264, 1999. ** Usage: compute_reach -g : guided symbolic state space traverse check_invariant -g : guided search for invariant checking The file HintsFileName contains a series of hints. A hint is a formula that does not contain any temporal operators, so hints_file has the same syntax as a file of invariants used for check_invariant. Also refer to: model_check -g 3. Guided Search for CTL Model Checking --------------------------------------- Guided Search for CTL is an extension of Guided Search for reachability. It works much along the same lines, and has the same benefits. There are a few differences. First, for greatest fixpoints (EG, AU, and AF), it uses overapproximations of the transition relation, instead of underapproximations. Second, there is a distinction between local and global hints. Local hints are the default. They can be used for any kind of CTL formula, and will apply all hints to a subformula before moving up in the parse tree. Global hints are only applicable to ACTL and ECTL formulae, and evaluate the entire formula once for every hint. See: R. Bloem, K. Ravi, and F. Somenzi, "Symbolic Guided Search for CTL Model Checking", Proceedings of the Design Automation Conference (DAC), pages 29-34, 2000. ** usage: model_check -g HintsFileName : perform model check guided by the hints specified in HintsFileName Also refer to: compute_reach -g check_invariant -g 4. Least Fix-point Machine-By-Machine Approximate FSM Traversal (LMBM) ---------------------------------------------------------------------- The knowledge of the reachable states of a sequential circuit can dramatically speed up optimization and model checking. Since exact reachability may be intractable, approximate techniques are often preferable. Least Fix-point MBM (LMBM) method is such a technique. It is as efficient as MBM, but provably more accurate. LMBM can compute RFBF-quality approximations for all the large ISCAS-89 benchmark circuit in a total of less than 9000 seconds. For more information, see: I.-H. Moon, J. Kukula, T. Shiple, F. Somenzi, "Least Fixpoint Approximation for Reachability Analysis," International Conference on Computer-Aided Design (ICCAD), pages 41-44, 1999. ** Usage: set ardc_traversal_method 4: LMBM(least fix-point MBM, default) is selected for ARDC set ardc_traversal_method 5: TLMBM(combination of LMBM and TFBF) is selected for ARDC model_check -D 3 : model checking with ARDCs compute_reach -A 2 : compute over-approximate reachable states compute_reach -D : compute exact reachable states with the help of ARDCs check_invariant -D : check invariants with the help of ARDCs synthesize_network -r 3 : synthesize sequential network with ARDCs Also refer to: print_ardc_options 5. Iterative Abstraction-Based Model Checking (IMC) --------------------------------------------------- VIS-1.4 introduces an automatic abstraction/refinement algorithm for symbolic CTL model checking. This algorithm supports full CTL language without fairness constraints. The algorithm begins with initial upper- and/or lower-bound approximations that include some exact sub-transition relations of a determined set of latches for a given CTL formula. As long as a conclusive verification decision can't be reached due to potentially false positives and negatives, the system is refined. Two refinement methods are implemented: Latch Name Sorting and Latch Affinity Scheduling. For more information, See: J.-Y. Jang, I.-H. Moon, G.D. Hachtel, "Iterative Abstraction-based CTL Model Checking," Design Automation and Test in Europe (DATE), pages 502-507, 2000. IMC supersedes the AMC package, which may disappear in future releases. ** Usage: iterative_model_check -i 8 : iterative model checking with incremental refinement step set to 8 latches iterative_model_check -r 0 : iterative model checking using Latch Name Sorting refinement scheduling iterative_model_check -g 1 : iterative model checking using Positive Operational Graph only Also refer to: model_check, approximate_model_check, incremental_ctl_verification 6. Lazy Sifting --------------- Lazy sifting is a new variable reordering option that is specifically designed for sequential verification with the transition relation method (i.e., IWLS95 in VIS). Lazy sifting groups together corresponding present state and next state variables only when it expects the grouping to be beneficial. See: H. Higuchi and F. Somenzi, "Lazy Group Sifting for Efficient Symbolic State Traversal of FSMs," Proceedings of the International Conference on Computer-Aided Design (ICCAD), pages 45-49, 1999. ** Usage: dynamic_var_ordering -e lazy_sift 7. SPFD-based placement and logic optimization ---------------------------------------------- This is an algorithm based on Sets of Pairs of Functions to be Distinguished (SPFDs) that combines logic and placement optimization of combinational circuits mapped to LUT-based Field-Programmable Gate Arrays to improve circuit area and speed. The flexibilities in the circuit are represented by SPFDs. The package contains two commands: spfd_pilo - perform SPFD-based placement-independent logic optimization; and spfd_pdlo - simultaneous placement and logic optimization. spfd_pilo performs SPFD-based wire and node removal/replacement and reprogramming of combinational circuits mapped to LUT-based FPGAs to reduce the number of wires and nodes in the circuit. Instead of computing the flexibilities for every node in the network at once, the algorithm computes the flexibilities for one `cluster' at a time. Working with clusters allows us to avoid the BDD explosion problem and hence handle large circuits. The SPFDs are computed for the cluster and the cluster nodes are reprogrammed based on the flexibility derived. Switching activity (computed via simulation of user specified bit vectors or randomly generated bit vectors) is used to drive the choice of alternate function to be implemented at the node, in such a way that the total switching activity in the circuit is minimized. In the absence of bit vectors, an arbitrary implementation for a node is chosen from the bounds represented by SPFDs. The command spfd_pdlo implements a technique that tightly links the logic and placement optimization steps. The algorithm is based on simulated annealing. Two types of moves (directed towards global reduction in the cost function of total wire length), are performed: (1) wire removal/replacement, and (2) swapping of a pair of blocks in the FPGA. Feedback from placement is valuable in making informed choice of a target wire during logic optimization moves. This command produces a placement file which is used by VPR for routing. spfd_pdlo can be used only if VIS is linked with VPR 4.22, an FPGA place and route tool from the University of Toronto (http://www.eecg.toronto.edu/~vaughn/vpr/vpr.html). VPack, a tool to convert circuits (mapped to FPGA blocks) in .BLIF format to the .net format (used by VPR), is also needed. Please contact Balakrishna Kumthekar (kumtheka@avanticorp.com) for details on integrating VPR with VIS. See: B. Kumthekar and F. Somenzi, "Power and Delay Reduction via Simultaneous Logic and Placement Optimization in FPGAs," Design Automation and Test in Europe (DATE), pages 202-207, 2000. ** usage: spfd_pilo -D : sets the cluster depth for SPFD computation. spfd_pilo -f : use simulation vectors from specified file. These vectors are used to compute switching activity of nodes in the circuit. spfd_pilo -S : selects one of several methods to choose the node to be optimized. spfd_pilo -m : selects the heuristic to use in optimizing a selected node. See 'help spfd_pilo' and 'help spfd_pdlo' for various options. 8. Truesim ---------- Simulates a network with a set of input vectors. Before calling this command, the user should create a partition (using the command build_partition_mdds). The simulation vectors can be provided by the user (using -f vectors_file), or generated randomly. When -d option is used, it performs event-driven true delay simulation. The fanout count of the nodes is used as an estimate for the node delay. Primary inputs are assumed to have arrival times of zero. 9. Arithmetic Functions with extended double precision (EPD) ------------------------------------------------------------ This is an arithmetic function package for extended double precision format floating-point numbers. It supports the IEEE-754 double (64-bit) precision floating-point number format: both the big_endian and the little_endian. The range is from 2.2631E-4932 to 1.1897E+4932. This package is used internally to provide fast and accurate counting of the states in large FSMs like those encountered in approximate reachability analysis. 10. New version of the CUDD package. ----------------------------------- VIS-1.4 includes CUDD 2.3.1. Compared to the version that was included in VIS-1.3, the new version contains a number of bug fixes and several new functions. * Miscellaneous --------------- ** One bug in the CAL package has been fixed. It affected platforms without the valloc function. ** Changes in supported platforms. Support for SunOS 5.8 (Solaris 2.8) on the Intel x86 platform has been added. Ultrix and SunOs 4 are no longer supported. ** Change of Verbosity level for debugging in model_check Debugging refers to the printing of an error-trace when a formula fails. The new debug levels are: -d0: no debugging (the old -d0) -d1: minimal debugging, with less verbosity than the old -d1 had -d2: minimal debugging with more verbosity (the old -d1) -d3: recursive debugging (the old -d2) -d4: interactive debugging (the old -d3) ** Early termination in Model Checking. In limited cases, VIS will terminate a model checking run before reaching a fixpoint. This may lead to a speedup. ** The set of fair states is not computed of there are no fairness constraints. This may lead to a speedup of the model_check command. ** Perl Script for pretty printing counter-examples. The Perl script visdbgpp, contributed by Toshi Isogai, can be run on counterexamples produced by vis to improve their readability. In particular, the script collects the bits of vectors and displays them on a single line. ** Counterexample generation. The states on an error trace now lie closer together, which means that, on average, fewer signal transitions will occur. ** Variable reordering. In flatten_hierarchy In VIS-1.4, variable reordering is invoked automatically during flatten_hierarchy. ** Changes of passing BDD cube arguments in VIS to CUDD. Some arguments in the CUDD functions are BDD cubes that are generated by the conjunctions of BDD variables on demand. VIS-1.4 pre-builds some BDD cubes that do not change, such as for present state variables, next state variables, and primary input variables. This speeds up significantly large runs, especially for approximate reachability analysis. ============================================================ Version 1.3 * Introduction Release 1.3 of VIS improves VIS 1.2 in the following areas: ** Approximate Reachability Don't Cares (ARDCs) ** High Density Reachability Analysis. ** On-the-Fly Invariant Checking. ** Seeding Reachability Analysis via Simulation ** Forward Model Checking ** Abstraction-refinement based Incremental CTL Verification ** Synthesis ** State Transition Graph Restructuring for Low Power ** Miscellaneous * Approximate Reachability Don't Cares (ARDCs) VIS-1.3 includes the use of ARDCs in model checking and reachability analysis. The power of using reachable states as a care set (RDCs) is well known; however, computing reachable states exactly is intractable in many large designs. ARDCs are an overapproximation of the reachable states, which are then used as the care set. Computing ARDCs is much cheaper than computing RDCs while their effectiveness in speeding up model checking is comparable to that of RDCs. Therefore, ARDCs are good for large designs, especially those in which exact reachability analysis is intractable. See: I.-H. Moon, J.-Y. Jang, G. D. Hachtel, F. Somenzi, "Approximate reachability don't cares for CTL model checking", ICCAD'98. ** Usage: model_check -D 3 : model checking with ARDCs compute_reach -A 2 : compute over-approximate reachable states compute_reach -D : compute exact reachable states with the help of ARDCs check_invariant -D : check invariants with the help of ARDCs synthesize_network -r 3 : synthesize sequential network with ARDCs Also refer to: print_ardc_options * High Density Reachability Analysis (HD) HD is an alternate approach to performing exact reachability analysis. Using BDD subsetting techniques, the HD method tries to keep the sizes of the BDDs small during the traversal. This is intended to keep the memory occupation under control as well as make the traversal more efficient by manipulating smaller BDDs. On large circuits, for which the default (breadth-first search) method does not complete, HD is likely to find many more reachable states. This is useful in invariant checking. For mid-size circuits, HD is sometimes faster in completing reachability analysis, but for smaller circuits, HD may result in too much overhead. It is recommended to use this option when the default method for reachability analysis fails (runs out of memory or takes very long). Refer to Ravi and Somenzi, "High-density reachability analysis", ICCAD'95. HD analysis only works with the CUDD package. ** Usage: compute_reach -A 1: reachability analysis with HD approach. Also refer to: print_hd_options * On-the-Fly Invariant Checking Checking invariants is done by performing reachability analysis and checking if all invariants hold in the reachable states. VIS-1.3 does invariant checking during reachability computation (on-the-fly verification). Invariants that fail are reported early, along with the counter examples if requested. Since reachability analysis can be expensive, one may use HD in invariant checking. For circuits on which the default reachability analysis runs out of resources, HD will typically explore more reachable states, and more invariants may prove false. However, the counter examples provided by using HD may not be of shortest length. HD invariant checking only works with the CUDD package. ** Usage: check_invariant -A 1 : check_invariant where HD is used for reachability analysis One may also start with an overapproximation of the reachable states. In this case, if all invariants hold on the overapproximation, verification is successfully completed. If not, the algorithm will compute the exact reachable states as before, and check the invariants that failed with the overapproximation. ** Usage: check_invariant -A 2 : check_invariant where over approximation is used for reachability analysis. * Seeding Reachability Analysis via Simulation A new option rch_simulate can be used to use simulation to augment the set of initial states for reachability analysis. The value of the variable is the number of random input vectors that are simulated. The states reached in this way are considered as initial states. Augmenting the set of initial states may sometimes lead to faster reachability analysis, or may sometimes lead to better underapproximations, when reachability analysis is not carried out to completion. The commands affected by this option are compute_reach and check_invariant. ** Usage: set rch_simulate n : simulate n vectors prior to reachability analysis * Forward Model Checking VIS-1.3 includes the capability of forward model checking based on H. Iwashita, T. Nakata, F. Hirose, "CTL model checking based on forward state traversal", ICCAD'96. Standard "backward" CTL model checking uses only preimage computations. Forward model checking tries to use image computations in place of preimage computations as much as possible, because they are typically faster. According to our experiments, forward model checking gives drastic performance improvement in many designs, but we have also seen many cases in which forward model checking does much worse. Performance depends on the design. ** Usage: model_check -F : model checking based on forward traversal * Incremental CTL Verification The command "incremental_ctl_verification" (aliased to "icv") performs verification of CTL formulas following the incremental paradigm described in A. Pardo, G. Hachtel, "Incremental CTL model checking using BDD subsetting", DAC'98. The algorithm starts with an initial simple approximation of the verification and then proceeds at refining the different evaluations until the formula can be proved conclusively. The approximation technique currently adopted makes use of BDD approximation techniques. As implemented in release 1.3, incremental_ctl_verification supports fairness constraints, but tends to be less efficient than model_check when they are specified. Incremental verification works only with the CUDD package. ** Usage: incremental_ctl_verification [options] ctl_file * Synthesis VIS 1.3 includes a new command "synthesize_network" (aliased to "synth") to transform both combinational and sequential circuits into multi-level boolean networks using symbolic factorization based on Zero-suppressed BDDs (ZDDs). In the case of sequential circuits, only the combinational part of the circuit is synthesized: state encoding is not altered. The emphasis of this algorithm is on the reduction of the number of literals in the factored form of the network. The final multi-level circuit can be obtained in either the BLIF format or the equation format. Designs described in BLIF or BLIF-MV format can be used as an input to this command. However, multiple valued variables are not supported. Hence, signals in the designs described in BLIF-MV need to be restricted to binary values. Synthesis can be used only when VIS is linked with the CUDD package. ** Usage: synthesize_network [options] * STG Restructuring for Low Power VIS-1.3 includes a new command "restruct_fsm". This command implements a State Transition Graph (STG) restructuring algorithm that exploits the existence of equivalent states to decrease power dissipation, not necessarily by collapsing the equivalence states, but by redirecting transitions in the graph. This algorithm is based on the monolithic transition relation. The complexity of the algorithm in general increases with an increase in the size of the state transition graph, which depends on the number of state variables and primary inputs. The algorithm can handle circuits described in both BLIF and BLIF-MV formats. However, multi-valued variables are not supported. Also, the final synthesized circuit (network implementation of the restructured STG) is available only in BLIF format. The sequential circuit should have a single initial state. For more details see, B. Kumthekar, I.-H. Moon, F. Somenzi, "A Symbolic Algorithm for Low-Power Sequential Synthesis", ISLPED 97. STG restructuring works only with the CUDD package. ** Usage: restruct_fsm [options] * Miscellaneous ** New versions of CUDD and CAL packages. VIS-1.3 includes CUDD 2.3.0 and CAL 2.0.1. Compared to the versions that were included in VIS-1.2, the new packages have better performance and improved statistics reporting. ** Changes in configure Configure now defaults to using 32-bit pointers on DEC Alpha machines. To use 64-bit pointers, invoke "configure" with "--enable-64." ** gmake check "gmake check" now consistently runs the local executable using the examples in the master source directory. Previously, there were different versions for local-area and central-area checks. ** Native Compiler. The configuration scripts now try to use the native C compiler (cc) by default. The use of gcc can be forced by running configure with the option --enable-gcc. On AIX and SunOS, however, only gcc is supported. As a result, the following configuration options have been removed --with-comp-mode=solaris --with-comp-mode=mips --with-comp-mode=alpha32 --with-comp-mode=alpha64 Configure now defaults to using 32-bit pointers on DEC Alpha machines. To use 64-bit pointers, invoke "configure" with "--enable-64." ** Changes in supported platforms. VIS-1.3 has been tested under IRIX 5.3 with both cc and gcc. VIS-1.3 has been tested under HP-UX with cc. (Previously only gcc was supported.) VIS-1.3 linked with the CAL BDD package currently does not work under CYGWIN32. When the problems are fixed, we shall issue a patch. ** Uniformity across platforms. VIS-1.3 provides enhanced architecture independence. For the commands model_check, approximate_model_check, compute_reach, incremental_ctl_verification, check_invariant, and lang_empty, the runs will be exactly the same on every platform with the same memory limits. Previously, invocations of reordering, and hence BDD sizes could differ from platform to platform. ** Changes to static_order. The static_order command has changed substantially. For combinational circuits, VIS-1.2 and earlier releases effectively generated random orders regardless of the method specified by the user. (Sequential circuits did not have this problem.) The randomness of the orders was due to a bug that has been fixed in VIS-1.3. For all circuits---combinational and sequential---the default ordering method is a new algorithm called "interleave." The new default method is substantially more memory efficient than the previous default method (merge_left). The quality of the resulting orders is comparable. ** New -v option for dynamic_var_ordering. The option -v 1 can be specified to cause VIS to write a one-line message whenever dynamic reordering is executed. The message reports the reduction in BDD or ZDD size, and on the time taken by reordering. This option is only effective with CUDD. ** New -i option for comb_verify and seq_verify. It is now possible to print statistics on BDD usage and performance when running combinational or sequential verification. This is done by specifying the -i option for comb_verify and seq_verify. It is important to notice that these two commands use a local BDD manager, which is destroyed before control is returned to the user. It is not therefore possible to use print_bdd_stats to inspect the statistics of the BDD package when invoking either of the two commands. ** Default method for build_partition_mdds changed to inout. The default method has been changed to inout, because this has been found to produce better results than frontier in many cases. The frontier method can build the partition MDDs in more cases than the inout method; the latter, however, tends to give better performance during model checking. ** set ctl_change_bracket [yes/no] VIS-1.3 includes this set command option for the CTL parser. VL2MV automatically converts "[]" to "<>" in node names, therefore the CTL parser does the same thing. However, in some cases a user does not want to change bracket type in the CTL formulas. This can be accomplished by setting this set command option to "no." The default is "yes". The commands affected are check_invariant, model_check, approximate_model_check, and incremental_ctl_verification. ** Printing time for model checking VIS-1.3 includes printing time for model checking. If verbosity is set on, then the model checking time for both each formula and total will be printed out. ** Incremental reachability analysis and invariant checking. In VIS-1.3 it is possible to perform reachability analysis incrementally. The -d option of compute_reach specifies how many steps (image computations) should be performed at most before returning control to the user. If compute_reach is invoked more than once with the -d option, each time reachability analysis starts from the previous result. If check_invariant is invoked after compute_reach has been invoked with the -d option, the partial reachability results are used to speed up verification. ** Completeness and determinism check in flatten_hierarchy The check for completeness and determinism performed by flatten_hierarchy that was previously optional is now always performed. The -b option to flatten_hierarchy and init_verify has no effect in VIS-1.3 and is retained for compatibility with existing scripts. It may disappear in future releases. Users of VIS-1.3 will observe modest increases in the time taken to flatten the hierarchy. Version 1.2 * Introduction ** Improvements *** Over 10x performance improvement in model checking for many examples *** extended CTL syntax *** better access to the BDD parameters and statistics *** enhanced user interface *** improved portability and flexibility of configuration ** New verification algorithms *** approximate_model_check: model checking of ACTL formulae for systems that are too large for model_check *** res_verify: residue based verification of arithmetic circuits * Performance improvement in model checking ** We have changed image computation (the underlying operation of model checking) to make the best use of don't care sets. The don't cares arise from unreachable states, and using them appropriately reduces the BDD sizes significantly, leading to improved performance of model checking. In addition, we have fixed a performance bug that caused repeated computation of simplified transition relations. We performed a performance comparison with VIS 1.1 on a set of examples, and on some cases we observed more than 30x performance improvement. In fact, on some examples VIS 1.2 could finish model checking in about 26 secs whereas VIS 1.1 took about 2400 secs. ** The model checking runs that use don't cares (-D option different from 0) are those that benefit the most from the changes in VIS 1.2. In general it is not trivial to tell whether -D 1 or -D 0 will produce the faster CPU time. An empirical approach consists of running "compute_reach -t 300" (reachability for 5 minutes). Depending upon the progress in reachable state computation, one can then invoke model checking with -D 0 or -D 1. * Approximate Model Checking ** VIS 1.2 includes a new command approximate_model_check, a model checker that performs ACTL model checking on an abstracted and flattened network. The command is designed to tackle the state explosion problem we encounter when dealing with large and complex circuits. Based on the initial size of the group (of latches), the command constructs an over- or under-approximation of the transition relation of the system. These approximations may not contain every detail of the exact system. However they may contain enough information to determine whether the formula is positive or negative. Starting from an initial coarse approximation, the command makes its effort to prove whether the given ACTL formula is true or false. When the procedure fails to prove correctness of the formula with initial approximations, it automatically refines the approximations. It repeats the process until the algorithm produces a reliable result or the available resources are exhausted. For detailed description, refer to the relevant manual page ("help approximate_model_check from" the VIS shell). ** approximate_model_check is faster than model_check for some of the VIS 1.2 distribution examples. However, significant improvements over the exact computation can be seen for even larger examples such as s15850. The current version of the code does not perform any refinements. The refinement techniques similar to the "machine by machine" and "frame by frame" may be implemented in future version. Furthermore, more aggressive reduction of the initial states can be performed while proving whether the ACTL formula is positive. The reduction of the initial states are made for each level of the lattice of approximations in this version. ** The current version includes two distinct "grouping method". More experiments are required to determine better grouping method(s). ** The current version only supports ACTL formulae. * Residue Based Verification ** VIS 1.2 includes a new command "res_verify" for combinational verification based on residue arithmetic. Residue-based verification is especially suited to multipliers and other arithmetic circuits. See below, however, for a discussion of the application of "res_verify" to other circuits. This command is only available if VIS has been linked with the cu library (default). ** The command res_verify takes two circuits (specification and implementation) whose equivalence is to be established, and an order for the outputs. The order for the outputs allows res_verify to interpret the output vectors as integers. Based on this interpretation, res_verify applies the Chinese remainder theorem to the equivalence verification: the specification and the implementation are equivalent if, for a suitable set of relatively prime numbers, the residues of their outputs are equivalent. The residues are computed by composing the two circuits into a function representing the residue computation. ** res_verify allows the user to specify what pairs of outputs of the circuits should be compared directly by building their BDDs, instead of computing residues for them. The -d option controls this feature; n pairs of outputs, starting from the least significant bits of the output vectors, are verified directly if -d n is specified. ** As a special case, the user can specify -d all. This causes res_verify to directly verify all the output pairs, effectively foregoing residue verification. This can be useful for non-arithmetic circuits that are not suited to residue verification. In this case res_verify works similarly to comb_verify, with a significant exception: res_verify verifies one output at the time. This often translates into reduced memory requirements and CPU times. ** res_verify can be applied to pairs of sequential circuits with the same state encoding. Several options and VIS variables control the detailed behavior of the command. Refer to the on-line documentation for the details (help res_verify). * Extended CTL Syntax ** Users can now write CTL fomulae using vector notation. Vector variables have the form of var[i:j] and each bit can be written as either var or var[i]. For instance, the following formulae are valid. counter[3:0] = 10 counter[3:0] = b1010 counter[3:0] = {1,2,10} The formula in the last line is true if counter has one of the listed values. ** Macros can be defined and used in CTL formulae to stand for subformulae. For instance: \define VALID_INPUT (a[3:0]=0 -> b=1) defines the macro VALID_INPUT, which can be later used in a formula like this: AG(start=1 * \VALID_INPUT -> AF(res[7:0]=b10101010)); ** The CTL parser allows users to write the following formulae: var1 == var2 var1[i:j] == var2[k:l] The first formula is equivalent to (var1=1) * (var2=1) + (var1=0) * (var2=0) and currently is allowed only in the boolean domain. (It cannot be used for variables of enumerated types.) The second formula can be used if the lengths of two vectors match. ** AX:n(f) is allowed as a shorthand for AX(AX(...AX(f)...)), where n is the number of invocations of AX. EX:n(f) is defined similarly. * BDD manipulation ** VIS 1.2 incorporates Release 2.1.1 of CUDD and an improved version of CAL. Improvements specific to CUDD and relevant to VIS are: ** All reordering methods preserve variable groups. Variable groups are created by VIS to keep corresponding present and next state variables adjacent. In VIS 1.1 only method "sift" retained the variable groups. ** CUDD determines the maximum size of the computed table based on the amount of main memory available. On systems where getrlimit is available, the datasize limit is used to determine how much memory is available. CUDD allows the computed table to grow up to one fourth of that amount. This feature allows VIS to self-calibrate for optimum performance. The computed table will not necessarily grow to its maximum value, and VIS is not guaranteed to stay within the memory bound returned by getrlimit. If the datasize limit is not set, if getrlimit is not available, or if it is available but does not know about datasize, then a suitable default value is used instead. The default value is normally 16MB. This value can be changed at configuration time. Even a value as low as 16MB gives a reasonably sized computed table for small-medium runs. However, for large runs--hundreds of MB--the ability to set the memory limit may produce much faster execution. The maximum computed table size can be set also from within VIS with set_bdd_parameters. ** CUDD now provides access to the package parameters and statistics via the commands bdd_print_stats and set_bdd_parameters. The parameters that can be set control the sizing of CUDD's main data structures (unique table and computed table) and many aspects of the variable reordering algorithms. The parameters reported refer to memory occupation, computed table (cache) performance, and variable reordering. ** It is now possible to impose a limit on the number of variable swaps performed during reordering. * User Interface ** New VIS command "set_bdd_parameters". The command "print_bdd_stats" prints two sets of data from the underlying BDD package, parameters and statistics. The parameters can be modified as follows. By using the "set" command, set the value of a variable whose prefix is "BDD." and whose suffix is exactly the name seen in the output of the command "print_bdd_stats", for example: vis> set "BDD.Garbage collection enabled" no Then, the command "set_bdd_parameters" reprograms the underlying BDD core based on the values of the variables of this type. ** Readline Library. The Readline library is a GNU package that provides command line editing, command history, and file name completion capabilities. If the system where VIS is built has this library and it is installed so that the linker can use it, the configure script will detect this situation and the executable will be linked with libreadline.a. ** Variable Interpolation. The VIS shell now allows variable interpolation. For instance, typing vis> echo $open_path causes vis to echo the current value of open_path. Typing vis> set open_path $open_path:/some/path will append /some/path to open_path. Variable interpolation can be used also to exchange parameters with scripts. This allows reliable parameter passing even when "source" is called with options. ** PAGER If the PAGER environment variable is set, VIS uses it to choose the program used to display the help pages. If PAGER is not set, VIS uses 'more.' ** File Buffering. The output of VIS when run in batch mode is now line buffered on systems that provide setvbuf. This makes it more convenient to observe the evolution of long-running jobs. * Portability and Configuration ** VIS 1.2 runs on two new platforms: IBM RS6000 running AIX and Intel Pentium running Windows95 with Gnu-Win32. The Gnu-Win32 environment (http://www.cygnus.com/misc/gnu-win32/) is a freely available GNU environment for Windows 95 and Windows NT. ** This release of VIS has been tested with some native compilers (Ultrix, Solaris, Digital Unix). In particular, when building with the native compiler on a DEC Alpha running Digital Unix, the option is provided to compile with 32 bit pointers. Please see the README file for specific instructions on how to compile with the different native compilers. ** The GLU library now provides portable functions for random number generation and sorting that help make results reproducible across different platforms. ** The GLU library now provides a function to read the available memory (based on getrlimit). This function is currently used by the CUDD package to choose the optimal size of data structures. For systems without getrlimit a suitable default is provided and can be changed at configuration time. Version 1.1 * Introduction ** Improvements over 1.0 *** multiple BDD packages *** more synthesis capability *** hierarchy restructuring *** new methods for partitioning *** automatic reduction during model checking *** support for multi-phase clocking and transparent latches *** support for invoking standard scripts *** support for graphically viewing simulation output These significantly improve VIS's performance in terms of computer time, memory usage, and ability to complete on larger designs. Further, additional capability for synthesis is provided. One particular example of the improved performance of VIS 1.1 is the first (to our knowledge) reported exact state space traversal of benchmark s5378. It was run with the cu BDD package on an Alpha 300MHz (using 32 bit pointers). The datasize limit was set at 1GB. The process grew to about 440MB. Dynamic reordering was enabled all the time and occurred more than 50 times. The orginal ISCAS89 circuit was used, which has 179 latches. *** Multiple BDD packages We have added the capability to run VIS with three different BDD packages, cu - from University of Colorado, cal - from UC Berkeley and cmu - from Carnegie Mellon University. Further details are in the section "BDD Packages" below. *** Synthesis VIS synthesis is represented by a number of commands, write_blif, read_blif, collapse_child, and decompose_child. These allow the user to manipulate the hierarchy and to write blif files to SIS and then later read in an optimized file. Each of these commands can be executed on sub-nodes or sub-trees of the hierarchy. Details about these commands are in the section "Collapsing and decomposing a hierarchy" and "Reading and writing blif files" below. *** Partitioning Partitioning in VIS is used in a number of places: simulation, model checking, computing the set of reached states, etc. Recall that the VIS data structure is simply a set of tables with outputs (signals) which can be inputs to other tables. There are also primary input signals and inputs from latches. Some signals are primary outputs and/or inputs to latches. A partition is simply a subset of nodes (signals) which are to be preserved, the remaining are to be eliminated. Of course, primary outputs and inputs to latches cannot be eliminated. We provide some new partitioning methods as described below (in the section "Creating partitions of the network"). In many cases, a formula to be model checked does not depend on all of the signals in the design. In such cases, the design can be reduced to include only signals in the transitive fan-in of the latches mentioned in the CTL formula plus the fairness constraints. This reduction can result in vastly more efficient model checking. *** Multi-phase clocking One question that is asked frequently is how does VIS support multi-phase clocking and transparent latches in Verilog. We provide this capability in our Verilog compiler "vl2mv" and detail this in a document that describes exactly the steps to be taken. This document is in the vis-1.1/doc directory and is called two_phase.ps. *** Standard scripts Standard scripts have been provided which should help the new user select certain options that we have determined to be good choices on a variety of examples. The scripts are divided into two categories: simple - which are recommended for small/medium examples, and robust - recommended for large examples where completion rather than compute time is the most important concern. The 10 scripts provided are summarized below in the section "Standard scripts". *** xsimv Finally, we have included "xsimv", which provides a graphical method for viewing simulation output. This is detailed in the section "Using Xsimv". * Multiple BDD packages We have added the capability to run VIS with three different BDD packages, cu - from University of Colorado, cal - from UC Berkeley and cmu - from Carnegie Mellon University. The commands for these respectively are vis-cu, vis-cal, and vis-cmu. The cmu package is the same as in VIS 1.0. The cu package is very strong in having a fast dynamic variable reordering capability. In addition, cu has been upgraded for the DEC alpha machines so that it uses 32 bit pointers, instead of 64 bit pointers; hence it realizes a factor of 2 in memory savings on such machines. The other two packages remain to be upgraded for 32 bit pointers on the DEC alphas. The cal package uses the BFS BDD technique and is particularly good at avoiding paging on large designs. For most problems, we recommend the cu package. * Reading and writing BLIF files The "write_blif" command in vis-1.0 only wrote out the combinational part of an hnode (a node of the hierarchy). Now this functionality is performed by the "write_blif -c" command. Other options have been added as well. The options are: (1) write_blif -l writes out the latches of the hnode as well. Additionally, all latch IOs are made into POs in the blif file that is created. This ensures that the these nodes do not get optimized away by SIS, so that mv-latches can be re-inserted by the read_blif command in VIS. (2) write_blif -c same as "write_blif" of vis-1.0 (3) write_blif writes out latches of the hnode, but does not make latch IOs into POs in the blif file. The .blif and .enc files that are generated by this command currently cannot be guaranteed to read back into VIS correctly using the read_blif command. (4) write_blif -R recursively writes out the entire hnode hierarchy rooted at the current hnode, to a blif file. This command opens up a direct path from Verilog to pure blif files and hence to synthesis in the SIS framework. For this command to work, 1) all variables in the hnode hierarchy rooted at the current hnode must be binary, 2) all tables should be deterministic, and 3) there must be a unique initial state. * Collapsing and decomposing a hierarchy If the user travels (via "cd" commands) to a particular node in the hierarchy and does a "write_blif", only the logic in the *current* node gets written out. The user might want to collapse some of the child nodes together and do synthesis in the "collapsed" node. The "collapse_child" command does just that. The usage is: collapse_child and the effect is that the child node is absorbed by the parent. By successive invocations of this command, multiple nodes can be collapsed into a single node. "decompose_child" is a command that effects the inverse operation of collapse_child. The user can specify components of the current node to be grouped as a separate newly created child node. The user must also specify the name of the new child. Successive invocations of "decompose_child" can be used to effect multiple decompositions. "decompose_child" provides the infra-structure for implementing and testing FSM decomposition algorithms (to appear later). Together, collapse_child and decompose_child provide powerful primitives that can be used to restructure the design hierarchy. * Creating a flattened network for verification The important change to note is the "-b" option in the "flatten_hierarchy" command. By default this option is off, implying that the system is not checked for complete and deterministic specification. However, if the given design does not meet this criteria, model checking may produce wrong results. (Note: In VIS nondeterminism is handled by providing pseudo-inputs. Internally all the tables are deterministic and completely specified.) Invoking this "-b" option forces the necessary checking. However this can be computationally expensive. The best strategy is to invoke "flatten_hierarchy" with "-b" option the first time and if the check passes, use it without "-b" option in subsequent runs. * Creating partitions of the network Three new methods for creating partitions for the "build_partition_mdds" command have been added. - partial This can be used to perform partitioning while forcing a user-specified set of signals (nodes) in the partition. The set of nodes to be included can either be supplied in a file, or on the command line. - boundary In this method, all nodes that are sub-circuit IOs are included in the partition. - frontier In this method (the default method), the user specifies a parameter "partition_threshold" which is used to include an intermediate variable whenever the BDD size for a node in the network increases beyond the threshold value. This method is very useful when it is not possible to create the next state functions in terms of primary inputs because of large BDD sizes. This method encompasses both "in_out" and "total" partitioning methods (corresponds to very large and 0 value of "partition_threshold", respectively). The parameter can be set by invoking the following from the VIS commandline: "set partition_threshold ". * Reachability computation A few new options to reachability computation have been added (command: compute_reach). -d depthValue Used to perform reachability up to a certain number of steps. -r threshold_value Invokes dynamic reordering of variables ONCE, after the size of the reached state set crosses the threshold_value. * CTL Syntax For Verilog compatibility, && and || are supported in addition to * (Boolean AND) and + (Boolean OR) respectively. * Model checking The mc command, by default, now reduces the model FSM with respect to the union of all the formulas in the CTL file and uses the reachability don't cares (thus reachablilty is done first before any model checking). Also, -d 0 is the default now, i.e. no error trace is computed. The -r option has been modified and a new capability for sharing sub-formulas has been added. -r (This option has been modified). If this option is used, each formula is model checked individually on an FSM reduced with respect to the formula. -c This disables the default that sub-formulas of the formulas given in the CTL file are shared. The sharing of sub-formulas makes sure that a sub-formula in the set of all sub-formulas of the formulas in the CTL file is evaluated only once. If both -r (formula dependent FSM reduction) or "-D 1" (use reachability don't cares) are enabled, this facility is automatically disabled. (Note that currently if the same sub-formula occurs more than once within a single formula, it may be checked twice.) * Standard scripts There are 10 standard scripts provided (in the "share" directory), divided into two categories, simple and robust. The simple scripts work best on small/medium size examples. The robust scripts are recommended for large problems where the objective is to complete the computation without too much concern for computation time. Below are the scripts with their required arguments. All scripts assume that a BLIV-MV file has already been read in. script_generic.simple script_compute_reach.simple script_model_check.simple foo.ctl script_fair_model_check.simple foo.fair foo.ctl script_lang_empty_check.simple foo.fair script_generic.robust script_compute_reach.robust script_model_check.robust foo.ctl script_fair_model_check.robust foo.fair foo.ctl script_lang_empty_check.robust foo.fair In all cases, "script_generic" is a preample to the other scripts. Generally, we recommend trying a "simple" script first, since it should be the fastest. * Using "xsimv" Before invoking xsimv, please modify the first line of the file "xsimv" and put the complete path name for "expectk". xsimv is invoked by the command xsimv where is a file produced by the vis command simulate -n -o When xsimv executes, it comes up with a window with 4 buttons in it, GO, ReDraw, Save and Quit. At the same time it produces a file, "strk.simv", with the signal names in it. For example sensor.rand_choice timer.rand_choice car_present farm_light hwy_light timer.state If only a subset of these names are required the user can edit this file and comment out a line using "#". For example, #sensor.rand_choice #timer.rand_choice car_present farm_light hwy_light timer.state will cause the first two signals' simulation to be not displayed. Pushing GO or ReDraw then produces a new window with the simulation results shown where time increases from left to right. The signal value names not commented out are shown vertically, one for each row. The "edit strk.simv" and REDRAW sequence can be iterated. Version 1.0 * Initial release