Merge branch 'master' into vmem_ext

1 files changed, 45 insertions, 1 deletions

diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 0df5ce8..10f3117 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -17,7 +17,7 @@ function clause execute UTYPE(imm, rd, op) = {
   let off : xlenbits = EXTS(imm @ 0x000);
   let ret : xlenbits = match op {
     RISCV_LUI   => off,
-    RISCV_AUIPC => PC + off
+    RISCV_AUIPC => get_arch_pc() + off
   };
   X(rd) = ret;
   RETIRE_SUCCESS
@@ -564,6 +564,31 @@ union clause ast = FENCE : (bits(4), bits(4))
 mapping clause encdec = FENCE(pred, succ)
   <-> 0b0000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111
 
+/* For future versions of Sail where barriers can be parameterised */
+$ifdef FEATURE_UNION_BARRIER
+
+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) @ 0b00, _ : bits(2) @ 0b00) => (),
+
+    _ => { print("FIXME: unsupported fence");
+           () }
+  };
+  RETIRE_SUCCESS
+}
+
+$else
+
 function clause execute (FENCE(pred, succ)) = {
   match (pred, succ) {
     (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw),
@@ -584,6 +609,8 @@ function clause execute (FENCE(pred, succ)) = {
   RETIRE_SUCCESS
 }
 
+$endif
+
 mapping bit_maybe_r : bits(1) <-> string = {
   0b1 <-> "r",
   0b0 <-> ""
@@ -617,6 +644,21 @@ union clause ast = FENCE_TSO : (bits(4), bits(4))
 mapping clause encdec = FENCE_TSO(pred, succ)
   <-> 0b1000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111
 
+$ifdef FEATURE_UNION_BARRIER
+
+function clause execute (FENCE_TSO(pred, succ)) = {
+  match (pred, succ) {
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso()),
+    (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (),
+
+    _ => { print("FIXME: unsupported fence");
+           () }
+  };
+  RETIRE_SUCCESS
+}
+
+$else
+
 function clause execute (FENCE_TSO(pred, succ)) = {
   match (pred, succ) {
     (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso),
@@ -628,6 +670,8 @@ function clause execute (FENCE_TSO(pred, succ)) = {
   RETIRE_SUCCESS
 }
 
+$endif
+
 mapping clause assembly = FENCE_TSO(pred, succ)
   <-> "fence.tso" ^ spc() ^ fence_bits(pred) ^ sep() ^ fence_bits(succ)