diff --git a/model/riscv_insts_zicbom.sail b/model/riscv_insts_zicbom.sail index a8fdd8bcb..c36478cd8 100644 --- a/model/riscv_insts_zicbom.sail +++ b/model/riscv_insts_zicbom.sail @@ -52,47 +52,51 @@ function process_clean_inval(rs1, cbop) = { match ext_data_get_addr(rs1, offset, Read(Data), cache_block_size) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - let res: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) { - TR_Address(paddr, _) => { - // "A cache-block management instruction is permitted to access the - // specified cache block whenever a load instruction or store instruction - // is permitted to access the corresponding physical addresses. If - // neither a load instruction nor store instruction is permitted to - // access the physical addresses, but an instruction fetch is permitted - // to access the physical addresses, whether a cache-block management - // instruction is permitted to access the cache block is UNSPECIFIED." - // - // In this implementation we currently don't allow access for fetches. - let exc_read = phys_access_check(Read(Data), cur_privilege, paddr, cache_block_size); - let exc_write = phys_access_check(Write(Data), cur_privilege, paddr, cache_block_size); - match (exc_read, exc_write) { - // Access is permitted if read OR write are allowed. If neither - // are allowed then we always report a store exception. - (Some(exc_read), Some(exc_write)) => Some(exc_write), - _ => None(), + if (instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(0b0), cacheBlockSize_to_matchSize(cache_block_size_exp), STORE_MATCH)) + then { RETIRE_FAIL } + else { + let res: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) { + TR_Address(paddr, _) => { + // "A cache-block management instruction is permitted to access the + // specified cache block whenever a load instruction or store instruction + // is permitted to access the corresponding physical addresses. If + // neither a load instruction nor store instruction is permitted to + // access the physical addresses, but an instruction fetch is permitted + // to access the physical addresses, whether a cache-block management + // instruction is permitted to access the cache block is UNSPECIFIED." + // + // In this implementation we currently don't allow access for fetches. + let exc_read = phys_access_check(Read(Data), cur_privilege, paddr, cache_block_size); + let exc_write = phys_access_check(Write(Data), cur_privilege, paddr, cache_block_size); + match (exc_read, exc_write) { + // Access is permitted if read OR write are allowed. If neither + // are allowed then we always report a store exception. + (Some(exc_read), Some(exc_write)) => Some(exc_write), + _ => None(), + } + }, + TR_Failure(e, _) => Some(e) + }; + // "If access to the cache block is not permitted, a cache-block management + // instruction raises a store page fault or store guest-page fault exception + // if address translation does not permit any access or raises a store access + // fault exception otherwise." + match res { + // The model has no caches so there's no action required. + None() => RETIRE_SUCCESS, + Some(e) => { + let e : ExceptionType = match e { + E_Load_Access_Fault() => E_SAMO_Access_Fault(), + E_SAMO_Access_Fault() => E_SAMO_Access_Fault(), + E_Load_Page_Fault() => E_SAMO_Page_Fault(), + E_SAMO_Page_Fault() => E_SAMO_Page_Fault(), + // No other exceptions should be generated since we're not checking + // for fetch access and it's can't be misaligned. + _ => internal_error(__FILE__, __LINE__, "unexpected exception for cmo.clean/inval"), + }; + handle_mem_exception(vaddr, e); + RETIRE_FAIL } - }, - TR_Failure(e, _) => Some(e) - }; - // "If access to the cache block is not permitted, a cache-block management - // instruction raises a store page fault or store guest-page fault exception - // if address translation does not permit any access or raises a store access - // fault exception otherwise." - match res { - // The model has no caches so there's no action required. - None() => RETIRE_SUCCESS, - Some(e) => { - let e : ExceptionType = match e { - E_Load_Access_Fault() => E_SAMO_Access_Fault(), - E_SAMO_Access_Fault() => E_SAMO_Access_Fault(), - E_Load_Page_Fault() => E_SAMO_Page_Fault(), - E_SAMO_Page_Fault() => E_SAMO_Page_Fault(), - // No other exceptions should be generated since we're not checking - // for fetch access and it's can't be misaligned. - _ => internal_error(__FILE__, __LINE__, "unexpected exception for cmo.clean/inval"), - }; - handle_mem_exception(vaddr, e); - RETIRE_FAIL } } } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 15a7c5cb3..177e1ad03 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -611,7 +611,7 @@ function check_trigger_firing(cur_priv : Privilege) -> bool = { var ITrigFired : bool = false; var ETrigFired : bool = false; var MCtrlTrigFired : bool = false; - var fired_trigger_idx : vector(2, dec, {'n, (0 <= 'n < 7). int('n)}) = [0, 0]; + var fired_trigger_idx : vector(2, dec, {'n, (0 <= 'n < N_TRIGGERS). int('n)}) = [0, 0]; var InstrCount : InstructionCount = Mk_InstructionCount(zero_extend(0b0)); var IEtrigger : InterruptTrigger = Mk_InterruptTrigger(zero_extend(0b0)); var MCtrl6 : MatchControlType6 = Mk_MatchControlType6(zero_extend(0b0)); @@ -745,7 +745,7 @@ function init_sys() -> unit = { vtype[vsew] = 0b000; vtype[vlmul] = 0b000; - foreach (i from 0 to 6) { + foreach (i from 0 to (sizeof(N_TRIGGERS) - 1)) { tdata1_x.tdata1[i][(xlen - 1) .. (xlen - 4)] = 0xf; }; diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index c33b7a620..bf1e4e7cd 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -694,7 +694,6 @@ register tselect : xlenbits /* Legalize TSELECT */ function legalize_tselect(o : xlenbits, v : xlenbits) -> xlenbits = { let t : xlenbits = o; - // TODO: Avoid hardcoded value if (unsigned(v) <= (sizeof(N_TRIGGERS) - 1)) then { v } else { t } }