SVA: add implementation for ranged always and s_always to instantiate_property

This adds an implementation for ranged always and s_always to the word-level
BMC instantiate_property module.

Author: kroening

regression/verilog/SVA/always_with_range1.desc

@@ -4,6 +4,7 @@ always_with_range1.sv
 ^\[main\.p0\] always \[0:9\] main\.x < 10: PROVED up to bound 20$
 ^\[main\.p1\] always \[0:\$\] main\.x < 10: REFUTED$
 ^\[main\.p2\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$
+^\[main\.p3\] always \(main\.x == 1 implies \(always \[1:1\] main\.x == 2\)\): PROVED up to bound 20$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/always_with_range1.sv

@@ -17,4 +17,7 @@ module main;
   // strong variant
   initial p2: assert property (s_always [0:9] x<10);
 
+  // nested
+  p3: assert property (always (x==1 implies always [1:1] x==2));
+
 endmodule

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>
@@ -350,6 +351,47 @@ 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_always || expr.id() == ID_sva_s_always)
+  {
+    auto &phi = expr.id() == ID_sva_ranged_always
+                  ? to_sva_ranged_always_expr(expr).op()
+                  : to_sva_s_always_expr(expr).op();
+    auto &lower = expr.id() == ID_sva_ranged_always
+                    ? to_sva_ranged_always_expr(expr).lower()
+                    : to_sva_s_always_expr(expr).lower();
+    auto &upper = expr.id() == ID_sva_ranged_always
+                    ? to_sva_ranged_always_expr(expr).upper()
+                    : to_sva_s_always_expr(expr).upper();
+
+    auto from_opt = numeric_cast<mp_integer>(lower);
+    if(!from_opt.has_value())
+      throw ebmc_errort() << "failed to convert SVA always from index";
+
+    auto from = t + std::max(mp_integer{0}, *from_opt);
+
+    mp_integer to;
+
+    if(upper.id() == ID_infinity)
+    {
+      to = no_timeframes - 1;
+    }
+    else
+    {
+      auto to_opt = numeric_cast<mp_integer>(upper);
+      if(!to_opt.has_value())
+        throw ebmc_errort() << "failed to convert SVA always to index";
+      to = std::min(t + *to_opt, no_timeframes - 1);
+    }
+
+    exprt::operandst conjuncts;
+
+    for(mp_integer c = from; c <= to; ++c)
+    {
+      conjuncts.push_back(instantiate_rec(phi, c).second);
+    }
+
+    return {to, conjunction(conjuncts)};
+  }
   else if(expr.id() == ID_X)
   {
     const auto next = t + 1;