diff options
| author | Brian Campbell | 2018-08-13 18:05:21 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-13 18:05:21 +0100 |
| commit | 342cd6a5a02b0478d37f8cc25410106d2846d5b2 (patch) | |
| tree | 1fc3f38f88b32be0b71d44e6ca0cd1edf90289ba /riscv/riscv_platform.sail | |
| parent | a3c66eb5bc5d98a8ce400e5c391e7d9db940c3a7 (diff) | |
More RISC-V built-in type constraints
Diffstat (limited to 'riscv/riscv_platform.sail')
| -rw-r--r-- | riscv/riscv_platform.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail index 7ab83aa6..6e3dee93 100644 --- a/riscv/riscv_platform.sail +++ b/riscv/riscv_platform.sail @@ -85,7 +85,7 @@ let MSIP_BASE : xlenbits = 0x0000000000000000 let MTIMECMP_BASE : xlenbits = 0x0000000000004000 let MTIME_BASE : xlenbits = 0x000000000000bff8 -val clint_load : forall 'n. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} +val clint_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} function clint_load(addr, width) = { let addr = addr - plat_clint_base (); /* FIXME: For now, only allow exact aligned access. */ @@ -224,7 +224,7 @@ function within_mmio_readable(addr : xlenbits, width : atom('n)) -> forall 'n. b function within_mmio_writable(addr : xlenbits, width : atom('n)) -> forall 'n. bool = within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8) -function mmio_read(addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) = +function mmio_read(addr : xlenbits, width : atom('n)) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) = if within_clint(addr, width) then clint_load(addr, width) else if within_htif_readable(addr, width) & (1 <= 'n) |