diff options
| author | Shaked Flur <fshaked@gmail.com> | 2019-07-18 10:13:31 +0100 |
|---|---|---|
| committer | Shaked Flur <fshaked@gmail.com> | 2019-07-18 10:13:31 +0100 |
| commit | 273ec8b0715b39844101c8081114f2697f291312 (patch) | |
| tree | a44777972455050cee4005e1f8c4146a1d6fde2a /handwritten_support | |
| parent | 8b39adca2fafad9037f21202782ac29c776b7526 (diff) | |
| download | sail-riscv-273ec8b0715b39844101c8081114f2697f291312.zip sail-riscv-273ec8b0715b39844101c8081114f2697f291312.tar.gz sail-riscv-273ec8b0715b39844101c8081114f2697f291312.tar.bz2 | |
Support DMB/DSB domains
Diffstat (limited to 'handwritten_support')
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 22 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras_sequential.lem | 22 |
2 files changed, 22 insertions, 22 deletions
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index da6106d..f4ade26 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -8,17 +8,17 @@ open import Sail2_prompt type bitvector 'a = mword 'a -let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw -let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw -let MEM_fence_r_r () = barrier Barrier_RISCV_r_r -let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w -let MEM_fence_w_w () = barrier Barrier_RISCV_w_w -let MEM_fence_w_rw () = barrier Barrier_RISCV_w_rw -let MEM_fence_rw_r () = barrier Barrier_RISCV_rw_r -let MEM_fence_r_w () = barrier Barrier_RISCV_r_w -let MEM_fence_w_r () = barrier Barrier_RISCV_w_r -let MEM_fence_tso () = barrier Barrier_RISCV_tso -let MEM_fence_i () = barrier Barrier_RISCV_i +let MEM_fence_rw_rw () = barrier (Barrier_RISCV_rw_rw ()) +let MEM_fence_r_rw () = barrier (Barrier_RISCV_r_rw ()) +let MEM_fence_r_r () = barrier (Barrier_RISCV_r_r ()) +let MEM_fence_rw_w () = barrier (Barrier_RISCV_rw_w ()) +let MEM_fence_w_w () = barrier (Barrier_RISCV_w_w ()) +let MEM_fence_w_rw () = barrier (Barrier_RISCV_w_rw ()) +let MEM_fence_rw_r () = barrier (Barrier_RISCV_rw_r ()) +let MEM_fence_r_w () = barrier (Barrier_RISCV_r_w ()) +let MEM_fence_w_r () = barrier (Barrier_RISCV_w_r ()) +let MEM_fence_tso () = barrier (Barrier_RISCV_tso ()) +let MEM_fence_i () = barrier (Barrier_RISCV_i ()) val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e val MEMea_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index 7715614..ac70ee5 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -8,17 +8,17 @@ open import Sail2_prompt type bitvector 'a = mword 'a -let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw -let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw -let MEM_fence_r_r () = barrier Barrier_RISCV_r_r -let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w -let MEM_fence_w_w () = barrier Barrier_RISCV_w_w -let MEM_fence_w_rw () = barrier Barrier_RISCV_w_rw -let MEM_fence_rw_r () = barrier Barrier_RISCV_rw_r -let MEM_fence_r_w () = barrier Barrier_RISCV_r_w -let MEM_fence_w_r () = barrier Barrier_RISCV_w_r -let MEM_fence_tso () = barrier Barrier_RISCV_tso -let MEM_fence_i () = barrier Barrier_RISCV_i +let MEM_fence_rw_rw () = barrier (Barrier_RISCV_rw_rw ()) +let MEM_fence_r_rw () = barrier (Barrier_RISCV_r_rw ()) +let MEM_fence_r_r () = barrier (Barrier_RISCV_r_r ()) +let MEM_fence_rw_w () = barrier (Barrier_RISCV_rw_w ()) +let MEM_fence_w_w () = barrier (Barrier_RISCV_w_w ()) +let MEM_fence_w_rw () = barrier (Barrier_RISCV_w_rw ()) +let MEM_fence_rw_r () = barrier (Barrier_RISCV_rw_r ()) +let MEM_fence_r_w () = barrier (Barrier_RISCV_r_w ()) +let MEM_fence_w_r () = barrier (Barrier_RISCV_w_r ()) +let MEM_fence_tso () = barrier (Barrier_RISCV_tso ()) +let MEM_fence_i () = barrier (Barrier_RISCV_i ()) val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e val MEMea_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e |