diff --git a/Makefile b/Makefile index 255224125..501c0149c 100644 --- a/Makefile +++ b/Makefile @@ -64,9 +64,11 @@ SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.s SAIL_SYS_SRCS = riscv_csr_map.sail SAIL_SYS_SRCS += riscv_vext_control.sail # helpers for the 'V' extension SAIL_SYS_SRCS += riscv_next_regs.sail +SAIL_SYS_SRCS += riscv_clic_regs.sail # Smclic/Ssclic extensions SAIL_SYS_SRCS += riscv_sys_exceptions.sail # default basic helpers for exception handling SAIL_SYS_SRCS += riscv_sync_exception.sail # define the exception structure used in the model SAIL_SYS_SRCS += riscv_next_control.sail # helpers for the 'N' extension +SAIL_SYS_SRCS += riscv_clic_control.sail # helpers for the Smclic/Ssclic extensions SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail SAIL_SYS_SRCS += riscv_csr_ext.sail # access to CSR extensions SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling @@ -88,11 +90,14 @@ SAIL_REGS_SRCS = riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_ SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail SAIL_REGS_SRCS += riscv_ext_regs.sail $(SAIL_CHECK_SRCS) SAIL_REGS_SRCS += riscv_vreg_type.sail riscv_vext_regs.sail +SAIL_REGS_SRCS += riscv_clic_type.sail # Smclic/Ssclic extensions SAIL_ARCH_SRCS = $(PRELUDE) SAIL_ARCH_SRCS += riscv_types_common.sail riscv_types_ext.sail riscv_types.sail SAIL_ARCH_SRCS += riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail SAIL_ARCH_SRCS += riscv_mem.sail $(SAIL_VM_SRCS) +SAIL_ARCH_SRCS += riscv_clic_mem.sail # clic vector table fetch uses mem_read in riscv_mem.sail + SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types_common.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS) riscv_types_kext.sail SAIL_ARCH_SRCS += riscv_types_kext.sail # Shared/common code for the cryptography extension. diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 253da353f..dd471b948 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -113,6 +113,16 @@ mach_bits plat_clint_size(unit u) return rv_clint_size; } +mach_bits plat_clic_base(unit u) +{ + return rv_clic_base; +} + +mach_bits plat_clic_size(unit u) +{ + return rv_clic_size; +} + unit load_reservation(mach_bits addr) { reservation = addr; diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 38fac2f07..175445072 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -29,6 +29,9 @@ mach_bits plat_get_16_random_bits(); mach_bits plat_clint_base(unit); mach_bits plat_clint_size(unit); +mach_bits plat_clic_base(unit); +mach_bits plat_clic_size(unit); + bool speculate_conditional(unit); unit load_reservation(mach_bits); bool match_reservation(mach_bits); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index c2ae256ef..64691056d 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -42,6 +42,9 @@ uint64_t rv_16_random_bits(void) uint64_t rv_clint_base = UINT64_C(0x2000000); uint64_t rv_clint_size = UINT64_C(0xc0000); +uint64_t rv_clic_base = UINT64_C(0x4000000); +uint64_t rv_clic_size = UINT64_C(0xc0000); + uint64_t rv_htif_tohost = UINT64_C(0x80001000); uint64_t rv_insns_per_tick = UINT64_C(100); diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index e3e4a9678..c8aeb1473 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -34,6 +34,9 @@ extern uint64_t rv_16_random_bits(void); extern uint64_t rv_clint_base; extern uint64_t rv_clint_size; +extern uint64_t rv_clic_base; +extern uint64_t rv_clic_size; + extern uint64_t rv_htif_tohost; extern uint64_t rv_insns_per_tick; diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index f3c63435b..2de102979 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -616,6 +616,8 @@ void init_sail(uint64_t elf_entry) rv_rom_size = UINT64_C(0); rv_clint_base = UINT64_C(0); rv_clint_size = UINT64_C(0); + rv_clic_base = UINT64_C(0); + rv_clic_size = UINT64_C(0); rv_htif_tohost = UINT64_C(0); zPC = elf_entry; } else diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 27e8ee5ed..cd607c1ed 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -193,6 +193,14 @@ val plat_clint_size : unit -> bitvector let plat_clint_size () = [] declare ocaml target_rep function plat_clint_size = `Platform.clint_size` +val plat_clic_base : unit -> bitvector +let plat_clic_base () = [] +declare ocaml target_rep function plat_clic_base = `Platform.clic_base` + +val plat_clic_size : unit -> bitvector +let plat_clic_size () = [] +declare ocaml target_rep function plat_clic_size = `Platform.clic_size` + val plat_enable_dirty_update : unit -> bool let plat_enable_dirty_update () = false declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update` diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index d1139081d..e61dcbfff 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -181,6 +181,14 @@ val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a let plat_clint_size () = wordFromInteger 0 declare ocaml target_rep function plat_clint_size = `Platform.clint_size` +val plat_clic_base : forall 'a. Size 'a => unit -> bitvector 'a +let plat_clic_base () = wordFromInteger 0 +declare ocaml target_rep function plat_clic_base = `Platform.clic_base` + +val plat_clic_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_clic_size () = wordFromInteger 0 +declare ocaml target_rep function plat_clic_size = `Platform.clic_size` + val plat_enable_dirty_update : unit -> bool let plat_enable_dirty_update () = false declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update` 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 } diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index a8bde44d6..e28c90277 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -102,6 +102,9 @@ let dram_size () = arch_bits_of_int64 !P.dram_size_ref let clint_base () = arch_bits_of_int64 P.clint_base let clint_size () = arch_bits_of_int64 P.clint_size +let clic_base () = arch_bits_of_int64 P.clic_base +let clic_size () = arch_bits_of_int64 P.clic_size + let insns_per_tick () = Big_int.of_int P.insns_per_tick let htif_tohost () = @@ -165,6 +168,7 @@ let init arch elf_file = print_platform (Printf.sprintf "\nRegistered htif_tohost at 0x%Lx.\n" (Big_int.to_int64 (Elf.elf_tohost ()))); print_platform (Printf.sprintf "Registered clint at 0x%Lx (size 0x%Lx).\n%!" P.clint_base P.clint_size); + print_platform (Printf.sprintf "Registered clic at 0x%Lx (size 0x%Lx).\n%!" P.clic_base P.clic_size); let start_pc = Elf.Big_int.to_int64 (Elf.elf_entry ()) in let rom = make_rom arch start_pc in diff --git a/ocaml_emulator/platform_impl.ml b/ocaml_emulator/platform_impl.ml index 39de43776..4e7f3a4c5 100644 --- a/ocaml_emulator/platform_impl.ml +++ b/ocaml_emulator/platform_impl.ml @@ -53,6 +53,8 @@ let reset_vec_int arch start_pc = [ let dram_base = 0x80000000L;; (* Spike::DRAM_BASE *) let clint_base = 0x02000000L;; (* Spike::CLINT_BASE *) let clint_size = 0x000c0000L;; (* Spike::CLINT_SIZE *) +let clic_base = 0x04000000L;; (* Spike::MCLIC_BASE *) +let clic_size = 0x000c0000L;; (* Spike::CLIC_SIZE *) let rom_base = 0x00001000L;; (* Spike::DEFAULT_RSTVEC *) let dram_size_ref = ref (Int64.(shift_left 64L 20)) @@ -108,6 +110,12 @@ let spike_dts isa_spec mmu_spec cpu_hz insns_per_rtc_tick mems = ^ " reg = <0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical clint_base 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand clint_base 0xffffffffL) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical clint_size 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand clint_size 0xffffffffL) ^ ">;\n" ^ " };\n" + ^ " clic@" ^ Printf.sprintf "%Lx" clic_base ^ " {\n" + ^ " compatible = \"riscv,clic0\";\n" + ^ " interrupts-extended = <&CPU0_intc 3 &CPU0_intc 7 >;\n" + ^ " reg = <0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical clic_base 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand clic_base 0xffffffffL) + ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical clic_size 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand clic_size 0xffffffffL) ^ ">;\n" + ^ " };\n" ^ " };\n" ^ " htif {\n" ^ " compatible = \"ucb,htif0\";\n"