SystemVerilog: test for cast from packed struct to vector

Author: kroening

regression/verilog/structs/structs4.desc

@@ -0,0 +1,7 @@
+CORE
+structs4.sv
+--bound 0
+^\[main\.p0\] always main\.w == 'h173: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/verilog/structs/structs4.sv

@@ -0,0 +1,21 @@
+module main;
+
+  // The first field is the most-significant bit.
+  struct packed {
+    bit field1, field2;
+    bit [6:0] field3;
+  } s;
+
+  initial begin
+    s.field1 = 1;
+    s.field2 = 0;
+    s.field3 = 'b1110011;
+  end
+
+  // structs can be converted without cast to bit-vectors
+  wire [8:0] w = s;
+
+  // Expected to pass.
+  p0: assert property (w == 'b1_0_1110011);
+
+endmodule