Skip to content

Commit 8bc59f2

Browse files
kroeningkroening
committed
BMC: completeness thresholds larger than one
1 parent 2d61d66 commit 8bc59f2

9 files changed

+60
-38
lines changed

‎regression/verilog/SVA/initial1.bmc.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ initial1.sv
33
--module main
44
^\[main\.p0\] main\.counter == 0: PROVED$
55
^\[main\.p1\] main\.counter == 100: REFUTED$
6-
^\[main\.p2\] ##1 main\.counter == 1: PROVED up to bound 5$
6+
^\[main\.p2\] ##1 main\.counter == 1: PROVED$
77
^\[main\.p3\] ##1 main\.counter == 100: REFUTED$
88
^\[main\.p4\] s_nexttime main\.counter == 1: PROVED$
99
^\[main\.p5\] always \[1:1\] main\.counter == 1: PROVED$

‎regression/verilog/SVA/named_sequence1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
named_sequence1.sv
33

4-
^\[main\.assert\.1\] always main\.x_is_ten: PROVED up to bound 5$
4+
^\[main\.assert\.1\] always main\.x_is_ten: PROVED$
55
^EXIT=0$
66
^SIGNAL=0$
77
--

‎regression/verilog/SVA/sequence6.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
sequence6.sv
33

4-
^\[main\.p0\] \(1 ##1 1\) \|-> main\.x == 1: PROVED up to bound 5$
4+
^\[main\.p0\] \(1 ##1 1\) \|-> main\.x == 1: PROVED$
55
^EXIT=0$
66
^SIGNAL=0$
77
--

‎regression/verilog/SVA/sequence_and1.bmc.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ sequence_and1.sv
33

44
^\[main\.p0\] main\.x == 0 and main\.x == 1: REFUTED$
55
^\[main\.p1\] strong\(main\.x == 0 and main\.x == 1\): REFUTED$
6-
^\[main\.p2\] main\.x == 0 and \(nexttime main\.x == 1\): PROVED up to bound \d+$
7-
^\[main\.p3\] \(nexttime main\.x == 1\) and main\.x == 0: PROVED up to bound \d+$
8-
^\[main\.p4\] \(main\.x == 0 and main\.x != 10\) |=> main\.x == 1: PROVED up to bound \d+$
6+
^\[main\.p2\] main\.x == 0 and \(nexttime main\.x == 1\): PROVED$
7+
^\[main\.p3\] \(nexttime main\.x == 1\) and main\.x == 0: PROVED$
8+
^\[main\.p4\] \(main\.x == 0 and main\.x != 10\) |=> main\.x == 1: PROVED$
99
^EXIT=10$
1010
^SIGNAL=0$
1111
--

‎regression/verilog/SVA/sequence_and2.desc

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

4-
\[.*\] \(1 and \(##2 1\)\) \|-> main\.x == 2: PROVED up to bound 5$
5-
\[.*\] \(\(##2 1\) and 1\) \|-> main\.x == 2: PROVED up to bound 5$
4+
\[.*\] \(1 and \(##2 1\)\) \|-> main\.x == 2: PROVED$
5+
\[.*\] \(\(##2 1\) and 1\) \|-> main\.x == 2: PROVED$
66
^EXIT=0$
77
^SIGNAL=0$
88
--

‎regression/verilog/SVA/sequence_and3.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ sequence_and3.sv
33

44
^\[.*\] \(\(1 or \(##2 1\)\) and 1\) \|-> main\.x == 2: REFUTED$
55
^\[.*\] \(1 and \(1 or \(##2 1\)\)\) \|-> main\.x == 2: REFUTED$
6-
^\[.*\] \(\(1 or \(##2 1\)\) and 1\) \|-> main\.x == 0 \|\| main\.x == 2: PROVED up to bound 5$
7-
^\[.*\] \(1 and \(1 or \(##2 1\)\)\) \|-> main\.x == 0 \|\| main\.x == 2: PROVED up to bound 5$
6+
^\[.*\] \(\(1 or \(##2 1\)\) and 1\) \|-> main\.x == 0 \|\| main\.x == 2: PROVED$
7+
^\[.*\] \(1 and \(1 or \(##2 1\)\)\) \|-> main\.x == 0 \|\| main\.x == 2: PROVED$
88
^EXIT=10$
99
^SIGNAL=0$
1010
--

‎regression/verilog/SVA/sequence_or1.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ sequence_or1.sv
33

44
^\[main\.p0\] main\.x == 0 or main\.x == 1: PROVED$
55
^\[main\.p1\] strong\(main\.x == 0 or main\.x == 1\): PROVED$
6-
^\[main\.p2\] main\.x == 0 or \(nexttime main\.x == 1\): PROVED up to bound \d+$
7-
^\[main\.p3\] \(nexttime main\.x == 1\) or main\.x == 1: PROVED up to bound \d+$
8-
^\[main\.p4\] \(main\.x == 0 or main\.x != 10\) |=> main\.x == 1: PROVED up to bound \d+$
6+
^\[main\.p2\] main\.x == 0 or \(nexttime main\.x == 1\): PROVED$
7+
^\[main\.p3\] \(nexttime main\.x == 1\) or main\.x == 1: PROVED$
8+
^\[main\.p4\] \(main\.x == 0 or main\.x != 10\) |=> main\.x == 1: PROVED$
99
^EXIT=0$
1010
^SIGNAL=0$
1111
--

‎regression/verilog/SVA/sequence_repetition4.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
sequence_repetition4.sv
33

4-
^\[main\.p0\] \(main\.x == 0 ##1 main\.x == 1\) \[\*2\]: PROVED up to bound \d+$
4+
^\[main\.p0\] \(main\.x == 0 ##1 main\.x == 1\) \[\*2\]: PROVED$
55
^\[main\.p1\] \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 0\) \[\*2\]: REFUTED$
66
^EXIT=10$
77
^SIGNAL=0$

‎src/ebmc/completeness_threshold.cpp

Lines changed: 46 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -16,16 +16,20 @@ Author: Daniel Kroening, [email protected]
1616

1717
#include "bmc.h"
1818

19-
bool has_low_completeness_threshold(const exprt &expr)
19+
// counting number of transitions
20+
std::optional<mp_integer> completeness_threshold(const exprt &expr)
2021
{
2122
if(!has_temporal_operator(expr))
2223
{
23-
return true; // state predicate only
24+
return 0; // state predicate only
2425
}
2526
else if(expr.id() == ID_X)
2627
{
2728
// X p
28-
return !has_temporal_operator(to_X_expr(expr).op());
29+
if(has_temporal_operator(to_X_expr(expr).op()))
30+
return {};
31+
else
32+
return 1;
2933
}
3034
else if(
3135
expr.id() == ID_sva_nexttime || expr.id() == ID_sva_s_nexttime ||
@@ -41,11 +45,12 @@ bool has_low_completeness_threshold(const exprt &expr)
4145
return false;
4246
else if(always_expr.upper().is_constant())
4347
{
44-
auto lower_int = numeric_cast_v<mp_integer>(always_expr.lower());
4548
auto upper_int =
4649
numeric_cast_v<mp_integer>(to_constant_expr(always_expr.upper()));
47-
return lower_int >= 0 && lower_int <= 1 && upper_int >= 0 &&
48-
upper_int <= 1;
50+
if(upper_int < 0)
51+
return {};
52+
else
53+
return upper_int;
4954
}
5055
else
5156
return false;
@@ -57,29 +62,38 @@ bool has_low_completeness_threshold(const exprt &expr)
5762
return false;
5863
else
5964
{
60-
auto lower_int = numeric_cast_v<mp_integer>(s_always_expr.lower());
6165
auto upper_int = numeric_cast_v<mp_integer>(s_always_expr.upper());
62-
return lower_int >= 0 && lower_int <= 1 && upper_int >= 0 &&
63-
upper_int <= 1;
66+
if(upper_int < 0)
67+
return {};
68+
else
69+
return upper_int;
6470
}
6571
}
6672
else if(
6773
expr.id() == ID_sva_strong || expr.id() == ID_sva_weak ||
6874
expr.id() == ID_sva_implicit_strong || expr.id() == ID_sva_implicit_weak)
6975
{
7076
auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
71-
return has_low_completeness_threshold(sequence);
77+
return completeness_threshold(sequence);
7278
}
7379
else if(expr.id() == ID_sva_boolean)
7480
{
75-
return true;
81+
return 0; // state predicate only
7682
}
7783
else if(expr.id() == ID_sva_or || expr.id() == ID_sva_and)
7884
{
85+
mp_integer max_ct = 0;
86+
7987
for(auto &op : expr.operands())
80-
if(!has_low_completeness_threshold(op))
81-
return false;
82-
return true;
88+
{
89+
auto ct_op = completeness_threshold(op);
90+
if(ct_op.has_value())
91+
max_ct = std::max(*ct_op, max_ct);
92+
else
93+
return {}; // no CT
94+
}
95+
96+
return max_ct;
8397
}
8498
else if(expr.id() == ID_sva_sequence_property)
8599
{
@@ -89,17 +103,23 @@ bool has_low_completeness_threshold(const exprt &expr)
89103
return false;
90104
}
91105

92-
bool has_low_completeness_threshold(const ebmc_propertiest::propertyt &property)
106+
std::optional<mp_integer> completeness_threshold(const ebmc_propertiest::propertyt &property)
93107
{
94-
return has_low_completeness_threshold(property.normalized_expr);
108+
return completeness_threshold(property.normalized_expr);
95109
}
96110

97-
bool have_low_completeness_threshold(const ebmc_propertiest &properties)
111+
std::optional<mp_integer> completeness_threshold(const ebmc_propertiest &properties)
98112
{
113+
std::optional<mp_integer> max_ct;
114+
99115
for(auto &property : properties.properties)
100-
if(has_low_completeness_threshold(property))
101-
return true;
102-
return false;
116+
{
117+
auto ct_opt = completeness_threshold(property);
118+
if(ct_opt.has_value())
119+
max_ct = std::max(max_ct.value_or(0), *ct_opt);
120+
}
121+
122+
return max_ct;
103123
}
104124

105125
property_checker_resultt completeness_threshold(
@@ -110,13 +130,15 @@ property_checker_resultt completeness_threshold(
110130
message_handlert &message_handler)
111131
{
112132
// Do we have an eligibile property?
113-
if(!have_low_completeness_threshold(properties))
133+
auto ct_opt = completeness_threshold(properties);
134+
135+
if(!ct_opt.has_value())
114136
return property_checker_resultt{properties}; // give up
115137

116138
// Do BMC with two timeframes
117139
auto result = bmc(
118-
1, // bound
119-
false, // convert_only
140+
numeric_cast_v<std::size_t>(*ct_opt), // bound
141+
false, // convert_only
120142
cmdline.isset("bmc-with-assumptions"),
121143
transition_system,
122144
properties,
@@ -128,7 +150,7 @@ property_checker_resultt completeness_threshold(
128150
if(property.is_proved_with_bound())
129151
{
130152
// Turn "PROVED up to bound k" into "PROVED" if k>=CT
131-
if(has_low_completeness_threshold(property) && property.bound >= 1)
153+
if(completeness_threshold(property).has_value())
132154
property.proved();
133155
else
134156
property.unknown();

0 commit comments

Comments
 (0)