Trap Handling: PC set to Other Adress than Specified by MTVEC

Created by: alda-tuk

Hi,

we are formally verifying the processors behavior upon privilege increase. Therefore we are checking if a user-level process sets the PC to the correct address when a trap to machine or supervisor mode is executed.

According to the RISCV-ISA (Document Version 20211203) section 3.1.7 (page 29) and 4.1.2 (page 66) the mtvec and stvec registers specify how the corresponding address is calculated. Both registers consist of a BASE-field and a MODE-field. The MODE for mtvec and stvec can be set independently from each other to either direct or vectored. That means upon a trap to machine mode

• PC is set to BASE of mtvec if the MODE of mtvec is direct
• PC is set to BASE + 4 * cause if MODE is vectored and it is an interrupt.

Similarly traps into supervisor mode are handled according to the settings of BASE and MODE in stvec.

When formally verifying this behavior on CVA6 we get a counterexample showing a behavior that does not comply with the ISA: A user-level process executes an interrupt and sets the PC to BASE + 4 * cause. However, the MODE of mtvec is set to direct.

The reason for that can be found in lines 981-998 or more precisely in line 996 of the csr_regfile.sv: https://github.com/openhwgroup/cva6/blob/e748564dd880d68a9b0bde7e1a92c48c75823391/core/csr_regfile.sv#L981-L998 Whenever one MODE, the MODE of mtvec or the MODE of stvec, is set to vectored and it is an interrupt, the address calculation for the PC is done in vectored mode. Is this a bug or am I missing something here?

Thanks and best regards, Anna