add Sstc extension

model/riscv_csr_map.sail

@@ -111,6 +111,11 @@ mapping clause csr_name_map = 0x141  <-> "sepc"
 mapping clause csr_name_map = 0x142  <-> "scause"
 mapping clause csr_name_map = 0x143  <-> "stval"
 mapping clause csr_name_map = 0x144  <-> "sip"
+/* supervisor environment configuration */
+mapping clause csr_name_map = 0x10A  <-> "senvcfg"
+/* Sstc - Supervisor Timer Register */
+mapping clause csr_name_map = 0x14D  <-> "stimecmp"
+mapping clause csr_name_map = 0x15D  <-> "stimecmph"
 /* supervisor protection and translation */
 mapping clause csr_name_map = 0x180  <-> "satp"
 /* machine information registers */
@@ -133,6 +138,9 @@ mapping clause csr_name_map = 0x341  <-> "mepc"
 mapping clause csr_name_map = 0x342  <-> "mcause"
 mapping clause csr_name_map = 0x343  <-> "mtval"
 mapping clause csr_name_map = 0x344  <-> "mip"
+/* machine environment configuration */
+mapping clause csr_name_map = 0x30A  <-> "menvcfg"
+mapping clause csr_name_map = 0x31A  <-> "menvcfgh"
 /* machine protection and translation */
 mapping clause csr_name_map = 0x3A0  <-> "pmpcfg0"
 mapping clause csr_name_map = 0x3A1  <-> "pmpcfg1"

model/riscv_insts_zicsr.sail

@@ -148,6 +148,8 @@ function readCSR csr : csreg -> xlenbits = {
     (0x142,  _) => scause.bits,
     (0x143,  _) => stval,
     (0x144,  _) => lower_mip(mip, mideleg).bits,
+    (0x14D,  _) => stimecmp[sizeof(xlen) - 1 .. 0],
+    (0x15D, 32) => stimecmp[63 .. 32],
     (0x180,  _) => satp,
 
     /* user mode counters */
@@ -184,10 +186,10 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x304,  _) => { mie = legalize_mie(mie, value); Some(mie.bits) },
     (0x305,  _) => { Some(set_mtvec(value)) },
     (0x306,  _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits)) },
-    (0x30A, 32) => { menvcfg = legalize_envcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); Some(menvcfg.bits[31 .. 0]) },
-    (0x30A, 64) => { menvcfg = legalize_envcfg(menvcfg, value); Some(menvcfg.bits) },
+    (0x30A, 32) => { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); Some(menvcfg.bits[31 .. 0]) },
+    (0x30A, 64) => { menvcfg = legalize_menvcfg(menvcfg, value); Some(menvcfg.bits) },
     (0x310, 32) => { Some(mstatush.bits) }, // ignore writes for now
-    (0x31A, 32) => { menvcfg = legalize_envcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); Some(menvcfg.bits[63 .. 32]) },
+    (0x31A, 32) => { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); Some(menvcfg.bits[63 .. 32]) },
     (0x320,  _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits)) },
     (0x340,  _) => { mscratch = value; Some(mscratch) },
     (0x341,  _) => { Some(set_xret_target(Machine, value)) },
@@ -223,12 +225,14 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x104,  _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits) },
     (0x105,  _) => { Some(set_stvec(value)) },
     (0x106,  _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits)) },
-    (0x10A,  _) => { senvcfg = legalize_envcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits[sizeof(xlen) - 1 .. 0]) },
+    (0x10A,  _) => { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits[sizeof(xlen) - 1 .. 0]) },
     (0x140,  _) => { sscratch = value; Some(sscratch) },
     (0x141,  _) => { Some(set_xret_target(Supervisor, value)) },
     (0x142,  _) => { scause.bits = value; Some(scause.bits) },
     (0x143,  _) => { stval = value; Some(stval) },
     (0x144,  _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits) },
