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 Jan 28, 2024
1 parent d7a3d80 commit fc68c76
Show file tree
Hide file tree
Showing 16 changed files with 235 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 @@ -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)srnmi_exc_trap_vec;
}
mach_bits rnmi_int_trap_vector(unit u)
{
return (mach_bits)srnmi_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 @@ -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);
4 changes: 4 additions & 0 deletions c_emulator/riscv_platform_impl.c
Original file line number Diff line number Diff line change
Expand Up @@ -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);

/* Srnmi : Resumable NMI vectors */
uint64_t srnmi_int_trap_vec = UINT64_C(0);
uint64_t srnmi_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 @@ -26,6 +26,10 @@ extern uint64_t rv_ram_size;
extern uint64_t rv_rom_base;
extern uint64_t rv_rom_size;

/* Srnmi : Resumable NMI vectors */
extern uint64_t srnmi_int_trap_vec;
extern uint64_t srnmi_exc_trap_vec;

// Provides entropy for the scalar cryptography extension.
extern uint64_t rv_16_random_bits(void);

Expand Down
13 changes: 13 additions & 0 deletions c_emulator/riscv_sim.c
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,9 @@ const char *RV32ISA = "RV32IMAC";
#define OPT_TRACE_OUTPUT 1000
#define OPT_ENABLE_WRITABLE_FIOM 1001

#define OPT_SRNMI_INT_TRAP_VEC 1004
#define OPT_SRNMI_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 @@ -145,6 +148,8 @@ static struct option options[] = {
#ifdef SAILCOV
{"sailcov-file", required_argument, 0, 'c' },
#endif
{"srnmi_int_trap_vec", required_argument, 0, OPT_SRNMI_INT_TRAP_VEC },
{"srnmi_exc_trap_vec", required_argument, 0, OPT_SRNMI_EXC_TRAP_VEC },
{0, 0, 0, 0 }
};

Expand Down Expand Up @@ -381,6 +386,14 @@ 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_SRNMI_INT_TRAP_VEC:
srnmi_int_trap_vec = strtoull(optarg, NULL, 16);
fprintf(stderr, "using 0x%lx as SRNMI Int. trap vector.\n", srnmi_int_trap_vec);
break;
case OPT_SRNMI_EXC_TRAP_VEC:
srnmi_exc_trap_vec = strtoull(optarg, NULL, 16);
fprintf(stderr, "using 0x%lx as SRNMI Exc. trap vector.\n", srnmi_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 @@ -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"
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 @@ -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 */

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

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 @@ -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
Expand Down Expand Up @@ -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.
*/
Expand Down Expand Up @@ -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) {
Expand All @@ -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 */
Expand Down Expand Up @@ -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 = {
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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 */
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 @@ -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
Expand Down Expand Up @@ -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) = {
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 fc68c76

Please sign in to comment.