From b395a5e5facc0325638db2ce60ab3e757ce61dda Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 16 Jan 2025 07:32:53 -0800
Subject: [PATCH 1/2] Verilog: KNOWNBUG test for property ... endproperty

The type checker uses the wrong fragement of the expression syntax for
property ...  endproperty.

Replicates #931.
---
 .../verilog/{SVA => property}/named_property1.desc   |  0
 .../verilog/{SVA => property}/named_property1.sv     |  0
 regression/verilog/property/named_property2.desc     | 11 +++++++++++
 regression/verilog/property/named_property2.sv       | 12 ++++++++++++
 .../{SVA => property}/recursive_property1.desc       |  0
 .../verilog/{SVA => property}/recursive_property1.sv |  0
 6 files changed, 23 insertions(+)
 rename regression/verilog/{SVA => property}/named_property1.desc (100%)
 rename regression/verilog/{SVA => property}/named_property1.sv (100%)
 create mode 100644 regression/verilog/property/named_property2.desc
 create mode 100644 regression/verilog/property/named_property2.sv
 rename regression/verilog/{SVA => property}/recursive_property1.desc (100%)
 rename regression/verilog/{SVA => property}/recursive_property1.sv (100%)

diff --git a/regression/verilog/SVA/named_property1.desc b/regression/verilog/property/named_property1.desc
similarity index 100%
rename from regression/verilog/SVA/named_property1.desc
rename to regression/verilog/property/named_property1.desc
diff --git a/regression/verilog/SVA/named_property1.sv b/regression/verilog/property/named_property1.sv
similarity index 100%
rename from regression/verilog/SVA/named_property1.sv
rename to regression/verilog/property/named_property1.sv
diff --git a/regression/verilog/property/named_property2.desc b/regression/verilog/property/named_property2.desc
new file mode 100644
index 000000000..a24ff735d
--- /dev/null
+++ b/regression/verilog/property/named_property2.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+named_property2.sv
+--bound 20
+^\[main\.assert\.1\] always main\.x_is_eventually_ten: PROVED up to bound 20$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The type checker only allows expressions, not properties in property ...
+endproperty.
diff --git a/regression/verilog/property/named_property2.sv b/regression/verilog/property/named_property2.sv
new file mode 100644
index 000000000..8e602154b
--- /dev/null
+++ b/regression/verilog/property/named_property2.sv
@@ -0,0 +1,12 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+  always_ff @(posedge clk) x++;
+
+  property x_is_eventually_ten;
+    s_eventually x == 10
+  endproperty : x_is_eventually_ten
+
+  assert property (x_is_eventually_ten);
+
+endmodule
diff --git a/regression/verilog/SVA/recursive_property1.desc b/regression/verilog/property/recursive_property1.desc
similarity index 100%
rename from regression/verilog/SVA/recursive_property1.desc
rename to regression/verilog/property/recursive_property1.desc
diff --git a/regression/verilog/SVA/recursive_property1.sv b/regression/verilog/property/recursive_property1.sv
similarity index 100%
rename from regression/verilog/SVA/recursive_property1.sv
rename to regression/verilog/property/recursive_property1.sv

From 729e0abf7268b41e43d61fa2e720c486158d3ac1 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 16 Jan 2025 10:13:51 -0800
Subject: [PATCH 2/2] SystemVerilog: allow SVA in property ... endproperty

This changes the type checker to allow SVA in property ... endproperty.
---
 regression/verilog/property/named_property2.desc | 4 +---
 src/verilog/verilog_typecheck.cpp                | 2 +-
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/regression/verilog/property/named_property2.desc b/regression/verilog/property/named_property2.desc
index a24ff735d..23e5c031a 100644
--- a/regression/verilog/property/named_property2.desc
+++ b/regression/verilog/property/named_property2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 named_property2.sv
 --bound 20
 ^\[main\.assert\.1\] always main\.x_is_eventually_ten: PROVED up to bound 20$
@@ -7,5 +7,3 @@ named_property2.sv
 --
 ^warning: ignoring
 --
-The type checker only allows expressions, not properties in property ...
-endproperty.
diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp
index 21495841a..b2134c086 100644
--- a/src/verilog/verilog_typecheck.cpp
+++ b/src/verilog/verilog_typecheck.cpp
@@ -1770,7 +1770,7 @@ void verilog_typecheckt::convert_property_declaration(
   auto base_name = declaration.base_name();
   auto full_identifier = hierarchical_identifier(base_name);
 
-  convert_expr(declaration.cond());
+  convert_sva(declaration.cond());
   make_boolean(declaration.cond());
 
   auto type = bool_typet{};