From 0edd11e1b1daa1bcce892616da435b02da95be6a Mon Sep 17 00:00:00 2001 From: Dan Smathers Date: Thu, 29 Feb 2024 23:46:52 -0700 Subject: [PATCH] Add unratified Smclic, Ssclic, Smclicshv extensions Spec: https://github.com/riscv/riscv-fast-interrupt Tests: https://github.com/riscv-non-isa/riscv-arch-test/pull/436 --- model/riscv_clic_control.sail | 528 ++++++++++++++++++++++++++++++++ model/riscv_clic_mem.sail | 21 ++ model/riscv_clic_regs.sail | 95 ++++++ model/riscv_clic_type.sail | 36 +++ model/riscv_insts_zicsr.sail | 97 ++++-- model/riscv_next_control.sail | 26 +- model/riscv_platform.sail | 182 ++++++++++- model/riscv_step.sail | 6 +- model/riscv_sys_control.sail | 145 +++++++-- model/riscv_sys_exceptions.sail | 10 +- model/riscv_sys_regs.sail | 4 + model/riscv_types.sail | 3 +- 12 files changed, 1090 insertions(+), 63 deletions(-) create mode 100644 model/riscv_clic_control.sail create mode 100644 model/riscv_clic_mem.sail create mode 100644 model/riscv_clic_regs.sail create mode 100644 model/riscv_clic_type.sail diff --git a/model/riscv_clic_control.sail b/model/riscv_clic_control.sail new file mode 100644 index 000000000..f4ce0a3cf --- /dev/null +++ b/model/riscv_clic_control.sail @@ -0,0 +1,528 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* Functional specification for the 'Smclic' fast interrupts extension. */ +val vector_table_fetch : xlenbits -> VectorTableFetchResult +scattered function vector_table_fetch + +val handle_mem_exception : (xlenbits, ExceptionType) -> unit +scattered function handle_mem_exception + +/* masking for reads to xepc */ +function inhv_pc_alignment_mask() -> xlenbits = + ~(zero_extend(if (sizeof(xlen) == 32) then 0b11 else 0b111)) + +function isClicInterruptPending() -> (bool) = { + var effective_pending : bits(1) = 0b0; + foreach (i from 0 to (4096 - 1)) { + effective_pending = effective_pending | (clicintip[i] & clicintie[i]); + }; + if effective_pending == 0b0 then false else true; +} + +/* Interrupts are prioritized in privilege order, level */ +function findClicPendingInterrupt() -> exc_code = { + + var top_ip_code : exc_code = zero_extend(0b0); + var top_ip_priority : bits(10) = zero_extend(0b0); + + var ip_valid : bits(1) = zero_extend(0b0); + var ip_priority : bits(10) = zero_extend(0b0); + var ip_attr : clicintattr_layout = undefined; + var ip_trig : bits(2) = zero_extend(0b0); + var ip_priv : bits(2) = zero_extend(0b0); + var ip_level : bits(8) = zero_extend(0b0); + var ip_code : exc_code = zero_extend(0b0); + + foreach (i from 0 to (4096 - 1)) { + ip_attr = clicintattr[i]; + ip_trig = zero_extend(ip_attr[TRIG]); + match ip_trig { + 0b00 => if (clicintip_raw[i] == 0b1) then clicintip[i] = 0b1 else clicintip[i] = 0b0, /* 00 - active high */ + 0b10 => if (clicintip_raw[i] == 0b1) then clicintip[i] = 0b0 else clicintip[i] = 0b1, /* 10 - active low */ + 0b01 => if (clicintip_raw[i] == 0b1) & (clicintip_raw_prev[i] == 0b0) then clicintip[i] = 0b1, /* 01 - posedge triggered */ + 0b11 => if (clicintip_raw[i] == 0b0) & (clicintip_raw_prev[i] == 0b1) then clicintip[i] = 0b1 /* 11 - negedge triggered */ + }; + clicintip_raw_prev[i] = clicintip_raw[i]; + + ip_valid = clicintip[i] & clicintie[i]; + ip_priv = zero_extend(ip_attr[MODE]); + ip_level = zero_extend(clicintctl[i]); + ip_priority[9..8] = zero_extend(ip_priv); + ip_priority[7..0] = zero_extend(ip_level); + ip_code = zero_extend(to_bits(8,i)); + if (ip_valid == 0b1) then { + /* if get_config_print_platform() + * then print_platform("pending and enabled interrupt ip_priority " ^BitStr(ip_priority) ^ " ip_code " ^ BitStr(ip_code)); + */ + if (unsigned(ip_priority) >= unsigned(top_ip_priority)) then { + top_ip_priority = ip_priority; + top_ip_code = ip_code; + /* if get_config_print_platform() + * then print_platform("new top_ip_priority " ^BitStr(ip_priority) ^ " ip_code " ^ BitStr(top_ip_code) ^ " mil " ^ BitStr(mil)); + */ + }; + }; + }; + top_ip_code; +} + +/* Given the current privilege level, iterate over privileges to get a + * pending set for an enabled privilege. This is only called for M/U or + * M/S/U systems. + */ +function dispatchClicInterrupt(priv : Privilege) -> option((exc_code, Privilege)) = { + assert(haveUsrMode(), "no user mode: M/U or M/S/U system required"); + + var top_ip_code : exc_code = undefined; + var top_ip_attr : clicintattr_layout = undefined; + var top_ip_priv : Privilege = undefined; + var top_ip_level : ilbits = undefined; + + top_ip_code = findClicPendingInterrupt(); + top_ip_attr = clicintattr[unsigned(top_ip_code)]; + top_ip_priv = privLevel_of_bits(top_ip_attr[MODE]); + top_ip_level = clicintctl[unsigned(top_ip_code)]; + + if isClicInterruptPending() == false then None() /* fast path */ + else { + /* if get_config_print_platform() + * then print_platform("ClicInterruptPending ip_code " ^ BitStr(top_ip_code) ^ "top_ip_level " ^BitStr(top_ip_level)); + */ + + /* Higher privileges than the current one are implicitly enabled, + * while lower privileges are blocked. An unsupported privilege is + * considered blocked. + */ + let mIE = priv != Machine | + (priv == Machine & mstatus[MIE] == 0b1 & (unsigned(top_ip_level) > unsigned(mintthresh))); + let sIE = haveSupMode() & (priv == User | + (priv == Supervisor & mstatus[SIE] == 0b1 & (unsigned(top_ip_level) > unsigned(sintthresh)))); + let uIE = haveNExt() & + (priv == User & mstatus[UIE] == 0b1 & (unsigned(top_ip_level) > unsigned(uintthresh))); + + if (uIE & (top_ip_priv == User) & (unsigned(top_ip_level) > unsigned(uil))) then + let r = (top_ip_code, User) in Some(r) + else if (sIE & (top_ip_priv == Supervisor) & (unsigned(top_ip_level) > unsigned(sil))) then + let r = (top_ip_code, Supervisor) in Some(r) + else if (mIE & (top_ip_priv == Machine) & (unsigned(top_ip_level) > unsigned(mil))) then + let r = (top_ip_code, Machine) in Some(r) + else None() + } +} + +function prepare_shv_clic_trap_vector(p : Privilege, c : exc_code) -> xlenbits = { + var tbase : xlenbits = mtvt; + + match (p) { + Machine => tbase = mtvt, + Supervisor => tbase = stvt, + User => tbase = utvt + }; + + var table_entry_addr : xlenbits = undefined; + table_entry_addr = if sizeof(xlen) == 32 then {tbase + 4*unsigned(c)} else {tbase + 8*unsigned(c)}; + + match vector_table_fetch(table_entry_addr) { + F_TableError(e, table_addr) => {inhv = 0b1; handle_mem_exception(table_entry_addr, e); table_entry_addr}, + F_TableEntry(table_entry) => { + clicintip[unsigned(c)] = 0b0; /* clear clicintip if edge_triggered */ + table_entry + } + } +} + +function init_clicintregs() -> unit = { + inhv = zero_extend(0b0); + mil = zero_extend(0b0); + mpil = zero_extend(0b0); + minhv = zero_extend(0b0); + sil = zero_extend(0b0); + spil = zero_extend(0b0); + sinhv = zero_extend(0b0); + uil = zero_extend(0b0); + spil = zero_extend(0b0); + sinhv = zero_extend(0b0); + + foreach (i from 0 to (4096 - 1)) { + clicintip_raw[i] = 0b0; + clicintip_raw_prev[i] = 0b0; + clicintip[i] = 0b0; + clicintie[i] = 0b0; + clicintctl[i] = zero_extend(0b0); + clicintattr[i] = [clicintattr[i] with MODE = 0b11, TRIG = 0b00, SHV = 0b0]; + }; +} + +val access_nxti_CSR : (csreg, xlenbits, bitvector(5), bool, csrop, bool, Privilege) -> option(xlenbits) +function access_nxti_CSR(csr, rs1_val, rd, is_imm, op, isWrite, priv) -> option(xlenbits) = { + /* nxti only valid for CSRR, CSRRSI, CSRRCI, CSRRS */ + let imm_nxti_writeCSR : bool = isWrite & ((op == CSRRS) | (op == CSRRC)) & is_imm == true; /* CSRRSI, CSRRCI */ + let csrrs_nxti_writeCSR : bool = isWrite & (op == CSRRS) & is_imm == false; /* CSRRS */ + + var pil : ilbits = mpil; + pil = match priv { + Machine => mpil, + Supervisor => spil, + User => upil + }; + + var csr_val : xlenbits = undefined; + csr_val = if (op == CSRRS) then (mstatus.bits & zero_extend(0b11111)) | zero_extend(rs1_val[4..0]) else + (mstatus.bits & zero_extend(0b11111)) & ~(zero_extend(rs1_val[4..0])); + + if (imm_nxti_writeCSR) then csr_val[23..16] = pil else csr_val[23..16] = rs1_val[23..16]; + + if (isWrite == false) then { + ext_read_CSR(csr); + } else if (imm_nxti_writeCSR | csrrs_nxti_writeCSR) then { + ext_write_CSR(csr, csr_val) + } else { + None() + } +} + +/* Smclic CSRs */ + +function clause ext_is_CSR_defined(0x307, _) = haveSmclic() // mtvt +function clause ext_is_CSR_defined(0x345, _) = haveSmclic() // mnxti +function clause ext_is_CSR_defined(0xFB1, _) = haveSmclic() // mintstatus +function clause ext_is_CSR_defined(0x347, _) = haveSmclic() // mintthresh +function clause ext_is_CSR_defined(0x348, _) = haveSmclic() // mscratchcsw +function clause ext_is_CSR_defined(0x349, _) = haveSmclic() // mscratchcswl + +function clause ext_read_CSR(0x307) = Some(mtvt) +function clause ext_read_CSR(0x345) = + if (isClicInterruptPending() == true & haveSmclic()) then { + var top_ip_code : exc_code = undefined; + var top_ip_attr : clicintattr_layout = undefined; + var top_ip_priv : Privilege = undefined; + var top_ip_level : ilbits = undefined; + var level_filter : ilbits = undefined; + + top_ip_code = findClicPendingInterrupt(); + top_ip_attr = clicintattr[unsigned(top_ip_code)]; + top_ip_priv = privLevel_of_bits(top_ip_attr[MODE]); + top_ip_level = clicintctl[unsigned(top_ip_code)]; + level_filter = if (unsigned(mpil) > unsigned(mintthresh)) then mpil else mintthresh; + + /* if get_config_print_platform() + * then print_platform("mnxti rd ip_code " ^BitStr(top_ip_code) ^ " ip_level " ^ BitStr(top_ip_level) ^ " level_filter " ^ BitStr(level_filter)); + */ + + if ((top_ip_priv == Machine) & (unsigned(top_ip_level) > unsigned(level_filter))) then { + let tbase : xlenbits = mtvt; + var table_entry_addr : xlenbits = undefined; + table_entry_addr = if sizeof(xlen) == 32 then {tbase + 4*unsigned(top_ip_code)} else {tbase + 8*unsigned(top_ip_code)}; + Some(table_entry_addr) + } else { + Some(zero_extend(0b0)) + } + } else { + Some(zero_extend(0b0)) + } + +function clause ext_read_CSR(0xFB1) = { + mintstatus.bits = zero_extend(0b0); + mintstatus[mil] = mil; + mintstatus[sil] = sil; + mintstatus[uil] = uil; + Some(mintstatus.bits); +} +function clause ext_read_CSR(0x347) = Some(zero_extend(mintthresh)) +function clause ext_read_CSR(0x348) = None() /* accessing with rs1 set to x0 is reserved */ +function clause ext_read_CSR(0x349) = None() /* accessing with rs1 set to x0 is reserved */ + +function clause ext_write_CSR(0x307, value) = { mtvt = value; Some(mtvt) } +function clause ext_write_CSR(0x345, value) = { + + /* In CLINT mode, reads of xnxti return 0, updates to xstatus proceed as in CLIC mode, but updates to + * xintstatus and xcause do not take effect. */ + /*if (haveSmclic()) then { */ + /* Performed regardless of interrupt readiness */ + clicmstatus.bits = value; + mstatus[MIE] = clicmstatus[MIE]; + mstatus[SIE] = clicmstatus[SIE]; + mstatus[UIE] = clicmstatus[UIE]; + /* }; */ + + if (isClicInterruptPending() == true & haveSmclic()) then { + var top_ip_code : exc_code = undefined; + var top_ip_attr : clicintattr_layout = undefined; + var top_ip_priv : Privilege = undefined; + var top_ip_level : ilbits = undefined; + var level_filter : ilbits = undefined; + var value_or_pil : ilbits = undefined; + + top_ip_code = findClicPendingInterrupt(); + top_ip_attr = clicintattr[unsigned(top_ip_code)]; + top_ip_priv = privLevel_of_bits(top_ip_attr[MODE]); + top_ip_level = clicintctl[unsigned(top_ip_code)]; + value_or_pil = value[23..16]; /* Note: access_nxti_CSR passes pil in value[23..16] for CSRRSI/CSRRCI, but rs1[23..16] for CSRRS */ + level_filter = if (unsigned(value_or_pil) > unsigned(mintthresh)) then value_or_pil else mintthresh; + + + /* if get_config_print_platform() + * then print_platform("mnxti wr ip_code " ^BitStr(top_ip_code) ^ " ip_level " ^ BitStr(top_ip_level) ^ " level_filter " ^ BitStr(level_filter) ^ " value_or_pil " ^ BitStr(value_or_pil) ^ " mpil " ^ BitStr(mpil)); + */ + if ((top_ip_priv == Machine) & (unsigned(top_ip_level) > unsigned(level_filter)) ) then { + if (value[4..0] != 0b00000) then { + mil = top_ip_level; + + mcause[Cause] = zero_extend(top_ip_code); + mcause[IsInterrupt] = 0b1; + clicintip[unsigned(top_ip_code)] = 0b0; /* clear clicintip if edge_triggered */ + }; + let tbase : xlenbits = mtvt; + var table_entry_addr : xlenbits = undefined; + table_entry_addr = if sizeof(xlen) == 32 then {tbase + 4*unsigned(top_ip_code)} else {tbase + 8*unsigned(top_ip_code)}; + Some(table_entry_addr) + } else { + Some(zero_extend(0b0)) + } + } else { + Some(zero_extend(0b0)) + } +} + +function clause ext_write_CSR(0x347, value) = { mintthresh = value[7..0]; Some(zero_extend(mintthresh)) } +function clause ext_write_CSR(0x348, value) = { + var rd_value : xlenbits = zero_extend(0b0); + if (privLevel_of_bits(mstatus[MPP]) == Machine) then { + Some(value) + } else { + rd_value = mscratch; + mscratch = value; + Some(rd_value) + } +} +function clause ext_write_CSR(0x349, value) = { + var rd_value : xlenbits = zero_extend(0b0); + if ((mpil==zero_extend(0b0)) != (mil == zero_extend(0b0))) then { + rd_value = mscratch; + mscratch = value; + Some(rd_value) + } else { + Some(value) + } +} + +/* Ssclic CSRs */ + +function clause ext_is_CSR_defined(0x107, _) = haveSmclic() & haveSupMode() // stvt +function clause ext_is_CSR_defined(0x145, _) = haveSmclic() & haveSupMode() // snxti +function clause ext_is_CSR_defined(0xDB1, _) = haveSmclic() & haveSupMode() // sintstatus +function clause ext_is_CSR_defined(0x147, _) = haveSmclic() & haveSupMode() // sintthresh +function clause ext_is_CSR_defined(0x148, _) = haveSmclic() & haveSupMode() // sscratchcsw +function clause ext_is_CSR_defined(0x149, _) = haveSmclic() & haveSupMode() // sscratchcswl + +function clause ext_read_CSR(0x107) = Some(stvt) +function clause ext_read_CSR(0x145) = + if (isClicInterruptPending() == true & haveSmclic()) then { + var top_ip_code : exc_code = undefined; + var top_ip_attr : clicintattr_layout = undefined; + var top_ip_priv : Privilege = undefined; + var top_ip_level : ilbits = undefined; + var level_filter : ilbits = undefined; + + top_ip_code = findClicPendingInterrupt(); + top_ip_attr = clicintattr[unsigned(top_ip_code)]; + top_ip_priv = privLevel_of_bits(top_ip_attr[MODE]); + top_ip_level = clicintctl[unsigned(top_ip_code)]; + level_filter = if (unsigned(spil) > unsigned(sintthresh)) then spil else sintthresh; + + if ((top_ip_priv == Supervisor) & (unsigned(top_ip_level) > unsigned(level_filter))) then { + let tbase : xlenbits = stvt; + var table_entry_addr : xlenbits = undefined; + table_entry_addr = if sizeof(xlen) == 32 then {tbase + 4*unsigned(top_ip_code)} else {tbase + 8*unsigned(top_ip_code)}; + Some(table_entry_addr) + } else { + Some(zero_extend(0b0)) + } + } else { + Some(zero_extend(0b0)) + } + +function clause ext_read_CSR(0xDB1) = { + mintstatus.bits = zero_extend(0b0); + mintstatus[sil] = sil; + mintstatus[uil] = uil; + Some(mintstatus.bits); +} +function clause ext_read_CSR(0x147) = Some(zero_extend(sintthresh)) +function clause ext_read_CSR(0x148) = None() /* accessing with rs1 set to x0 is reserved */ +function clause ext_read_CSR(0x149) = None() /* accessing with rs1 set to x0 is reserved */ + +function clause ext_write_CSR(0x107, value) = { stvt = value; Some(stvt) } +function clause ext_write_CSR(0x145, value) = { + /* In CLINT mode, reads of xnxti return 0, updates to xstatus proceed as in CLIC mode, but updates to + * xintstatus and xcause do not take effect. */ + /*if (haveSmclic()) then { */ + /* Performed regardless of interrupt readiness */ + clicmstatus.bits = value; + mstatus[SIE] = clicmstatus[SIE]; + mstatus[UIE] = clicmstatus[UIE]; + /* }; */ + + if (isClicInterruptPending() == true & haveSmclic()) then { + var top_ip_code : exc_code = undefined; + var top_ip_attr : clicintattr_layout = undefined; + var top_ip_priv : Privilege = undefined; + var top_ip_level : ilbits = undefined; + var level_filter : ilbits = undefined; + + top_ip_code = findClicPendingInterrupt(); + top_ip_attr = clicintattr[unsigned(top_ip_code)]; + top_ip_priv = privLevel_of_bits(top_ip_attr[MODE]); + top_ip_level = clicintctl[unsigned(top_ip_code)]; + level_filter = if (unsigned(value[23..16]) > unsigned(sintthresh)) then value[23..16] else sintthresh; + /* Note: value[23..16] is pil for CSRRSI/CSRRCI, it is rs1[23..16] for CSRRS */ + + /* if get_config_print_platform() + * then print_platform("snxti wr ip_code " ^BitStr(top_ip_code) ^ " ip_level " ^ BitStr(top_ip_level) ^ " level_filter " ^ BitStr(level_filter)); + */ + if ((top_ip_priv == Supervisor) & (unsigned(top_ip_level) > unsigned(level_filter)) ) then { + if (value[4..0] != 0b00000) then { + sil = top_ip_level; + + scause[Cause] = zero_extend(top_ip_code); + scause[IsInterrupt] = 0b1; + clicintip[unsigned(top_ip_code)] = 0b0; /* clear clicintip if edge_triggered */ + }; + let tbase : xlenbits = stvt; + var table_entry_addr : xlenbits = undefined; + table_entry_addr = if sizeof(xlen) == 32 then {tbase + 4*unsigned(top_ip_code)} else {tbase + 8*unsigned(top_ip_code)}; + Some(table_entry_addr) + } else { + Some(zero_extend(0b0)) + } + } else { + Some(zero_extend(0b0)) + } +} + +function clause ext_write_CSR(0x147, value) = { sintthresh = value[7..0]; Some(zero_extend(sintthresh)) } +function clause ext_write_CSR(0x148, value) = { + var rd_value : xlenbits = zero_extend(0b0); + if ((cur_privilege == Supervisor) & (privLevel_of_bits(mstatus[MPP]) == Supervisor)) then { + Some(value) + } else { + rd_value = sscratch; + sscratch = value; + Some(rd_value) + } +} +function clause ext_write_CSR(0x149, value) = { + var rd_value : xlenbits = zero_extend(0b0); + if ((spil==zero_extend(0b0)) != (sil == zero_extend(0b0))) then { + rd_value = sscratch; + sscratch = value; + Some(rd_value) + } else { + Some(value) + } +} + +/* Suclic CSRs */ + +function clause ext_is_CSR_defined(0x007, _) = haveSmclic() & haveNExt() // utvt +function clause ext_is_CSR_defined(0x045, _) = haveSmclic() & haveNExt() // unxti +function clause ext_is_CSR_defined(0xCB1, _) = haveSmclic() & haveNExt() // uintstatus +function clause ext_is_CSR_defined(0x047, _) = haveSmclic() & haveNExt() // uintthresh +function clause ext_is_CSR_defined(0x049, _) = haveSmclic() & haveNExt() // uscratchcswl + +function clause ext_read_CSR(0x007) = Some(utvt) +function clause ext_read_CSR(0x045) = + if (isClicInterruptPending() == true & haveSmclic()) then { + var top_ip_code : exc_code = undefined; + var top_ip_attr : clicintattr_layout = undefined; + var top_ip_priv : Privilege = undefined; + var top_ip_level : ilbits = undefined; + var level_filter : ilbits = undefined; + + top_ip_code = findClicPendingInterrupt(); + top_ip_attr = clicintattr[unsigned(top_ip_code)]; + top_ip_priv = privLevel_of_bits(top_ip_attr[MODE]); + top_ip_level = clicintctl[unsigned(top_ip_code)]; + level_filter = if (unsigned(upil) > unsigned(uintthresh)) then upil else uintthresh; + + if ((top_ip_priv == User) & (unsigned(top_ip_level) > unsigned(level_filter))) then { + let tbase : xlenbits = utvt; + var table_entry_addr : xlenbits = undefined; + table_entry_addr = if sizeof(xlen) == 32 then {tbase + 4*unsigned(top_ip_code)} else {tbase + 8*unsigned(top_ip_code)}; + Some(table_entry_addr) + } else { + Some(zero_extend(0b0)) + } + } else { + Some(zero_extend(0b0)) + } + +function clause ext_read_CSR(0xCB1) = { + mintstatus.bits = zero_extend(0b0); + mintstatus[uil] = uil; + Some(mintstatus.bits); +} +function clause ext_read_CSR(0x047) = Some(zero_extend(uintthresh)) +function clause ext_read_CSR(0x049) = None() /* accessing with rs1 set to x0 is reserved */ + +function clause ext_write_CSR(0x007, value) = { utvt = value; Some(utvt) } +function clause ext_write_CSR(0x045, value) = { +/* In CLINT mode, reads of xnxti return 0, updates to xstatus proceed as in CLIC mode, but updates to + * xintstatus and xcause do not take effect. */ + /*if (haveSmclic()) then { */ + /* Performed regardless of interrupt readiness */ + clicmstatus.bits = value; + mstatus[UIE] = clicmstatus[UIE]; + /* }; */ + + if (isClicInterruptPending() == true & haveSmclic()) then { + var top_ip_code : exc_code = undefined; + var top_ip_attr : clicintattr_layout = undefined; + var top_ip_priv : Privilege = undefined; + var top_ip_level : ilbits = undefined; + var level_filter : ilbits = undefined; + + top_ip_code = findClicPendingInterrupt(); + top_ip_attr = clicintattr[unsigned(top_ip_code)]; + top_ip_priv = privLevel_of_bits(top_ip_attr[MODE]); + top_ip_level = clicintctl[unsigned(top_ip_code)]; + level_filter = if (unsigned(value[23..16]) > unsigned(uintthresh)) then value[23..16] else uintthresh; + /* Note: value[23..16] is pil for CSRRSI/CSRRCI, it is rs1[23..16] for CSRRS */ + + if ((top_ip_priv == User) & (unsigned(top_ip_level) > unsigned(level_filter)) ) then { + if (value[4..0] != 0b00000) then { + uil = top_ip_level; + + ucause[Cause] = zero_extend(top_ip_code); + ucause[IsInterrupt] = 0b1; + clicintip[unsigned(top_ip_code)] = 0b0; /* clear clicintip if edge_triggered */ + }; + let tbase : xlenbits = utvt; + var table_entry_addr : xlenbits = undefined; + table_entry_addr = if sizeof(xlen) == 32 then {tbase + 4*unsigned(top_ip_code)} else {tbase + 8*unsigned(top_ip_code)}; + Some(table_entry_addr) + } else { + Some(zero_extend(0b0)) + } + } else { + Some(zero_extend(0b0)) + } +} + +function clause ext_write_CSR(0x047, value) = { uintthresh = value[7..0]; Some(zero_extend(uintthresh)) } +function clause ext_write_CSR(0x049, value) = { + var rd_value : xlenbits = zero_extend(0b0); + if ((upil==zero_extend(0b0)) != (uil == zero_extend(0b0))) then { + rd_value = uscratch; + uscratch = value; + Some(rd_value) + } else { + Some(value) + } +} diff --git a/model/riscv_clic_mem.sail b/model/riscv_clic_mem.sail new file mode 100644 index 000000000..f0a2446b4 --- /dev/null +++ b/model/riscv_clic_mem.sail @@ -0,0 +1,21 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +val vector_table_fetch : xlenbits -> VectorTableFetchResult +function vector_table_fetch(table_addr) -> VectorTableFetchResult = + if sizeof(xlen) == 32 then { + match mem_read(Execute(), table_addr, 4, false, false, false) { + MemException(e) => F_TableError(e, table_addr), + MemValue(table_entry) => F_TableEntry(table_entry) + } + } else { /* xlen == 64 */ + match mem_read(Execute(), table_addr, 8, false, false, false) { + MemException(e) => F_TableError(e, table_addr), + MemValue(table_entry) => F_TableEntry(table_entry) + } + } diff --git a/model/riscv_clic_regs.sail b/model/riscv_clic_regs.sail new file mode 100644 index 000000000..2f6dbcd83 --- /dev/null +++ b/model/riscv_clic_regs.sail @@ -0,0 +1,95 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* Architectural state for the 'Smclic' fast interrupts extension. */ + +/* Smclic csrs */ +mapping clause csr_name_map = 0x307 <-> "mtvt" +mapping clause csr_name_map = 0x345 <-> "mnxti" +mapping clause csr_name_map = 0xFB1 <-> "mintstatus" +mapping clause csr_name_map = 0x347 <-> "mintthresh" +mapping clause csr_name_map = 0x348 <-> "mscratchcsw" +mapping clause csr_name_map = 0x349 <-> "mscratchcswl" +/* Ssclic csrs */ +mapping clause csr_name_map = 0x107 <-> "stvt" +mapping clause csr_name_map = 0x145 <-> "snxti" +mapping clause csr_name_map = 0xDB1 <-> "sintstatus" +mapping clause csr_name_map = 0x147 <-> "sintthresh" +mapping clause csr_name_map = 0x148 <-> "sscratchcsw" +mapping clause csr_name_map = 0x149 <-> "sscratchcswl" +/* Suclic csrs */ +mapping clause csr_name_map = 0x107 <-> "utvt" +mapping clause csr_name_map = 0x145 <-> "unxti" +mapping clause csr_name_map = 0xDB1 <-> "uintstatus" +mapping clause csr_name_map = 0x147 <-> "uintthresh" +mapping clause csr_name_map = 0x148 <-> "sscratchcsw" +mapping clause csr_name_map = 0x149 <-> "sscratchcswl" + +register inhv : bits(1) /* internal state of accessing vector table, exception handler will decide which xinhv to set */ + +register mtvt : xlenbits +register mintthresh : ilbits +register mil : ilbits +register mpil : ilbits +register minhv : bits(1) + +register stvt : xlenbits +register sintthresh : ilbits +register sil : ilbits +register spil : ilbits +register sinhv : bits(1) + +register utvt : xlenbits +register uintthresh : ilbits +register uil : ilbits +register upil : ilbits +register uinhv : bits(1) + +register clicintip_raw : vector(4096, dec, bits(1)) +register clicintip_raw_prev : vector(4096, dec, bits(1)) +register clicintip : vector(4096, dec, bits(1)) +register clicintie : vector(4096, dec, bits(1)) +register clicintctl : vector(4096, dec, ilbits) +register clicintattr : vector(4096, dec, clicintattr_layout) + +bitfield ClicMcause : xlenbits = { + IsInterrupt : xlen - 1, + Minhv : 30, + ClicMcauseMpp : 29 .. 28, + ClicMcauseMpie: 27, + Mpil : 23 .. 16, + Exccode : 11 .. 0 +} +register clicmcause : ClicMcause +register clicmstatus : Mstatus + +bitfield ClicScause : xlenbits = { + IsInterrupt : xlen - 1, + Sinhv : 30, + ClicScauseSpp : 28, + ClicScauseSpie: 27, + Spil : 23 .. 16, + Exccode : 11 .. 0 +} +register clicscause : ClicScause + +bitfield ClicUcause : xlenbits = { + IsInterrupt : xlen - 1, + Uinhv : 30, + ClicUcauseUpie: 27, + Upil : 23 .. 16, + Exccode : 11 .. 0 +} +register clicucause : ClicUcause + +bitfield Mintstatus : xlenbits = { + mil : 31 .. 24, + sil : 15 .. 8, + uil : 7 .. 0 +} +register mintstatus : Mintstatus diff --git a/model/riscv_clic_type.sail b/model/riscv_clic_type.sail new file mode 100644 index 000000000..def917e40 --- /dev/null +++ b/model/riscv_clic_type.sail @@ -0,0 +1,36 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* Definitions for fast interrupt (Smclic extensions) */ + +/* default register type */ +type ilbits = bits(8) + +bitfield clicintattr_layout : bits(8) = { + MODE : 7 .. 6, /* privilege mode */ + TRIG : 2 .. 1, /* 11 - negedge triggered */ + /* 10 - active low */ + /* 01 - posedge triggered */ + /* 00 - active high */ + SHV : 0 /* hardware vectored interrupt */ +} + +val is_shv : bitvector(1) -> bool +function is_shv (shv) = + match (shv) { + 0b0 => false, + 0b1 => true + } + +let CLIC_MTI = 7 +let CLIC_MSI = 3 + +union VectorTableFetchResult = { + F_TableEntry : xlenbits, /* Entry in vector table */ + F_TableError : (ExceptionType, xlenbits) /* standard exception and table entry addr */ +} diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index ef9e73e11..1b0c9bcd3 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -33,7 +33,7 @@ function readCSR csr : csreg -> xlenbits = { (0x301, _) => misa.bits, (0x302, _) => medeleg.bits, (0x303, _) => mideleg.bits, - (0x304, _) => mie.bits, + (0x304, _) => if haveSmclic() then { zero_extend(0b0) } else mie.bits, (0x305, _) => get_mtvec(), (0x306, _) => zero_extend(mcounteren.bits), (0x30A, _) => menvcfg.bits[sizeof(xlen) - 1 .. 0], @@ -43,9 +43,17 @@ function readCSR csr : csreg -> xlenbits = { (0x340, _) => mscratch, (0x341, _) => get_xret_target(Machine) & pc_alignment_mask(), - (0x342, _) => mcause.bits, + (0x342, _) => if haveSmclic() then { + clicmcause.bits = mcause.bits; + clicmcause[Minhv] = minhv; + clicmcause[ClicMcauseMpp] = mstatus[MPP]; + clicmcause[ClicMcauseMpie] = mstatus[MPIE]; + clicmcause[Mpil] = mpil; + clicmcause.bits + } else + mcause.bits, (0x343, _) => mtval, - (0x344, _) => mip.bits, + (0x344, _) => if haveSmclic() then { zero_extend(0b0) } else mip.bits, // pmpcfgN (0x3A @ idx : bits(4), _) if idx[0] == bitzero | sizeof(xlen) == 32 => pmpReadCfgReg(unsigned(idx)), @@ -77,15 +85,23 @@ function readCSR csr : csreg -> xlenbits = { (0x100, _) => lower_mstatus(mstatus).bits, (0x102, _) => sedeleg.bits, (0x103, _) => sideleg.bits, - (0x104, _) => lower_mie(mie, mideleg).bits, + (0x104, _) => if haveSmclic() then { zero_extend(0b0) } else lower_mie(mie, mideleg).bits, (0x105, _) => get_stvec(), (0x106, _) => zero_extend(scounteren.bits), (0x10A, _) => senvcfg.bits[sizeof(xlen) - 1 .. 0], (0x140, _) => sscratch, (0x141, _) => get_xret_target(Supervisor) & pc_alignment_mask(), - (0x142, _) => scause.bits, + (0x142, _) => if haveSmclic() then { + clicscause.bits = scause.bits; + clicscause[Sinhv] = sinhv; + clicscause[ClicScauseSpp] = mstatus[SPP]; + clicscause[ClicScauseSpie] = mstatus[SPIE]; + clicscause[Spil] = mpil; + clicscause.bits + } else + scause.bits, (0x143, _) => stval, - (0x144, _) => lower_mip(mip, mideleg).bits, + (0x144, _) => if haveSmclic() then { zero_extend(0b0) } else lower_mip(mip, mideleg).bits, (0x180, _) => satp, /* user mode counters */ @@ -119,7 +135,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x301, _) => { misa = legalize_misa(misa, value); Some(misa.bits) }, (0x302, _) => { medeleg = legalize_medeleg(medeleg, value); Some(medeleg.bits) }, (0x303, _) => { mideleg = legalize_mideleg(mideleg, value); Some(mideleg.bits) }, - (0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits) }, + (0x304, _) => { if haveSmclic() then { mie = mie; Some(mie.bits) } else { mie = legalize_mie(mie, value); Some(mie.bits) } }, (0x305, _) => { Some(set_mtvec(value)) }, (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits)) }, (0x30A, 32) => { menvcfg = legalize_envcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); Some(menvcfg.bits[31 .. 0]) }, @@ -129,9 +145,19 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits)) }, (0x340, _) => { mscratch = value; Some(mscratch) }, (0x341, _) => { Some(set_xret_target(Machine, value)) }, - (0x342, _) => { mcause.bits = value; Some(mcause.bits) }, + (0x342, _) => { if haveSmclic() then { + clicmcause.bits = value; + minhv = clicmcause[Minhv]; + mstatus[MPP] = clicmcause[ClicMcauseMpp]; + mstatus[MPIE] = clicmcause[ClicMcauseMpie]; + mpil = clicmcause[Mpil]; + Some(clicmcause.bits) + } else { + mcause.bits = value; Some(mcause.bits) + } + }, (0x343, _) => { mtval = value; Some(mtval) }, - (0x344, _) => { mip = legalize_mip(mip, value); Some(mip.bits) }, + (0x344, _) => { if haveSmclic() then { mip = mip; Some(mip.bits) } else { mip = legalize_mip(mip, value); Some(mip.bits) } }, // pmpcfgN (0x3A @ idx : bits(4), _) if idx[0] == bitzero | sizeof(xlen) == 32 => { @@ -158,15 +184,25 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x100, _) => { mstatus = legalize_sstatus(mstatus, value); Some(mstatus.bits) }, (0x102, _) => { sedeleg = legalize_sedeleg(sedeleg, value); Some(sedeleg.bits) }, (0x103, _) => { sideleg.bits = value; Some(sideleg.bits) }, /* TODO: does this need legalization? */ - (0x104, _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits) }, + (0x104, _) => { if haveSmclic() then { mie = mie; Some(mie.bits) } else { mie = legalize_sie(mie, mideleg, value); Some(mie.bits) } }, (0x105, _) => { Some(set_stvec(value)) }, (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits)) }, (0x10A, _) => { senvcfg = legalize_envcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits[sizeof(xlen) - 1 .. 0]) }, (0x140, _) => { sscratch = value; Some(sscratch) }, (0x141, _) => { Some(set_xret_target(Supervisor, value)) }, - (0x142, _) => { scause.bits = value; Some(scause.bits) }, + (0x142, _) => { if haveSmclic() then { + clicscause.bits = value; + sinhv = clicscause[Sinhv]; + mstatus[SPP] = clicscause[ClicScauseSpp]; + mstatus[SPIE] = clicscause[ClicScauseSpie]; + spil = clicscause[Spil]; + Some(clicscause.bits) + } else { + scause.bits = value; Some(scause.bits) + } + }, (0x143, _) => { stval = value; Some(stval) }, - (0x144, _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits) }, + (0x144, _) => { if haveSmclic() then { mip = mip; Some(mip.bits) } else { mip = legalize_sip(mip, mideleg, value); Some(mip.bits) } }, (0x180, _) => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) }, /* user mode: seed (entropy source). writes are ignored */ @@ -201,17 +237,32 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = { else if not(ext_check_CSR(csr, cur_privilege, isWrite)) then { ext_check_CSR_fail(); RETIRE_FAIL } else { - let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */ - if isWrite then { - let new_val : xlenbits = match op { - CSRRW => rs1_val, - CSRRS => csr_val | rs1_val, - CSRRC => csr_val & ~(rs1_val) - }; - writeCSR(csr, new_val) - }; - X(rd) = csr_val; - RETIRE_SUCCESS + let cond_writeCSR : bool = isWrite & (op == CSRRW) & is_imm == false; + match (csr, sizeof(xlen)) { + /* special conditional write CSRs, CSRRS/C/I/read behavior reserved */ + (0x348, _) => {if cond_writeCSR then {match ext_write_CSR(csr, rs1_val) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};}else{ext_check_CSR_fail(); RETIRE_FAIL}}, + (0x349, _) => {if cond_writeCSR then {match ext_write_CSR(csr, rs1_val) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};}else{ext_check_CSR_fail(); RETIRE_FAIL}}, + (0x148, _) => {if cond_writeCSR then {match ext_write_CSR(csr, rs1_val) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};}else{ext_check_CSR_fail(); RETIRE_FAIL}}, + (0x149, _) => {if cond_writeCSR then {match ext_write_CSR(csr, rs1_val) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};}else{ext_check_CSR_fail(); RETIRE_FAIL}}, + (0x049, _) => {if cond_writeCSR then {match ext_write_CSR(csr, rs1_val) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};}else{ext_check_CSR_fail(); RETIRE_FAIL}}, + /* special Smclic nxti CSRs */ + (0x345, _) => {match access_nxti_CSR(csr, rs1_val, rd, is_imm, op, isWrite, Machine) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};}, + (0x145, _) => {match access_nxti_CSR(csr, rs1_val, rd, is_imm, op, isWrite, Supervisor) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};}, + (0x045, _) => {match access_nxti_CSR(csr, rs1_val, rd, is_imm, op, isWrite, User) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};}, + _ => { /* standard CSRs */ + let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */ + if isWrite then { + let new_val : xlenbits = match op { + CSRRW => rs1_val, + CSRRS => csr_val | rs1_val, + CSRRC => csr_val & ~(rs1_val) + }; + writeCSR(csr, new_val) + }; + X(rd) = csr_val; + RETIRE_SUCCESS + } + } } } diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail index 688d16d72..0e1220e5b 100644 --- a/model/riscv_next_control.sail +++ b/model/riscv_next_control.sail @@ -18,13 +18,21 @@ function clause ext_is_CSR_defined(0x043, _) = haveUsrMode() & haveNExt() // utv function clause ext_is_CSR_defined(0x044, _) = haveUsrMode() & haveNExt() // uip function clause ext_read_CSR(0x000) = Some(lower_sstatus(lower_mstatus(mstatus)).bits) -function clause ext_read_CSR(0x004) = Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits) +function clause ext_read_CSR(0x004) = if haveSmclic() then { Some(zero_extend(0b0)) } else Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits) function clause ext_read_CSR(0x005) = Some(get_utvec()) function clause ext_read_CSR(0x040) = Some(uscratch) function clause ext_read_CSR(0x041) = Some(get_xret_target(User) & pc_alignment_mask()) -function clause ext_read_CSR(0x042) = Some(ucause.bits) +function clause ext_read_CSR(0x042) = if haveSmclic() then { + clicucause.bits = ucause.bits; + clicucause[Uinhv] = uinhv; + clicucause[ClicUcauseUpie] = mstatus[UPIE]; + clicucause[Upil] = upil; + Some(clicucause.bits) + } else + Some(ucause.bits) + function clause ext_read_CSR(0x043) = Some(utval) -function clause ext_read_CSR(0x044) = Some(lower_sip(lower_mip(mip, mideleg), sideleg).bits) +function clause ext_read_CSR(0x044) = if haveSmclic() then { Some(zero_extend(0b0)) } else Some(lower_sip(lower_mip(mip, mideleg), sideleg).bits) function clause ext_write_CSR(0x000, value) = { mstatus = legalize_ustatus(mstatus, value); Some(mstatus.bits) } function clause ext_write_CSR(0x004, value) = { let sie = legalize_uie(lower_mie(mie, mideleg), sideleg, value); @@ -33,7 +41,17 @@ function clause ext_write_CSR(0x004, value) = { let sie = legalize_uie(lower_mie function clause ext_write_CSR(0x005, value) = { Some(set_utvec(value)) } function clause ext_write_CSR(0x040, value) = { uscratch = value; Some(uscratch) } function clause ext_write_CSR(0x041, value) = { Some(set_xret_target(User, value)) } -function clause ext_write_CSR(0x042, value) = { ucause.bits = value; Some(ucause.bits) } +function clause ext_write_CSR(0x042, value) = { if haveSmclic() then { + clicucause.bits = value; + uinhv = clicucause[Uinhv]; + mstatus[UPIE] = clicucause[ClicUcauseUpie]; + upil = clicucause[Upil]; + Some(clicucause.bits) + } else { + ucause.bits = value; Some(ucause.bits) + } + } + function clause ext_write_CSR(0x043, value) = { utval = value; Some(utval) } function clause ext_write_CSR(0x044, value) = { let sip = legalize_uip(lower_mip(mip, mideleg), sideleg, value); mip = lift_sip(mip, mideleg, sip); diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 9f38090a6..279dd4b10 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -58,6 +58,10 @@ val plat_rom_size = {ocaml: "Platform.rom_size", interpreter: "Platform.rom_si val plat_clint_base = {ocaml: "Platform.clint_base", interpreter: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits val plat_clint_size = {ocaml: "Platform.clint_size", interpreter: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits +/* Location of clic memory mapped registers */ +val plat_clic_base = {ocaml: "Platform.clic_base", interpreter: "Platform.clic_base", c: "plat_clic_base", lem: "plat_clic_base"} : unit -> xlenbits +val plat_clic_size = {ocaml: "Platform.clic_size", interpreter: "Platform.clic_size", c: "plat_clic_size", lem: "plat_clic_size"} : unit -> xlenbits + /* Location of HTIF ports */ val plat_htif_tohost = {ocaml: "Platform.htif_tohost", c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits function plat_htif_tohost () = to_bits(sizeof(xlen), elf_tohost ()) @@ -111,6 +115,18 @@ function within_clint forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, wi & (addr_int + sizeof('n)) <= (clint_base_int + clint_size_int) } +function within_clic forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = { + /* To avoid overflow issues when physical memory extends to the end + * of the addressable range, we need to perform address bound checks + * on unsigned unbounded integers. + */ + let addr_int = unsigned(addr); + let clic_base_int = unsigned(plat_clic_base ()); + let clic_size_int = unsigned(plat_clic_size ()); + clic_base_int <= addr_int + & (addr_int + sizeof('n)) <= (clic_base_int + clic_size_int) +} + function within_htif_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = plat_htif_tohost() == addr | (plat_htif_tohost() + 4 == addr & width == 4) @@ -208,10 +224,14 @@ function clint_dispatch() -> unit = { if get_config_print_platform() then print_platform("clint::tick mtime <- " ^ BitStr(mtime)); mip[MTI] = 0b0; + clicintip_raw[CLIC_MTI] = 0b0; if mtimecmp <=_u mtime then { if get_config_print_platform() then print_platform(" clint timer pending at mtime " ^ BitStr(mtime)); - mip[MTI] = 0b1 + mip[MTI] = 0b1; + clicintip_raw[CLIC_MTI] = 0b1; + if get_config_print_platform() + then print_platform(" clicintip[MTI] pending " ^ BitStr(clicintip[CLIC_MTI]) ^ " clicintip_raw[MTI] pending " ^ BitStr(clicintip_raw[CLIC_MTI])) } } @@ -223,6 +243,7 @@ function clint_store(addr, width, data) = { if get_config_print_platform() then print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mip.MSI <- " ^ BitStr(data[0]) ^ ")"); mip[MSI] = [data[0]]; + clicintip_raw[CLIC_MSI] = [data[0]]; clint_dispatch(); MemValue(true) } else if addr == MTIMECMP_BASE & 'n == 8 then { @@ -259,6 +280,157 @@ function tick_clock() = { clint_dispatch() } +/* CLIC memory-mapped IO */ + +/* relative address map: + * + * 100C clicint[3] -- connected to CLINT MSI software interrupt + * 101C clicint[7] -- connected to CLINT MTI timer interrupt + * no other clicint regs currently implemented + */ + +let CLIC_MSI_BASE : xlenbits = zero_extend(0x0100C) +let CLIC_MTI_BASE : xlenbits = zero_extend(0x0101C) + + + +val clic_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) +function clic_load(t, addr, width) = { + var clicint : bits(32) = undefined; + var ip_ip : bits(1) = undefined; + var ip_ie : bits(1) = undefined; + var ip_attr_layout : clicintattr_layout = undefined; + var ip_attr : bits(8) = undefined; + var ip_ctl : ilbits = undefined; + + let addr = addr - plat_clic_base (); + /* FIXME: For now, only allow exact aligned access. */ + if addr == CLIC_MSI_BASE & ('n == 4) + then { + ip_ip = clicintip[CLIC_MSI]; + ip_ie = clicintie[CLIC_MSI]; + ip_attr_layout = clicintattr[CLIC_MSI]; + ip_attr = zero_extend(shiftl(ip_attr_layout[MODE],6)) | + zero_extend(shiftl(ip_attr_layout[TRIG],1)) | + zero_extend(ip_attr_layout[SHV]); + ip_ctl = clicintctl[CLIC_MSI]; + clicint = zero_extend(shiftl(ip_ctl,24)) | + zero_extend(shiftl(ip_attr,16)) | + zero_extend(shiftl(ip_ie,8)) | + zero_extend(ip_ip); + if get_config_print_platform() + then print_platform("clic[" ^ BitStr(addr) ^ "] -> " ^ BitStr(clicint)); + MemValue(sail_zero_extend(clicint[31..0], 32)) + } + else if addr == CLIC_MTI_BASE & ('n == 4) + then { + ip_ip = clicintip[CLIC_MTI]; + ip_ie = clicintie[CLIC_MTI]; + ip_attr_layout = clicintattr[CLIC_MSI]; + ip_attr = zero_extend(shiftl(ip_attr_layout[MODE],6)) | + zero_extend(shiftl(ip_attr_layout[TRIG],1)) | + zero_extend(ip_attr_layout[SHV]); + ip_ctl = clicintctl[CLIC_MTI]; + clicint = zero_extend(shiftl(ip_ctl,24)) | + zero_extend(shiftl(ip_attr,16)) | + zero_extend(shiftl(ip_ie,8)) | + zero_extend(ip_ip); + if get_config_print_platform() + then print_platform("clic[" ^ BitStr(addr) ^ "] -> " ^ BitStr(clicint)); + MemValue(sail_zero_extend(clicint[31..0], 32)) + } + else { + if get_config_print_platform() + then print_platform("clic[" ^ BitStr(addr) ^ "] -> "); + MemValue( sail_zero_extend(0b0, sizeof(8 * 'n))) + } +} + +val clic_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) +function clic_store(addr, width, data) = { + var ip_attr_layout : clicintattr_layout = undefined; + var ip_attr : bits(8) = undefined; + var ip_shv : bits(1) = undefined; + let addr = addr - plat_clic_base (); + /* FIXME: For now, only allow word or byte access. */ + if addr == CLIC_MSI_BASE & ('n == 4) then { + if get_config_print_platform() + then print_platform("clic[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (clicintip.MSI <- " ^ BitStr(data[0]) ^ ")"); + clicintip[CLIC_MSI] = [data[0]]; + clicintie[CLIC_MSI] = [data[8]]; + ip_attr = zero_extend(data[23..16]); + ip_attr_layout[MODE] = zero_extend(ip_attr[7..6]); + ip_attr_layout[TRIG] = zero_extend(ip_attr[2..1]); + if bit_to_bool(ip_attr[0]) then ip_shv = 0b1 else ip_shv = 0b0; + ip_attr_layout[SHV] = ip_shv; + clicintattr[CLIC_MSI] = ip_attr_layout; + clicintctl[CLIC_MSI] = zero_extend(data[31..24]); + MemValue(true) + } else if addr == CLIC_MSI_BASE & ('n == 1) then { + if get_config_print_platform() + then print_platform("clic[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (clicintip.MSI <- " ^ BitStr(data[0]) ^ ")"); + clicintip[CLIC_MSI] = [data[0]]; + MemValue(true) + } else if addr == CLIC_MSI_BASE+1 & ('n == 1) then { + if get_config_print_platform() + then print_platform("clic[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (clicintie.MSI <- " ^ BitStr(data[0]) ^ ")"); + clicintie[CLIC_MSI] = [data[0]]; + MemValue(true) + } else if addr == CLIC_MSI_BASE+2 & ('n == 1) then { + if get_config_print_platform() + then print_platform("clic[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (clicintattr.MSI <- " ^ BitStr(data[7..0]) ^ ")"); + ip_attr = zero_extend(data[7..0]); + ip_attr_layout[MODE] = zero_extend(ip_attr[7..6]); + ip_attr_layout[TRIG] = zero_extend(ip_attr[2..1]); + if bit_to_bool(ip_attr[0]) then ip_shv = 0b1 else ip_shv = 0b0; + ip_attr_layout[SHV] = ip_shv; + clicintattr[CLIC_MSI] = ip_attr_layout; + MemValue(true) + } else if addr == CLIC_MSI_BASE+3 & ('n == 1) then { + if get_config_print_platform() + then print_platform("clic[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (clicintctl.MSI <- " ^ BitStr(data[7..0]) ^ ")"); + clicintctl[CLIC_MSI] = zero_extend(data[7..0]); + MemValue(true) + } else if addr == CLIC_MTI_BASE & 'n == 4 then { + if get_config_print_platform() + then print_platform("clic[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (clicintip.MTI <- " ^ BitStr(data[0]) ^ ")"); + clicintip[CLIC_MTI] = [data[0]]; + clicintie[CLIC_MTI] = [data[8]]; + ip_attr = zero_extend(data[23..16]); + ip_attr_layout[MODE] = zero_extend(ip_attr[7..6]); + ip_attr_layout[TRIG] = zero_extend(ip_attr[2..1]); + if bit_to_bool(ip_attr[0]) then ip_shv = 0b1 else ip_shv = 0b0; + ip_attr_layout[SHV] = ip_shv; + clicintattr[CLIC_MTI] = ip_attr_layout; + clicintctl[CLIC_MTI] = zero_extend(data[31..24]); + MemValue(true) + } else if addr == CLIC_MTI_BASE+1 & ('n == 1) then { + if get_config_print_platform() + then print_platform("clic[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (clicintie.MTI <- " ^ BitStr(data[0]) ^ ")"); + clicintie[CLIC_MTI] = [data[0]]; + MemValue(true) + } else if addr == CLIC_MTI_BASE+2 & ('n == 1) then { + if get_config_print_platform() + then print_platform("clic[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (clicintattr.MTI <- " ^ BitStr(data[7..0]) ^ ")"); + ip_attr = zero_extend(data[7..0]); + ip_attr_layout[MODE] = zero_extend(ip_attr[7..6]); + ip_attr_layout[TRIG] = zero_extend(ip_attr[2..1]); + if bit_to_bool(ip_attr[0]) then ip_shv = 0b1 else ip_shv = 0b0; + ip_attr_layout[SHV] = ip_shv; + clicintattr[CLIC_MTI] = ip_attr_layout; + MemValue(true) + } else if addr == CLIC_MTI_BASE+3 & ('n == 1) then { + if get_config_print_platform() + then print_platform("clic[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (clicintctl.MTI <- " ^ BitStr(data[7..0]) ^ ")"); + clicintctl[CLIC_MTI] = zero_extend(data[7..0]); + MemValue(true) + } else { + if get_config_print_platform() + then print_platform("clic[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " ()"); + MemValue(true) + } +} + /* Basic terminal character I/O. */ val plat_term_write = {ocaml: "Platform.term_write", c: "plat_term_write", lem: "plat_term_write"} : bits(8) -> unit @@ -386,14 +558,14 @@ function htif_tick() = { /* Top-level MMIO dispatch */ $ifndef RVFI_DII function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = - within_clint(addr, width) | (within_htif_readable(addr, width) & 1 <= 'n) + within_clint(addr, width) | within_clic(addr, width) | (within_htif_readable(addr, width) & 1 <= 'n) $else function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false $endif $ifndef RVFI_DII function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = - within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8) + within_clint(addr, width) | within_clic(addr, width) | (within_htif_writable(addr, width) & 'n <= 8) $else function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false $endif @@ -401,6 +573,8 @@ $endif function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) = if within_clint(paddr, width) then clint_load(t, paddr, width) + else if within_clic(paddr, width) + then clic_load(t, paddr, width) else if within_htif_readable(paddr, width) & (1 <= 'n) then htif_load(t, paddr, width) else match t { @@ -412,6 +586,8 @@ function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_acc function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = if within_clint(paddr, width) then clint_store(paddr, width, data) + else if within_clic(paddr, width) + then clic_store(paddr, width, data) else if within_htif_writable(paddr, width) & 'n <= 8 then htif_store(paddr, width, data) else MemException(E_SAMO_Access_Fault()) diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 012f63b4d..dcd302a22 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -25,10 +25,10 @@ function step(step_no : int) -> bool = { let (retired, stepped) : (Retired, bool) = match dispatchInterrupt(cur_privilege) { - Some(intr, priv) => { + Some(exccode, priv) => { if get_config_print_instr() - then print_bits("Handling interrupt: ", interruptType_to_bits(intr)); - handle_interrupt(intr, priv); + then print_bits("Handling interrupt: ", exccode); + handle_interrupt(exccode, priv); (RETIRE_FAIL, false) }, None() => { diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index ecc53ae85..f072850e0 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -262,24 +262,30 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { /* 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 { - assert(priv == Machine, "invalid current privilege"); - let enabled_pending = mip.bits & mie.bits; - match findPendingInterrupt(enabled_pending) { - Some(i) => let r = (i, Machine) in Some(r), - None() => None() - } - } else { - match getPendingSet(priv) { - None() => None(), - Some(ip, p) => match findPendingInterrupt(ip) { - None() => None(), - Some(i) => let r = (i, p) in Some(r) - } +function dispatchInterrupt(priv : Privilege) -> option((exc_code, Privilege)) = { + + if haveSmclic() then + dispatchClicInterrupt(priv) + else { + + /* 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 { + assert(priv == Machine, "invalid current privilege"); + let enabled_pending = mip.bits & mie.bits; + match findPendingInterrupt(enabled_pending) { + Some(i) => let r = (interruptType_to_bits(i), Machine) in Some(r), + None() => None() + } + } else { + match getPendingSet(priv) { + None() => None(), + Some(ip, p) => match findPendingInterrupt(ip) { + None() => None(), + Some(i) => let r = (interruptType_to_bits(i), p) in Some(r) + } + } } } } @@ -316,6 +322,13 @@ $endif function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits), ext : option(ext_exception)) -> xlenbits = { + var top_ip_attr : clicintattr_layout = undefined; + if haveSmclic() then { + top_ip_attr = clicintattr[unsigned(c)]; + } else { + top_ip_attr = [top_ip_attr with MODE = 0b11, TRIG = 0b00, SHV = 0b0]; + }; + rvfi_trap(); if get_config_print_platform() then print_platform("handling " ^ (if intr then "int#" else "exc#") @@ -335,6 +348,16 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen mtval = tval(info); mepc = pc; + if haveSmclic() then { + mpil = mil; + if intr then { + mil = clicintctl[unsigned(c)]; + } else { + minhv = inhv; + inhv = 0b0; + } + }; + cur_privilege = del_priv; handle_trap_extension(del_priv, pc, ext); @@ -342,7 +365,11 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen if get_config_print_reg() then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); - prepare_trap_vector(del_priv, mcause) + if (haveSmclic() & intr & is_shv(top_ip_attr[SHV])) then { + prepare_shv_clic_trap_vector(del_priv, c) + } else { + prepare_trap_vector(del_priv, mcause) + } }, Supervisor => { assert (haveSupMode(), "no supervisor mode present for delegation"); @@ -360,6 +387,16 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen stval = tval(info); sepc = pc; + if haveSmclic() then { + spil = sil; + if intr then { + sil = clicintctl[unsigned(c)]; + } else { + sinhv = inhv; + inhv = 0b0; + } + }; + cur_privilege = del_priv; handle_trap_extension(del_priv, pc, ext); @@ -367,7 +404,11 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen if get_config_print_reg() then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); - prepare_trap_vector(del_priv, scause) + if (haveSmclic() & intr & is_shv(top_ip_attr[SHV])) then { + prepare_shv_clic_trap_vector(del_priv, c) + } else { + prepare_trap_vector(del_priv, scause) + } }, User => { assert(haveUsrMode(), "no user mode present for delegation"); @@ -380,6 +421,16 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen utval = tval(info); uepc = pc; + if haveSmclic() then { + upil = uil; + if intr then { + uil = clicintctl[unsigned(c)]; + } else { + uinhv = inhv; + inhv = 0b0; + } + }; + cur_privilege = del_priv; handle_trap_extension(del_priv, pc, ext); @@ -387,7 +438,11 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen if get_config_print_reg() then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); - prepare_trap_vector(del_priv, ucause) + if (haveSmclic() & intr & is_shv(top_ip_attr[SHV])) then { + prepare_shv_clic_trap_vector(del_priv, c) + } else { + prepare_trap_vector(del_priv, ucause) + } } }; } @@ -406,6 +461,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, let prev_priv = cur_privilege; mstatus[MIE] = mstatus[MPIE]; mstatus[MPIE] = 0b1; + if haveSmclic() then mil = mpil; cur_privilege = privLevel_of_bits(mstatus[MPP]); mstatus[MPP] = privLevel_to_bits(if haveUsrMode() then User else Machine); if cur_privilege != Machine @@ -417,12 +473,24 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); cancel_reservation(); - prepare_xret_target(Machine) & pc_alignment_mask() + if haveSmclic() & (minhv == 0b1) then { + minhv = 0b0; + var table_entry_addr : xlenbits = prepare_xret_target(Machine) & inhv_pc_alignment_mask(); + match vector_table_fetch(table_entry_addr) { + F_TableError(e, table_addr) => {inhv = 0b1; handle_mem_exception(table_entry_addr, e); table_entry_addr}, + F_TableEntry(table_entry) => { + table_entry + } + } + } else { + prepare_xret_target(Machine) & pc_alignment_mask() + } }, (_, CTL_SRET()) => { let prev_priv = cur_privilege; mstatus[SIE] = mstatus[SPIE]; mstatus[SPIE] = 0b1; + if haveSmclic() then sil = spil; cur_privilege = if mstatus[SPP] == 0b1 then Supervisor else User; mstatus[SPP] = 0b0; if cur_privilege != Machine @@ -435,12 +503,24 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, ^ " to " ^ to_str(cur_privilege)); cancel_reservation(); - prepare_xret_target(Supervisor) & pc_alignment_mask() + if haveSmclic() & (sinhv == 0b1) then { + sinhv = 0b0; + var table_entry_addr : xlenbits = prepare_xret_target(Supervisor) & inhv_pc_alignment_mask(); + match vector_table_fetch(table_entry_addr) { + F_TableError(e, table_addr) => {inhv = 0b1; handle_mem_exception(table_entry_addr, e); table_entry_addr}, + F_TableEntry(table_entry) => { + table_entry + } + } + } else { + prepare_xret_target(Supervisor) & pc_alignment_mask() + } }, (_, CTL_URET()) => { let prev_priv = cur_privilege; mstatus[UIE] = mstatus[UPIE]; mstatus[UPIE] = 0b1; + if haveSmclic() then uil = upil; cur_privilege = User; if get_config_print_reg() @@ -449,7 +529,18 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); cancel_reservation(); - prepare_xret_target(User) & pc_alignment_mask() + if haveSmclic() & (uinhv == 0b1) then { + uinhv = 0b0; + var table_entry_addr : xlenbits = prepare_xret_target(User) & inhv_pc_alignment_mask(); + match vector_table_fetch(table_entry_addr) { + F_TableError(e, table_addr) => {inhv = 0b1; handle_mem_exception(table_entry_addr, e); table_entry_addr}, + F_TableEntry(table_entry) => { + table_entry + } + } + } else { + prepare_xret_target(User) & pc_alignment_mask() + } } } } @@ -468,8 +559,8 @@ function handle_exception(e: ExceptionType) -> unit = { set_next_pc(exception_handler(cur_privilege, CTL_TRAP(t), PC)) } -function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit = - set_next_pc(trap_handler(del_priv, true, interruptType_to_bits(i), PC, None(), None())) +function handle_interrupt(i : exc_code, del_priv : Privilege) -> unit = + set_next_pc(trap_handler(del_priv, true, i, PC, None(), None())) /* state state initialization */ @@ -545,6 +636,8 @@ function init_sys() -> unit = { vtype[vta] = 0b0; vtype[vsew] = 0b000; vtype[vlmul] = 0b000; + /* initialize Smclic csrs */ + init_clicintregs(); // PMP's L and A fields are set to 0 on reset. init_pmp(); diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail index 0059e2a7f..61b61a411 100644 --- a/model/riscv_sys_exceptions.sail +++ b/model/riscv_sys_exceptions.sail @@ -63,16 +63,20 @@ function prepare_xret_target(p) = /* other trap-related CSRs */ function get_mtvec() -> xlenbits = - mtvec.bits + if haveSmclic() then { mtvec.bits & sign_extend(0b1000011)} else + mtvec.bits function get_stvec() -> xlenbits = - stvec.bits + if haveSmclic() then { stvec.bits | zero_extend(0b11) & sign_extend(0b1000011)} else + stvec.bits & sign_extend(0b101) function get_utvec() -> xlenbits = - utvec.bits + if haveSmclic() then { utvec.bits | zero_extend(0b11) & sign_extend(0b1000011)} else + utvec.bits & sign_extend(0b101) function set_mtvec(value : xlenbits) -> xlenbits = { mtvec = legalize_tvec(mtvec, value); + if haveSmclic() == false then {mpil = zero_extend(0b0); spil = zero_extend(0b0); upil = zero_extend(0b0)}; mtvec.bits } diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index fc20e4af4..519b52090 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -403,10 +403,13 @@ function legalize_tvec(o : Mtvec, v : xlenbits) -> Mtvec = { match (trapVectorMode_of_bits(v[Mode])) { TV_Direct => v, TV_Vector => v, + TV_Smclic => v, _ => [v with Mode = o[Mode]] } } +function haveSmclic() -> bool = mtvec[Mode] == 0b11 + bitfield Mcause : xlenbits = { IsInterrupt : xlen - 1, Cause : xlen - 2 .. 0 @@ -421,6 +424,7 @@ function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = { TV_Vector => if c[IsInterrupt] == 0b1 then Some(base + (zero_extend(c[Cause]) << 2)) else Some(base), + TV_Smclic => Some(base), TV_Reserved => None() } } diff --git a/model/riscv_types.sail b/model/riscv_types.sail index d26f79b43..f319327fd 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -266,13 +266,14 @@ overload to_str = {exceptionType_to_str} /* trap modes */ type tv_mode = bits(2) -enum TrapVectorMode = {TV_Direct, TV_Vector, TV_Reserved} +enum TrapVectorMode = {TV_Direct, TV_Vector, TV_Smclic, TV_Reserved} val trapVectorMode_of_bits : tv_mode -> TrapVectorMode function trapVectorMode_of_bits (m) = match (m) { 0b00 => TV_Direct, 0b01 => TV_Vector, + 0b11 => TV_Smclic, _ => TV_Reserved }