Merge branch 'master-cleanup'

5 files changed, 20 insertions, 4 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 636170b..a435786 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_platform.sail b/model/riscv_platform.sail
index 9184f02..52511a9 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -337,12 +337,19 @@ function htif_tick() = {
 }
 
 /* Top-level MMIO dispatch */
-
+$ifndef RVFI_DII
 function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool =
   within_clint(addr, width) | (within_htif_readable(addr, width) & 1 <= 'n)
+$else
+function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false
+$endif
 
+$ifndef RVFI_DII
 function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool =
   within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8)
+$else
+function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false
+$endif
 
 function mmio_read forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) =
   if   within_clint(addr, width)
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}