bus_imem_fault checks assume compressed instructions are fetched in LSBs of memory read word

[coreyqh]

Hello,

I think the structure of the bus_imem_fault relies on an assumption that imem accesses occur on a per-instruction basis and compressed instructions always sit in the LSBs of an imem transaction.

The core I am working with fetches ahead with a prefetch buffer, reading aligned words from memory. This means that a compressed instruction can live in the upper bits of an instruction bus transaction.

However, the following assertions are present in the rvfi_bus_imem_fault_check.sv file:

if (check) begin
    if (rvfi_valid[`RISCV_FORMAL_CHANNEL_IDX]) begin
        pc = rvfi_pc_rdata[`RISCV_FORMAL_CHANNEL_IDX*`RISCV_FORMAL_XLEN +: `RISCV_FORMAL_XLEN];
        insn = rvfi_insn[`RISCV_FORMAL_CHANNEL_IDX*`RISCV_FORMAL_ILEN +: `RISCV_FORMAL_ILEN];

        if (`rvformal_addr_valid(pc) && pc == imem_addr) begin
            cover (1);
            assert (rvfi_trap[`RISCV_FORMAL_CHANNEL_IDX]);
            assert (insn == 0);
`ifdef RISCV_FORMAL_MEM_FAULT
            assert (rvfi_mem_fault[`RISCV_FORMAL_CHANNEL_IDX]);
`endif
        end;

        if (`rvformal_addr_valid(pc+2) && pc+2 == imem_addr) begin
            cover (1);
            assert (rvfi_trap[`RISCV_FORMAL_CHANNEL_IDX]);
            assert (insn == 0);
`ifdef RISCV_FORMAL_MEM_FAULT
            assert (rvfi_mem_fault[`RISCV_FORMAL_CHANNEL_IDX]);
`endif
        end;
    end
end

Where the 2nd set of assertions (lines 65-70) check that any instruction with a PC that is 2 less than an address that is assume()ed to cause an access fault, must also cause an access fault.

This is true when an entire word is accessed for compressed instructions, but not for machines that prefetch and may already have a compressed instruction from a previous valid memory access.

As an example, in the counter example trace produced by the failed check, the random reg imem_addr (that is assume()ed to cause an access fault) is 0x4000. Based on these assertions, any instruction with a PC of 0x3ffe should also access fault. However, since the aligned word beginning at 0x3ffc was fetched from a valid memory operation a few cycles before, the prefetch buffer already held a valid compressed instruction starting at 0x3ffe.

I would suggest amending this check to include an additional assume() that the current instruction is not compressed, something like the following:

if (check) begin
    if (rvfi_valid[`RISCV_FORMAL_CHANNEL_IDX]) begin
        pc = rvfi_pc_rdata[`RISCV_FORMAL_CHANNEL_IDX*`RISCV_FORMAL_XLEN +: `RISCV_FORMAL_XLEN];
        insn = rvfi_insn[`RISCV_FORMAL_CHANNEL_IDX*`RISCV_FORMAL_ILEN +: `RISCV_FORMAL_ILEN];

        if (`rvformal_addr_valid(pc) && pc == imem_addr) begin
            cover (1);
            assert (rvfi_trap[`RISCV_FORMAL_CHANNEL_IDX]);
            assert (insn == 0);
`ifdef RISCV_FORMAL_MEM_FAULT
            assert (rvfi_mem_fault[`RISCV_FORMAL_CHANNEL_IDX]);
`endif
        end;
        if (`rvformal_addr_valid(pc+2) && pc+2 == imem_addr) begin
            cover (1);
            assume(insn[1:0] == 2'b11); // following assertions only hold for non-compressed instructions 
            assert (rvfi_trap[`RISCV_FORMAL_CHANNEL_IDX]);
            assert (insn == 0);
`ifdef RISCV_FORMAL_MEM_FAULT
            assert (rvfi_mem_fault[`RISCV_FORMAL_CHANNEL_IDX]);
`endif
        end;
    end
end

Unfortunately, however, the rvfi_insn signal is required to be 0 when an instruction access fault occurs, so this cannot be done.

I think it can only be guaranteed that an exact match of the PC with an address proven to cause an access fault will cause an access fault. This is what is checked by the first set of assertions in the code above. Unfortunately, I believe that the second set of assertions rely on implementation specific choices.

Let me know if my understanding of this check is correct, and if I am right to suspect that this is not true in all implementations.

Thanks!

[coreyqh]

I think the following assertion from rvfi_bus_imem_check may reflect the same issue.

					if (`rvformal_addr_valid(pc) && pc == imem_addr) begin
						cover (1);
						assert (insn[15:0] == imem_data);
					end;

This assertion checks that (assuming a given half word can be read without error from a given memory address) then an instruction with the PC that is the same as that address must have that half word in the lower 16 bits.

Again, this suffers from the underlying design assumption that imem accesses occur on a per-instruction basis, and do lot leave open the possibility of having two half-instructions that come from separate memory transactions.

In my case, the lower half comes from a valid address and the upper half from an invalid one. Since this causes an instruction access fault, per the RVFI spec the instruction must be all zeros and therefore fails this assertion.