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

@@ -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)

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)) {

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)

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)

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)
  }
 }

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