Closed dansmathers closed 2 years ago
https://github.com/riscv/sail-riscv/blob/master/model/riscv_sys_exceptions.sail / xRET handling involves three functions:
https://github.com/riscv/sail-riscv/blob/master/model/riscv_sys_control.sail / handle exceptional ctl flow by updating nextPC and operating privilege / function trap_handler( function exception_handler( set_next_pc(exception_handler(cur_privilege, CTL_TRAP(t), PC))
https://github.com/riscv/sail-riscv/blob/master/model/riscv_pc_access.sail function set_next_pc(pc) = {
adding MarkHillHuawei comment from merge of #276 here: My only comment is that for systems which only support horizontal traps (e.g. U/M with no N-extension and M only systems) then perhaps minhv can be hardwired to zero and the associated mechanism dropped. There are precedents for similar caveats in the Privileged ISA spec already.
When taking a horizontal trap on a table fetch, the trap handler should not be trying to use MRET with the original inhv value, so we should simplify the logic to not include the (cur_priv != prev_priv) clause. In other words, we don't need to special-case horizontal traps for xRET. Software trap handlers should figure out it's a horizontal trap on table fetch and report the error for debugging.
Currently, the pseudo-code appears to show the pc mem_read with prev_inhv set in the priv mode of the exception handler, but the pc mem read needs to be in the priv mode after the xRET instruction.
is better for xRET to pass xepc and xinhv to function and that function in the new priv mode decides whether to treat epc as table read (address) or as instruction.
clean up pseudo-code. think about current sail code.