[FIRRTL] (mem) mismatch

The following FIRRTL program

```python
; seed: 6243
circuit top_mod :
module top_mod :
input clock0: Clock
input raddr: UInt<10>
input waddr: UInt<10>
input wdata: UInt<20>
output tmp54: UInt<20>
mem tmp53:
data-type => UInt<20>
depth => 10
read-latency => 0
write-latency => 1
read-under-write => undefined
reader => r0
writer => w0
tmp53.r0.clk <= clock0
tmp53.r0.en <= UInt(0)
tmp53.r0.addr <= waddr
tmp53.w0.clk <= clock0
tmp53.w0.en <= UInt(1)
tmp53.w0.addr <= raddr
tmp53.w0.data <= wdata
tmp53.w0.mask <= UInt(1)
tmp54 <= tmp53.r0.data
```

Compiled with firtool --lower-to-hw --infer-widths --imconstprop --lowering-options=disallowPackedArrays,emittedLineLength=8192 --mlir-timing --verilog -o=$VFILE2 produces this Verilog:

```verilog
module tmp53_ext( // a_top_mod.fir:9:5
input [3:0] R0_addr,
input R0_en, R0_clk,
input [3:0] W0_addr,
input W0_en, W0_clk,
input [19:0] W0_data,
input W0_mask,
output [19:0] R0_data);

reg [19:0] Memory[0:9];

wire _T = W0_en & W0_mask;
always @(posedge W0_clk) begin
if (_T)
Memory[W0_addr] <= W0_data;
end // always @(posedge)
assign R0_data = R0_en ? Memory[R0_addr] : 20'bx; // a_top_mod.fir:9:5
endmodule

module top_mod( // a_top_mod.fir:3:10
input clock0,
input [9:0] raddr, waddr,
input [19:0] wdata,
output [19:0] tmp54);

tmp53_ext tmp53 ( // a_top_mod.fir:9:5
.R0_addr (waddr[3:0]), // a_top_mod.fir:19:19
.R0_en (1'h0), // a_top_mod.fir:18:20
.R0_clk (clock0),
.W0_addr (raddr[3:0]), // a_top_mod.fir:22:19
.W0_en (1'h1), // a_top_mod.fir:21:20
.W0_clk (clock0),
.W0_data (wdata),
.W0_mask (1'h1), // a_top_mod.fir:21:20
.R0_data (tmp54)
);
endmodule
```

Compiled with firrtl-1.5-SNAPSHOT produces this Verilog:

```verilog
module top_mod(
input clock0,
input [9:0] raddr,
input [9:0] waddr,
input [19:0] wdata,
output [19:0] tmp54
);
`ifdef RANDOMIZE_GARBAGE_ASSIGN
reg [31:0] _RAND_1;
`endif // RANDOMIZE_GARBAGE_ASSIGN
`ifdef RANDOMIZE_MEM_INIT
reg [31:0] _RAND_0;
`endif // RANDOMIZE_MEM_INIT
reg [19:0] tmp53 [0:9];
wire tmp53_r0_en;
wire [3:0] tmp53_r0_addr;
wire [19:0] tmp53_r0_data;
wire [19:0] tmp53_w0_data;
wire [3:0] tmp53_w0_addr;
wire tmp53_w0_mask;
wire tmp53_w0_en;
assign tmp53_r0_en = 1'h0;
assign tmp53_r0_addr = waddr[3:0];
`ifndef RANDOMIZE_GARBAGE_ASSIGN
assign tmp53_r0_data = tmp53[tmp53_r0_addr];
`else
assign tmp53_r0_data = tmp53_r0_addr >= 4'ha ? _RAND_1[19:0] : tmp53[tmp53_r0_addr];
`endif // RANDOMIZE_GARBAGE_ASSIGN
assign tmp53_w0_data = wdata;
assign tmp53_w0_addr = raddr[3:0];
assign tmp53_w0_mask = 1'h1;
assign tmp53_w0_en = 1'h1;
assign tmp54 = tmp53_r0_data;
always @(posedge clock0) begin
if (tmp53_w0_en & tmp53_w0_mask) begin
tmp53[tmp53_w0_addr] <= tmp53_w0_data;
end
end
// Register and memory initialization
`ifdef RANDOMIZE_GARBAGE_ASSIGN
`define RANDOMIZE
`endif
`ifdef RANDOMIZE_INVALID_ASSIGN
`define RANDOMIZE
`endif
`ifdef RANDOMIZE_REG_INIT
`define RANDOMIZE
`endif
`ifdef RANDOMIZE_MEM_INIT
`define RANDOMIZE
`endif
`ifndef RANDOM
`define RANDOM $random
`endif
`ifdef RANDOMIZE_MEM_INIT
integer initvar;
`endif
`ifndef SYNTHESIS
`ifdef FIRRTL_BEFORE_INITIAL
`FIRRTL_BEFORE_INITIAL
`endif
initial begin
`ifdef RANDOMIZE
`ifdef INIT_RANDOM
`INIT_RANDOM
`endif
`ifndef VERILATOR
`ifdef RANDOMIZE_DELAY
#`RANDOMIZE_DELAY begin end
`else
#0.002 begin end
`endif
`endif
`ifdef RANDOMIZE_GARBAGE_ASSIGN
_RAND_1 = {1{`RANDOM}};
`endif // RANDOMIZE_GARBAGE_ASSIGN
`ifdef RANDOMIZE_MEM_INIT
_RAND_0 = {1{`RANDOM}};
for (initvar = 0; initvar < 10; initvar = initvar+1)
tmp53[initvar] = _RAND_0[19:0];
`endif // RANDOMIZE_MEM_INIT
`endif // RANDOMIZE
end // initial
`ifdef FIRRTL_AFTER_INITIAL
`FIRRTL_AFTER_INITIAL
`endif
`endif // SYNTHESIS
endmodule
```
`Yosys 0.13+15 (git sha1 bc027b2ca, clang 13.0.0 -fPIC -Os)` reports formal mismatch:

```
ERROR: Found 20 unproven $equiv cells in 'equiv_status -assert'.
```

Reproduce the issue with the FIRRTL program and the shown firtool command, then compare its Verilog with the firrtl-1.5-SNAPSHOT output using Yosys formal equivalence. Trace the memory lowering and address-width behavior in firtool; done means the generated designs no longer produce unproven $equiv cells for this case.

Written by the indexing model from the issue text.