From 07e3d648aa26fb9f24802b5bb0b5b2e7b5d1c85b Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 29 May 2026 18:40:23 +1200 Subject: [PATCH 01/10] Add check_mem command Comes with a set of tests which (currently) pass with `read_verilog` but fail with `verific` based on #5878. Add `--check-sv`, an alternative to `--prove-sv` with generator defined yosys commands. Helpful for when you want to run the same set of commands on a bunch of sv files. --- passes/cmds/check.cc | 78 +++++++++++++++++++++++++++++++++ tests/check_mem/bad_il.ys | 47 ++++++++++++++++++++ tests/check_mem/generate_mk.py | 8 ++++ tests/check_mem/init.sv | 15 +++++++ tests/check_mem/non_zero.sv | 21 +++++++++ tests/check_mem/power_of_two.sv | 24 ++++++++++ tests/gen_tests_makefile.py | 21 +++++++-- 7 files changed, 210 insertions(+), 4 deletions(-) create mode 100644 tests/check_mem/bad_il.ys create mode 100644 tests/check_mem/generate_mk.py create mode 100644 tests/check_mem/init.sv create mode 100644 tests/check_mem/non_zero.sv create mode 100644 tests/check_mem/power_of_two.sv diff --git a/passes/cmds/check.cc b/passes/cmds/check.cc index 6e0d65297..9a0070996 100644 --- a/passes/cmds/check.cc +++ b/passes/cmds/check.cc @@ -23,6 +23,7 @@ #include "kernel/newcelltypes.h" #include "kernel/utils.h" #include "kernel/log_help.h" +#include "kernel/mem.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -453,4 +454,81 @@ struct CheckPass : public Pass { } } CheckPass; +struct CheckMemPass : public Pass { + CheckMemPass() : Pass("check_mem", "check for obvious memory problems in the design") { } + bool formatted_help() override { + auto *help = PrettyHelp::get_current(); + help->set_group("passes/status"); + + auto content_root = help->get_root(); + + content_root->usage("check_mem [selection]"); + content_root->paragraph( + "This pass identifies the following problems in the current design: " + "addressing invalid memory." + ); + + content_root->option("-assert", "produce a runtime error if any problems are found in the current design"); + + return true; + } + void execute(std::vector args, RTLIL::Design *design) override + { + int counter = 0; + bool assert_mode = false; + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-assert") { + assert_mode = true; + continue; + } + break; + } + + extra_args(args, argidx, design); + + log_header(design, "Executing CHECK_MEM pass.\n"); + + for (auto *module : design->selected_unboxed_modules_warn()) { + for (auto mem : Mem::get_selected_memories(module)) { + int min_addr = mem.mem->start_offset; + int max_addr = mem.mem->size + min_addr - 1; + for (auto &init : mem.inits) { + int start = init.addr.as_int(); + if (start < min_addr) { + log_warning("Mem %s.%s starts at %d but initializes address %d.\n", log_id(module), log_id(mem.mem), min_addr, start); + counter++; + } + int end = start + (GetSize(init.data) / mem.width) - 1; + if (end > max_addr) { + log_warning("Mem %s.%s ends at %d but initializes address %d.\n", log_id(module), log_id(mem.mem), max_addr, end); + counter++; + } + } + + auto check_addr = [min_addr, max_addr, &counter, module, &mem](SigSpec &addr_sig, const char* access) { + if (addr_sig.is_fully_const()) { + auto addr = addr_sig.as_int(); + if (addr < min_addr || addr > max_addr) { + log_warning("Mem %s.%s contains entries for addresses %d..%d but %s address %d.\n", log_id(module), log_id(mem.mem), min_addr, max_addr, access, addr); + counter++; + } + } else { + // TODO test variable addresses? may need sat solver + } + }; + + // TODO test ABITS and WIDTH? + for (auto &rd_port : mem.rd_ports) + check_addr(rd_port.addr, "reads"); + for (auto &wr_port : mem.wr_ports) + check_addr(wr_port.addr, "writes"); + } + } + + if (assert_mode && counter > 0) + log_error("Found %d problems in 'check_mem -assert'.\n", counter); + } +} CheckMemPass; + PRIVATE_NAMESPACE_END diff --git a/tests/check_mem/bad_il.ys b/tests/check_mem/bad_il.ys new file mode 100644 index 000000000..06968c32c --- /dev/null +++ b/tests/check_mem/bad_il.ys @@ -0,0 +1,47 @@ +read_rtlil << EOF +module \top + wire input 1 \clk + wire output 1 \o + memory size 2 offset 1 \my_array + cell $meminit \bad_init + parameter \WORDS 1 + parameter \MEMID "\\my_array" + parameter \ABITS 32 + parameter \WIDTH 1 + parameter \PRIORITY 1 + connect \ADDR 0 + connect \DATA 1'0 + end + cell $memwr \bad_wr + parameter \MEMID "\\my_array" + parameter \CLK_ENABLE 1 + parameter \CLK_POLARITY 1 + parameter \PRIORITY 1 + parameter \ABITS 2 + parameter \WIDTH 1 + connect \EN 1'1 + connect \CLK \clk + connect \ADDR 2'00 + connect \DATA 1'0 + end + cell $memrd \bad_rd + parameter \MEMID "\\my_array" + parameter \CLK_ENABLE 0 + parameter \CLK_POLARITY 1 + parameter \TRANSPARENT 0 + parameter \ABITS 2 + parameter \WIDTH 1 + connect \CLK 1'x + connect \EN 1'x + connect \ADDR 2'11 + connect \DATA \o + end +end +EOF + +logger -expect warning "initializes address 0" 1 +logger -expect warning "writes address 0" 1 +logger -expect warning "reads address 3" 1 +check_mem +logger -check-expected +design -reset diff --git a/tests/check_mem/generate_mk.py b/tests/check_mem/generate_mk.py new file mode 100644 index 000000000..ee8dbeb44 --- /dev/null +++ b/tests/check_mem/generate_mk.py @@ -0,0 +1,8 @@ +#!/usr/bin/env python3 + +import sys +sys.path.append("..") + +import gen_tests_makefile + +gen_tests_makefile.generate(["--check-sv", "--yosys-scripts"], yosys_cmds="hierarchy; proc; check_mem -assert") diff --git a/tests/check_mem/init.sv b/tests/check_mem/init.sv new file mode 100644 index 000000000..f55a0d1c5 --- /dev/null +++ b/tests/check_mem/init.sv @@ -0,0 +1,15 @@ +module top ( + input logic clk, + input logic idx, + output logic [2:0] out_data +); + (* nomem2reg *) + logic my_array [3:2][2:0] = '{'{0, 1, 1}, '{1, 0, 1}}; + + always_comb begin + for (int i=0; i < 3; i++) begin + out_data[i] = my_array[{1'b1, idx}][i]; + end + end + +endmodule diff --git a/tests/check_mem/non_zero.sv b/tests/check_mem/non_zero.sv new file mode 100644 index 000000000..5b3f45c0a --- /dev/null +++ b/tests/check_mem/non_zero.sv @@ -0,0 +1,21 @@ +module top ( + input logic clk, + input logic [3:1][2:0] in_data, + output logic [3:1][2:0] out_data +); + (* nomem2reg *) + logic [2:0] my_array [3:1]; + + always_ff @(posedge clk) begin + for (int i = 1; i <= 3; i++) begin + my_array[i] <= in_data[i]; + end + end + + always_comb begin + for (int i = 1; i <= 3; i++) begin + out_data[i] = my_array[i]; + end + end + +endmodule diff --git a/tests/check_mem/power_of_two.sv b/tests/check_mem/power_of_two.sv new file mode 100644 index 000000000..786168ea0 --- /dev/null +++ b/tests/check_mem/power_of_two.sv @@ -0,0 +1,24 @@ +module top ( + input logic clk, + input logic [1:0][5:0] in_data, + output logic [1:0][5:0] out_data +); + (* nomem2reg *) + logic my_array [1:0][5:0]; + + always_ff @(posedge clk) begin + for (int i = 0; i < 2; i++) begin + for (int j = 0; j <= 5; j++) begin + my_array[i][j] <= in_data[i][j]; + end + end + end + + always_comb begin + for (int i = 0; i < 2; i++) begin + for (int j = 0; j <= 5; j++) begin + out_data[i][j] = my_array[i][j]; + end + end + end +endmodule diff --git a/tests/gen_tests_makefile.py b/tests/gen_tests_makefile.py index 034883a2c..efaa9a652 100644 --- a/tests/gen_tests_makefile.py +++ b/tests/gen_tests_makefile.py @@ -37,6 +37,11 @@ def generate_tcl_test(tcl_file, yosys_args="", commands=""): cmd += f"; \\\n{commands}" generate_target(tcl_file, cmd) +def generate_sv_check(sv_file, yosys_args="", yosys_cmds=""): + yosys_cmd = f'read -sv {sv_file}; {yosys_cmds}' + cmd = f'$(YOSYS) -ql {sv_file}.err -p "{yosys_cmd}" {yosys_args} && mv {sv_file}.err {sv_file}.log' + generate_target(sv_file, cmd) + def generate_sv_test(sv_file, yosys_args="", commands=""): base = os.path.splitext(sv_file)[0] if not os.path.exists(base + ".ys"): @@ -62,19 +67,23 @@ def unpack_cmd(cmd): def generate_cmd_test(test_name, cmd, yosys_args="", deps = None): generate_target(test_name, unpack_cmd(cmd), deps) -def generate_tests(argv, cmds): +def generate_tests(argv, cmds, yosys_cmds=""): parser = argparse.ArgumentParser(add_help=False) parser.add_argument("-y", "--yosys-scripts", action="store_true") parser.add_argument("-t", "--tcl-scripts", action="store_true") + parser.add_argument("-c", "--check-sv", action="store_true") parser.add_argument("-s", "--prove-sv", action="store_true") parser.add_argument("-b", "--bash", action="store_true") parser.add_argument("-a", "--yosys-args", default="") args = parser.parse_args(argv) - if not (args.yosys_scripts or args.tcl_scripts or args.prove_sv or args.bash): + if not (args.yosys_scripts or args.tcl_scripts or args.check_sv or args.prove_sv or args.bash): raise RuntimeError("No file types selected") + if args.check_sv and args.prove_sv: + raise RuntimeError("Unable to use --check-sv and --prove-sv together") + if args.yosys_scripts: for f in sorted(glob.glob("*.ys")): generate_ys_test(f, args.yosys_args, cmds) @@ -83,6 +92,10 @@ def generate_tests(argv, cmds): for f in sorted(glob.glob("*.tcl")): generate_tcl_test(f, args.yosys_args, cmds) + if args.check_sv: + for f in sorted(glob.glob("*.sv")): + generate_sv_check(f, args.yosys_args, yosys_cmds) + if args.prove_sv: for f in sorted(glob.glob("*.sv")): generate_sv_test(f, args.yosys_args, cmds) @@ -109,11 +122,11 @@ def redirect_stdout(new_target): finally: sys.stdout = old_target -def generate(argv, extra=None, cmds=""): +def generate(argv, extra=None, cmds="", yosys_cmds=""): with open("Makefile", "w") as f: with redirect_stdout(f): print_header(extra) - generate_tests(argv, cmds) + generate_tests(argv, cmds, yosys_cmds) def generate_custom(callback, extra=None): with open("Makefile", "w") as f: From 7cf0c554665f40a8ba717e98ab393b009fe819f1 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 29 May 2026 18:40:23 +1200 Subject: [PATCH 02/10] verific: Fix non-contiguous memory flattening May not be the best approach, insofar as it uses empty memory elements for padding out the alignment, but it does avoid costly address arithmetic. Still needs to adjust ascii init val addresses, but should work fine for read/write accesses. --- frontends/verific/verific.cc | 81 ++++++++++++++++++++++++++++++------ 1 file changed, 69 insertions(+), 12 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 6b876c0f1..76a5c13bc 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1630,22 +1630,78 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma import_attributes(memory->attributes, net, nl); int number_of_bits = net->Size(); - int bits_in_word = number_of_bits; + int min_bits_in_word = number_of_bits; + int max_bits_in_addr = 0; + + // get the size of each memory access FOREACH_PORTREF_OF_NET(net, si, pr) { - if (pr->GetInst()->Type() == OPER_READ_PORT) { - bits_in_word = min(bits_in_word, pr->GetInst()->OutputSize()); - continue; + auto *inst = pr->GetInst(); + int bits_in_word; + if (inst->Type() == OPER_READ_PORT) + bits_in_word = inst->OutputSize(); + else if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT) + bits_in_word = inst->Input2Size(); + else + log_error("%sVerific RamNet %s is connected to unsupported instance type %s (%s).\n", announce_src_location(inst), + net->Name(), inst->View()->Owner()->Name(), inst->Name()); + + if (bits_in_word < min_bits_in_word) { + min_bits_in_word = bits_in_word; + max_bits_in_addr = inst->Input1Size(); } - if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) { - bits_in_word = min(bits_in_word, pr->GetInst()->Input2Size()); - continue; - } - log_error("%sVerific RamNet %s is connected to unsupported instance type %s (%s).\n", announce_src_location(pr->GetInst()), - net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name()); } - memory->width = bits_in_word; - memory->size = number_of_bits / bits_in_word; + int number_of_words = number_of_bits / min_bits_in_word; + // TODO Verific has u64 sizes + int size = 1 << max_bits_in_addr; + int min_idx = 0; + int max_idx = size - 1; + + // attempt to infer min/max address for memory definition + RTLIL::SigSpec min_addr, max_addr; + auto typeRange = net->GetOrigTypeRange(); + while (typeRange) { + RTLIL::SigSpec min_addr_chunk(RTLIL::Const(typeRange->RightRangeBound(), typeRange->NumBits())); + min_addr_chunk.reverse(); + min_addr.append(min_addr_chunk); + + RTLIL::SigSpec max_addr_chunk(RTLIL::Const(typeRange->LeftRangeBound(), typeRange->NumBits())); + max_addr_chunk.reverse(); + max_addr.append(max_addr_chunk); + + typeRange = typeRange->GetNext(); + } + min_addr = min_addr.extract(0, max_bits_in_addr); + max_addr = max_addr.extract(0, max_bits_in_addr); + min_addr.reverse(); + max_addr.reverse(); + + if (min_addr.convertible_to_int()) { + min_idx = min_addr.as_int(); + if (max_addr.convertible_to_int()) { + max_idx = max_addr.as_int(); + } else { + log_debug("Unable to set maximum index\n"); + } + size = max_idx - min_idx + 1; + } else { + log_debug("Unable to set minimum index\n"); + } + + // sanity check we haven't shrunk the memory + log_assert(size >= number_of_words); + + memory->width = min_bits_in_word; + memory->size = size; + memory->start_offset = min_idx; + + // warn on oversize memories + // TODO consider using a minimum ratio? + if (size > number_of_words) { + float ratio = size / (float)number_of_words; + log_warning("RAM for identifier '%s' may be up to %.0f%% oversize due to addressing\n", net->Name(), (ratio-1)*100); + log_debug("Expected memory of size %d words, but got %d for address range %d to %d (inclusive)\n", number_of_words, size, min_idx, max_idx); + } const char *ascii_initdata = net->GetWideInitialValue(); if (ascii_initdata) { @@ -1672,6 +1728,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma if (initval_valid) { RTLIL::Cell *cell = module->addCell(new_verific_id(net), ID($meminit)); cell->parameters[ID::WORDS] = 1; + // TODO non contiguous memory addressing if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound()) cell->setPort(ID::ADDR, word_idx); else From 099c664dc9cb08955dba5ae508bc7801b24e3e54 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 29 May 2026 18:40:23 +1200 Subject: [PATCH 03/10] verific: Fix upto ranges --- frontends/verific/verific.cc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 76a5c13bc..74ebcc2be 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1661,11 +1661,13 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma RTLIL::SigSpec min_addr, max_addr; auto typeRange = net->GetOrigTypeRange(); while (typeRange) { - RTLIL::SigSpec min_addr_chunk(RTLIL::Const(typeRange->RightRangeBound(), typeRange->NumBits())); + auto left = typeRange->LeftRangeBound(); + auto right = typeRange->RightRangeBound(); + RTLIL::SigSpec min_addr_chunk(RTLIL::Const(left > right ? right : left, typeRange->NumBits())); min_addr_chunk.reverse(); min_addr.append(min_addr_chunk); - RTLIL::SigSpec max_addr_chunk(RTLIL::Const(typeRange->LeftRangeBound(), typeRange->NumBits())); + RTLIL::SigSpec max_addr_chunk(RTLIL::Const(left > right ? left : right, typeRange->NumBits())); max_addr_chunk.reverse(); max_addr.append(max_addr_chunk); From f6327cc4447187f19658e01833eb2d6ec26f553c 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 04/10] check_mem: Add -non-const option Can identify potentially dangerous addressing, but also prone to false-positives. --- passes/cmds/check.cc | 20 ++++++++++-- tests/check_mem/variable.ys | 65 +++++++++++++++++++++++++++++++++++++ 2 files changed, 82 insertions(+), 3 deletions(-) create mode 100644 tests/check_mem/variable.ys diff --git a/passes/cmds/check.cc b/passes/cmds/check.cc index 9a0070996..426216800 100644 --- a/passes/cmds/check.cc +++ b/passes/cmds/check.cc @@ -468,6 +468,7 @@ struct CheckMemPass : public Pass { "addressing invalid memory." ); + content_root->option("-non-const", "also check non-const address signals (may produce false-positives)"); content_root->option("-assert", "produce a runtime error if any problems are found in the current design"); return true; @@ -476,12 +477,17 @@ struct CheckMemPass : public Pass { { int counter = 0; bool assert_mode = false; + bool nonconst_mode = false; size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { if (args[argidx] == "-assert") { assert_mode = true; continue; } + if (args[argidx] == "-non-const") { + nonconst_mode = true; + continue; + } break; } @@ -506,19 +512,27 @@ struct CheckMemPass : public Pass { } } - auto check_addr = [min_addr, max_addr, &counter, module, &mem](SigSpec &addr_sig, const char* access) { + auto check_addr = [min_addr, max_addr, &counter, module, &mem, &nonconst_mode](SigSpec &addr_sig, const char* access) { if (addr_sig.is_fully_const()) { auto addr = addr_sig.as_int(); if (addr < min_addr || addr > max_addr) { log_warning("Mem %s.%s contains entries for addresses %d..%d but %s address %d.\n", log_id(module), log_id(mem.mem), min_addr, max_addr, access, addr); counter++; } - } else { - // TODO test variable addresses? may need sat solver + } else if (nonconst_mode) { + // TODO check addr_sig.has_const() for constant MSb/LSb that may change effective min/max + // TODO consider sat solver for variable addresses + int addr_sig_min = 0; + int addr_sig_max = (1 << addr_sig.size()) - 1; + if (min_addr > addr_sig_min || max_addr < addr_sig_max) { + log_warning("Mem %s.%s contains entries for addresses %d..%d but has a potentially dangerous non-const input %s\n", log_id(module), log_id(mem.mem), min_addr, max_addr, log_signal(addr_sig)); + counter++; + } } }; // TODO test ABITS and WIDTH? + // TODO can we limit ports via selection? for (auto &rd_port : mem.rd_ports) check_addr(rd_port.addr, "reads"); for (auto &wr_port : mem.wr_ports) diff --git a/tests/check_mem/variable.ys b/tests/check_mem/variable.ys new file mode 100644 index 000000000..8da49758b --- /dev/null +++ b/tests/check_mem/variable.ys @@ -0,0 +1,65 @@ + + +read_rtlil << EOF +module \top + wire input 1 \clk + wire input 2 width 2 \addr + wire output 1 \o + memory size 3 offset 0 \my_array + # potentially dangerous - requires external control to avoid illegal access + cell $memrd \bad_rd + parameter \MEMID "\\my_array" + parameter \CLK_ENABLE 0 + parameter \CLK_POLARITY 1 + parameter \TRANSPARENT 0 + parameter \ABITS 2 + parameter \WIDTH 1 + connect \CLK 1'x + connect \EN 1'x + connect \ADDR \addr + connect \DATA \o + end + wire width 2 \n_addr + cell $not \not_addr + parameter \A_SIGNED 0 + parameter \A_WIDTH 2 + parameter \Y_WIDTH 2 + connect \A \addr + connect \Y \n_addr + end + # address is partially const, making the illegal access of 2'11 impossible + cell $memrd \partial_const_rd + parameter \MEMID "\\my_array" + parameter \CLK_ENABLE 0 + parameter \CLK_POLARITY 1 + parameter \TRANSPARENT 0 + parameter \ABITS 2 + parameter \WIDTH 1 + connect \CLK 1'x + connect \EN 1'x + connect \ADDR { 1'0 \addr [0] } + connect \DATA \o + end + # address is non-const but limited to 2'10 and 2'01 - both of which are valid + cell $memrd \limited_rd + parameter \MEMID "\\my_array" + parameter \CLK_ENABLE 0 + parameter \CLK_POLARITY 1 + parameter \TRANSPARENT 0 + parameter \ABITS 2 + parameter \WIDTH 1 + connect \CLK 1'x + connect \EN 1'x + connect \ADDR { \n_addr [0] \addr [0] } + connect \DATA \o + end +end +EOF + +logger -expect warning "potentially dangerous non-const input \\addr" 1 +# unhandled false-positives +# logger -werror "potentially dangerous non-const input \{ 1'0" +# logger -werror "potentially dangerous non-const input \{ \\n_addr" +check_mem -non-const +logger -check-expected +design -reset From aac7366862af73a4b51b452f44fb1339f828d607 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 05/10] tests: Add check_mem to vanilla-test --- tests/Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/Makefile b/tests/Makefile index 05e5410b7..6c2689c79 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -78,6 +78,7 @@ MK_TEST_DIRS += ./liberty MK_TEST_DIRS += ./memories MK_TEST_DIRS += ./aiger MK_TEST_DIRS += ./alumacc +MK_TEST_DIRS += ./check_mem all: vanilla-test 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 06/10] 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 From 21966ef496fc11ffc6a9e5076a095f5d30e7ce92 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 29 May 2026 18:40:25 +1200 Subject: [PATCH 07/10] verific: Fix non-contiguous memory init Recurse over nested type ranges to calculate true addresses. --- frontends/verific/verific.cc | 66 +++++++++++++++++++++--------------- frontends/verific/verific.h | 3 ++ 2 files changed, 42 insertions(+), 27 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 74ebcc2be..24c91c3c4 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1444,6 +1444,44 @@ static std::string sha1_if_contain_spaces(std::string str) return str; } +void VerificImporter::recurse_ascii_initdata(RTLIL::Module *module, RTLIL::Memory *memory, Net *net, const char *&ascii_initdata, TypeRange *typeRange, int base_idx) { + if (typeRange == nullptr) + typeRange = net->GetOrigTypeRange(); + + auto *nextRange = typeRange->GetNext(); + base_idx <<= typeRange->NumBits(); + auto left = typeRange->LeftRangeBound(); + auto right = typeRange->RightRangeBound(); + for (auto i = left; left < right ? i <= right : i >= right; left < right ? i++ : i--) { + auto next_idx = base_idx + i; + if (nextRange != nullptr) { + recurse_ascii_initdata(module, memory, net, ascii_initdata, nextRange, next_idx); + } else { + Const initval = Const(State::Sx, memory->width); + bool initval_valid = false; + for (int bit_idx = memory->width-1; bit_idx >= 0; bit_idx--) { + if (*ascii_initdata == 0) + break; + if (*ascii_initdata == '0' || *ascii_initdata == '1') { + initval.set(bit_idx, (*ascii_initdata == '0') ? State::S0 : State::S1); + initval_valid = true; + } + ascii_initdata++; + } + if (initval_valid) { + RTLIL::Cell *cell = module->addCell(new_verific_id(net), ID($meminit)); + cell->parameters[ID::WORDS] = 1; + cell->setPort(ID::ADDR, next_idx); + cell->setPort(ID::DATA, initval); + cell->parameters[ID::MEMID] = RTLIL::Const(memory->name.str()); + cell->parameters[ID::ABITS] = 32; + cell->parameters[ID::WIDTH] = memory->width; + cell->parameters[ID::PRIORITY] = RTLIL::Const(autoidx-1); + } + } + } +} + void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::map &nl_todo, bool norename) { std::string netlist_name = nl->GetAtt(" \\top") || is_blackbox(nl) ? nl->CellBaseName() : nl->Owner()->Name(); @@ -1715,33 +1753,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma log_assert(*ascii_initdata == 'b'); ascii_initdata++; } - for (int word_idx = 0; word_idx < memory->size; word_idx++) { - Const initval = Const(State::Sx, memory->width); - bool initval_valid = false; - for (int bit_idx = memory->width-1; bit_idx >= 0; bit_idx--) { - if (*ascii_initdata == 0) - break; - if (*ascii_initdata == '0' || *ascii_initdata == '1') { - initval.set(bit_idx, (*ascii_initdata == '0') ? State::S0 : State::S1); - initval_valid = true; - } - ascii_initdata++; - } - if (initval_valid) { - RTLIL::Cell *cell = module->addCell(new_verific_id(net), ID($meminit)); - cell->parameters[ID::WORDS] = 1; - // TODO non contiguous memory addressing - if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound()) - cell->setPort(ID::ADDR, word_idx); - else - cell->setPort(ID::ADDR, memory->size - word_idx - 1); - cell->setPort(ID::DATA, initval); - cell->parameters[ID::MEMID] = RTLIL::Const(memory->name.str()); - cell->parameters[ID::ABITS] = 32; - cell->parameters[ID::WIDTH] = memory->width; - cell->parameters[ID::PRIORITY] = RTLIL::Const(autoidx-1); - } - } + recurse_ascii_initdata(module, memory, net, ascii_initdata); } continue; } diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h index f33a380f7..478ab82cb 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -66,6 +66,9 @@ struct VerificClocking { struct VerificImporter { +private: + void recurse_ascii_initdata(RTLIL::Module *module, RTLIL::Memory *memory, Verific::Net *net, const char *&ascii_initdata, Verific::TypeRange *typeRange = nullptr, int base_idx = 0); +public: RTLIL::Module *module; Verific::Netlist *netlist; From 52e0030cc52a3af6a65de62c54b47f3476244f64 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 29 May 2026 18:40:25 +1200 Subject: [PATCH 08/10] tests/check_mem: Add problematic case Verific reports it as 16 2-bit addresses, meaning we have to iterate over the last dimension while skipping indices. --- tests/check_mem/negative_idx.sv | 2 +- tests/check_mem/sub_addr.sv | 32 ++++++++++++++++++++++++++++++++ 2 files changed, 33 insertions(+), 1 deletion(-) create mode 100644 tests/check_mem/sub_addr.sv diff --git a/tests/check_mem/negative_idx.sv b/tests/check_mem/negative_idx.sv index dcfad94a3..99a26cdae 100644 --- a/tests/check_mem/negative_idx.sv +++ b/tests/check_mem/negative_idx.sv @@ -10,4 +10,4 @@ module top; assert(a3[-1][0] == 0); assert(a3[-1][1] == 3); end -endmodule \ No newline at end of file +endmodule diff --git a/tests/check_mem/sub_addr.sv b/tests/check_mem/sub_addr.sv new file mode 100644 index 000000000..cc4cb3ba3 --- /dev/null +++ b/tests/check_mem/sub_addr.sv @@ -0,0 +1,32 @@ +module memtest05(clk, addr, wdata, rdata, wen); + +input clk; +input [1:0] addr; +input [7:0] wdata; +output reg [7:0] rdata; +input [3:0] wen; + +reg [7:0] mem [0:3] = {8'h01, 8'h23, 8'h45, 8'h67}; + +integer i; +always @(posedge clk) begin + for (i = 0; i < 4; i = i+1) + if (wen[i]) mem[addr][i*2 +: 2] <= wdata[i*2 +: 2]; + rdata <= mem[addr]; +end + +always @(posedge clk) begin + // not sure how to verify this one without SBY + // or alternatively, how to replicate the problematic sub addressing without the read&write + assume (wen == 0); + assert (mem[0][7:4] == 4'h0); + assert (mem[0][3:0] == 4'h1); + assert (mem[1][7:4] == 4'h2); + assert (mem[1][3:0] == 4'h3); + assert (mem[2][7:4] == 4'h4); + assert (mem[2][3:0] == 4'h5); + assert (mem[3][7:4] == 4'h6); + assert (mem[3][3:0] == 4'h7); +end + +endmodule From 5f53410db71d76f55af5f98cf998ffa4e567169e Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 29 May 2026 18:40:25 +1200 Subject: [PATCH 09/10] verific: Fix negative array dimensions Recurse over memory dimensions once, doing both our min/max address checking and parsing out the initval. This also avoids problems with negative numbers (if `a < b` and one or both are negative, `a` might be the intended `max_addr_chunk`). Fix sub addressing, where we use some but not all of the current dimension's bits. --- frontends/verific/verific.cc | 119 ++++++++++++++++------------------- frontends/verific/verific.h | 2 +- 2 files changed, 56 insertions(+), 65 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 24c91c3c4..4d1bd0e48 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1444,30 +1444,48 @@ static std::string sha1_if_contain_spaces(std::string str) return str; } -void VerificImporter::recurse_ascii_initdata(RTLIL::Module *module, RTLIL::Memory *memory, Net *net, const char *&ascii_initdata, TypeRange *typeRange, int base_idx) { +void VerificImporter::recurse_mem_dimensions(RTLIL::Module *module, RTLIL::Memory *memory, Net *net, const char *&ascii_initdata, int max_bits_in_addr, const RTLIL::SigSpec &prefix, TypeRange *typeRange) { if (typeRange == nullptr) typeRange = net->GetOrigTypeRange(); auto *nextRange = typeRange->GetNext(); - base_idx <<= typeRange->NumBits(); auto left = typeRange->LeftRangeBound(); auto right = typeRange->RightRangeBound(); - for (auto i = left; left < right ? i <= right : i >= right; left < right ? i++ : i--) { - auto next_idx = base_idx + i; - if (nextRange != nullptr) { - recurse_ascii_initdata(module, memory, net, ascii_initdata, nextRange, next_idx); + bool is_up = left < right; + for (auto i = left; is_up ? i <= right : i >= right; is_up ? i++ : i--) { + // TODO verific can do u64 + auto max_bits = max_bits_in_addr - prefix.size(); + auto next_sig = SigSpec(Const(i, typeRange->NumBits())); + auto extra_bits = next_sig.size() - max_bits; + if (extra_bits > 0) { + next_sig = next_sig.extract_end(extra_bits); + auto extra_inc = (1 << extra_bits) - 1; + i = is_up ? i + extra_inc : i - extra_inc; + } + next_sig.append(prefix); + if (nextRange != nullptr && extra_bits < 0) { + recurse_mem_dimensions(module, memory, net, ascii_initdata, max_bits_in_addr, next_sig, nextRange); } else { + if (next_sig.size() != max_bits_in_addr) { + // TODO verific can do u64 + log_error("Expected %d bits for addr but got %d!\n", max_bits_in_addr, next_sig.size()); + } Const initval = Const(State::Sx, memory->width); bool initval_valid = false; - for (int bit_idx = memory->width-1; bit_idx >= 0; bit_idx--) { - if (*ascii_initdata == 0) - break; - if (*ascii_initdata == '0' || *ascii_initdata == '1') { - initval.set(bit_idx, (*ascii_initdata == '0') ? State::S0 : State::S1); - initval_valid = true; + if (ascii_initdata) { + for (int bit_idx = memory->width-1; bit_idx >= 0; bit_idx--) { + if (*ascii_initdata == 0) + break; + if (*ascii_initdata == '0' || *ascii_initdata == '1') { + initval.set(bit_idx, (*ascii_initdata == '0') ? State::S0 : State::S1); + initval_valid = true; + } + ascii_initdata++; } - ascii_initdata++; } + if (!next_sig.convertible_to_int()) + log_error("Address %s on RAM for identifier '%s' too wide!\n", log_signal(next_sig), net->Name()); + auto next_idx = next_sig.as_int(); if (initval_valid) { RTLIL::Cell *cell = module->addCell(new_verific_id(net), ID($meminit)); cell->parameters[ID::WORDS] = 1; @@ -1478,6 +1496,8 @@ void VerificImporter::recurse_ascii_initdata(RTLIL::Module *module, RTLIL::Memor cell->parameters[ID::WIDTH] = memory->width; cell->parameters[ID::PRIORITY] = RTLIL::Const(autoidx-1); } + memory->start_offset = min(memory->start_offset, next_idx); + memory->size = max(memory->size, next_idx); } } } @@ -1690,58 +1710,10 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma } int number_of_words = number_of_bits / min_bits_in_word; - // TODO Verific has u64 sizes - int size = 1 << max_bits_in_addr; - int min_idx = 0; - int max_idx = size - 1; - - // attempt to infer min/max address for memory definition - RTLIL::SigSpec min_addr, max_addr; - auto typeRange = net->GetOrigTypeRange(); - while (typeRange) { - auto left = typeRange->LeftRangeBound(); - auto right = typeRange->RightRangeBound(); - RTLIL::SigSpec min_addr_chunk(RTLIL::Const(left > right ? right : left, typeRange->NumBits())); - min_addr_chunk.reverse(); - min_addr.append(min_addr_chunk); - - RTLIL::SigSpec max_addr_chunk(RTLIL::Const(left > right ? left : right, typeRange->NumBits())); - max_addr_chunk.reverse(); - max_addr.append(max_addr_chunk); - - typeRange = typeRange->GetNext(); - } - min_addr = min_addr.extract(0, max_bits_in_addr); - max_addr = max_addr.extract(0, max_bits_in_addr); - min_addr.reverse(); - max_addr.reverse(); - - if (min_addr.convertible_to_int()) { - min_idx = min_addr.as_int(); - if (max_addr.convertible_to_int()) { - max_idx = max_addr.as_int(); - } else { - log_debug("Unable to set maximum index\n"); - } - size = max_idx - min_idx + 1; - } else { - log_debug("Unable to set minimum index\n"); - } - - // sanity check we haven't shrunk the memory - log_assert(size >= number_of_words); memory->width = min_bits_in_word; - memory->size = size; - memory->start_offset = min_idx; - - // warn on oversize memories - // TODO consider using a minimum ratio? - if (size > number_of_words) { - float ratio = size / (float)number_of_words; - log_warning("RAM for identifier '%s' may be up to %.0f%% oversize due to addressing\n", net->Name(), (ratio-1)*100); - log_debug("Expected memory of size %d words, but got %d for address range %d to %d (inclusive)\n", number_of_words, size, min_idx, max_idx); - } + memory->size = 0; + memory->start_offset = INT_MAX; const char *ascii_initdata = net->GetWideInitialValue(); if (ascii_initdata) { @@ -1753,7 +1725,26 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma log_assert(*ascii_initdata == 'b'); ascii_initdata++; } - recurse_ascii_initdata(module, memory, net, ascii_initdata); + } + + // process initdata and fixup min/max address + auto prefix = SigSpec(); + recurse_mem_dimensions(module, memory, net, ascii_initdata, max_bits_in_addr, prefix); + + auto min_idx = memory->start_offset; + auto max_idx = memory->size; + memory->size = max_idx - min_idx + 1; + + // sanity check we haven't shrunk the memory + if (memory->size < number_of_words) + log_error("Expected memory of size %d words, but got %d for address range %d to %d (inclusive)\n", number_of_words, memory->size, min_idx, max_idx); + + // warn on oversize memories + // TODO consider using a minimum ratio? + if (memory->size > number_of_words) { + float ratio = memory->size / (float)number_of_words; + log_warning("RAM for identifier '%s' may be up to %.0f%% oversize due to addressing\n", net->Name(), (ratio-1)*100); + log_debug("Expected memory of size %d words, but got %d for address range %d to %d (inclusive)\n", number_of_words, memory->size, min_idx, max_idx); } continue; } diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h index 478ab82cb..0bd4d800a 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -67,7 +67,7 @@ struct VerificClocking { struct VerificImporter { private: - void recurse_ascii_initdata(RTLIL::Module *module, RTLIL::Memory *memory, Verific::Net *net, const char *&ascii_initdata, Verific::TypeRange *typeRange = nullptr, int base_idx = 0); + void recurse_mem_dimensions(RTLIL::Module *module, RTLIL::Memory *memory, Verific::Net *net, const char *&ascii_initdata, int max_bits_in_addr, const RTLIL::SigSpec &prefix, Verific::TypeRange *typeRange = nullptr); public: RTLIL::Module *module; Verific::Netlist *netlist; From 0360a4bd0af91ba8b019dbf77d2dd9b8a0f7b095 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 30 May 2026 11:06:11 +1200 Subject: [PATCH 10/10] tests/check_mem: Drop unused init check It was also raising an error in `read_verilog`. --- tests/check_mem/sub_addr.sv | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/tests/check_mem/sub_addr.sv b/tests/check_mem/sub_addr.sv index cc4cb3ba3..025bdc881 100644 --- a/tests/check_mem/sub_addr.sv +++ b/tests/check_mem/sub_addr.sv @@ -6,7 +6,7 @@ input [7:0] wdata; output reg [7:0] rdata; input [3:0] wen; -reg [7:0] mem [0:3] = {8'h01, 8'h23, 8'h45, 8'h67}; +reg [7:0] mem [0:3]; integer i; always @(posedge clk) begin @@ -15,18 +15,4 @@ always @(posedge clk) begin rdata <= mem[addr]; end -always @(posedge clk) begin - // not sure how to verify this one without SBY - // or alternatively, how to replicate the problematic sub addressing without the read&write - assume (wen == 0); - assert (mem[0][7:4] == 4'h0); - assert (mem[0][3:0] == 4'h1); - assert (mem[1][7:4] == 4'h2); - assert (mem[1][3:0] == 4'h3); - assert (mem[2][7:4] == 4'h4); - assert (mem[2][3:0] == 4'h5); - assert (mem[3][7:4] == 4'h6); - assert (mem[3][3:0] == 4'h7); -end - endmodule