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 Jun 22, 2024
1 parent 40ed0c5 commit ebf046f
Show file tree
Hide file tree
Showing 16 changed files with 232 additions and 11 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 @@ -176,3 +177,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 @@ -42,3 +42,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 @@ -26,6 +26,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 @@ -30,6 +30,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 @@ -56,6 +56,9 @@ const char *RV32ISA = "RV32IMAC";
#define OPT_ENABLE_SVINVAL 1004
#define OPT_ENABLE_ZCB 10014

#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 @@ -152,6 +155,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 @@ -408,6 +413,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 @@ -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"
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 @@ -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"
12 changes: 12 additions & 0 deletions model/riscv_insts_zicsr.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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 */

Expand Down Expand Up @@ -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) },

Expand Down
5 changes: 4 additions & 1 deletion model/riscv_step.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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() => {
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 @@ -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),
Expand Down Expand Up @@ -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.
*/
Expand Down Expand Up @@ -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) {
Expand All @@ -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 */
Expand Down Expand Up @@ -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 = {
Expand Down Expand Up @@ -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];
Expand Down Expand Up @@ -529,6 +580,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 @@ -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
};
Expand Down
35 changes: 34 additions & 1 deletion model/riscv_sys_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -168,6 +168,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.
Expand Down Expand Up @@ -227,8 +233,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

Expand Down Expand Up @@ -444,6 +460,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) = {
Expand Down Expand Up @@ -480,6 +498,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) = {
Expand Down
Loading

0 comments on commit ebf046f

Please sign in to comment.