source: vis_dev/vis-2.3/README

This is release 2.3 of VIS, a system for verifying and synthesizing
finite-state systems.  VIS builds on GLU, a collection of BDD packages
and low-level utilities.

To build VIS and GLU, you will need

   * An ANSI C compiler (gcc will do, as will several versions of cc)
   * GNU Flex version 2.5 or greater
   * GNU Bison version 1.22 or greater
   * GNU's make utility
   * GNU's gzip utility
   * Approximately 90 MB of free disk space for the build of both
     vis and glu
   * Approximately 60 MB of free disk space for the installation

---------------------------------------------------------------------------
* Useful Addresses

The most recent version of vl2mv, the Verilog compiler designed to work 
with VIS:

        ftp://vlsi.colorado.edu/pub/vis/vl2mv-2.3.tar.gz

The most recent versions of VIS and GLU:

        ftp://vlsi.colorado.edu/pub/vis/{glu-2.3.tar.gz,vis-2.3.tar.gz}

The VIS home page, which includes additional documentation:

        http://vlsi.colorado.edu/~vis

The most recent version of the GNU tools:

        http://www.gnu.org

The most recent version of perl, which is required to run 'visdbgpp':

        http://www.cpan.org

The most recent version of expectk, which is required to run 'xsimv':

        http://expect.nist.gov

The most recent version of Tcl/Tk, which is required to run 'expectk':

        http://www.scriptics.com/

Optionally, the most recent version of cusp, the SAT solver which
can be used instead of CirCUs 1.0 (included in VIS) to execute the
bounded_model_check command:

        ftp://vlsi.colorado.edu/pub/CUSP/cusp-1.1.tar.gz

---------------------------------------------------------------------------
* Platforms

This is the list of architecture/operating system/compiler
combinations we have tested. (For installation with compilers marked
with (*) please refer to the Platform Specific Instructions.)

        * Intel ia32 / Linux / gcc, g++
        * Intel x86_64 / Linux / gcc, g++, icc(*)
        * Intel ia32/x86_64 / Windows XP with Cygwin 1.5.16-1 / gcc, g++(*)
        * Intel ia32 / Mac OS X / gcc(*)

The following platforms are no longer supported, but should still work.

        * IBM RISC System/6000 / AIX Version 4.3.3 / gcc(*)
        * Intel ia64 / Linux / gcc
        * Sun Sparc/ Solaris 2.8 / gcc, g++, cc(*)

The following instructions are for the generic build process.  Before
building the tool please refer to the section "Platform Specific
Instructions".

---------------------------------------------------------------------------
* Building VIS

To build a VIS executable for a single operating system:

1. Download the most recent versions of VIS and GLU from the address
   above into a convenient directory, (e.g., /tmp).

2. Move to where you would like to build VIS and GLU and unpack the
   distributions:

        % cd /home/vis                                  # for example
        % gzip -dc /tmp/glu-2.3.tar.gz | tar xf -
        % gzip -dc /tmp/vis-2.3.tar.gz | tar xf -

3. Move into the glu-2.3 directory and run configure, which will
   determine some system-specific parameters and create the Makefile:

        % cd glu-2.3
        % ./configure

   By default, this will use your system's native compiler.  To use gcc,

        % ./configure --enable-gcc

   (You may want to do this because you don't have the native compiler
   installed or because it is not ANSI.)

   Note: For platforms where VIS is not supported for the native compiler,
   the default compiler is set to gcc.

   Note: Not all checks in ./configure will return "yes."  This is
   normal and should not affect compilation.  However, do be concerned
   with any warnings "configure" produces.

   Note: Occasionally, configure will make a bad guess or will choose
   a default you do not want.  In this case, simply edit the Makefile
   after configure finishes.

   Note: You may want to specify parameters to configure -- see the
   "Installing" sections below.

   Note: To parallelize the installation procedure, you can begin steps 
   5 and 6 at this point, as long as step 4 completes before step 6
   (since VIS must link against the GLU library).

   Note: The Makefile by default uses the "-g" option for
   compilation.  The resultant "vis" executable may be much larger than
   the executable generated without using the "-g" option.  Using the
   "-g" option however, provides debugging capabilities.

   Note: The following is of interest only to people developing code
   within vis.  For full debugging support, specify
   --with-comp-mode=debug.  This will turn off optimization, and turn
   on the assertions (sanity checks) in the code.  Similarly,
   --with-comp-mode=purify and --with-comp-mode=quantify will link vis
   with IBM Rational's Purify or Quantify tool, if it is installed.

