Skip to content

Commit

Permalink
Merge [with] updates
Browse files Browse the repository at this point in the history
  • Loading branch information
@Yui5427
Yui5427 committed Oct 10, 2024
1 parent 60f8ae6 commit e2c47d2
Show file tree
Hide file tree
Showing 2 changed files with 66 additions and 58 deletions.
33 changes: 19 additions & 14 deletions model/riscv_next_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,15 +17,18 @@ bitfield Ustatus : xlenbits = {
/* This is a view, so there is no register defined. */
function lower_sstatus(s : Sstatus) -> Ustatus = {
let u = Mk_Ustatus(zero_extend(0b0));
let u = [u with UPIE = s[UPIE]];
let u = [u with UIE = s[UIE]];
u

[u with
UPIE = s[UPIE],
UIE = s[UIE],
]
}

function lift_ustatus(s : Sstatus, u : Ustatus) -> Sstatus = {
let s = [s with UPIE = u[UPIE]];
let s = [s with UIE = u[UIE]];
s
[s with
UPIE = u[UPIE],
UIE = u[UIE],
]
}

function legalize_ustatus(m : Mstatus, v : xlenbits) -> Mstatus = {
Expand All @@ -45,19 +48,21 @@ bitfield Uinterrupts : xlenbits = {
/* Provides the uip read view of sip (s) as delegated by sideleg (d). */
function lower_sip(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = {
let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0));
let u = [u with UEI = s[UEI] & d[UEI]];
let u = [u with UTI = s[UTI] & d[UTI]];
let u = [u with USI = s[USI] & d[USI]];
u
[u with
UEI = s[UEI] & d[UEI],
UTI = s[UTI] & d[UTI],
USI = s[USI] & d[USI],
]
}

/* Provides the uie read view of sie as delegated by sideleg. */
function lower_sie(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = {
let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0));
let u = [u with UEI = s[UEI] & d[UEI]];
let u = [u with UTI = s[UTI] & d[UTI]];
let u = [u with USI = s[USI] & d[USI]];
u
[u with
UEI = s[UEI] & d[UEI],
UTI = s[UTI] & d[UTI],
USI = s[USI] & d[USI],
]
}

/* Returns the new value of sip from the previous sip (o) and the written uip (u) as delegated by sideleg (d). */
Expand Down
91 changes: 47 additions & 44 deletions model/riscv_sys_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -279,8 +279,7 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {

/* Hardwired to zero in the absence of 'U' or 'N'. */
let m = if not(extensionEnabled(Ext_N)) then {
let m = [m with UPIE = 0b0];
let m = [m with UIE = 0b0];
let m = [m with UPIE = 0b0, UIE = 0b0];
m
} else m;

Expand Down Expand Up @@ -577,37 +576,38 @@ function lower_mstatus(m : Mstatus) -> Sstatus = {
let s = Mk_Sstatus(zero_extend(0b0));
let s = [s with SD = m[SD]];
let s = set_sstatus_UXL(s, get_mstatus_UXL(m));
let s = [s with MXR = m[MXR]];
let s = [s with SUM = m[SUM]];
let s = [s with XS = m[XS]];
let s = [s with FS = m[FS]];
let s = [s with VS = m[VS]];
let s = [s with SPP = m[SPP]];
let s = [s with SPIE = m[SPIE]];
let s = [s with UPIE = m[UPIE]];
let s = [s with SIE = m[SIE]];
let s = [s with UIE = m[UIE]];
s

[s with
MXR = m[MXR],
SUM = m[SUM],
XS = m[XS],
FS = m[FS],
VS = m[VS],
SPP = m[SPP],
SPIE = m[SPIE],
UPIE = m[UPIE],
SIE = m[SIE],
UIE = m[UIE],
]
}

function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = {
let m = [m with MXR = s[MXR]];
let m = [m with SUM = s[SUM]];

let m = [m with XS = s[XS]];
// See comment for mstatus.FS.
let m = [m with FS = s[FS]];
let m = [m with VS = s[VS]];
let dirty = extStatus_of_bits(m[FS]) == Dirty | extStatus_of_bits(m[XS]) == Dirty |
extStatus_of_bits(m[VS]) == Dirty;
let m = [m with SD = bool_to_bits(dirty)];

let m = [m with SPP = s[SPP]];
let m = [m with SPIE = s[SPIE]];
let m = [m with UPIE = s[UPIE]];
let m = [m with SIE = s[SIE]];
let m = [m with UIE = s[UIE]];
m
let dirty = extStatus_of_bits(s[FS]) == Dirty | extStatus_of_bits(s[XS]) == Dirty |
extStatus_of_bits(s[VS]) == Dirty;

[m with
SD = bool_to_bits(dirty),
MXR = s[MXR],
SUM = s[SUM],
XS = s[XS],
FS = s[FS],
VS = s[VS],
SPP = s[SPP],
SPIE = s[SPIE],
UPIE = s[UPIE],
SIE = s[SIE],
UIE = s[UIE]
]
}

function legalize_sstatus(m : Mstatus, v : xlenbits) -> Mstatus = {
Expand Down Expand Up @@ -645,26 +645,29 @@ bitfield Sinterrupts : xlenbits = {
/* Provides the sip read view of mip (m) as delegated by mideleg (d). */
function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
let s : Sinterrupts = Mk_Sinterrupts(zero_extend(0b0));
let s = [s with SEI = m[SEI] & d[SEI]];
let s = [s with STI = m[STI] & d[STI]];
let s = [s with SSI = m[SSI] & d[SSI]];

let s = [s with UEI = m[UEI] & d[UEI]];
let s = [s with UTI = m[UTI] & d[UTI]];
let s = [s with USI = m[USI] & d[USI]];
s
[s with
SEI = m[SEI] & d[SEI],
STI = m[STI] & d[STI],
SSI = m[SSI] & d[SSI],
UEI = m[UEI] & d[UEI],
UTI = m[UTI] & d[UTI],
USI = m[USI] & d[USI]
]
}

/* Provides the sie read view of mie (m) as delegated by mideleg (d). */
function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
let s : Sinterrupts = Mk_Sinterrupts(zero_extend(0b0));
let s = [s with SEI = m[SEI] & d[SEI]];
let s = [s with STI = m[STI] & d[STI]];
let s = [s with SSI = m[SSI] & d[SSI]];
let s = [s with UEI = m[UEI] & d[UEI]];
let s = [s with UTI = m[UTI] & d[UTI]];
let s = [s with USI = m[USI] & d[USI]];
s

[s with
SEI = m[SEI] & d[SEI],
STI = m[STI] & d[STI],
SSI = m[SSI] & d[SSI],
UEI = m[UEI] & d[UEI],
UTI = m[UTI] & d[UTI],
USI = m[USI] & d[USI]
]
}

/* Returns the new value of mip from the previous mip (o) and the written sip (s) as delegated by mideleg (d). */
Expand Down

0 comments on commit e2c47d2

Please sign in to comment.