Add unratified Smrnmi extension

c_emulator/riscv_platform.c

@@ -16,6 +16,7 @@
 
 static mach_bits reservation = 0;
 static bool reservation_valid = false;
+static int is_rnmi_pending = 1;
 
 bool sys_enable_rvc(unit u)
 {
@@ -181,3 +182,22 @@ unit memea(mach_bits len, sail_int n)
 {
   return UNIT;
 }
+
+// Smrnmi : resumable NMI pending
+bool rnmi_pending(bool nmie)
+{
+  if (is_rnmi_pending && nmie) {
+    is_rnmi_pending = 0;
+    return true;
+  } else {
+    return false;
+  }
+}
+mach_bits rnmi_exc_trap_vector(unit u)
+{
+  return (mach_bits)smrnmi_exc_trap_vec;
+}
+mach_bits rnmi_int_trap_vector(unit u)
+{
+  return (mach_bits)smrnmi_int_trap_vec;
+}

c_emulator/riscv_platform.h

@@ -43,3 +43,8 @@ unit plat_term_write(mach_bits);
 mach_bits plat_htif_tohost(unit);
 
 unit memea(mach_bits, sail_int);
+
+// Smrnmi : resumable NMI
+bool rnmi_pending(bool);
+mach_bits rnmi_int_trap_vector(unit u);
+mach_bits rnmi_exc_trap_vector(unit u);

c_emulator/riscv_platform_impl.c

@@ -27,6 +27,10 @@ uint64_t rv_ram_size = UINT64_C(0x4000000);
 uint64_t rv_rom_base = UINT64_C(0x1000);
 uint64_t rv_rom_size = UINT64_C(0x100);
 
+/* Smrnmi : Resumable NMI vectors */
+uint64_t smrnmi_int_trap_vec = UINT64_C(0);
+uint64_t smrnmi_exc_trap_vec = UINT64_C(0);
+
 // Provides entropy for the scalar cryptography extension.
 uint64_t rv_16_random_bits(void)
 {

c_emulator/riscv_platform_impl.h

@@ -31,6 +31,10 @@ extern uint64_t rv_ram_size;
 extern uint64_t rv_rom_base;
 extern uint64_t rv_rom_size;
 
+/* Smrnmi : Resumable NMI vectors */
+extern uint64_t smrnmi_int_trap_vec;
+extern uint64_t smrnmi_exc_trap_vec;
+
 // Provides entropy for the scalar cryptography extension.
 extern uint64_t rv_16_random_bits(void);
 

c_emulator/riscv_sim.c

@@ -56,6 +56,8 @@ enum {
   OPT_PMP_GRAIN,
   OPT_ENABLE_SVINVAL,
   OPT_ENABLE_ZCB,
+  OPT_SMRNMI_INT_TRAP_VEC,
+  OPT_SMRNMI_EXC_TRAP_VEC,
 };
 
 static bool do_dump_dts = false;
@@ -154,6 +156,8 @@ static struct option options[] = {
 #ifdef SAILCOV
     {"sailcov-file",                required_argument, 0, 'c'                     },
 #endif
+    {"smrnmi_int_trap_vec",         required_argument, 0, OPT_SMRNMI_INT_TRAP_VEC },
+    {"smrnmi_exc_trap_vec",         required_argument, 0, OPT_SMRNMI_EXC_TRAP_VEC },
     {0,                             0,                 0, 0                       }
 };
 
@@ -415,6 +419,16 @@ static int process_args(int argc, char **argv)
       trace_log_path = optarg;
       fprintf(stderr, "using %s for trace output.\n", trace_log_path);
       break;
+    case OPT_SMRNMI_INT_TRAP_VEC:
+      smrnmi_int_trap_vec = strtoull(optarg, NULL, 16);
+      fprintf(stderr, "using 0x%lx as SMRNMI Int. trap vector.\n",
+              smrnmi_int_trap_vec);
+      break;
+    case OPT_SMRNMI_EXC_TRAP_VEC:
+      smrnmi_exc_trap_vec = strtoull(optarg, NULL, 16);
+      fprintf(stderr, "using 0x%lx as SMRNMI Exc. trap vector.\n",
+              smrnmi_exc_trap_vec);
+      break;
     case '?':
       print_usage(argv[0], 1);
       break;

model/riscv_csr_map.sail

@@ -163,6 +163,13 @@ mapping clause csr_name_map = 0xB02  <-> "minstret"
 mapping clause csr_name_map = 0xB80  <-> "mcycleh"
 mapping clause csr_name_map = 0xB82  <-> "minstreth"
 /* TODO: other hpm counters and events */
+
+/* Smrnmi - resumable NMI CSRs */
+mapping clause csr_name_map = 0x740  <-> "mnscratch"
+mapping clause csr_name_map = 0x741  <-> "mnepc"
+mapping clause csr_name_map = 0x742  <-> "mncause"
+mapping clause csr_name_map = 0x744  <-> "mnstatus"
+
 /* trigger/debug */
 mapping clause csr_name_map = 0x7a0  <-> "tselect"
 mapping clause csr_name_map = 0x7a1  <-> "tdata1"

model/riscv_insts_base.sail

@@ -729,3 +729,22 @@ 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 = MNRET : unit
+
+mapping clause encdec = MNRET() if haveSmrnmi()
+  <-> 0b0111000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSmrnmi()
+
+function clause execute MNRET() = {
+  if   cur_privilege != Machine
+  then { handle_illegal(); RETIRE_FAIL }
+  else if not(ext_check_mnret_priv ())
+  then { ext_fail_mnret_priv(); RETIRE_FAIL }
+  else {
+    set_next_pc(exception_handler(cur_privilege, CTL_MNRET(), PC));
+    RETIRE_SUCCESS
+  }
+}
+
+mapping clause assembly = MNRET() <-> "mnret"

model/riscv_insts_zicsr.sail

@@ -71,6 +71,12 @@ function readCSR csr : csreg -> xlenbits = {
     (0xC21, _) => vtype.bits,
     (0xC22, _) => vlenb,
 
+    /* Smrnmi - resumable NMI */
+    (0x740, _) => mnscratch,
+    (0x741, _) => mnepc & pc_alignment_mask(),
+    (0x742, _) => mncause.bits,
+    (0x744, _) => mnstatus.bits,
+
     /* trigger/debug */
     (0x7a0,  _) => ~(tselect),  /* this indicates we don't have any trigger support */
 
@@ -152,6 +158,12 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0xB80, 32) => { mcycle[63 .. 32] = value; Some(value) },
     (0xB82, 32) => { minstret[63 .. 32] = value; minstret_increment = false; Some(value) },
 
+    /* Smrnmi : resumable NMI */
+    (0x740,  _) => { mnscratch = value; Some(mnscratch) },
+    (0x741,  _) => { mnepc = value & pc_alignment_mask(); Some(mnepc & pc_alignment_mask()) },
+    (0x742,  _) => { mncause = legalize_mncause(mncause, value); Some(mncause.bits) },
+    (0x744,  _) => { mnstatus = legalize_mnstatus(mnstatus, value); Some(mnstatus.bits) },
+
     /* trigger/debug */
     (0x7a0,  _) => { tselect = value; Some(tselect) },
 

model/riscv_step.sail

@@ -28,7 +28,10 @@ function step(step_no : int) -> bool = {
       Some(intr, priv) => {
         if   get_config_print_instr()
         then print_bits("Handling interrupt: ", interruptType_to_bits(intr));
-        handle_interrupt(intr, priv);
+        match intr {
+          I_M_RNMI => { set_next_pc(rnmi_handler(PC)) },
+          _        => { handle_interrupt(intr, priv); }
+        };
         (RETIRE_FAIL, false)
       },
       None() => {

model/riscv_sys_control.sail

@@ -44,6 +44,12 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     // pmpcfgN
     0x3A @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | sizeof(xlen) == 32),
 
+    /* machine mode: Smrnmi RNMi handling */
+    0x740 => p == Machine & haveSmrnmi(), // mnscratch
+    0x741 => p == Machine & haveSmrnmi(), // mnepc
+    0x742 => p == Machine & haveSmrnmi(), // mncause
+    0x744 => p == Machine & haveSmrnmi(), // mnstatus
+
     // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits.
     0x3B @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b00 @ idx),
     0x3C @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b01 @ idx),
@@ -161,6 +167,7 @@ val load_reservation = {ocaml: "Platform.load_reservation", interpreter: "Platfo
 val match_reservation = {ocaml: "Platform.match_reservation", interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool
 val cancel_reservation = {ocaml: "Platform.cancel_reservation", interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit
 
+
 /* Exception delegation: given an exception and the privilege at which
  * it occured, returns the privilege at which it should be handled.
  */
@@ -260,14 +267,18 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
   }
 }
 
+/* Smrnmi : whether RNMI is pending */
+val rnmi_pending = {ocaml: "Platform.rnmi_pending", interpreter: "Platform.rnmi_pending", c: "rnmi_pending", lem: "rnmi_pending"} : bool -> bool
 /* Examine the current interrupt state and return an interrupt to be *
  * handled (if any), and the privilege it should be handled at.
  */
 function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege)) = {
   /* If we don't have different privilege levels, we don't need to check delegation.
    * Absence of U-mode implies absence of S-mode.
    */
-  if not(haveUsrMode()) | (not(haveSupMode()) & not(haveNExt())) then {
+  if haveSmrnmi() & rnmi_pending(mnstatus[NMIE] == 0b1) & mnstatus[NMIE] == 0b1 then {
+    let r = (I_M_RNMI, Machine) in Some(r)
+  } else if not(haveUsrMode()) | (not(haveSupMode()) & not(haveNExt())) then {
     assert(priv == Machine, "invalid current privilege");
     let enabled_pending = mip.bits & mie.bits;
     match findPendingInterrupt(enabled_pending) {
@@ -288,10 +299,11 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege
 /* types of privilege transitions */
 
 union ctl_result = {
-  CTL_TRAP : sync_exception,
-  CTL_SRET : unit,
-  CTL_MRET : unit,
-  CTL_URET : unit
+  CTL_TRAP  : sync_exception,
+  CTL_SRET  : unit,
+  CTL_MRET  : unit,
+  CTL_MNRET : unit,
+  CTL_URET  : unit
 }
 
 /* trap value */
@@ -392,6 +404,30 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
     }
   };
 }
+/* Smrnmi - resumable NMI */
+val rnmi_int_trap_vector = {ocaml: "Platform.rnmi_int_trap_vector", interpreter: "Platform.rnmi_int_trap_vector", c: "rnmi_int_trap_vector", lem: "rnmi_int_trap_vector"} : unit -> xlenbits
+function rnmi_handler(pc : xlenbits) -> xlenbits = {
+
+  rvfi_trap();
+  if   get_config_print_platform()
+  then print_platform("handling RNMI");
+
+  cancel_reservation();
+
+  mncause[Cause] = zero_extend(0b0);
+  mnstatus[NMIE] = 0b0;
+  mnstatus[MNPP] = privLevel_to_bits(cur_privilege);
+  mnepc          = pc;
+
+  cur_privilege  = Machine;
+
+  handle_trap_extension(Machine, pc, None());
+
+  if   get_config_print_reg()
+  then print_reg("CSR mnstatus <- " ^ BitStr(mnstatus.bits()));
+
+  rnmi_int_trap_vector();
+}
 
 function exception_handler(cur_priv : Privilege, ctl : ctl_result,
                            pc: xlenbits) -> xlenbits = {
@@ -420,6 +456,21 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       cancel_reservation();
       prepare_xret_target(Machine) & pc_alignment_mask()
     },
+    (_, CTL_MNRET())  => {
+      let prev_priv  = cur_privilege;
+      mnstatus[NMIE] = 0b1;
+      cur_privilege  = privLevel_of_bits(mnstatus.MNPP());
+      if   cur_privilege != Machine
+      then mstatus[MPRV] = 0b0;
+
+      if   get_config_print_reg()
+      then print_reg("CSR mnstatus <- " ^ BitStr(mnstatus.bits));
+      if   get_config_print_platform()
+      then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
+
+      cancel_reservation();
+      mnepc & pc_alignment_mask()
+    },
     (_, CTL_SRET())  => {
       let prev_priv   = cur_privilege;
       mstatus[SIE]  = mstatus[SPIE];
@@ -530,6 +581,14 @@ function init_sys() -> unit = {
 
   menvcfg.bits = zero_extend(0b0);
   senvcfg.bits = zero_extend(0b0);
+
+  /* Srnmi : resumable NMI */
+  mncause[Cause]       = zero_extend(0b0);
+  mncause[IsInterrupt] = 0b1;
+  mnepc                = zero_extend(0b0);
+  mnscratch            = zero_extend(0b0);
+  mnstatus.bits        = zero_extend(0b0);
+
   /* initialize vector csrs */
   elen               = 0b1; /* ELEN=64 as the common case */
   vlen               = 0b0100; /* VLEN=512 as a default value */

model/riscv_sys_exceptions.sail

@@ -15,12 +15,26 @@ function ext_check_xret_priv (p : Privilege) : Privilege -> bool = true
 /* Called if above check fails */
 function ext_fail_xret_priv () : unit -> unit = ()
 
+/* Is MNRET permitted by extension? */
+function ext_check_mnret_priv () : unit -> bool = true
+/* Called if above MNRET check fails */
+function ext_fail_mnret_priv () : unit -> unit = ()
+
 function handle_trap_extension(p : Privilege, pc : xlenbits, u : option(unit)) -> unit = ()
 
+/* Smrnmi : resumable NMI exception trap vector */
+val rnmi_exc_trap_vector = {ocaml: "Platform.rnmi_exc_trap_vector", interpreter: "Platform.rnmi_exc_trap_vector", c: "rnmi_exc_trap_vector", lem: "rnmi_exc_trap_vector"} : unit -> xlenbits
+
 /* used for traps and ECALL */
 function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = {
+
+  let to_rnmi_vec : bool = if haveSmrnmi() & p == Machine & mnstatus[NMIE] == 0b0 &
+                           privLevel_of_bits(mstatus[MPP]) == Machine then true
+                           else false;
+  let rnmi_exc_trap_vec : Mtvec = Mk_Mtvec(rnmi_exc_trap_vector());
+
   let tvec : Mtvec = match p {
-                       Machine    => mtvec,
+                       Machine    => if to_rnmi_vec then rnmi_exc_trap_vec else mtvec,
                        Supervisor => stvec,
                        User       => utvec
                      };

model/riscv_sys_regs.sail

@@ -172,6 +172,12 @@ function haveZalrsc() -> bool = haveAtomics()
 /* Zicond extension support */
 function haveZicond() -> bool = true
 
+/* Smrnmi extension support */
+function haveSmrnmi() -> bool = true
+
+/* H extension support */
+function haveHext() -> bool = false
+
 /*
  * Illegal values legalized to least privileged mode supported.
  * Note: the only valid combinations of supported modes are M, M+U, M+S+U.
@@ -231,8 +237,18 @@ bitfield Mstatus : xlenbits = {
 }
 register mstatus : Mstatus
 
+/* Smrnmi : resumable NMI registers */
+bitfield Mnstatus : xlenbits = {
+  MNPP : 12 .. 11,
+  MNPV : 7,
+  NMIE : 3,
+}
+register mnstatus  : Mnstatus
+register mnscratch : xlenbits
+register mnepc     : xlenbits
+
 function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv : Privilege) -> Privilege =
-  if   t != Execute() & m[MPRV] == 0b1
+  if   t != Execute() & m[MPRV] == 0b1 & ((mnstatus[NMIE] == 0b1) | not(haveSmrnmi()))
   then privLevel_of_bits(m[MPP])
   else priv
 
@@ -448,6 +464,8 @@ bitfield Mcause : xlenbits = {
   Cause       : xlen - 2 .. 0
 }
 register mcause : Mcause
+/* Smrnmi : resumable NMI cause register */
+register mncause   : Mcause
 
 /* Interpreting the trap-vector address */
 function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = {
@@ -484,6 +502,21 @@ function pc_alignment_mask() -> xlenbits =
 register mtval    : xlenbits
 register mscratch : xlenbits
 
+function legalize_mnstatus(o : Mnstatus, v : xlenbits) -> Mnstatus = {
+  let m = o;
+  let v = Mk_Mnstatus(v);
+  let m = [m with MNPV = if haveHext() then v[MNPV] else 0b0];
+  let m = [m with MNPP = if have_privLevel(v[MNPP]) then v[MNPP]
+                         else privLevel_to_bits(lowest_supported_privLevel())];
+  /* NMIE can be set but not cleared */
+  let m = [m with NMIE = (m[NMIE] | v[NMIE])];
+  m
+}
+function legalize_mncause(o : Mcause, v : xlenbits) -> Mcause = {
+  let v = Mk_Mcause(v);
+  [o with Cause = v[Cause]];
+}
+
 /* counters */
 
 bitfield Counteren : bits(32) = {