Add Ssdbltrp and Smdbltrp extensions

model/riscv_csr_map.sail

@@ -75,7 +75,7 @@ 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"
-mapping clause csr_name_map = 0x348  <-> "mtval2"
+mapping clause csr_name_map = 0x34B  <-> "mtval2"
 /* machine protection and translation */
 mapping clause csr_name_map = 0x3A0  <-> "pmpcfg0"
 mapping clause csr_name_map = 0x3A1  <-> "pmpcfg1"

model/riscv_insts_zicsr.sail

@@ -46,7 +46,7 @@ function readCSR csr : csreg -> xlenbits = {
     (0x342,  _) => mcause.bits,
     (0x343,  _) => mtval,
     (0x344,  _) => mip.bits,
-    (0x348,  _) => mtval2,
+    (0x34B,  _) => mtval2,
 
     // pmpcfgN
     (0x3A @ idx : bits(4),  _) if idx[0] == bitzero | sizeof(xlen) == 32 => pmpReadCfgReg(unsigned(idx)),
@@ -133,7 +133,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x342,  _) => { mcause.bits = value; Some(mcause.bits) },
     (0x343,  _) => { mtval = value; Some(mtval) },
     (0x344,  _) => { mip = legalize_mip(mip, value); Some(mip.bits) },
-    (0x348,  _) => { mtval = value; Some(mtval) },
+    (0x34B,  _) => { mtval = value; Some(mtval) },
 
     // pmpcfgN
     (0x3A @ idx : bits(4),  _) if idx[0] == bitzero | sizeof(xlen) == 32 => {

model/riscv_platform.sail

@@ -458,6 +458,8 @@ function platform_handle_critical_error() -> unit = {
   /* When Debug Mode is added to model, then add Sddbltrp 
    * to wait for halt request.
    */
+  if   get_config_print_platform()
+  then print_platform("handling M-mode critical error");
   htif_done = true;
   htif_exit_code = zeros();
 }

model/riscv_sys_control.sail

@@ -39,7 +39,7 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0x342 => p == Machine, // mcause
     0x343 => p == Machine, // mtval
     0x344 => p == Machine, // mip
-    0x348 => p == Machine & (haveHExt() | haveSmdbltrp()), // mtval2
+    0x34B => p == Machine & (haveHExt() | haveSsdbltrp()), // mtval2
 
     // pmpcfgN
     0x3A @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | sizeof(xlen) == 32),

model/riscv_sys_regs.sail

@@ -211,31 +211,18 @@ register menvcfg : MEnvcfg
 register senvcfg : SEnvcfg
 
 bitfield Mstatush : bits(32) = {
-  MDT  : 6,
+  MDT  : 13,
   MBE  : 5,
   SBE  : 4
 }
 register mstatush : Mstatush
 
