From ab97931fc5772d90431e2ecfd116227a1451c7f6 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 26 Nov 2025 11:42:30 -0800
Subject: [PATCH] SVA: type for named sequences and properties

This introduces a type for named sequences and properties, similar to the
type for functions and tasks.
---
 src/hw_cbmc_irep_ids.h            |  2 ++
 src/verilog/verilog_typecheck.cpp |  4 ++++
 src/verilog/verilog_types.h       | 20 ++++++++++++++++++++
 3 files changed, 26 insertions(+)

diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index a48dbb9ea..012deea56 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/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)
diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp
index c4721b49f..870f6f046 100644
--- a/src/verilog/verilog_typecheck.cpp
+++ b/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};
 
diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h
index 08940b284..2be07878a 100644
--- a/src/verilog/verilog_types.h
+++ b/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