From fabc6983224ce9f2c834d0f79535543bea913041 Mon Sep 17 00:00:00 2001 From: Weiwei Li Date: Fri, 26 May 2023 10:34:48 +0800 Subject: [PATCH] Change the parameters of ext_data_get_addr in riscv_insns_zicbo*.sail to conform to the interface. Update the type of width parameter of ext_data_get_addr to xlenbits. --- model/riscv_addr_checks.sail | 2 +- model/riscv_insts_aext.sail | 6 +++--- model/riscv_insts_base.sail | 4 ++-- model/riscv_insts_fext.sail | 4 ++-- model/riscv_insts_zicbom.sail | 17 +++++++++-------- model/riscv_insts_zicboz.sail | 29 +++++++++++++++-------------- 6 files changed, 32 insertions(+), 30 deletions(-) diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail index 5211dcbb9..4cf17fd12 100644 --- a/model/riscv_addr_checks.sail +++ b/model/riscv_addr_checks.sail @@ -114,7 +114,7 @@ type ext_data_addr_error = unit /* Default data addr is just base register + immediate offset (may be zero). Extensions might override and add additional checks. */ -function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width) +function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : xlenbits) -> Ext_DataAddr_Check(ext_data_addr_error) = let addr = X(base) + offset in Ext_DataAddr_OK(addr) diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 22523e266..bad618556 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -125,7 +125,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { /* Get the address, X(rs1) (no offset). * Extensions might perform additional checks on address validity. */ - match ext_data_get_addr(rs1, zeros(), Read(Data), width) { + match ext_data_get_addr(rs1, zeros(), Read(Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { let aligned : bool = @@ -186,7 +186,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { /* Get the address, X(rs1) (no offset). * Extensions might perform additional checks on address validity. */ - match ext_data_get_addr(rs1, zeros(), Write(Data), width) { + match ext_data_get_addr(rs1, zeros(), Write(Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { let aligned : bool = @@ -276,7 +276,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { /* Get the address, X(rs1) (no offset). * Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) { + match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { match translateAddr(vaddr, ReadWrite(Data, Data)) { diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index b6d792cb6..33b9112d1 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -386,7 +386,7 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { let offset : xlenbits = EXTS(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Read(Data), width) { + match ext_data_get_addr(rs1, offset, Read(Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) @@ -442,7 +442,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { let offset : xlenbits = EXTS(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Write(Data), width) { + match ext_data_get_addr(rs1, offset, Write(Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 7bfc43ffc..030fd2895 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -375,7 +375,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = { let offset : xlenbits = EXTS(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Read(Data), width) { + match ext_data_get_addr(rs1, offset, Read(Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) @@ -441,7 +441,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = { let (aq, rl, con) = (false, false, false); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Write(Data), width) { + match ext_data_get_addr(rs1, offset, Write(Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) diff --git a/model/riscv_insts_zicbom.sail b/model/riscv_insts_zicbom.sail index b464f539e..53402c99d 100644 --- a/model/riscv_insts_zicbom.sail +++ b/model/riscv_insts_zicbom.sail @@ -22,13 +22,17 @@ mapping cbop_mnemonic : cbop_zicbom <-> string = { mapping clause assembly = RISCV_ZICBOM(cbop, rs1) <-> cbop_mnemonic(cbop) ^ spc() ^ "(" ^ reg_name(rs1) ^ ")" -val process_clean_inval : (xlenbits, xlenbits, cbop_zicbom) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} -function process_clean_inval(vaddr, width, cbop) = { - match ext_data_get_addr(zeros(), vaddr, Read(Data), BYTE) { +val process_clean_inval : (regidx, cbop_zicbom) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +function process_clean_inval(rs1, cbop) = { + let rs1_val = X(rs1); + let cache_block_size = plat_cache_block_size(); + let begin_addr = rs1_val & ~(cache_block_size - EXTZ(0b1)); + let offset = begin_addr - rs1_val; + 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, _) => pmpCheck_xlen(paddr, width, Read(Data), cur_privilege), + TR_Address(paddr, _) => pmpCheck_xlen(paddr, cache_block_size, Read(Data), cur_privilege), TR_Failure(e, _) => Some(e) }; match res { @@ -58,9 +62,6 @@ function cbop_for_cbo_inval(p : Privilege) -> option(cbop_zicbom) = { } function clause execute(RISCV_ZICBOM(cbop, rs1)) = { - let rs1_val = X(rs1); - let cache_block_size = plat_cache_block_size(); - let vaddr = rs1_val & ~(cache_block_size - EXTZ(0b1)); let cbcfe = cbo_clean_flush_enable(cur_privilege); let final_op : option(cbop_zicbom) = match (cbop, cbcfe) { (CBO_CLEAN, true) => Some(CBO_CLEAN), @@ -71,6 +72,6 @@ function clause execute(RISCV_ZICBOM(cbop, rs1)) = { }; match final_op { None() => { handle_illegal(); RETIRE_FAIL }, - Some(cbop) => process_clean_inval(vaddr, cache_block_size, cbop) + Some(cbop) => process_clean_inval(rs1, cbop) } } diff --git a/model/riscv_insts_zicboz.sail b/model/riscv_insts_zicboz.sail index 863e7cc65..cfbb808ab 100644 --- a/model/riscv_insts_zicboz.sail +++ b/model/riscv_insts_zicboz.sail @@ -12,16 +12,20 @@ mapping clause assembly = RISCV_ZICBOZ(rs1) function get_envcfg_cbze(p : Privilege) -> bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) | ((p == User) & (senvcfg.CBZE() == 0b0))) -val process_cbo_zero : (xlenbits, xlenbits) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg} -function process_cbo_zero(vaddr, width) = { - offset : xlenbits = zeros(); +val process_cbo_zero : (regidx) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +function process_cbo_zero(rs1) = { + let rs1_val = X(rs1); + let cache_block_size = plat_cache_block_size(); + let begin_addr = rs1_val & ~(cache_block_size - EXTZ(0b1)); + let offset = begin_addr - rs1_val; + index : xlenbits = zeros(); failed : bool = false; - while (offset <_u width) & (failed == false) do { - let addr = vaddr + offset; - match ext_data_get_addr(zeros(), addr, Write(Data), BYTE) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); failed = true }, - Ext_DataAddr_OK(vaddr) => - match translateAddr(vaddr, Write(Data)) { + match ext_data_get_addr(rs1, offset, Write(Data), cache_block_size) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); failed = true }, + Ext_DataAddr_OK(vaddr) => + while (index <_u cache_block_size) & (failed == false) do { + let addr = vaddr + index; + match translateAddr(addr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); failed = true }, TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false); @@ -30,7 +34,7 @@ function process_cbo_zero(vaddr, width) = { MemValue(_) => { let res : MemoryOpResult(bool) = mem_write_value(paddr, 1, zeros(), false, false, false); match (res) { - MemValue(true) => offset = offset + EXTZ(0b1), + MemValue(true) => index = index + EXTZ(0b1), MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), MemException(e) => { handle_mem_exception(vaddr, e); failed = true } } @@ -45,11 +49,8 @@ function process_cbo_zero(vaddr, width) = { } function clause execute(RISCV_ZICBOZ(rs1)) = { - let rs1_val = X(rs1); - let cache_block_size = plat_cache_block_size(); - let vaddr = rs1_val & ~(cache_block_size - EXTZ(0b1)); if get_envcfg_cbze(cur_privilege) then - process_cbo_zero(vaddr, cache_block_size) + process_cbo_zero(rs1) else { handle_illegal(); RETIRE_FAIL