-function legalize_mstatush(o : Mstatush, v : xlenbits) -> Mstatush = {
-  /*
-   * Populate all defined fields using the bits of v, stripping anything
-   * that does not have a matching bitfield entry. All bits above 32 are handled
-   * explicitly later.
-   */
-  /* We don't currently support changing MBE and SBE. */
-  let m : Mstatush = Mk_Mstatush(zero_extend(v[6 .. 6] @ 0b000000));
-  let m = if not(haveSsdbltrp()) then [m with MDT = 0b0] else m;
-  m
-}
-
-
 bitfield Mstatus : xlenbits = {
   SD   : xlen - 1,
 
   // MDT bit introduced by Smdbltrp is also handled in same ad-hoc way
   // as done for MBE and SBE
-  // MDT  : 38
+  // MDT  : 45
 
   // The MBE and SBE fields are in mstatus in RV64 and absent in RV32.
   // On RV32, they are in mstatush, which doesn't exist in RV64.  For now,
@@ -248,7 +235,7 @@ bitfield Mstatus : xlenbits = {
   // SXL  : 35 .. 34,
   // UXL  : 33 .. 32,
 
-  SDT  : 23,
+  SDT  : 24,
   TSR  : 22,
   TW   : 21,
   TVM  : 20,
@@ -273,6 +260,20 @@ bitfield Mstatus : xlenbits = {
 }
 register mstatus : Mstatus
 
+function legalize_mstatush(o : Mstatush, v : xlenbits) -> Mstatush = {
+  /*
+   * Populate all defined fields using the bits of v, stripping anything
+   * that does not have a matching bitfield entry. All bits above 32 are handled
+   * explicitly later.
+   */
+  /* We don't currently support changing MBE and SBE. */
+  let m : Mstatush = Mk_Mstatush(zero_extend(v[6 .. 6] @ 0b000000));
+  let m = if not(haveSsdbltrp()) then [m with MDT = 0b0] else m;
+  /* When the MDT bit is set to 1, the MIE bit is cleared to 0. */
+  if m[MDT] == 0b1 then mstatus[MIE] = 0b0;
+  m
+}
+
 function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv : Privilege) -> Privilege =
   if   t != Execute() & m[MPRV] == 0b1
   then privLevel_of_bits(m[MPP])
@@ -311,13 +312,13 @@ function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
 function set_mstatus_MDT(v : bits(1) ) -> unit = {
   if   sizeof(xlen) == 32
   then mstatush[MDT] = v
-  else mstatus.bits[38 .. 38] = v;
+  else mstatus.bits[45 .. 45] = v;
 }
 
 function get_mstatus_MDT() -> bits(1) = {
   if   sizeof(xlen) == 32
   then mstatush[MDT]
-  else mstatus.bits[38 .. 38]
+  else mstatus.bits[45 .. 45]
 }
 
 function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
@@ -326,7 +327,7 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
    * that does not have a matching bitfield entry. All bits above 32 are handled
    * explicitly later.
    */
-  let m : Mstatus = Mk_Mstatus(zero_extend(v[23 .. 7] @ 0b0 @ v[5 .. 3] @ 0b0 @ v[1 .. 0]));
+  let m : Mstatus = Mk_Mstatus(zero_extend(v[24 .. 24] @ 0b0 @ v[22 .. 7] @ 0b0 @ v[5 .. 3] @ 0b0 @ v[1 .. 0]));
 
   /* We don't have any extension context yet. */
   let m = [m with XS = extStatus_to_bits(Off)];
@@ -350,11 +351,21 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
              Mk_Mstatus([m.bits with 37 .. 36 = 0b00])
           } else m;
 
-  /* Smdbltrp: legalize MDT (bit 38 - RV64 only) and SDT */
+  /* Smdbltrp: legalize MDT (bit 45 - RV64 only) and SDT */
   let m = if sizeof(xlen) == 64 then {
-             Mk_Mstatus([m.bits with 38 .. 38 = if haveSmdbltrp() then v[38 ..  38] else 0b0])
+             Mk_Mstatus([m.bits with 45 .. 45 = if haveSmdbltrp() then v[45 .. 45] else 0b0])
           } else m;
   let m = if not(haveSsdbltrp()) then [m with SDT = 0b0] else m;
+  /*
+   * When the MDT bit is set to 1, the MIE bit is cleared to 0.
+   * MIE cannot be set unless SDT is already 0 or is being set to 0
+   */
+  if m.bits[45 .. 45] == 0b1 then mstatus[MIE] = 0b0;
+  /*
+   * When the SDT bit is set to 1, the SIE bit is cleared to 0.
+   * SIE cannot be set unless SDT is already 0 or is being set to 0
+   */
+  if m[SDT] == 0b1 then mstatus[SIE] = 0b0;
 
   /* Hardwired to zero in the absence of 'U' or 'N'. */
   let m = if not(haveNExt()) then {
@@ -455,6 +466,7 @@ function legalize_mideleg(o : Minterrupts, v : xlenbits) -> Minterrupts = {
 /* exception processing state */
 
 bitfield Medeleg : xlenbits = {
+  Double_Trap_Fault : 16,
   SAMO_Page_Fault   : 15,
   Load_Page_Fault   : 13,
   Fetch_Page_Fault  : 12,
@@ -474,7 +486,8 @@ register medeleg : Medeleg  /* Delegation to S-mode */
 
 function legalize_medeleg(o : Medeleg, v : xlenbits) -> Medeleg = {
   /* M-EnvCalls delegation is not supported */
-  [Mk_Medeleg(v) with MEnvCall = 0b0]
+  /* Ssdbltrp: Double Trap delegation is not supported */
+  [Mk_Medeleg(v) with MEnvCall = 0b0, Double_Trap_Fault = 0b0]
 }
 
 /* registers for trap handling */
@@ -607,7 +620,7 @@ bitfield Sstatus : xlenbits = {
   // The UXL field does not exist on RV32, so we define an explicit
   // getter and setter below.
   // UXL  : 30 .. 29,
-  SDT  : 23,
+  SDT  : 24,
   MXR  : 19,
   SUM  : 18,
   XS   : 16 .. 15,