diff options
| author | Tim Hutt <timothy.hutt@codasip.com> | 2023-09-23 19:57:38 +0100 |
|---|---|---|
| committer | Bill McSpadden <bill@riscv.org> | 2023-10-11 20:50:13 -0500 |
| commit | 51a6c967fb320c2d47a3630b1f392e54eb69c3d7 (patch) | |
| tree | cd864017e11911f4e86c32e7a437993a9ce05a58 /handwritten_support/riscv_extras.v | |
| parent | 532714a6c71b47a91176eb90fef3b3b049c52fce (diff) | |
| download | sail-riscv-51a6c967fb320c2d47a3630b1f392e54eb69c3d7.zip sail-riscv-51a6c967fb320c2d47a3630b1f392e54eb69c3d7.tar.gz sail-riscv-51a6c967fb320c2d47a3630b1f392e54eb69c3d7.tar.bz2 | |
Implement menvcfg
This implements the m/senvcfg(h) CSRs. This CSR is used to enable/disable extensions and behaviours for lower privilege modes. Currently the only implemented bit is FIOM which affects how fences work.
It also affects how atomic memory accesses work in non-cacheable regions, but the model does not currently support PMAs so that can't easily be implemented.
Diffstat (limited to 'handwritten_support/riscv_extras.v')
| -rw-r--r-- | handwritten_support/riscv_extras.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index 14029ee..c879bf8 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -200,6 +200,7 @@ Axiom sys_enable_rvc : unit -> bool. Axiom sys_enable_fdext : unit -> bool. Axiom sys_enable_next : unit -> bool. Axiom sys_enable_zfinx : unit -> bool. +Axiom sys_enable_fiom : unit -> bool. (* The constraint solver can do this itself, but a Coq bug puts anonymous_subproof into the term instead of an actual subproof. *) |