Line | |
---|
1 | # Script file for checking a set of CTL formula (no fairness |
---|
2 | # constraints, no debugging) |
---|
3 | |
---|
4 | # Author: Rajeev K. Ranjan |
---|
5 | |
---|
6 | # Usage: |
---|
7 | # After reading in the design using one of |
---|
8 | # "read_blif, read_blif_mv, or read_verilog" commands, |
---|
9 | # on VIS prompt type: |
---|
10 | # source script_model_check.simple <ctl_file> |
---|
11 | # |
---|
12 | # Trouble shooting: |
---|
13 | # i) Invoke the script exactly the way prescribed (no option to "source") |
---|
14 | # ii) The script tries to create a file in the current directory. Make sure |
---|
15 | # that the directory is writable by you. |
---|
16 | |
---|
17 | ### Script starts here ################################################# |
---|
18 | |
---|
19 | # Source the generic script |
---|
20 | |
---|
21 | source script_generic.simple |
---|
22 | |
---|
23 | # Invoke the model checking command. |
---|
24 | |
---|
25 | model_check -d 0 %:2 |
---|
Note: See
TracBrowser
for help on using the repository browser.