diff --git a/tests/check_mem/init_correct.ys b/tests/check_mem/init_correct.ys new file mode 100644 index 000000000..5e922c7df --- /dev/null +++ b/tests/check_mem/init_correct.ys @@ -0,0 +1,44 @@ +read -sv << EOT +module top; + (* nomem2reg *) + logic a1 [2:3][3:1] = '{'{0, 1, 1}, '{1, 0, 1}}; + + always_comb begin + assert(a1[2][3] == 0); + assert(a1[2][2] == 1); + assert(a1[2][1] == 1); + assert(a1[3][3] == 1); + assert(a1[3][2] == 0); + assert(a1[3][1] == 1); + end + + (* nomem2reg *) + logic [1:0] a2 [6:5][2:4] = '{'{0, 1, 2}, '{1, 0, 3}}; + + always_comb begin + assert(a2[6][2] == 0); + assert(a2[6][3] == 1); + assert(a2[6][4] == 2); + assert(a2[5][2] == 1); + assert(a2[5][3] == 0); + assert(a2[5][4] == 3); + end + + (* nomem2reg *) + logic [1:0] a3 [-2:-1][-1:1] = '{'{0, 1, 2}, '{1, 0, 3}}; + + always_comb begin + assert(a3[-2][-1] == 0); + assert(a3[-2][0] == 1); + assert(a3[-2][1] == 2); + assert(a3[-1][-1] == 1); + assert(a3[-1][0] == 0); + assert(a3[-1][1] == 3); + end +endmodule +EOT +hierarchy +proc +memory +async2sync +sat -enable_undef -verify -prove-asserts diff --git a/tests/check_mem/negative_idx.sv b/tests/check_mem/negative_idx.sv new file mode 100644 index 000000000..dcfad94a3 --- /dev/null +++ b/tests/check_mem/negative_idx.sv @@ -0,0 +1,13 @@ +module top; + (* nomem2reg *) + logic [1:0] a3 [-2:-1][-1:1] = '{'{0, 1, 2}, '{1, 0, 3}}; + + always_comb begin + assert(a3[-2][-1] == 0); + assert(a3[-2][0] == 1); + assert(a3[-2][1] == 2); + assert(a3[-1][-1] == 1); + assert(a3[-1][0] == 0); + assert(a3[-1][1] == 3); + end +endmodule \ No newline at end of file