source: vis_dev/vis-2.1/examples/ping_pong/README @ 15

Last change on this file since 15 was 11, checked in by cecile, 13 years ago

Add vis

File size: 1.1 KB
Line 
1This directory has the verilog and pif files that are consistent
2with the tutorial on ping_pong. So this directory should be put in
3the examples directory for regression testing.
4
5For the language containment test on properties never_no_balls and
6infinitely_often_hit, these have been put into ping_pong.v as
7monitors. Without their fairness constraints, they have no effect
8(except for expanding the state space). It turns out that the ioh property
9cannot be expressed with just Buchi fairness constraints. So
10there are not special fairness constraints and the property is
11stated in terms of a CTL formula (prop2.ctl).
12
13The various commands  that should be run on it are:
14
15read_blif_mv ping_pong.mv
16init
17compute_reach -v 1
18# reachable # states is 5
19read_fairness prop1.fair
20compute_reach -v 1
21# reachable # states is still 5
22mc lang_empt.ctl
23#this should pass
24
25read_fairness ping_pong.fair
26mc prop2.ctl
27#this should pass
28
29mc lang_empt.ctl
30#this should fail
31 
32mc ping_pong.ctl
33# Both formulas should pass
34
35# now flush the fairness constraints.
36read_fairness all.fair
37mc ping_pong.ctl
38#The first one should pass and the last should fail
39
Note: See TracBrowser for help on using the repository browser.