From 846a4e067d2835e4827f5e7038797b29302fdaeb Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 28 Aug 2025 08:47:39 -0700
Subject: [PATCH] Verilog: reject use of SVA sequences and properties as
 Boolean expression

SVA named sequences and named properties cannot be used as Booleans.  This
adds a check.
---
 .../verilog/property/named_property5.desc     |  4 ++--
 .../verilog/property/named_property6.desc     |  3 +--
 .../verilog/property/named_property7.desc     |  8 +++++++
 .../verilog/property/named_property7.sv       | 10 ++++++++
 src/verilog/verilog_typecheck_expr.cpp        | 24 ++++++++++++++++++-
 5 files changed, 44 insertions(+), 5 deletions(-)
 create mode 100644 regression/verilog/property/named_property7.desc
 create mode 100644 regression/verilog/property/named_property7.sv

diff --git a/regression/verilog/property/named_property5.desc b/regression/verilog/property/named_property5.desc
index 0a5fe2ee3..2c04566d2 100644
--- a/regression/verilog/property/named_property5.desc
+++ b/regression/verilog/property/named_property5.desc
@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 named_property5.sv
 
+^file .* line 8: cannot use SVA property as an expression$
 ^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This should be rejected.
diff --git a/regression/verilog/property/named_property6.desc b/regression/verilog/property/named_property6.desc
index 4c1e77aa7..3a85b05ef 100644
--- a/regression/verilog/property/named_property6.desc
+++ b/regression/verilog/property/named_property6.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 named_property6.sv
 
 ^EXIT=2$
@@ -6,4 +6,3 @@ named_property6.sv
 --
 ^warning: ignoring
 --
-This should be rejected.
diff --git a/regression/verilog/property/named_property7.desc b/regression/verilog/property/named_property7.desc
new file mode 100644
index 000000000..2b17f8288
--- /dev/null
+++ b/regression/verilog/property/named_property7.desc
@@ -0,0 +1,8 @@
+CORE
+named_property7.sv
+
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/property/named_property7.sv b/regression/verilog/property/named_property7.sv
new file mode 100644
index 000000000..0529093d3
--- /dev/null
+++ b/regression/verilog/property/named_property7.sv
@@ -0,0 +1,10 @@
+module main;
+
+  property P;
+    1
+  endproperty
+
+  // This should be rejected
+  wire x = P + P;
+
+endmodule
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index a57aaf355..2af22e8d4 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -121,6 +121,17 @@ void verilog_typecheck_exprt::propagate_type(
   if(expr.type()==type)
     return;
 
+  if(expr.type().id() == ID_verilog_sva_sequence)
+  {
+    throw errort{}.with_location(expr.source_location())
+      << "cannot use SVA sequence as an expression";
+  }
+  else if(expr.type().id() == ID_verilog_sva_property)
+  {
+    throw errort{}.with_location(expr.source_location())
+      << "cannot use SVA property as an expression";
+  }
+
   vtypet vt_from=vtypet(expr.type());
   vtypet vt_to  =vtypet(type);
 
@@ -2174,8 +2185,19 @@ Function: verilog_typecheck_exprt::make_boolean
 
 void verilog_typecheck_exprt::make_boolean(exprt &expr)
 {
-  if(expr.type().id()!=ID_bool)
+  if(expr.type().id() == ID_verilog_sva_sequence)
+  {
+    throw errort{}.with_location(expr.source_location())
+      << "cannot use SVA sequence as an expression";
+  }
+  else if(expr.type().id() == ID_verilog_sva_property)
+  {
+    throw errort{}.with_location(expr.source_location())
+      << "cannot use SVA property as an expression";
+  }
+  else if(expr.type().id() != ID_bool)
   {
+    // everything else can be converted to Boolean
     mp_integer value;
     if(!to_integer_non_constant(expr, value))
       expr = make_boolean_expr(value != 0);