diff --git a/passes/cmds/check.cc b/passes/cmds/check.cc index 1019c2955..34c89dae0 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 38596f63b..baa70290b 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) @@ -112,11 +125,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: