Add overload operators for virtaddr

Add a subtraction operator overload for `virtaddr` and use it in the CMO code.
riscv · Jan 14, 2025 · fca81a3 · fca81a3
1 parent ff4077c
commit fca81a3
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 2 deletions.
diff --git a/model/prelude_mem_addrtype.sail b/model/prelude_mem_addrtype.sail
@@ -19,3 +19,7 @@ newtype virtaddr = virtaddr : xlenbits
 function physaddr_bits(physaddr(paddr) : physaddr) -> physaddrbits = paddr
 
 function virtaddr_bits(virtaddr(vaddr) : virtaddr) -> xlenbits = vaddr
+
+function sub_virtaddr_xlenbits(virtaddr(addr) : virtaddr, offset : xlenbits) -> virtaddr = virtaddr(addr - offset)
+
+overload operator - = { sub_virtaddr_xlenbits }
diff --git a/model/riscv_insts_zicbom.sail b/model/riscv_insts_zicbom.sail
@@ -92,7 +92,7 @@ function process_clean_inval(rs1, cbop) = {
           };
           // Errors report the address that was encoded in the instruction rather
           // than the address that caused the fault (i.e. the aligned address).
-          handle_mem_exception(virtaddr(virtaddr_bits(vaddr) - offset), e);
+          handle_mem_exception(vaddr - offset, e);
           RETIRE_FAIL
         }
       }

diff --git a/model/riscv_insts_zicboz.sail b/model/riscv_insts_zicboz.sail
@@ -52,7 +52,7 @@ function clause execute(RISCV_ZICBOZ(rs1)) = {
                   MemException(e) => {
                     // Errors report the address that was encoded in the instruction rather
                     // than the address that caused the fault (i.e. the aligned address).
-                    handle_mem_exception(virtaddr(virtaddr_bits(vaddr) - offset), e);
+                    handle_mem_exception(vaddr - offset, e);
                     RETIRE_FAIL
                   },
                 }