diff options
| author | Shaked Flur | 2017-08-17 13:41:21 +0100 |
|---|---|---|
| committer | Shaked Flur | 2017-08-17 13:41:21 +0100 |
| commit | cc46b5a2366cd73d34117590448f6779fac4d312 (patch) | |
| tree | 7a5cad41c3cfb46fcf2b9b3a57a2cb2e1bbe2adb /risc-v/riscv_extras_embed_sequential.lem | |
| parent | c6d639e0f03053b905a9cb0ab6929f4efe6153f4 (diff) | |
added RISC-V load-acquire
Diffstat (limited to 'risc-v/riscv_extras_embed_sequential.lem')
| -rw-r--r-- | risc-v/riscv_extras_embed_sequential.lem | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem index f6709ff7..518a5a15 100644 --- a/risc-v/riscv_extras_embed_sequential.lem +++ b/risc-v/riscv_extras_embed_sequential.lem @@ -4,11 +4,15 @@ open import Sail_impl_base open import Sail_values open import State -val MEMr : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserve : (vector bitU * integer) -> M (vector bitU) - -let MEMr (addr,size) = read_mem false Read_plain addr size -let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size +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 val MEMea : (vector bitU * integer) -> M unit val MEMea_conditional : (vector bitU * integer) -> M unit |