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 | |
| parent | a3c66eb5bc5d98a8ce400e5c391e7d9db940c3a7 (diff) | |
More RISC-V built-in type constraints
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/prelude.sail | 10 | ||||
| -rw-r--r-- | riscv/riscv_mem.sail | 2 | ||||
| -rw-r--r-- | riscv/riscv_platform.sail | 4 |
3 files changed, 8 insertions, 8 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 5bc5be13..8636bda6 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -64,11 +64,11 @@ function def_spc_backwards s = () val def_spc_matches_prefix = "opt_spc_matches_prefix" : string -> option((unit, nat)) -val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm. (atom('n), atom('m)) -> bool -val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool -val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool -val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool -val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool +val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val lteq_atom = {coq: "Z.leb", _: "lteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val lt_atom = {coq: "Z.ltb", _: "lt"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val gt_atom = {coq: "Z.gtb", _: "gt"} : forall 'n 'm. (atom('n), atom('m)) -> bool val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit"} : (bit, bit) -> bool diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail index 9425c0ff..7268e9cc 100644 --- a/riscv/riscv_mem.sail +++ b/riscv/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) 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) |