KNOWNBUG test for assignments to packed array elements

[kroening]

Summary

Adds a KNOWNBUG regression test for a soundness bug in the RTL construction introduced with #2119.

verilog_rtl_buildert::decompose_lhs places the elements of packed arrays as it does for unpacked arrays: the element with the left index of the declared range in the least significant position. In a packed array the element with the left index is the most significant (1800-2017 7.4.1), which is what verilog_lowering assumes for reads. Assignments to the elements of a packed array are hence written in reverse order, irrespective of the direction of the range.

logic [1:0][3:0] a1;
always @(posedge clk) begin a1[1] = 4'hA; a1[0] = 4'h5; end
p0: assert property (@(posedge clk) ##1 a1 == 8'hA5);  // REFUTED: a1 == 8'h5A

--show-rtl shows a1[3:0] register, next-state value: 4'b1010 for the assignment to a1[1].

Testing

• regression/verilog/arrays/packed_element_assignment1.desc is reported as SKIPPED by test.pl.
• Run as CORE, the test passes with the legacy synthesis flow and fails with the RTL flow at e224197c.

Root cause

decompose_lhs in src/verilog/verilog_rtl.cpp, ID_verilog_bit_select branch on array types: the layout differs for packed arrays.