Add Svinval extension.

Makefile

@@ -27,6 +27,8 @@ SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_cext
 SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_cfext.sail
 SAIL_DEFAULT_INST += riscv_insts_dext.sail riscv_insts_cdext.sail
 
+SAIL_DEFAULT_INST += riscv_insts_svinval.sail
+
 SAIL_DEFAULT_INST += riscv_insts_zba.sail
 SAIL_DEFAULT_INST += riscv_insts_zbb.sail
 SAIL_DEFAULT_INST += riscv_insts_zbc.sail

c_emulator/riscv_platform.c

@@ -32,6 +32,11 @@ bool sys_enable_fdext(unit u)
   return rv_enable_fdext;
 }
 
+bool sys_enable_svinval(unit u)
+{
+  return rv_enable_svinval;
+}
+
 bool sys_enable_zcb(unit u)
 {
   return rv_enable_zcb;

c_emulator/riscv_platform.h

@@ -4,6 +4,7 @@
 bool sys_enable_rvc(unit);
 bool sys_enable_next(unit);
 bool sys_enable_fdext(unit);
+bool sys_enable_svinval(unit);
 bool sys_enable_zcb(unit);
 bool sys_enable_zfinx(unit);
 bool sys_enable_writable_misa(unit);

c_emulator/riscv_platform_impl.c

@@ -6,6 +6,7 @@
 uint64_t rv_pmp_count = 0;
 uint64_t rv_pmp_grain = 0;
 
+bool rv_enable_svinval = false;
 bool rv_enable_zcb = false;
 bool rv_enable_zfinx = false;
 bool rv_enable_rvc = true;

c_emulator/riscv_platform_impl.h

@@ -11,6 +11,7 @@
 extern uint64_t rv_pmp_count;
 extern uint64_t rv_pmp_grain;
 
+extern bool rv_enable_svinval;
 extern bool rv_enable_zcb;
 extern bool rv_enable_zfinx;
 extern bool rv_enable_rvc;

c_emulator/riscv_sim.c

@@ -53,6 +53,7 @@ const char *RV32ISA = "RV32IMAC";
 #define OPT_ENABLE_WRITABLE_FIOM 1001
 #define OPT_PMP_COUNT 1002
 #define OPT_PMP_GRAIN 1003
+#define OPT_ENABLE_SVINVAL 1004
 #define OPT_ENABLE_ZCB 10014
 
 static bool do_dump_dts = false;
@@ -146,6 +147,7 @@ static struct option options[] = {
     {"inst-limit",                  required_argument, 0, 'l'                     },
     {"enable-zfinx",                no_argument,       0, 'x'                     },
     {"enable-writable-fiom",        no_argument,       0, OPT_ENABLE_WRITABLE_FIOM},
+    {"enable-svinval",              no_argument,       0, OPT_ENABLE_SVINVAL      },
     {"enable-zcb",                  no_argument,       0, OPT_ENABLE_ZCB          },
 #ifdef SAILCOV
     {"sailcov-file",                required_argument, 0, 'c'                     },

model/riscv_insts_svinval.sail

@@ -0,0 +1,52 @@
+/*=======================================================================================*/
+/*  This Sail RISC-V architecture model, comprising all files and                        */
+/*  directories except where otherwise noted is subject the BSD                          */
+/*  two-clause license in the LICENSE file.                                              */
+/*                                                                                       */
+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+union clause ast = SINVAL_VMA : (regidx, regidx)
+
+mapping clause encdec =
+      SINVAL_VMA(rs1, rs2)                                                  if haveSvinval()
+  <-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
+
+function clause execute SINVAL_VMA(rs1, rs2) = {
+  execute(SFENCE_VMA(rs1, rs2))
+}
+
+mapping clause assembly = SINVAL_VMA(rs1, rs2)
+  <-> "sinval.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
+/* ****************************************************************** */
+
+union clause ast = SFENCE_W_INVAL : unit
+
+mapping clause encdec =
+      SFENCE_W_INVAL()                                            if haveSvinval()
+  <-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
+
+function clause execute SFENCE_W_INVAL() = {
+  if cur_privilege == User
+  then { handle_illegal(); RETIRE_FAIL }
+  else { RETIRE_SUCCESS } // Implemented as no-op as all memory operations are visible immediately the current Sail model
+}
+
+mapping clause assembly = SFENCE_W_INVAL() <-> "sfence.w.inval"
+
+/* ****************************************************************** */
+
+union clause ast = SFENCE_INVAL_IR : unit
+
+mapping clause encdec =
+      SFENCE_INVAL_IR()                                           if haveSvinval()
+  <-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
+
+function clause execute SFENCE_INVAL_IR() = {
+  if cur_privilege == User
+  then { handle_illegal(); RETIRE_FAIL }
+  else { RETIRE_SUCCESS } // Implemented as no-op as all memory operations are visible immediately in current Sail model
+}
+
+mapping clause assembly = SFENCE_INVAL_IR() <-> "sfence.inval.ir"

model/riscv_sys_regs.sail

@@ -84,6 +84,8 @@ val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform.
 val sys_enable_rvc = {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool
 /* whether misa.{f,d} were enabled at boot */
 val sys_enable_fdext = {c: "sys_enable_fdext", ocaml: "Platform.enable_fdext", _: "sys_enable_fdext"} : unit -> bool
+/* whether Svinval was enabled at boot */
+val sys_enable_svinval = {c: "sys_enable_svinval", ocaml: "Platform.enable_svinval", _: "sys_enable_svinval"} : unit -> bool
 /* whether Zcb was enabled at boot */
 val sys_enable_zcb = {c: "sys_enable_zcb", ocaml: "Platform.enable_zcb", _: "sys_enable_zcb"} : unit -> bool
 /* whether zfinx was enabled at boot */
@@ -311,6 +313,8 @@ function haveZfh()     -> bool = (misa[F] == 0b1) & (mstatus[FS] != 0b00)
 /* V extension has to enable both via misa.V as well as mstatus.VS */
 function haveVExt()    -> bool = (misa[V] == 0b1) & (mstatus[VS] != 0b00)
 
+function haveSvinval() -> bool = sys_enable_svinval()
+
 /* Zcb has simple code-size saving instructions. (The Zcb extension depends on the Zca extension.) */
 function haveZcb()     -> bool = sys_enable_zcb()
 

ocaml_emulator/platform.ml

@@ -10,6 +10,7 @@ let config_enable_writable_misa        = ref true
 let config_enable_dirty_update         = ref false
 let config_enable_misaligned_access    = ref false
 let config_mtval_has_illegal_inst_bits = ref false
+let config_enable_svinval              = ref false
 let config_enable_zcb                  = ref false
 let config_enable_writable_fiom        = ref true
 let config_enable_vext                 = ref true
@@ -89,6 +90,7 @@ let enable_vext ()                   = !config_enable_vext
 let enable_dirty_update ()           = !config_enable_dirty_update
 let enable_misaligned_access ()      = !config_enable_misaligned_access
 let mtval_has_illegal_inst_bits ()   = !config_mtval_has_illegal_inst_bits
+let enable_svinval ()                = !config_enable_svinval
 let enable_zcb ()                    = !config_enable_zcb
 let enable_zfinx ()                  = false
 let enable_writable_fiom ()          = !config_enable_writable_fiom

ocaml_emulator/riscv_ocaml_sim.ml

@@ -53,6 +53,9 @@ let options = Arg.align ([("-dump-dts",
                           ("-mtval-has-illegal-inst-bits",
                            Arg.Set P.config_mtval_has_illegal_inst_bits,
                            " mtval stores instruction bits on an illegal instruction exception");
+                          ("-enable-svinval",
+                           Arg.Set P.config_enable_svinval,
+                           " enable Svinval extension");
                           ("-enable-zcb",
                            Arg.Set P.config_enable_zcb,
                            " enable Zcb (simple code size) extension");