"rvfi_dbg" wrong cause

[silabs-robin]

Component:RTL: For issues in the RTL (e.g. for files in the rtl directory)
Component:Other: For any other issues

Description

On the first instr in dmode, rvfi_dbg "contains the debug cause".
Also, dcsr.cause "Explains why Debug Mode was entered"
AFAICT, they should be the same on the first instr in dmode.
Problem: They are not. (See screenshot below.)

The trace above shows the core entering dmode because of debug_req_i.
This cause is correctly reflected in dcsr.cause (3 is "haltreq").
But rvfi incorrectly shows the cause to be "1", because it has some special handling of "ebreak".

Steps to Reproduce

1. Use my fork and branch https://github.com/silabs-robin/core-v-verif/tree/rvfi_assert, hash f9b040d4.
2. Run formal and check a_dbg_cause.

[Silabs-ArjanB]

This is both an RVFI issue and an assertion issue.

The RVFI issue should be solved by #258.

The assertion issue relates to a misunderstanding of the rvfi_dbg signal. It does not always have to be equal the debug cause in dcsr as shown in Table 27 Table of scenarios for first instruction of exception/interrupt/debug handler. Further clarification has been added in the user manual via openhwgroup/cv32e40x#621.

Resolving this issue (as it tracks the design repos and not core-v-verif that still requires an assertion update).

[silabs-robin]

an ebreak in debug mode will be reported via rvfi_dbg

Why?
"For the first instruction after entering debug, the rvfi_dbg signal contains the debug cause".
An ebreak in debug mode goes from D-mode to D-mode, so I don't see why that is "entering debug".

[Silabs-ArjanB]

@silabs-robin This scenario is considered 'entering debug' because a branch is performed to dm_halt_addr_i.

[silabs-robin]

The RVFI issue appears to have been fixed. CEXes now point to the need to update the assertion itself.