From ab5f25db9a0c498342caac1d19afce83bbd7e1cd Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 29 May 2026 18:40:24 +1200 Subject: [PATCH] Add test for non-contiguous memory init Also negative memory addresses. --- tests/check_mem/init_correct.ys | 44 +++++++++++++++++++++++++++++++++ tests/check_mem/negative_idx.sv | 13 ++++++++++ 2 files changed, 57 insertions(+) create mode 100644 tests/check_mem/init_correct.ys create mode 100644 tests/check_mem/negative_idx.sv 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