Don't use rd_wdata of instructions that trapped in the reg check #26
Conversation
The reg check used rd_wdata of any valid instruction as the value for register_shadow. However, for instructions that trapped, this value is invalid. This commit ensures that rd_wdata of trapped instructions is never used for register_shadow.
|
Quoting the RVFI spec:
So if for any reason you'd output different (non-zero) values for a trapping instruction then you'd have to gate them accordingly on the core side. But for most cores you'd just hook it into the pipeline in a way so that rvfi_rd_addr=0 and rvfi_rd_wdata=0 whenever there's no writeback, regardless of the reason. (For example, branch instruction also have no writeback.) Otherwise, if the check would test rvfi_trap, you'd tie the instruction decoder and a whole bunch of other stuff into that path, dramatically reducing the to-expected proof performance for what's already one of the most challenging formal checks in the riscv-formal suite. |
Ok, I'll solve it that way. Thanks! |
The reg check used rd_wdata of any valid instruction as the value for
register_shadow. However, for instructions that trapped, this value is
invalid. This commit ensures that rd_wdata of trapped instructions is
never used for register_shadow.