search

microsoft / cheriot-ibex

cheriot-ibex is a RTL implementation of CHERIoT ISA based on LowRISC's Ibex core.
Apache License 2.0
73 stars 14 forks source link

Instruction Fetch failing when the Sail doesn't #34

Closed mndstrmr closed 1 month ago

mndstrmr commented 4 months ago

Currently the IF stage will incorrectly raise a fetch error exception in the following two cases:

  1. The instruction is uncompressed and the PC is2**32 - 2, meaning the instruction wraps around the address space, but the PCC allows execution anywhere. This is allowed by the Sail because it checks the two two byte chunks of the instruction separately.
  2. The PC is 0 and PCC.top33 = 2**32. This fails because PCC.top33 - 0 still has the top bit set, even though no overflow occurred. This is easily fixed by updating cheri_bound_vio to 
    assign cheri_bound_vio = /* snip */ || (instr_hdrm[32] & (|if_instr_addr)) || ~hdrm_ok;

The first case is very minor, especially since the RTL is being stricter (not weaker) than the Sail. One could update the RTL to do both checks separately, or update the Sail to do one the one check.

Less ideally, because we know the RTL is stricter than the Spec in a very specific and documentable way I could just allow it in the verification setup and essentially relax the constraint to be at least as strict, instead of identical to. Again, I would obviously prefer not to do this.

kliuMsft commented 4 months ago

Thanks, I will fix #2. @rmn30, does sail allow execution in case #1?

kliuMsft commented 4 months ago

RTL commit 4a739b4 fixed issue #2 (PC=0, top33=0x10000_0000) by extending the math to 34 bit.

mndstrmr commented 4 months ago

I can confirm that your fix did fix the second issue. Are you intending to fix the first or should I close this issue?

kliuMsft commented 4 months ago

Thanks, let's keep this open for now.

rmn30 commented 4 months ago

Hmmm, 1. definitely feels like it shouldn't be allowed. It's unlikely to be an issue in practice as there probably won't be memory mapped at the very bottom and top of the address space. What does the RISC-V spec say about this case?

kliuMsft commented 3 months ago

@mndstrmr , I checked in an RTL fix (2a0c157) by adding the allow_all condition (pcc top33/base32 covers the entire address space). I think it should make it match sail behavior now - please verify. thanks.

mndstrmr commented 1 month ago

This seems to prove, thanks.