Skip to content

Commit a363d90

Browse files
kroeningkroening
authored
Merge pull request #758 from diffblue/SVA-sequence-misc
SVA: add eight sequence operators to Verilog Frontend
2 parents 90eb3c7 + 2992b87 commit a363d90

12 files changed

+175
-54
lines changed

‎regression/verilog/SVA/sequence_first_match1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
sequence_first_match1.sv
33

4-
^file .* line \d+: no support for 'first_match'$
5-
^EXIT=2$
4+
^\[.*\] first_match\(main\.x == 0\): FAILURE: property not supported by BMC engine$
5+
^EXIT=10$
66
^SIGNAL=0$
77
--
88
^warning: ignoring

‎regression/verilog/SVA/sequence_intersect1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
sequence_intersect1.sv
33

4-
^file .* line \d+: no support for 'intersect'$
5-
^EXIT=2$
4+
^\[.*\] main\.x == 0 intersect main\.x == 1: FAILURE: property not supported by BMC engine$
5+
^EXIT=10$
66
^SIGNAL=0$
77
--
88
^warning: ignoring

‎regression/verilog/SVA/sequence_repetition1.desc

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,12 @@
1-
KNOWNBUG
1+
CORE
22
sequence_repetition1.sv
33
--bound 10
4+
^\[.*\] 1 \[\*\] main\.half_x == 0: FAILURE: property not supported by BMC engine$
5+
^\[.*\] 1 \[->\] main\.half_x == 0: FAILURE: property not supported by BMC engine$
6+
^\[.*\] 1 \[=\] main\.half_x == 0: FAILURE: property not supported by BMC engine$
7+
^\[.*\] 1 \[\*\] main\.x == 0: FAILURE: property not supported by BMC engine$
8+
^\[.*\] 1 \[->\] main\.x == 0: FAILURE: property not supported by BMC engine$
9+
^\[.*\] 1 \[=\] main\.x == 0: FAILURE: property not supported by BMC engine$
410
^EXIT=10$
511
^SIGNAL=0$
612
--

‎regression/verilog/SVA/sequence_repetition2.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
sequence_repetition2.sv
3+
--bound 10
4+
^\[main\.p0\] main\.x == 0\[\*\]: FAILURE: property not supported by BMC engine$
5+
^\[main\.p1\] main\.x == 1\[\*\]: FAILURE: property not supported by BMC engine$
6+
^\[main\.p2\] \(main\.x == 0\[\+\]\) #-# main\.x == 1: FAILURE: property not supported by BMC engine$
7+
^\[main\.p3\] main\.x == 0\[\+\]: FAILURE: property not supported by BMC engine$
8+
^\[main\.p4\] main\.half_x == 0\[\*\]: FAILURE: property not supported by BMC engine$
9+
^\[main\.p5\] main\.x == 1\[\+\]: FAILURE: property not supported by BMC engine$
10+
^\[main\.p6\] \(main\.x == 0\[\+\]\) #=# main\.x == 1: FAILURE: property not supported by BMC engine$
11+
^EXIT=10$
12+
^SIGNAL=0$
13+
--
14+
^warning: ignoring
15+
--

