diff --git a/regression/verilog/SVA/s_eventually2.desc b/regression/verilog/SVA/s_eventually2.desc index ddef5abf1..4ae02f506 100644 --- a/regression/verilog/SVA/s_eventually2.desc +++ b/regression/verilog/SVA/s_eventually2.desc @@ -1,7 +1,9 @@ CORE s_eventually2.sv --module main --bound 20 -^EXIT=0$ +^\[main\.p0\] always s_eventually main.reset \|\| main\.counter == 10: PROVED up to bound 20$ +^\[main\.p1\] always \(s_eventually \[0:2\] main.reset \|\| main\.counter == 10\): REFUTED$ +^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/verilog/SVA/s_eventually2.sv b/regression/verilog/SVA/s_eventually2.sv index aa53a7dda..c0bf9d118 100644 --- a/regression/verilog/SVA/s_eventually2.sv +++ b/regression/verilog/SVA/s_eventually2.sv @@ -15,4 +15,7 @@ module main(input clk, input reset); // expected to pass for any bound p0: assert property (s_eventually (reset || counter == 10)); + // expected to fail, owing to range + p1: assert property (s_eventually[0:2] (reset || counter == 10)); + endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index c8343a7a0..77e9ac37f 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -46,6 +46,7 @@ IREP_ID_ONE(sva_nexttime) IREP_ID_ONE(sva_s_nexttime) IREP_ID_ONE(sva_eventually) IREP_ID_ONE(sva_s_eventually) +IREP_ID_ONE(sva_ranged_s_eventually) IREP_ID_ONE(sva_until) IREP_ID_ONE(sva_s_until) IREP_ID_ONE(sva_until_with) diff --git a/src/trans-word-level/instantiate_word_level.cpp b/src/trans-word-level/instantiate_word_level.cpp index 49f580104..46fac41e2 100644 --- a/src/trans-word-level/instantiate_word_level.cpp +++ b/src/trans-word-level/instantiate_word_level.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -428,6 +429,45 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); return {no_timeframes - 1, conjunction(conjuncts)}; } + else if(expr.id() == ID_sva_ranged_s_eventually) + { + auto &phi = to_sva_ranged_s_eventually_expr(expr).op(); + auto &lower = to_sva_ranged_s_eventually_expr(expr).lower(); + auto &upper = to_sva_ranged_s_eventually_expr(expr).upper(); + + auto from_opt = numeric_cast(lower); + if(!from_opt.has_value()) + throw ebmc_errort() << "failed to convert SVA s_eventually from index"; + + auto from = t + std::max(mp_integer{0}, *from_opt); + + mp_integer to; + + if(upper.id() == ID_infinity) + { + throw ebmc_errort() + << "failed to convert SVA s_eventually to index (infinity)"; + } + else + { + auto to_opt = numeric_cast(upper); + if(!to_opt.has_value()) + throw ebmc_errort() << "failed to convert SVA s_eventually to index"; + to = std::min(t + *to_opt, no_timeframes - 1); + } + + exprt::operandst disjuncts; + mp_integer time = 0; + + for(mp_integer c = from; c <= to; ++c) + { + auto tmp = instantiate_property(phi, c, no_timeframes, ns); + time = std::max(time, tmp.first); + disjuncts.push_back(tmp.second); + } + + return {time, disjunction(disjuncts)}; + } else if(expr.id()==ID_sva_until || expr.id()==ID_sva_s_until) { diff --git a/src/trans-word-level/obligations.h b/src/trans-word-level/obligations.h index b3d4c7e92..84eaa69a9 100644 --- a/src/trans-word-level/obligations.h +++ b/src/trans-word-level/obligations.h @@ -19,6 +19,11 @@ class obligationst public: obligationst() = default; + explicit obligationst(const mp_integer &t, const exprt &expr) + { + add(t, expr); + } + explicit obligationst(const std::pair &pair) { add(pair.first, pair.second); diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 8a8d71971..dd3f6bda1 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -1521,6 +1521,11 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) return precedence = verilog_precedencet::MIN, convert_sva_unary("s_eventually", to_sva_s_eventually_expr(src)); + else if(src.id() == ID_sva_ranged_s_eventually) + return precedence = verilog_precedencet::MIN, + convert_sva_ranged_predicate( + "s_eventually", to_sva_ranged_s_eventually_expr(src)); + else if(src.id()==ID_sva_until) return precedence = verilog_precedencet::MIN, convert_sva_binary("until", to_sva_until_expr(src)); diff --git a/src/verilog/parser.y b/src/verilog/parser.y index c87acbd2c..7a284cdb1 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2197,7 +2197,7 @@ property_expr_proper: | "eventually" '[' constant_range ']' property_expr %prec "eventually" { init($$, ID_sva_eventually); swapop($$, $3); mto($$, $5); } | "s_eventually" '[' cycle_delay_const_range_expression ']' property_expr %prec "s_eventually" - { init($$, ID_sva_s_eventually); swapop($$, $3); mto($$, $5); } + { init($$, ID_sva_ranged_s_eventually); swapop($$, $3); mto($$, $5); } | property_expr "until" property_expr { init($$, "sva_until"); mto($$, $1); mto($$, $3); } | property_expr "s_until" property_expr diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 2885b3735..d353c7db2 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -296,6 +296,35 @@ static inline sva_s_eventually_exprt &to_sva_s_eventually_expr(exprt &expr) return static_cast(expr); } +class sva_ranged_s_eventually_exprt : public sva_ranged_predicate_exprt +{ +public: + explicit sva_ranged_s_eventually_exprt(exprt lower, exprt upper, exprt op) + : sva_ranged_predicate_exprt( + ID_sva_s_eventually, + std::move(lower), + std::move(upper), + std::move(op)) + { + } +}; + +static inline const sva_ranged_s_eventually_exprt & +to_sva_ranged_s_eventually_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_ranged_s_eventually); + sva_ranged_s_eventually_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +static inline sva_ranged_s_eventually_exprt & +to_sva_ranged_s_eventually_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_ranged_s_eventually); + sva_ranged_s_eventually_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + class sva_always_exprt : public unary_predicate_exprt { public: diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 0b44855cd..6a331f3e4 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -3108,8 +3108,8 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr) return std::move(expr); } else if( - expr.id() == ID_sva_eventually || expr.id() == ID_sva_ranged_always || - expr.id() == ID_sva_s_always) + expr.id() == ID_sva_eventually || expr.id() == ID_sva_ranged_s_eventually || + expr.id() == ID_sva_s_always || expr.id() == ID_sva_ranged_always) { auto lower = convert_integer_constant_expression(expr.op0());