Verilog: reject use of SVA sequences and properties as Boolean expression

SVA named sequences and named properties cannot be used as Booleans.  This
adds a check.

Author: kroening

regression/verilog/property/named_property5.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 named_property5.sv
 
+^file .* line 8: cannot use SVA property as an expression$
 ^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This should be rejected.

regression/verilog/property/named_property6.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 named_property6.sv
 
 ^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This should be rejected.

regression/verilog/property/named_property7.desc

@@ -0,0 +1,8 @@
+CORE
+named_property7.sv
+
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/property/named_property7.sv

@@ -0,0 +1,10 @@
+module main;
+
+  property P;
+    1
+  endproperty
+
+  // This should be rejected
+  wire x = P + P;
+
+endmodule

src/verilog/verilog_typecheck_expr.cpp

@@ -121,6 +121,17 @@ void verilog_typecheck_exprt::propagate_type(
   if(expr.type()==type)
     return;
 
+  if(expr.type().id() == ID_verilog_sva_sequence)
+  {
+    throw errort{}.with_location(expr.source_location())
+      << "cannot use SVA sequence as an expression";
+  }
+  else if(expr.type().id() == ID_verilog_sva_property)
+  {
+    throw errort{}.with_location(expr.source_location())
+      << "cannot use SVA property as an expression";
+  }
+
   vtypet vt_from=vtypet(expr.type());
   vtypet vt_to  =vtypet(type);
 
@@ -2174,8 +2185,19 @@ Function: verilog_typecheck_exprt::make_boolean
 
 void verilog_typecheck_exprt::make_boolean(exprt &expr)
 {
-  if(expr.type().id()!=ID_bool)
+  if(expr.type().id() == ID_verilog_sva_sequence)
+  {
+    throw errort{}.with_location(expr.source_location())
+      << "cannot use SVA sequence as an expression";
+  }
+  else if(expr.type().id() == ID_verilog_sva_property)
+  {
+    throw errort{}.with_location(expr.source_location())
+      << "cannot use SVA property as an expression";
+  }
+  else if(expr.type().id() != ID_bool)
   {
+    // everything else can be converted to Boolean
     mp_integer value;
     if(!to_integer_non_constant(expr, value))
       expr = make_boolean_expr(value != 0);