diff --git a/Makefile b/Makefile index 7ec256cdf..513f66061 100644 --- a/Makefile +++ b/Makefile @@ -31,7 +31,6 @@ SAIL_DEFAULT_INST += riscv_insts_zkn.sail SAIL_DEFAULT_INST += riscv_insts_zks.sail SAIL_DEFAULT_INST += riscv_insts_zicbom.sail -SAIL_DEFAULT_INST += riscv_insts_zicbop.sail SAIL_DEFAULT_INST += riscv_insts_zicboz.sail SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail diff --git a/model/riscv_insts_zicbom.sail b/model/riscv_insts_zicbom.sail index fab3ee713..e210bcf00 100644 --- a/model/riscv_insts_zicbom.sail +++ b/model/riscv_insts_zicbom.sail @@ -25,47 +25,28 @@ mapping clause assembly = RISCV_ZICBOM(cbop, rs1) val process_clean_inval : (xlenbits, xlenbits, bool, bool) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} function process_clean_inval(vaddr, width, clean, inval) = { - let load: option(ExceptionType) = match ext_data_get_addr(zeros(), vaddr, Read(Data), BYTE) { - Ext_DataAddr_Error(e) => Some(E_Reserved_14()), - Ext_DataAddr_OK(vaddr) => - match translateAddr(vaddr, Read(Cbo)) { - TR_Failure(e, _) => Some(e), - TR_Address(paddr, _) => None() - } - }; - match load { - None() => RETIRE_SUCCESS, - Some(le) => { - let store: option(ExceptionType) = match ext_data_get_addr(zeros(), vaddr, Write(Data), BYTE) { - Ext_DataAddr_Error(e) => Some(E_Reserved_14()), - Ext_DataAddr_OK(vaddr) => - match translateAddr(vaddr, Write(Cbo)) { - TR_Failure(e, _) => Some(e), - TR_Address(paddr, _) => None() - } + match ext_data_get_addr(zeros(), vaddr, Cbo(Data), BYTE) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => { + let data: option(ExceptionType) = match translateAddr(vaddr, Cbo(Data)) { + TR_Address(paddr, _) => pmpCheck_xlen(paddr, width, Cbo(Data), cur_privilege), + TR_Failure(e, _) => Some(e) }; - match store { + match data { None() => RETIRE_SUCCESS, - Some(se) => { - let fetch: option(ExceptionType) = match ext_control_check_addr(vaddr) { - Ext_ControlAddr_Error(e) => Some(E_Reserved_14()), - Ext_ControlAddr_OK(vaddr) => - match translateAddr(vaddr, Execute()) { - TR_Failure(e, _) => Some(e), - TR_Address(paddr, _) => None() - } + Some(de) => { + let fetch: option(ExceptionType) = match translateAddr(vaddr, Cbo(Fetch)) { + TR_Address(paddr, _) => pmpCheck_xlen(paddr, width, Cbo(Fetch), cur_privilege), + TR_Failure(e, _) => Some(e) }; match fetch { None() => RETIRE_SUCCESS, Some(fe) => - match (le, se, fe) { - (E_Load_Access_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, - (_, E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, - (_, _, E_Fetch_Access_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, - (E_Load_Page_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, - (_, E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, - (_, _, E_Fetch_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, - (E_Extension(e), _, _) => { ext_handle_data_check_error(e); RETIRE_FAIL } + match (de, fe) { + (E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, + (_, E_SAMO_Access_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, + (E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, + (_, E_SAMO_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL } } } } diff --git a/model/riscv_insts_zicbop.sail b/model/riscv_insts_zicbop.sail deleted file mode 100644 index bb16e7738..000000000 --- a/model/riscv_insts_zicbop.sail +++ /dev/null @@ -1,62 +0,0 @@ -/* ****************************************************************** */ -/* This file specifies the instructions in the Zicbop extension */ - - -/* ****************************************************************** */ -union clause ast = RISCV_ZICBOP : (prop_zicbop, regidx, bits(7)) - -mapping encdec_prop : prop_zicbop <-> bits(5) = { - PREFETCH_I <-> 0b00000, - PREFETCH_R <-> 0b00001, - PREFETCH_W <-> 0b00011 -} - -mapping clause encdec = RISCV_ZICBOP(prop, rs1, offset) if haveZicbop() - <-> offset @ encdec_prop(prop) @ rs1 @ 0b110 @ 0b00000 @ 0b0010011 if haveZicbop() - -mapping prop_mnemonic : prop_zicbop <-> string = { - PREFETCH_I <-> "prefetch.i", - PREFETCH_R <-> "prefetch.r", - PREFETCH_W <-> "prefetch.w" -} - -mapping clause assembly = RISCV_ZICBOP(prop, rs1, offset) - <-> prop_mnemonic(prop) ^ spc() ^ hex_bits_12(offset @ 0b00000) ^ "(" ^ reg_name(rs1) ^ ")" - -function clause execute(RISCV_ZICBOP(prop, rs1, offset)) = { - /* do nothing other than translate_address for prefetch.i/r/w */ - match prop { - PREFETCH_I => { - let vaddr = X(rs1) + EXTS(offset @ 0b00000); - match ext_control_check_addr(vaddr) { - Ext_ControlAddr_Error(e) => RETIRE_SUCCESS, - Ext_ControlAddr_OK(vaddr) => - match translateAddr(vaddr, Execute()) { - TR_Failure(e, _) => RETIRE_SUCCESS, - TR_Address(paddr, _) => RETIRE_SUCCESS - } - } - }, - PREFETCH_W => { - match ext_data_get_addr(rs1, EXTS(offset @ 0b00000), Write(Data), BYTE) { - Ext_DataAddr_Error(e) => RETIRE_SUCCESS, - Ext_DataAddr_OK(vaddr) => - match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => RETIRE_SUCCESS, - TR_Address(paddr, _) => RETIRE_SUCCESS - } - } - }, - PREFETCH_R => { - match ext_data_get_addr(rs1, EXTS(offset @ 0b00000), Read(Data), BYTE) { - Ext_DataAddr_Error(e) => RETIRE_SUCCESS, - Ext_DataAddr_OK(vaddr) => - match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => RETIRE_SUCCESS, - TR_Address(paddr, _) => RETIRE_SUCCESS - } - } - } - } -} - diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index 669725b5b..3aa698900 100644 --- a/model/riscv_pmp_control.sail +++ b/model/riscv_pmp_control.sail @@ -100,7 +100,9 @@ function pmpCheckRWX(ent, acc) = { Read(_) => ent.R() == 0b1, Write(_) => ent.W() == 0b1, ReadWrite(_) => ent.R() == 0b1 & ent.W() == 0b1, - Execute() => ent.X() == 0b1 + Execute() => ent.X() == 0b1, + Cbo(Data) => ent.R() == 0b1 | ent.W() == 0b1, + Cbo(Fetch) => ent.X() == 0b1 } } @@ -149,10 +151,8 @@ function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType(ext_acce } /* priority checks */ - -function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege) +function pmpCheck_xlen (addr: xlenbits, width: xlenbits, acc: AccessType(ext_access_type), priv: Privilege) -> option(ExceptionType) = { - let width : xlenbits = to_bits(sizeof(xlen), width); let check : bool = match pmpMatchEntry(addr, width, acc, priv, pmp0cfg, pmpaddr0, zeros()) { PMP_Success => true, @@ -222,17 +222,23 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: Acce _ => false } }}}}}}}}}}}}}}}}; - if check then None() else match acc { Read(_) => Some(E_Load_Access_Fault()), Write(_) => Some(E_SAMO_Access_Fault()), ReadWrite(_) => Some(E_SAMO_Access_Fault()), - Execute() => Some(E_Fetch_Access_Fault()) + Execute() => Some(E_Fetch_Access_Fault()), + Cbo(_) => Some(E_SAMO_Access_Fault()) } } +function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege) + -> option(ExceptionType) = { + let width : xlenbits = to_bits(sizeof(xlen), width); + pmpCheck_xlen(addr, width, acc, priv) +} + function init_pmp() -> unit = { pmp0cfg = update_A(pmp0cfg, pmpAddrMatchType_to_bits(OFF)); pmp1cfg = update_A(pmp1cfg, pmpAddrMatchType_to_bits(OFF)); diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail index 5ce049b3a..efc0484ec 100644 --- a/model/riscv_pte.sail +++ b/model/riscv_pte.sail @@ -125,11 +125,15 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, (Write(_), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1), (ReadWrite(_, _), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))), (Execute(), User) => to_pte_check(p.U() == 0b1 & p.X() == 0b1), + (Cbo(Data), User) => to_pte_check(p.U() == 0b1 & (p.W() == 0b1 | (p.R() == 0b1 | (p.X() == 0b1 & mxr)))), + (Cbo(Fetch), User) => to_pte_check(p.U() == 0b1 & p.X() == 0b1), (Read(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & (p.R() == 0b1 | (p.X() == 0b1 & mxr))), (Write(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1), (ReadWrite(_, _), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))), (Execute(), Supervisor) => to_pte_check(p.U() == 0b0 & p.X() == 0b1), + (Cbo(Data), Supervisor) => to_pte_check((p.U() == 0b1 | do_sum) & (p.W() == 0b1 | (p.R() == 0b1 | (p.X() == 0b1 & mxr)))), + (Cbo(Fetch), Supervisor) => to_pte_check(p.U() == 0b0 & p.X() == 0b1), (_, Machine) => internal_error("m-mode mem perm check") } @@ -140,7 +144,7 @@ function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : ex Execute() => false, Read() => false, Write(Data) => true, - Write(Cbo) => false, + Cbo(_) => false, ReadWrite(_,_) => true }); diff --git a/model/riscv_ptw.sail b/model/riscv_ptw.sail index 1a128d23a..3e8f06f9e 100644 --- a/model/riscv_ptw.sail +++ b/model/riscv_ptw.sail @@ -111,7 +111,9 @@ function translationException(a : AccessType(ext_access_type), f : PTW_Error) -> (Write(_), PTW_Access()) => E_SAMO_Access_Fault(), (Write(_), _) => E_SAMO_Page_Fault(), (Execute(), PTW_Access()) => E_Fetch_Access_Fault(), - (Execute(), _) => E_Fetch_Page_Fault() + (Execute(), _) => E_Fetch_Page_Fault(), + (Cbo(_), PTW_Access()) => E_SAMO_Access_Fault(), + (Cbo(_), _) => E_SAMO_Page_Fault() } in { /* print_mem("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */ e diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 0eb1bc821..56a494d53 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -827,9 +827,14 @@ bitfield Envcfg : xlenbits = { register senvcfg : Envcfg register menvcfg : Envcfg -function legalize_envcfg(c : Envcfg, v : xlenbits) -> Envcfg = { - let c = update_CBZE(c, [v[7]]); +function legalize_envcfg_cbie(o : bits(2), v : bits(2)) -> bits(2) = match (v) { + 0b10 => 0b00, + _ => v +} + +function legalize_envcfg(o : Envcfg, v : xlenbits) -> Envcfg = { + let c = update_CBZE(o, [v[7]]); let c = update_CBCFE(c, [v[6]]); - let c = update_CBIE(c, v[5 .. 4]); + let c = update_CBIE(c, legalize_envcfg_cbie(o.CBIE(), v[5 .. 4])); c } \ No newline at end of file diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 903f64b72..8603a52be 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -168,6 +168,7 @@ enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL} union AccessType ('a : Type) = { Read : 'a, Write : 'a, + Cbo : 'a, ReadWrite : ('a, 'a), Execute : unit } diff --git a/model/riscv_vmem_types.sail b/model/riscv_vmem_types.sail index 65cffb23e..f3419b69f 100644 --- a/model/riscv_vmem_types.sail +++ b/model/riscv_vmem_types.sail @@ -71,7 +71,7 @@ type ext_access_type = unit let Data : ext_access_type = () -let Cbo : ext_access_type = () +let Fetch : ext_access_type = () let default_write_acc : ext_access_type = Data @@ -81,7 +81,8 @@ function accessType_to_str (a) = Read(_) => "R", Write(_) => "W", ReadWrite(_, _) => "RW", - Execute() => "X" + Execute() => "X", + Cbo(_) => "RWX" } overload to_str = {accessType_to_str}