Verilog SVA: indexed nexttime and s_nexttime

regression/verilog/SVA/nexttime1.desc

@@ -0,0 +1,12 @@
+KNOWNBUG
+nexttime1.sv
+--module main --bound 10
+^\[main\.property\.1\] s_nexttime\[0\] main\.counter == 0: PROVED up to bound 10$
+^\[main\.property\.2\] s_nexttime\[1\] main\.counter == 1: PROVED up to bound 10$
+^\[main\.property\.3\] nexttime\[8\] main\.counter == 8: PROVED up to bound 10$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Backend support missing.

regression/verilog/SVA/nexttime1.sv

@@ -0,0 +1,23 @@
+module main(input clk);
+
+  // count up from 0 to 10
+  reg [7:0] counter;
+
+  initial counter = 0;
+
+  always @(posedge clk)
+    if(counter == 10)
+      counter = 0;
+    else
+      counter = counter + 1;
+
+  // expected to pass
+  initial p1: assert property (s_nexttime[0] counter == 0);
+
+  // expected to pass
+  initial p2: assert property (s_nexttime[1] counter == 1);
+
+  // expected to pass
+  initial p3: assert property (nexttime[8] counter == 8);
+
+endmodule

src/temporal-logic/negate_property.cpp

@@ -93,7 +93,7 @@ exprt negate_property(const exprt &expr)
   }
   else if(expr.id() == ID_sva_nexttime)
   {
-    unary_exprt result = to_sva_nexttime_expr(expr);
+    auto result = to_sva_nexttime_expr(expr);
     result.op() = negate_property(result.op());
     return std::move(result);
   }

src/temporal-logic/normalize_property.cpp

@@ -112,9 +112,15 @@ exprt normalize_property(exprt expr)
     expr = normalize_pre_sva_non_overlapped_implication(
       to_sva_non_overlapped_implication_expr(expr));
   else if(expr.id() == ID_sva_nexttime)
-    expr = X_exprt{to_sva_nexttime_expr(expr).op()};
+  {
+    if(!to_sva_nexttime_expr(expr).is_indexed())
+      expr = X_exprt{to_sva_nexttime_expr(expr).op()};
+  }
   else if(expr.id() == ID_sva_s_nexttime)
-    expr = X_exprt{to_sva_s_nexttime_expr(expr).op()};
+  {
+    if(!to_sva_s_nexttime_expr(expr).is_indexed())
+      expr = X_exprt{to_sva_s_nexttime_expr(expr).op()};
+  }
   else if(expr.id() == ID_sva_cycle_delay)
     expr = normalize_pre_sva_cycle_delay(to_sva_cycle_delay_expr(expr));
   else if(expr.id() == ID_sva_cycle_delay_plus)

src/verilog/expr2verilog.cpp

