SymbioticEDA / riscv-formal

RISC-V Formal Verification Framework
ISC License
573 stars 94 forks source link

Debug modelling #44

Open silabs-PaulZ opened 3 years ago

silabs-PaulZ commented 3 years ago

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”?