diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 10feac3bc..f3e49142e 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1444,6 +1444,64 @@ static std::string sha1_if_contain_spaces(std::string str) return str; } +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(); + auto left = typeRange->LeftRangeBound(); + auto right = typeRange->RightRangeBound(); + 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; + 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++; + } + } + 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; + 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); + } + memory->start_offset = min(memory->start_offset, next_idx); + memory->size = max(memory->size, next_idx); + } + } +} + 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(); @@ -1630,22 +1688,32 @@ 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; + + memory->width = min_bits_in_word; + memory->size = 0; + memory->start_offset = INT_MAX; const char *ascii_initdata = net->GetWideInitialValue(); if (ascii_initdata) { @@ -1657,32 +1725,26 @@ 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; - 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); - } - } + } + + // 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 f33a380f7..0bd4d800a 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -66,6 +66,9 @@ struct VerificClocking { struct VerificImporter { +private: + 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; diff --git a/passes/cmds/check.cc b/passes/cmds/check.cc index 6e0d65297..426216800 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,95 @@ 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("-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; + } + void execute(std::vector args, RTLIL::Design *design) override + { + 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; + } + + 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, &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 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) + 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/Makefile b/tests/Makefile index 4291ee58d..1721dba71 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -74,6 +74,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 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/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..99a26cdae --- /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 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/check_mem/sub_addr.sv b/tests/check_mem/sub_addr.sv new file mode 100644 index 000000000..025bdc881 --- /dev/null +++ b/tests/check_mem/sub_addr.sv @@ -0,0 +1,18 @@ +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]; + +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 + +endmodule 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 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: