From 5cea5201a4dafef0814ce67d65380b17020c944a Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Wed, 16 Oct 2024 09:37:07 +0100 Subject: [PATCH] Remove N extension This extension was never ratified, has been removed from the ISA manual and apparently would need significant changes if it were to ever come back. Therefore it makes sense to remove it from the model in order to simplify the code. Co-authored-by: KotorinMinami --- Makefile | 4 +- model/riscv_csr_begin.sail | 12 ---- model/riscv_insts_next.sail | 26 ------- model/riscv_insts_zicsr.sail | 4 -- model/riscv_next_control.sail | 40 ----------- model/riscv_next_regs.sail | 96 -------------------------- model/riscv_sys_control.sail | 118 +++++--------------------------- model/riscv_sys_exceptions.sail | 14 +--- model/riscv_sys_regs.sail | 70 ++----------------- 9 files changed, 28 insertions(+), 356 deletions(-) delete mode 100644 model/riscv_insts_next.sail delete mode 100644 model/riscv_next_control.sail delete mode 100644 model/riscv_next_regs.sail diff --git a/Makefile b/Makefile index c2a0b332f..6e6483320 100644 --- a/Makefile +++ b/Makefile @@ -21,7 +21,7 @@ SAIL_VLEN := riscv_vlen.sail # Instruction sources, depending on target SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail riscv_misa_ext.sail -SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_zca.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_next.sail riscv_insts_hints.sail +SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_zca.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_hints.sail SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_zcf.sail SAIL_DEFAULT_INST += riscv_insts_dext.sail riscv_insts_zcd.sail @@ -72,10 +72,8 @@ SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.s # System and platform sources SAIL_SYS_SRCS = riscv_csr_begin.sail # Start of CSR scattered definitions. SAIL_SYS_SRCS += riscv_vext_control.sail # helpers for the 'V' extension -SAIL_SYS_SRCS += riscv_next_regs.sail 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_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail index 0e67746cf..053776435 100644 --- a/model/riscv_csr_begin.sail +++ b/model/riscv_csr_begin.sail @@ -15,16 +15,6 @@ scattered mapping csr_name_map // TODO: These csr_name_map definitions should be moved to the files // corresponding to their extensions rather than all be here. -/* user trap setup */ -mapping clause csr_name_map = 0x000 <-> "ustatus" -mapping clause csr_name_map = 0x004 <-> "uie" -mapping clause csr_name_map = 0x005 <-> "utvec" -/* user trap handling */ -mapping clause csr_name_map = 0x040 <-> "uscratch" -mapping clause csr_name_map = 0x041 <-> "uepc" -mapping clause csr_name_map = 0x042 <-> "ucause" -mapping clause csr_name_map = 0x043 <-> "utval" -mapping clause csr_name_map = 0x044 <-> "uip" /* user floating-point context */ mapping clause csr_name_map = 0x001 <-> "fflags" mapping clause csr_name_map = 0x002 <-> "frm" @@ -100,8 +90,6 @@ mapping clause csr_name_map = 0xC9F <-> "hpmcounter31h" /* supervisor trap setup */ mapping clause csr_name_map = 0x100 <-> "sstatus" -mapping clause csr_name_map = 0x102 <-> "sedeleg" -mapping clause csr_name_map = 0x103 <-> "sideleg" mapping clause csr_name_map = 0x104 <-> "sie" mapping clause csr_name_map = 0x105 <-> "stvec" mapping clause csr_name_map = 0x106 <-> "scounteren" diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail deleted file mode 100644 index 52d8bc26d..000000000 --- a/model/riscv_insts_next.sail +++ /dev/null @@ -1,26 +0,0 @@ -/*=======================================================================================*/ -/* 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 */ -/*=======================================================================================*/ - -/* *****************************************************************/ -/* This file specifies the instruction added by the 'N' extension. */ - -union clause ast = URET : unit - -mapping clause encdec = URET() - <-> 0b0000000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 - -function clause execute URET() = { - if not(extensionEnabled(Ext_U)) | not(sys_enable_next()) - then handle_illegal() - else if not(ext_check_xret_priv(User)) - then ext_fail_xret_priv() - else set_next_pc(exception_handler(cur_privilege, CTL_URET(), PC)); - RETIRE_FAIL -} - -mapping clause assembly = URET() <-> "uret" diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 8e8c0dce2..5e4d47b9e 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -74,8 +74,6 @@ function clause read_CSR(0x7a0) = ~(tselect) /* this indicates we don't have an /* supervisor mode */ function clause read_CSR(0x100) = lower_mstatus(mstatus).bits -function clause read_CSR(0x102) = sedeleg.bits -function clause read_CSR(0x103) = sideleg.bits function clause read_CSR(0x104) = lower_mie(mie, mideleg).bits function clause read_CSR(0x105) = get_stvec() function clause read_CSR(0x106) = zero_extend(scounteren.bits) @@ -162,8 +160,6 @@ function clause write_CSR(0x7a0, value) = { tselect = value; tselect } /* supervisor mode */ function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits } -function clause write_CSR(0x102, value) = { sedeleg = legalize_sedeleg(sedeleg, value); sedeleg.bits } -function clause write_CSR(0x103, value) = { sideleg.bits = value; sideleg.bits } /* TODO: does this need legalization? */ function clause write_CSR(0x104, value) = { mie = legalize_sie(mie, mideleg, value); mie.bits } function clause write_CSR(0x105, value) = { set_stvec(value) } function clause write_CSR(0x106, value) = { scounteren = legalize_scounteren(scounteren, value); zero_extend(scounteren.bits) } diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail deleted file mode 100644 index aa10bad98..000000000 --- a/model/riscv_next_control.sail +++ /dev/null @@ -1,40 +0,0 @@ -/*=======================================================================================*/ -/* 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 'N' user-level interrupts standard extension. */ - -function clause is_CSR_defined(0x000) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ustatus -function clause is_CSR_defined(0x004) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uie -function clause is_CSR_defined(0x005) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utvec -function clause is_CSR_defined(0x040) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uscratch -function clause is_CSR_defined(0x041) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uepc -function clause is_CSR_defined(0x042) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ucause -function clause is_CSR_defined(0x043) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utval -function clause is_CSR_defined(0x044) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uip - -function clause read_CSR(0x000) = lower_sstatus(lower_mstatus(mstatus)).bits -function clause read_CSR(0x004) = lower_sie(lower_mie(mie, mideleg), sideleg).bits -function clause read_CSR(0x005) = get_utvec() -function clause read_CSR(0x040) = uscratch -function clause read_CSR(0x041) = get_xret_target(User) & pc_alignment_mask() -function clause read_CSR(0x042) = ucause.bits -function clause read_CSR(0x043) = utval -function clause read_CSR(0x044) = lower_sip(lower_mip(mip, mideleg), sideleg).bits - -function clause write_CSR(0x000, value) = { mstatus = legalize_ustatus(mstatus, value); mstatus.bits } -function clause write_CSR(0x004, value) = { let sie = legalize_uie(lower_mie(mie, mideleg), sideleg, value); - mie = lift_sie(mie, mideleg, sie); - mie.bits } -function clause write_CSR(0x005, value) = { set_utvec(value) } -function clause write_CSR(0x040, value) = { uscratch = value; uscratch } -function clause write_CSR(0x041, value) = { set_xret_target(User, value) } -function clause write_CSR(0x042, value) = { ucause.bits = value; ucause.bits } -function clause write_CSR(0x043, value) = { utval = value; utval } -function clause write_CSR(0x044, value) = { let sip = legalize_uip(lower_mip(mip, mideleg), sideleg, value); - mip = lift_sip(mip, mideleg, sip); - mip.bits } diff --git a/model/riscv_next_regs.sail b/model/riscv_next_regs.sail deleted file mode 100644 index 64c9f77c2..000000000 --- a/model/riscv_next_regs.sail +++ /dev/null @@ -1,96 +0,0 @@ -/*=======================================================================================*/ -/* 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 'N' user-level interrupts standard extension. */ - -/* ustatus reveals a subset of mstatus */ -bitfield Ustatus : xlenbits = { - UPIE : 4, - UIE : 0 -} - -/* This is a view, so there is no register defined. */ -function lower_sstatus(s : Sstatus) -> Ustatus = { - let u = Mk_Ustatus(zero_extend(0b0)); - - [u with - UPIE = s[UPIE], - UIE = s[UIE], - ] -} - -function lift_ustatus(s : Sstatus, u : Ustatus) -> Sstatus = { - [s with - UPIE = u[UPIE], - UIE = u[UIE], - ] -} - -function legalize_ustatus(m : Mstatus, v : xlenbits) -> Mstatus = { - let u = Mk_Ustatus(v); - let s = lower_mstatus(m); // lower current mstatus to sstatus - let s = lift_ustatus(s, u); // get updated sstatus - let m = lift_sstatus(m, s); // lift it to an updated mstatus - m -} - -bitfield Uinterrupts : xlenbits = { - UEI : 8, /* external interrupt */ - UTI : 4, /* timer interrupt */ - USI : 0 /* software interrupt */ -} - -/* Provides the uip read view of sip (s) as delegated by sideleg (d). */ -function lower_sip(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = { - let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0)); - [u with - UEI = s[UEI] & d[UEI], - UTI = s[UTI] & d[UTI], - USI = s[USI] & d[USI], - ] -} - -/* Provides the uie read view of sie as delegated by sideleg. */ -function lower_sie(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = { - let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0)); - [u with - UEI = s[UEI] & d[UEI], - UTI = s[UTI] & d[UTI], - USI = s[USI] & d[USI], - ] -} - -/* Returns the new value of sip from the previous sip (o) and the written uip (u) as delegated by sideleg (d). */ -function lift_uip(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = { - let s : Sinterrupts = o; - let s = if d[USI] == 0b1 then [s with USI = u[USI]] else s; - s -} - -function legalize_uip(s : Sinterrupts, d : Sinterrupts, v : xlenbits) -> Sinterrupts = { - lift_uip(s, d, Mk_Uinterrupts(v)) -} - -/* Returns the new value of sie from the previous sie (o) and the written uie (u) as delegated by sideleg (d). */ -function lift_uie(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = { - let s : Sinterrupts = o; - let s = if d[UEI] == 0b1 then [s with UEI = u[UEI]] else s; - let s = if d[UTI] == 0b1 then [s with UTI = u[UTI]] else s; - let s = if d[USI] == 0b1 then [s with USI = u[USI]] else s; - s -} - -function legalize_uie(s : Sinterrupts, d : Sinterrupts, v : xlenbits) -> Sinterrupts = { - lift_uie(s, d, Mk_Uinterrupts(v)) -} - -register utvec : Mtvec -register uscratch : xlenbits -register uepc : xlenbits -register ucause : Mcause -register utval : xlenbits diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 80e6ea5c7..f408c0942 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -28,8 +28,8 @@ function clause is_CSR_defined(0xf15) = true // mconfigptr /* machine mode: trap setup */ function clause is_CSR_defined(0x300) = true // mstatus function clause is_CSR_defined(0x301) = true // misa -function clause is_CSR_defined(0x302) = extensionEnabled(Ext_S) | extensionEnabled(Ext_N) // medeleg -function clause is_CSR_defined(0x303) = extensionEnabled(Ext_S) | extensionEnabled(Ext_N) // mideleg +function clause is_CSR_defined(0x302) = extensionEnabled(Ext_S) // medeleg +function clause is_CSR_defined(0x303) = extensionEnabled(Ext_S) // mideleg function clause is_CSR_defined(0x304) = true // mie function clause is_CSR_defined(0x305) = true // mtvec function clause is_CSR_defined(0x306) = extensionEnabled(Ext_U) // mcounteren @@ -73,8 +73,6 @@ function clause is_CSR_defined(0x7a0) = true /* supervisor mode: trap setup */ function clause is_CSR_defined(0x100) = extensionEnabled(Ext_S) // sstatus -function clause is_CSR_defined(0x102) = extensionEnabled(Ext_S) & extensionEnabled(Ext_N) // sedeleg -function clause is_CSR_defined(0x103) = extensionEnabled(Ext_S) & extensionEnabled(Ext_N) // sideleg function clause is_CSR_defined(0x104) = extensionEnabled(Ext_S) // sie function clause is_CSR_defined(0x105) = extensionEnabled(Ext_S) // stvec function clause is_CSR_defined(0x106) = extensionEnabled(Ext_S) // scounteren @@ -183,13 +181,7 @@ val cancel_reservation = impure {interpreter: "Platform.cancel_reservation", c: function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = { let idx = num_of_ExceptionType(e); let super = bit_to_bool(medeleg.bits[idx]); - /* if S-mode is absent, medeleg delegates to U-mode if 'N' is supported. */ - let user = if extensionEnabled(Ext_S) - then super & extensionEnabled(Ext_N) & bit_to_bool(sedeleg.bits[idx]) - else super & extensionEnabled(Ext_N); - let deleg = if extensionEnabled(Ext_U) & user then User - else if extensionEnabled(Ext_S) & super then Supervisor - else Machine; + let deleg = if extensionEnabled(Ext_S) & super then Supervisor else Machine; /* We cannot transition to a less-privileged mode. */ if privLevel_to_bits(deleg) <_u privLevel_to_bits(p) then p else deleg @@ -206,10 +198,7 @@ function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = { else if ip[SEI] == 0b1 then Some(I_S_External) else if ip[SSI] == 0b1 then Some(I_S_Software) else if ip[STI] == 0b1 then Some(I_S_Timer) - else if ip[UEI] == 0b1 then Some(I_U_External) - else if ip[USI] == 0b1 then Some(I_U_Software) - else if ip[UTI] == 0b1 then Some(I_U_Timer) - else None() + else None() } /* Process the pending interrupts xip at a privilege according to @@ -225,28 +214,26 @@ union interrupt_set = { function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits, priv_enabled : bool) -> interrupt_set = { /* interrupts that are enabled but not delegated are pending */ - let effective_pend = xip.bits & xie.bits & (~ (xideleg)); + let effective_pend = xip.bits & xie.bits & ~(xideleg); /* the others are delegated */ let effective_delg = xip.bits & xideleg; /* we have pending interrupts if this privilege is enabled */ - if priv_enabled & (effective_pend != zero_extend(0b0)) + if priv_enabled & (effective_pend != zeros()) then Ints_Pending(effective_pend) - else if effective_delg != zero_extend(0b0) + else if effective_delg != zeros() then Ints_Delegated(effective_delg) else Ints_Empty() } /* 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. + * pending set for an enabled privilege. * * We don't use the lowered views of {xie,xip} here, since the spec - * allows for example the M_Timer to be delegated to the U-mode. + * allows for example the M_Timer to be delegated to the S-mode. */ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { - assert(extensionEnabled(Ext_U), "no user mode: M/U or M/S/U system required"); let effective_pending = mip.bits & mie.bits; - if effective_pending == zero_extend(0b0) then None() /* fast path */ + if effective_pending == zeros() then None() /* fast path */ else { /* Higher privileges than the current one are implicitly enabled, * while lower privileges are blocked. An unsupported privilege is @@ -254,24 +241,10 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { */ let mIE = priv != Machine | (priv == Machine & mstatus[MIE] == 0b1); let sIE = extensionEnabled(Ext_S) & (priv == User | (priv == Supervisor & mstatus[SIE] == 0b1)); - let uIE = extensionEnabled(Ext_N) & (priv == User & mstatus[UIE] == 0b1); match processPending(mip, mie, mideleg.bits, mIE) { Ints_Empty() => None(), - Ints_Pending(p) => let r = (p, Machine) in Some(r), - Ints_Delegated(d) => - if not(extensionEnabled(Ext_S)) then { - if uIE then let r = (d, User) in Some(r) - else None() - } else { - /* the delegated bits are pending for S-mode */ - match processPending(Mk_Minterrupts(d), mie, sideleg.bits, sIE) { - Ints_Empty() => None(), - Ints_Pending(p) => let r = (p, Supervisor) in Some(r), - Ints_Delegated(d) => if uIE - then let r = (d, User) in Some(r) - else None() - } - } + Ints_Pending(p) => Some((p, Machine)), + Ints_Delegated(d) => if sIE then Some((d, Supervisor)) else None(), } } } @@ -280,32 +253,12 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { * 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. - */ - let multipleModesSupported = extensionEnabled(Ext_U); - if not(multipleModesSupported) then { - assert(priv == Machine, "invalid current privilege") - }; - /* Even with U-mode, we don't need to check delegation when M-mode is the only - one that can take interrupts, i.e. when we don't have S-mode and don't have - the N extension - */ - let delegationPossible = extensionEnabled(Ext_S) | extensionEnabled(Ext_N); - if multipleModesSupported & delegationPossible then { - match getPendingSet(priv) { - None() => None(), - Some(ip, p) => match findPendingInterrupt(ip) { - None() => None(), - Some(i) => let r = (i, p) in Some(r) - } - } - } else { - let enabled_pending = mip.bits & mie.bits; - match findPendingInterrupt(enabled_pending) { - Some(i) => let r = (i, Machine) in Some(r), - None() => None() - } + match getPendingSet(priv) { + None() => None(), + Some(ip, p) => match findPendingInterrupt(ip) { + None() => None(), + Some(i) => Some((i, p)), + } } } @@ -315,7 +268,6 @@ union ctl_result = { CTL_TRAP : sync_exception, CTL_SRET : unit, CTL_MRET : unit, - CTL_URET : unit } /* trap value */ @@ -392,26 +344,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen prepare_trap_vector(del_priv, scause) }, - User => { - assert(extensionEnabled(Ext_U), "no user mode present for delegation"); - - ucause[IsInterrupt] = bool_to_bits(intr); - ucause[Cause] = zero_extend(c); - - mstatus[UPIE] = mstatus[UIE]; - mstatus[UIE] = 0b0; - utval = tval(info); - uepc = pc; - - cur_privilege = del_priv; - - handle_trap_extension(del_priv, pc, ext); - - if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); - - prepare_trap_vector(del_priv, ucause) - } + User => internal_error(__FILE__, __LINE__, "Invalid privilege level"), }; } @@ -458,19 +391,6 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, prepare_xret_target(Supervisor) & pc_alignment_mask() }, - (_, CTL_URET()) => { - let prev_priv = cur_privilege; - mstatus[UIE] = mstatus[UPIE]; - mstatus[UPIE] = 0b1; - cur_privilege = User; - - if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); - if get_config_print_platform() - then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); - - prepare_xret_target(User) & pc_alignment_mask() - } } } diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail index 0059e2a7f..4e4b550ad 100644 --- a/model/riscv_sys_exceptions.sail +++ b/model/riscv_sys_exceptions.sail @@ -22,7 +22,7 @@ function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = { let tvec : Mtvec = match p { Machine => mtvec, Supervisor => stvec, - User => utvec + User => internal_error(__FILE__, __LINE__, "Invalid privilege level"), }; match tvec_addr(tvec, cause) { Some(epc) => epc, @@ -42,7 +42,7 @@ function get_xret_target(p) = match p { Machine => mepc, Supervisor => sepc, - User => uepc + User => internal_error(__FILE__, __LINE__, "Invalid privilege level"), } val set_xret_target : (Privilege, xlenbits) -> xlenbits @@ -51,7 +51,7 @@ function set_xret_target(p, value) = { match p { Machine => mepc = target, Supervisor => sepc = target, - User => uepc = target + User => internal_error(__FILE__, __LINE__, "Invalid privilege level"), }; target } @@ -68,9 +68,6 @@ function get_mtvec() -> xlenbits = function get_stvec() -> xlenbits = stvec.bits -function get_utvec() -> xlenbits = - utvec.bits - function set_mtvec(value : xlenbits) -> xlenbits = { mtvec = legalize_tvec(mtvec, value); mtvec.bits @@ -80,8 +77,3 @@ function set_stvec(value : xlenbits) -> xlenbits = { stvec = legalize_tvec(stvec, value); stvec.bits } - -function set_utvec(value : xlenbits) -> xlenbits = { - utvec = legalize_tvec(utvec, value); - utvec.bits -} diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 2a5a219c8..787b77fd9 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -136,9 +136,6 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = { } } -enum clause extension = Ext_N -function clause extensionEnabled(Ext_N) = misa[N] == 0b1 - enum clause extension = Ext_U function clause extensionEnabled(Ext_U) = misa[U] == 0b1 @@ -200,11 +197,9 @@ bitfield Mstatus : xlenbits = { MPIE : 7, SPIE : 5, - UPIE : 4, MIE : 3, SIE : 1, - UIE : 0 } register mstatus : Mstatus @@ -277,11 +272,6 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { Mk_Mstatus([m.bits with 37 .. 36 = 0b00]) } else m; - /* Hardwired to zero in the absence of 'U' or 'N'. */ - let m = if not(extensionEnabled(Ext_N)) then { - [m with UPIE = 0b0, UIE = 0b0] - } else m; - if not(extensionEnabled(Ext_U)) then { let m = [m with MPRV = 0b0]; m @@ -312,15 +302,12 @@ function in32BitMode() -> bool = { bitfield Minterrupts : xlenbits = { MEI : 11, /* external interrupts */ SEI : 9, - UEI : 8, MTI : 7, /* timers interrupts */ STI : 5, - UTI : 4, MSI : 3, /* software interrupts */ SSI : 1, - USI : 0, } register mip : Minterrupts /* Pending */ register mie : Minterrupts /* Enabled */ @@ -330,26 +317,19 @@ function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = { /* The only writable bits are the S-mode bits, and with the 'N' * extension, the U-mode bits. */ let v = Mk_Minterrupts(v); - let m = [o with SEI = v[SEI], STI = v[STI], SSI = v[SSI]]; - if extensionEnabled(Ext_U) & extensionEnabled(Ext_N) then { - [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]] - } else m + [o with SEI = v[SEI], STI = v[STI], SSI = v[SSI]] } function legalize_mie(o : Minterrupts, v : xlenbits) -> Minterrupts = { let v = Mk_Minterrupts(v); - let m = [o with + [o with MEI = v[MEI], MTI = v[MTI], MSI = v[MSI], SEI = v[SEI], STI = v[STI], SSI = v[SSI] - ]; - /* The U-mode bits will be modified if we have the 'N' extension. */ - if extensionEnabled(Ext_U) & extensionEnabled(Ext_N) then { - [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]] - } else m + ] } function legalize_mideleg(o : Minterrupts, v : xlenbits) -> Minterrupts = { @@ -554,9 +534,7 @@ bitfield Sstatus : xlenbits = { VS : 10 .. 9, SPP : 8, SPIE : 5, - UPIE : 4, SIE : 1, - UIE : 0 } /* sstatus is a view of mstatus, so there is no register defined. */ @@ -584,9 +562,7 @@ function lower_mstatus(m : Mstatus) -> Sstatus = { VS = m[VS], SPP = m[SPP], SPIE = m[SPIE], - UPIE = m[UPIE], SIE = m[SIE], - UIE = m[UIE], ] } @@ -603,9 +579,7 @@ function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = { VS = s[VS], SPP = s[SPP], SPIE = s[SPIE], - UPIE = s[UPIE], SIE = s[SIE], - UIE = s[UIE], ] } @@ -613,32 +587,14 @@ function legalize_sstatus(m : Mstatus, v : xlenbits) -> Mstatus = { legalize_mstatus(m, lift_sstatus(m, Mk_Sstatus(v)).bits) } -bitfield Sedeleg : xlenbits = { - UEnvCall : 8, - SAMO_Access_Fault : 7, - SAMO_Addr_Align : 6, - Load_Access_Fault : 5, - Load_Addr_Align : 4, - Breakpoint : 3, - Illegal_Instr : 2, - Fetch_Access_Fault: 1, - Fetch_Addr_Align : 0 -} -register sedeleg : Sedeleg -function legalize_sedeleg(s : Sedeleg, v : xlenbits) -> Sedeleg = { - Mk_Sedeleg(zero_extend(v[8..0])) -} bitfield Sinterrupts : xlenbits = { SEI : 9, /* external interrupts */ - UEI : 8, STI : 5, /* timers interrupts */ - UTI : 4, SSI : 1, /* software interrupts */ - USI : 0 } /* Provides the sip read view of mip (m) as delegated by mideleg (d). */ @@ -649,9 +605,6 @@ function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { SEI = m[SEI] & d[SEI], STI = m[STI] & d[STI], SSI = m[SSI] & d[SSI], - UEI = m[UEI] & d[UEI], - UTI = m[UTI] & d[UTI], - USI = m[USI] & d[USI], ] } @@ -663,9 +616,6 @@ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { SEI = m[SEI] & d[SEI], STI = m[STI] & d[STI], SSI = m[SSI] & d[SSI], - UEI = m[UEI] & d[UEI], - UTI = m[UTI] & d[UTI], - USI = m[USI] & d[USI], ] } @@ -673,11 +623,7 @@ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = { let m : Minterrupts = o; let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m; - if extensionEnabled(Ext_N) then { - let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m; - let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m; - m - } else m + m } function legalize_sip(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterrupts = { @@ -690,19 +636,13 @@ function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterru let m = if d[SEI] == 0b1 then [m with SEI = s[SEI]] else m; let m = if d[STI] == 0b1 then [m with STI = s[STI]] else m; let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m; - if extensionEnabled(Ext_N) then { - let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m; - let m = if d[UTI] == 0b1 then [m with UTI = s[UTI]] else m; - let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m; - m - } else m + m } function legalize_sie(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterrupts = { lift_sie(m, d, Mk_Sinterrupts(v)) } -register sideleg : Sinterrupts /* other non-VM related supervisor state */ register stvec : Mtvec