Skip to content

Commit d3071f4

Browse files
tautschnigtautschnig
authored
Merge pull request #434 from diffblue/smv_eventually
Verilog: vl2smv extensions
2 parents 132151e + d4d26c0 commit d3071f4

19 files changed

+471
-12
lines changed

‎regression/ebmc/assume1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
CORE
22
main.v
3-
--module main --bound 3 --aig
3+
--module main --bound 3 --aig --vl2smv-extensions
44
^EXIT=0$
55
^SIGNAL=0$

‎regression/verilog/vl2smv-extensions/README

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
From the Cadence SMV distribution, doc/smv/examples/vlog.

‎regression/verilog/vl2smv-extensions/traffic-1.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
traffic/1.v
3+
--vl2smv-extensions
4+
^file .* line 50: assignment in 'always' context without event guard$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--

‎regression/verilog/vl2smv-extensions/traffic-2.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
traffic/2.v
3+
--vl2smv-extensions
4+
^file .* line 50: assignment in 'always' context without event guard$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--

‎regression/verilog/vl2smv-extensions/traffic-3.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
traffic/3.v
3+
--vl2smv-extensions
4+
^file .* line 50: assignment in 'always' context without event guard$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--

‎regression/verilog/vl2smv-extensions/traffic/1.v

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,115 @@
1+
module main(N_SENSE,S_SENSE,E_SENSE,N_GO,S_GO,E_GO);
2+
3+
/*
4+
This program implements a traffic light controller.
5+
6+
Input signals:
7+
N_SENSE -
8+
When this goes high, a car from the north is waiting to cross the
9+
intersection. (This signal does not have to remain high until
10+
the request is granted.) Once the request has been granted, this
11+
signal goes low to indicate that the car has finished crossing
12+
the intersection.
13+
S_SENSE - Same as N, except for traffic from the south.
14+
E_SENSE - Same as N, except for traffic from the east.
15+
16+
Output signals:
17+
N_GO - If this signal is high, traffic from the north is permitted to
18+
enter the intersection. If it is low, traffic must wait.
19+
S_GO - Same as N_GO, except for traffic from the south.
20+
E_GO - Same as N_GO, except for traffic from the east.
21+
22+
Internal signals:
23+
N_REQ - Since N is not required to remain high to indicate that a
24+
car from the north wants to cross the intersection, this signal
25+
is used to latch requests from the north.
26+
S_REQ - Same as N_REQ, except for traffic from the south.
27+
E_REQ - Same as N_REQ, except for traffic from the east.
28+
NS_LOCK - This signal is set high by north/south traffic in order to
29+
lock out traffic from the east.
30+
EW_LOCK - This signal is set high by east traffic in order to
31+
lock out traffic from the north/south.
32+
*/
33+
34+
input N_SENSE, S_SENSE, E_SENSE;
35+
output N_GO, S_GO, E_GO;
36+
37+
wire N_SENSE, S_SENSE, E_SENSE;
38+
reg N_GO, S_GO, E_GO;
39+
reg NS_LOCK, EW_LOCK, N_REQ, S_REQ, E_REQ;
40+
41+
initial begin
42+
N_REQ = 0; S_REQ = 0; E_REQ = 0;
43+
N_GO = 0; S_GO = 0; E_GO = 0;
44+
NS_LOCK = 0; EW_LOCK = 0;
45+
end
46+
47+
48+
/* latch traffic sensor inputs */
49+
50+
always begin if (!N_REQ & N_SENSE) N_REQ = 1; end
51+
always begin if (!S_REQ & S_SENSE) S_REQ = 1; end
52+
always begin if (!E_REQ & E_SENSE) E_REQ = 1; end
53+
54+
/* North traffic controller */
55+
56+
always begin
57+
if (N_REQ)
58+
begin
59+
wait (!EW_LOCK);
60+
NS_LOCK = 1;
61+
N_GO = 1;
62+
wait (!N_SENSE);
63+
if (!S_GO) NS_LOCK = 0;
64+
N_GO = 0;
65+
N_REQ = 0;
66+
end
67+
end
68+
69+
/* South traffic controller */
70+
71+
always begin
72+
if (S_REQ)
73+
begin
74+
wait (!EW_LOCK);
75+
NS_LOCK = 1; S_GO = 1;
76+
wait (!S_SENSE);
77+
if (!N_GO) NS_LOCK = 0;
78+
S_GO = 0; S_REQ = 0;
79+
end
80+
end
81+
82+
/* East traffic controller */
83+
84+
always begin
85+
if (E_REQ)
86+
begin
87+
EW_LOCK = 1;
88+
wait (!NS_LOCK);
89+
E_GO = 1;
90+
wait (!E_SENSE);
91+
EW_LOCK = 0; E_GO = 0; E_REQ = 0;
92+
end
93+
end
94+
95+
/* specifications */
96+
97+
always begin
98+
assert mutex: !(E_GO & (S_GO | N_GO));
99+
if (E_SENSE) assert E_live: eventually E_GO;
100+
if (S_SENSE) assert S_live: eventually S_GO;
101+
if (N_SENSE) assert N_live: eventually N_GO;
102+
end
103+
104+
/* assumptions */
105+
106+
always begin
107+
assert E_fair: eventually !(E_GO & E_SENSE);
108+
assert S_fair: eventually !(S_GO & S_SENSE);
109+
assert N_fair: eventually !(N_GO & N_SENSE);
110+
end
111+
112+
using E_fair, S_fair, N_fair prove E_live, S_live, N_live;
113+
assume E_fair, S_fair, N_fair;
114+
115+
endmodule

