Line | |
---|
1 | read_blif_mv dcnew.mv |
---|
2 | init_verify |
---|
3 | compute_reach -v 1 |
---|
4 | print_fairness |
---|
5 | lang_empty -d 0 |
---|
6 | model_check -d 0 affalse |
---|
7 | read_fairness prop.fair |
---|
8 | print_fairness |
---|
9 | lang_empty -d 0 |
---|
10 | reset_fairness |
---|
11 | print_fairness |
---|
12 | model_check -d 0 agtrue |
---|
13 | model_check -d 0 osc2.ctl |
---|
14 | model_check -d 0 osc3.ctl |
---|
15 | model_check -d 0 osc4.ctl |
---|
16 | model_check -d 0 osc5.ctl |
---|
17 | model_check -d 0 osc6.ctl |
---|
18 | model_check -d 0 safe.ctl |
---|
19 | model_check -d 0 safe1.ctl |
---|
20 | ltl_model_check -v1 -d1 dcnew.ltl |
---|
21 | model_check -d 0 -V dcnew.ctl |
---|
22 | time |
---|
23 | quit -s |
---|
Note: See
TracBrowser
for help on using the repository browser.