Skip to content

Conversation

Wren6991
Copy link

@Wren6991 Wren6991 commented Sep 19, 2025

When a 16-bit instruction occurs immediately before a faulting instruction fetch, the bus_imem_fault check erroneously asserts that it must fault, as though the instruction were 32-bit and the fetch had occurred in its second half.

Avoid this by introducing a new free variable imem_prev_32bit which conditionally enables the problematic check on pc + 2, and also constrains fetch from the halfword before imem_addr to start with 2'b11, i.e. to be a 32-bit instruction.

This might seem to weaken the check because if the data at imem_addr - 2 is actually the second half of a previous 32-bit instruction, this would force two bits in the middle of that instruction to be 2'b11, limiting the possible instructions. However in this case imem_addr will take exactly the value of pc so, assuming fetches are at least 32 bits in size, the pc+2 assertions are unnecessary. If the pc+2 assertions aren't needed then the imem_prev_32bit variable can be clear, meaning the 2'b11 constraint doesn't apply. Therefore I don't think this restricts the instruction sequences that can be checked, at least for a processor with at least 32-bit-wide fetch.

See discussion in #44

The bus_imem_fault check fails on Hazard3 without this patch, and passes with it. Repro:

git clone [email protected]:Wren6991/Hazard3.git hazard3
cd hazard3
git checkout 0722c1a64
. project_env.sh
git submodule update --init -- scripts test/formal/riscv-formal
cd test/formal/riscv-formal/riscv-formal/cores/hazard3/
./generate.sh 
make -C checks bus_imem_fault_ch0

(note this is a different git hash than the one I gave in the issue thread because I had to make a couple of changes to my RVFI monitor)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant