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_types.h

@@ -867,4 +867,88 @@ class verilog_sva_sequence_typet : public typet
   }
 };
 
+// base class for SVA named sequences and properties
+class verilog_sva_named_sequence_property_typet : public typet
+{
+public:
+  class portt : public irept
+  {
+  public:
+    portt(irep_idt _identifier, typet _type) : irept(ID_symbol)
+    {
+      identifier(_identifier);
+      type() = std::move(_type);
+    }
+
+    typet &type()
+    {
+      return static_cast<typet &>(add(ID_type));
+    }
+
+    const typet &type() const
+    {
+      return static_cast<const typet &>(find(ID_type));
+    }
+
+    irep_idt identifier() const
+    {
+      return get(ID_identifier);
+    }
+
+    void identifier(irep_idt _identifier)
+    {
+      set(ID_identifier, _identifier);
+    }
+
+    const source_locationt &source_location() const
+    {
+      return (const source_locationt &)find(ID_C_source_location);
+    }
+  };
+
+  using portst = std::vector<portt>;
+
+  verilog_sva_named_sequence_property_typet(irep_idt _id, portst _ports)
+    : typet(_id)
+  {
+    ports() = std::move(_ports);
+  }
+
+  portst &ports()
+  {
+    return (portst &)(add(ID_ports).get_sub());
+  }
+
+  const portst &ports() const
+  {
+    return (const portst &)(find(ID_ports).get_sub());
+  }
+};
+
+/// SVA named properties
+class verilog_sva_named_property_typet
+  : public verilog_sva_named_sequence_property_typet
+{
+public:
+  explicit verilog_sva_named_property_typet(portst _ports)
+    : verilog_sva_named_sequence_property_typet{
+        ID_verilog_sva_named_property,
+        std::move(_ports)}
+  {
+  }
+};
+
+/// SVA named sequences
+class verilog_sva_named_sequence_typet
+  : public verilog_sva_named_sequence_property_typet
+{
+public:
+  explicit verilog_sva_named_sequence_typet(portst _ports)
+    : verilog_sva_named_sequence_property_typet{
+        ID_verilog_sva_named_sequence,
+        std::move(_ports)}
+  {
+  }
+};
+
 #endif