RVFI CSR support

[Timmmm]

Is there a reason Ibex's RVFI interface doesn't support CSR writes? I'd like to add it so we can trace CSR writes.

Note there appear to be two different approaches:

1. Give each supported CSR a wire.
2. Use a vector of wires. Hard to tell what each index corresponds to.
3. Use a 4096-element vector of wires!

That last one seems pretty mad. I think the first options is probably best given the relatively small number of CSRs that Ibex has. I'd probably put them in an interface to save wiring insanity. Something like:

struct rvfi_csr {
  logic [31:0] wdata;
  logic wvalid;
}

interface rvfi_csrs {
    rvfi_csr mstatus;
    rvfi_csr mcause;
    ...
}

I don't think there's any need to record CSR reads. I'm not aware of any with read side effects (seed almost is but you aren't allowed to only read it). Does that sound reasonable?

[SamuelRiedel]

As far as I know, the reason is just that we haven't needed it so far in the traces. But people working on the formal verification can correct me. However, I think it makes sense to record and include them in the traces more explicitly than just through CSR read/write instructions.

Approach 3 is quite an overkill, I agree, but I still like it better than Approach 2, since the addresses are still the default ones and the tool will optimize most of them away. But I also don't want to have tens or hundreds of extra signals in the rvfi as the specification foresees. So your approach with collecting them into an interface sounds reasonable to me. Although, I would use a struct instead of an interface. For example:

typedef struct packed {
  logic [31:0] wdata;
  logic wvalid;
} rvfi_csr_t

struct rvfi_csrs packed{
    rvfi_csr_t mstatus;
    rvfi_csr_t mcause;
    ...
} rvfi_csrs_t

and then we simply have to add one more rvfi_csrs_t signal to the rvfi interface. This also makes extending it to include read accesses very easy.