Use formal tests by adding a RVFI interface

[tilk]

There is a very nice set of formal tests for the RISC-V architecture (riscv-formal). To use it, the processor should have a RVFI interface, which presents the currently retired instructions to the formal verification framework.