2 files changed, 8 insertions, 0 deletions
diff --git a/model/sys/vmem.sail b/model/sys/vmem.sail
index 875ba7a..45150c2 100644
--- a/model/sys/vmem.sail
+++ b/model/sys/vmem.sail
@@ -156,6 +156,8 @@ function pt_walk(
   }
 }
 
+termination_measure pt_walk(_,_,_,_,_,_,_,level,_, _) = level
+
 // ****************************************************************
 // Architectural SATP CSR
 
diff --git a/model/sys/vmem_utils.sail b/model/sys/vmem_utils.sail
index c07b661..1b6216c 100644
--- a/model/sys/vmem_utils.sail
+++ b/model/sys/vmem_utils.sail
@@ -172,6 +172,9 @@ function vmem_read_addr(vaddr, offset, width, acc, aq, rl, res) = {
   Ok(data)
 }
 
+// This lets the Rocq extraction know why the repeat loop above terminates
+termination_measure vmem_read_addr repeat n
+
 val vmem_write_addr : forall 'width, is_mem_width('width).
   (virtaddr, int('width), bits(8 * 'width), MemoryAccessType(ext_access_type), bool, bool, bool)
   -> result(bool, ExecutionResult)
@@ -227,6 +230,9 @@ function vmem_write_addr(vaddr, width, data, acc, aq, rl, res) = {
   Ok(write_success)
 }
 
+// This lets the Rocq extraction know why the repeat loop above terminates
+termination_measure vmem_write_addr repeat n
+
 val vmem_read : forall 'width, is_mem_width('width).
   (regidx, xlenbits, int('width), MemoryAccessType(ext_access_type), bool, bool, bool)
   -> result(bits(8 * 'width), ExecutionResult)