4. Build the GLU system by running GNU's gmake utility:

        % gmake

   You may not have GNU make installed on your system under the name
   'gmake' -- try make.  If this fails, you probably need the latest
   version of GNU's make program -- download it from the address
   above.

5. Move into the vis-2.3 directory and run configure:

        % cd ../vis-2.3
        % ./configure

   By default, this will use your system's native compiler.  To use gcc,
  
        % ./configure --enable-gcc

   (You may wish to do this because you don't have the native compiler  
   installed or because it is not ANSI.)

   Note: For platforms where VIS is not supported for the native compiler,
   the default compiler is set to gcc.

   Note: If you supplied compilation-option flags (e.g., --enable-64)
   to the GLU configure, provide the same to the VIS configure.
 
   Note: Not all checks in ./configure will return "yes."  This is
   normal and should not affect compilation.  However, do be concerned
   with any warnings "configure" produces.

   Note: Occasionally, configure will make a bad guess or will choose
   a default you do not want.  In this case, simply edit the Makefile
   after configure finishes.

   Note: You may want to specify parameters to configure -- see the
   "Installing" sections below.

   Note: You may want to remove the "-g" flag from the make file.  See
   under 3.

6. Build the VIS system by running GNU's gmake utility:

        % gmake

   This builds an executable "vis" in the current directory.

   WARNING: If you are not successful in building a VIS executable, 
   double check that you are using Flex version 2.5 or greater (check 
   using "flex -V") and GNU Bison version 1.22 or greater (check with 
   "bison -V").  Having out-of-date versions of these programs can 
   lead to obscure compilation and linking errors.  You can download
   the new versions from the GNU FTP address above.

   VIS expects to find master.visrc, two .nawk files, and a directory
   of help files in the directory given by the environment variable
   VIS_LIBRARY_PATH.  Set this to the "share" directory in the source
   tree:

        % setenv VIS_LIBRARY_PATH $cwd/share

7. OPTIONAL: Verify VIS works by running it on some of the examples
   included in the distribution:

        % gmake check

   This step finishes in less than five minutes on most machines
   and requires approximately 32 MB of RAM.

---------------------------------------------------------------------------
* Installing GLU:

Developers will want to install the GLU library and its associated header
files in a central area:

To install the GLU library and its header files, type, while in the
glu-2.3 directory,

        % gmake install 

By default, this will put libraries and headers in /usr/local/lib
and /usr/local/include respectively.  To choose a different
location, provide a default prefix when you invoke configure, e.g.,
to install in /projects/glu/bin, etc., use

        % ./configure --prefix=/projects/glu

