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 | |
parent | 8b39adca2fafad9037f21202782ac29c776b7526 (diff) | |
download | sail-riscv-273ec8b0715b39844101c8081114f2697f291312.zip sail-riscv-273ec8b0715b39844101c8081114f2697f291312.tar.gz sail-riscv-273ec8b0715b39844101c8081114f2697f291312.tar.bz2 |
Support DMB/DSB domains
-rw-r--r-- | handwritten_support/riscv_extras.lem | 22 | ||||
-rw-r--r-- | handwritten_support/riscv_extras_sequential.lem | 22 | ||||
-rw-r--r-- | model/riscv_analysis.sail | 22 | ||||
-rw-r--r-- | model/riscv_insts_base.sail | 22 |
4 files changed, 44 insertions, 44 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 diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail index 34572f8..1f0f59b 100644 --- a/model/riscv_analysis.sail +++ b/model/riscv_analysis.sail @@ -112,15 +112,15 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst FENCE(pred, succ) => { ik = match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_rw_rw), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_r_rw), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_r_r), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_rw_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_w_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_w_rw), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_rw_r), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_r_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_w_r), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_rw_rw ()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_r_rw ()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_r_r ()), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_rw_w ()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_w_w ()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_w_rw ()), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_rw_r ()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_r_w ()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_w_r ()), (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => IK_simple (), @@ -131,12 +131,12 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst FENCE_TSO(pred, succ) => { ik = match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso ()), _ => internal_error("barrier type not implemented in initial_analysis") }; }, FENCEI() => { - ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i + ik = IK_simple (); // for RMEM, should morally be (Barrier_RISCV_i ()) }, LOADRES(aq, rl, rs1, width, rd) => { if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 14a626e..eab4bfc 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -566,15 +566,15 @@ mapping clause encdec = FENCE(pred, succ) function clause execute (FENCE(pred, succ)) = { match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_r_r), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_rw_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_w_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_w_rw), - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_rw_r), - (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_r_w), - (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_w_r), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw ()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw ()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_r_r ()), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_rw_w ()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_w_w ()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_w_rw ()), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_rw_r ()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_r_w ()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_w_r ()), (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (), @@ -619,7 +619,7 @@ mapping clause encdec = FENCE_TSO(pred, succ) function clause execute (FENCE_TSO(pred, succ)) = { match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso ()), (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (), _ => { print("FIXME: unsupported fence"); @@ -638,7 +638,7 @@ mapping clause encdec = FENCEI() <-> 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111 /* fence.i is a nop for the memory model */ -function clause execute FENCEI() = { /* __barrier(Barrier_RISCV_i); */ RETIRE_SUCCESS } +function clause execute FENCEI() = { /* __barrier(Barrier_RISCV_i ()); */ RETIRE_SUCCESS } mapping clause assembly = FENCEI() <-> "fence.i" |