Merge pull request #3682 from daglem/struct-member-out-of-bounds

Out of bounds checking for struct/union members

tests/gen-tests-makefile.sh

@@ -75,7 +75,7 @@ generate_tests() {
 	if [[ $do_sv = true ]]; then
 		for x in *.sv; do
 			if [ ! -f "${x%.sv}.ys"  ]; then
-				generate_ys_test "$x" "-p \"prep -top top; sat -verify -prove-asserts\" $yosys_args"
+				generate_ys_test "$x" "-p \"prep -top top; sat -enable_undef -verify -prove-asserts\" $yosys_args"
 			fi;
 		done
 	fi;

tests/svtypes/struct_array.sv

@@ -12,12 +12,16 @@ module top;
 
 		s.a[2:1] = 16'h1234;
 		s.a[5] = 8'h42;
+		s.a[-1] = '0;
 
 		s.b = '1;
 		s.b[1:0] = '0;
 	end
 
 	always_comb assert(s==64'h4200_0012_3400_FFFC);
+	always_comb assert(s.a[0][3:-4]===8'h0x);
+	always_comb assert(s.b[23:16]===8'hxx);
+	always_comb assert(s.b[19:12]===8'hxf);
 
 	struct packed {
 		bit [7:0] [7:0] a;	// 8 element packed array of bytes

tests/svtypes/struct_dynamic_range.sv

@@ -0,0 +1,67 @@
+module range_shift_mask(
+    input logic [2:0] addr_i,
+    input logic [7:0] data_i,
+    input logic [2:0] addr_o,
+    output logic [7:0] data_o
+);
+    // (* nowrshmsk = 0 *)
+    struct packed {
+        logic [7:0] msb;
+        logic [0:3][7:0] data;
+        logic [7:0] lsb;
+    } s;
+
+    always_comb begin
+        s = '1;
+        s.data[addr_i] = data_i;
+        data_o = s.data[addr_o];
+    end
+endmodule
+
+module range_case(
+    input logic [2:0] addr_i,
+    input logic [7:0] data_i,
+    input logic [2:0] addr_o,
+    output logic [7:0] data_o
+);
+    // (* nowrshmsk = 1 *)
+    struct packed {
+        logic [7:0] msb;
+        logic [0:3][7:0] data;
+        logic [7:0] lsb;
+    } s;
+
+    always_comb begin
+        s = '1;
+        s.data[addr_i] = data_i;
+        data_o = s.data[addr_o];
+    end
+endmodule
+
+module top;
+    logic [7:0] data_shift_mask1;
+    range_shift_mask range_shift_mask1(3'd1, 8'h7e, 3'd1, data_shift_mask1);
+    logic [7:0] data_shift_mask2;
+    range_shift_mask range_shift_mask2(3'd1, 8'h7e, 3'd2, data_shift_mask2);
+    logic [7:0] data_shift_mask3;
+    range_shift_mask range_shift_mask3(3'd1, 8'h7e, 3'd4, data_shift_mask3);
+
+    always_comb begin
+        assert(data_shift_mask1 === 8'h7e);
+        assert(data_shift_mask2 === 8'hff);
+        assert(data_shift_mask3 === 8'hxx);
+    end
+
+    logic [7:0] data_case1;
+    range_case range_case1(3'd1, 8'h7e, 3'd1, data_case1);
+    logic [7:0] data_case2;
+    range_case range_case2(3'd1, 8'h7e, 3'd2, data_case2);
+    logic [7:0] data_case3;
+    range_case range_case3(3'd1, 8'h7e, 3'd4, data_case3);
+
+    always_comb begin
+        assert(data_case1 === 8'h7e);
+        assert(data_case2 === 8'hff);
+        assert(data_case3 === 8'hxx);
+    end
+endmodule

tests/svtypes/struct_dynamic_range.ys

@@ -0,0 +1,4 @@
+read_verilog -sv struct_dynamic_range.sv
+prep -top top
+flatten
+sat -enable_undef -verify -prove-asserts