aboutsummaryrefslogtreecommitdiff
path: root/model/riscv_sys_regs.sail
diff options
context:
space:
mode:
Diffstat (limited to 'model/riscv_sys_regs.sail')
-rw-r--r--model/riscv_sys_regs.sail4
1 files changed, 4 insertions, 0 deletions
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index f3cd7e3..6c66492 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -84,6 +84,8 @@ val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform.
val sys_enable_rvc = {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool
/* whether misa.{f,d} were enabled at boot */
val sys_enable_fdext = {c: "sys_enable_fdext", ocaml: "Platform.enable_fdext", _: "sys_enable_fdext"} : unit -> bool
+/* whether Svinval was enabled at boot */
+val sys_enable_svinval = {c: "sys_enable_svinval", ocaml: "Platform.enable_svinval", _: "sys_enable_svinval"} : unit -> bool
/* whether Zcb was enabled at boot */
val sys_enable_zcb = {c: "sys_enable_zcb", ocaml: "Platform.enable_zcb", _: "sys_enable_zcb"} : unit -> bool
/* whether zfinx was enabled at boot */
@@ -311,6 +313,8 @@ function haveZfh() -> bool = (misa[F] == 0b1) & (mstatus[FS] != 0b00)
/* V extension has to enable both via misa.V as well as mstatus.VS */
function haveVExt() -> bool = (misa[V] == 0b1) & (mstatus[VS] != 0b00)
+function haveSvinval() -> bool = sys_enable_svinval()
+
/* Zcb has simple code-size saving instructions. (The Zcb extension depends on the Zca extension.) */
function haveZcb() -> bool = sys_enable_zcb()