SymbioticEDA / riscv-formal

RISC-V Formal Verification Framework
ISC License
573 stars 94 forks source link

RVFI load/store error detection #32

Open udinator opened 4 years ago

udinator commented 4 years ago

Hi, The Ibex core has mechanisms to handle data memory transactions returning error responses. The RVFI spec details that rvfi_trap should be used to indicate memory access violations, but is there any way to signal a load/store error through the interface? Right now, I can view all memory transactions through the RVFI, but I have no way of knowing whether the transaction is actually valid, or has raised an error response. Thanks!

ben-marshall commented 4 years ago

Hi there

If I understand correctly, I came across this issue a while back with my own core. See here for the issue and Clifford's response.

Cheers, Ben

udinator commented 4 years ago

Hi, From the discussion that you linked, this seems similar to a PMP/PMP-type feature, which the Ibex core also implements, but which is separate from the data_err_i signal in the core's load/store memory interface. It seemed like the PMA_MAP issue and the issue I'm facing are somewhat independent problems, so I'm thinking there is currently no way of monitoring this? Best, Udi

ben-marshall commented 4 years ago

so I'm thinking there is currently no way of monitoring this?

Yeah, your're right.

The PMP thing was put forward as a workaround for the fact that riscv-formal has no built-in notion of a memory bus error condition.

Cheers, Ben