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