RELEASE NOTES FOR VIS 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.