aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRobert Norton <rmn30@cam.ac.uk>2019-11-05 16:14:08 +0000
committerRobert Norton <rmn30@cam.ac.uk>2019-11-05 16:14:08 +0000
commitb07478942f9e3060bf807147f65e0a91852db029 (patch)
tree402a4a07c736895360c553e25b932bf72128f11e
parent75550b059c957c65b7ee69a83ddfe53afbd147ac (diff)
downloadsail-riscv-csr_ext.zip
sail-riscv-csr_ext.tar.gz
sail-riscv-csr_ext.tar.bz2
Add extension point for checking CSR access.csr_ext
-rw-r--r--model/riscv_ext_regs.sail15
-rw-r--r--model/riscv_insts_zicsr.sail2
2 files changed, 17 insertions, 0 deletions
diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail
index 9ff83b3..b03ecd5 100644
--- a/model/riscv_ext_regs.sail
+++ b/model/riscv_ext_regs.sail
@@ -12,3 +12,18 @@ to omnipotent instead of null).
*/
val ext_rvfi_init : unit -> unit effect {wreg}
function ext_rvfi_init () = ()
+
+
+/*!
+THIS(csrno, priv, isWrite) allows an extension to block access to csrno,
+at Privilege level priv. It should return true if the access is allowed.
+*/
+val ext_check_CSR : (bits(12), Privilege, bool) -> bool
+function ext_check_CSR (csrno, p, isWrite) = true
+
+/*!
+THIS is called if ext_check_CSR returns false. It should
+cause an appropriate RISCV exception.
+ */
+val ext_check_CSR_fail : unit->unit
+function ext_check_CSR_fail () = ()
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index dd8a4a0..056f537 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -179,6 +179,8 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = {
};
if ~ (check_CSR(csr, cur_privilege, isWrite))
then { handle_illegal(); RETIRE_FAIL }
+ else if ~ (ext_check_CSR(csr, cur_privilege, isWrite))
+ then { ext_check_CSR_fail(); RETIRE_FAIL }
else {
let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */
if isWrite then {