Hi everyone,
I am implementing and verifying an RV32A Atomic extension in a 5-stage pipelined RISC-V core using Spike as the reference model.
I observed a mismatch between my RTL and Spike for the following instruction sequence:
lr.w.rl zero,(tp)
sc.w.rl s7,t1,(tp)
In this case:
* Spike returns:
s7 = 1
indicating SC failure and suppressing the store.
* My RTL returns:
s7 = 0
and performs the store successfully.
However, I observed that a very similar sequence passes successfully in Spike:
lr.w.rl zero,(sp)
sc.w.rl a3,s2,(sp)
In this case:
* Spike returns success (`rd = 0`)
* Store happens correctly.
From the Spike log:
Failing case:
Address = 0x80015e94
Spike WB = 1
Store suppressed
Passing case:
Address = 0x80015d3c
Spike WB = 0
Store successful
My questions are:
1. Is this behavior expected according to the RISC-V A-extension specification?
2. Can Spike legally fail an SC instruction spuriously even when no obvious conflicting write exists?
3. Is there any address-dependent reservation invalidation behavior in Spike?
4. Does the `.rl` variant affect reservation behavior in this scenario?
5. Should RTL verification allow SC failures even without visible interference?
I understand that SC failure may be implementation-dependent, but I would like clarification on whether this specific Spike behavior is expected and spec-compliant.
Thank you.
<img width="446" height="239" alt="Image" src="https://github.com/user-attachments/assets/df38146c-4bf9-45f6-a822-dc669ec295b0" />
<img width="449" height="257" alt="Image" src="https://github.com/user-attachments/assets/2eefb7d4-929c-4962-a214-1c2247a2ba44" />
Hi everyone,
I am implementing and verifying an RV32A Atomic extension in a 5-stage pipelined RISC-V core using Spike as the reference model.
I observed a mismatch between my RTL and Spike for the following instruction sequence:
lr.w.rl zero,(tp)
sc.w.rl s7,t1,(tp)