Merge pull request #665 from diffblue/indexed_nexttime

SVA: implement indexed nexttime

Author: tautschnig

regression/verilog/SVA/nexttime1.desc

@@ -1,10 +1,10 @@
-KNOWNBUG
+CORE
 nexttime1.sv
 --module main --bound 10
-^\[main\.assert\.1\] s_nexttime\[0\] main\.counter == 0: PROVED up to bound 10$
-^\[main\.assert\.2\] s_nexttime\[1\] main\.counter == 1: PROVED up to bound 10$
-^\[main\.assert\.3\] nexttime\[8\] main\.counter == 8: PROVED up to bound 10$
-^EXIT=10$
+^\[main\.p1\] s_nexttime\[0\] main\.counter == 0: PROVED up to bound 10$
+^\[main\.p2\] s_nexttime\[1\] main\.counter == 1: PROVED up to bound 10$
+^\[main\.p3\] nexttime\[8\] main\.counter == 8: PROVED up to bound 10$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

src/temporal-logic/normalize_property.cpp

@@ -151,12 +151,20 @@ exprt normalize_property(exprt expr)
     expr = normalize_pre_sva_or(to_sva_or_expr(expr));
   else if(expr.id() == ID_sva_nexttime)
   {
-    if(!to_sva_nexttime_expr(expr).is_indexed())
-      expr = X_exprt{to_sva_nexttime_expr(expr).op()};
+    auto &nexttime_expr = to_sva_nexttime_expr(expr);
+    if(nexttime_expr.is_indexed())
+      expr = sva_ranged_always_exprt{
+        nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()};
+    else
+      expr = X_exprt{nexttime_expr.op()};
   }
   else if(expr.id() == ID_sva_s_nexttime)
   {
-    if(!to_sva_s_nexttime_expr(expr).is_indexed())
+    auto &nexttime_expr = to_sva_s_nexttime_expr(expr);
+    if(nexttime_expr.is_indexed())
+      expr = sva_s_always_exprt{
+        nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()};
+    else
       expr = X_exprt{to_sva_s_nexttime_expr(expr).op()};
   }
   else if(expr.id() == ID_sva_cycle_delay)

src/temporal-logic/normalize_property.h

@@ -22,7 +22,9 @@ Author: Daniel Kroening, [email protected]
 /// sva_overlapped_implication --> ¬a ∨ b       if a and b are not SVA sequences
 /// sva_non_overlapped_implication --> ¬a ∨ Xb  if a and b are not SVA sequences
 /// sva_nexttime φ --> Xφ
+/// sva_nexttime[i] φ --> sva_always[i:i] φ
 /// sva_s_nexttime φ --> Xφ
+/// sva_s_nexttime[i] φ --> sva_s_always[i:i] φ
 /// sva_if --> ? :
 /// a sva_disable_iff b --> a ∨ b
 /// a sva_accept_on b --> a ∨ b

src/verilog/sva_expr.h

@@ -324,7 +324,7 @@ class sva_ranged_always_exprt : public sva_ranged_predicate_exprt
 public:
   sva_ranged_always_exprt(exprt lower, exprt upper, exprt op)
     : sva_ranged_predicate_exprt(
-        ID_sva_always,
+        ID_sva_ranged_always,
         std::move(lower),
         std::move(upper),
         std::move(op))