3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-05-29 21:36:33 +00:00

check_mem: Add -non-const option

Can identify potentially dangerous addressing, but also prone to false-positives.
This commit is contained in:
Krystine Sherwin 2026-05-29 18:40:24 +12:00
parent 099c664dc9
commit f6327cc444
No known key found for this signature in database
2 changed files with 82 additions and 3 deletions

View file

@ -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)

View file

@ -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