diff options
| author | Robert Norton <rmn30@cam.ac.uk> | 2019-09-16 17:50:25 +0100 |
|---|---|---|
| committer | Robert Norton <rmn30@cam.ac.uk> | 2019-09-17 14:55:17 +0100 |
| commit | b3d31566099101ac7399d74adcb1d138a016b390 (patch) | |
| tree | 98f83dc823cfe53c063823f3f4a48933622fc634 | |
| parent | d07ded0537e9367bb6e8c53f75a02403b6cdc0e4 (diff) | |
| download | sail-riscv-b3d31566099101ac7399d74adcb1d138a016b390.zip sail-riscv-b3d31566099101ac7399d74adcb1d138a016b390.tar.gz sail-riscv-b3d31566099101ac7399d74adcb1d138a016b390.tar.bz2 | |
Add a hook for extensions to supress writes to misa.C if necessary.ext_misa
| -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()) } |