summaryrefslogtreecommitdiff
path: root/riscv/riscv_duopod.sail
diff options
context:
space:
mode:
Diffstat (limited to 'riscv/riscv_duopod.sail')
-rw-r--r--riscv/riscv_duopod.sail4
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) }