Mismatch between uarch spec and implementation for FwdRdAck/LOAD_FWDACK transition to Shared

[mujahid-10xe]

Description:
According to the micro-arch (Section 3.2, Figure 5), the following transitions should occur when a FwdRdAck is received from the owner:
M → S
E → S
Reference Figure:

Currently, the RTL does not handle the M → S transition.

Verification Setup:
1- I wrote the following assertion based on the specification:
as_state_m_s_load_fwd_ack: assert property(
l2.pipe2.ctrl.valid_S2 &&
l2.pipe2.ctrl.msg_type_S2_f == LOAD_FWDACK &&
l2.pipe2.ctrl.l2_way_state_mesi_S2 == MODIFIED
|->
l2.pipe2.ctrl.state_mesi_S2 == SHARED
);

2- When running formal verification, the antecedent (conditions for firing) was covered, but the consequent (transition to SHARED) was never covered.
3- On inspecting the RTL, I found that there is no case defined for this transition in pipe2 of L2 cache.

Conclusion:
When the current state is Modified and a LOAD_FWDACK is received, the next state should transition to Shared, consistent with the specification (Section 3.2, Figure 5). However, the M → S transition is not implemented in the RTL, and as a result, assertions based on the specification fail to cover this scenario. This causes the L2 state machine behavior to diverge from the documented specification and can potentially lead to incorrect coherence behavior when a cache line in M receives a LOAD_FWDACK. To resolve this, the L2 controller state transition logic should be updated to handle the M → S case, similar to the existing E → S transition.

[Jbalkind]

Hi there! Thanks for taking a look at this. Could you tell me more about your methodology here? I want to be sure that we have a full understanding of both the specification and the RTL itself. Have you run any tests to validate that this is causing an issue? It may be that the state machines were not updated to reflect the implementation or that there is more complexity related to the use of writeback guards for example.

[mujahid-10xe]

I compiled the L2 cache module to verify coherency behavior using a formal tool with property-based verification. In this setup, the NoC1 input is constrained so that only LOAD_REQ and STORE_REQ messages can appear for now. I also modeled NoC3 as a response generator that collects outgoing requests from NoC2 (such as LOAD_MEM or LOAD_FWD) and generates the corresponding responses back on NoC3. Additionally, I constrained that wb_req cannot appear in this environment. This setup allows me to focus on verifying the L2 coherence protocol through formal properties.

Within this environment, I wrote several SystemVerilog assertions covering different state transitions defined in the specification, focusing to compare the state diagram’s transitions with the actual RTL behavior in pipeline1 and pipeline2 of the L2. One of these assertions — for the LOAD_FWDACK message — is not covering the expected scenario described in Section 3.2, Figure 5. Specifically, the M → S transition does not occur in the RTL even though it is defined in the spec.

I manually inspected l2_pipe2’s state transition logic and confirmed that there’s no explicit handling for the LOAD_FWDACK case when the line is in the MODIFIED state. There is a defined case for E → S, but not for M → S. This observation aligns with my formal assertion results, where the antecedent was covered but the consequent (transition to SHARED) was never reached.

[Jbalkind]

Ok so am I right in understanding that you haven't actually identified a correctness issue that manifests as a functional bug (with evidence of that bug)? Rather, you're using the specification to set up the formal properties and those don't match with the implementation? I have a feeling that it's going to be more likely that the transition just shouldn't exist in the specification. That or perhaps there is a performance bug that could be in place because the transition isn't implemented.

[mujahid-10xe]

Yes, you’re right — I’m not currently checking for a direct functional bug. My focus right now is on verifying the micro-architectural behavior against the specified state transitions in the spec.

However, there are two possibilities here:
1- The specification might be outdated or incorrect, and the transition shouldn’t actually exist.
2- The specification is correct, but the transition hasn’t been properly implemented in RTL — which could potentially lead to a functional bug later on.

Specifically, according to the MESI protocol, a line in the Modified (M) state must transition to Shared (S) when a Load request is forwarded to the owner, and after receiving the acknowledgment, the state must update from M → S.
If this transition isn’t implemented, it would indeed represent a functional bug in the coherence behavior.

[Jbalkind]

Ok I see. There are multiple other considerations about the protocol that make it more complex than a simple MESI. For one, the L1.5 is likely sending a writeback guard on noc1 which may change which states are transitioned through or cause other effects (I haven't been fully clear on how this affects the pipe2 state, I just know the messages are necessary for ordering purposes). For another, (as far as I recall) the L1.5 itself effectively tracks MSI states rather than full MESI. I vaguely recall that the L1.5 may also be able to do silent downgrades. As a result, I'm not sure whether a simple monitoring of the transition like this is sufficient to observe these cases which could potentially obscure the M->S transition.

[mujahid-10xe]

Well, I don’t think the silent downgrade explanation applies in this case. Silent transitions typically occur for E → M, not for M → S.

If the owner transitions from M → S but the directory isn’t updated accordingly, then the directory would still believe the line is in M and owned by another core. When a new request for the same block arrives, the lookup would still return “state = M, owner = X,” leading the L2 to incorrectly issue a LOAD_FWD instead of a DATA_ACK.
This could result in a functional bug.