From 3ca84d1283b6481cceea41db55fe5ad345be36ca Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 19 Oct 2025 16:31:37 -0700
Subject: [PATCH] KNOWNBUG test for module port constraints

This reproduces the second instance of #635.
---
 regression/verilog/modules/ports9.desc |  9 +++++++++
 regression/verilog/modules/ports9.sv   | 15 +++++++++++++++
 2 files changed, 24 insertions(+)
 create mode 100644 regression/verilog/modules/ports9.desc
 create mode 100644 regression/verilog/modules/ports9.sv

diff --git a/regression/verilog/modules/ports9.desc b/regression/verilog/modules/ports9.desc
new file mode 100644
index 000000000..201224631
--- /dev/null
+++ b/regression/verilog/modules/ports9.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+ports9.sv
+--bound 1
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This gives the wrong answer.
diff --git a/regression/verilog/modules/ports9.sv b/regression/verilog/modules/ports9.sv
new file mode 100644
index 000000000..50fbad159
--- /dev/null
+++ b/regression/verilog/modules/ports9.sv
@@ -0,0 +1,15 @@
+module sub(input in, output logic data);
+
+  assign data = in;
+
+endmodule
+
+module main;
+  logic subout;
+
+  sub sub_inst(.data(subout));
+
+  // The value of the output needs to be able to change
+  cover property (##1 subout != $past(subout));
+
+endmodule