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,

‎src/verilog/expr2verilog_class.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -120,6 +120,8 @@ class expr2verilogt
120120

121121
resultt convert_sva_unary(const std::string &name, const unary_exprt &);
122122

123+
resultt convert_sva_unary(const unary_exprt &, const std::string &name);
124+
123125
resultt convert_sva_binary(const std::string &name, const binary_exprt &);
124126

125127
resultt convert_sva_abort(const std::string &name, const sva_abort_exprt &);

‎src/verilog/verilog_typecheck_expr.cpp

Lines changed: 21 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -2465,27 +2465,15 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
24652465
expr.id() == ID_sva_cycle_delay_plus ||
24662466
expr.id() == ID_sva_cycle_delay_star || expr.id() == ID_sva_weak ||
24672467
expr.id() == ID_sva_strong || expr.id() == ID_sva_nexttime ||
2468-
expr.id() == ID_sva_s_nexttime)
2468+
expr.id() == ID_sva_s_nexttime ||
2469+
expr.id() == ID_sva_sequence_first_match ||
2470+
expr.id() == ID_sva_sequence_repetition_plus ||
2471+
expr.id() == ID_sva_sequence_repetition_star)
24692472
{
24702473
convert_expr(expr.op());
24712474
make_boolean(expr.op());
24722475
expr.type()=bool_typet();
24732476
}
2474-
else if(expr.id() == ID_sva_sequence_first_match)
2475-
{
2476-
throw errort().with_location(expr.source_location())
2477-
<< "no support for 'first_match'";
2478-
}
2479-
else if(expr.id() == ID_sva_sequence_repetition_plus)
2480-
{
2481-
throw errort().with_location(expr.source_location())
2482-
<< "currently no support for [+]";
2483-
}
2484-
else if(expr.id() == ID_sva_sequence_repetition_star)
2485-
{
2486-
throw errort().with_location(expr.source_location())
2487-
<< "currently no support for [*]";
2488-
}
24892477
else if(expr.id() == ID_verilog_explicit_cast)
24902478
{
24912479
// SystemVerilog has got type'(expr). This is an explicit
@@ -2959,20 +2947,24 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
29592947

29602948
return std::move(expr);
29612949
}
2962-
else if(expr.id() == ID_sva_sequence_intersect)
2963-
{
2964-
throw errort().with_location(expr.source_location())
2965-
<< "no support for 'intersect'";
2966-
}
2967-
else if(expr.id() == ID_sva_sequence_throughout)
2968-
{
2969-
throw errort().with_location(expr.source_location())
2970-
<< "no support for 'throughout'";
2971-
}
2972-
else if(expr.id() == ID_sva_sequence_within)
2950+
else if(
2951+
expr.id() == ID_sva_sequence_intersect ||
2952+
expr.id() == ID_sva_sequence_throughout ||
2953+
expr.id() == ID_sva_sequence_within ||
2954+
expr.id() == ID_sva_sequence_non_consecutive_repetition ||
2955+
expr.id() == ID_sva_sequence_consecutive_repetition ||
2956+
expr.id() == ID_sva_sequence_goto_repetition)
29732957
{
2974-
throw errort().with_location(expr.source_location())
2975-
<< "no support for 'within'";
2958+
auto &binary_expr = to_binary_expr(expr);
2959+
2960+
convert_expr(binary_expr.lhs());
2961+
make_boolean(binary_expr.lhs());
2962+
convert_expr(binary_expr.rhs());
2963+
make_boolean(binary_expr.rhs());
2964+
2965+
expr.type() = bool_typet();
2966+
2967+
return std::move(expr);
29762968
}
29772969
else if(expr.id()==ID_hierarchical_identifier)
29782970
{
@@ -3026,21 +3018,6 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
30263018
expr.type() = bool_typet();
30273019
return std::move(expr);
30283020
}
3029-
else if(expr.id() == ID_sva_sequence_non_consecutive_repetition)
3030-
{
3031-
throw errort().with_location(expr.source_location())
3032-
<< "currently no support for [=]";
3033-
}
3034-
else if(expr.id() == ID_sva_sequence_consecutive_repetition)
3035-
{
3036-
throw errort().with_location(expr.source_location())
3037-
<< "currently no support for [*]";
3038-
}
3039-
else if(expr.id() == ID_sva_sequence_goto_repetition)
3040-
{
3041-
throw errort().with_location(expr.source_location())
3042-
<< "currently no support for [->]";
3043-
}
30443021
else
30453022
{
30463023
// type is guessed for now

0 commit comments

Comments
 (0)