diff --git a/Makefile b/Makefile index e26ee2901..8194d87dc 100644 --- a/Makefile +++ b/Makefile @@ -23,7 +23,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 @@ -70,10 +70,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_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_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_csr_ext.sail # access to CSR extensions SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 6478919ca..805143b56 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -12,16 +12,7 @@ val csr_name_map : csreg <-> string scattered mapping csr_name_map -/* 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" @@ -38,8 +29,6 @@ mapping clause csr_name_map = 0xC82 <-> "instreth" /* TODO: other hpm counters */ /* 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 f2980fb9e..6cd64e0eb 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -76,8 +76,6 @@ function readCSR csr : csreg -> xlenbits = { /* supervisor mode */ (0x100, _) => lower_mstatus(mstatus).bits, - (0x102, _) => sedeleg.bits, - (0x103, _) => sideleg.bits, (0x104, _) => lower_mie(mie, mideleg).bits, (0x105, _) => get_stvec(), (0x106, _) => zero_extend(scounteren.bits), @@ -157,8 +155,6 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { /* supervisor mode */ (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) }, (0x105, _) => { Some(set_stvec(value)) }, (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits)) }, diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail deleted file mode 100644 index 2f83a0abc..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 ext_is_CSR_defined(0x000) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ustatus -function clause ext_is_CSR_defined(0x004) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uie -function clause ext_is_CSR_defined(0x005) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utvec -function clause ext_is_CSR_defined(0x040) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uscratch -function clause ext_is_CSR_defined(0x041) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uepc -function clause ext_is_CSR_defined(0x042) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ucause -function clause ext_is_CSR_defined(0x043) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utval -function clause ext_is_CSR_defined(0x044) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // 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(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(0x043) = Some(utval) -function clause ext_read_CSR(0x044) = 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); - mie = lift_sie(mie, mideleg, sie); - Some(mie.bits) } -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(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); - Some(mip.bits) } diff --git a/model/riscv_next_regs.sail b/model/riscv_next_regs.sail deleted file mode 100644 index 6f25447b8..000000000 --- a/model/riscv_next_regs.sail +++ /dev/null @@ -1,91 +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)); - let u = [u with UPIE = s[UPIE]]; - let u = [u with UIE = s[UIE]]; - u -} - -function lift_ustatus(s : Sstatus, u : Ustatus) -> Sstatus = { - let s = [s with UPIE = u[UPIE]]; - let s = [s with UIE = u[UIE]]; - s -} - -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)); - let u = [u with UEI = s[UEI] & d[UEI]]; - let u = [u with UTI = s[UTI] & d[UTI]]; - let u = [u with USI = s[USI] & d[USI]]; - u -} - -/* 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)); - let u = [u with UEI = s[UEI] & d[UEI]]; - let u = [u with UTI = s[UTI] & d[UTI]]; - let u = [u with USI = s[USI] & d[USI]]; - u -} - -/* 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 4f7b3540b..fcd1400e4 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -27,8 +27,8 @@ function is_CSR_defined (csr : csreg) -> bool = /* machine mode: trap setup */ 0x300 => true, // mstatus 0x301 => true, // misa - 0x302 => extensionEnabled(Ext_S) | extensionEnabled(Ext_N), // medeleg - 0x303 => extensionEnabled(Ext_S) | extensionEnabled(Ext_N), // mideleg + 0x302 => extensionEnabled(Ext_S) , // medeleg + 0x303 => extensionEnabled(Ext_S) , // mideleg 0x304 => true, // mie 0x305 => true, // mtvec 0x306 => extensionEnabled(Ext_U), // mcounteren @@ -62,8 +62,6 @@ function is_CSR_defined (csr : csreg) -> bool = /* supervisor mode: trap setup */ 0x100 => extensionEnabled(Ext_S), // sstatus - 0x102 => extensionEnabled(Ext_S) & extensionEnabled(Ext_N), // sedeleg - 0x103 => extensionEnabled(Ext_S) & extensionEnabled(Ext_N), // sideleg 0x104 => extensionEnabled(Ext_S), // sie 0x105 => extensionEnabled(Ext_S), // stvec 0x106 => extensionEnabled(Ext_S), // scounteren @@ -169,12 +167,7 @@ val cancel_reservation = {ocaml: "Platform.cancel_reservation", interpreter: "Pl 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 + 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) @@ -240,24 +233,12 @@ 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() - } - } + if not(extensionEnabled(Ext_S)) then None() + else let r = (d, Supervisor) in Some(r) } } } @@ -269,7 +250,7 @@ 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(extensionEnabled(Ext_U)) | (not(extensionEnabled(Ext_S)) & not(extensionEnabled(Ext_N))) then { + if not(extensionEnabled(Ext_U)) | (not(extensionEnabled(Ext_S))) then { assert(priv == Machine, "invalid current privilege"); let enabled_pending = mip.bits & mie.bits; match findPendingInterrupt(enabled_pending) { diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail index 0059e2a7f..bc761af7e 100644 --- a/model/riscv_sys_exceptions.sail +++ b/model/riscv_sys_exceptions.sail @@ -21,8 +21,7 @@ function handle_trap_extension(p : Privilege, pc : xlenbits, u : option(unit)) - function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = { let tvec : Mtvec = match p { Machine => mtvec, - Supervisor => stvec, - User => utvec + Supervisor => stvec }; match tvec_addr(tvec, cause) { Some(epc) => epc, @@ -68,9 +67,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 +76,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 fc19d5161..cca68100b 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -128,9 +128,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 @@ -265,13 +262,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 { - let m = [m with UPIE = 0b0]; - let m = [m with UIE = 0b0]; - m - } else m; - if not(extensionEnabled(Ext_U)) then { let m = [m with MPRV = 0b0]; m @@ -321,9 +311,7 @@ function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = { * 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 + m } function legalize_mie(o : Minterrupts, v : xlenbits) -> Minterrupts = { @@ -336,10 +324,7 @@ function legalize_mie(o : Minterrupts, v : xlenbits) -> Minterrupts = { 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 + m } function legalize_mideleg(o : Minterrupts, v : xlenbits) -> Minterrupts = { @@ -568,32 +553,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). */ @@ -625,10 +592,10 @@ 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 + m + } else m + m } else m } @@ -642,19 +609,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