From e0d14c519d18d4e86ddd3d856b41711d5d53bf9d Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur <103736+pmundkur@users.noreply.github.com> Date: Thu, 6 Feb 2025 13:51:11 -0600 Subject: [PATCH] Improve Zicbom implementation. Clarify the privilege checking of xenvcfg.CBIE in cbo.inval. The privilege check should extend to the hypervisor case, when two possible illegal exceptions could be thrown. This check as written doesn't match the pseudo-Sail in the CMO spec, but is arguably clearer. Make sure that the reserved CBIE value is not representable. --- model/riscv_insts_zicbom.sail | 68 +++++++++++++++++++++++++++-------- 1 file changed, 54 insertions(+), 14 deletions(-) diff --git a/model/riscv_insts_zicbom.sail b/model/riscv_insts_zicbom.sail index b2aa9cde7..0e6624d33 100644 --- a/model/riscv_insts_zicbom.sail +++ b/model/riscv_insts_zicbom.sail @@ -11,8 +11,6 @@ function clause extensionEnabled(Ext_Zicbom) = sys_enable_zicbom() function cbo_clean_flush_enabled(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBCFE][0], senvcfg[CBCFE][0]) -function cbo_inval_enabled(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBIE][0], senvcfg[CBIE][0]) -function cbo_inval_as_inval(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBIE][1], senvcfg[CBIE][1]) /* ****************************************************************** */ union clause ast = RISCV_ZICBOM : (cbop_zicbom, regidx) @@ -35,6 +33,35 @@ mapping cbop_mnemonic : cbop_zicbom <-> string = { mapping clause assembly = RISCV_ZICBOM(cbop, rs1) <-> cbop_mnemonic(cbop) ^ spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")" +/* CBIE from xenvcfg */ +enum cbie = {CBIE_ILLEGAL, CBIE_EXEC_FLUSH, CBIE_EXEC_INVAL} + +mapping encdec_cbie : cbie <-> bits(2) = { + CBIE_ILLEGAL <-> 0b00, + CBIE_EXEC_FLUSH <-> 0b01, + CBIE_EXEC_INVAL <-> 0b11, + backwards 0b10 => internal_error(__FILE__, __LINE__, "reserved CBIE"), +} + +// Illegal-Virtual will be needed by the hypervisor mode, but is currently unused. +enum checked_cbop = {CBOP_ILLEGAL, CBOP_ILLEGAL_VIRTUAL, CBOP_INVAL_FLUSH, CBOP_INVAL_INVAL} + +// Select the cbop to perform based on the privilege. +function cbop_priv_check(p: Privilege) -> checked_cbop = { + let mCBIE : cbie = encdec_cbie(menvcfg[CBIE]); + let sCBIE : cbie = if extensionEnabled(Ext_S) + then encdec_cbie(senvcfg[CBIE]) + else encdec_cbie(menvcfg[CBIE]); + match (p, mCBIE, sCBIE) { + (Machine, _, _ ) => CBOP_INVAL_INVAL, + (_, CBIE_ILLEGAL, _ ) => CBOP_ILLEGAL, // (priv_mode != M) && mCBIE == 00 + (User, _, CBIE_ILLEGAL ) => CBOP_ILLEGAL, // (priv_mode == U) && sCBIE == 00 + (_, CBIE_EXEC_FLUSH, _ ) => CBOP_INVAL_FLUSH, // (priv_mode != M) && mCBIE == 01 + (User, _, CBIE_EXEC_FLUSH) => CBOP_INVAL_FLUSH, // (priv_mode == U) && sCBIE == 01 + _ => CBOP_INVAL_INVAL, + } +} + val process_clean_inval : (regidx, cbop_zicbom) -> Retired function process_clean_inval(rs1, cbop) = { let rs1_val = X(rs1); @@ -100,16 +127,29 @@ function process_clean_inval(rs1, cbop) = { } } -function clause execute(RISCV_ZICBOM(cbop, rs1)) = - match cbop { - CBO_CLEAN if cbo_clean_flush_enabled(cur_privilege) => - process_clean_inval(rs1, cbop), - CBO_FLUSH if cbo_clean_flush_enabled(cur_privilege) => - process_clean_inval(rs1, cbop), - CBO_INVAL if cbo_inval_enabled(cur_privilege) => - process_clean_inval(rs1, if cbo_inval_as_inval(cur_privilege) then CBO_INVAL else CBO_FLUSH), - _ => { - handle_illegal(); - RETIRE_FAIL - }, +function clause execute(RISCV_ZICBOM(CBO_CLEAN, rs1)) = { + if cbo_clean_flush_enabled(cur_privilege) + then process_clean_inval(rs1, CBO_CLEAN) + else { + handle_illegal(); + RETIRE_FAIL } +} +function clause execute(RISCV_ZICBOM(CBO_FLUSH, rs1)) = { + if cbo_clean_flush_enabled(cur_privilege) + then process_clean_inval(rs1, CBO_FLUSH) + else { + handle_illegal(); + RETIRE_FAIL + } +} + +function clause execute(RISCV_ZICBOM(CBO_INVAL, rs1)) = { + match cbop_priv_check(cur_privilege) { + CBOP_ILLEGAL => { handle_illegal(); + RETIRE_FAIL }, + CBOP_ILLEGAL_VIRTUAL => internal_error(__FILE__, __LINE__, "unimplemented"), + CBOP_INVAL_INVAL => process_clean_inval(rs1, CBO_INVAL), + CBOP_INVAL_FLUSH => process_clean_inval(rs1, CBO_FLUSH), + } +}