diff options
Diffstat (limited to 'model/sys/vmem_utils.sail')
| -rw-r--r-- | model/sys/vmem_utils.sail | 6 |
1 files changed, 6 insertions, 0 deletions
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) |