+    (0x14D,  _) => { stimecmp[(sizeof(xlen) - 1) .. 0] = value; Some(stimecmp[sizeof(xlen) - 1 ..0]) },
+    (0x15D, 32) => { stimecmp[63 ..32] = value; Some(stimecmp[63 .. 32]) },
     (0x180,  _) => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) },
 
     /* user mode: seed (entropy source). writes are ignored */

model/riscv_platform.sail

@@ -273,7 +273,16 @@ function clint_dispatch() -> unit = {
   if mtimecmp <=_u mtime then {
     if   get_config_print_platform()
     then print_platform(" clint timer pending at mtime " ^ BitStr(mtime));
-    mip[MTI] = 0b1
+    mip[MTI] = 0b1;
+  };
+  /* Sstc - supervisor Timer Register */
+  if haveSstc() & menvcfg[STCE] == 0b1 then {
+    mip[STI] = 0b0;
+    if stimecmp <=_u mtime then {
+      if   get_config_print_platform()
+      then print_platform(" supervisor timer pending at mtime " ^ BitStr(mtime));
+      mip[STI] = 0b1;
+    }
   }
 }
 

model/riscv_sys_control.sail

@@ -134,6 +134,9 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0x142 => haveSupMode() & (p == Machine | p == Supervisor), // scause
     0x143 => haveSupMode() & (p == Machine | p == Supervisor), // stval
     0x144 => haveSupMode() & (p == Machine | p == Supervisor), // sip
+    /* Sstc : Supervisor Timer Register */
+    0x14D => haveSupMode() & haveSstc() & (p == Machine | (p == Supervisor & (menvcfg.STCE() == 0b1))), // stimecmp
+    0x15D => haveSupMode() & haveSstc() & (p == Machine | (p == Supervisor & (menvcfg.STCE() == 0b1))), // stimecmph
 
     /* supervisor mode: address translation */
     0x180 => haveSupMode() & (p == Machine | p == Supervisor), // satp
@@ -167,7 +170,9 @@ function check_Counteren(csr : csreg, p : Privilege) -> bool =
     (0xC00, Supervisor) => mcounteren[CY] == 0b1,
     (0xC01, Supervisor) => mcounteren[TM] == 0b1,
     (0xC02, Supervisor) => mcounteren[IR] == 0b1,
-
+    /* Sstc extension */
+    (0x14D, Supervisor) => mcounteren[TM] == 0b1,
+    (0x15D, Supervisor) => mcounteren[TM] == 0b1,
     (0xC00, User) => mcounteren[CY] == 0b1 & (not(haveSupMode()) | scounteren[CY] == 0b1),
     (0xC01, User) => mcounteren[TM] == 0b1 & (not(haveSupMode()) | scounteren[TM] == 0b1),
     (0xC02, User) => mcounteren[IR] == 0b1 & (not(haveSupMode()) | scounteren[IR] == 0b1),

model/riscv_sys_regs.sail

@@ -140,6 +140,30 @@ bitfield Misa : xlenbits = {
 }
 register misa : Misa
 
+// menvcfg is 64 bits. senvcfg is SXLEN bits and does not have the two
+// upper fields so for simplicity we can use the same type.
+bitfield Envcfg : bits(64) = {
+  // Supervisor TimeCmp Extension
+  STCE   : 63,
+  // Page Based Memory Types Extension
+  PBMTE  : 62,
+  // Reserved WPRI bits.
+  wpri_1 : 61 .. 8,
+  // Cache Block Zero instruction Enable
+  CBZE   : 7,
+  // Cache Block Clean and Flush instruction Enable
+  CBCFE  : 6,
+  // Cache Block Invalidate instruction Enable
+  CBIE   : 5 .. 4,
+  // Reserved WPRI bits.
+  wpri_0 : 3 .. 1,
+  // Fence of I/O implies Memory
+  FIOM   : 0,
+}
+
+register menvcfg : Envcfg
+register senvcfg : Envcfg
+
 /* whether misa is R/W */
 val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform.enable_writable_misa", _: "sys_enable_writable_misa"} : unit -> bool
 /* whether misa.c was enabled at boot */
