Merge pull request #691 from diffblue/sva_ranged_s_eventually

SVA: implement ranged `s_eventually` operator

Author: kroening

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

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

src/hw_cbmc_irep_ids.h

@@ -48,6 +48,7 @@ IREP_ID_ONE(sva_s_nexttime)
 IREP_ID_ONE(sva_indexed_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)

src/trans-word-level/instantiate_word_level.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/ebmc_util.h>
 #include <util/expr_util.h>
 
+#include <ebmc/ebmc_error.h>
 #include <temporal-logic/temporal_expr.h>
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
@@ -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<mp_integer>(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<mp_integer>(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)
   {

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<mp_integer, exprt> &pair)
   {
     add(pair.first, pair.second);

src/verilog/expr2verilog.cpp

@@ -1530,6 +1530,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));

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

src/verilog/sva_expr.h

@@ -341,6 +341,35 @@ static inline sva_s_eventually_exprt &to_sva_s_eventually_expr(exprt &expr)
   return static_cast<sva_s_eventually_exprt &>(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<const sva_ranged_s_eventually_exprt &>(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<sva_ranged_s_eventually_exprt &>(expr);
+}
+
 class sva_always_exprt : public unary_predicate_exprt
 {
 public:

src/verilog/verilog_typecheck_expr.cpp

@@ -3107,8 +3107,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());