Merge pull request #1185 from diffblue/sequence_not1-fix

SVA: `not`/`implies`/`iff` operators yield a property

Author: tautschnig

regression/verilog/SVA/sequence_not1.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 sequence_not1.sv
 
-^EXIT=0$
+^file .* line 9: sequence required, but got property$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The grammar for 'SVA sequence not' is missing.

regression/verilog/SVA/sequence_not1.sv

@@ -5,10 +5,7 @@ module main(input clk);
   always @(posedge clk)
     x<=x+1;
 
-  // should pass
-  initial p0: assert property (not x == 1);
-
-  // Given a sequence, 'not' yields a sequence, not a property
-  initial p1: assert property ((not x == 1)[*1]);
+  // Given a sequence, 'not' yields a property, not a sequence
+  assert property ((not x == 1)[*1]);
 
 endmodule

src/verilog/verilog_typecheck_sva.cpp

@@ -28,7 +28,9 @@ void verilog_typecheck_exprt::require_sva_sequence(exprt &expr)
     type.id() == ID_signedbv || type.id() == ID_verilog_unsignedbv ||
     type.id() == ID_verilog_signedbv)
   {
-    if(has_temporal_operator(expr))
+    if(
+      has_temporal_operator(expr) || expr.id() == ID_sva_not ||
+      expr.id() == ID_sva_implies || expr.id() == ID_sva_iff)
     {
       throw errort().with_location(expr.source_location())
         << "sequence required, but got property";