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 1 commit
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
30 changes: 11 additions & 19 deletions model/riscv_sys_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -220,18 +220,6 @@ 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]
Expand Down Expand Up @@ -324,13 +312,17 @@ function clause write_CSR((0x310, value) if xlen == 32) = { mstatus = legalize_m
/* 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
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