RISCV_FORMAL_VALIDADDR ignored for loads and stores

[acw1251]

I'm setting a region of memory to be invalid using RISCV_FORMAL_VALIDADDR. This works as expected for instruction fetch (after fixing some bugs in my processor). Unfortunately I'm still failing some load instruction checks. The example trace it gave me for the test I looked at had a load from an invalid address with spec_trap = 0.

It looks like the following lines in rvfi_insn_check.sv
https://github.com/cliffordwolf/riscv-formal/blob/master/checks/rvfi_insn_check.sv#L104-L105
should be something like this:

        wire mem_access_fault = spec_valid && (spec_rs1_addr == rs1_addr) &&
                ((spec_mem_rmask && !mem_pma_r) || (spec_mem_wmask && !mem_pma_w)
                || ((spec_mem_rmask || spec_mem_wmask) && !`rvformal_addr_valid(spec_mem_addr)));

I tried this out on my processor and all the checks pass now.

[cliffordwolf]

This should be fixed now in current git HEAD.

(Some background: Until now we only had cores with RISCV_FORMAL_VALIDADDR that also had RISCV_FORMAL_PMA_MAP, and the PMA map only contains valid addresses. That's why this was not an issue before.)