diff options
| author | Tim Hutt <timothy.hutt@codasip.com> | 2024-05-21 14:48:25 +0100 |
|---|---|---|
| committer | Tim Hutt <timothy.hutt@codasip.com> | 2024-06-03 16:01:37 +0100 |
| commit | 9194dd51e58ee6767d4494a04fdddb4635c6bfdc (patch) | |
| tree | 30a982ce043ee8a6dec3d4ffcf8e295c56a44cdb /model/prelude_mem.sail | |
| parent | e1663e985e2bc6c6311b6e81c296f6c4fd794e2d (diff) | |
| download | sail-riscv-9194dd51e58ee6767d4494a04fdddb4635c6bfdc.zip sail-riscv-9194dd51e58ee6767d4494a04fdddb4635c6bfdc.tar.gz sail-riscv-9194dd51e58ee6767d4494a04fdddb4635c6bfdc.tar.bz2 | |
Change ext_data_get_addr to use bytes for width
Instead of `word_width` which can only be up to 8 bytes, just use bytes. This allows larger accesses (the limit is increased to 4096), e.g. for `cbo.zero`.
Diffstat (limited to 'model/prelude_mem.sail')
| -rw-r--r-- | model/prelude_mem.sail | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index 345e78c..03ac69e 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -80,8 +80,15 @@ instantiation sail_mem_write with because it means width argument can be fast native integer. It would be even better if it could be <= 8 bytes so that data can also be a 64-bit int but CHERI needs 128-bit accesses for - capabilities and SIMD / vector instructions will also need more. */ -type max_mem_access : Int = 16 + capabilities and SIMD / vector instructions will also need more. + + The specific value does not matter (if it is >8) since anything up + to 2^64-1 will result in a native int being used for the width type. + + 4096 was chosen because it is a page size, and a reasonable maximum + for cbo.zero. + */ +type max_mem_access : Int = 4096 val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool |