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 /model | |
| 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.
Diffstat (limited to 'model')
| -rw-r--r-- | model/riscv_misa_ext.sail | 2 | ||||
| -rw-r--r-- | model/riscv_sys_regs.sail | 9 |
2 files changed, 9 insertions, 2 deletions
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()) } |