Skip to content

Commit 0299e1d

Browse files
kroeningkroening
authored
Merge pull request #687 from diffblue/bmc-supported-SVA
Fix fragment of SVA supported by word-level BMC
2 parents 8d28b46 + 0675677 commit 0299e1d

12 files changed

+390
-279
lines changed

‎regression/verilog/SVA/s_eventually4.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
s_eventually4.sv
3+
--module main --bound 11
4+
^\[main\.p0\] always \(\(s_eventually main\.counter == 1\) or \(s_eventually main.counter == 10\)\): PROVED up to bound 11$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎regression/verilog/SVA/s_eventually4.sv

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
module main(input clk);
2+
3+
reg [7:0] counter;
4+
5+
initial counter = 0;
6+
7+
// 0, 1, 2, 3, 4, 0, ...
8+
always @(posedge clk)
9+
if(counter < 5)
10+
counter = counter + 1;
11+
else
12+
counter = 0;
13+
14+
// expected to pass, owing to the first disjunct
15+
p0: assert property ((s_eventually counter==1) or (s_eventually counter==10));
16+
17+
endmodule

‎src/temporal-logic/normalize_property.cpp

Lines changed: 38 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#include "normalize_property.h"
1010

1111
#include <util/arith_tools.h>
12+
#include <util/mathematical_types.h>
1213
#include <util/std_expr.h>
1314

