Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 4cb485d

Browse files
kroeningkroening
committedApr 25, 2025·
BMC: implement weak/strong sequences
This implements strong semantics for SVA sequences in the word-level BMC engine. Strong semantics are used with an explicit strong(...) operator or for SVA cover. The difference between weak and strong semantics arises in BMC when the sequence reaches the end of the unwinding: using weak semantics, the sequence matches, whereas using strong semantics the sequence does not.
1 parent 831cc43 commit 4cb485d

File tree

14 files changed

+191
-67
lines changed

14 files changed

+191
-67
lines changed
 

‎CHANGELOG

Lines changed: 1 addition & 0 deletions
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

Lines changed: 6 additions & 5 deletions
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

Lines changed: 9 additions & 3 deletions
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

Lines changed: 11 additions & 0 deletions
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

Lines changed: 18 additions & 0 deletions
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

Lines changed: 12 additions & 0 deletions
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

Lines changed: 18 additions & 0 deletions
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

Lines changed: 4 additions & 5 deletions
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

Lines changed: 5 additions & 6 deletions
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

Lines changed: 2 additions & 2 deletions
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

Lines changed: 2 additions & 2 deletions
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/property.cpp

Lines changed: 46 additions & 11 deletions
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;

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

Lines changed: 54 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
99
#include "sequence.h"
1010

1111
#include <util/arith_tools.h>
12-
#include <util/ebmc_util.h>
1312

13+
#include <ebmc/ebmc_error.h>
1414
#include <temporal-logic/temporal_logic.h>
1515
#include <verilog/sva_expr.h>
1616

@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
2020

