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

mstatus cleanup #683

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

mstatus cleanup #683

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
825a625
insts_base: ignore architecture in SFENCE_VMA
radimkrcmar Jan 11, 2025
9716f11
sys_regs: remove SXL and UXL accessors
radimkrcmar Jan 27, 2025
27f6296
sys_regs: compute mstatus and sstatus SD bit on CSR read
radimkrcmar Jan 11, 2025
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
1 change: 0 additions & 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,6 @@ register f31 : fregtype
function dirty_fd_context() -> unit = {
assert(sys_enable_fdext());
mstatus[FS] = extStatus_to_bits(Dirty);
mstatus = set_mstatus_SD(mstatus, 0b1);
}

function dirty_fd_context_if_present() -> unit = {
Expand Down
6 changes: 3 additions & 3 deletions model/riscv_insts_base.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -714,9 +714,9 @@ function clause execute SFENCE_VMA(rs1, rs2) = {
let asid = if rs2 != zreg then Some(X(rs2)[asidlen - 1 .. 0]) else None();
match cur_privilege {
User => { handle_illegal(); RETIRE_FAIL },
Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus[TVM]) {
(_, 0b1) => { handle_illegal(); RETIRE_FAIL },
(_, 0b0) => { flush_TLB(asid, addr); RETIRE_SUCCESS },
Supervisor => match mstatus[TVM] {
0b1 => { handle_illegal(); RETIRE_FAIL },
0b0 => { flush_TLB(asid, addr); RETIRE_SUCCESS },
},
Machine => { flush_TLB(asid, addr); RETIRE_SUCCESS }
}
Expand Down
81 changes: 24 additions & 57 deletions model/riscv_sys_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -176,8 +176,6 @@ function have_privLevel(priv : priv_level) -> bool =
}

bitfield Mstatus : bits(64) = {
SD_64: 63,

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

Expand All @@ -190,8 +188,6 @@ bitfield Mstatus : bits(64) = {
SXL : 35 .. 34,
UXL : 33 .. 32,

SD_32: 31,

//SDT : 24,
//SPELP: 23,
TSR : 22,
Expand Down Expand Up @@ -220,27 +216,10 @@ function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv :
then privLevel_of_bits(m[MPP])
else priv

function get_mstatus_SXL(m : Mstatus) -> arch_xlen = {
if xlen == 32
then architecture(RV32)
else m[SXL]
}

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

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 with SD_32 = v]
else [m with SD_64 = v]
function status_dirty(s : Mstatus) -> bits(1) = {
bool_to_bits(extStatus_of_bits(s[FS]) == Dirty |
extStatus_of_bits(s[XS]) == Dirty |
extStatus_of_bits(s[VS]) == Dirty)
}

function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = {
Expand All @@ -251,7 +230,9 @@ function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = {
*/
let v = Mk_Mstatus(v);

let o = [o with
[o with
/* SD is handled in CSR accessors */

// MDT = v[MDT],
// MPELP = v[MPELP],
// MPV = v[MPV],
Expand Down Expand Up @@ -285,16 +266,6 @@ function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = {
SPIE = v[SPIE],
MIE = v[MIE],
SIE = v[SIE],
];

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

[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],
]
}

Expand All @@ -314,23 +285,27 @@ 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[xlen - 1 .. 0]
function clause read_CSR(0x300) = status_dirty(mstatus) @ mstatus.bits[xlen - 2 .. 0]
function clause read_CSR(0x310 if xlen == 32) = mstatus.bits[63 .. 32]

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((0x300, value) if xlen == 64) = { mstatus = legalize_mstatus(mstatus, value); status_dirty(mstatus) @ mstatus.bits[62 .. 0] }
function clause write_CSR((0x300, value) if xlen == 32) = { mstatus = legalize_mstatus(mstatus, mstatus.bits[63 .. 32] @ value); status_dirty(mstatus) @ mstatus.bits[30 .. 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 */

function cur_architecture() -> Architecture = {
let a : arch_xlen =
match cur_privilege {
Machine => misa[MXL],
Supervisor => get_mstatus_SXL(mstatus),
User => get_mstatus_UXL(mstatus)
};
architecture(a)
if xlen == 32
then RV32
else {
let a : arch_xlen =
match cur_privilege {
Machine => misa[MXL],
Supervisor => mstatus[SXL],
User => mstatus[UXL],
};
architecture(a)
}
}

function in32BitMode() -> bool = {
Expand Down Expand Up @@ -708,10 +683,9 @@ function clause read_CSR(0xF15) = mconfigptr

/* sstatus reveals a subset of mstatus */
bitfield Sstatus : bits(64) = {
SD_64 : 63,
/* SD is handled in CSR accessors */

UXL : 33 .. 32,
SD_32 : 31,
// SDT : 24,
// SPELP : 23,
MXR : 19,
Expand All @@ -729,9 +703,7 @@ function lower_mstatus(m : Mstatus) -> Sstatus = {
let s = Mk_Sstatus(zeros());

[s with
SD_64 = m[SD_64],
UXL = m[UXL],
SD_32 = m[SD_32],
//SDT = m[SDT],
//SPELP = m[SPELP],
MXR = m[MXR],
Expand All @@ -746,12 +718,7 @@ function lower_mstatus(m : Mstatus) -> Sstatus = {
}

function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = {
let dirty = extStatus_of_bits(s[FS]) == Dirty | extStatus_of_bits(s[XS]) == Dirty |
extStatus_of_bits(s[VS]) == Dirty;

[m with
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],
Expand All @@ -772,8 +739,8 @@ function legalize_sstatus(m : Mstatus, v : xlenbits) -> Mstatus = {

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[xlen - 1 .. 0]
function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits[xlen - 1 .. 0] }
function clause read_CSR(0x100) = status_dirty(mstatus) @ lower_mstatus(mstatus).bits[xlen - 2 .. 0]
function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); status_dirty(mstatus) @ mstatus.bits[xlen - 2 .. 0] }


bitfield Sinterrupts : xlenbits = {
Expand Down
1 change: 0 additions & 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,6 @@ mapping vreg_name = {
function dirty_v_context() -> unit = {
assert(sys_enable_vext());
mstatus[VS] = extStatus_to_bits(Dirty);
mstatus = set_mstatus_SD(mstatus, 0b1);
}

function rV (r : regno) -> vregtype = {
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_vmem.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,7 @@ function satp_to_ppn(satp_val) =
function translationMode(priv : Privilege) -> SATPMode = {
if priv == Machine then Bare
else {
let arch = architecture(get_mstatus_SXL(mstatus));
let arch = if xlen == 32 then RV32 else architecture(mstatus[SXL]);
let mbits : satp_mode = match arch {
RV64 => {
// Can't have an effective architecture of RV64 on RV32.
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I tried to remove the assert(xlen >= 64) in the RV64 match, but Sail didn't compile with this hunk, nor with

let arch = if xlen >= 64 then architecture(mstatus[SXL]) else RV32;

Type error:
riscv_vmem.sail:187.24-28:
187 |        Mk_Satp64(satp)[Mode]
    |                        ^--^
    | Identifier Mode is unbound
    | 
    | Caused by riscv_vmem.sail:187.18-22:
    | 187 |        Mk_Satp64(satp)[Mode]
    |     |                  ^--^ checking function argument has type bitvector(64)
    |     | Failed to prove constraint: 32 == 64

Am I missing some better way to provide this constraint?

Thanks.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does it work if you change it to if xlen < 64 then RV32 else ...?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh wait I can't read... Never mind.

Copy link
Collaborator

@Alasdair Alasdair Feb 8, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The constraints mostly flow lexically, i.e. from the condition in the if down into the branches. The type-checker isn't smart enough to understand that arch == RV64 implies that branch in a previous if was taken, it's a bit too indirect.

You can use an assert that's always true at runtime just to assert a fact to the type system. Sometimes it's better to do that than to try to re-write the logic.

Expand Down
Loading