aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
authorAlasdair Armstrong <alasdair.armstrong@cl.cam.ac.uk>2019-07-18 16:39:18 +0100
committerAlasdair Armstrong <alasdair.armstrong@cl.cam.ac.uk>2019-07-18 17:11:14 +0100
commit1714f50b4879329614064dcfd1cd1e14154711fe (patch)
tree622892976c778916582ae1aa2c48c86af712c23f /model
parent273ec8b0715b39844101c8081114f2697f291312 (diff)
downloadsail-riscv-1714f50b4879329614064dcfd1cd1e14154711fe.zip
sail-riscv-1714f50b4879329614064dcfd1cd1e14154711fe.tar.gz
sail-riscv-1714f50b4879329614064dcfd1cd1e14154711fe.tar.bz2
Revert "Support DMB/DSB domains"
Move this commit to new_barriers branch until we can update C/SMT/etc and make a new release of Sail for backwards compatability with the opam package This reverts commit 273ec8b0715b39844101c8081114f2697f291312.
Diffstat (limited to 'model')
-rw-r--r--model/riscv_analysis.sail22
-rw-r--r--model/riscv_insts_base.sail22
2 files changed, 22 insertions, 22 deletions
diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail
index 1f0f59b..34572f8 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 eab4bfc..14a626e 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"