.\" $Id: vis.1,v 1.3 2001/04/13 20:45:04 rbloem Exp $
.\"
.TH vis 1 "April 11, 2001" "Release 1.4"
.LO 1
.SH NAME
Vis \- Verification Interacting with Synthesis
.SH SYNOPSIS
.B vis  
[\-c cmd] [\-f 
.I script
] [\-h] [\-o 
.I file
] [\-s] [\-t type] [\-T type] [\-x] [
.I file
]
.SH DESCRIPTION
.B Vis
is a system for formal verification, synthesis, and simulation of finite state
systems. It has been developed jointly at the University of California at
Berkeley and the University of Colorado at Boulder.
.PP
Vis is primarily used interactively, using a prompt system.  Most help on its
commands is given within vis: type
.B help 
at the vis command prompt.  The 
.I examples 
directory gives some examples of how
to use vis.  The definitive documentation resides at the Vis Home Page.  This
man page concentrates on the command options.
.PP
Vis works interactively if invoked without any options.  Vis can also be called
in batch mode, using 
.B -c 
or
.B -f.
In this case, either 
.B -x
needs to be specified, or the last argument needs to denote a file. 
.PP
The case in which 
.B -x 
is not specified is only used in practice for synthesis.
.I File
is read before the script is executed, and after execution another file is
written.  The details are determined by the
.B -t, -T, 
and
.B -o
flags.  It is probably easier to incorporate the reading and writing
of the file in the script.
.SH OPTIONS
.TP
.B  \-\^c cmd 
 Execute VIS commands `cmd'.
.TP
.BR  "\-\^f " file
Execute script containing vis commands
.TP
.B  \-\^h          
Print the command usage
.TP 
.BR "-\^o  " file
Specify output filename (default is -)
.TP
.B \-\^s 
Do not read any initialization file.  If not specified, the files 
.I $VIS_LIBRARY_PATH/master.visrc, 
and 
.I $HOME/.visrc
are executed in that order.
.TP 
.B \-\^t type
 specify input type (blif_mv (default), blif, or none)
.TP
.B \-\^x
Equivalent to '-t none -T none'
.\"
.SH EXAMPLES
.TP
.B vis\^
Calls vis interactively
.TP
.BI "vis -x -f " file\^
Executes the named vis script.
.\"
.SH FILES
The scripts
.I $VIS_LIBRARY_PATH/master.visrc, 
and 
.I $HOME/.visrc
are read in that order before any other script executes.  They are used to
define aliases and the like.
.\"
.SH ENVIRONMENT
.B $VIS_LIBRARY_PATH
determines the location of the master visrc file and the help files.
.\"
.SH NOTES
Vis will produce line-buffered output if you set vis_stdout and
vis_stderr from the vis prompt.  In any case, you can force vis to
flush the output by sending it a USR1 signal, using kill.
.\"
.SH BUGS
For optimum performance, set the 
.B datasize limit 
to a reasonable size (such as something less than the amount of RAM
you have).
.\"
.SH "SEE ALSO"
The Vis Home Page: 
.UR http://vlsi.colorado.edu/~vis
http://vlsi.colorado.edu/~vis
.UE
.PP
R. K. Brayton et al, 
.I VIS:  A system for verification and synthesis, 
Eighth Conference on Computer Aided Verification (CAV'96), pp. 428-432, 1996.
.PP
.BR limit (1),
.BR kill(1).