Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor mstatus handler function #652

Merged
merged 1 commit into from
Jan 27, 2025
Merged

refactor mstatus handler function #652

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion model/riscv_fdext_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ register f31 : fregtype
function dirty_fd_context() -> unit = {
assert(sys_enable_fdext());
mstatus[FS] = extStatus_to_bits(Dirty);
mstatus[SD] = 0b1
mstatus = set_mstatus_SD(mstatus, 0b1);
}

function dirty_fd_context_if_present() -> unit = {
Expand Down
21 changes: 11 additions & 10 deletions model/riscv_sys_control.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -370,16 +370,17 @@ function init_sys() -> unit = {
then bool_to_bits(sys_enable_fdext()) /* double-precision */
else 0b0;

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 xlen == 64 then {
mstatus = Mk_Mstatus([mstatus.bits with 37 .. 36 = 0b00])
};
mstatush.bits = zeros();
mstatus = [mstatus with
SD_64 = 0b0,
SD_32 = 0b0,
/* SXL and UXL is only valid for 64-bit systems and in RV32 WPRI */
SXL = misa[MXL],
UXL = misa[MXL],
MPP = privLevel_to_bits(lowest_supported_privLevel()),
/* set to little-endian mode */
MBE = 0b0,
SBE = 0b0,
];

mip.bits = zeros();
mie.bits = zeros();
Expand Down
193 changes: 99 additions & 94 deletions model/riscv_sys_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -167,26 +167,25 @@ function have_privLevel(priv : priv_level) -> bool =
0b11 => true,
}

bitfield Mstatush : bits(32) = {
MBE : 5,
SBE : 4
}
register mstatush : Mstatush
bitfield Mstatus : bits(64) = {
SD_64: 63,

//MDT : 42,
//MPELP: 41,

//MPV : 39,
//GVA : 38,

bitfield Mstatus : xlenbits = {
SD : xlen - 1,
MBE : 37,
SBE : 36,

// The MBE and SBE fields are in mstatus in RV64 and absent in RV32.
// On RV32, they are in mstatush, which doesn't exist in RV64. For now,
// they are handled in an ad-hoc way.
// MBE : 37
// SBE : 36
SXL : 35 .. 34,
UXL : 33 .. 32,

// The SXL and UXL fields don't exist on RV32, so they are modelled
// via explicit getters and setters; see below.
// SXL : 35 .. 34,
// UXL : 33 .. 32,
SD_32: 31,

//SDT : 24,
//SPELP: 23,
TSR : 22,
TW : 21,
TVM : 20,
Expand Down Expand Up @@ -217,84 +216,92 @@ function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv :
function get_mstatus_SXL(m : Mstatus) -> arch_xlen = {
if xlen == 32
then arch_to_bits(RV32)
else m.bits[35 .. 34]
}

function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
if xlen == 32
then m
else {
let m = vector_update_subrange(m.bits, 35, 34, a);
Mk_Mstatus(m)
}
else m[SXL]
}

function get_mstatus_UXL(m : Mstatus) -> arch_xlen = {
if xlen == 32
then arch_to_bits(RV32)
else m.bits[33 .. 32]
else m[UXL]
}

function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
function get_mstatus_SD(m : Mstatus) -> bits(1) = {
if xlen == 32 then m[SD_32]
else m[SD_64]
}

function set_mstatus_SD(m : Mstatus, v : bits(1)) -> Mstatus = {
if xlen == 32
then m
else {
let m = vector_update_subrange(m.bits, 33, 32, a);
Mk_Mstatus(m)
}
then [m with SD_32 = v]
else [m with SD_64 = v]
}

function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = {
/*
* Populate all defined fields using the bits of v, stripping anything
* that does not have a matching bitfield entry. All bits above 32 are handled
* explicitly later.
* that does not have a matching bitfield entry. The SD bits are handled
* explicitly later depending on xlen.
*/
// TODO: This method is error prone. We should instead explicitly copy the
// fields that are implemented. See legalize_mie() for an example.
let m : Mstatus = Mk_Mstatus(zero_extend(v[22 .. 7] @ 0b0 @ v[5 .. 5] @ 0b0 @ v[3 .. 3] @ 0b0 @ v[1 .. 1] @ 0b0));

let v = Mk_Mstatus(v);

let o = [o with
// MDT = v[MDT],
// MPELP = v[MPELP],
// MPV = v[MPV],
// GVA = v[GVA],
/* We don't currently support changing MBE and SBE. */
// MBE = v[MBE],
// SBE = v[SBE],
/* We don't support dynamic changes to SXL and UXL. */
// SXL = if xlen == 64 then v[SXL] else o[SXL],
// UXL = if xlen == 64 then v[UXL] else o[UXL],
// SDT = v[SDT],
// SPELP = v[SPELP],
TSR = v[TSR],
TW = v[TW],
TVM = v[TVM],
MXR = v[MXR],
SUM = v[SUM],
MPRV = if extensionEnabled(Ext_U) then v[MPRV] else 0b0,
/* We don't have any extension context yet. */
XS = extStatus_to_bits(Off),
/* FS is WARL, and making FS writable can support the M-mode emulation of an FPU
* to support code running in S/U-modes. Spike does this, and for now, we match it,
* but only if Zfinx isn't enabled.
* FIXME: This should be made a platform parameter.
*/
let m = [m with
/* Legalize MPP */
MPP = if have_privLevel(m[MPP]) then m[MPP] else privLevel_to_bits(lowest_supported_privLevel()),
/* We don't have any extension context yet. */
XS = extStatus_to_bits(Off),
FS = if sys_enable_zfinx() then extStatus_to_bits(Off) else m[FS],
MPRV = if extensionEnabled(Ext_U) then m[MPRV] else 0b0,
FS = if sys_enable_zfinx() then extStatus_to_bits(Off) else v[FS],
MPP = if have_privLevel(v[MPP]) then v[MPP] else privLevel_to_bits(lowest_supported_privLevel()),
VS = v[VS],
SPP = v[SPP],
MPIE = v[MPIE],
SPIE = v[SPIE],
MIE = v[MIE],
SIE = v[SIE],
];

// Set dirty bit to OR of other status bits.
let m = [m with
SD = bool_to_bits(extStatus_of_bits(m[FS]) == Dirty |
extStatus_of_bits(m[XS]) == Dirty |
extStatus_of_bits(m[VS]) == Dirty),
];

/* We don't support dynamic changes to SXL and UXL. */
let m = set_mstatus_SXL(m, get_mstatus_SXL(o));
let m = set_mstatus_UXL(m, get_mstatus_UXL(o));
let dirty = extStatus_of_bits(o[FS]) == Dirty |
extStatus_of_bits(o[XS]) == Dirty |
extStatus_of_bits(o[VS]) == Dirty;

/* We don't currently support changing MBE and SBE. */
if xlen == 64 then {
Mk_Mstatus([m.bits with 37 .. 36 = 0b00])
} else m
[o with
SD_64 = if xlen == 64 then bool_to_bits(dirty) else o[SD_64],
SD_32 = if xlen == 32 then bool_to_bits(dirty) else o[SD_32],
]
}

mapping clause csr_name_map = 0x300 <-> "mstatus"

function clause is_CSR_defined(0x300) = true // mstatus
function clause is_CSR_defined(0x310) = xlen == 32 // mstatush

function clause read_CSR(0x300) = mstatus.bits
function clause read_CSR(0x310 if xlen == 32) = mstatush.bits
function clause read_CSR(0x300) = mstatus.bits[xlen - 1 .. 0]
function clause read_CSR(0x310 if xlen == 32) = mstatus.bits[63 .. 32]

function clause write_CSR(0x300, value) = { mstatus = legalize_mstatus(mstatus, value); mstatus.bits }
function clause write_CSR((0x310, value) if xlen == 32) = { mstatush.bits } // ignore writes for now
function clause write_CSR((0x300, value) if xlen == 64) = { mstatus = legalize_mstatus(mstatus, value); mstatus.bits }
function clause write_CSR((0x300, value) if xlen == 32) = { mstatus = legalize_mstatus(mstatus, mstatus.bits[63 .. 32] @ value); mstatus.bits[31 .. 0] }
function clause write_CSR((0x310, value) if xlen == 32) = { mstatus = legalize_mstatus(mstatus, value @ mstatus.bits[31 .. 0]); mstatus.bits[63 .. 32] }

/* architecture and extension checks */

Expand Down Expand Up @@ -673,39 +680,33 @@ function clause read_CSR(0xF15) = mconfigptr
/* S-mode registers */

/* sstatus reveals a subset of mstatus */
bitfield Sstatus : xlenbits = {
SD : xlen - 1,
// The UXL field does not exist on RV32, so we define an explicit
// getter and setter below.
// UXL : 30 .. 29,
MXR : 19,
SUM : 18,
XS : 16 .. 15,
FS : 14 .. 13,
VS : 10 .. 9,
SPP : 8,
SPIE : 5,
SIE : 1,
bitfield Sstatus : bits(64) = {
SD_64 : 63,

UXL : 33 .. 32,
SD_32 : 31,
// SDT : 24,
// SPELP : 23,
MXR : 19,
SUM : 18,
XS : 16 .. 15,
FS : 14 .. 13,
VS : 10 .. 9,
SPP : 8,
SPIE : 5,
SIE : 1,
}
/* sstatus is a view of mstatus, so there is no register defined. */

function get_sstatus_UXL(s : Sstatus) -> arch_xlen = {
let m = Mk_Mstatus(s.bits);
get_mstatus_UXL(m)
}

function set_sstatus_UXL(s : Sstatus, a : arch_xlen) -> Sstatus = {
let m = Mk_Mstatus(s.bits);
let m = set_mstatus_UXL(m, a);
Mk_Sstatus(m.bits)
}

function lower_mstatus(m : Mstatus) -> Sstatus = {
let s = Mk_Sstatus(zeros());
let s = set_sstatus_UXL(s, get_mstatus_UXL(m));

[s with
SD = m[SD],
SD_64 = m[SD_64],
UXL = m[UXL],
SD_32 = m[SD_32],
//SDT = m[SDT],
//SPELP = m[SPELP],
MXR = m[MXR],
SUM = m[SUM],
XS = m[XS],
Expand All @@ -722,7 +723,11 @@ function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = {
extStatus_of_bits(s[VS]) == Dirty;

[m with
SD = bool_to_bits(dirty),
SD_64 = if xlen == 64 then bool_to_bits(dirty) else m[SD_64],
SD_32 = if xlen == 32 then bool_to_bits(dirty) else m[SD_32],
UXL = s[UXL],
//SDT = s[SDT],
//SPELP = s[SPELP],
MXR = s[MXR],
SUM = s[SUM],
XS = s[XS],
Expand All @@ -735,13 +740,13 @@ function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = {
}

function legalize_sstatus(m : Mstatus, v : xlenbits) -> Mstatus = {
legalize_mstatus(m, lift_sstatus(m, Mk_Sstatus(v)).bits)
legalize_mstatus(m, lift_sstatus(m, Mk_Sstatus(zero_extend(v))).bits)
}

mapping clause csr_name_map = 0x100 <-> "sstatus"
function clause is_CSR_defined(0x100) = extensionEnabled(Ext_S) // sstatus
function clause read_CSR(0x100) = lower_mstatus(mstatus).bits
function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits }
function clause read_CSR(0x100) = lower_mstatus(mstatus).bits[xlen - 1 .. 0]
function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits[xlen - 1 .. 0] }


bitfield Sinterrupts : xlenbits = {
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_vext_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ mapping vreg_name = {
function dirty_v_context() -> unit = {
assert(sys_enable_vext());
mstatus[VS] = extStatus_to_bits(Dirty);
mstatus[SD] = 0b1
mstatus = set_mstatus_SD(mstatus, 0b1);
}

function rV (r : regno) -> vregtype = {
Expand Down
Loading