diff options
Diffstat (limited to 'riscv/riscv_duopod.sail')
| -rw-r--r-- | riscv/riscv_duopod.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/riscv/riscv_duopod.sail b/riscv/riscv_duopod.sail index ff1e4065..0a5a7f8c 100644 --- a/riscv/riscv_duopod.sail +++ b/riscv/riscv_duopod.sail @@ -5,7 +5,7 @@ type xlen_t = bits(64) type regno ('n : Int), 0 <= 'n < 32 = atom('n) type regbits = bits(5) -val zeros : forall 'n. atom('n) -> bits('n) +val zeros : forall 'n, 'n >= 0. atom('n) -> bits('n) function zeros n = replicate_bits(0b0, n) val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)} @@ -35,7 +35,7 @@ overload X = {rX, wX} /* Accessors for memory */ -val MEMr : forall 'n. (xlen_t, atom('n)) -> bits(8 * 'n) effect {rmem} +val MEMr : forall 'n, 'n >= 0. (xlen_t, atom('n)) -> bits(8 * 'n) effect {rmem} function MEMr (addr, width) = match __RISCV_read(addr, width, false, false, false) { Some(v) => v, None() => zeros(8 * width) } |
