source: vis_dev/vis-2.3/README @ 16

Last change on this file since 16 was 14, checked in by cecile, 13 years ago

vis2.3

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