diff options
Diffstat (limited to 'risc-v/riscv_extras_embed.lem')
| -rw-r--r-- | risc-v/riscv_extras_embed.lem | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem index 1146d1cd..440ad378 100644 --- a/risc-v/riscv_extras_embed.lem +++ b/risc-v/riscv_extras_embed.lem @@ -4,11 +4,16 @@ open import Sail_impl_base open import Sail_values open import Prompt -val MEMr : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserve : (vector bitU * integer) -> M (vector bitU) +val MEMr : (vector bitU * integer) -> M (vector bitU) +val MEMr_acquire : (vector bitU * integer) -> M (vector bitU) +val MEMr_reserved : (vector bitU * integer) -> M (vector bitU) +val MEMr_reserved_acquire : (vector bitU * integer) -> M (vector bitU) + +let MEMr (addr,size) = read_mem false Read_plain addr size +let MEMr_acquire (addr,size) = read_mem false Read_RISCV_acquire addr size +let MEMr_reserved (addr,size) = read_mem false Read_RISCV_reserved addr size +let MEMr_reserved_acquire (addr,size) = read_mem false Read_RISCV_reserved_acquire addr size -let MEMr (addr,size) = read_mem false Read_plain addr size -let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size val MEMea : (vector bitU * integer) -> M unit val MEMea_conditional : (vector bitU * integer) -> M unit |