Skip to content

Commit 0a1c5ce

Browse files
kroeningkroening
authored
Merge pull request #1070 from diffblue/sva-weak-strong
BMC: implement weak/strong sequences
2 parents 6643d61 + 4cb485d commit 0a1c5ce

15 files changed

+198
-99
lines changed

‎CHANGELOG

+1
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
* SystemVerilog: within
1010
* SystemVerilog: bugfix for |-> and |=>
1111
* SystemVerilog: bugfix for SVA sequence and
12+
* SystemVerilog: strong/weak sequence semantics
1213
* Verilog: 'dx, 'dz
1314
* SMV: LTL V operator, xnor operator
1415
* SMV: word types and operators

‎regression/verilog/SVA/cover_sequence2.desc

+6-5
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,12 @@
1-
KNOWNBUG
1+
CORE
22
cover_sequence2.sv
3-
--bound 2
4-
^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): PROVED$
5-
^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): REFUTED up to bound 2$
3+
--bound 5
4+
^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): REFUTED up to bound 5$
5+
^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): REFUTED up to bound 5$
6+
^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): PROVED$
7+
^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): REFUTED up to bound 5$
68
^EXIT=10$
79
^SIGNAL=0$
810
--
911
^warning: ignoring
1012
--
11-
Cover property p0 cannot ever hold, but is shown proven when using a small bound.

‎regression/verilog/SVA/cover_sequence2.sv

+9-3
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,21 @@
11
module main(input clk);
22

33
// count up
4-
reg [7:0] x = 0;
4+
int x = 0;
55

6-
always @(posedge clk)
6+
always_ff @(posedge clk)
77
x++;
88

