add 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)
 {
@@ -161,3 +162,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

@@ -38,3 +38,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

@@ -22,6 +22,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

@@ -26,6 +26,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

@@ -52,6 +52,9 @@ const char *RV32ISA = "RV32IMAC";
 #define OPT_TRACE_OUTPUT 1000
 #define OPT_ENABLE_WRITABLE_FIOM 1001
 
+#define OPT_SMRNMI_INT_TRAP_VEC 1004
+#define OPT_SMRNMI_EXC_TRAP_VEC 1005
+
 static bool do_dump_dts = false;
 static bool do_show_times = false;
 struct tv_spike_t *s = NULL;
@@ -145,6 +148,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 }
 };
 
@@ -381,6 +386,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

@@ -160,6 +160,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

@@ -856,3 +856,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

@@ -146,6 +146,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 */
 
@@ -238,6 +244,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

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

@@ -102,6 +102,12 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
  0x343 => p == Machine, // mtval
  0x344 => p == Machine, // mip
 
+ /* 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
+
  0x3A0 => p == Machine, // pmpcfg0
  0x3A1 => p == Machine & (sizeof(xlen) == 32), // pmpcfg1
  0x3A2 => p == Machine, // pmpcfg2
@@ -237,6 +243,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.
  */
@@ -336,14 +343,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) {
@@ -364,10 +375,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 */
@@ -468,6 +480,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 = {
@@ -496,6 +532,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();
@@ -602,6 +653,14 @@ function init_sys() -> unit = {
  minstret_increment = true;
 
  menvcfg->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);
+
  senvcfg->bits() = zero_extend(0b0);
  /* initialize vector csrs */
  elen = 0b1; /* ELEN=64 as the common case */

model/riscv_sys_exceptions.sail

@@ -77,12 +77,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

@@ -215,6 +215,20 @@ function haveZmmul() -> bool = true
 /* Zicond extension support */
 function haveZicond() -> bool = true
 
+/* Smrnmi extension support */
+function haveSmrnmi() -> bool = true
+
+/* H extension support */
+function haveHext() -> bool = false
+
+function legalize_priv_level (p : priv_level) -> priv_level =
+ match (haveUsrMode(), p) {
+ (false, _) => privLevel_to_bits(Machine),
+ (true, 0b01) => if haveSupMode() then p else privLevel_to_bits(User),
+ (true, 0b10) => privLevel_to_bits(User),
+ (true, _) => p
+ }
+
 bitfield Mstatush : bits(32) = {
  MBE : 5,
  SBE : 4
@@ -515,6 +529,31 @@ function pc_alignment_mask() -> xlenbits =
 register mtval : xlenbits
 register mscratch : xlenbits
 
+/* Smrnmi : resumable NMI registers */
+bitfield Mnstatus : xlenbits = {
+ MNPP : 12 .. 11,
+ MNPV : 7,
+ NMIE : 3,
+}
+register mnscratch : xlenbits
+register mnepc : xlenbits
+register mncause : Mcause
+register mnstatus : Mnstatus
+
+function legalize_mnstatus(o : Mnstatus, v : xlenbits) -> Mnstatus = {
+ let m = o;
+ let v = Mk_Mnstatus(v);
+ let m = if haveHext() then update_MNPV(m, v.MNPV()) else m;
+ let m = update_MNPP(m, legalize_priv_level(v.MNPP()));
+ /* NMIE can be set but not cleared */
+ let m = update_NMIE(m, (m.NMIE() | v.NMIE()));
+ m
+}
+function legalize_mncause(o : Mcause, v : xlenbits) -> Mcause = {
+ let v = Mk_Mcause(v);
+ update_Cause(o, v.Cause());
+}
+
 /* counters */
 
 bitfield Counteren : bits(32) = {

model/riscv_types.sail

@@ -209,7 +209,8 @@ enum InterruptType = {
  I_M_Timer,
  I_U_External,
  I_S_External,
- I_M_External
+ I_M_External,
+ I_M_RNMI
 }
 
 val interruptType_to_bits : InterruptType -> exc_code
@@ -223,7 +224,8 @@ function interruptType_to_bits (i) =
  I_M_Timer => 0x07,
  I_U_External => 0x08,
  I_S_External => 0x09,
- I_M_External => 0x0b
+ I_M_External => 0x0b,
+ I_M_RNMI => 0xff
  }
 
 /* architectural exception definitions */