From fdbbad1d24ca9bddadd1268c58d619442ba32d44 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 12 Jul 2025 15:11:08 -0700
Subject: [PATCH] Verilog: test for hierarchical identifier inside an assertion

---
 .../hierarchical_identifiers3.desc            |  7 +++++
 .../hierarchical_identifiers3.v               | 28 +++++++++++++++++++
 2 files changed, 35 insertions(+)
 create mode 100644 regression/verilog/hierarchical_identifiers/hierarchical_identifiers3.desc
 create mode 100644 regression/verilog/hierarchical_identifiers/hierarchical_identifiers3.v

diff --git a/regression/verilog/hierarchical_identifiers/hierarchical_identifiers3.desc b/regression/verilog/hierarchical_identifiers/hierarchical_identifiers3.desc
new file mode 100644
index 000000000..4809cd20d
--- /dev/null
+++ b/regression/verilog/hierarchical_identifiers/hierarchical_identifiers3.desc
@@ -0,0 +1,7 @@
+CORE
+hierarchical_identifiers3.v
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/verilog/hierarchical_identifiers/hierarchical_identifiers3.v b/regression/verilog/hierarchical_identifiers/hierarchical_identifiers3.v
new file mode 100644
index 000000000..22162de61
--- /dev/null
+++ b/regression/verilog/hierarchical_identifiers/hierarchical_identifiers3.v
@@ -0,0 +1,28 @@
+module Msubsub;
+
+  wire [31:0] magic_number = -1;
+
+endmodule
+
+module Msub;
+  reg [31:0] out;
+  wire x;
+
+  Msubsub subsub();
+
+  always @x out = subsub.magic_number;
+
+endmodule
+
+module main;
+  wire [31:0] bin;
+
+  assign bin=sub.out;
+
+  Msub sub();
+
+  always assert property1: bin=='hffffffff;
+
+  always assert property2: sub.subsub.magic_number =='hffffffff;
+
+endmodule