Merge pull request #1034 from diffblue/sequence_repetition6

SVA: `[*]`, `[+]` and `[*x:y]` require sequence arguments

Author: tautschnig

regression/verilog/SVA/sequence_repetition6.desc

@@ -0,0 +1,8 @@
+CORE
+sequence_repetition6.sv
+
+^file .* line 4: sequence required$
+^EXIT=2$
+^SIGNAL=0$
+--
+--

regression/verilog/SVA/sequence_repetition6.sv

@@ -0,0 +1,6 @@
+module main(input clk);
+
+  // Sequence repetition requires a sequence argument.
+  assert property ((s_nexttime 1)[*]);
+
+endmodule

src/verilog/verilog_typecheck_sva.cpp

@@ -28,15 +28,26 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr)
     expr.id() == ID_sva_cycle_delay_plus ||
     expr.id() == ID_sva_cycle_delay_star || expr.id() == ID_sva_weak ||
     expr.id() == ID_sva_strong || expr.id() == ID_sva_nexttime ||
-    expr.id() == ID_sva_s_nexttime ||
-    expr.id() == ID_sva_sequence_repetition_plus ||
-    expr.id() == ID_sva_sequence_repetition_star)
+    expr.id() == ID_sva_s_nexttime)
   {
     convert_sva(expr.op());
     make_boolean(expr.op());
     expr.type() = bool_typet();
     return std::move(expr);
   }
+  else if(
+    expr.id() == ID_sva_sequence_repetition_plus || // x[+]
+    expr.id() == ID_sva_sequence_repetition_star)   // x[*}
+  {
+    // These both take a sequence as argument.
+    // The grammar allows properties to implement and/or over
+    // sequences. Check here that the argument is a sequence.
+    convert_sva(expr.op());
+    require_sva_sequence(expr.op());
+    make_boolean(expr.op());
+    expr.type() = bool_typet{};
+    return std::move(expr);
+  }
   else
   {
     // not SVA
@@ -260,7 +271,11 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr)
   {
     auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr);
 
+    // This expression takes a sequence as argument.
+    // The grammar allows properties to implement and/or over
+    // sequences. Check here that the argument is a sequence.
     convert_sva(repetition.op());
+    require_sva_sequence(repetition.op());
     make_boolean(repetition.op());
 
     convert_expr(repetition.from());