SystemVerilog: property-typed ports for checkers

regression/verilog/checker/checker3.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 checker3.sv
 --bound 20
 ^\[main\.c\.assert\.1\] always myChecker\.data != 10: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 --
-Support for property parameters for checkers is missing.

src/hw_cbmc_irep_ids.h

@@ -161,6 +161,7 @@ IREP_ID_ONE(verilog_indexed_part_select_plus)
 IREP_ID_ONE(verilog_indexed_part_select_minus)
 IREP_ID_ONE(verilog_past)
 IREP_ID_ONE(verilog_property_declaration)
+IREP_ID_ONE(verilog_property)
 IREP_ID_ONE(verilog_scope_prefix)
 IREP_ID_ONE(verilog_sequence_declaration)
 IREP_ID_ONE(verilog_sequence)

src/verilog/parser.y

@@ -773,9 +773,19 @@ checker_port_list_opt:
 
 checker_port_list:
           checker_port_item
-                { init($$); mts($$, $1); }
+                {
+                  // No direction on declaration? Defaults to 'input'.
+                  auto &decl = stack_expr($1);
+                  if(decl.get(ID_class) == irep_idt{})
+                    decl.set(ID_class, ID_input);
+                  init($$);
+                  mts($$, $1);
+                }
         | checker_port_list ',' checker_port_item
-                { $$ = $1; mts($$, $3); }
+                {
+                  $$ = $1;
+                  mts($$, $3);
+                }
         ;
 
 checker_port_item:
@@ -2569,6 +2579,7 @@ property_port_item:
 property_formal_type:
           sequence_formal_type
         | TOK_PROPERTY
+                { init($$, ID_verilog_property); }
         ;
 
 property_spec:

src/verilog/verilog_elaborate_type.cpp

@@ -533,6 +533,10 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
     tmp.set(ID_C_const, true);
     return tmp;
   }
+  else if(src.id() == ID_verilog_property)
+  {
+    return src;
+  }
   else
   {
     throw errort().with_location(source_location)

src/verilog/verilog_typecheck_expr.cpp

@@ -301,6 +301,12 @@ void verilog_typecheck_exprt::assignment_conversion(
   if(lhs_type == rhs.type())
     return;
 
+  if(lhs_type.id() == ID_verilog_property)
+  {
+    rhs = typecast_exprt::conditional_cast(rhs, lhs_type);
+    return;
+  }
+
   if(lhs_type.id() == ID_struct && !lhs_type.get_bool(ID_packed))
   {
     // assignment of a non-matching type to unpacked struct

src/verilog/verilog_typecheck_sva.cpp

@@ -70,6 +70,11 @@ void verilog_typecheck_exprt::require_sva_property(exprt &expr)
   {
     // good as is
   }
+  else if(type.id() == ID_verilog_property)
+  {
+    // checker property formal port -- treat as SVA property
+    expr.type() = verilog_sva_property_typet{};
+  }
   else if(
     type.id() == ID_bool || type.id() == ID_unsignedbv ||
     type.id() == ID_signedbv || type.id() == ID_verilog_unsignedbv ||