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

@@ -162,6 +162,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 */
@@ -198,10 +200,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)) },
@@ -248,12 +250,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

@@ -280,6 +280,15 @@ function clint_dispatch() -> unit = {
     if   get_config_print_platform()
     then print_platform(" clint timer pending at mtime " ^ BitStr(mtime));
     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

@@ -149,6 +149,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
@@ -182,6 +185,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),

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 */
@@ -215,6 +239,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
@@ -393,7 +420,9 @@ function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = {
    * extension, the U-mode bits. */
   let v = Mk_Minterrupts(v);
   let m = update_SEI(o, v.SEI());
-  let m = update_STI(m, v.STI());
+  let m = if ( not(haveSstc()) | (haveSstc() & (menvcfg.STCE() == 0b0)) ) then {
+    update_STI(m, v.STI());
+  } else m;
   let m = update_SSI(m, v.SSI());
   if haveUsrMode() & haveNExt() then {
     let m = update_UEI(m, v.UEI());
@@ -716,6 +745,9 @@ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
 function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = {
   let m : Minterrupts = o;
   let m = if d.SSI() == 0b1 then update_SSI(m, s.SSI()) else m;
+  let m = if d.STI() == 0b1 & (not(haveSstc()) | (haveSstc() & menvcfg.STCE() == 0b0)) then {
+    update_STI(m, s.STI());
+  } else m;
   if haveNExt() then {
     let m = if d.UEI() == 0b1 then update_UEI(m, s.UEI()) else m;
     let m = if d.USI() == 0b1 then update_USI(m, s.USI()) else m;
@@ -841,37 +873,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,
+function legalize_senvcfg(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);
+  // Other extensions are not implemented yet so all other fields are read only zero.
+  o
 }
 
-register menvcfg : Envcfg
-register senvcfg : Envcfg
-
-function legalize_envcfg(o : Envcfg, v : bits(64)) -> Envcfg = {
+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.
@@ -964,3 +979,6 @@ 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)