diff options
author | Robert Norton <rmn30@cam.ac.uk> | 2019-09-16 17:50:25 +0100 |
---|---|---|
committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-09-18 09:42:12 -0700 |
commit | 8c418a0255f51bf2f9283de6117f8c34630b018b (patch) | |
tree | 7039b5e36917f9039451c669e21afa7e78d79906 | |
parent | c54a10dc0d45f8946d3d4a127c358bc8e9f2e914 (diff) | |
download | sail-riscv-8c418a0255f51bf2f9283de6117f8c34630b018b.zip sail-riscv-8c418a0255f51bf2f9283de6117f8c34630b018b.tar.gz sail-riscv-8c418a0255f51bf2f9283de6117f8c34630b018b.tar.bz2 |
Add a hook for extensions to supress writes to misa.C if necessary.
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | model/riscv_misa_ext.sail | 2 | ||||
-rw-r--r-- | model/riscv_sys_regs.sail | 9 |
3 files changed, 10 insertions, 3 deletions
@@ -16,7 +16,7 @@ else endif # Instruction sources, depending on target -SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail +SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail riscv_misa_ext.sail SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_cext.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_next.sail SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail diff --git a/model/riscv_misa_ext.sail b/model/riscv_misa_ext.sail new file mode 100644 index 0000000..77b9982 --- /dev/null +++ b/model/riscv_misa_ext.sail @@ -0,0 +1,2 @@ +function ext_veto_disable_C () = false + diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 143fd35..722c1d5 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -75,13 +75,18 @@ val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform. /* whether misa.c was enabled at boot */ val sys_enable_rvc = {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool +/* This function allows an extension to veto a write to Misa + if it would violate an alignment restriction on + unsetting C. If it returns true the write will have no effect. */ +val ext_veto_disable_C : unit -> bool effect {rreg} + /* We currently only support dynamic changes for the C extension. */ function legalize_misa(m : Misa, v : xlenbits) -> Misa = { if sys_enable_writable_misa () then { /* Allow modifications to C only for now. */ let v = Mk_Misa(v); - /* Suppress changing C if nextPC would become misaligned or C was disabled at boot. */ - if (v.C() == 0b0 & nextPC[1] == bitone) | ~(sys_enable_rvc()) + /* Suppress changing C if nextPC would become misaligned or an extension vetoes or C was disabled at boot (i.e. not supported). */ + if (v.C() == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C())) | ~(sys_enable_rvc()) then m else update_C(m, v.C()) } |