VIS 1.2 Released 
Author Message
 VIS 1.2 Released

We are glad to announce the release of VIS 1.2. Below is a description
of VIS and of the new features. VIS 1.2 can be downloaded from the VIS
homepage at http://www.*-*-*.com/ ~vis

DESCRIPTION

Formal verification system with Verilog HDL front end.  Computation
model is a set of synchronously communicating FSMs.  Emphasis is on
fair CTL (computation tree logic) model checking, with error trace
generation.  Supports, as proof of concept, cycle-based simulation,
combinational equivalence checking, and sequential equivalence
checking. Has links to the sequential synthesis tool, SIS.  Jointly
developed by Univ. of California at Berkeley, Univ. of Colorado at
Boulder, and Univ. of Texas at Austin.

RELEASE NOTES FOR VIS 1.2

* Introduction

** Release 1.2 of VIS improves VIS 1.1 in the following ways:
  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.

** Release 1.2 also introduces two 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.*-*-*.com/ ) 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.

--
Fabio Somenzi          | Phone: 303-492-3466
University of Colorado | Fax:   303-492-2758

Boulder CO 80309-0425  | WWW:   http://www.*-*-*.com/ ~fabio



Sat, 21 Aug 1999 03:00:00 GMT  
 
 [ 1 post ] 

 Relevant Pages 

1. Cast Off 1.2 Released!

2. TimeSavers Scheduler 1.2 Released

3. WinAPI Toolkit Version 1.2 Beta 3 Released (FREE)

4. XScan 1.2 Released

5. twTools version 1.2 released

6. SearchFlash 1.2 Released

7. Details on Tower's new 1.2 release

8. Xbase++ SL1, 1.2 patches released today.

9. StarLogo 1.2 Official Release!

10. ANNOUNCE: Glasgow Haskell 0.29 release (for Haskell 1.2) [repost]

11. ANNOUNCE: Glasgow Haskell 0.29 release (for Haskell 1.2)

 

 
Powered by phpBB® Forum Software