Documentation of rvfi_csr_<csrname>_wmask is unclear.

[coreyqh]

Hello, I am running into failing csrw checks that do not seem to make sense. It seems that one of the assertions does not take the write mask into account where I think it should. For the MISA csr, I am failing the following assertion from rvfi_csrw_check.sv:

assert ((csr_insn_cmask & effective_csr_insn_wdata) == 0);

I've been investigating the trace.vcd counter example that sby produced. It executes the instruction 0x30125173 (csrrwi x2, misa, 4).

Since the MISA csr is read only in this implementation, the write mask rvfi_csr_misa_wmask is hardwired to 0. As such, the effective_csr_insn_wdata is the hardwired constant value that the CSR contained out of reset.

since the csr_insn_arg is 4 from the immediate, the write mask is 0x0000_0000, and funct3[1:0] == 2'b01, the following assignment makes csr_insn_cmask 0x0ffff_fffb:

wire [`RISCV_FORMAL_XLEN-1:0] csr_insn_cmask =
    /* CSRRW, CSRRWI */ (rvfi.insn[13:12] == 1) ? ~csr_insn_arg :
    /* CSRCS, CSRRCI */ (rvfi.insn[13:12] == 3) ? csr_insn_arg : 0;

Then, since csr_insn_cmask is nearly all 1s, and the MISA CSR contains a 0x40801104, the above assertion fails.

While I understand that for writable CSRs, this assertion checks that there are no cleared bits that are still 1 in the resultant CSR values, in this case I think the all zero write mask should have some bearing.

Let me know if there is something I am missing, or how I can change the check generation flow to fix this.
Thanks!

[KrystalDelusion]

The wmask field is not "which bits have been written," it is "which bits in wdata are valid." If your wdata value is the read-only value, all of the bits are valid and wmask should be all 1's not all 0's. Your problem is not that the all zero write mask has no bearing, but rather that each zero bit in the write mask means that the corresponding "effective" bit gets taken from rdata instead of wdata.

I'll leave this issue open for now because it indicates a problem with how the rmask and wmask fields are documented.

[coreyqh]

That makes a lot more sense, thank you for your response!