source: vis_dev/vis-2.3/NEWS @ 99

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

Release 2.3 of VIS improves VIS 2.2 in the following areas:

* Builds with bison 2.4.1 and gcc 4.4.1

* Supports cusp-1.1 as external SAT solver for bounded model checking
  instead of zchaff

* Bug fixes

======================================================================

Version 2.2

Release 2.2 of VIS improves VIS 2.1 in the following areas:

* Compiles with gcc 4.3 and bison 2.3
* Supports both 64-bit and 32-bit compilation on x86_64 machines
* Allows the use of up to 4 GB of memory with 32-bit pointers
  (previously 2 GB)
* improved vl2mv produces smaller blif-MV files
* vl2mv 2.2 drops support of obsolete output formats (e.g., Shift)
* Support for weak until operator in both CTL and LTL
* Improved node matching for combinational equivalence (comb_verify)
* Fixed bug in the translation of LTL properties to Buechi automata
* New command write_network_blif_mv
* faster flatten_hierarchy
* new functions mdd_array_dump_dot mdd_array_print_cover make
  debugging easier
* CUDD 2.4.2
* vis-verilog-models-1.2

======================================================================

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 <HintsFileName> : guided symbolic state space 
                                       traverse
    check_invariant -g <HintsFileName> : 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 <HintsFileName>


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 <HintsFileName>
               check_invariant -g <HintsFileName>


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 <depth> : sets the cluster depth for SPFD
                            computation. 
     spfd_pilo -f <file>  : use simulation vectors from specified
                            file. These vectors are used to compute 
                            switching activity of nodes in the circuit.
     spfd_pilo -S <method-number> : selects one of several methods to
                            choose the node to be optimized.
     spfd_pilo -m <method-number> : 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 <n> 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<i> 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 <child_name>

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

* 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 <sim-file>

  where <sim-file> is a file produced by the vis command 

        simulate -n <num> -o <sim-file>

  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