diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 1baa33701..95ed4d6a5 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -501,6 +501,7 @@ function init_sys() -> unit = { mstatus = set_mstatus_SXL(mstatus, misa[MXL]); mstatus = set_mstatus_UXL(mstatus, misa[MXL]); mstatus[SD] = 0b0; + mstatus[MPP] = privLevel_to_bits(lowest_supported_privLevel()); /* set to little-endian mode */ if sizeof(xlen) == 64 then { diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 3537abc16..65d141923 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -168,6 +168,21 @@ function haveZalrsc() -> bool = haveAtomics() /* Zicond extension support */ function haveZicond() -> bool = true +/* + * Illegal values legalized to least privileged mode supported. + * Note: the only valid combinations of supported modes are M, M+U, M+S+U. + */ +function lowest_supported_privLevel() -> Privilege = + if haveUsrMode() then User else Machine + +function have_privLevel(priv : priv_level) -> bool = + match priv { + 0b00 => haveUsrMode(), + 0b01 => haveSupMode(), + 0b10 => false, + 0b11 => true, + } + bitfield Mstatush : bits(32) = { MBE : 5, SBE : 4 @@ -255,6 +270,10 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { */ let m : Mstatus = Mk_Mstatus(zero_extend(v[22 .. 7] @ 0b0 @ v[5 .. 3] @ 0b0 @ v[1 .. 0])); + /* Legalize MPP */ + let m = [m with MPP = if have_privLevel(m[MPP]) then m[MPP] + else privLevel_to_bits(lowest_supported_privLevel())]; + /* We don't have any extension context yet. */ let m = [m with XS = extStatus_to_bits(Off)];