Add a new pc access function to get the architectural PC: on CHERI this is not what is in the PC register because the architectural PC is the offset of PCC and the PC register stores the absolute PC (at present -- may review this decision in future). This allows fix for AUIPC and RVFI reported PC.master-cleanup

4 files changed, 12 insertions, 3 deletions

diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail
index 03b6010..c2a5e74 100644
--- a/model/riscv_fetch_rvfi.sail
+++ b/model/riscv_fetch_rvfi.sail
@@ -5,7 +5,7 @@ function fetch() -> FetchResult =
   else {
     let i = rvfi_instruction.rvfi_insn();
     rvfi_exec->rvfi_order()    = minstret;
-    rvfi_exec->rvfi_pc_rdata() = EXTZ(PC);
+    rvfi_exec->rvfi_pc_rdata() = EXTZ(get_arch_pc());
     rvfi_exec->rvfi_insn()     = EXTZ(i);
 
     /* TODO: should we write these even if they're not really registers? */
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 14a626e..9327948 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -17,7 +17,7 @@ function clause execute UTYPE(imm, rd, op) = {
   let off : xlenbits = EXTS(imm @ 0x000);
   let ret : xlenbits = match op {
     RISCV_LUI   => off,
-    RISCV_AUIPC => PC + off
+    RISCV_AUIPC => get_arch_pc() + off
   };
   X(rd) = ret;
   RETIRE_SUCCESS
diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail
index a51e627..d371953 100644
--- a/model/riscv_pc_access.sail
+++ b/model/riscv_pc_access.sail
@@ -1,6 +1,15 @@
 /* accessors for default architectural addresses, for use from within instructions */
 /* FIXME: see note in cheri_addr_checks.sail */
 
+/*!
+  Retrieves the architectural PC value. This is not necessarily the value
+  found in the PC register as extensions may choose to override this function.
+  The value in the PC register is the absolute virtual address of the instruction
+  to fetch.
+ */
+val get_arch_pc : unit -> xlenbits effect {rreg}
+function get_arch_pc() = PC
+
 val get_next_pc : unit -> xlenbits effect {rreg}
 function get_next_pc() = nextPC
 
diff --git a/model/riscv_step_rvfi.sail b/model/riscv_step_rvfi.sail
index 0efcdce..0ab482a 100644
--- a/model/riscv_step_rvfi.sail
+++ b/model/riscv_step_rvfi.sail
@@ -6,7 +6,7 @@ function ext_pre_step_hook()  -> unit = ()
 
 function ext_post_step_hook() -> unit = {
   /* record the next pc */
-  rvfi_exec->rvfi_pc_wdata() = EXTZ(PC)
+  rvfi_exec->rvfi_pc_wdata() = EXTZ(get_arch_pc())
 }
 
 val ext_init : unit -> unit effect {wreg}