when configuring GLU.  Note that "tilde expansion" doesn't work for the  
prefix (i.e., don't specify --prefix=~smith/glu).

---------------------------------------------------------------------------
* Installing VIS:

Administrators and people who want to discard the source files after
building VIS may install VIS in a central area:

To install the VIS executable, library, headers, and help files, type,
while in the vis-2.3 directory,

        % gmake install

By default, this will put binaries, libraries, headers, and help files
in /usr/local/bin, /usr/local/lib, /usr/local/include, and
/usr/local/share respectively.  To choose a different location,
provide a default prefix when you invoke configure, e.g., to install
in /projects/vis/bin, etc., use

        % ./configure --prefix=/projects/vis

when configuring VIS.

"gmake clean" removes all the files generated during "gmake."  This is
useful when you want to rebuild VIS with a different prefix,
different compiler options, etc.

During configure if --prefix option is used, files found in the
"share" directory will be installed in $prefix/share/vis; otherwise
they will be installed in /usr/local/share/vis by default.  Set the
environment variable "VIS_LIBRARY_PATH" to the appropriate directory so
that VIS can find master.visrc, the two .nawk files and the "help"
directory.  The above mentioned files can also be present in a
different directory, but "VIS_LIBRARY_PATH" should be set to that
directory.  For example,

        % setenv VIS_LIBRARY_PATH /projects/vis/common

---------------------------------------------------------------------------
* Installation for multiple platforms

To install VIS on multiple operating systems depending on the same
source tree, see the file "INSTALL" included in the distribution.

In this case, when the build directory is different from the source
directory, it's necessary to configure VIS to look elsewhere for the
GLU libraries and headers, e.g.,

        % ./configure --with-glu-libdir=/tmp/glu-2.2/alpha \
                --with-glu-incdir=/tmp/glu-2.1/include

Also, make sure that there is an obj/ directory in the directory in
which you are compiling.  See ./configure --help for more information.

---------------------------------------------------------------------------
* Selecting a different BDD package

To create VIS with a different BDD library (say cal) than the default
one (cu), use the following command:

        %./configure --with-bdd=cal

The same can be achieved by changing the "BDDPKG" definition in the
Makefile from "cu" to "cal".

VIS can work with three different BDD packages (cmu, cal, cu), all of
which are supplied with glu-2.3.  However, some commands in VIS are
available only with the cu BDD package.  Please refer to the NEWS file
for more details. 

---------------------------------------------------------------------------
To create three versions of VIS, each with different BDD libraries,
run 'gmake allprods'.  This will create vis-cal, vis-cu, and
vis-cmu.  To verify whether all these executables are compiled
correctly, use 'gmake check-allprods' at the end.
---------------------------------------------------------------------------

* Files in the VIS distribution:

README          This file.

INSTALL         Generic installation instructions for use with configure, 
                including instructions for simultaneous multi-platform 
                builds.  These are not specific to VIS nor GLU, so don't 
                follow them word for word.

NEWS            Changes since the last version/release.

configure       An executable shell script that creates "Makefile" from
                Makefile.in after determining system-specific parameters.

configure.in    Autoconf source for generating the configure file.
                Only needed if you want to modify the configure script.

Makefile.in     The template Makefile.

vis.1           Unix-style man page documenting vis invocation
                parameters.

xsimv           An expectk script to visualize VIS simulation traces.

helpers/        Programs useful during configuration and building
 install-sh     Shell scripts used by "gmake install."
 mkinstalldirs
 config.guess
 config.sub
 dependency.make

doc/vis_user.ps
                A user's manual for the VIS system, describing our approach
                to formal verification and how to use the tool.

doc/blifmv.ps   Documentation on the BLIF-MV file format, a low-level 
                language for specifying designs.

doc/ctl.ps      Documentation on the CTL file format, a language
                for specifying properties.

examples/*/     A collection of small systems and properties to be
                verified.  Used by "gmake check."

share/master.visrc
                A VIS script designed to be run automatically at
                start-up: contains aliases for commonly used commands
                and some default parameter settings.

share/*.nawk    nawk scripts for converting BLIF files to BLIF-MV,
                used by the "read_blif" command.

share/script*   Sample scripts.

share/sislib.mv Library of gates used by models translated by vl2mv
                from gate-level Verilog descriptions.

share/visdbgpp  A perl script to pretty-print counterexamples produced
                by the model_check and check_invariant commands.

share/help/     ASCII documentation for each VIS command, accessible
                through the "help" command within VIS.

src/*/          Source code and headers for the VIS system.

obj/            Directory where .o files and generated .c files are
                placed during a build.

checkresults/   Directory where tests (i.e., gmake check) are run.
                Results of the tests are placed here.  The directory
                is only created when 'gmake check' is run.

---------------------------------------------------------------------------
* Platform Specific Instructions

Note: some instructions apply to platforms we no longer support.

** Little-endian machines:

  vis-cal will occasionally fail when compiled with
  --with-comp-mode=debug on little-endian machines like the Alphas and
  the Intel ix86 CPUs.

** x86_64 machines:

  Compilation is possible in both 64 and 32-bit modes.  

  For 32-bit compilation with gcc, make sure the appropriate libraries
  are installed.  On Ubuntu, for instance, you need the multilib-g++
  package.  Configure both glu and vis with --enable-gcc="gcc -m32".

  With the Intel compiler (icc), the choice between 64 and 32-bit
  modes is made when the compiler variables are initialized.  Once
  that is done, configure both glu and vis with --enable-gcc=icc.

** Mac OS X:

  For correct operation of vis-cmu, uncomment the definition
  of USE_MALLOC_FREE at line 126 of src/mem/memint.h before building glu.

** Solaris (Sparc and ix86):

  If Sun's C compiler is not installed on your system, use gcc
  (./configure --enable-gcc).

  Warnings about redefined symbol are harmless, so are the warnings
  that say "end-of-loop code not reached".

  The sun cc compiler (Workshop 6 update 1) on ix86 appears to have a
  bug in the optimization routines.  The -xO4 an -xO5 compiler options
  will make vis crash in some runs.  As a safety precaution, we have
  changed the optimization flag to be -xO3 for all Sun platforms that
  use the cc compiler.  You can try higher optimization flags on your
  machine.  In general, it is hard to determine cc options that will
  give optimal results on every platform, so it may pay off to play
  atound with the optimization options.

** MS Windows with Cygwin:

  You need Red Hat's Cygwin environment (freely available from
  http://www.cygwin.com) to build GLU and VIS.

  With Cygwin the configuration script automatically selects gcc.

** HP-UX:

  Some operating systems on HP machines have a built-in command called
  "vis" under /usr/ucb.  In light of this, be careful about the
  definition of your  path.

** AIX:
 
  The configuration script automatically selects gcc.  vis-cal
  occasionally produces incorrect results when optimization is turned
  on.  If you plan to use vis-cal with AIX, you should configure glu
  and vis with --with-comp-mode=debug.

** Intel A64:

  vis-cal compiled with gcc 3.2.3 crashes when sifting is invoked.

** DEC Alpha:

  Warnings about MIN and MAX are harmless.
  Warnings about Olimit are harmless.  They can be gotten rid of by
  increasing the number following Olimit under CFLAGS.

  By default, configure uses 32-bit pointers when using DEC's OSF/1 C
  compiler for the Alpha, which is more efficient if your processes
  use less than 2GB.  To use 64-bit pointers, invoke configure as follows:

        % ./configure --enable-64

  The gcc compiler always compiles with 64-bit pointers.

  Note that you must also specify this flag when configuring GLU.

  Some machines do not have the program 'om'.  In this case, simply
  removing the om flag from LDFLAGS is sufficient to complete
  compilation.

** IRIX

  When compiling VIS with gcc, you may get the error message

  gcc.x: cannot specify -o with -c or -S and multiple compilations

  If this happens, edit Makefile, and replace the definition of
  VERDATE with the following:

  VERDATE := -DCUR_DATE="\"N/A\"" -DCUR_VER="\"$(PRODUCT)-$(VERSION)\""

---------------------------------------------------------------------------
* Verilog front-end

vl2mv, written by Szu-Tsung Cheng, allows one to translate a subset of
Verilog into blif-MV, the input format of VIS.  The most recent
version of vl2mv can be found in ftp://vlsi.colorado.edu/pub/vl2mv-2.3.tar.gz.
This version requires glu-2.3 to compile and link.