JAL handling procedure

[RojasMilo]

I have been working with the riscv-formal for a couple of months now.
Arithmetic, load and store checks are passing but I want to ask you what would be the procedure for a JAL?, at the end of the pipe I have 2 PC values without importance when JAL comes.

I see the correct PC in the pipe.

But how could I tell that the data is not ready yet? if I put the jump trigger signal in the valid the output is warmup!

I am working with a SIIO 5-stage pipeline core.

Thank you for a great tool.

[RojasMilo]

Hi, I still have this question, but now JAL and JALR are passing.

I add a mux in the RVFI and when JAL comes, it performs a forwarding data from EX to WB. Delivering the correct destination address.

These strategi allow me to find a bug in JALR calculation, do you think is a valid approach?

Thanks