diff options
| author | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2018-08-13 18:05:21 +0100 |
|---|---|---|
| committer | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2018-08-13 18:05:21 +0100 |
| commit | 7d5093130cb9ac24656de54f79e32a8ed8d24853 (patch) | |
| tree | 0f5f7a6d7b4dabc4557e3fcf2c11278a53c358d2 /riscv_mem.sail | |
| parent | 92348672229c2819d5b3ebb02de76fb7558184fa (diff) | |
| download | sail-riscv-7d5093130cb9ac24656de54f79e32a8ed8d24853.zip sail-riscv-7d5093130cb9ac24656de54f79e32a8ed8d24853.tar.gz sail-riscv-7d5093130cb9ac24656de54f79e32a8ed8d24853.tar.bz2 | |
More RISC-V built-in type constraints
Diffstat (limited to 'riscv_mem.sail')
| -rw-r--r-- | riscv_mem.sail | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/riscv_mem.sail b/riscv_mem.sail index 9425c0f..7268e9c 100644 --- a/riscv_mem.sail +++ b/riscv_mem.sail @@ -16,7 +16,7 @@ function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : boo MemValue(v) } } -function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n, 'n >= 0. MemoryOpResult(bits(8 * 'n)) = +function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) = /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */ if t == Data & within_mmio_readable(addr, width) then mmio_read(addr, width) |