Remove pc alignment mask

Remove `pc_alignment_mask()` and fix some issues around `xepc` legalisation.

1. `pc_alignment_mask()` didn't zero the lowest bit.
2. `pc_alignment_mask()` was applied ad-hoc after reading `xepc`, but in the spec it is just the read legalisation of `xepc`.
3. `legalize_xpec()` had incorrect condition for allowing `xepc[1]` to be writable.

Signed-off-by: guan jian <[email protected]>
Co-authored-by: Yui5427 <[email protected]>
Co-authored-by: Jessica Clarke <[email protected]>

model/riscv_sys_control.sail

@@ -293,7 +293,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       if   get_config_print_platform()
       then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
 
-      prepare_xret_target(Machine) & pc_alignment_mask()
+      prepare_xret_target(Machine)
     },
     (_, CTL_SRET())  => {
       let prev_priv   = cur_privilege;
@@ -310,7 +310,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       then print_platform("ret-ing from " ^ to_str(prev_priv)
                           ^ " to " ^ to_str(cur_privilege));
 
-      prepare_xret_target(Supervisor) & pc_alignment_mask()
+      prepare_xret_target(Supervisor)
     },
   }
 }

model/riscv_sys_exceptions.sail

@@ -32,21 +32,21 @@ function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = {
 
 /* xRET handling involves three functions:
  *
- * get_xret_target:     used to read the value of the xret target  (no control flow transfer)
- * set_xret_target:     used to write a value of the xret target   (no control flow transfer)
+ * get_xepc:            used to read the value of the xret target  (no control flow transfer)
+ * set_xepc:            used to write a value of the xret target   (no control flow transfer)
  * prepare_xret_target: used to get the value for control transfer to the xret target
  */
 
-val get_xret_target : Privilege -> xlenbits
-function get_xret_target(p) =
+val get_xepc : Privilege -> xlenbits
+function get_xepc(p) =
   match p {
-    Machine    => mepc,
-    Supervisor => sepc,
+    Machine    => align_pc(mepc),
+    Supervisor => align_pc(sepc),
     User       => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
   }
 
-val set_xret_target : (Privilege, xlenbits) -> xlenbits
-function set_xret_target(p, value) = {
+val set_xepc : (Privilege, xlenbits) -> xlenbits
+function set_xepc(p, value) = {
   let target = legalize_xepc(value);
   match p {
     Machine    => mepc = target,
@@ -58,7 +58,7 @@ function set_xret_target(p, value) = {
 
 val prepare_xret_target : (Privilege) -> xlenbits
 function prepare_xret_target(p) =
-  get_xret_target(p)
+  get_xepc(p)
 
 /* other trap-related CSRs */
 
@@ -89,11 +89,11 @@ function clause is_CSR_defined(0x305) = true // mtvec
 function clause is_CSR_defined(0x341) = true // mepc
 
 function clause read_CSR(0x105) = get_stvec()
-function clause read_CSR(0x141) = get_xret_target(Supervisor) & pc_alignment_mask()
+function clause read_CSR(0x141) = get_xepc(Supervisor)
 function clause read_CSR(0x305) = get_mtvec()
-function clause read_CSR(0x341) = get_xret_target(Machine) & pc_alignment_mask()
+function clause read_CSR(0x341) = get_xepc(Machine)
 
 function clause write_CSR(0x105, value) = { set_stvec(value) }
-function clause write_CSR(0x141, value) = { set_xret_target(Supervisor, value) }
+function clause write_CSR(0x141, value) = { set_xepc(Supervisor, value) }
 function clause write_CSR(0x305, value) = { set_mtvec(value) }
-function clause write_CSR(0x341, value) = { set_xret_target(Machine, value) }
+function clause write_CSR(0x341, value) = { set_xepc(Machine, value) }

model/riscv_sys_regs.sail

@@ -445,16 +445,20 @@ register mepc : xlenbits
 /* The xepc legalization zeroes xepc[1:0] when misa.C is hardwired to 0.
  * When misa.C is writable, it zeroes only xepc[0].
  */
-function legalize_xepc(v : xlenbits) -> xlenbits =
-  /* allow writing xepc[1] only if misa.C is enabled or could be enabled
-     XXX specification says this legalization should be done on read */
-  if   (sys_enable_writable_misa() & sys_enable_rvc()) | misa[C] == 0b1
+function legalize_xepc(v : xlenbits) -> xlenbits = {
+  // allow writing xepc[1] only if misa.C is enabled or could be enabled.
+  if   sys_enable_rvc()
   then [v with 0 = bitzero]
-  else v & sign_extend(0b100)
+  else [v with 1..0 = zeros()]
+}
 
-/* masking for reads to xepc */
-function pc_alignment_mask() -> xlenbits =
-  ~(zero_extend(if misa[C] == 0b1 then 0b00 else 0b10))
+// Align value to min supported PC alignment. This is used to
+// legalize xepc reads.
+function align_pc(addr : xlenbits) -> xlenbits = {
+  if misa[C] == 0b1
+  then [addr with 0 = bitzero]
+  else [addr with 1..0 = zeros()]
+}
 
 /* auxiliary exception registers */