Out-of-bounds index addressing in memory module formal verification

[zsxpdsyz]

Hello everyone,

I've encountered some issues when I use SymbiYosys verifying a memory module. Although I know this is not the SymbiYosys repository, I believe this issue might also be related to how Yosys performs synthesis. Therefore, I'm posting here in hopes of getting some help and insights from the community.

The contents of the SystemVerilog file and the SBY configuration file are as follows:
test_ram.sv:

module ram_tb (
    input clk,
    input [2:0] addr,
    input w_en,
    input [15:0] w_data
);
    wire [15:0] r_data1, r_data2;
    ram_5x16 ram1 (
        .addr(addr),
        .r_en(1),
        .r_data(r_data1),
        .w_en(w_en),
        .clk(clk),
        .w_data(w_data)
    );

    ram_5x16 ram2 (
        .addr(addr),
        .r_en(1),
        .r_data(r_data2),
        .w_en(w_en),
        .clk(clk),
        .w_data(w_data)
    );
    always @(clk) begin
        assert(r_data1 == r_data2);
    end

    initial begin
        assume (r_data1 == r_data2);
    end
endmodule

module ram_5x16(
    input [2:0] addr,
    input       r_en,
    output [15:0] r_data,
    input       w_en,
    input       clk,
    input  [15:0] w_data
);

    reg [15:0] Memory [0:4];
    always @ (posedge clk) begin
        if (w_en)
            Memory[addr] <= w_data;
    end
    assign r_data = r_en ? Memory[addr] : 16'bx;

    initial begin
        Memory[0] = 16'b0;
        Memory[1] = 16'b0;
        Memory[2] = 16'b0;
        Memory[3] = 16'b0;
        Memory[4] = 16'b0;
    end

endmodule

test_ram.sby

[options]
# mode prove
mode bmc
depth 11
tbtop sby_tb.sv

[engines]
smtbmc boolector

[script]
read -formal test_ram.sv
prep -top ram_tb

[files]
./test_ram.sv

My goal is to verify that two instantiations of the ram_5x16 module produce the same output data given the same inputs. In theory, r_data1 should indeed be equal to r_data2, but in practice, the verification fails.

I examined the waveform from the generated counterexample, and I suspect the issue may be as follows: The memory we defined only has 5 entries. However, the address used to access the memory is 3 bits width — meaning it can index up to 8 locations. We only initialized entries 0 through 4, but did not initialize entries 5 through 7. The sby tool likely generated an addr value greater than 4, accessing uninitialized memory locations, which leads to differing outputs between the two RAM instances.

How should I do to prevent the verification failure caused by the verfier's random initialization of out-of-bounds memory addresses?

[KrystalDelusion]

I replied in YosysHQ/sby#324 (comment)