diff --git a/regression/verilog/structs/structs4.desc b/regression/verilog/structs/structs4.desc new file mode 100644 index 000000000..2fecd6979 --- /dev/null +++ b/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$ +-- diff --git a/regression/verilog/structs/structs4.sv b/regression/verilog/structs/structs4.sv new file mode 100644 index 000000000..0cb9c4441 --- /dev/null +++ b/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