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