‎regression/verilog/SVA/sequence_repetition2.sv

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
module main(input clk);
2+
3+
reg [31:0] x = 0;
4+
5+
// 0 1 2 3 4 ...
6+
always_ff @(posedge clk)
7+
x<=x+1;
8+
9+
// 0 0 1 1 2 2 3 3 ...
10+
wire [31:0] half_x = x/2;
11+
12+
// should pass
13+
initial p0: assert property (x==0[*]);
14+
initial p1: assert property (x==1[*]);
15+
initial p2: assert property (x==0[+] #-# x==1);
16+
initial p3: assert property (x==0[+]);
17+
initial p4: assert property (half_x==0[*]);
18+
19+
// should fail
20+
initial p5: assert property (x==1[+]);
21+
initial p6: assert property (x==0[+] #=# x==1);
22+
23+
endmodule

‎regression/verilog/SVA/sequence_throughout1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
sequence_throughout1.sv
33

4-
^file .* line \d+: no support for 'throughout'$
5-
^EXIT=2$
4+
^\[.*\] main\.x == 0 throughout main\.x == 1: FAILURE: property not supported by BMC engine$
5+
^EXIT=10$
66
^SIGNAL=0$
77
--
88
^warning: ignoring

‎regression/verilog/SVA/sequence_within1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
sequence_within1.sv
33

4-
^file .* line \d+: no support for 'within'$
5-
^EXIT=2$
4+
^\[.*\] main\.x == 0 within main\.x == 1: FAILURE: property not supported by BMC engine$
5+
^EXIT=10$
66
^SIGNAL=0$
77
--
88
^warning: ignoring

‎src/temporal-logic/temporal_logic.cpp

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,12 @@ bool is_SVA_sequence(const exprt &expr)
7474
id == ID_sva_non_overlapped_implication || id == ID_sva_cycle_delay ||
7575
id == ID_sva_sequence_concatenation ||
7676
id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match ||
77-
id == ID_sva_sequence_throughout || id == ID_sva_sequence_within;
77+
id == ID_sva_sequence_throughout || id == ID_sva_sequence_within ||
78+
id == ID_sva_sequence_goto_repetition ||
79+
id == ID_sva_sequence_consecutive_repetition ||
80+
id == ID_sva_sequence_non_consecutive_repetition ||
81+
id == ID_sva_sequence_repetition_star ||
82+
id == ID_sva_sequence_repetition_plus;
7883
}
7984

8085
bool is_SVA_operator(const exprt &expr)

‎src/trans-word-level/property.cpp

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -110,6 +110,42 @@ Function: bmc_supports_SVA_property
110110

111111
bool bmc_supports_SVA_property(const exprt &expr)
112112
{
113+
// sva_sequence_first_match is not supported yet
114+
if(has_subexpr(expr, ID_sva_sequence_first_match))
115+
return false;
116+
117+
// sva_sequence_troughout is not supported yet
118+
if(has_subexpr(expr, ID_sva_sequence_throughout))
119+
return false;
120+
121+
// sva_sequence_intersect is not supported yet
122+
if(has_subexpr(expr, ID_sva_sequence_intersect))
123+
return false;
124+
125+
// sva_sequence_within is not supported yet
126+
if(has_subexpr(expr, ID_sva_sequence_within))
127+
return false;
128+
129+
// sva_sequence_repetition_plus is not supported yet
130+
if(has_subexpr(expr, ID_sva_sequence_repetition_plus))
131+
return false;
132+
133+
// sva_sequence_repetition_star is not supported yet
134+
if(has_subexpr(expr, ID_sva_sequence_repetition_star))
135+
return false;
136+
137+
// sva_sequence_non_consecutive_repetition is not supported yet
138+
if(has_subexpr(expr, ID_sva_sequence_non_consecutive_repetition))
139+
return false;
140+
141+
// sva_sequence_consecutive_repetition is not supported yet
142+
if(has_subexpr(expr, ID_sva_sequence_consecutive_repetition))
143+
return false;
144+
145+
// sva_sequence_goto_repetition is not supported yet
146+
if(has_subexpr(expr, ID_sva_sequence_goto_repetition))
147+
return false;
148+
113149
return true;
114150
}
115151

‎src/verilog/expr2verilog.cpp

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -453,6 +453,28 @@ expr2verilogt::resultt expr2verilogt::convert_sva_unary(
453453

454454
/*******************************************************************\
455455
456+
Function: expr2verilogt::convert_sva_unary
457+
458+
Inputs:
459+
460+
Outputs:
461+
462+
Purpose:
463+
464+
\*******************************************************************/
465+
466+
expr2verilogt::resultt expr2verilogt::convert_sva_unary(
467+
const unary_exprt &src,
468+
const std::string &name)
469+
{
470+
auto op = convert_rec(src.op());
471+
if(op.p == verilog_precedencet::MIN && src.op().operands().size() >= 2)
472+
op.s = "(" + op.s + ")";
473+
return {verilog_precedencet::MIN, op.s + name};
474+
}
475+
476+
/*******************************************************************\
477+
456478
Function: expr2verilogt::convert_sva_binary
457479
458480
Inputs:
@@ -1446,6 +1468,16 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
14461468
convert_sva_binary("intersect", to_binary_expr(src));
14471469
// not sure about precedence
14481470

1471+
else if(src.id() == ID_sva_sequence_throughout)
1472+
return precedence = verilog_precedencet::MIN,
1473+
convert_sva_binary("throughout", to_binary_expr(src));
1474+
// not sure about precedence
1475+
1476+
else if(src.id() == ID_sva_sequence_within)
1477+
return precedence = verilog_precedencet::MIN,
1478+
convert_sva_binary("within", to_binary_expr(src));
1479+
// not sure about precedence
1480+
14491481
else if(src.id() == ID_sva_sequence_within)
14501482
return convert_sva_sequence_concatenation(
14511483
to_binary_expr(src), precedence = verilog_precedencet::MIN);
@@ -1460,6 +1492,31 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
14601492
return precedence = verilog_precedencet::MIN,
14611493
convert_sva_unary("always", to_sva_always_expr(src));
14621494

1495+
else if(src.id() == ID_sva_sequence_repetition_star)
1496+
return precedence = verilog_precedencet::MIN,
1497+
convert_sva_unary(to_unary_expr(src), "[*]");
1498+
// not sure about precedence
1499+
1500+
else if(src.id() == ID_sva_sequence_repetition_plus)
1501+
return precedence = verilog_precedencet::MIN,
1502+
convert_sva_unary(to_unary_expr(src), "[+]");
1503+
// not sure about precedence
1504+
1505+
else if(src.id() == ID_sva_sequence_non_consecutive_repetition)
1506+
return precedence = verilog_precedencet::MIN,
1507+
convert_sva_binary("[=]", to_binary_expr(src));
1508+
// not sure about precedence
1509+
1510+
else if(src.id() == ID_sva_sequence_consecutive_repetition)
1511+
return precedence = verilog_precedencet::MIN,
1512+
convert_sva_binary("[*]", to_binary_expr(src));
1513+
// not sure about precedence
1514+
1515+
else if(src.id() == ID_sva_sequence_goto_repetition)
1516+
return precedence = verilog_precedencet::MIN,
1517+
convert_sva_binary("[->]", to_binary_expr(src));
1518+
// not sure about precedence
1519+
14631520
else if(src.id() == ID_sva_ranged_always)
14641521
{
14651522
return precedence = verilog_precedencet::MIN,

0 commit comments

Comments
 (0)