Document RVFI-DII V2 protocol

[Timmmm]

As far as I can tell there are two versions of the RVFI-DII protocol. Version negotiation is done by sending an EndOfTrace command with the instruction set to VERS. Version 1 will respond by halting; later versions send some kind of version packet. There's also a new "set version" command, and presumably there are some differences to the rest of the protocol.

Unfortunately none of this is documented in the RVFI-DII.md file, and Haskell isn't the easiest language to read. Any chance you could update that document?

[Timmmm]

Also I couldn't really understand how rvfi_time is supposed to work but as far as I can see nothing actually uses it?

[nwf-msr]

I find myself in the same boat of wanting to understand v2 (with the intent of adding it to another model).

FWIW, the implementation in https://github.com/riscv/sail-riscv/blob/master/model/rvfi_dii.sail (and associated bits under #ifdef RVFI_DII guards in https://github.com/riscv/sail-riscv/blob/master/c_emulator/riscv_sim.c) is another source of understanding, though also perhaps not the easiest to read, as it requires reading C and sail and tolerating the unusual things sail does when lowered to C.

[arichardson]

V2 is a somewhat hacky extension of the initial format to report more information. In hindsight it might have been better to use a well-known binary format such as cbor and just define the schema.

[arichardson]

Cheri qemu also has an implementation of this format

[Timmmm]

Yeah Protobuf or FlatBuffers are probably the way to go IMO. CBOR is still quite an inefficient format because it repeats keys.

There are quite a lot of other deficiencies in the format that would be worth fixing at the same time (if anyone is thinking of designing RVFI V3!):

• Max 8 byte memory accesses. CHERI can be 16, and cbo.zero 64 (or more!)
• Only one read and one write
• Doesn't record virtual addresses (not technically necessary but eases debugging)
• Doesn't record CSR writes I think?
• Only 2 input registers and 1 output register. Some instructions do way more than this. Traps also do hardware writes of lots of registers.
• Doesn't record the privilege/debug mode (again, helpful for debugging)
• Doesn't record the trap/interrupt cause.

Also I've found that for verification there should really be a reset event that contains the contents of all initialised memory, otherwise it is hard to compare different DUTs in the presence of resets due to caches.

[arichardson]

A few items on your wishlist already exist: execution mode (but not debug mode) is logged in V2 and also memory accesses can be up to 32 bytes. Some of the other missing logging was intended to be added but I never got around to it.

A more flexible binary format would make that a lot easier to add but we'd need to ensure that there is a reasonably easy way to expose it both from Sail (well I guess a C library is good enough and could also be used by QEMU) and haskell.

Regarding the specific format I'm not sure how important it is that it's space-efficient, the main overhead will most likely be in the simulators themselves. That said choosing something efficient that has bindings for many languages would be ideal.

[Timmmm]

From that point of view Protobuf is probably best then. It is supported basically everywhere including Haskell and OCaml.

Space efficiency is important if you are storing logs for post processing. Booting Linux is like 20 million instructions.

But aside from that, Protobuf is a bit nicer to program because it generates static types for you.

Neither are perfect formats IMO - Protobuf makes too many things Optional which leads to a ton of .unwrap()s in properly typed languages like Rust (and I assume Haskell and OCaml). I think both of them lack sum types. But they're pretty good overall.