source: vis_dev/vis-2.1/README @ 15

Last change on this file since 15 was 11, checked in by cecile, 13 years ago

Add vis

File size: 15.8 KB
Line 
1This is release 2.1 of VIS, a system for verifying and synthesizing
2finite-state systems.  VIS builds on GLU, a collection of BDD packages
3and low-level utilities.
4
5To build VIS and GLU, you will need
6
7   * An ANSI C compiler (gcc will do, as will several versions of cc)
8   * GNU Flex version 2.5 or greater
9   * GNU Bison version 1.22 or greater
10   * GNU's make utility
11   * GNU's gzip utility
12   * Approximately 90 MB of free disk space for the build of both
13     vis and glu
14   * Approximately 60 MB of free disk space for the installation
15
16---------------------------------------------------------------------------
17* Useful Addresses
18
19The most recent version of vl2mv, the Verilog compiler designed to work
20with VIS:
21
22        ftp://vlsi.colorado.edu/pub/vis/vl2mv-2.01.tar.gz
23
24The most recent versions of VIS and GLU:
25
26        ftp://vlsi.colorado.edu/pub/vis/{glu-2.1.tar.gz,vis-2.1.tar.gz}
27
28The VIS home page, which includes additional documentation:
29
30        http://vlsi.colorado.edu/~vis
31
32The most recent version of the GNU tools:
33
34        http://www.gnu.org
35
36The most recent version of perl, which is required to run 'visdbgpp':
37
38        http://www.cpan.org
39
40The most recent version of expectk, which is required to run 'xsimv':
41
42        http://expect.nist.gov
43
44The most recent version of Tcl/Tk, which is required to run 'expectk':
45
46        http://www.scriptics.com/
47
48Optionally, the most recent version of zchaff, the SAT solver which can
49be used to CirCUs (included in VIS) to execute the bounded_model_check command:
50
51        http://www.ee.princeton.edu/~chaff/
52
53---------------------------------------------------------------------------
54* Platforms
55
56This is the list of architecture/operating system/compiler
57combinations we have tested. (For installation with compilers marked
58with (*) please refer to the Platform Specific Instructions.)
59
60        * IBM RISC System/6000 / AIX Version 4.3.3 / gcc(*)
61        * Intel ix86 / Linux / gcc, g++, icc
62        * Intel ix86 / Windows XP with Cygwin 1.5.16-1 / gcc, g++(*)
63        * Intel ia64 / Linux / gcc
64        * Sun Sparc/ Solaris 2.8 / gcc, g++, cc(*)
65
66The following instructions are for the generic build process.  Before
67building the tool please refer to the section "Platform Specific
68Instructions".
69
70---------------------------------------------------------------------------
71* Building VIS
72
73To build a VIS executable for a single operating system:
74
751. Download the most recent versions of VIS and GLU from the address
76   above into a convenient directory, (e.g., /tmp).
77
782. Move to where you would like to build VIS and GLU and unpack the
79   distributions:
80
81        % cd /home/vis                                  # for example
82        % gzip -dc /tmp/glu-2.1.tar.gz | tar xf -
83        % gzip -dc /tmp/vis-2.1.tar.gz | tar xf -
84
853. Move into the glu-2.1 directory and run configure, which will
86   determine some system-specific parameters and create the Makefile:
87
88        % cd glu-2.1
89        % ./configure
90
91   By default, this will use your system's native compiler.  To use gcc,
92
93        % ./configure --enable-gcc
94
95   (You may want to do this because you don't have the native compiler
96   installed or because it is not ANSI.)
97
98   Note: For platforms where VIS is not supported for the native compiler,
99   the default compiler is set to gcc.
100
101   Note: Not all checks in ./configure will return "yes."  This is
102   normal and should not affect compilation.  However, do be concerned
103   with any warnings "configure" produces.
104
105   Note: Occasionally, configure will make a bad guess or will choose
106   a default you do not want.  In this case, simply edit the Makefile
107   after configure finishes.
108
109   Note: You may want to specify parameters to configure -- see the
110   "Installing" sections below.
111
112   Note: To parallelize the installation procedure, you can begin steps
113   5 and 6 at this point, as long as step 4 completes before step 6
114   (since VIS must link against the GLU library).
115
116   Note: The Makefile by default uses the "-g" option for
117   compilation.  The resultant "vis" executable may be much larger than
118   the executable generated without using the "-g" option.  Using the
119   "-g" option however, provides debugging capabilities.
120
121   Note: The following is of interest only to people developing code
122   within vis.  For full debugging support, specify
123   --with-comp-mode=debug.  This will turn off optimization, and turn
124   on the assertions (sanity checks) in the code.  Similarly,
125   --with-comp-mode=purify and --with-comp-mode=quantify will link vis
126   with IBM Rational's Purify or Quantify tool, if it is installed.
127
1284. Build the GLU system by running GNU's gmake utility:
129
130        % gmake
131
132   You may not have GNU make installed on your system under the name
133   'gmake' -- try make.  If this fails, you probably need the latest
134   version of GNU's make program -- download it from the address
135   above.
136
1375. Move into the vis-2.1 directory and run configure:
138
139        % cd ../vis-2.1
140        % ./configure
141
142   By default, this will use your system's native compiler.  To use gcc,
143 
144        % ./configure --enable-gcc
145
146   (You may wish to do this because you don't have the native compiler 
147   installed or because it is not ANSI.)
148
149   Note: For platforms where VIS is not supported for the native compiler,
150   the default compiler is set to gcc.
151
152   Note: If you supplied compilation-option flags (e.g., --enable-64)
153   to the GLU configure, provide the same to the VIS configure.
154 
155   Note: Not all checks in ./configure will return "yes."  This is
156   normal and should not affect compilation.  However, do be concerned
157   with any warnings "configure" produces.
158
159   Note: Occasionally, configure will make a bad guess or will choose
160   a default you do not want.  In this case, simply edit the Makefile
161   after configure finishes.
162
163   Note: You may want to specify parameters to configure -- see the
164   "Installing" sections below.
165
166   Note: You may want to remove the "-g" flag from the make file.  See
167   under 3.
168
1696. Build the VIS system by running GNU's gmake utility:
170
171        % gmake
172
173   This builds an executable "vis" in the current directory.
174
175   WARNING: If you are not successful in building a VIS executable,
176   double check that you are using Flex version 2.5 or greater (check
177   using "flex -V") and GNU Bison version 1.22 or greater (check with
178   "bison -V").  Having out-of-date versions of these programs can
179   lead to obscure compilation and linking errors.  You can download
180   the new versions from the GNU FTP address above.
181
182   VIS expects to find master.visrc, two .nawk files, and a directory
183   of help files in the directory given by the environment variable
184   VIS_LIBRARY_PATH.  Set this to the "share" directory in the source
185   tree:
186
187        % setenv VIS_LIBRARY_PATH $cwd/share
188
1897. OPTIONAL: Verify VIS works by running it on some of the examples
190   included in the distribution:
191
192        % gmake check
193
194   This step finishes in less than five minutes on most machines
195   and requires approximately 32MB of RAM.
196
197---------------------------------------------------------------------------
198* Installing GLU:
199
200Developers will want to install the GLU library and its associated header
201files in a central area:
202
203To install the GLU library and its header files, type, while in the
204glu-2.1 directory,
205
206        % gmake install
207
208By default, this will put libraries and headers in /usr/local/lib
209and /usr/local/include respectively.  To choose a different
210location, provide a default prefix when you invoke configure, e.g.,
211to install in /projects/glu/bin, etc., use
212
213        % ./configure --prefix=/projects/glu
214
215when configuring GLU.  Note that "tilde expansion" doesn't work for the 
216prefix (i.e., don't specify --prefix=~smith/glu).
217
218---------------------------------------------------------------------------
219* Installing VIS:
220
221Administrators and people who want to discard the source files after
222building VIS may install VIS in a central area:
223
224To install the VIS executable, library, headers, and help files, type,
225while in the vis-2.1 directory,
226
227        % gmake install
228
229By default, this will put binaries, libraries, headers, and help files
230in /usr/local/bin, /usr/local/lib, /usr/local/include, and
231/usr/local/share respectively.  To choose a different location,
232provide a default prefix when you invoke configure, e.g., to install
233in /projects/vis/bin, etc., use
234
235        % ./configure --prefix=/projects/vis
236
237when configuring VIS.
238
239"gmake clean" removes all the files generated during "gmake."  This is
240useful when you want to rebuild VIS with a different prefix,
241different compiler options, etc.
242
243During configure if --prefix option is used, files found in the
244"share" directory will be installed in $prefix/share/vis; otherwise
245they will be installed in /usr/local/share/vis by default.  Set the
246environment variable "VIS_LIBRARY_PATH" to the appropriate directory so
247that VIS can find master.visrc, the two .nawk files and the "help"
248directory.  The above mentioned files can also be present in a
249different directory, but "VIS_LIBRARY_PATH" should be set to that
250directory.  For example,
251
252        % setenv VIS_LIBRARY_PATH /projects/vis/common
253
254---------------------------------------------------------------------------
255* Installation for multiple platforms
256
257To install VIS on multiple operating systems depending on the same
258source tree, see the file "INSTALL" included in the distribution.
259
260In this case, when the build directory is different from the source
261directory, it's necessary to configure VIS to look elsewhere for the
262GLU libraries and headers, e.g.,
263
264        % ./configure --with-glu-libdir=/tmp/glu-2.1/alpha \
265                --with-glu-incdir=/tmp/glu-2.1/include
266
267Also, make sure that there is an obj/ directory in the directory in
268which you are compiling.  See ./configure --help for more information.
269
270---------------------------------------------------------------------------
271* Selecting a different BDD package
272
273To create VIS with a different BDD library (say cal) than the default
274one (cu), use the following command:
275
276        %./configure --with-bdd=cal
277
278The same can be achieved by changing the "BDDPKG" definition in the
279Makefile from "cu" to "cal".
280
281VIS can work with three different BDD packages (cmu, cal, cu), all of
282which are supplied with glu-2.1.  However, some commands in VIS are
283available only with the cu BDD package.  Please refer to the NEWS file
284for more details.
285
286---------------------------------------------------------------------------
287To create three versions of VIS, each with different BDD libraries,
288run 'gmake allprods'.  This will create vis-cal, vis-cu, and
289vis-cmu.  To verify whether all these executables are compiled
290correctly, use 'gmake check-allprods' at the end.
291---------------------------------------------------------------------------
292
293* Files in the VIS distribution:
294
295README          This file.
296
297INSTALL         Generic installation instructions for use with configure,
298                including instructions for simultaneous multi-platform
299                builds.  These are not specific to VIS nor GLU, so don't
300                follow them word for word.
301
302NEWS            Changes since the last version/release.
303
304configure       An executable shell script that creates "Makefile" from
305                Makefile.in after determining system-specific parameters.
306
307configure.in    Autoconf source for generating the configure file.
308                Only needed if you want to modify the configure script.
309
310Makefile.in     The template Makefile.
311
312vis.1           Unix-style man page documenting vis invocation
313                parameters.
314
315xsimv           An expectk script to visualize VIS simulation traces.
316
317helpers/        Programs useful during configuration and building
318 install-sh     Shell scripts used by "gmake install."
319 mkinstalldirs
320 config.guess
321 config.sub
322 dependency.make
323
324doc/vis_user.ps
325                A user's manual for the VIS system, describing our approach
326                to formal verification and how to use the tool.
327
328doc/blifmv.ps   Documentation on the BLIF-MV file format, a low-level
329                language for specifying designs.
330
331doc/ctl.ps      Documentation on the CTL file format, a language
332                for specifying properties.
333
334examples/*/     A collection of small systems and properties to be
335                verified.  Used by "gmake check."
336
337share/master.visrc
338                A VIS script designed to be run automatically at
339                start-up: contains aliases for commonly used commands
340                and some default parameter settings.
341
342share/*.nawk    nawk scripts for converting BLIF files to BLIF-MV,
343                used by the "read_blif" command.
344
345share/script*   Sample scripts.
346
347share/sislib.mv Library of gates used by models translated by vl2mv
348                from gate-level Verilog descriptions.
349
350share/visdbgpp  A perl script to pretty-print counterexamples produced
351                by the model_check and check_invariant commands.
352
353share/help/     ASCII documentation for each VIS command, accessible
354                through the "help" command within VIS.
355
356src/*/          Source code and headers for the VIS system.
357
358obj/            Directory where .o files and generated .c files are
359                placed during a build.
360
361checkresults/   Directory where tests (i.e., gmake check) are run.
362                Results of the tests are placed here.  The directory
363                is only created when 'gmake check' is run.
364
365---------------------------------------------------------------------------
366* Platform Specific Instructions
367
368Note: some instructions apply to platforms we no longer support.
369
370** Little-endian machines:
371
372  vis-cal will occasionally fail when compiled with
373  --with-comp-mode=debug on little-endian machines like the Alphas and
374  the Intel ix86 CPUs.
375
376** DEC Alpha:
377
378  Warnings about MIN and MAX are harmless.
379  Warnings about Olimit are harmless.  They can be gotten rid of by
380  increasing the number following Olimit under CFLAGS.
381
382  By default, configure uses 32-bit pointers when using DEC's OSF/1 C
383  compiler for the Alpha, which is more efficient if your processes
384  use less than 2GB.  To use 64-bit pointers, invoke configure as follows:
385
386        % ./configure --enable-64
387
388  The gcc compiler always compiles with 64-bit pointers.
389
390  Note that you must also specify this flag when configuring GLU.
391
392  Some machines do not have the program 'om'.  In this case, simply
393  removing the om flag from LDFLAGS is sufficient to complete
394  compilation.
395
396** Intel A64:
397
398  vis-cal compiled with gcc 3.2.3 crashes when sifting is invoked.
399
400** Solaris (Sparc and ix86):
401
402  If Sun's C compiler is not installed on your system, use gcc
403  (./configure --enable-gcc).
404
405  Warnings about redefined symbol are harmless, so are the warnings
406  that say "end-of-loop code not reached".
407
408  The sun cc compiler (Workshop 6 update 1) on ix86 appears to have a
409  bug in the optimization routines.  The -xO4 an -xO5 compiler options
410  will make vis crash in some runs.  As a safety precaution, we have
411  changed the optimization flag to be -xO3 for all Sun platforms that
412  use the cc compiler.  You can try higher optimization flags on your
413  machine.  In general, it is hard to determine cc options that will
414  give optimal results on every platform, so it may pay off to play
415  atound with the optimization options.
416
417** HP-UX:
418
419  Some operating systems on HP machines have a built-in command called
420  "vis" under /usr/ucb.  In light of this, be careful about the
421  definition of your  path.
422
423** MS Windows with Cygwin:
424
425  You need Red Hat's Cygwin environment (freely available from
426  http://www.cygwin.com) to build GLU and VIS.
427
428  With Cygwin the configuration script automatically selects gcc.
429
430** AIX:
431 
432  The configuration script automatically selects gcc.  vis-cal
433  occasionally produces incorrect results when optimization is turned
434  on.  If you plan to use vis-cal with AIX, you should configure glu
435  and vis with --with-comp-mode=debug.
436
437** IRIX
438
439  When compiling VIS with gcc, you may get the error message
440
441  gcc.x: cannot specify -o with -c or -S and multiple compilations
442
443  If this happens, edit Makefile, and replace the definition of
444  VERDATE with the following:
445
446  VERDATE := -DCUR_DATE="\"N/A\"" -DCUR_VER="\"$(PRODUCT)-$(VERSION)\""
447
448---------------------------------------------------------------------------
449* Verilog front-end
450
451vl2mv, written by Szu-Tsung Cheng, allows one to translate a subset of
452Verilog into blif-MV, the input format of VIS.  The most recent
453version of vl2mv can be found in ftp://vlsi.colorado.edu/pub/vl2mv-2.1.tar.gz.
454This version requires glu-2.1 to compile and link.
Note: See TracBrowser for help on using the repository browser.