Debug modelling

[silabs-PaulZ]

In some cores, such as CV32E40P, the processor will retire an instruction before knowing that it was the last instruction prior to a halt being executed. A simple example is when the last instruction is a branch, the next instruction has not been retrieved and an external halt request is executed.

Can you change the rvfi_halt definition to be set on the first instruction that is part of the debug handler (similar to rvfi_intr).

Also, can you expand on the statement “This signal enables verification of liveness properties”?