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.