99
// expected to fail
1010
p0: cover property (x==2 ##1 x==3 ##1 x==100);
1111

12-
// expected to fail until bound reaches 100
12+
// expected to fail until x reaches 100
1313
p1: cover property (x==98 ##1 x==99 ##1 x==100);
1414

15+
// expected to pass once x reaches 5
16+
p2: cover property (x==3 ##1 x==4 ##1 x==5);
17+
18+
// expected to pass once x reaches 6
19+
p3: cover property (x==4 ##1 x==5 ##1 x==6);
20+
1521
endmodule

‎regression/verilog/SVA/cover_sequence3.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
cover_sequence3.sv
3+
--bound 3
4+
^\[main\.p0\] cover \(1 \[\*10\]\): REFUTED up to bound 3$
5+
^\[main\.p1\] cover \(1 \[\*4:10\]\): PROVED$
6+
^\[main\.p2\] cover \(1 \[\*5:10\]\): REFUTED up to bound 3$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
^warning: ignoring
11+
--

‎regression/verilog/SVA/cover_sequence3.sv

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
module main(input clk);
2+
3+
// count up
4+
int x = 0;
5+
6+
always_ff @(posedge clk)
7+
x++;
8+
9+
// passes with bound >=9
10+
p0: cover property (1[*10]);
11+
12+
// passes with bound >=3
13+
p1: cover property (1[*4:10]);
14+
15+
// passes with bound >=4
16+
p2: cover property (1[*5:10]);
17+
18+
endmodule

‎regression/verilog/SVA/cover_sequence4.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
KNOWNBUG
2+
cover_sequence4.sv
3+
--bound 3
4+
^\[main\.p0\] cover \(1 \[=10\]\): REFUTED up to bound 3$
5+
^\[main\.p1\] cover \(1 \[=4:10\]\): PROVED$
6+
^\[main\.p2\] cover \(1 \[=5:10\]\): REFUTED up to bound 3$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
^warning: ignoring
11+
--
12+
Implementation of [=x:y] is missing.

‎regression/verilog/SVA/cover_sequence4.sv

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
module main(input clk);
2+
3+
// count up
4+
int x = 0;
5+
6+
always_ff @(posedge clk)
7+
x++;
8+
9+
// passes with bound >=9
10+
p0: cover property (1[=10]);
11+
12+
// passes with bound >=3
13+
p1: cover property (1[=4:10]);
14+
15+
// passes with bound >=4
16+
p2: cover property (1[=5:10]);
17+
18+
endmodule

‎regression/verilog/SVA/sequence2.desc

+4-5
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,10 @@
1-
KNOWNBUG
1+
CORE
22
sequence2.sv
3-
--bound 10 --numbered-trace
4-
^\[main\.p0] ##\[0:\$\] main\.x == 10: PROVED up to bound 10$
5-
^\[main\.p1] ##\[0:\$\] main\.x == 10: REFUTED$
3+
--bound 10
4+
^\[main\.p0] weak\(##\[0:\$\] main\.x == 10\): PROVED up to bound 10$
5+
^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): REFUTED$
66
^EXIT=10$
77
^SIGNAL=0$
88
--
99
^warning: ignoring
1010
--
11-
strong(...) is missing.

‎regression/verilog/SVA/sequence3.desc

+5-6
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,12 @@
1-
KNOWNBUG
1+
CORE
22
sequence3.sv
33
--bound 20 --numbered-trace
4-
^\[main\.p0\] ##\[\*\] main\.x == 6: REFUTED$
5-
^\[main\.p1\] ##\[\*\] main\.x == 5: PROVED up to bound 20$
6-
^\[main\.p2\] ##\[\+\] main\.x == 0: REFUTED$
7-
^\[main\.p3\] ##\[\+\] main\.x == 5: PROVED up to bound 20$
4+
^\[main\.p0\] strong\(##\[\*\] main\.x == 6\): REFUTED$
5+
^\[main\.p1\] strong\(##\[\*\] main\.x == 5\): PROVED up to bound 20$
6+
^\[main\.p2\] strong\(##\[\+\] main\.x == 0\): REFUTED$
7+
^\[main\.p3\] strong\(##\[\+\] main\.x == 5\): PROVED up to bound 20$
88
^EXIT=10$
99
^SIGNAL=0$
1010
--
1111
^warning: ignoring
1212
--
13-
strong(...) is missing

‎regression/verilog/SVA/strong1.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
strong1.sv
3-
--bound 20
4-
^\[main\.p0\] strong\(##\[0:9\] main\.x == 100\): REFUTED$
3+
--bound 4
4+
^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): REFUTED$
55
^EXIT=10$
66
^SIGNAL=0$
77
--

‎regression/verilog/SVA/strong1.sv

+2-2
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ module main;
88
always @(posedge clk)
99
x<=x+1;
1010

11-
// fails
12-
initial p0: assert property (strong(##[0:9] x==100));
11+
// fails if bound is too low
12+
initial p0: assert property (strong(##[0:9] x==5));
1313

1414
endmodule

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

+7-32
Original file line numberDiff line numberDiff line change
@@ -123,40 +123,15 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
123123
expr.id() == ID_typecast && expr.type().id() == ID_bool &&
124124
to_typecast_expr(expr).op().type().id() == ID_verilog_sva_sequence)
125125
{
126-
auto &sequence = to_typecast_expr(expr).op();
127-
128-
// sequence expressions -- these may have multiple potential
129-
// match points, and evaluate to true if any of them matches
130-
const auto matches = instantiate_sequence(sequence, t, no_timeframes);
131-
exprt::operandst disjuncts;
132-
disjuncts.reserve(matches.size());
133-
mp_integer max = t;
134-
135-
for(auto &match : matches)
136-
{
137-
disjuncts.push_back(match.condition);
138-
max = std::max(max, match.end_time);
139-
}
140-
141-
return {max, disjunction(disjuncts)};
126+
// should have been done by property_obligations_rec
127+
PRECONDITION(false);
142128
}
143-
else if(expr.id() == ID_sva_sequence_property)
129+
else if(
130+
expr.id() == ID_sva_sequence_property || expr.id() == ID_sva_weak ||
131+
expr.id() == ID_sva_strong)
144132
{
145-
// sequence expressions -- these may have multiple potential
146-
// match points, and evaluate to true if any of them matches
147-
auto &sequence = to_sva_sequence_property_expr(expr);
148-
const auto matches = instantiate_sequence(sequence, t, no_timeframes);
149-
exprt::operandst disjuncts;
150-
disjuncts.reserve(matches.size());
151-
mp_integer max = t;
152-
153-
for(auto &match : matches)
154-
{
155-
disjuncts.push_back(match.condition);
156-
max = std::max(max, match.end_time);
157-
}
158-
159-
return {max, disjunction(disjuncts)};
133+
// should have been done by property_obligations_rec
134+
PRECONDITION(false);
160135
}
161136
else if(expr.id() == ID_verilog_past)
162137
{

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

+46-11
Original file line numberDiff line numberDiff line change
@@ -140,6 +140,32 @@ bool bmc_supports_property(const exprt &expr)
140140

141141
/*******************************************************************\
142142
143+
Function: sva_sequence_semantics
144+
145+
Inputs:
146+
147+
Outputs:
148+
149+
Purpose:
150+
151+
\*******************************************************************/
152+
153+
static sva_sequence_semanticst sva_sequence_semantics(irep_idt id)
154+
{
155+
if(id == ID_sva_strong)
156+
return sva_sequence_semanticst::STRONG;
157+
else if(id == ID_sva_weak)
158+
return sva_sequence_semanticst::WEAK;
159+
else if(id == ID_sva_implicit_strong)
160+
return sva_sequence_semanticst::STRONG;
161+
else if(id == ID_sva_implicit_weak)
162+
return sva_sequence_semanticst::WEAK;
163+
else
164+
PRECONDITION(false);
165+
}
166+
167+
/*******************************************************************\
168+
143169
Function: property_obligations_rec
144170
145171
Inputs:
@@ -527,16 +553,17 @@ static obligationst property_obligations_rec(
527553
op.id() == ID_sva_strong || op.id() == ID_sva_weak ||
528554
op.id() == ID_sva_implicit_strong || op.id() == ID_sva_implicit_weak)
529555
{
530-
// The sequence must not match.
531556
auto &sequence = to_sva_sequence_property_expr_base(op).sequence();
557+
auto semantics = sva_sequence_semantics(op.id());
532558

533559
const auto matches =
534-
instantiate_sequence(sequence, current, no_timeframes);
560+
instantiate_sequence(sequence, semantics, current, no_timeframes);
535561

536562
obligationst obligations;
537563

538564
for(auto &match : matches)
539565
{
566+
// The sequence must not match.
540567
obligations.add(match.end_time, not_exprt{match.condition});
541568
}
542569

@@ -577,10 +604,13 @@ static obligationst property_obligations_rec(
577604
auto &implication = to_binary_expr(property_expr);
578605

579606
// The LHS is a sequence, the RHS is a property.
580-
// The implication must hold for _all_ matches on the LHS,
607+
// The implication must hold for _all_ (strong) matches on the LHS,
581608
// i.e., each pair of LHS match and RHS obligation yields an obligation.
582-
const auto lhs_match_points =
583-
instantiate_sequence(implication.lhs(), current, no_timeframes);
609+
const auto lhs_match_points = instantiate_sequence(
610+
implication.lhs(),
611+
sva_sequence_semanticst::STRONG,
612+
current,
613+
no_timeframes);
584614

585615
obligationst result;
586616

@@ -620,9 +650,12 @@ static obligationst property_obligations_rec(
620650
// the result is a property expression.
621651
auto &followed_by = to_sva_followed_by_expr(property_expr);
622652

623-
// get match points for LHS sequence
624-
auto matches =
625-
instantiate_sequence(followed_by.antecedent(), current, no_timeframes);
653+
// get (proper) match points for LHS sequence
654+
auto matches = instantiate_sequence(
655+
followed_by.antecedent(),
656+
sva_sequence_semanticst::STRONG,
657+
current,
658+
no_timeframes);
626659

627660
exprt::operandst disjuncts;
628661
mp_integer t = current;
@@ -660,12 +693,14 @@ static obligationst property_obligations_rec(
660693
property_expr.id() == ID_sva_implicit_strong ||
661694
property_expr.id() == ID_sva_implicit_weak)
662695
{
696+
// sequence expressions -- these may have multiple potential
697+
// match points, and evaluate to true if any of them matches
663698
auto &sequence =
664699
to_sva_sequence_property_expr_base(property_expr).sequence();
700+
auto semantics = sva_sequence_semantics(property_expr.id());
665701

666-
// sequence expressions -- these may have multiple potential
667-
// match points, and evaluate to true if any of them matches
668-
const auto matches = instantiate_sequence(sequence, current, no_timeframes);
702+
const auto matches =
703+
instantiate_sequence(sequence, semantics, current, no_timeframes);
669704
exprt::operandst disjuncts;
670705
disjuncts.reserve(matches.size());
671706
mp_integer max = current;

0 commit comments

Comments
 (0)