From 51a6c967fb320c2d47a3630b1f392e54eb69c3d7 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Sat, 23 Sep 2023 19:57:38 +0100 Subject: 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. --- handwritten_support/riscv_extras.lem | 4 ++++ handwritten_support/riscv_extras.v | 1 + handwritten_support/riscv_extras_sequential.lem | 4 ++++ 3 files changed, 9 insertions(+) (limited to 'handwritten_support') diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index a476136..5d1fd85 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -161,6 +161,10 @@ val sys_enable_zfinx : unit -> bool let sys_enable_zfinx () = false declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx` +val sys_enable_fiom : unit -> bool +let sys_enable_fiom () = true +declare ocaml target_rep function sys_enable_fiom = `Platform.enable_fiom` + val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_ram_base () = wordFromInteger 0 declare ocaml target_rep function plat_ram_base = `Platform.dram_base` 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. *) diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index 41ca9c6..a7b4899 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -153,6 +153,10 @@ val sys_enable_next : unit -> bool let sys_enable_next () = true declare ocaml target_rep function sys_enable_next = `Platform.enable_next` +val sys_enable_fiom : unit -> bool +let sys_enable_fiom () = true +declare ocaml target_rep function sys_enable_fiom = `Platform.enable_fiom` + val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_ram_base () = wordFromInteger 0 declare ocaml target_rep function plat_ram_base = `Platform.dram_base` -- cgit v1.1