2121
sequence_matchest instantiate_sequence(
2222
exprt expr,
23+
sva_sequence_semanticst semantics,
2324
const mp_integer &t,
2425
const mp_integer &no_timeframes)
2526
{
@@ -32,17 +33,21 @@ sequence_matchest instantiate_sequence(
3233
{
3334
const auto u = t + from;
3435

35-
// Do we exceed the bound? Make it 'true'
36+
// Do we exceed the bound? Make it 'false'/'true', depending
37+
// on semantics.
3638
if(u >= no_timeframes)
3739
{
3840
DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
39-
return {{no_timeframes - 1, true_exprt()}};
41+
if(semantics == sva_sequence_semanticst::WEAK)
42+
return {{no_timeframes - 1, true_exprt{}}};
43+
else // STRONG
44+
return {}; // no match
4045
}
4146
else
4247
return instantiate_sequence(
43-
sva_cycle_delay_expr.op(), u, no_timeframes);
48+
sva_cycle_delay_expr.op(), semantics, u, no_timeframes);
4449
}
45-
else // a range
50+
else // ##[from:to] something
4651
{
4752
auto lower = t + from;
4853
mp_integer upper;
@@ -52,29 +57,35 @@ sequence_matchest instantiate_sequence(
5257
DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
5358
upper = no_timeframes;
5459
}
55-
else
60+
else if(sva_cycle_delay_expr.to().is_constant())
5661
{
57-
mp_integer to;
58-
if(to_integer_non_constant(sva_cycle_delay_expr.to(), to))
59-
throw "failed to convert sva_cycle_delay offsets";
62+
auto to = numeric_cast_v<mp_integer>(
63+
to_constant_expr(sva_cycle_delay_expr.to()));
6064
upper = t + to;
6165
}
66+
else
67+
throw ebmc_errort{} << "failed to convert sva_cycle_delay offsets";
6268

6369
sequence_matchest matches;
6470

65-
// Do we exceed the bound? Add an unconditional match.
71+
// Do we exceed the bound? Add an unconditional match when using
72+
// weak semantics.
6673
if(upper >= no_timeframes)
6774
{
68-
DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
69-
matches.emplace_back(no_timeframes - 1, true_exprt());
7075
upper = no_timeframes - 1;
76+
77+
if(semantics == sva_sequence_semanticst::WEAK)
78+
{
79+
DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
80+
matches.emplace_back(no_timeframes - 1, true_exprt());
81+
}
7182
}
7283

7384
// Add a potential match for each timeframe in the range
7485
for(mp_integer u = lower; u <= upper; ++u)
7586
{
76-
auto sub_result =
77-
instantiate_sequence(sva_cycle_delay_expr.op(), u, no_timeframes);
87+
auto sub_result = instantiate_sequence(
88+
sva_cycle_delay_expr.op(), semantics, u, no_timeframes);
7889
for(auto &match : sub_result)
7990
matches.push_back(match);
8091
}
@@ -85,12 +96,14 @@ sequence_matchest instantiate_sequence(
8596
else if(expr.id() == ID_sva_cycle_delay_star) // ##[*] something
8697
{
8798
auto &cycle_delay_star = to_sva_cycle_delay_star_expr(expr);
88-
return instantiate_sequence(cycle_delay_star.lower(), t, no_timeframes);
99+
return instantiate_sequence(
100+
cycle_delay_star.lower(), semantics, t, no_timeframes);
89101
}
90102
else if(expr.id() == ID_sva_cycle_delay_plus) // ##[+] something
91103
{
92104
auto &cycle_delay_plus = to_sva_cycle_delay_plus_expr(expr);
93-
return instantiate_sequence(cycle_delay_plus.lower(), t, no_timeframes);
105+
return instantiate_sequence(
106+
cycle_delay_plus.lower(), semantics, t, no_timeframes);
94107
}
95108
else if(expr.id() == ID_sva_sequence_concatenation)
96109
{
@@ -99,21 +112,25 @@ sequence_matchest instantiate_sequence(
99112

100113
// This is the product of the match points on the LHS and RHS
101114
const auto lhs_matches =
102-
instantiate_sequence(implication.lhs(), t, no_timeframes);
115+
instantiate_sequence(implication.lhs(), semantics, t, no_timeframes);
103116

104117
for(auto &lhs_match : lhs_matches)
105118
{
106119
auto t_rhs = lhs_match.end_time;
107120

108-
// Do we exceed the bound? Make it 'true'
121+
// Do we exceed the bound? Make it 'false'/'true', depending
122+
// on semantics.
109123
if(t_rhs >= no_timeframes)
110124
{
111125
DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
112-
return {{no_timeframes - 1, true_exprt()}};
126+
if(semantics == sva_sequence_semanticst::WEAK)
127+
return {{no_timeframes - 1, true_exprt{}}};
128+
else // STRONG
129+
return {}; // no match
113130
}
114131

115-
const auto rhs_matches =
116-
instantiate_sequence(implication.rhs(), t_rhs, no_timeframes);
132+
const auto rhs_matches = instantiate_sequence(
133+
implication.rhs(), semantics, t_rhs, no_timeframes);
117134

118135
for(auto &rhs_match : rhs_matches)
119136
{
@@ -134,9 +151,9 @@ sequence_matchest instantiate_sequence(
134151
auto &intersect = to_sva_sequence_intersect_expr(expr);
135152

136153
const auto lhs_matches =
137-
instantiate_sequence(intersect.lhs(), t, no_timeframes);
154+
instantiate_sequence(intersect.lhs(), semantics, t, no_timeframes);
138155
const auto rhs_matches =
139-
instantiate_sequence(intersect.rhs(), t, no_timeframes);
156+
instantiate_sequence(intersect.rhs(), semantics, t, no_timeframes);
140157

141158
sequence_matchest result;
142159

@@ -161,7 +178,7 @@ sequence_matchest instantiate_sequence(
161178
auto &first_match = to_sva_sequence_first_match_expr(expr);
162179

163180
const auto lhs_matches =
164-
instantiate_sequence(first_match.lhs(), t, no_timeframes);
181+
instantiate_sequence(first_match.lhs(), semantics, t, no_timeframes);
165182

166183
// the match of seq with the earliest ending clock tick is a
167184
// match of first_match (seq)
@@ -198,7 +215,7 @@ sequence_matchest instantiate_sequence(
198215
auto &throughout = to_sva_sequence_throughout_expr(expr);
199216

200217
const auto rhs_matches =
201-
instantiate_sequence(throughout.rhs(), t, no_timeframes);
218+
instantiate_sequence(throughout.rhs(), semantics, t, no_timeframes);
202219

203220
sequence_matchest result;
204221

@@ -225,16 +242,16 @@ sequence_matchest instantiate_sequence(
225242

226243
auto &within_expr = to_sva_sequence_within_expr(expr);
227244
const auto matches_rhs =
228-
instantiate_sequence(within_expr.rhs(), t, no_timeframes);
245+
instantiate_sequence(within_expr.rhs(), semantics, t, no_timeframes);
229246

230247
sequence_matchest result;
231248

232249
for(auto &match_rhs : matches_rhs)
233250
{
234251
for(auto start_lhs = t; start_lhs <= match_rhs.end_time; ++start_lhs)
235252
{
236-
auto matches_lhs =
237-
instantiate_sequence(within_expr.lhs(), start_lhs, no_timeframes);
253+
auto matches_lhs = instantiate_sequence(
254+
within_expr.lhs(), semantics, start_lhs, no_timeframes);
238255

239256
for(auto &match_lhs : matches_lhs)
240257
{
@@ -260,8 +277,10 @@ sequence_matchest instantiate_sequence(
260277
// 3. The end time of the composite sequence is
261278
// the end time of the operand sequence that completes last.
262279
auto &and_expr = to_sva_and_expr(expr);
263-
auto matches_lhs = instantiate_sequence(and_expr.lhs(), t, no_timeframes);
264-
auto matches_rhs = instantiate_sequence(and_expr.rhs(), t, no_timeframes);
280+
auto matches_lhs =
281+
instantiate_sequence(and_expr.lhs(), semantics, t, no_timeframes);
282+
auto matches_rhs =
283+
instantiate_sequence(and_expr.rhs(), semantics, t, no_timeframes);
265284

266285
sequence_matchest result;
267286

@@ -283,7 +302,7 @@ sequence_matchest instantiate_sequence(
283302
sequence_matchest result;
284303

285304
for(auto &op : expr.operands())
286-
for(auto &match : instantiate_sequence(op, t, no_timeframes))
305+
for(auto &match : instantiate_sequence(op, semantics, t, no_timeframes))
287306
result.push_back(match);
288307

289308
return result;
@@ -292,7 +311,8 @@ sequence_matchest instantiate_sequence(
292311
{
293312
// x[*n] is syntactic sugar for x ##1 ... ##1 x, with n repetitions
294313
auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr);
295-
return instantiate_sequence(repetition.lower(), t, no_timeframes);
314+
return instantiate_sequence(
315+
repetition.lower(), semantics, t, no_timeframes);
296316
}
297317
else if(
298318
expr.id() == ID_sva_sequence_repetition_plus ||
@@ -370,7 +390,8 @@ sequence_matchest instantiate_sequence(
370390

371391
// We add up the number of matches of 'op' starting from
372392
// timeframe u, until the end of our unwinding.
373-
const auto bits = address_bits(no_timeframes);
393+
const auto bits =
394+
address_bits(std::max(no_timeframes, repetitions_int + 1));
374395
const auto zero = from_integer(0, unsignedbv_typet{bits});
375396
const auto one = from_integer(1, zero.type());
376397
const auto repetitions = from_integer(repetitions_int, zero.type());

‎src/trans-word-level/sequence.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
1212
#include <util/expr.h>
1313
#include <util/mp_arith.h>
1414

15+
#include <verilog/sva_expr.h>
16+
1517
/// A match for an SVA sequence.
1618
class sequence_matcht
1719
{
@@ -32,6 +34,7 @@ using sequence_matchest = std::vector<sequence_matcht>;
3234
/// for the given sequence expression starting at time t
3335
[[nodiscard]] sequence_matchest instantiate_sequence(
3436
exprt expr,
37+
sva_sequence_semanticst,
3538
const mp_integer &t,
3639
const mp_integer &no_timeframes);
3740

0 commit comments

Comments
 (0)
Please sign in to comment.