| [11] | 1 | .\" $Id: vis.1,v 1.3 2001/04/13 20:45:04 rbloem Exp $ |
|---|
| 2 | .\" |
|---|
| 3 | .TH vis 1 "April 11, 2001" "Release 1.4" |
|---|
| 4 | .LO 1 |
|---|
| 5 | .SH NAME |
|---|
| 6 | Vis \- Verification Interacting with Synthesis |
|---|
| 7 | .SH SYNOPSIS |
|---|
| 8 | .B vis |
|---|
| 9 | [\-c cmd] [\-f |
|---|
| 10 | .I script |
|---|
| 11 | ] [\-h] [\-o |
|---|
| 12 | .I file |
|---|
| 13 | ] [\-s] [\-t type] [\-T type] [\-x] [ |
|---|
| 14 | .I file |
|---|
| 15 | ] |
|---|
| 16 | .SH DESCRIPTION |
|---|
| 17 | .B Vis |
|---|
| 18 | is a system for formal verification, synthesis, and simulation of finite state |
|---|
| 19 | systems. It has been developed jointly at the University of California at |
|---|
| 20 | Berkeley and the University of Colorado at Boulder. |
|---|
| 21 | .PP |
|---|
| 22 | Vis is primarily used interactively, using a prompt system. Most help on its |
|---|
| 23 | commands is given within vis: type |
|---|
| 24 | .B help |
|---|
| 25 | at the vis command prompt. The |
|---|
| 26 | .I examples |
|---|
| 27 | directory gives some examples of how |
|---|
| 28 | to use vis. The definitive documentation resides at the Vis Home Page. This |
|---|
| 29 | man page concentrates on the command options. |
|---|
| 30 | .PP |
|---|
| 31 | Vis works interactively if invoked without any options. Vis can also be called |
|---|
| 32 | in batch mode, using |
|---|
| 33 | .B -c |
|---|
| 34 | or |
|---|
| 35 | .B -f. |
|---|
| 36 | In this case, either |
|---|
| 37 | .B -x |
|---|
| 38 | needs to be specified, or the last argument needs to denote a file. |
|---|
| 39 | .PP |
|---|
| 40 | The case in which |
|---|
| 41 | .B -x |
|---|
| 42 | is not specified is only used in practice for synthesis. |
|---|
| 43 | .I File |
|---|
| 44 | is read before the script is executed, and after execution another file is |
|---|
| 45 | written. The details are determined by the |
|---|
| 46 | .B -t, -T, |
|---|
| 47 | and |
|---|
| 48 | .B -o |
|---|
| 49 | flags. It is probably easier to incorporate the reading and writing |
|---|
| 50 | of the file in the script. |
|---|
| 51 | .SH OPTIONS |
|---|
| 52 | .TP |
|---|
| 53 | .B \-\^c cmd |
|---|
| 54 | Execute VIS commands `cmd'. |
|---|
| 55 | .TP |
|---|
| 56 | .BR "\-\^f " file |
|---|
| 57 | Execute script containing vis commands |
|---|
| 58 | .TP |
|---|
| 59 | .B \-\^h |
|---|
| 60 | Print the command usage |
|---|
| 61 | .TP |
|---|
| 62 | .BR "-\^o " file |
|---|
| 63 | Specify output filename (default is -) |
|---|
| 64 | .TP |
|---|
| 65 | .B \-\^s |
|---|
| 66 | Do not read any initialization file. If not specified, the files |
|---|
| 67 | .I $VIS_LIBRARY_PATH/master.visrc, |
|---|
| 68 | and |
|---|
| 69 | .I $HOME/.visrc |
|---|
| 70 | are executed in that order. |
|---|
| 71 | .TP |
|---|
| 72 | .B \-\^t type |
|---|
| 73 | specify input type (blif_mv (default), blif, or none) |
|---|
| 74 | .TP |
|---|
| 75 | .B \-\^x |
|---|
| 76 | Equivalent to '-t none -T none' |
|---|
| 77 | .\" |
|---|
| 78 | .SH EXAMPLES |
|---|
| 79 | .TP |
|---|
| 80 | .B vis\^ |
|---|
| 81 | Calls vis interactively |
|---|
| 82 | .TP |
|---|
| 83 | .BI "vis -x -f " file\^ |
|---|
| 84 | Executes the named vis script. |
|---|
| 85 | .\" |
|---|
| 86 | .SH FILES |
|---|
| 87 | The scripts |
|---|
| 88 | .I $VIS_LIBRARY_PATH/master.visrc, |
|---|
| 89 | and |
|---|
| 90 | .I $HOME/.visrc |
|---|
| 91 | are read in that order before any other script executes. They are used to |
|---|
| 92 | define aliases and the like. |
|---|
| 93 | .\" |
|---|
| 94 | .SH ENVIRONMENT |
|---|
| 95 | .B $VIS_LIBRARY_PATH |
|---|
| 96 | determines the location of the master visrc file and the help files. |
|---|
| 97 | .\" |
|---|
| 98 | .SH NOTES |
|---|
| 99 | Vis will produce line-buffered output if you set vis_stdout and |
|---|
| 100 | vis_stderr from the vis prompt. In any case, you can force vis to |
|---|
| 101 | flush the output by sending it a USR1 signal, using kill. |
|---|
| 102 | .\" |
|---|
| 103 | .SH BUGS |
|---|
| 104 | For optimum performance, set the |
|---|
| 105 | .B datasize limit |
|---|
| 106 | to a reasonable size (such as something less than the amount of RAM |
|---|
| 107 | you have). |
|---|
| 108 | .\" |
|---|
| 109 | .SH "SEE ALSO" |
|---|
| 110 | The Vis Home Page: |
|---|
| 111 | .UR http://vlsi.colorado.edu/~vis |
|---|
| 112 | http://vlsi.colorado.edu/~vis |
|---|
| 113 | .UE |
|---|
| 114 | .PP |
|---|
| 115 | R. K. Brayton et al, |
|---|
| 116 | .I VIS: A system for verification and synthesis, |
|---|
| 117 | Eighth Conference on Computer Aided Verification (CAV'96), pp. 428-432, 1996. |
|---|
| 118 | .PP |
|---|
| 119 | .BR limit (1), |
|---|
| 120 | .BR kill(1). |
|---|
| 121 | |
|---|