aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
authorRobert Norton <rmn30@cam.ac.uk>2019-07-09 15:04:08 +0100
committerRobert Norton <rmn30@cam.ac.uk>2019-07-09 15:04:08 +0100
commit6541c02412d6c8744f4c3a137ec302ea40d8117d (patch)
tree8b7e2e64c62e812a2fc455c4a240fa5ad70f07f5 /model
parentcc53e6272416ac3ba680849d0b29b0571e2bbcbd (diff)
downloadsail-riscv-6541c02412d6c8744f4c3a137ec302ea40d8117d.zip
sail-riscv-6541c02412d6c8744f4c3a137ec302ea40d8117d.tar.gz
sail-riscv-6541c02412d6c8744f4c3a137ec302ea40d8117d.tar.bz2
Add ext_rvfi_init to allow model to be initialised differently for rvfi.
Diffstat (limited to 'model')
-rw-r--r--model/riscv_ext_regs.sail8
-rw-r--r--model/riscv_step_rvfi.sail1
2 files changed, 9 insertions, 0 deletions
diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail
index 55600af..9ff83b3 100644
--- a/model/riscv_ext_regs.sail
+++ b/model/riscv_ext_regs.sail
@@ -4,3 +4,11 @@
val ext_init_regs : unit -> unit effect {wreg}
function ext_init_regs () = ()
+
+/*!
+This function is called after above when running rvfi and allows the model
+to be initialised differently (e.g. CHERI cap regs are initialised
+to omnipotent instead of null).
+ */
+val ext_rvfi_init : unit -> unit effect {wreg}
+function ext_rvfi_init () = ()
diff --git a/model/riscv_step_rvfi.sail b/model/riscv_step_rvfi.sail
index f594c00..0efcdce 100644
--- a/model/riscv_step_rvfi.sail
+++ b/model/riscv_step_rvfi.sail
@@ -19,5 +19,6 @@ function ext_init() = {
rvfi_zero_exec_packet();
rvfi_halt_exec_packet();
let _ = rvfi_get_exec_packet();
+ ext_rvfi_init();
()
}