Verilog: test for hierarchical identifier inside an assertion

Author: kroening

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

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