Skip to content

Commit

Permalink
update to new bitfield syntax
Browse files Browse the repository at this point in the history
  • Loading branch information
ved-rivos committed Feb 7, 2024
1 parent e31e8f3 commit cd0c422
Show file tree
Hide file tree
Showing 3 changed files with 10 additions and 10 deletions.
8 changes: 4 additions & 4 deletions model/riscv_insts_zicfiss.sail
Original file line number Diff line number Diff line change
Expand Up @@ -88,9 +88,9 @@ function zicfiss_xSSE(priv : Privilege) -> bool = {
if priv == Machine
then false
else if priv == Supervisor
then menvcfg.SSE() == 0b1
then menvcfg[SSE] == 0b1
else if haveSupMode()
then senvcfg.SSE() == 0b1
then senvcfg[SSE] == 0b1
else false
}

Expand Down Expand Up @@ -312,11 +312,11 @@ mapping clause assembly = SSAMOSWAP(aq, rl, rs2, rs1, size, rd)
if haveZicfiss() & ssamoswap_width_valid(size)
/* ****************************************************************** */
function clause execute (SSAMOSWAP(aq, rl, rs2, rs1, width, rd)) = {
if cur_privilege != Machine & menvcfg.SSE() == 0b0
if cur_privilege != Machine & menvcfg[SSE] == 0b0
then { handle_illegal(); RETIRE_FAIL }
else if not(haveSupMode())
then { handle_illegal(); RETIRE_FAIL }
else if cur_privilege == User & senvcfg.SSE() == 0b0
else if cur_privilege == User & senvcfg[SSE] == 0b0
then { handle_illegal(); RETIRE_FAIL }
else {
match ext_data_get_addr(rs1, zeros(), SSReadWrite(Data, Data), width) {
Expand Down
6 changes: 3 additions & 3 deletions model/riscv_sys_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -874,17 +874,17 @@ function legalize_menvcfg(o : Envcfg, v : bits(64)) -> Envcfg = {

function legalize_senvcfg(o : Envcfg, v : bits(64)) -> Envcfg = {
let v = Mk_Envcfg(v);
let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0);
let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0];
// Zicfiss - SSE: shadow stack enable - is ROZ in senvcfg if menvcfg.SSE is 0
let o = update_SSE(o, if haveZicfiss() & menvcfg.SSE() == 0b1 then v.SSE() else 0b0);
let o = [o with SSE = if haveZicfiss() & menvcfg[SSE] == 0b1 then v[SSE] else 0b0];
// Other extensions are not implemented yet so all other fields are read only zero.
o
}

function get_senvcfg() -> bits(64) = {
let o : Envcfg = senvcfg;
// Zicfiss - SSE: shadow stack enable - is ROZ in senvcfg if menvcfg.SSE is 0
let o = update_SSE(o, if haveZicfiss() & menvcfg.SSE() == 0b1 then o.SSE() else 0b0);
let o = [o with SSE = if haveZicfiss() & menvcfg[SSE] == 0b1 then o[SSE] else 0b0];
o.bits()
}

Expand Down
6 changes: 3 additions & 3 deletions model/riscv_zicfiss_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -88,9 +88,9 @@ function clause ext_is_CSR_defined(0x011, priv) = { // ssp
if priv == Machine
then true
else if priv == Supervisor
then menvcfg.SSE() == 0b1
then menvcfg[SSE] == 0b1
else if haveSupMode()
then senvcfg.SSE() == 0b1
then senvcfg[SSE] == 0b1
else false
}
function clause ext_read_CSR(0x011) = Some(ssp)
Expand All @@ -101,7 +101,7 @@ function clause ext_write_CSR(0x011, value) = {
* Sail model does not support dynamic switching of UXL/SXL so that is
* not considered in the following algorithm yet.
*/
if ( architecture(misa.MXL()) == Some(RV64) ) then
if ( architecture(misa[MXL]) == Some(RV64) ) then
ssp[2 .. 2] = 0b0;
Some(ssp);
}
Expand Down

0 comments on commit cd0c422

Please sign in to comment.