MemECC - possible spurious store-response alerts

As I'm continuing some formal verification work looking into the ECC functionality in Ibex, I hit another issue here with my property below:

```
// Property: no_store_ecc_alert
// Intent: Store acknowledgements must never raise the store integrity error output because the
// ECC decoder only inspects read data.
// Source: ibex_load_store_unit.sv lines 520-555 (analysis of MemECC handling).
// Timing: Same-cycle implication on the LSU clk domain (posedge clk_i, active-low reset).
// Status: intended_to_pass (BUG_WITH_ASSERTION once it fails).
generate
if (MemECC) begin : gen_store_ecc_assert
property no_store_ecc_alert;
@(posedge clk_i) disable iff (!rst_ni)
(data_rvalid_i && data_we_q) |-> !store_resp_intg_err_o;
endproperty
ast_no_store_ecc_alert: assert property (no_store_ecc_alert);
end
endgenerate

```
Here are some thoughts/questions I was thinking and the detailed analysis:
- **Store acknowledgement marker**: In ibex_load_store_unit, the FSM registers the operation direction in data_we_q (latched when the request issues). When the bus returns data_rvalid_i, the LSU still has data_we_q telling whether that outstanding access was a store (1 means store). See data_we_q assignments/uses in src/rtl/ibex_load_store_unit.sv.
- **“Arbitrary” data on store responses**: The external bus returns a 32b payload even for writes. That payload is don't-care (typically the previous bus contents or zero), but because the LSU feeds data_rdata_i—including its 7 ECC bits—into prim_secded_inv_39_32_dec, any random combination of parity bits yields a non-zero syndrome (data_intg_err=1). With data_we_q=1, the logic sets _store_resp_intg_err_o = data_intg_err & data_rvalid_i & data_we_q_, so every store response can assert the integrity flag regardless of actual memory contents.
- **Why the alert exists even though stores can’t be checked**: The design seems to implement symmetric reporting of “integrity errors on responses”, but it overlooked that the only integrity checker instantiated comes from the read-data path. There is no encoder/decoder on the returning data for stores—only the outgoing write data goes through prim_secded_inv_39_32_enc. Therefore, _store_resp_intg_err_o_ has no real meaning; it simply mirrors the load-side data_intg_err. Because ibex_core ORs this flag into alert_major_bus_o (src/rtl/ibex_core.sv), the spurious ECC flag propagates up as an alert even though no ECC verification was performed for the store.
- _data_rvalid_i_ does toggle for stores in the design. The LSU is treating the incoming _data_rvalid_i_ as “response complete” for both loads and stores (look at l_su_resp_valid_o = (ls_fsm_cs == IDLE) & data_rvalid_i & …_ in src/rtl/ibex_load_store_unit.sv). So a compliant bus will raise _data_rvalid_i_ to acknowledge a write, even though it doesn’t return meaningful data. My formal run left the bus unconstrained, but the failure it found is exactly how the RTL runs: on a store response, data_rvalid_i=1, data_we_q=1 (latched direction), and the payload bits are don’t-care. The ECC decoder still chews on those 39 bits (prim_secded_inv_39_32_dec). Any junk parity/data combination gives a non-zero syndrome → _data_intg_err=1_. Because the code simply does _store_resp_intg_err_o = data_intg_err & data_rvalid_i & data_we_q_, the store acknowledgement propagates that bogus error all the way to _alert_major_bus_o_. So the bug isn’t a formal-only artifact—it’s the natural hardware behavior unless the bus HW “kindly” echoes a valid ECC word for every store, which it doesn’t by spec.

Looking at the actual datapath:

- **Read side only:** The only ECC checker in the LSU is prim_secded_inv_39_32_dec u_data_intg_dec at src/rtl/ibex_load_store_unit.sv. Its input is _data_rdata_i_ (bus read data). The comments immediately above it say “Read data integrity check … _data_intg_err = |ecc_err_;”. That’s the sole source of _data_intg_err_.
- **Write side**: When MemECC is enabled, the write path instantiates prim_secded_inv_39_32_enc at src/rtl/ibex_load_store_unit.sv to generate parity bits for _data_wdata_o_. There is no decoder on returning store data; the protocol doesn’t send meaningful data back for writes.
- **Alert wiring**: _store_resp_intg_err_o_ is literally _data_intg_err & data_rvalid_i & data_we_q_ (src/rtl/ibex_load_store_unit.sv). Since _data_intg_err_ comes only from the read decoder, tying it to a write response has no physical basis. The intent is spelled out in the comment block just above: “Integrity errors are their own category… The _data_intg_err_ signal is generated combinatorially from the incoming _data_rdata_i_.” No mention of a store checker because there isn’t one. So the design itself dictates “ECC errors are valid only during reads”: the checker exists only on read data, and the documentation around it explicitly says it uses _data_rdata_i_ (read path) to generate errors. The store alert output simply reuses that read-only flag, which is why it seems bogus.

So what use is _store_resp_intg_err_o_? if the _data_intg_err_ is only trigger from reads, then what possibly can the _store_resp_intg_err_o_ mean?

• It effectively looks to be meaningless. _store_resp_intg_err_o_ is meant to flag an integrity failure on a store response, but the circuit never actually checks store data— _data_intg_err_ is computed exclusively from the read-return bus (prim_secded_inv_39_32_dec on _data_rdata_i_). When a write completes the bus still raises _data_rvalid_i_, but the returned “data” is don’t-care; feeding that junk through the read decoder is what produces the false alert. So _store_resp_intg_err_o_ is just _data_intg_err & data_we_q_, i.e. “whatever the read checker said, but only when the outstanding transaction happened to be a store.” That’s why the assertion fails and why the top-level alert OR tree propagates bogus store faults: the signal doesn’t represent any real store-side ECC check currently.

The possible fix might either to drop _store_resp_intg_err_o_ (tie it low) or to implement a genuine write-data return check—but the current RTL clearly intends only the read path to validate ECC.

## Observed Behavior

## Expected Behavior

## Steps to reproduce the issue

## My Environment

**EDA tool and version:**

**Operating system:**

**Version of the Ibex source code:**

Start in src/rtl/ibex_load_store_unit.sv around prim_secded_inv_39_32_dec, data_intg_err, data_we_q, and store_resp_intg_err_o, then trace the alert connection in src/rtl/ibex_core.sv. Reproduce or extend the no_store_ecc_alert formal property described in the issue and confirm that completed stores no longer produce a store integrity alert without changing read-data checking.

Written by the indexing model from the issue text.