1415
#include <verilog/sva_expr.h>
@@ -75,9 +76,8 @@ exprt normalize_pre_implies(implies_exprt expr)
7576
exprt normalize_pre_sva_overlapped_implication(
7677
sva_overlapped_implication_exprt expr)
7778
{
78-
// Same as regular implication if lhs and rhs are not
79-
// sequences.
80-
if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
79+
// Same as regular implication if lhs is not a sequence.
80+
if(!is_SVA_sequence(expr.lhs()))
8181
return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
8282
else
8383
return std::move(expr);
@@ -86,9 +86,13 @@ exprt normalize_pre_sva_overlapped_implication(
8686
exprt normalize_pre_sva_non_overlapped_implication(
8787
sva_non_overlapped_implication_exprt expr)
8888
{
89-
// Same as a->Xb if lhs and rhs are not sequences.
90-
if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
91-
return or_exprt{not_exprt{expr.lhs()}, X_exprt{expr.rhs()}};
89+
// Same as a->always[1:1] b if lhs is not a sequence.
90+
if(!is_SVA_sequence(expr.lhs()))
91+
{
92+
auto one = natural_typet{}.one_expr();
93+
return or_exprt{
94+
not_exprt{expr.lhs()}, sva_ranged_always_exprt{one, one, expr.rhs()}};
95+
}
9296
else
9397
return std::move(expr);
9498
}
@@ -125,13 +129,14 @@ exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
125129
expr.from().is_constant() &&
126130
numeric_cast_v<mp_integer>(to_constant_expr(expr.from())) == 0)
127131
{
128-
// ##[0:$] φ --> F φ
129-
return F_exprt{expr.op()};
132+
// ##[0:$] φ --> s_eventually φ
133+
return sva_s_eventually_exprt{expr.op()};
130134
}
131135
else
132136
{
133-
// ##[i:$] φ --> ##i F φ
134-
return sva_cycle_delay_exprt{expr.from(), F_exprt{expr.op()}};
137+
// ##[i:$] φ --> always[i:i] s_eventually φ
138+
return sva_ranged_always_exprt{
139+
expr.from(), expr.from(), sva_s_eventually_exprt{expr.op()}};
135140
}
136141
}
137142
else
@@ -171,11 +176,13 @@ exprt normalize_property(exprt expr)
171176
expr = normalize_pre_sva_or(to_sva_or_expr(expr));
172177
else if(expr.id() == ID_sva_nexttime)
173178
{
174-
expr = X_exprt{to_sva_nexttime_expr(expr).op()};
179+
auto one = natural_typet{}.one_expr();
180+
expr = sva_ranged_always_exprt{one, one, to_sva_nexttime_expr(expr).op()};
175181
}
176182
else if(expr.id() == ID_sva_s_nexttime)
177183
{
178-
expr = X_exprt{to_sva_s_nexttime_expr(expr).op()};
184+
auto one = natural_typet{}.one_expr();
185+
expr = sva_s_always_exprt{one, one, to_sva_s_nexttime_expr(expr).op()};
179186
}
180187
else if(expr.id() == ID_sva_indexed_nexttime)
181188
{
@@ -190,11 +197,28 @@ exprt normalize_property(exprt expr)
190197
nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()};
191198
}
192199
else if(expr.id() == ID_sva_cycle_delay)
200+
{
193201
expr = normalize_pre_sva_cycle_delay(to_sva_cycle_delay_expr(expr));
202+
}
194203
else if(expr.id() == ID_sva_cycle_delay_plus)
195-
expr = F_exprt{X_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
204+
{
205+
expr = sva_s_eventually_exprt{
206+
sva_s_nexttime_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
207+
}
196208
else if(expr.id() == ID_sva_cycle_delay_star)
197-
expr = F_exprt{to_sva_cycle_delay_star_expr(expr).op()};
209+
{
210+
expr = sva_s_eventually_exprt{to_sva_cycle_delay_star_expr(expr).op()};
211+
}
212+
else if(expr.id() == ID_sva_sequence_concatenation)
213+
{
214+
auto &sequence_concatenation = to_sva_sequence_concatenation_expr(expr);
215+
if(!is_SVA_sequence(sequence_concatenation.lhs()))
216+
{
217+
// a ##0 b --> a && b if a is not a sequence
218+
expr =
219+
and_exprt{sequence_concatenation.lhs(), sequence_concatenation.rhs()};
220+
}
221+
}
198222
else if(expr.id() == ID_sva_if)
199223
{
200224
auto &sva_if_expr = to_sva_if_expr(expr);

‎src/temporal-logic/normalize_property.h

Lines changed: 20 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -12,38 +12,47 @@ Author: Daniel Kroening, [email protected]
1212
#include <util/expr.h>
1313

1414
/// This applies the following rewrites:
15+
///
1516
/// cover(φ) --> G¬φ
17+
///
18+
/// -----Propositional-----
1619
/// ¬(a ∨ b) --> ¬a ∧ ¬b
1720
/// ¬(a ∧ b) --> ¬a ∨ ¬b
1821
/// (a -> b) --> ¬a ∨ b
22+
///
23+
/// -----SVA-----
1924
/// a sva_iff b --> a <-> b
2025
/// a sva_implies b --> a -> b
2126
/// sva_not a --> ¬a
22-
/// a sva_and b --> a ∧ b if a and b are not SVA sequences
23-
/// a sva_or b --> a ∨ b if a and b are not SVA sequences
24-
/// sva_overlapped_implication --> ¬a ∨ b if a and b are not SVA sequences
25-
/// sva_non_overlapped_implication --> ¬a ∨ Xb if a and b are not SVA sequences
26-
/// sva_nexttime φ --> Xφ
27+
/// a sva_and b --> a ∧ b if a and b are not SVA sequences
28+
/// a sva_or b --> a ∨ b if a and b are not SVA sequences
29+
/// sva_overlapped_implication --> ¬a ∨ b if a is not an SVA sequence
30+
/// sva_non_overlapped_implication --> ¬a ∨ always[1:1] b if a is not an SVA sequence
31+
/// sva_nexttime φ --> sva_always[1:1] φ
2732
/// sva_nexttime[i] φ --> sva_always[i:i] φ
28-
/// sva_s_nexttime φ --> Xφ
33+
/// sva_s_nexttime φ --> sva_always[1:1] φ
2934
/// sva_s_nexttime[i] φ --> sva_s_always[i:i] φ
3035
/// sva_if --> ? :
36+
/// ##[0:$] φ --> s_eventually φ
37+
/// ##[i:$] φ --> s_nexttime[i] s_eventually φ
38+
/// ##[*] φ --> s_eventually φ
39+
/// ##[+] φ --> always[1:1] s_eventually φ
40+
/// strong(φ) --> φ
41+
/// weak(φ) --> φ
42+
/// sva_case --> ? :
3143
/// a sva_disable_iff b --> a ∨ b
3244
/// a sva_accept_on b --> a ∨ b
3345
/// a sva_reject_on b --> ¬a ∧ b
3446
/// a sva_sync_accept_on b --> a ∨ b
3547
/// a sva_sync_reject_on b --> ¬a ∧ b
3648
/// ¬ sva_s_eventually φ --> sva_always ¬φ
3749
/// ¬ sva_always φ --> sva_s_eventually ¬φ
50+
///
51+
/// ----LTL-----
3852
/// ¬Xφ --> X¬φ
3953
/// ¬¬φ --> φ
4054
/// ¬Gφ --> F¬φ
4155
/// ¬Fφ --> G¬φ
42-
/// ##[*] φ --> F φ
43-
/// ##[+] φ --> X F φ
44-
/// strong(φ) --> φ
45-
/// weak(φ) --> φ
46-
/// sva_case --> ? :
4756
exprt normalize_property(exprt);
4857

4958
#endif

‎src/temporal-logic/temporal_logic.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -85,9 +85,10 @@ bool is_SVA_operator(const exprt &expr)
8585
id == ID_sva_sync_accept_on || id == ID_sva_sync_reject_on ||
8686
id == ID_sva_always || id == ID_sva_ranged_always ||
8787
id == ID_sva_nexttime || id == ID_sva_s_nexttime ||
88-
id == ID_sva_until || id == ID_sva_s_until ||
89-
id == ID_sva_until_with || id == ID_sva_s_until_with ||
90-
id == ID_sva_eventually || id == ID_sva_s_eventually ||
88+
id == ID_sva_indexed_nexttime || id == ID_sva_until ||
89+
id == ID_sva_s_until || id == ID_sva_until_with ||
90+
id == ID_sva_s_until_with || id == ID_sva_eventually ||
91+
id == ID_sva_s_eventually || id == ID_sva_ranged_s_eventually ||
9192
id == ID_sva_cycle_delay || id == ID_sva_overlapped_followed_by ||
9293
id == ID_sva_nonoverlapped_followed_by;
9394
}

‎src/temporal-logic/temporal_logic.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ bool is_SVA_sequence(const exprt &);
4545
/// Returns true iff the given expression is an SVA temporal operator
4646
bool is_SVA_operator(const exprt &);
4747

48-
/// Returns true iff the given expression contains an SVA temporal operator
48+
/// Returns true iff the given expression is an SVA expression
4949
bool is_SVA(const exprt &);
5050

5151
#endif

‎src/trans-word-level/Makefile

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,13 @@
1-
SRC = get_trans.cpp \
1+
SRC = counterexample_word_level.cpp \
2+
get_trans.cpp \
3+
obligations.cpp \
4+
property.cpp \
5+
trans_trace_word_level.cpp \
6+
instantiate_word_level.cpp \
27
show_modules.cpp \
38
show_module_hierarchy.cpp \
49
unwind.cpp \
5-
word_level_trans.cpp \
6-
property.cpp \
7-
counterexample_word_level.cpp \
8-
trans_trace_word_level.cpp \
9-
instantiate_word_level.cpp
10+
word_level_trans.cpp
1011

1112
include ../config.inc
1213
include ../common

0 commit comments

Comments
 (0)