@@ -430,7 +430,7 @@ std::string expr2verilogt::convert_sva_unary(
 
 /*******************************************************************\
 
-Function: expr2verilogt::convert_sva
+Function: expr2verilogt::convert_sva_binary
 
   Inputs:
 
@@ -459,6 +459,35 @@ std::string expr2verilogt::convert_sva_binary(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_sva_indexed_binary
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string expr2verilogt::convert_sva_indexed_binary(
+  const std::string &name,
+  const binary_exprt &expr)
+{
+  std::string s0;
+
+  if(expr.op0().is_not_nil())
+    s0 = '[' + convert(expr.lhs()) + ']';
+
+  unsigned p1;
+  auto s1 = convert(expr.rhs(), p1);
+  if(p1 == 0)
+    s1 = "(" + s1 + ")";
+
+  return name + s0 + ' ' + s1;
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_replication
 
   Inputs:
@@ -1161,11 +1190,11 @@ std::string expr2verilogt::convert(
 
   else if(src.id()==ID_sva_nexttime)
     return precedence = 0,
-           convert_sva_unary("nexttime", to_sva_nexttime_expr(src));
+           convert_sva_indexed_binary("nexttime", to_sva_nexttime_expr(src));
 
   else if(src.id()==ID_sva_s_nexttime)
-    return precedence = 0,
-           convert_sva_unary("s_nexttime", to_sva_s_nexttime_expr(src));
+    return precedence = 0, convert_sva_indexed_binary(
+                             "s_nexttime", to_sva_s_nexttime_expr(src));
 
   else if(src.id()==ID_sva_eventually)
   {

src/verilog/expr2verilog_class.h

@@ -92,6 +92,9 @@ class expr2verilogt
 
   std::string convert_sva_binary(const std::string &name, const binary_exprt &);
 
+  std::string
+  convert_sva_indexed_binary(const std::string &name, const binary_exprt &);
+
   virtual std::string
   convert_replication(const replication_exprt &, unsigned precedence);
 

src/verilog/parser.y

@@ -2059,11 +2059,18 @@ property_expr_proper:
         | property_expr "and" property_expr { init($$, ID_and); mto($$, $1); mto($$, $3); }
         | property_expr "|->" property_expr { init($$, ID_sva_overlapped_implication); mto($$, $1); mto($$, $3); }
         | property_expr "|=>" property_expr { init($$, ID_sva_non_overlapped_implication); mto($$, $1); mto($$, $3); }
-        | "nexttime" property_expr          { init($$, "sva_nexttime"); mto($$, $2); }
-        | "s_nexttime" property_expr        { init($$, "sva_s_nexttime"); mto($$, $2); }
+        | "nexttime" property_expr
+		{ init($$, "sva_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); }
+        | "nexttime" '[' constant_expression ']' property_expr %prec "nexttime"
+		{ init($$, "sva_nexttime"); mto($$, $3); mto($$, $5); }
+        | "s_nexttime" property_expr
+		{ init($$, "sva_s_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); }
+        | "s_nexttime" '[' constant_expression ']' property_expr %prec "s_nexttime"
+		{ init($$, "sva_s_nexttime"); mto($$, $3); mto($$, $5); }
         | "always" '[' cycle_delay_const_range_expression ']' property_expr %prec "always"
 		{ init($$, ID_sva_ranged_always); swapop($$, $3); mto($$, $5); }
-        | "always" property_expr            { init($$, "sva_always"); mto($$, $2); }
+        | "always" property_expr
+		{ init($$, "sva_always"); mto($$, $2); }
         | "s_always" '[' constant_range ']' property_expr %prec "s_always"
 		{ init($$, ID_sva_s_always); swapop($$, $3); mto($$, $5); }
         | "s_eventually" property_expr

src/verilog/sva_expr.h

@@ -11,13 +11,43 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_expr.h>
 
-class sva_nexttime_exprt : public unary_predicate_exprt
+class sva_nexttime_exprt : public binary_predicate_exprt
 {
 public:
+  // nonindexed variant
   explicit sva_nexttime_exprt(exprt op)
-    : unary_predicate_exprt(ID_sva_nexttime, std::move(op))
+    : binary_predicate_exprt(nil_exprt(), ID_sva_nexttime, std::move(op))
   {
   }
+
+  bool is_indexed() const
+  {
+    return index().is_not_nil();
+  }
+
+  const exprt &index() const
+  {
+    return op0();
+  }
+
+  exprt &index()
+  {
+    return op0();
+  }
+
+  const exprt &op() const
+  {
+    return op1();
+  }
+
+  exprt &op()
+  {
+    return op1();
+  }
+
+protected:
+  using binary_predicate_exprt::op0;
+  using binary_predicate_exprt::op1;
 };
 
 static inline const sva_nexttime_exprt &to_sva_nexttime_expr(const exprt &expr)
@@ -34,13 +64,43 @@ static inline sva_nexttime_exprt &to_sva_nexttime_expr(exprt &expr)
   return static_cast<sva_nexttime_exprt &>(expr);
 }
 
-class sva_s_nexttime_exprt : public unary_predicate_exprt
+class sva_s_nexttime_exprt : public binary_predicate_exprt
 {
 public:
+  // nonindexed variant
   explicit sva_s_nexttime_exprt(exprt op)
-    : unary_predicate_exprt(ID_sva_s_nexttime, std::move(op))
+    : binary_predicate_exprt(nil_exprt(), ID_sva_s_nexttime, std::move(op))
   {
   }
+
+  bool is_indexed() const
+  {
+    return index().is_not_nil();
+  }
+
+  const exprt &index() const
+  {
+    return op0();
+  }
+
+  exprt &index()
+  {
+    return op0();
+  }
+
+  const exprt &op() const
+  {
+    return op1();
+  }
+
+  exprt &op()
+  {
+    return op1();
+  }
+
+protected:
+  using binary_predicate_exprt::op0;
+  using binary_predicate_exprt::op1;
 };
 
 static inline const sva_s_nexttime_exprt &

src/verilog/verilog_typecheck_expr.cpp

@@ -1905,8 +1905,7 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     expr.type() = expr.op().type();
   }
   else if(
-    expr.id() == ID_sva_always || expr.id() == ID_sva_nexttime ||
-    expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_s_eventually ||
+    expr.id() == ID_sva_always || expr.id() == ID_sva_s_eventually ||
     expr.id() == ID_sva_cycle_delay_plus ||
     expr.id() == ID_sva_cycle_delay_star)
   {
@@ -2237,6 +2236,30 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     return std::move(expr);
   }
+  else if(expr.id() == ID_sva_nexttime)
+  {
+    if(to_sva_nexttime_expr(expr).is_indexed())
+      convert_expr(to_sva_nexttime_expr(expr).index());
+
+    auto &op = to_sva_nexttime_expr(expr).op();
+    convert_expr(op);
+    make_boolean(op);
+    expr.type() = bool_typet();
+
+    return std::move(expr);
+  }
+  else if(expr.id() == ID_sva_s_nexttime)
+  {
+    if(to_sva_s_nexttime_expr(expr).is_indexed())
+      convert_expr(to_sva_s_nexttime_expr(expr).index());
+
+    auto &op = to_sva_s_nexttime_expr(expr).op();
+    convert_expr(op);
+    make_boolean(op);
+    expr.type() = bool_typet();
+
+    return std::move(expr);
+  }
   else if(expr.id()==ID_sva_overlapped_implication ||
           expr.id()==ID_sva_non_overlapped_implication ||
           expr.id()==ID_sva_until ||