Skip to content

Commit

Permalink
add Smrnmi extension
Browse files Browse the repository at this point in the history
  • Loading branch information
ved-rivos committed Feb 6, 2024
1 parent 4de2bff commit d9204f6
Show file tree
Hide file tree
Showing 16 changed files with 237 additions and 10 deletions.
20 changes: 20 additions & 0 deletions c_emulator/riscv_platform.c
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand Down Expand Up @@ -166,3 +167,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;
}
5 changes: 5 additions & 0 deletions c_emulator/riscv_platform.h
Original file line number Diff line number Diff line change
Expand Up @@ -40,3 +40,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);
4 changes: 4 additions & 0 deletions c_emulator/riscv_platform_impl.c
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,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)
{
Expand Down
4 changes: 4 additions & 0 deletions c_emulator/riscv_platform_impl.h
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,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);

Expand Down
15 changes: 15 additions & 0 deletions c_emulator/riscv_sim.c
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,9 @@ const char *RV32ISA = "RV32IMAC";
#define OPT_PMP_COUNT 1002
#define OPT_PMP_GRAIN 1003

#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;
Expand Down Expand Up @@ -148,6 +151,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 }
};

Expand Down Expand Up @@ -400,6 +405,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;
Expand Down
7 changes: 7 additions & 0 deletions model/riscv_csr_map.sail
Original file line number Diff line number Diff line change
Expand Up @@ -220,6 +220,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"
Expand Down
19 changes: 19 additions & 0 deletions model/riscv_insts_base.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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"
12 changes: 12 additions & 0 deletions model/riscv_insts_zicsr.sail
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,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 */

Expand Down Expand Up @@ -213,6 +219,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) },

Expand Down
5 changes: 4 additions & 1 deletion model/riscv_step.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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() => {
Expand Down
69 changes: 64 additions & 5 deletions model/riscv_sys_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -105,6 +105,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),
Expand Down Expand Up @@ -222,6 +228,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.
*/
Expand Down Expand Up @@ -321,14 +328,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) {
Expand All @@ -349,10 +360,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 */
Expand Down Expand Up @@ -453,6 +465,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 = {
Expand Down Expand Up @@ -481,6 +517,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];
Expand Down Expand Up @@ -588,6 +639,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 */
Expand Down
16 changes: 15 additions & 1 deletion model/riscv_sys_exceptions.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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
};
Expand Down
39 changes: 39 additions & 0 deletions model/riscv_sys_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -222,6 +222,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
Expand Down Expand Up @@ -510,6 +524,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) = {
Expand Down
6 changes: 4 additions & 2 deletions model/riscv_types.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 */
Expand Down
Loading

0 comments on commit d9204f6

Please sign in to comment.