SymbioticEDA / riscv-formal

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

Notion of a memory bus error #18

Closed ben-marshall closed 5 years ago

ben-marshall commented 5 years ago

Hi there

I noticed that the insn_lw_ch0 check has no notion of a memory bus error. That is, it only specifies that a trap should be raised iff the address is wrongly aligned, or the misa_ok check fails.

Is there a recommended way of handling this in cores which raise a memory bus error? My current plan is to assume bus responses do not fault, and test that scenario by other means.

Cheers, Ben

cliffordwolf commented 5 years ago

If the bus error is purely a function of the address then this can be done with the experimental RISCV_FORMAL_PMA_MAP feature. See here for details, and here for an example of the current interface (may be subject to change in the future).