‎regression/verilog/vl2smv-extensions/traffic/2.v

Lines changed: 116 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
module main(N_SENSE,S_SENSE,E_SENSE,N_GO,S_GO,E_GO);
2+
3+
/*
4+
This program implements a traffic light controller.
5+
6+
Input signals:
7+
N_SENSE -
8+
When this goes high, a car from the north is waiting to cross the
9+
intersection. (This signal does not have to remain high until
10+
the request is granted.) Once the request has been granted, this
11+
signal goes low to indicate that the car has finished crossing
12+
the intersection.
13+
S_SENSE - Same as N, except for traffic from the south.
14+
E_SENSE - Same as N, except for traffic from the east.
15+
16+
Output signals:
17+
N_GO - If this signal is high, traffic from the north is permitted to
18+
enter the intersection. If it is low, traffic must wait.
19+
S_GO - Same as N_GO, except for traffic from the south.
20+
E_GO - Same as N_GO, except for traffic from the east.
21+
22+
Internal signals:
23+
N_REQ - Since N is not required to remain high to indicate that a
24+
car from the north wants to cross the intersection, this signal
25+
is used to latch requests from the north.
26+
S_REQ - Same as N_REQ, except for traffic from the south.
27+
E_REQ - Same as N_REQ, except for traffic from the east.
28+
NS_LOCK - This signal is set high by north/south traffic in order to
29+
lock out traffic from the east.
30+
EW_LOCK - This signal is set high by east traffic in order to
31+
lock out traffic from the north/south.
32+
*/
33+
34+
input N_SENSE, S_SENSE, E_SENSE;
35+
output N_GO, S_GO, E_GO;
36+
37+
wire N_SENSE, S_SENSE, E_SENSE;
38+
reg N_GO, S_GO, E_GO;
39+
reg NS_LOCK, EW_LOCK, N_REQ, S_REQ, E_REQ;
40+
41+
initial begin
42+
N_REQ = 0; S_REQ = 0; E_REQ = 0;
43+
N_GO = 0; S_GO = 0; E_GO = 0;
44+
NS_LOCK = 0; EW_LOCK = 0;
45+
end
46+
47+
48+
/* latch traffic sensor inputs */
49+
50+
always begin if (!N_REQ & N_SENSE) N_REQ = 1; end
51+
always begin if (!S_REQ & S_SENSE) S_REQ = 1; end
52+
always begin if (!E_REQ & E_SENSE) E_REQ = 1; end
53+
54+
/* North traffic controller */
55+
56+
always begin
57+
if (N_REQ)
58+
begin
59+
wait (!EW_LOCK & !(S_GO & !S_SENSE));
60+
NS_LOCK = 1;
61+
N_GO = 1;
62+
wait (!N_SENSE);
63+
if (!S_GO) NS_LOCK = 0;
64+
N_GO = 0;
65+
N_REQ = 0;
66+
end
67+
end
68+
69+
/* South traffic controller */
70+
71+
always begin
72+
if (S_REQ)
73+
begin
74+
wait (!EW_LOCK & !(N_GO & !N_SENSE));
75+
NS_LOCK = 1; S_GO = 1;
76+
wait (!S_SENSE);
77+
if (!N_GO) NS_LOCK = 0;
78+
S_GO = 0; S_REQ = 0;
79+
end
80+
end
81+
82+
/* East traffic controller */
83+
84+
always begin
85+
if (E_REQ)
86+
begin
87+
EW_LOCK = 1;
88+
wait (!NS_LOCK);
89+
E_GO = 1;
90+
wait (!E_SENSE);
91+
EW_LOCK = 0; E_GO = 0; E_REQ = 0;
92+
end
93+
end
94+
95+
/* specifications */
96+
97+
always begin
98+
assert mutex: !(E_GO & (S_GO | N_GO));
99+
if (E_SENSE) assert E_live: eventually E_GO;
100+
if (S_SENSE) assert S_live: eventually S_GO;
101+
if (N_SENSE) assert N_live: eventually N_GO;
102+
end
103+
104+
/* assumptions */
105+
106+
always begin
107+
assert E_fair: eventually !(E_GO & E_SENSE);
108+
assert S_fair: eventually !(S_GO & S_SENSE);
109+
assert N_fair: eventually !(N_GO & N_SENSE);
110+
end
111+
112+
using E_fair, S_fair, N_fair prove E_live, S_live, N_live;
113+
assume E_fair, S_fair, N_fair;
114+
115+
116+
endmodule

