3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-23 00:55:32 +00:00

mem2reg: tolerate out of bounds constant accesses

This brings the mem2reg behavior in line with the nomem2reg behavior.
This commit is contained in:
Zachary Snow 2021-05-26 18:22:31 -04:00 committed by Zachary Snow
parent d9f11bb7a6
commit c79fbfe0a1
4 changed files with 94 additions and 5 deletions

View file

@ -0,0 +1,19 @@
module top(
input clk,
input wire [1:0] sel,
input wire [7:0] base,
output reg [7:0] line
);
reg [0:7] mem [0:2];
generate
genvar i;
for (i = 0; i < 4; i = i + 1) begin : gen
always @(posedge clk)
mem[i] <= i == 0 ? base : mem[i - 1] + 1;
end
endgenerate
always @(posedge clk)
line = mem[sel];
endmodule

View file

@ -0,0 +1,27 @@
module top;
reg [0:7] mem [0:2];
initial mem[1] = '1;
wire [31:0] a, b, c, d;
assign a = mem[1];
assign b = mem[-1];
assign c = mem[-1][0];
assign d = mem[-1][0:1];
always @* begin
assert ($countbits(a, '0) == 24);
assert ($countbits(a, '1) == 8);
assert ($countbits(a, 'x) == 0);
assert ($countbits(b, '0) == 24);
assert ($countbits(b, 'x) == 8);
assert ($countbits(c, '0) == 31);
assert ($countbits(c, 'x) == 1);
assert ($countbits(d, '0) == 30);
assert ($countbits(d, 'x) == 2);
end
endmodule

View file

@ -0,0 +1,6 @@
read_verilog -sv -mem2reg mem_bounds.sv
proc
flatten
opt -full
select -module top
sat -verify -seq 1 -tempinduct -prove-asserts -show-all -enable_undef