Skip to content

Commit 1bf5a17

Browse files
committed
SVA: implement ranged s_eventually operator
This adds a BMC encoding for the ranged variant of the s_eventually operator.
1 parent 4a82eca commit 1bf5a17

File tree

9 files changed

+89
-4
lines changed

9 files changed

+89
-4
lines changed
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
CORE
22
s_eventually2.sv
33
--module main --bound 20
4-
^EXIT=0$
4+
^\[main\.p0\] always s_eventually main.reset \|\| main\.counter == 10: PROVED up to bound 20$
5+
^\[main\.p1\] always \(s_eventually \[0:2\] main.reset \|\| main\.counter == 10\): REFUTED$
6+
^EXIT=10$
57
^SIGNAL=0$
68
--
79
^warning: ignoring

regression/verilog/SVA/s_eventually2.sv

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,4 +15,7 @@ module main(input clk, input reset);
1515
// expected to pass for any bound
1616
p0: assert property (s_eventually (reset || counter == 10));
1717

18+
// expected to fail, owing to range
19+
p1: assert property (s_eventually[0:2] (reset || counter == 10));
20+
1821
endmodule

src/hw_cbmc_irep_ids.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ IREP_ID_ONE(sva_nexttime)
4646
IREP_ID_ONE(sva_s_nexttime)
4747
IREP_ID_ONE(sva_eventually)
4848
IREP_ID_ONE(sva_s_eventually)
49+
IREP_ID_ONE(sva_ranged_s_eventually)
4950
IREP_ID_ONE(sva_until)
5051
IREP_ID_ONE(sva_s_until)
5152
IREP_ID_ONE(sva_until_with)

src/trans-word-level/instantiate_word_level.cpp

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111
#include <util/ebmc_util.h>
1212
#include <util/expr_util.h>
1313