‎regression/verilog/vl2smv-extensions/traffic/3.v

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
module main(N_SENSE,S_SENSE,E_SENSE,N_GO,S_GO,E_GO);
2+
3+
/*
4+
This program implements a traffic light controller.
5+
6+
Input signals:
7+
N_SENSE -
8+
When this goes high, a car from the north is waiting to cross the
9+
intersection. (This signal does not have to remain high until
10+
the request is granted.) Once the request has been granted, this
11+
signal goes low to indicate that the car has finished crossing
12+
the intersection.
13+
S_SENSE - Same as N, except for traffic from the south.
14+
E_SENSE - Same as N, except for traffic from the east.
15+
16+
Output signals:
17+
N_GO - If this signal is high, traffic from the north is permitted to
18+
enter the intersection. If it is low, traffic must wait.
19+
S_GO - Same as N_GO, except for traffic from the south.
20+
E_GO - Same as N_GO, except for traffic from the east.
21+
22+
Internal signals:
23+
N_REQ - Since N is not required to remain high to indicate that a
24+
car from the north wants to cross the intersection, this signal
25+
is used to latch requests from the north.
26+
S_REQ - Same as N_REQ, except for traffic from the south.
27+
E_REQ - Same as N_REQ, except for traffic from the east.
28+
NS_LOCK - This signal is set high by north/south traffic in order to
29+
lock out traffic from the east.
30+
EW_LOCK - This signal is set high by east traffic in order to
31+
lock out traffic from the north/south.
32+
*/
33+
34+
input N_SENSE, S_SENSE, E_SENSE;
35+
output N_GO, S_GO, E_GO;
36+
37+
wire N_SENSE, S_SENSE, E_SENSE;
38+
reg N_GO, S_GO, E_GO;
39+
reg NS_LOCK, EW_LOCK, N_REQ, S_REQ, E_REQ;
40+
41+
initial begin
42+
N_REQ = 0; S_REQ = 0; E_REQ = 0;
43+
N_GO = 0; S_GO = 0; E_GO = 0;
44+
NS_LOCK = 0; EW_LOCK = 0;
45+
end
46+
47+
48+
/* latch traffic sensor inputs */
49+
50+
always begin if (!N_REQ & N_SENSE) N_REQ = 1; end
51+
always begin if (!S_REQ & S_SENSE) S_REQ = 1; end
52+
always begin if (!E_REQ & E_SENSE) E_REQ = 1; end
53+
54+
/* North traffic controller */
55+
56+
always begin
57+
if (N_REQ)
58+
begin
59+
wait (!EW_LOCK & !(S_GO & !S_SENSE));
60+
NS_LOCK = 1; N_GO = 1;
61+
wait (!N_SENSE);
62+
if (!S_GO | !S_SENSE) NS_LOCK = 0;
63+
N_GO = 0; N_REQ = 0;
64+
end
65+
end
66+
67+
/* South traffic controller */
68+
69+
always begin
70+
if (S_REQ)
71+
begin
72+
wait (!EW_LOCK & !(N_GO & !N_SENSE));
73+
NS_LOCK = 1; S_GO = 1;
74+
wait (!S_SENSE);
75+
if (!N_GO | !N_SENSE) NS_LOCK = 0;
76+
S_GO = 0; S_REQ = 0;
77+
end
78+
end
79+
80+
/* East traffic controller */
81+
82+
always begin
83+
if (E_REQ)
84+
begin
85+
EW_LOCK = 1;
86+
wait (!NS_LOCK);
87+
E_GO = 1;
88+
wait (!E_SENSE);
89+
EW_LOCK = 0; E_GO = 0; E_REQ = 0;
90+
end
91+
end
92+
93+
/* specifications */
94+
95+
always begin
96+
assert mutex: !(E_GO & (S_GO | N_GO));
97+
if (E_SENSE) assert E_live: eventually E_GO;
98+
if (S_SENSE) assert S_live: eventually S_GO;
99+
if (N_SENSE) assert N_live: eventually N_GO;
100+
end
101+
102+
/* assumptions */
103+
104+
always begin
105+
assert E_fair: eventually !(E_GO & E_SENSE);
106+
assert S_fair: eventually !(S_GO & S_SENSE);
107+
assert N_fair: eventually !(N_GO & N_SENSE);
108+
end
109+
110+
using E_fair, S_fair, N_fair prove E_live, S_live, N_live;
111+
assume E_fair, S_fair, N_fair;
112+
113+
114+
endmodule

‎src/ebmc/ebmc_parse_options.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ class ebmc_parse_optionst:public parse_options_baset
4646
"(random-traces)(trace-steps):(random-seed):(number-of-traces):"
4747
"(random-trace)(random-waveform)"
4848
"(liveness-to-safety)"
49-
"I:(preprocess)(systemverilog)",
49+
"I:(preprocess)(systemverilog)(vl2smv-extensions)",
5050
argc,
5151
argv,
5252
std::string("EBMC ") + EBMC_VERSION),

0 commit comments

Comments
 (0)