SVA: type for named sequences and properties

This introduces a type for named sequences and properties, similar to the
type for functions and tasks.

Author: kroening

src/hw_cbmc_irep_ids.h

@@ -228,6 +228,8 @@ IREP_ID_ONE(verilog_always)
 IREP_ID_ONE(verilog_always_comb)
 IREP_ID_ONE(verilog_always_ff)
 IREP_ID_ONE(verilog_always_latch)
+IREP_ID_ONE(verilog_sva_named_property)
+IREP_ID_ONE(verilog_sva_named_sequence)
 IREP_ID_ONE(named_port_connection)
 IREP_ID_ONE(verilog_final)
 IREP_ID_ONE(initial)

src/verilog/verilog_typecheck.cpp

@@ -1805,6 +1805,8 @@ void verilog_typecheckt::convert_property_declaration(
   convert_sva(declaration.cond());
   require_sva_property(declaration.cond());
 
+  declaration.type() = verilog_sva_named_property_typet{};
+
   auto type = verilog_sva_property_typet{};
   symbolt symbol{full_identifier, type, mode};
 
@@ -1840,6 +1842,8 @@ void verilog_typecheckt::convert_sequence_declaration(
   convert_sva(sequence);
   require_sva_sequence(sequence);
 
+  declaration.type() = verilog_sva_named_sequence_typet{};
+
   symbolt symbol{full_identifier, sequence.type(), mode};
 
   symbol.module = module_identifier;

src/verilog/verilog_types.h

@@ -867,4 +867,28 @@ class verilog_sva_sequence_typet : public typet
   }
 };
 
+/// SVA named properties
+class verilog_sva_named_property_typet
+  : public typet
+{
+public:
+  explicit verilog_sva_named_property_typet()
+    : typet{
+        ID_verilog_sva_named_property}
+  {
+  }
+};
+
+/// SVA named sequences
+class verilog_sva_named_sequence_typet
+  : public typet
+{
+public:
+  explicit verilog_sva_named_sequence_typet()
+    : typet{
+        ID_verilog_sva_named_sequence}
+  {
+  }
+};
+
 #endif