14+
#include <ebmc/ebmc_error.h>
1415
#include <temporal-logic/temporal_expr.h>
1516
#include <temporal-logic/temporal_logic.h>
1617
#include <verilog/sva_expr.h>
@@ -428,6 +429,45 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
428429
DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
429430
return {no_timeframes - 1, conjunction(conjuncts)};
430431
}
432+
else if(expr.id() == ID_sva_ranged_s_eventually)
433+
{
434+
auto &phi = to_sva_ranged_s_eventually_expr(expr).op();
435+
auto &lower = to_sva_ranged_s_eventually_expr(expr).lower();
436+
auto &upper = to_sva_ranged_s_eventually_expr(expr).upper();
437+
438+
auto from_opt = numeric_cast<mp_integer>(lower);
439+
if(!from_opt.has_value())
440+
throw ebmc_errort() << "failed to convert SVA s_eventually from index";
441+
442+
auto from = t + std::max(mp_integer{0}, *from_opt);
443+
444+
mp_integer to;
445+
446+
if(upper.id() == ID_infinity)
447+
{
448+
throw ebmc_errort()
449+
<< "failed to convert SVA s_eventually to index (infinity)";
450+
}
451+
else
452+
{
453+
auto to_opt = numeric_cast<mp_integer>(upper);
454+
if(!to_opt.has_value())
455+
throw ebmc_errort() << "failed to convert SVA s_eventually to index";
456+
to = std::min(t + *to_opt, no_timeframes - 1);
457+
}
458+
459+
exprt::operandst disjuncts;
460+
mp_integer time = 0;
461+
462+
for(mp_integer c = from; c <= to; ++c)
463+
{
464+
auto tmp = instantiate_property(phi, c, no_timeframes, ns);
465+
time = std::max(time, tmp.first);
466+
disjuncts.push_back(tmp.second);
467+
}
468+
469+
return {time, disjunction(disjuncts)};
470+
}
431471
else if(expr.id()==ID_sva_until ||
432472
expr.id()==ID_sva_s_until)
433473
{

src/trans-word-level/obligations.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,11 @@ class obligationst
1919
public:
2020
obligationst() = default;
2121

22+
explicit obligationst(const mp_integer &t, const exprt &expr)
23+
{
24+
add(t, expr);
25+
}
26+
2227
explicit obligationst(const std::pair<mp_integer, exprt> &pair)
2328
{
2429
add(pair.first, pair.second);

src/verilog/expr2verilog.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1521,6 +1521,11 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
15211521
return precedence = verilog_precedencet::MIN,
15221522
convert_sva_unary("s_eventually", to_sva_s_eventually_expr(src));
15231523

1524+
else if(src.id() == ID_sva_ranged_s_eventually)
1525+
return precedence = verilog_precedencet::MIN,
1526+
convert_sva_ranged_predicate(
1527+
"s_eventually", to_sva_ranged_s_eventually_expr(src));
1528+
15241529
else if(src.id()==ID_sva_until)
15251530
return precedence = verilog_precedencet::MIN,
15261531
convert_sva_binary("until", to_sva_until_expr(src));

src/verilog/parser.y

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2197,7 +2197,7 @@ property_expr_proper:
21972197
| "eventually" '[' constant_range ']' property_expr %prec "eventually"
21982198
{ init($$, ID_sva_eventually); swapop($$, $3); mto($$, $5); }
21992199
| "s_eventually" '[' cycle_delay_const_range_expression ']' property_expr %prec "s_eventually"
2200-
{ init($$, ID_sva_s_eventually); swapop($$, $3); mto($$, $5); }
2200+
{ init($$, ID_sva_ranged_s_eventually); swapop($$, $3); mto($$, $5); }
22012201
| property_expr "until" property_expr
22022202
{ init($$, "sva_until"); mto($$, $1); mto($$, $3); }
22032203
| property_expr "s_until" property_expr

src/verilog/sva_expr.h

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -296,6 +296,35 @@ static inline sva_s_eventually_exprt &to_sva_s_eventually_expr(exprt &expr)
296296
return static_cast<sva_s_eventually_exprt &>(expr);
297297
}
298298

299+
class sva_ranged_s_eventually_exprt : public sva_ranged_predicate_exprt
300+
{
301+
public:
302+
explicit sva_ranged_s_eventually_exprt(exprt lower, exprt upper, exprt op)
303+
: sva_ranged_predicate_exprt(
304+
ID_sva_s_eventually,
305+
std::move(lower),
306+
std::move(upper),
307+
std::move(op))
308+
{
309+
}
310+
};
311+
312+
static inline const sva_ranged_s_eventually_exprt &
313+
to_sva_ranged_s_eventually_expr(const exprt &expr)
314+
{
315+
PRECONDITION(expr.id() == ID_sva_ranged_s_eventually);
316+
sva_ranged_s_eventually_exprt::check(expr, validation_modet::INVARIANT);
317+
return static_cast<const sva_ranged_s_eventually_exprt &>(expr);
318+
}
319+
320+
static inline sva_ranged_s_eventually_exprt &
321+
to_sva_ranged_s_eventually_expr(exprt &expr)
322+
{
323+
PRECONDITION(expr.id() == ID_sva_ranged_s_eventually);
324+
sva_ranged_s_eventually_exprt::check(expr, validation_modet::INVARIANT);
325+
return static_cast<sva_ranged_s_eventually_exprt &>(expr);
326+
}
327+
299328
class sva_always_exprt : public unary_predicate_exprt
300329
{
301330
public:

src/verilog/verilog_typecheck_expr.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3108,8 +3108,8 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr)
31083108
return std::move(expr);
31093109
}
31103110
else if(
3111-
expr.id() == ID_sva_eventually || expr.id() == ID_sva_ranged_always ||
3112-
expr.id() == ID_sva_s_always)
3111+
expr.id() == ID_sva_eventually || expr.id() == ID_sva_ranged_s_eventually ||
3112+
expr.id() == ID_sva_s_always || expr.id() == ID_sva_ranged_always)
31133113
{
31143114
auto lower = convert_integer_constant_expression(expr.op0());
31153115

0 commit comments

Comments
 (0)