aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
authorShaked Flur <fshaked@gmail.com>2019-07-18 10:13:31 +0100
committerShaked Flur <fshaked@gmail.com>2019-07-18 10:13:31 +0100
commit273ec8b0715b39844101c8081114f2697f291312 (patch)
treea44777972455050cee4005e1f8c4146a1d6fde2a /model
parent8b39adca2fafad9037f21202782ac29c776b7526 (diff)
downloadsail-riscv-273ec8b0715b39844101c8081114f2697f291312.zip
sail-riscv-273ec8b0715b39844101c8081114f2697f291312.tar.gz
sail-riscv-273ec8b0715b39844101c8081114f2697f291312.tar.bz2
Support DMB/DSB domains
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 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"