@@ -222,6 +246,9 @@ function haveZmmul()  -> bool = true
 /* Zicond extension support */
 function haveZicond() -> bool = true
 
+/* Sstc extension support */
+function haveSstc() -> bool = true
+
 bitfield Mstatush : bits(32) = {
   MBE  : 5,
   SBE  : 4
@@ -399,7 +426,13 @@ function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = {
   /* The only writable bits are the S-mode bits, and with the 'N'
    * extension, the U-mode bits. */
   let v = Mk_Minterrupts(v);
-  let m = [o with SEI = v[SEI], STI = v[STI], SSI = v[SSI]];
+
+  let m = [o with SEI = v[SEI], SSI = v[SSI]];
+
+  let m = if ( not(haveSstc()) | (haveSstc() & (menvcfg[STCE] == 0b0)) ) then {
+    [m with STI = v[STI]];
+  } else m;
+
   if haveUsrMode() & haveNExt() then {
     [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]]
   } else m
@@ -702,7 +735,13 @@ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
 /* Returns the new value of mip from the previous mip (o) and the written sip (s) as delegated by mideleg (d). */
 function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = {
   let m : Minterrupts = o;
+
   let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m;
+
+  let m = if d[STI] == 0b1 & (not(haveSstc()) | (haveSstc() & menvcfg[STCE] == 0b0)) then {
+    [m with STI = s[STI]]
+  } else m;
+
   if haveNExt() then {
     let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m;
     let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m;
@@ -828,37 +867,20 @@ function read_seed_csr() -> xlenbits = {
 /* Writes to the seed CSR are ignored */
 function write_seed_csr () -> option(xlenbits) = None()
 
-// menvcfg is 64 bits. senvcfg is SXLEN bits and does not have the two
-// upper fields so for simplicity we can use the same type.
-bitfield Envcfg : bits(64) = {
-  // Supervisor TimeCmp Extension
-  STCE   : 63,
-  // Page Based Memory Types Extension
-  PBMTE  : 62,
-  // Reserved WPRI bits.
-  wpri_1 : 61 .. 8,
-  // Cache Block Zero instruction Enable
-  CBZE   : 7,
-  // Cache Block Clean and Flush instruction Enable
-  CBCFE  : 6,
-  // Cache Block Invalidate instruction Enable
-  CBIE   : 5 .. 4,
-  // Reserved WPRI bits.
-  wpri_0 : 3 .. 1,
-  // Fence of I/O implies Memory
-  FIOM   : 0,
-}
-
-register menvcfg : Envcfg
-register senvcfg : Envcfg
-
-function legalize_envcfg(o : Envcfg, v : bits(64)) -> Envcfg = {
+function legalize_senvcfg(o : Envcfg, v : bits(64)) -> Envcfg = {
   let v = Mk_Envcfg(v);
   let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0];
   // Other extensions are not implemented yet so all other fields are read only zero.
   o
 }
 
+function legalize_menvcfg(o : Envcfg, v : bits(64)) -> Envcfg = {
+  let v = Mk_Envcfg(v);
+  let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0);
+  let o = update_STCE(o, if haveSstc() then v.STCE() else 0b0);
+  // Other extensions are not implemented yet so all other fields are read only zero.
+  o
+}
 // Return whether or not FIOM is currently active, based on the current
 // privilege and the menvcfg/senvcfg settings. This means that I/O fences
 // imply memory fence.
@@ -950,4 +972,8 @@ val get_vtype_vma : unit -> agtype
 function get_vtype_vma() = decode_agtype(vtype[vma])
 
 val get_vtype_vta : unit -> agtype
+
 function get_vtype_vta() = decode_agtype(vtype[vta])
+
+/* Sstc : Supervisor Timer Register */
+register stimecmp : bits(64)