From bc9f38a30a7339cf6edaaa5c6d41ece575ae4ebe Mon Sep 17 00:00:00 2001
From: Kristin Barber <kristinbarber@google.com>
Date: Thu, 24 Aug 2023 04:29:58 +0000
Subject: [PATCH]     Add Svinval extension.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

    These changes add the “Svinval” Standard Extension for Fine-Grained
    Address-Translation Cache Invalidation, Version 1.0 to the sail-riscv model.

    This extension defines five new instructions: SINVAL.VMA, SFENCE.W.INVAL,
    SFENCE.INVAL.IR, HINVAL.VVMA, HINVAL.GVMA.

    HINVAL.VVMA & HINVAL.GVMA are omitted since they build on the
    Hypervisor Extension which is yet to be included in the model.

    SFENCE.W.INVAL & SFENCE.INVAL.IR are treated as nops pending integration
    of the coherency model (rmem) with sail.

    The specification says that SINVAL.VMA behaves just as SFENCE.VMA,
    except there are additional ordering constraints with respect to the new
    SFENCE.W.INVAL & SFENCE.INVAL.IR instructions. Since these are nops, we
    can treat SINVAL.VMA as if it were SFENCE.VMA.
---
 model/riscv_insts_base.sail | 55 +++++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)

diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index d68e7a34f..cb8d4332f 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -877,3 +877,58 @@ function clause execute SFENCE_VMA(rs1, rs2) = {
 
 mapping clause assembly = SFENCE_VMA(rs1, rs2)
   <-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
+/* ****************************************************************** */
+union clause ast = SINVAL_VMA : (regidx, regidx)
+
+mapping clause encdec = SINVAL_VMA(rs1, rs2)
+  <-> 0b0001011 @ rs2 @ rs1 @ 0b000 @ 0b00000 @ 0b1110011
+
+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()
+    <-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
+
+function clause execute SFENCE_W_INVAL() = {
+  /* Guarantees that any previous stores already visible to the
+   * current RISC-V hart are ordered before subsequent SINVAL.VMA.
+   * Can be implemented as a no-op since all memory operations are
+   * visible immediately in the current model.*/
+
+  if cur_privilege == User
+  then { handle_illegal(); RETIRE_FAIL }
+  else { RETIRE_SUCCESS }
+}
+
+mapping clause assembly = SFENCE_W_INVAL() <-> "sfence.w.inval"
+
+/* ****************************************************************** */
+union clause ast = SFENCE_INVAL_IR : unit
+
+mapping clause encdec = SFENCE_INVAL_IR()
+    <-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
+
+function clause execute SFENCE_INVAL_IR() = {
+  /* Guarantees that any previous SINVAL.VMA instructions executed
+   * by the current hart are ordered before memory accesses from
+   * the current hart to the memory-management data structures.
+   * Can be implemented as a no-op since all memory operations are
+   * visible immediately in the current model. */
+
+  if cur_privilege == User
+  then { handle_illegal(); RETIRE_FAIL }
+  else { RETIRE_SUCCESS }
+
+}
+
+mapping clause assembly = SFENCE_INVAL_IR() <-> "sfence.inval.ir"
+
+/* ****************************************************************** */