add Sstc extension

model/riscv_csr_map.sail

@@ -49,6 +49,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"
 /* supervisor envcfg */
@@ -76,6 +81,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

@@ -87,6 +87,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 */
@@ -168,6 +170,8 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (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

@@ -211,7 +211,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

@@ -73,6 +73,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
@@ -106,7 +109,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

@@ -78,6 +78,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 */
@@ -168,6 +192,9 @@ function haveZalrsc() -> bool = haveAtomics()
 /* Zicond extension support */
 function haveZicond() -> bool = true
 
+/* Sstc extension support */
+function haveSstc() -> bool = true
+
 /*
  * Illegal values legalized to least privileged mode supported.
  * Note: the only valid combinations of supported modes are M, M+U, M+S+U.
@@ -369,7 +396,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()) | 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
@@ -673,7 +706,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()) | 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;
@@ -799,6 +838,7 @@ function read_seed_csr() -> xlenbits = {
 /* Writes to the seed CSR are ignored */
 function write_seed_csr () -> option(xlenbits) = None()
 
+<<<<<<< HEAD
 bitfield MEnvcfg : bits(64) = {
   // Supervisor TimeCmp Extension
   STCE   : 63,
@@ -843,11 +883,22 @@ function legalize_menvcfg(o : MEnvcfg, v : bits(64)) -> MEnvcfg = {
 
 function legalize_senvcfg(o : SEnvcfg, v : xlenbits) -> SEnvcfg = {
   let v = Mk_SEnvcfg(v);
+=======
+function legalize_senvcfg(o : Envcfg, v : bits(64)) -> Envcfg = {
+  let v = Mk_Envcfg(v);
+>>>>>>> 1d0f240 (add Sstc extension)
   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.
@@ -941,4 +992,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)