Merge pull request #1441 from diffblue/verilog_sva_named_sequence_property_typet

SVA: type for named sequences and properties

Author: tautschnig

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.property());
   require_sva_property(declaration.property());
 
+  declaration.type() = verilog_sva_named_property_typet{};
+
   // The symbol uses the full declaration as value
   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{};
+
   // The symbol uses the full declaration as value
   symbolt symbol{full_identifier, sequence.type(), mode};
 

src/verilog/verilog_types.h

@@ -867,4 +867,24 @@ 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