update to new bitfield syntax

riscv · Feb 7, 2024 · 9d8f002 · 9d8f002
1 parent e31e8f3
commit 9d8f002
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 12 deletions.
diff --git a/model/riscv_insts_zicfiss.sail b/model/riscv_insts_zicfiss.sail
@@ -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
 }
 
@@ -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) {

diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail
@@ -107,7 +107,7 @@ function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {
 /* Zicfiss: ss pte -> rwx=010b */
 val is_shadow_stack_PTE_enable : unit -> bool
 function is_ss_pte(p : PTE_Bits) -> bool =
-  (p.R() == 0b0 & p.W() == 0b1 & p.X() == 0b0 & is_shadow_stack_PTE_enable())
+  (p[R] == 0b0 & p[W] == 0b1 & p[X] == 0b0 & is_shadow_stack_PTE_enable())
 
 function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
   let a = Mk_PTE_Bits(p);
@@ -125,7 +125,7 @@ function to_pte_check(b : bool) -> PTE_Check =
 
 /* Zicfiss: access-fault conditions */
 function is_read_only_pte(p : PTE_Bits) -> bool =
-  (p.R() == 0b1 & p.W() == 0b0 & p.X() == 0b0)
+  (p[R] == 0b1 & p[W] == 0b0 & p[X] == 0b0)
 function is_shadow_stack_pte_access_fault(ac : AccessType(ext_access_type), p : PTE_Bits) -> bool = {
   match (haveZicfiss(), ac) {
     (false, _)                 => false,

diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
@@ -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()
 }
 

diff --git a/model/riscv_zicfiss_control.sail b/model/riscv_zicfiss_control.sail
@@ -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)
@@ -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);
 }